CollapseBoundaryTransport
plain-language theorem explainer
CollapseBoundaryTransport defines the class interface that carries boundary approach from the realized defect collapse scalar to the Euler ledger scalar proxy whenever charge is nonzero. Researchers formalizing the T1-bounded realizability architecture cite it when separating the collapse observable from the admissible Euler proxy. The declaration is a direct class definition whose single field encodes the required transport implication.
Claim. Let $sensor$ be a defect sensor equipped with a physically realizable ledger instance. For every nonzero charge $hm$, if the realized defect collapse scalar can be driven arbitrarily close to zero then the ledger scalar proxy state can also be driven arbitrarily close to zero.
background
The Unified RH module organizes T1-bounded realizability into four components: cost divergence for nonzero charge, Euler trace admissibility, the PhysicallyRealizableLedger class, and boundary transport. PhysicallyRealizableLedger sensor requires an admissible Euler trace together with a scalar proxy state whose T1 defect remains uniformly bounded. RealizedCollapseBoundaryApproaching sensor hm asserts that the concrete collapse scalar from the realized defect family approaches zero. BoundaryApproaching sensor asserts that the ledger scalar proxy itself approaches zero. The module replaces the earlier OntologicalPrimeLedger to avoid contradicting the proved annular cost divergence. Upstream results supply the one element in LogicInt and LogicRat together with the is instances for collision-free programs and edge lengths.
proof idea
This is a class definition with an empty proof body. It directly introduces the single axiom toLedgerBoundary that states the transport implication from RealizedCollapseBoundaryApproaching to BoundaryApproaching under the PhysicallyRealizableLedger instance.
why it matters
The definition supplies the transport interface required by EulerBoundaryBridgeAssumption, which recovers the old boundary-bridge statement as a theorem once the bridge hypothesis is supplied. It is used by euler_divergence_witnesses_boundary to convert divergence into boundary approach for the Euler proxy and by single_scalar_obstruction to prove that no scalar family approaching zero can carry a uniform T1 defect bound. In the Recognition Science framework it closes the link between the realized collapse observable and the T1 boundary forbidden for realizable ledgers, leaving the external bridge hypothesis as the remaining open question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.