realizedDefectCollapseScalar_defect_unbounded
plain-language theorem explainer
The T1 defect of the realized collapse scalar grows without bound above for any nonzero-charge sensor. Researchers on the Recognition Science route to RH cite it to block a uniformly bounded T1 Euler ledger proxy. A short tactic proof obtains ε from the T1 cost barrier, N from the boundary-approaching lemma for nonzero charge, then applies the barrier inequality to the positive scalar and the closeness witness.
Claim. Let $J$ be the defect functional. For any sensor with nonzero charge, $J$ applied to the realized collapse scalar is unbounded above: for every real $C$ there exists a natural number $N$ such that $C < J$ of the scalar at step $N$.
background
The Unified RH module replaces earlier bounded-total-cost attempts with a three-component T1-bounded realizability architecture. CostDivergent holds for nonzero charge by annular coercivity; EulerTraceAdmissible holds for the Euler carrier; PhysicallyRealizableLedger requires the scalar proxy to keep T1 defect uniformly bounded. The defect functional equals $J(x)$ for $x>0$, where $J(x)=(x+x^{-1})/2-1$ diverges as $x$ approaches the T1 boundary at 0. The realized collapse scalar is the sensor-indexed proxy state whose approach to 0 is forced by divergence.
proof idea
The term-mode proof (written with tactics) introduces arbitrary $C$. It obtains positive ε and the implication $hε$ from the t1_cost_barrier lemma. It obtains $N$ from realizedDefectCollapseBoundaryApproaching_of_nonzero_charge using the sensor, nonzero-charge hypothesis, and ε. It then refines to that $N$ and applies $hε$ to the realized scalar, its positivity, and the boundary-closeness witness $hN$ to conclude the inequality.
why it matters
This result directly supplies the unboundedness needed for not_realizedDefectCollapseScalar_t1_bounded, which negates any uniform bound $K$ on the defect. That negation supports EBBA_iff_rh, equating the EulerBoundaryBridgeAssumption to the Riemann Hypothesis. It closes the obstruction step in the module chain: divergence forces the scalar toward the T1 boundary, which T1-bounded realizability forbids. It touches the remaining external bridge hypothesis that would otherwise discharge the architecture without assuming RH.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.