toClassicalData
plain-language theorem explainer
The definition converts logic-aware RH decomposition data to its classical counterpart by selecting the classical prime ledger field while copying all other components. Researchers on the RH-from-RCL chain cite it to recover the standard interface from the recovered-prime wrapper. The construction is a direct field projection with no computation or lemmas.
Claim. Let $D_L$ be a structure containing a recovered-prime ledger certificate, a classical prime ledger certificate, an Euler partition certificate, a completed zeta ledger certificate, a zero-defect sensor certificate, a realizable ledger certificate, a boundary transport certificate, and a T1 boundary exclusion certificate. The map $D_L$ to classical data yields the structure whose prime ledger is the classical component of $D_L$ and whose remaining fields are identical to those of $D_L$.
background
The module introduces a recovered-prime-ledger wrapper for the RH-from-RCL decomposition. The analytic zeta/xi/winding infrastructure remains Mathlib-backed and unchanged. This module only replaces the arithmetic ledger hook with a certificate that includes the recovered-prime ledger, then transports back to the existing PrimeLedgerCert required by the RH assembly.
proof idea
The definition is a direct constructor. It sets the prime ledger to the classical field of the input structure and copies the Euler partition, completed ledger, zero defect, realizable ledger, boundary transport, and T1 boundary verbatim from the input. No upstream lemmas are invoked.
why it matters
The definition is applied inside rsPhysicalThesis_of_logic_data to recover the standard RSPhysicalThesis interface from logic-aware data. It closes the recovered-prime wrapper step in the RH-from-RCL chain while leaving BoundaryTransportCert as the remaining obstruction, consistent with the module's stated purpose of maintaining compatibility with the classical analytic stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.