euler_ledger_realizable
plain-language theorem explainer
The Euler ledger realizability definition supplies a physically realizable ledger instance for any defect sensor by delegating to the upstream unified result. Researchers on the RH-from-RCL derivation plan cite it to confirm the Euler carrier meets T1-bounded ledger conditions. The body is a one-line wrapper that invokes the upstream construction.
Claim. For any defect sensor with integer charge $m$ and real part location, the Euler ledger is a physically realizable ledger: it carries an admissible Euler trace, positive scalar proxy states at each refinement depth, and a uniform bound on the T1 defect.
background
DefectSensor is a structure with charge (multiplicity of the zeta zero) and realPart (location in the critical strip). PhysicallyRealizableLedger is the class requiring an admissible Euler trace, strictly positive scalar states, and a uniform T1 defect bound. The module extracts the Euler carrier realization already present in UnifiedRH into the file layout required by the RH-from-RCL derivation plan.
proof idea
This is a one-line wrapper that applies the upstream euler_physically_realizable definition, which itself uses infer_instance to supply the ledger instance.
why it matters
The definition feeds the Euler realizability certificate in the same module, which pairs it with the concrete admissible trace. It completes the extraction step in the RH-from-RCL plan and confirms the Euler carrier satisfies the T1-bounded ledger conditions of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.