add_event_cost_formula
plain-language theorem explainer
The theorem states that adjoining a paired recognition event to any ledger increases its total cost by exactly twice the single-event cost. Number theorists building finite Euler ledgers from prime data in Recognition Science cite this when deriving explicit aggregate cost expressions. The proof is a direct term reduction that unfolds the cost and addition definitions, applies reciprocity to pair the costs, invokes the fold-with-offset accumulation lemma, and closes with algebraic simplification.
Claim. For any ledger $L$ and recognition event $e$, the total cost of the ledger obtained by adjoining $e$ and its reciprocal satisfies $C(L + e) = 2J(r) + C(L)$, where $C$ denotes ledger cost, $J$ is the recognition cost function, and $r$ is the ratio of $e$.
background
A LedgerForcing.Ledger is a finite list of RecognitionEvents together with a double-entry balance witness. Each RecognitionEvent carries a positive real ratio; its event_cost is defined as $J$ of that ratio, where $J$ is the symmetric cost function calibrated in the LedgerFactorization structure. The ledger_cost is the sum of event_cost over the event list, implemented via foldl. The add_event operation prepends both an event and its reciprocal while preserving balance by construction. The upstream reciprocity theorem asserts that event_cost of an event equals event_cost of its reciprocal, which follows from $J$-symmetry. The module constructs concrete finite Euler ledgers whose event ratios are the prime terms $p^{-σ}$ and their reciprocals, providing an explicit arithmetic model whose total cost is expressed via the present formula.
proof idea
The term proof unfolds ledger_cost and add_event, replaces the foldl on a cons cell with the corresponding recursive step, rewrites the paired addition using the reciprocity theorem, applies the ledger_cost_foldl_with_offset lemma to shift the accumulation, and finishes with the ring tactic for the resulting arithmetic identity.
why it matters
This result supplies the explicit total-cost formula required by the downstream finiteEulerLedger_cost_formula theorem, which in turn closes the arithmetic-to-ledger identification step described in the module documentation. It thereby supports the construction of balanced, zero-net-flow Euler ledgers indexed by the sensor real-part coordinate. Within the Recognition framework the lemma instantiates the general ledger_cost definition for the concrete prime-supported case that precedes the full RSPhysicalThesis identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.