EulerRealizableLedgerCert
plain-language theorem explainer
The structure EulerRealizableLedgerCert packages two universal statements over every DefectSensor: the Euler trace admits a compatible regular carrier that is nonvanishing and derivative-bounded for sigma greater than 1/2, and the attached ledger is physically realizable with positive scalar states whose T1 defects remain bounded. Researchers assembling the RH-from-RCL decomposition cite it when populating the realizableLedger field of RSPhysicalThesisData. It is introduced as a bare structure definition that simply bundles the two quantified 1
Claim. A certificate $C$ such that for every defect sensor $ρ$ (with integer charge and real part $σ_0$), the Euler trace at $ρ$ is admissible (there exists a regular carrier of radius $σ_0 - 1/2 > 0$ that is nonvanishing and has bounded logarithmic derivative for all $σ > 1/2$) and the ledger attached to $ρ$ is physically realizable (carries a positive scalar proxy state $x_N$ whose T1 defect stays uniformly bounded for all refinement depths $N$).
background
In the Euler Carrier Realizability module the Euler carrier is already realized in UnifiedRH as a T1-bounded ledger; this module extracts that result into the file layout required by the RH-from-RCL derivation plan. A DefectSensor at location $ρ$ records the multiplicity of a zero of $ζ$ (equivalently the order of the pole of $ζ^{-1}$) together with its real part. EulerTraceAdmissible sensor asserts the existence of a RegularCarrier covering the disk from Re($ρ$) to the critical line, with the carrier nonvanishing and derivative-bounded for $σ > 1/2$. PhysicallyRealizableLedger sensor is the class requiring an admissible Euler trace plus a scalarState function that stays positive and whose defect is uniformly bounded.
proof idea
The declaration is a structure definition that directly packages the two universal statements. No lemmas are applied; the fields admissible and realizable are simply the quantified predicates drawn from EulerTraceAdmissible and PhysicallyRealizableLedger.
why it matters
This certificate supplies the realizableLedger component required by RSPhysicalThesisData in the RSPhysicalThesisDecomposition module and by RSPhysicalThesisDataLogic in the LogicRH_From_RCL module. It closes the extraction step in the RH-from-RCL plan by confirming that the Euler carrier infrastructure from UnifiedRH is available for every defect sensor. The construction appears in the downstream definition eulerRealizableLedgerCert, which populates the fields using concrete witnesses euler_trace_admissible_concrete and euler_ledger_realizable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.