realizedDefectCollapseBoundaryApproaching_of_nonzero_charge
plain-language theorem explainer
Nonzero charge on a defect sensor forces the realized defect collapse scalar to approach the T1 boundary value of zero. Researchers working on the unified RH equivalence would cite this result to establish the divergence side of the boundary transport. The proof proceeds by case analysis on the target epsilon, invoking the unboundedness of the sampled family and algebraic manipulation of the scalar expression.
Claim. For any defect sensor with nonzero charge, the realized defect collapse scalar satisfies $∀ ε > 0, ∃ N ∈ ℕ$ such that the scalar at $N$ is less than $ε$.
background
DefectSensor carries a charge value whose nonzero status triggers cost divergence. RealizedCollapseBoundaryApproaching is the predicate asserting that the realized defect collapse scalar approaches the T1 boundary 0. The scalar itself is obtained from the canonical defect sampled family via annularCost on successive mesh points. In the Unified RH module this supplies the quantitative collapse mechanism that replaces the former structural axiom of bounded total annular cost. Upstream, the defect functional equals J for positive arguments, and defectSampledFamily_unbounded supplies the required N for any target bound B.
proof idea
The proof introduces the canonical defect sampled family and performs case analysis on whether ε ≤ 1. For ε ≤ 1 it sets B = ε^{-1} - 1, applies defectSampledFamily_unbounded to obtain N, then verifies 1 < ε(1 + annularCost) via linarith, field_simp and a short calc. For ε > 1 it applies the same unboundedness at B = 0, shows the scalar is strictly less than 1, and concludes via lt_trans.
why it matters
This theorem supplies the realized-collapse side of obstruction_structural_asymmetry, which juxtaposes approach to zero against the bounded Euler proxy. It is invoked directly in unified_rh_cert_of_bridge and thereby in the equivalence EBBA_iff_rh that identifies the bridge hypothesis with RH. Within the framework it realizes the T1 boundary approach for divergent costs, closing the quantitative replacement for the old structural axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.