T1BoundaryExclusionCert
plain-language theorem explainer
The T1 boundary exclusion certificate states that any physically realizable ledger attached to a defect sensor cannot have its scalar proxy state driven arbitrarily close to zero. Number theorists deriving the Riemann hypothesis from Recognition Science principles cite this result to establish that T1-bounded trajectories remain bounded away from the non-existence boundary. The certificate is realized by a direct appeal to the realizable_not_boundary_approaching lemma.
Claim. A certificate asserting that for every defect sensor with a physically realizable ledger, the scalar proxy state $x_N$ does not approach the boundary: it is not the case that for all $ε > 0$ there exists $N ∈ ℕ$ such that $x_N < ε$.
background
DefectSensor records the multiplicity (charge) and real part of a zero of ζ, located in the right half of the critical strip. BoundaryApproaching is the predicate that a ledger's scalar proxy state can be made smaller than any positive ε. PhysicallyRealizableLedger is the class requiring an admissible Euler trace, positive scalar states at every depth, and uniformly bounded T1 defects. This module extracts the T1 boundary exclusion theorem, which shows that T1-bounded physically realizable ledgers cannot approach the non-existence boundary x=0. It imports from UnifiedRH the key definitions for the ontology route to the Riemann hypothesis.
proof idea
The structure is a definition whose single field is witnessed by applying the lemma realizable_not_boundary_approaching to the sensor. This is a one-line wrapper that discharges the negation of BoundaryApproaching using the bounded defect property of the ledger.
why it matters
This certificate feeds directly into the decomposed data structures RSPhysicalThesisData and RSPhysicalThesisDataLogic, which assemble the full physical thesis for the Riemann hypothesis. It closes the T1 boundary exclusion step in the Recognition Science derivation, confirming that admissible ledgers stay positive and bounded away from zero. The result supports the ontology route by ensuring physical realizability implies non-approaching behavior.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.