euler_trace_admissible_concrete
plain-language theorem explainer
Every defect sensor admits an admissible Euler trace. Workers deriving the Riemann hypothesis from the Recognition Composition Law cite this when assembling the Euler carrier certificate for the T1-bounded ledger. The proof is a direct term application of the general admissibility theorem from UnifiedRH.
Claim. For every defect sensor with integer multiplicity $m$ and real part in the right half of the critical strip, the associated Euler trace is admissible.
background
DefectSensor is a structure with fields charge (the multiplicity of the zeta zero) and realPart (its real coordinate), restricted to the right half of the critical strip. EulerTraceAdmissible is the proposition bundle requiring carrier compatibility, nonvanishing, and positive derivative bounds. The module extracts the T1-bounded Euler carrier already realized in UnifiedRH into the layout needed for the RH-from-RCL derivation plan. Upstream, the theorem euler_trace_admissible states that every DefectSensor has an admissible Euler trace, following directly from sensor_carrier_compatible, carrier_nonvanishing, and carrierDerivBound_pos.
proof idea
The proof is a one-line wrapper that applies the upstream theorem euler_trace_admissible to the supplied sensor.
why it matters
This supplies the concrete admissibility instance required by the Euler realizability certificate eulerRealizableLedgerCert. It extracts the T1-bounded ledger result from UnifiedRH into the NumberTheory module to support the RH-from-RCL derivation. The step addresses Euler trace admissibility within the unification framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.