foldl_addEvent_length
plain-language theorem explainer
A ledger assembled from the empty list by n successive double-entry postings has length exactly 2n. Cosmology proofs that fix the eight-tick cosmogenesis ledger size cite this. The argument is induction on n, reducing each step by the two-event length of a single paired posting.
Claim. For any map $f:\mathbb{N}\to Q$ from naturals to rational recognition events and any $n\in\mathbb{N}$, if $L_n$ is the list obtained by folding $t\mapsto$ (post $f(t)$ with its reciprocal) over $\{0,\ldots,n-1\}$ starting from the empty list, then $|L_n|=2n$.
background
The module supplies a computable $\mathbb{Q}$-mirror of the real cosmogenesis dynamics in PreBigBang and FirstTick. A QEvent is a recognition event (source, target, rational ratio). Double-entry posting addEvent prepends an event together with its reciprocal (source/target swapped, ratio inverted), so each tick contributes two ledger rows.
The length lemma for one posting states that each paired add increases list length by exactly two. Cosmogenesis itself is the fold of eight such postings (one per edge of the 3-cube cadence) onto the empty ledger. The present result lifts the single-step length identity to an arbitrary number of folded postings, independent of the particular event map.
proof idea
Induction on $n$. The zero case is immediate by simplification of range and foldl on the empty list. In the successor step, rewrite range (k+1) via range_succ and split the fold with foldl_append; the remaining one-step fold is just addEvent on the inductive list. Apply the single-posting length lemma (addEvent_length) and the inductive hypothesis, then close with ring to obtain $2(k+1)$.
why it matters
Downstream, cosmogenesis_length instantiates this lemma at $n=8$ (and the cosmogenesis event map) to conclude that the full eight-tick ledger has length 16: eight ticks, each paired. That count is the discrete footprint of the T7 eight-tick octave inside the computable simulation. The module's conservation theorem (cosmogenesis_conserves) and cost identities sit on the same ledger object; fixing its cardinality is the elementary bookkeeping step before those invariants are stated. No open scaffold: the result is fully proved and only serves the length specialization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.