cosmogenesis_conserves
plain-language theorem explainer
After the full eight-tick cosmogenesis ledger is posted from any positive rational seed, the multiplicative flow product at every agent equals exactly 1. Cosmologists and ledger auditors cite this as the kernel-checked σ-conservation law in the computable ℚ mirror of PreBigBang/FirstTick. The proof is a direct application of the foldl invariance lemma, using positivity of the self-similar recurrence to guarantee every posted ratio is nonzero.
Claim. For every positive rational seed $s>0$ and every agent $a\in\mathbb{N}$, the flow product of the eight-tick cosmogenesis ledger built from $s$ equals $1$ at $a$: $\prod_e c_a(e)=1$, where each contribution $c_a(e)$ is the ratio (or its inverse) of an event touching $a$, and events are posted in double-entry pairs along the 3-cube cadence.
background
This module supplies a computable ℚ mirror of the real-valued cosmogenesis in PreBigBang and FirstTick. Recognition events are rationals: each QEvent carries source, target, and ratio. Double-entry posting (addEvent) always inserts an event together with its reciprocal (source/target swapped, ratio inverted), so the ledger stays balanced.
The conserved quantity σ is tracked multiplicatively as the flow product at an agent: the product of all event contributions touching that agent. Each double-entry pair multiplies the product by $r\cdot r^{-1}=1$, so the product is invariant under posting. Cosmogenesis posts eight such paired events, one per edge of the 3-cube cadence, with ratios from the self-similar recurrence $r\mapsto 1+1/r$ started at the seed. That recurrence stays positive for positive seeds and yields the Fibonacci convergents toward $\varphi$.
Upstream, flowProduct_foldl already proves that any ledger built solely by addEvent from the empty list has flow product 1 at every agent, provided every posted ratio is nonzero. Positivity of the recurrence supplies that hypothesis.
proof idea
One-line term proof. Instantiate the general foldl invariance theorem on the cosmogenesis construction: the event family is cosmoEvent seed, the length is 8, and the nonzero-ratio hypothesis is discharged by recurSeq_pos seed hs, which shows every recurrence value is strictly positive (hence nonzero) when the seed is positive. No induction or case split is written here; those live inside the foldl lemma.
why it matters
This is the kernel-checked conservation certificate for the full eight-tick cosmogenesis run. Downstream, trace_certificates_seed2 packages it as the sigma_at_zero field of the seed-2 trace certificate bundle, so auditors get a proved equality rather than a runtime check.
In the Recognition framework it closes the computable side of the ledger story that FirstTick tells over ℝ: double-entry forces σ multiplicative conservation, and the eight-tick octave (T7) is exactly the posting horizon. The same run exhibits the rational Fibonacci ladder converging to $\varphi$ (T6), so conservation and the golden fixed point appear together in one #eval-able object. No sorry remains on this path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.