eulerLedgerScalarState_eq_one
plain-language theorem explainer
The declaration shows that the Euler ledger scalar state evaluates to one for any defect sensor with zero charge and any natural number index. Workers on the T1-bounded realizability architecture cite it to anchor the zero-charge sector of the Euler carrier. The proof reduces directly by unfolding the conditional definition under the zero-charge hypothesis.
Claim. If $s$ is a defect sensor with charge zero, then for every natural number $N$ the Euler ledger scalar state satisfies $s(s, N) = 1$.
background
The module sets out a three-component architecture for the unified Riemann hypothesis that replaces an earlier claim of bounded total annular cost. DefectSensor is a structure recording the multiplicity (charge) of a zero of the zeta function together with its real part; the zero lies in the right half of the critical strip. The Euler ledger scalar state is defined by cases: it returns the constant 1 when charge is zero and otherwise returns the realized defect collapse scalar drawn from the canonical defect family.
proof idea
The proof is a one-line wrapper that applies simp to the definition of eulerLedgerScalarState together with the zero-charge hypothesis, yielding the constant value 1.
why it matters
This result supplies the base case for the zero-charge sector inside the PhysicallyRealizableLedger component of the unified RH architecture. It ensures the scalar proxy remains at the stable value 1 when the sensor carries no charge, consistent with the Euler trace admissibility already established upstream. The module uses this fact to separate the zero-charge regime from the cost-divergent nonzero-charge regime and to maintain uniform T1 defect bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.