Lean 4 · Formal audit

Machine-verified audit

The Emergence of Time and Space

A formal account of how temporal and spatial structure arise from a primitive state, checked by the Lean 4 kernel. Every theorem below carries a proof; the badges report what is proved rather than assumed.

source: Emergence_of_Time_and_Space.lean generated: — imports: — items: —
Claim checks

Summary

Items grouped by kind. One colour per kind throughout the report.

Dependency graph

Nodes are formal items, coloured by kind. Edges point from an item to what it depends on.

Loading interactive graph…

Results

All formal items, grouped by section.

Implications

What the formalization teaches, read through the same honesty taxonomy as the audit.

The 0 and 1 doctrine

The primitive is literally {one, zero} = {1, 0}: zero is the finite-transition floor — the fastest a state can change to another state (the minimum interval), from which the speed of light c emerges (light is not a separate primitive; c is the late expression of the finite-transition limit, §9) — and one is everything else: the superforce, a single unified interaction. Every dimensionless quantity is forced by their involution, tick, and loop closure: 2 (involution period), 3 (minimal non-retracing loop), 6 = 2×3, 12, and the 8+3+1 census all fall out (sections 0–29, kernel-checked). The one dimensionless quantity not yet forced is the coupling: the observed 137 and 1836 are running (low-energy) values, not inputs — the fundamental input is the superforce "1", and the renormalization-group flow from 1 down to low energy is the dynamics frontier that would force them.

The method, not the numbers, is the result

The kernel cleanly separates the Standard Model's structural content from its numerical content. Machine-verified: the fermion census (12), the gauge dimensions (8·3·1), charge quantization, the confinement triples, Lorentz kinematics, the inverse-square law, the gauge group {±1}, the curvature spectrum, and closure⇔charge. Not contained — and provably not containable — are the dimensionless constants and any dynamics: the α⁻¹ = 137 and mₚ/mₑ = 1836 identities are single-point arithmetic fits (their "depth series" runs −210, 137, 21805, 1400637 — no coherent sequence, no prediction). The result is a proof-of-concept that particle-physics structure is finitely axiomatizable: countable, decidable, and kernel-verifiable on a six-element lattice.

Closure, charge, and gap are one phenomenon

Sections 7, 20c and 24 compose into the theory's deepest statement: a phase closes with a distinct partner if and only if the gauge group moves it, if and only if it carries charge. The gauge-invariant phases {0,3} are exactly the ones that never close — the massless sector. This is a discrete shadow of the center-symmetry mechanism of confinement: in QCD the ℤ₃ center of SU(3) governs confinement, and the photon stays massless because U(1) is unbroken. Here the CRT split ℤ₆ ≅ ℤ₂ × ℤ₃ carries the same two factors — ℤ₃ matches the color triplet, ℤ₂ the matter/antimatter role. Gapped versus massless is a property of group action on a finite ring, not of a Hamiltonian.

Why Lorentz invariance is so robust

The Euclidean budget shows the light cone and time dilation are an exact Pythagorean identity, scale-covariant at every refinement. There is no O(γ) correction to the dispersion relation because the constraint is refinement-invariant — the same identity at every scale. That is why Lorentz invariance survives to extreme precision: it is not an emergent approximation but a symmetry of the counting. The caveat the file itself records: the Euclidean (L2) versus taxicab (L1) choice is an input, not a derivation.

The arrow of time is not in the clock

The tick is a period-2 involution — time-reversible by construction. Direction cannot come from the map; it must live in a monotone quantity the theory does not yet contain. The lesson is precise: the arrow of time is a consequence, not a primitive.

The negative results are boundaries

The method fails, provably, on: exact constants (137/1836 are arbitrary polynomials tuned to land on them), spin-statistics (assumed via exchangeSign := (−1)ⁿ), the charge table (an input), and dynamics (no amplitude, no cross-section). These are not defects to patch — they are the boundary of what a finite, decidable kernel can contain. Any claim to derive them from a finite lattice is, by construction, numerology.

The one falsifiable point

