EulerTraceAdmissible
plain-language theorem explainer
EulerTraceAdmissible packages the predicate that any defect sensor admits an Euler trace once a regular carrier exists with radius exactly equal to the real-part offset from the critical line and positive, the carrier value stays nonzero above sigma equals one half, and the logarithmic derivative remains bounded by a positive function. Workers on T1-bounded realizability in the Unified RH architecture cite this structure to anchor the Euler carrier infrastructure before invoking boundary transport or ontological exclusion. The definition is a 3
Claim. A defect sensor $s$ admits an admissible Euler trace when there exists a regular carrier $C$ satisfying radius$(C) = $Re$($rho$_s) - 1/2 > 0$, $C(sigma) neq 0$ for every $sigma > 1/2$, and the derivative bound $M_C(sigma) > 0$ for every $sigma > 1/2$.
background
The Unified RH module organizes T1-bounded realizability into four components: cost divergence from annular coercivity, Euler trace admissibility, the physically realizable ledger, and boundary transport. EulerTraceAdmissible encodes the second component by requiring a regular carrier (imported from AnnularCost) that supplies a holomorphic nonvanishing envelope between Re(rho) and the critical line Re(s) = 1/2. The module document states that this admissibility follows from Euler instantiation data and replaces the earlier total-cost-boundedness claim that contradicted not_realizedDefectAnnularCostBounded. Upstream results supply the carrier radius definition and the admissible ledger predicate from Thermodynamics.
proof idea
The structure is a definition that directly assembles three carrier properties: existence of a compatible regular carrier with positive radius offset, universal nonvanishing of carrierValue above sigma = 1/2, and positivity of carrierDerivBound above the critical line. The companion theorem euler_trace_admissible constructs an instance by applying sensor_carrier_compatible, carrier_nonvanishing, and carrierDerivBound_pos from the Euler instantiation certificate.
why it matters
This definition supplies the admissibility interface required by EulerLedgerOntologyInterface and EulerRealizableLedgerCert, and it is invoked inside ontological_exclusion to obtain the contradiction with cost divergence once the boundary bridge is assumed. In the Recognition framework it anchors the Euler carrier for the phi-ladder and T1 defect bounds, completing the realizability path before the divergence-witness step. It touches the remaining external bridge hypothesis for boundary transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.