realizable_not_boundary_approaching
plain-language theorem explainer
A physically realizable ledger cannot drive its scalar proxy state arbitrarily close to zero. Researchers formalizing the Riemann hypothesis inside Recognition Science cite the result to enforce T1 boundary exclusion on admissible Euler traces. The proof is a one-line wrapper that applies the upstream theorem physicallyRealizableLedger_not_boundaryApproaching.
Claim. Let $s$ be a defect sensor equipped with a PhysicallyRealizableLedger instance. Then the ledger is not boundary-approaching: there is no sequence of scalar proxy states $x_N$ satisfying $x_N < ε$ for every $ε > 0$.
background
The T1 Boundary Exclusion module isolates the consequence that T1-bounded physically realizable ledgers stay away from the non-existence boundary $x=0$. A DefectSensor at a point $ρ$ records the multiplicity (charge) of a zeta zero together with its real part, restricted to the right half of the critical strip. The class PhysicallyRealizableLedger sensor supplies an admissible Euler trace, a scalar proxy state function returning strictly positive reals, and a uniform bound on the T1 defect along the realized trajectory. BoundaryApproaching sensor asserts that the scalar state can be driven below any positive $ε$ at sufficiently large refinement depth $N$. The upstream theorem physicallyRealizableLedger_not_boundaryApproaching derives the negation from the T1 cost barrier and the axiom that nothing cannot exist.
proof idea
The proof is a one-line wrapper that directly invokes the upstream theorem physicallyRealizableLedger_not_boundaryApproaching on the supplied sensor.
why it matters
This theorem supplies the core content of the T1 boundary exclusion certificate t1BoundaryExclusionCert. It closes the loop from the PhysicallyRealizableLedger interface to the explicit exclusion of $x=0$ states, consistent with the Recognition Science forcing chain in which T1 enforces positive defect bounds that contradict boundary approach. The result touches the open question of whether every admissible trace remains strictly positive under the uniform T1 constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.