pith. sign in
module module high

IndisputableMonolith.NumberTheory.EulerCarrierRealizability

show as:
view Lean formalization →

The module establishes Euler trace admissibility for every defect sensor inside the T1-bounded realizability architecture. Researchers deriving RH from the Recognition Composition Law cite it to obtain the Euler carrier certificate. It organizes the material as concrete definitions and a ledger certificate rather than a single theorem.

claimEuler trace admissibility holds for every defect sensor in the T1-bounded realizability architecture.

background

The module imports UnifiedRH, whose doc-comment states it replaces the former OntologicalPrimeLedger (which asserted bounded total annular cost, directly contradicting the proved not_realizedDefectAnnularCostBounded) with a structured three-component architecture for T1-Bounded Realizability. Euler trace admissibility supplies one of those components for defect sensors. The module sits in the NumberTheory domain and exposes the Euler carrier as a named certificate.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds BoundaryTransport, the remaining physical bridge in the RH-from-RCL route that connects the concrete collapse scalar to the T1-bounded Euler realizability scalar, and RSPhysicalThesisDecomposition, which replaces the opaque RSPhysicalThesis dependency with a structured bundle of ingredients for the RH proof.

scope and limits

used by (2)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)