pith. sign in
module module high

IndisputableMonolith.NumberTheory.BoundaryTransport

show as:
view Lean formalization →

BoundaryTransport module supplies the boundary transport certificate linking realized defect collapse to the Euler ledger boundary. Researchers deriving the Riemann hypothesis from the Recognition Composition Law cite it as the central physical bridge. The module composes Euler carrier realizability with T1 boundary exclusion into a certificate and its equivalences.

claimThe boundary transport certificate asserts that, for a T1-bounded physically realizable Euler carrier ledger, realized defect collapse transports to the actual Euler ledger boundary.

background

This module sits in the NumberTheory domain and assembles two upstream results for the RH-from-RCL derivation. EulerCarrierRealizability extracts the Euler carrier already realized in UnifiedRH.lean as a T1-bounded ledger into the file layout used by the derivation plan. T1BoundaryExclusion supplies the proved statement that a T1-bounded physically realizable ledger cannot approach the non-existence boundary at x=0.

proof idea

This is a definition module, no proofs. It imports the two upstream modules and defines the certificate together with its equivalences to EBBA and RH-core conditions.

why it matters in Recognition Science

The module feeds the boundary transport certificate directly into RSPhysicalThesisDecomposition, which replaces the opaque RSPhysicalThesis dependency with a structured bundle of ingredients needed for the RH proof. It supplies the main remaining RS physical bridge: realized defect collapse must transport to the actual Euler ledger boundary.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (5)