TraceCertificates
plain-language theorem explainer
Bundles five kernel-checkable certificates for the seed-2 cosmogenesis ledger: sixteen posted events, unit flow product at agent 0, eight-tick cadence, nine-vertex Gray-code cycle, and strictly positive first-tick J-cost. Cosmologists and RS auditors cite it as the typed interface the golden-trace microkernel must discharge. As a structure of propositions it has no proof body; instances are built by applying the conservation and length lemmas.
Claim. A record of five certificates for the rational cosmogenesis simulation with seed $2$: the ledger has length $16$; the flow product at agent $0$ equals $1$; the cadence range has length $8$; the Gray-code cycle on the $3$-cube has length $9$; and the recognition cost $J$ of the initial recurrence value is strictly positive.
background
The module supplies a computable mirror over $\mathbb{Q}$ of the real-valued PreBigBang and FirstTick dynamics. Events are double-entry posted (ratio $r$ with $r^{-1}$); cost is the rational $J(x)=(x+x^{-1})/2-1$; conserved $\sigma$ is the multiplicative flow product of ratios touching each agent. Double-entry multiplies by $r\cdot r^{-1}=1$, so the product is invariant.
The cosmogenesis ledger posts eight ticks, one per edge of the $3$-cube cadence, each paired by double-entry, hence sixteen events. The cycle is the Gray-code Hamiltonian walk on the cube closed to its start (nine vertices, eight edges). The recurrence $r\mapsto 1+1/r$ from a positive seed yields exact Fibonacci convergents to $\varphi$.
Upstream: flow product is the product of per-event contributions; cosmogenesis folds double-entry posting over eight ticks from the empty ledger; $J$ is the canonical recognition cost over $\mathbb{Q}$.
proof idea
Structure definition, not a proved theorem. Each field is a proposition specialized to seed $2$: ledger length equals $16$; flow product at agent $0$ equals $1$; the eight-tick range has length $8$; the closed Gray-code cycle has length $9$; and $J$ of the seed (recurrence at step $0$) is strictly positive. No tactics or lemmas fire here. The structure only packages the certificate interface that a downstream instance must inhabit by citing the length, conservation, and positivity lemmas.
why it matters
The sole consumer constructs an inhabited instance for seed $2$, discharging each field via the cosmogenesis length lemma, the proved flow-product conservation at every agent, the tick-count identity, the cycle-length fact, and first-tick cost positivity. That instance is the Lean-side mirror of the Python golden-trace microkernel, so the conservation law and cadence geometry become typed, kernel-checked data rather than runtime asserts.
Framework landmarks: the eight-tick octave (T7) appears as the cadence length and the $3$-cube Gray code (D=3, T8); the recurrence seed feeds the $\varphi$-ladder of Fibonacci convergents (T6). The bundle closes the computable half of the cosmogenesis story against the real-valued FirstTick ledger-cost theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.