The CHSH grid ceiling is the single place the theory differs from quantum mechanics: a six-fold grid caps CHSH at 5/2, below Tsirelson's 2√2, while Bell experiments already measure 2.73 ± 0.02 — about 11σ above the ceiling. The forced, honest reading is that the ℤ₆ structure is a substrate symmetry, not a measurement-basis symmetry. That is not a dodge; it is a precise boundary on what the lattice may be.

Causal order: the 2026 connection

A 2026 literature sweep (arXiv, retrieved 2026-09-07) shows indefinite causal order (ICO) is now experimentally real — device-independently — while its theoretical limits are being tightened. Key anchors: device-independent ICO 2508.04643 (24σ causal-inequality violation), 2506.16949 (18σ above the definite-order bound), 2604.11878 (causal witness C_W = −0.305); tightened limits 2609.05355 (no asymptotic metrological advantage), 2608.04685 (switch memory not genuinely quantum), 2605.08351 (physically realizable class = QC-QCs); and "time as gluing" — 2601.16494 (ICO = failure-to-glue of definite orders; parametric time τ), 2603.11571 ("subtime"; the arrow of time emerges through decoherence), 2608.16694 (event order vs intervention order), review 2606.19438.

The mapping onto the kernel is clean, and — so far — absent from the literature:

  • closing sectors (color 8, weak 3) → gapped/confined = definite causal order (glued temporal axes)
  • never-closing gauge singlet {0,3} → gapless/long-range (§24) = indefinite causal order (failure-to-glue)
  • tick is an involution; the arrow is not primitive (§1) = Borrill's "subtime": the arrow emerges from decoherence
  • quarks = localized temporal binding (§16) = color charge is a definite temporal/causal order

A numeric pass (tools/explore_causal.cjs) block-diagonalizes the kinetic 6-cycle by the negation gauge {±1}: the symmetric (gauge-invariant) sector is 4-dimensional and contains the massless mode (λ=0); the antisymmetric (charged) sector is 2-dimensional. Adding the gauge-charge mass term — the antisymmetrizer (I−N)/2 — gaps the charged sector by exactly μ while the massless mode survives untouched: the closure⇔charge⇒gap split, demonstrated. Honest caveat: μ is a hand-set coupling (structure forced, value not derived), and this is a single-site toy — a full delocalized massless gauge boson needs a proper lattice-gauge field.

This reframes the dynamics step: build a discrete dynamics where causal order is a degree of freedom — closure is the "definite-order gluing", its gauge-invariant complement is the "indefinite / never-closing" sector — and test whether confinement (gapped) and a long-range carrier (gapless) emerge from one mechanism.

First pass done (tools/lattice_gauge.cjs): 2D ℤ₃ (color) gauge shows Wilson-loop area-law confinement (string tension matches the analytic value); 3D ℤ₂ gauge shows the confinement→deconfinement transition (area → perimeter law, the massless photon) across β_c ≈ 0.76. And §29 formalizes the combinatorial split — the negation gauge fixes exactly 2 phases (massless) and moves 4 (gapped). On the coupling: the mass gap is exactly μ and the string tension is smooth in β, so μ is the theory's single dimensional input — not derivable from the combinatorics (matching §9's "one dimensional scale").

What the theory teaches for its own advancement

  1. Derive the inputs. Role = 2 and Axis3 = 3 are postulates. The loop-closure trichotomy already shows 3 is minimal for a non-retracing loop; a matching argument that 2 is the period of the involution would turn the primitive from assumed into forced minimality.
  2. Bridge the gapless gap. Section 24 exhibits the never-closing sector; the missing step is proving it actually yields inverse-square long-range behavior, tying fluxExponent = 2 to the singlet. This is the file's own "one remaining structural gap."
  3. Add a toy dynamics. A discrete transfer matrix on ℤ₆ with closure as weights would let the theory compute — a spectrum, a correlation — and test closure⇔gap numerically, turning classification into prediction.

The dynamics frontier — second pass

