sensorEulerLedger_identification
plain-language theorem explainer
For any DefectSensor and finite prime support the constructed ledger is balanced with zero net flow, contains each prime Euler event at ratio p to the minus real part together with its reciprocal, and carries total J-cost equal to twice the sum of J(p to the minus real part). Number theorists and RS sensor modelers cite this as the first explicit arithmetic-to-ledger bridge. The proof is a direct refinement that invokes four sibling lemmas for balance, net-flow vanishing, event membership, and the closed-form cost sum.
Claim. Let $L$ be the ledger built from a DefectSensor with real part $σ$ and a finite set $S$ of primes. Then $L$ is balanced, every agent has net flow zero, each prime $p∈S$ contributes the recognition event of ratio $p^{-σ}$ and its reciprocal to the event list of $L$, and the total ledger cost equals $2∑_{p∈S}J(p^{-σ})$.
background
A LedgerForcing.Ledger is a finite list of RecognitionEvent records, each carrying a positive real ratio together with source and target agents. The balanced predicate requires that the list of events is balanced in the double-entry sense. Ledger cost is the sum of individual event costs, where each event cost is given by the J function from CostAlgebra. Net flow at an agent is the sum of signed log-ratios of events incident on that agent. The reciprocal operation on an event simply swaps source and target while inverting the ratio. The module constructs, for any positive real exponent σ and finite prime support, an explicit Ledger whose ratios are exactly the Euler factors p^{-σ} together with their reciprocals; when σ is taken from a DefectSensor this yields a concrete arithmetic ledger indexed by the sensor coordinate.
proof idea
The tactic proof opens with refine and supplies four subgoals. The first subgoal is discharged by the sibling lemma sensorEulerLedger_balanced. The second subgoal (universal net-flow zero) is discharged by sensorEulerLedger_net_flow_zero. The third subgoal (membership of each prime event and its reciprocal) is discharged by primeEulerEvent_mem_sensorEulerLedger together with the reciprocal membership lemma. The fourth subgoal (cost formula) is discharged directly by sensorEulerLedger_cost_formula.
why it matters
This theorem supplies the first fully concrete bridge object from finite Euler-product arithmetic into the ledger language of the RS sensor framework. It realizes the arithmetic-to-ledger identification step described in the module documentation and thereby populates the initial stage of the Recognition Science forcing chain with an explicit, balanced, zero-net-flow ledger whose total J-cost is given by a closed sum. Because the used-by list is empty the declaration currently stands as a foundational lemma rather than an intermediate step toward a larger parent theorem such as RSPhysicalThesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.