trace_certificates_seed2
plain-language theorem explainer
Kernel-checked certificates for the canonical seed-2 cosmogenesis run over rationals: sixteen ledger events, flow-product σ equal to 1 at agent 0, eight-tick cadence, nine-vertex closed cycle, and strictly positive first-tick J-cost. Anyone matching the computable cosmogenesis mirror to the Python microkernel would cite this bundle. The proof is a term-mode structure instance wiring five already-proved lemmas.
Claim. The seed-$2$ cosmogenesis ledger satisfies the full certificate bundle: its length is $16$; the multiplicative flow product at agent $0$ equals $1$; the cadence list has length $8$; the closed cycle walk has length $9$; and the first-tick cost $J(r_0)$ is strictly positive, where $r_0$ is the initial ratio of the self-similar recurrence $r \mapsto 1+1/r$ started at $2$.
background
This module supplies a computable rational mirror of the real-valued PreBigBang and FirstTick dynamics. Recognition events are posted over $\mathbb{Q}$ by double-entry: each tick adds a ratio event together with its reciprocal, so the multiplicative flow product at every agent is multiplied by $r \cdot r^{-1} = 1$ and stays invariant. The summed $J$-cost climbs by $2J(r)$ per tick, matching the real ledger increment.
The cosmogenesis ledger itself is eight ticks folded onto the empty list, one per edge of the 3-cube cadence. For any positive seed the flow product after the full run is exactly $1$ at every agent (proved, no decide). The self-similar recurrence $r \mapsto 1+1/r$ started at seed $2$ yields the Fibonacci convergents $2, 3/2, 5/3, 8/5, \ldots$ converging to $\varphi$, so $\varphi$-emergence is visible as an exact rational sequence.
The certificate structure packages five concrete equalities and inequalities that the Python microkernel also checks for the golden-trace run. Upstream lemmas already establish length $16$, $\sigma$-conservation for every positive seed, the eight-tick count, the nine-vertex cycle, and positivity of the first-tick cost at seed $2$.
proof idea
Term-mode structure instance. Each field is discharged by a single upstream lemma specialized to seed $2$:
- event count from the general length theorem (eight paired postings give sixteen events);
- $\sigma$ at agent $0$ from the conservation theorem, with positivity of $2$ by
norm_num; - cadence length from the trivial eight-tick count;
- cycle length from the native decision that the cadence walk has nine vertices;
- first-tick cost positivity from the dedicated seed-$2$ positivity lemma.
No new arithmetic is performed here; the instance only assembles the five certificates into one record.
why it matters
This is the kernel-side seal that the canonical seed-$2$ run really does what the Python microkernel claims: sixteen events, conserved $\sigma$, eight-tick octave cadence, closed nine-vertex walk, and a strictly positive opening $J$-cost. In the Recognition forcing chain the eight-tick period is landmark T7; the rational recurrence making $\varphi$ emerge as Fibonacci convergents is the computable face of T6. Because conservation and length hold for every positive seed, specializing to $2$ is the natural golden-trace witness rather than an ad-hoc choice.
No downstream Lean theorem currently consumes the bundle (used-by is empty), so its role is documentary and audit-facing: a single named object a referee can point at when asking whether the simulation certificates are proved rather than merely evaluated. It closes the gap between the real-analytic FirstTick development and the runnable rational ledger without introducing sorry or runtime decide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.