sensorEulerLedger_balanced
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not extend the construction to infinite prime supports.
- Does not establish positivity of individual recognition costs or explicit J-cost sums.
- Does not prove the full physical thesis or any dynamical evolution law.
- Does not address directed ledger properties or net-flow vanishing beyond the balance predicate.
formal statement (Lean)
188theorem sensorEulerLedger_balanced (sensor : DefectSensor) (support : Finset Nat.Primes) :
189 LedgerForcing.balanced (sensorEulerLedger sensor support) := by
proof body
Term-mode proof.
190 unfold sensorEulerLedger
191 exact finiteEulerLedger_balanced sensor.realPart (sensor_realPart_pos sensor) support.toList
192
193/-- The sensor-indexed concrete Euler ledger has zero net flow. -/