sensorEulerLedger_balanced
plain-language theorem explainer
The theorem shows that the concrete Euler ledger built from a defect sensor's real part and any finite prime support is balanced in the ledger forcing sense. Researchers constructing arithmetic bridges to physical recognition models cite it to confirm conservation at the first identification step. The proof is a one-line wrapper that unfolds the sensor definition and applies the general finite Euler ledger balance theorem with the sensor real-part positivity witness.
Claim. For any defect sensor with positive real part $σ$ and any finite set of primes $S$, the ledger whose recognition events are the Euler factors $p^{-σ}$ for $p ∈ S$ (together with their reciprocals) is balanced.
background
The Concrete Euler Ledger module builds explicit LedgerForcing.Ledger objects from prime Euler data at a fixed real exponent. A defect sensor is a structure carrying a charge (zero multiplicity), a realPart $σ > 0$ inside the critical strip, and the in_strip predicate. The sensor-indexed ledger definition simply instantiates the finite Euler ledger at that $σ$ over the supplied prime support converted to a list.
proof idea
The proof is a one-line wrapper. It unfolds the sensor-indexed ledger definition, which reduces to the finite Euler ledger at the sensor real part together with the positivity witness supplied by the sensor real-part positivity theorem, then applies the finite Euler ledger balance theorem exactly.
why it matters
This supplies the balance property required by the first concrete arithmetic identification theorem, which assembles balance, zero net flow, and explicit prime-event membership into a single ledger object. It is also invoked when constructing the canonical directed Euler ledger system attached to a sensor. In the Recognition Science setting it completes the initial arithmetic-to-ledger bridge step described in the module, furnishing a balanced concrete object before any appeal to the full physical thesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.