RealizedCollapseBoundaryApproaching
plain-language theorem explainer
The definition introduces a predicate asserting that the realized defect collapse scalar for any defect sensor with nonzero charge approaches the T1 boundary at zero. Researchers establishing the collapse mechanism within the Unified RH T1-bounded realizability architecture cite it when linking cost divergence to boundary transport. The predicate is introduced directly as the statement that the scalar can be made smaller than any positive epsilon by choosing a sufficiently large natural number N.
Claim. Let $s$ be a defect sensor with nonzero charge. The predicate holds precisely when the realized defect collapse scalar sequence satisfies: for every $ε > 0$ there exists a natural number $N$ such that the scalar at step $N$ is strictly less than $ε$.
background
The Unified RH module organizes T1-bounded realizability into four components: cost divergence (nonzero charge forces annular cost to grow unbounded), Euler trace admissibility (convergent nonvanishing carrier with bounded logarithmic derivative), physically realizable ledger (T1 defect uniformly bounded for the Euler carrier), and boundary transport (divergence forces the scalar proxy toward the T1 boundary at zero). The predicate concerns the concrete realized-defect collapse scalar that replaces the earlier structural axiom. Upstream results supply the Cost quantity from RSNative measurement and the collision-free and algebraic-tautology properties from OptionAEmpiricalProgram and SimplicialLedger that underwrite the sensor and scalar constructions.
proof idea
The definition directly encodes the limit condition as a universal quantification over positive epsilons with an existential witness N making the realized defect collapse scalar smaller than epsilon. No lemmas are invoked; the body is the primitive statement of boundary approach for the collapse observable.
why it matters
This definition supplies the realized collapse component inside the UnifiedRHCert structure that packages the full admissibility-based ontology-to-RH deduction. It is invoked by the CollapseBoundaryTransport class to link the collapse scalar to ledger boundary approach and by the theorem realizedDefectCollapseBoundaryApproaching_of_nonzero_charge that establishes the predicate for the canonical defect family. It fills the quantitative step from cost divergence to T1 boundary approach while the T1 barrier theorem prevents realizable ledgers from crossing zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.