sensor_realPart_pos
plain-language theorem explainer
The real part of any defect sensor is strictly positive by the right-half critical-strip placement of its zero. Researchers constructing arithmetic ledgers from Euler factors cite this to guarantee that the exponents yield positive real ratios less than one. The proof is a one-line linear-arithmetic discharge of the first component of the sensor's in-strip hypothesis.
Claim. Let $s$ be a defect sensor whose associated zero of the reciprocal zeta function lies in the right half of the critical strip. Then the real part of $s$ satisfies $0 < s$.
background
A defect sensor is a structure recording an integer charge (the multiplicity of a zero of zeta) together with a real number that is the real part of that zero location; the in-strip predicate asserts that this real part lies strictly between 0 and 1. The Concrete Euler Ledger module builds a finite LedgerForcing ledger whose recognition events are the Euler factors $p^{-s}$ and their reciprocals, indexed by the same real part $s$ taken from the sensor. This supplies the first fully concrete arithmetic object that is balanced by construction and has zero net flow.
proof idea
The proof is a one-line term that applies linear arithmetic to the first projection of the in-strip field carried by the input sensor.
why it matters
The result is invoked by sensorEulerLedger and by the membership theorems that place prime Euler events inside the sensor-indexed ledger; it thereby feeds the identification theorem establishing balance, zero net flow, and an explicit total J-cost formula. In the Recognition framework it ensures the exponents remain positive, so that each prime event carries a positive J-cost consistent with the forcing chain from T5 (J-uniqueness) onward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.