eulerLedgerScalarState_eq_one
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not address sensors with nonzero charge.
- Does not establish any bound on the scalar state when charge is nonzero.
- Does not prove convergence or admissibility properties of the Euler trace.
- Does not supply numerical evaluations or approximations for any N.
formal statement (Lean)
454theorem eulerLedgerScalarState_eq_one (sensor : DefectSensor)
455 (hzero : sensor.charge = 0) (N : ℕ) :
456 eulerLedgerScalarState sensor N = 1 := by
proof body
Term-mode proof.
457 simp [eulerLedgerScalarState, hzero]
458
459/-- In the nonzero-charge sector, the Euler ledger scalar is the concrete
460realized collapse observable. -/