BoundaryApproaching
plain-language theorem explainer
BoundaryApproaching encodes the property that a physically realizable ledger's scalar proxy state sequence can be driven arbitrarily close to zero. Researchers working on T1 boundary exclusion and the Unified RH contradiction for nonzero charge cite this definition to isolate the forbidden limit behavior. It is introduced as a direct universal-existential quantifier over the scalarState function supplied by the PhysicallyRealizableLedger instance.
Claim. A physically realizable ledger attached to a defect sensor is boundary-approaching if its scalar proxy state sequence satisfies: for every $ε > 0$ there exists $N ∈ ℕ$ such that the state at refinement depth $N$ is strictly less than $ε$.
background
In the Unified RH module a DefectSensor is a structure holding the integer charge (multiplicity of a zeta zero) and its real part. The PhysicallyRealizableLedger class instance supplies an admissible Euler trace together with a scalarState : ℕ → ℝ that remains positive and whose defect (equal to the J-functional) stays uniformly bounded. The module document replaces earlier total-cost bounds with three components: cost divergence for nonzero charge, Euler trace admissibility, and the realizable ledger interface that carries the bounded-defect scalar proxy.
proof idea
This is a direct definition that encodes the limit condition on the scalar proxy state. It is used verbatim as the target predicate in downstream theorems such as realizable_not_boundary_approaching and bridge_contradiction_core.
why it matters
The definition supplies the predicate negated by the T1 boundary exclusion theorem and appears inside the certificate T1BoundaryExclusionCert. It is the final link in the chain from cost divergence through DivergenceWitnessesBoundary to the ontological contradiction for nonzero-charge sensors. In the Recognition Science framework it implements the T1 step that forbids approach to the x=0 boundary, consistent with nothing_cannot_exist.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.