All three items above are now executed and machine-checked where possible. §30 derives Role = 2 (any fixed-point-free map needs ≥ 2 elements) and Axis3 = 3 (the minimal non-retracing loop count), so the two inputs are forced minima, not postulates. §31 pins the closure structure: on the moving phases {1,2,4,5} closure is a perfect matching (each phase has a unique distinct partner; closing twice returns home), and {0,3} are exactly the self-conjugate phases. §32 derives n² − 1 as the unique quadratic through the closure-forced values 0, 3, 8 — the adjoint census 8+3+0 = 11, with the singlet 1 closing to 12 = |Dir6|. §33 proves the negative boundary: the only bijections of the primitive are id and inverse, so no deterministic map carries an arrow — direction must be extra-dynamical.

The numerics now span five tools. lattice_gauge.cjs (#1) shows 2D ℤ₃ area-law confinement and the 3D ℤ₂ deconfinement transition; polyakov_loop.cjs (#4) reproduces the Polyakov-loop order parameter (⟨P⟩: 0 → 1 across β_c). transfer_matrix.cjs (#2) and spectrum.cjs (#5) make closure⇔gap spectral: the charge gap opens with slope exactly 2 (ΔE_charge = β + 2μ) while the gauge-invariant {0,3} singlet's internal gap stays μ-independent (= β) — the never-closing sector does not confine. running_coupling.cjs (#3) extracts Creutz ratios from ℤ₃ Wilson loops, showing the coupling runs with scale (clean at weak coupling; the 1D toy has zero beta — running is a 2D/3D effect).

Honest boundary, unchanged: μ is hand-set (structure forced, value not derived), and none of this derives α⁻¹ = 137 or mₚ/mₑ = 1836 — those remain numerological. The §30 count match (singlet size = flux exponent = 2) bridges the gapless gap only at the counting level; the actual r⁻² falloff is still the open dynamics step.

Simulations

The forced results, animated. Every number here is a machine-checked theorem (T1), not a fit.

The seed and the tick

The two poles — extension vs. the rate floor — alternate under the involution. Period 2; directed succession; no null state (the contrast cannot be switched off).

Closure forces three axes

One axis cannot close; two axes retrace or stall; three axes close non-trivially (a→b→c→a). Space has three dimensions because two cannot close and four are not needed.

The charge partition

The unique positive-integer solution of x²+y²+z² = 9 is {1,2,2}; normalized by 3 these are {⅓, ⅔, ⅔} — the quark charges.

The gauge fixes 2, moves 4

The negation gauge N: x ↦ −x (mod 6) fixes {0,3} and swaps {1↔5, 2↔4}. A phase is massless exactly when the gauge leaves it put; gapped exactly when it is moved.

Speed limit and time dilation

Motion m and ticking t spend one Euclidean budget: m² + t² = c². Rest spends it all on ticking; the speed limit c spends it all on motion and time halts.

Curvature spectrum / extension↔tension

Six axes split into extension and tension; local curvature is the tension-minus-extension count. Over all 2⁶ subsets it is the binomial spectrum 1·6·15·20·15·6·1, and the role mirror sends C to −C.

The 60°/120° architecture

Expansion advances 60° per step (six spokes close a turn); contraction advances 120° per step (three spokes close the same turn). Contraction is exactly twice expansion.

The gauge census closes to 12

Colour 8 + weak 3 + substrate 0 + one singlet = 12 = |Dir6|. The four sectors assemble into the full direction ring; gravity contributes zero gauge bosons.

The CHSH ceiling 5/2

A six-fold setting grid caps CHSH at exactly 5/2 — above the classical bound 2, below Tsirelson's 2√2. Bell experiments already measure 2.73 ± 0.02, ~11σ above the ceiling.

Closure gaps the charged sector

The closure weight μ gaps the charged {1,2,4,5} sector linearly (ΔE = β + 2μ, slope exactly 2), while the singlet {0,3} sector's internal gap stays μ-independent (= β).

Area law vs perimeter law

2D ℤ₃ colour gauge confines: the Wilson loop obeys −log W ∝ R² (area law, string tension). 3D ℤ₂ gauge above β_c ≈ 0.76 deconfines: −log W ∝ R (perimeter law — the massless photon).

Two is the forced minimum

A fixed-point-free map needs at least 2 elements; on one element it has nowhere to go. The founding involution attains the minimum: |Role| = |PState| = 2.