eulerLedgerScalarState_eq_collapse
plain-language theorem explainer
For any defect sensor with nonzero charge and any natural number N, the Euler ledger scalar state equals the realized defect collapse scalar. Researchers tracing scalar proxies in the nonzero-charge sector of the Unified RH architecture would cite this when reducing ledger states to collapse observables. The proof is a one-line simplification that unfolds the conditional definition of the ledger scalar and discharges the nonzero-charge hypothesis.
Claim. Let $m$ be the charge of a defect sensor with $m ≠ 0$. For any natural number $N$, the Euler ledger scalar state at that sensor equals the realized defect collapse scalar.
background
DefectSensor is a structure recording the multiplicity (charge) of a zero of the Riemann zeta function together with its real part; the sensor is used to index ledger states in the T1-bounded realizability architecture. The definition of eulerLedgerScalarState returns the constant 1 when charge is zero and otherwise delegates to realizedDefectCollapseScalar. The module replaces an earlier global bounded-cost claim with a three-component structure: cost divergence for nonzero charge, Euler trace admissibility, and a physically realizable ledger whose T1 defect remains uniformly bounded.
proof idea
One-line wrapper that applies simp to the definition of eulerLedgerScalarState together with the hypothesis that charge is nonzero, directly yielding the equality to realizedDefectCollapseScalar.
why it matters
The result supplies the nonzero-charge half of the ontological dichotomy theorem, which states that the cost scalar is T1-bounded if and only if charge equals zero. This is the Recognition Science ontological argument for the Riemann hypothesis: nonzero charge forces unbounded T1 defect and therefore non-realizability. It closes the ledger-scalar reduction step inside the T1-bounded realizability chain and feeds directly into the boundary-transport argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.