sensorEulerLedger_cost_formula
plain-language theorem explainer
The theorem equates the total ledger cost of the sensor-indexed Euler ledger to twice the sum of J(p^{-σ}) over the finite prime support, with σ the sensor real part. Recognition Science researchers bridging arithmetic Euler data to physical ledger models cite it for explicit cost calculations on prime-based sensors. The proof is a one-line wrapper that unfolds the sensor ledger definition and invokes the generic finite Euler ledger cost formula.
Claim. For a defect sensor with real part σ and finite prime support S, the total cost of the constructed Euler ledger L satisfies ledger_cost(L) = 2 ∑_{p ∈ S} J(p^{-σ}), where J is the recognition cost function on positive ratios.
background
The Concrete Euler Ledger module constructs a finite LedgerForcing.Ledger from Euler terms p^{-σ} (with reciprocals) for any positive real σ and finite prime set. Here σ is taken as the realPart of a DefectSensor, yielding a balanced double-entry ledger whose events carry explicit J-costs. The ledger_cost definition sums event costs via fold, while J itself satisfies the Recognition Composition Law from upstream MultiplicativeRecognizerL4 and ObserverForcing.
proof idea
One-line wrapper that unfolds sensorEulerLedger to expose the underlying finite Euler ledger, then applies simpa to the upstream finiteEulerLedger_cost_formula_J lemma at the sensor realPart (using the positivity fact sensor_realPart_pos) and the prime list extracted from the support.
why it matters
This supplies the explicit J-cost formula required by the downstream sensorEulerLedger_identification theorem, which asserts balance, zero net flow, and prime-event membership for the arithmetic ledger. It advances the Recognition Science forcing chain by furnishing the first fully concrete bridge object from Euler-product data into the ledger language, without yet reaching RSPhysicalThesis. The result feeds the directed Euler ledger system construction and closes an arithmetic-to-ledger identification step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.