IndisputableMonolith.NumberTheory.RSPhysicalThesisDecomposition

   1import IndisputableMonolith.NumberTheory.PrimeLedgerAtom
   2import IndisputableMonolith.NumberTheory.EulerLedgerPartition
   3import IndisputableMonolith.NumberTheory.CompletedZetaLedger
   4import IndisputableMonolith.NumberTheory.ArgumentPrincipleSensor
   5import IndisputableMonolith.NumberTheory.EulerCarrierRealizability
   6import IndisputableMonolith.NumberTheory.BoundaryTransport
   7import IndisputableMonolith.NumberTheory.ZetaLedgerBridge
   8
   9/-!
  10# RS Physical Thesis Decomposition
  11
  12Replaces the opaque `RSPhysicalThesis` dependency with a structured bundle of
  13the exact ingredients needed for the RH proof.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace NumberTheory
  18
  19open IndisputableMonolith.Unification.UnifiedRH
  20
  21/-- Decomposed data behind the old `RSPhysicalThesis`. -/
  22structure RSPhysicalThesisData where
  23  primeLedger : PrimeLedgerCert
  24  eulerPartition : EulerLedgerPartitionCert
  25  completedLedger : CompletedZetaLedgerCert
  26  zeroDefect : ArgumentPrincipleSensorCert
  27  realizableLedger : EulerRealizableLedgerCert
  28  boundaryTransport : BoundaryTransportCert
  29  t1Boundary : T1BoundaryExclusionCert
  30
  31/-- The current proved/explicit data bundle, except for the remaining physical
  32boundary transport bridge. -/
  33noncomputable def rsPhysicalThesisData_of_boundaryTransport
  34    (boundary : BoundaryTransportCert) : RSPhysicalThesisData where
  35  primeLedger := primeLedgerCert
  36  eulerPartition := eulerLedgerPartitionCert
  37  completedLedger := completedZetaLedgerCert
  38  zeroDefect := argumentPrincipleSensorCert
  39  realizableLedger := eulerRealizableLedgerCert
  40  boundaryTransport := boundary
  41  t1Boundary := t1BoundaryExclusionCert
  42
  43/-- Boundary transport rules out every right-half strip zero. -/
  44theorem no_strip_zeros_of_decomposed_data (data : RSPhysicalThesisData) :
  45    ∀ ρ : ℂ, riemannZeta ρ = 0 → 1 / 2 < ρ.re → ρ.re < 1 → False := by
  46  intro ρ _hzero hlo hhi
  47  let sensor : DefectSensor := zetaDefectSensor ρ.re ⟨hlo, hhi⟩ 1
  48  have hm : sensor.charge ≠ 0 := by
  49    dsimp [sensor]
  50    exact zetaDefectSensor_charge_ne_zero ρ.re ⟨hlo, hhi⟩
  51  have hdiv : CostDivergent sensor :=
  52    nonzero_charge_cost_divergent sensor hm
  53  exact no_cost_divergent_sensor_of_boundary_transport data.boundaryTransport sensor hdiv
  54
  55/-- If no strip zero exists, the old `RSPhysicalThesis` holds vacuously. -/
  56theorem rsPhysicalThesis_of_no_strip_zeros
  57    (hno : ∀ ρ : ℂ, riemannZeta ρ = 0 → 1 / 2 < ρ.re → ρ.re < 1 → False) :
  58    RSPhysicalThesis := by
  59  intro ρ hzero hlo hhi
  60  exact False.elim (hno ρ hzero hlo hhi)
  61
  62/-- Decomposed data implies the old `RSPhysicalThesis` interface. -/
  63theorem rsPhysicalThesis_of_data (data : RSPhysicalThesisData) :
  64    RSPhysicalThesis :=
  65  rsPhysicalThesis_of_no_strip_zeros (no_strip_zeros_of_decomposed_data data)
  66
  67end NumberTheory
  68end IndisputableMonolith
  69