rsPhysicalThesis_of_logic_data
plain-language theorem explainer
Logic-equipped RH decomposition data yields the RS Physical Thesis. Researchers extending the RCL-based RH argument to recovered primes cite this bridge step. The proof is a one-line wrapper that maps the input to classical data and invokes the prior decomposition theorem.
Claim. Let $D$ be RH decomposition data equipped with a recovered-prime ledger. Then every nontrivial zero $ρ$ of the Riemann zeta function satisfying $1/2 < Re(ρ) < 1$ corresponds to a physically existing defect sensor on the arithmetic ledger.
background
The module supplies a recovered-prime-ledger wrapper around the RH-from-RCL decomposition. Analytic zeta, xi, and winding infrastructure stays Mathlib-backed and unchanged; only the arithmetic ledger hook is replaced by a certificate that includes the recovered prime ledger before transport back to the classical PrimeLedgerCert. RSPhysicalThesisDataLogic is the structure holding primeLedgerLogic, primeLedgerClassical, eulerPartition, completedLedger, zeroDefect, realizableLedger, boundaryTransport, and t1Boundary.
proof idea
One-line wrapper that applies toClassicalData to discard the recovered-prime component and then invokes rsPhysicalThesis_of_data on the resulting classical bundle.
why it matters
This declaration supplies the logic-augmented input required by riemann_hypothesis_from_rcl_logicPrime, completing the recovered-prime path inside the RH-from-RCL decomposition. It preserves the analytic boundary transport obstruction noted in the module documentation while feeding the single non-mechanical ingredient of the RS argument for RH.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.