IndisputableMonolith.NumberTheory.LogicRH_From_RCL

   1import IndisputableMonolith.NumberTheory.RH_From_RCL
   2import IndisputableMonolith.NumberTheory.LogicPrimeLedgerAtom
   3
   4/-!
   5  LogicRH_From_RCL.lean
   6
   7  Recovered-prime-ledger wrapper for the RH-from-RCL decomposition.
   8
   9  The analytic zeta/xi/winding infrastructure remains Mathlib-backed and
  10  unchanged.  This module only replaces the arithmetic ledger hook with a
  11  certificate that includes the recovered-prime ledger, then transports back
  12  to the existing `PrimeLedgerCert` required by the RH assembly.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace NumberTheory
  17namespace LogicRH_From_RCL
  18
  19open LogicPrimeLedgerAtom
  20
  21/-- RH decomposition data with an explicit recovered-prime-ledger component.
  22
  23The classical field is retained because the analytic zeta stack still speaks
  24Mathlib's `ℕ`/`ℂ`; the `primeLedgerLogic` field records that the arithmetic
  25ledger has been recovered from `LogicNat` and is compatible with the classical
  26ledger by transport. -/
  27structure RSPhysicalThesisDataLogic where
  28  primeLedgerLogic : PrimeLedgerLogicCert
  29  primeLedgerClassical : PrimeLedgerCert
  30  eulerPartition : EulerLedgerPartitionCert
  31  completedLedger : CompletedZetaLedgerCert
  32  zeroDefect : ArgumentPrincipleSensorCert
  33  realizableLedger : EulerRealizableLedgerCert
  34  boundaryTransport : BoundaryTransportCert
  35  t1Boundary : T1BoundaryExclusionCert
  36
  37/-- Forget the recovered-prime wrapper to the current decomposed data bundle. -/
  38def toClassicalData (data : RSPhysicalThesisDataLogic) : RSPhysicalThesisData where
  39  primeLedger := data.primeLedgerClassical
  40  eulerPartition := data.eulerPartition
  41  completedLedger := data.completedLedger
  42  zeroDefect := data.zeroDefect
  43  realizableLedger := data.realizableLedger
  44  boundaryTransport := data.boundaryTransport
  45  t1Boundary := data.t1Boundary
  46
  47/-- Build logic-aware RH decomposition data from the current boundary transport
  48certificate. The only remaining obstruction is still `BoundaryTransportCert`;
  49the recovered-prime ledger is no longer an extra assumption. -/
  50noncomputable def logicData_of_boundaryTransport
  51    (boundary : BoundaryTransportCert) : RSPhysicalThesisDataLogic where
  52  primeLedgerLogic := primeLedgerLogicCert
  53  primeLedgerClassical := primeLedgerCert
  54  eulerPartition := eulerLedgerPartitionCert
  55  completedLedger := completedZetaLedgerCert
  56  zeroDefect := argumentPrincipleSensorCert
  57  realizableLedger := eulerRealizableLedgerCert
  58  boundaryTransport := boundary
  59  t1Boundary := t1BoundaryExclusionCert
  60
  61/-- Logic-aware data implies the old `RSPhysicalThesis` interface. -/
  62theorem rsPhysicalThesis_of_logic_data (data : RSPhysicalThesisDataLogic) :
  63    RSPhysicalThesis :=
  64  rsPhysicalThesis_of_data (toClassicalData data)
  65
  66/-- RH from RCL with a recovered-prime-ledger wrapper. Analytic boundary
  67transport remains exactly the previous obstruction. -/
  68theorem riemann_hypothesis_from_rcl_logicPrime
  69    (boundary : BoundaryTransportCert) :
  70    RiemannHypothesis :=
  71  rh_full (rsPhysicalThesis_of_logic_data (logicData_of_boundaryTransport boundary))
  72
  73/-- Completion boundary is unchanged: the recovered prime ledger changes the
  74arithmetic input surface, not the analytic RH core. -/
  75theorem rh_from_rcl_logicPrime_completion_boundary :
  76    (BoundaryTransportCert → RiemannHypothesis) ∧
  77    (BoundaryTransportCert ↔
  78      (∀ sensor : DefectSensor, sensor.charge ≠ 0 → False)) := by
  79  exact ⟨riemann_hypothesis_from_rcl_logicPrime, boundaryTransportCert_iff_rh_core⟩
  80
  81end LogicRH_From_RCL
  82end NumberTheory
  83end IndisputableMonolith
  84