PhysicallyRealizableLedger
plain-language theorem explainer
A defect sensor carries a physically realizable ledger when it supplies an admissible Euler trace, a strictly positive scalar proxy state, and a uniform bound on the T1 defect of that state. Number theorists bridging arithmetic Euler data to the ontology layer cite this interface to enforce T1-bounded realizability. The declaration is a structure definition that packages the three fields required by the T1-bounded realizability architecture.
Claim. A defect sensor admits a physically realizable ledger when it possesses an admissible Euler trace, a map $Nmapsto x_N$ with $x_N>0$ for every natural number $N$, and a constant $K$ such that the defect $J(x_N)$ remains at most $K$ for all $N$.
background
The module replaces an earlier total-cost claim with a three-component architecture separating cost divergence, Euler trace admissibility, and T1-bounded realizability. EulerTraceAdmissible requires a RegularCarrier covering the disk from Re(ρ) to the critical line, with nonvanishing values and bounded logarithmic derivative for all σ>1/2. The defect functional is defined as defect(x)=J(x) for positive x, and the scalar proxy state is required to stay strictly positive while its defect remains uniformly bounded.
proof idea
This is a structure definition that directly encodes the three required fields: the admissible Euler trace, the scalar state map, and the uniform defect bound. No lemmas are applied; the declaration serves as the interface for downstream realizability theorems.
why it matters
This interface supplies the realizability component of EulerLedgerOntologyInterface and is used in concreteEulerLedgerOntologyInterface_exists to connect directed Euler ledgers to the ontology layer. It enforces that realizable ledgers cannot approach the T1 boundary x=0, consistent with the nothing_cannot_exist principle inside the T1-bounded realizability architecture. The construction sits between proved Euler trace admissibility and the remaining external bridge hypothesis for boundary transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.