ledger_cost_foldl_with_offset
plain-language theorem explainer
This lemma establishes that the left-fold accumulation of recognition-event costs starting from an arbitrary real accumulator equals the accumulator plus the total cost computed from zero. It is cited in constructions of finite Euler ledgers from prime data within the Recognition Science arithmetic-to-ledger bridge. The proof is a direct induction on the event list that unfolds foldl and closes with ring arithmetic.
Claim. Let $(e_i)$ be any finite list of recognition events and let $a$ be any real number. Then the left-folded sum satisfies $a + J(e_1) + J(e_2) + ... + J(e_n) = a + (J(e_1) + J(e_2) + ... + J(e_n))$, where each $J(e_i)$ is the J-cost of the event ratio.
background
The Concrete Euler Ledger module constructs explicit finite ledgers whose recognition-event ratios are the Euler factors $p^{-σ}$ together with their reciprocals, for positive real $σ$ and finite prime support. A RecognitionEvent is a structure carrying source and target indices plus a positive real ratio; its cost is defined as the J-function applied to that ratio. The module supplies the first concrete, balanced arithmetic ledger indexed by the sensor strip coordinate, with double-entry balance and zero net flow by construction, but does not yet reach the full RSPhysicalThesis.
proof idea
Proof by induction on the list of events. The nil case is immediate from the definition of foldl on the empty list. In the cons case, unfold the foldl definition, apply the inductive hypothesis once to the updated accumulator and once to zero, then equate the two sides with the ring tactic.
why it matters
The identity is used by add_event_cost_formula to show that appending one paired event contributes exactly twice its single-event cost to the total ledger cost. It therefore supports the explicit total-cost formula in terms of J that appears in the finiteEulerLedger theorems of the same module. This supplies the arithmetic-to-ledger identification step that realizes a balanced, zero-net-flow ledger from prime Euler data, consistent with the Recognition Composition Law and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.