eulerRealizableLedgerCert
plain-language theorem explainer
This definition assembles the Euler realizability certificate by populating the admissible and realizable fields of the EulerRealizableLedgerCert structure with concrete witnesses. Researchers deriving the RH-from-RCL decomposition would cite it when building the logic-aware physical thesis data bundle. It is a direct instantiation that supplies the Euler trace admissibility theorem for every defect sensor together with the T1-bounded ledger realizability map.
Claim. The Euler carrier realizability certificate is the structure whose admissible component is the predicate that every defect sensor satisfies the Euler trace admissibility condition and whose realizable component is the predicate that every defect sensor carries a physically realizable ledger, instantiated by the concrete trace admissibility theorem and the ledger realizability definition.
background
The module extracts the Euler carrier result already obtained in UnifiedRH as a T1-bounded ledger into the file layout required by the RH-from-RCL derivation plan. The EulerRealizableLedgerCert structure is defined with two fields: admissible, which asserts EulerTraceAdmissible for every DefectSensor, and realizable, which asserts PhysicallyRealizableLedger for every DefectSensor. Upstream, euler_trace_admissible_concrete proves the trace admissibility predicate holds for an arbitrary sensor, while euler_ledger_realizable constructs the physical realizability witness from the underlying euler_physically_realizable map; the thermodynamics admissible predicate is the trivial True predicate on ledger states.
proof idea
This is a one-line wrapper definition that directly assigns the theorem euler_trace_admissible_concrete to the admissible field and the definition euler_ledger_realizable to the realizable field of the EulerRealizableLedgerCert structure.
why it matters
The certificate populates the eulerPartition slot in both the RSPhysicalThesisData and RSPhysicalThesisDataLogic bundles that are constructed from a BoundaryTransportCert. It thereby closes the Euler carrier portion of the RH-from-RCL derivation plan, leaving only the boundary transport bridge as the remaining obstruction. In the Recognition Science setting it supplies the number-theoretic extraction step that converts the T1-bounded Euler ledger into the decomposition data used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.