realizedDefectCollapseScalar_pos
plain-language theorem explainer
The realized defect collapse scalar attached to any nonzero-charge defect sensor is strictly positive for every sample size N. Researchers on the T1-bounded realizability architecture cite this to guarantee positivity of the scalar proxy before proving its T1 defect is unbounded. The proof is a term-mode reduction that unfolds the scalar to the reciprocal of annular cost, invokes annularCost_nonneg, and closes with linarith.
Claim. Let $s$ be a defect sensor with nonzero charge $m$. For every natural number $N$, the realized defect collapse scalar satisfies $0 < 1/C_N$, where $C_N$ is the total annular cost of the canonical defect-sampled mesh of size $N$.
background
The Unified RH module implements a T1-bounded realizability architecture with four components: cost divergence for nonzero-charge sensors, Euler trace admissibility, physically realizable ledgers, and boundary transport. The defect functional equals the J-cost and vanishes at unity. A DefectSensor records the multiplicity (charge) and real part of a zeta zero in the critical strip. The canonicalDefectSampledFamily builds the sampled family from the chosen defect phase family. Annular cost sums ring costs over the mesh of size N.
proof idea
The proof unfolds the definition of the realized defect collapse scalar to expose its form as the reciprocal of annular cost on the mesh of the canonicalDefectSampledFamily. It applies one_div_pos.mpr to reduce to showing the cost is positive. Nonnegativity of the annular cost is obtained directly from the annularCost_nonneg theorem, after which linarith finishes the argument.
why it matters
This result supplies the positivity step required by eulerLedgerScalarState_pos for nonzero-charge sensors and underpins realizedDefectCollapseScalar_defect_unbounded, which shows the T1 defect grows without bound and therefore obstructs a uniformly realizable Euler ledger proxy. It closes the positivity half of the boundary transport component in the T1 architecture, confirming the divergence forced by nonzero charge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.