IndisputableMonolith.NumberTheory.CarrierBudgetComparison

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.NumberTheory.AnnularCost
   4import IndisputableMonolith.NumberTheory.CostCoveringBridge
   5import IndisputableMonolith.NumberTheory.DefectSampledTrace
   6import IndisputableMonolith.NumberTheory.CirclePhaseLift
   7import IndisputableMonolith.NumberTheory.MeromorphicCircleOrder
   8import IndisputableMonolith.NumberTheory.EulerInstantiation
   9import IndisputableMonolith.NumberTheory.HonestPhaseBudgetBridge
  10
  11/-!
  12# Carrier–Defect Budget Comparison
  13
  14This module formalizes the carrier budget comparison strategy (Phase 4a
  15of the RH closure plan): on the SAME circles around a hypothetical zero,
  16the carrier's sampled cost is bounded while the defect's topological floor
  17diverges, providing a contradiction for nonzero charge.
  18
  19## Architecture
  20
  21Given a hypothetical zero of ζ at ρ with charge m ≠ 0:
  22
  231. **Carrier family**: The Euler carrier C(s) = det₂(I−A(s))² is holomorphic
  24   and nonvanishing on Re(s) > 1/2. On circles around ρ, it has charge 0,
  25   so its topological floor is 0 and its sampled cost equals its excess.
  26
  272. **Defect family**: The reciprocal ζ⁻¹ has a pole/zero of order m at ρ.
  28   On circles around ρ, it has charge m ≠ 0, so its topological floor
  29   grows as Θ(m² log N).
  30
  313. **Budget transfer**: The carrier and defect sample the SAME geometric
  32   circles. The carrier's excess is bounded (by its regularity), while the
  33   defect's floor diverges. Since the total cost on each circle decomposes
  34   as floor + excess, the defect's total cost diverges.
  35
  36## Key result
  37
  38`carrier_defect_budget_contradiction`: for any `DefectSensor` with nonzero
  39charge and any finite carrier budget, there exists a refinement depth N
  40such that the defect's topological floor exceeds the carrier budget.
  41-/
  42
  43namespace IndisputableMonolith
  44namespace NumberTheory
  45
  46open Constants
  47
  48noncomputable section
  49
  50/-! ### §1. Carrier sampled family on common circles -/
  51
  52/-- A carrier sampled family paired with a defect family on shared circles.
  53
  54This structure records that two sampled families (carrier and defect) are
  55defined on the same concentric circles around a common center, allowing
  56direct comparison of their annular costs. -/
  57structure SharedCircleFamilyPair where
  58  sensor : DefectSensor
  59  carrierPhaseFamily : DefectPhaseFamily
  60  defectPhaseFamily : DefectPhaseFamily
  61  carrier_sensor_charge_zero : carrierPhaseFamily.sensor.charge = 0
  62  defect_sensor_eq : defectPhaseFamily.sensor = sensor
  63  shared_radius : carrierPhaseFamily.witnessRadius = defectPhaseFamily.witnessRadius
  64
  65/-- The carrier family in a shared-circle pair has bounded annular cost
  66because its charge is 0 (topological floor vanishes). -/
  67theorem carrier_cost_bounded_of_shared_pair
  68    (pair : SharedCircleFamilyPair)
  69    (hexcess : RealizedDefectAnnularExcessBounded
  70      (pair.carrierPhaseFamily.toSampledFamily)) :
  71    RealizedDefectAnnularCostBounded
  72      (pair.carrierPhaseFamily.toSampledFamily) := by
  73  have hcharge : (pair.carrierPhaseFamily.toSampledFamily).sensor.charge = 0 :=
  74    pair.carrier_sensor_charge_zero
  75  exact realizedDefectCostBounded_of_charge_zero_and_excessBounded
  76    pair.carrierPhaseFamily.toSampledFamily hcharge hexcess
  77
  78/-- The defect family in a shared-circle pair has UNBOUNDED annular cost
  79when the sensor has nonzero charge. -/
  80theorem defect_cost_unbounded_of_shared_pair
  81    (pair : SharedCircleFamilyPair)
  82    (hm : pair.sensor.charge ≠ 0) :
  83    ¬ RealizedDefectAnnularCostBounded
  84      (pair.defectPhaseFamily.toSampledFamily) := by
  85  intro hbound
  86  have hcharge : (pair.defectPhaseFamily.toSampledFamily).sensor.charge ≠ 0 := by
  87    simpa [DefectPhaseFamily.toSampledFamily, pair.defect_sensor_eq] using hm
  88  exact not_realizedDefectAnnularCostBounded
  89    pair.defectPhaseFamily.toSampledFamily hcharge hbound
  90
  91/-! ### §2. Floor divergence versus carrier budget -/
  92
  93/-- The carrier's topological floor is identically zero (since charge = 0),
  94while the defect's floor diverges. For any finite bound K, the defect floor
  95eventually exceeds K. -/
  96theorem defect_floor_exceeds_any_bound
  97    (sensor : DefectSensor) (hm : sensor.charge ≠ 0)
  98    (K : ℝ) :
  99    ∃ N : ℕ, K < annularTopologicalFloor N sensor.charge :=
 100  defect_topological_floor_unbounded sensor hm K
 101
 102/-- Carrier cost on zero-charge circles: annularCost = annularExcess
 103since the topological floor is 0. -/
 104theorem carrier_cost_eq_excess_of_zero_charge (N : ℕ) (mesh : AnnularMesh N)
 105    (hcharge : mesh.charge = 0) :
 106    annularCost mesh = annularExcess mesh := by
 107  unfold annularExcess
 108  rw [hcharge, annularTopologicalFloor_zero]
 109  ring
 110
 111/-! ### §3. Budget transfer theorem -/
 112
 113/-- **Budget Transfer Theorem.**
 114
 115On shared circles, the defect's total annular cost exceeds the carrier's
 116excess budget for sufficiently large refinement depth.
 117
 118The logic:
 119- The carrier has charge 0 → topological floor = 0 → cost = excess ≤ B
 120- The defect has charge m ≠ 0 → topological floor > B for large N
 121- Since cost ≥ floor, the defect cost > B for large N
 122
 123This theorem packages the key mathematical comparison: no finite carrier
 124budget can bound the defect's divergent cost when the charge is nonzero. -/
 125theorem carrier_defect_budget_contradiction
 126    (sensor : DefectSensor) (hm : sensor.charge ≠ 0)
 127    (B : ℝ) :
 128    ∃ N : ℕ, B < annularTopologicalFloor N sensor.charge := by
 129  exact defect_topological_floor_unbounded sensor hm B
 130
 131/-- **Cost divergence from budget comparison.**
 132
 133If the carrier's excess on shared circles is bounded by `B`, then for
 134sufficiently large N, the defect's total cost exceeds `B` because its
 135topological floor (which is a lower bound on total cost) diverges. -/
 136theorem defect_cost_exceeds_carrier_budget
 137    (sensor : DefectSensor) (hm : sensor.charge ≠ 0)
 138    (fam : DefectSampledFamily)
 139    (hfam_sensor : fam.sensor = sensor)
 140    (B : ℝ) :
 141    ∃ N : ℕ, B < annularCost (fam.mesh N) := by
 142  have hfam_charge : fam.sensor.charge ≠ 0 := by rwa [hfam_sensor]
 143  exact defectSampledFamily_unbounded fam hfam_charge B
 144
 145/-! ### §4. Building shared-circle pairs from genuine phase data -/
 146
 147/-- Construct a `SharedCircleFamilyPair` from a `QuantitativeLocalFactorization`
 148and a `DefectSensor`.
 149
 150The carrier family uses the regular factor phase (charge 0, bounded cost),
 151while the defect family uses the full meromorphic phase (charge m). Both
 152are sampled on circles of decreasing radius `r₀/(n+1)` around the same
 153center. -/
 154noncomputable def mkSharedCirclePair
 155    (sensor : DefectSensor)
 156    (qlf : QuantitativeLocalFactorization)
 157    (horder : qlf.order = -sensor.charge) :
 158    SharedCircleFamilyPair where
 159  sensor := sensor
 160  carrierPhaseFamily := {
 161    sensor := { charge := 0, realPart := sensor.realPart, in_strip := sensor.in_strip }
 162    witnessRadius := qlf.radius
 163    witnessRadius_pos := qlf.radius_pos
 164    phaseAtLevel := fun n hn => by
 165      have hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
 166      have hd : (0 : ℝ) < ↑n + 1 := by linarith
 167      have hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
 168      let rfp := regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
 169        (qlf.radius / (↑n + 1)) (div_pos qlf.radius_pos hd) (div_lt_self qlf.radius_pos hgt1)
 170        qlf.logDerivBound qlf.logDerivBound_pos
 171      exact rfp.toContinuousPhaseData
 172    charge_uniform := fun n hn => by
 173      simp only
 174      have hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
 175      have hd : (0 : ℝ) < ↑n + 1 := by linarith
 176      have hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
 177      exact (regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
 178        (qlf.radius / (↑n + 1)) (div_pos qlf.radius_pos hd) (div_lt_self qlf.radius_pos hgt1)
 179        qlf.logDerivBound qlf.logDerivBound_pos).charge_zero
 180  }
 181  defectPhaseFamily := genuineZetaDerivedPhaseFamily sensor qlf horder
 182  carrier_sensor_charge_zero := rfl
 183  defect_sensor_eq := rfl
 184  shared_radius := rfl
 185
 186/-- The shared-circle pair's carrier has bounded excess because the regular
 187factor phase is Lipschitz-controlled.
 188
 189The carrier family has charge 0, so `defectPhasePureIncrement = 0`:
 190- `small`: via `epsilon_log_phi_small` (same underlying `RegularFactorPhase`)
 191- `linear_term_bounded`: trivially 0 since `phiCostLinearCoeff(0) = 0`
 192- `quadratic_term_bounded`: `phiCostQuadraticCoeff(0) = κ` times convergent `∑ ε²` -/
 193theorem mkSharedCirclePair_carrier_excess_bounded
 194    (sensor : DefectSensor)
 195    (qlf : QuantitativeLocalFactorization)
 196    (horder : qlf.order = -sensor.charge) :
 197    RealizedDefectAnnularExcessBounded
 198      ((mkSharedCirclePair sensor qlf horder).carrierPhaseFamily.toSampledFamily) := by
 199  let carrierDpf := (mkSharedCirclePair sensor qlf horder).carrierPhaseFamily
 200  have hw : DefectPhasePerturbationWitness carrierDpf := {
 201    epsilon := fun n hn j =>
 202      (genuineRegularFactorPhaseAt qlf n hn).sampleIncrements n j
 203    increment_eq := by
 204      intro n hn j
 205      simp only [carrierDpf, mkSharedCirclePair, defectPhasePureIncrement, Int.cast_zero,
 206        neg_zero, mul_zero, zero_div, zero_add]
 207      simp only [genuineRegularFactorPhaseAt, regularFactorPhaseFromWitness, mkRegularFactorPhase]
 208    small := epsilon_log_phi_small qlf
 209    linear_term_bounded := by
 210      refine ⟨0, fun N => ?_⟩
 211      have hpure_zero : ∀ (n : Fin N),
 212          defectPhasePureIncrement carrierDpf (n.val + 1) = 0 := by
 213        intro n
 214        simp [carrierDpf, mkSharedCirclePair, defectPhasePureIncrement]
 215      simp only [hpure_zero, abs_zero, phiCostLinearCoeff, mul_zero, Real.sinh_zero,
 216        zero_mul, Finset.sum_const_zero, le_refl]
 217    quadratic_term_bounded := by
 218      refine ⟨kappa * (qlf.logDerivBound ^ 2 * qlf.radius ^ 2 * (2 * Real.pi) ^ 2), fun N => ?_⟩
 219      have hpure_zero : ∀ (n : Fin N),
 220          defectPhasePureIncrement carrierDpf (n.val + 1) = 0 := by
 221        intro n
 222        simp [carrierDpf, mkSharedCirclePair, defectPhasePureIncrement]
 223      let C : ℝ :=
 224        kappa * (qlf.logDerivBound ^ 2 * qlf.radius ^ 2 * (2 * Real.pi) ^ 2) / 8
 225      have hbig_nonneg :
 226          0 ≤ kappa * (qlf.logDerivBound ^ 2 * qlf.radius ^ 2 * (2 * Real.pi) ^ 2) := by
 227        exact mul_nonneg kappa_pos.le (by positivity)
 228      have hC_nonneg : 0 ≤ C := by
 229        dsimp [C]
 230        exact div_nonneg hbig_nonneg (by positivity)
 231      have hterm :
 232          ∀ n : Fin N,
 233            phiCostQuadraticCoeff |defectPhasePureIncrement carrierDpf (n.val + 1)| *
 234                ∑ j : Fin (8 * (n.val + 1)),
 235                  ((genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
 236                    (n.val + 1) j) ^ 2
 237              ≤ C * ((1 : ℝ) / ((n.val : ℝ) + 1) / ((n.val : ℝ) + 2) ^ 2) := by
 238        intro n
 239        let innerSum : ℝ :=
 240          ∑ j : Fin (8 * (n.val + 1)),
 241            ((genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
 242              (n.val + 1) j) ^ 2
 243        have hinner := sum_epsilon_sq_bound qlf n
 244        have hbound :
 245            kappa * innerSum ≤
 246              kappa *
 247                (qlf.logDerivBound ^ 2 * qlf.radius ^ 2 * (2 * Real.pi) ^ 2 /
 248                  (8 * ((n.val : ℝ) + 1) * ((n.val : ℝ) + 2) ^ 2)) := by
 249          simpa [innerSum] using mul_le_mul_of_nonneg_left hinner kappa_pos.le
 250        rw [hpure_zero n]
 251        simp [phiCostQuadraticCoeff]
 252        simpa [C, div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm] using hbound
 253      calc
 254        ∑ n : Fin N,
 255            phiCostQuadraticCoeff |defectPhasePureIncrement carrierDpf (n.val + 1)| *
 256              ∑ j : Fin (8 * (n.val + 1)),
 257                ((genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
 258                  (n.val + 1) j) ^ 2
 259          ≤ ∑ n : Fin N, C * ((1 : ℝ) / ((n.val : ℝ) + 1) / ((n.val : ℝ) + 2) ^ 2) := by
 260              apply Finset.sum_le_sum
 261              intro n hn
 262              exact hterm n
 263        _ = C * ∑ n : Fin N, (1 : ℝ) / ((n.val : ℝ) + 1) / ((n.val : ℝ) + 2) ^ 2 := by
 264              rw [← Finset.mul_sum]
 265        _ ≤ C * 1 := by
 266              exact mul_le_mul_of_nonneg_left (sum_inv_succ_mul_succ_sq_le_one N) hC_nonneg
 267        _ ≤ kappa * (qlf.logDerivBound ^ 2 * qlf.radius ^ 2 * (2 * Real.pi) ^ 2) := by
 268              dsimp [C]
 269              simpa using (div_le_self hbig_nonneg (by norm_num : (1 : ℝ) ≤ 8))
 270  }
 271  exact phaseFamily_excess_bounded_of_perturbationWitness carrierDpf hw
 272
 273/-! ### §5. The full comparison chain -/
 274
 275/-- **Full carrier–defect comparison for hypothetical zeros.**
 276
 277For any hypothetical zero of ζ with nonzero charge, the carrier budget
 278comparison shows that the defect's cost exceeds any carrier budget bound
 279for sufficiently large refinement depth. This is the concrete instantiation
 280of the abstract budget transfer theorem on shared circles. -/
 281theorem carrier_defect_comparison_rh
 282    (sensor : DefectSensor) (hm : sensor.charge ≠ 0)
 283    (qlf : QuantitativeLocalFactorization)
 284    (horder : qlf.order = -sensor.charge) :
 285    ¬ RealizedDefectAnnularCostBounded
 286      ((mkSharedCirclePair sensor qlf horder).defectPhaseFamily.toSampledFamily) := by
 287  exact defect_cost_unbounded_of_shared_pair _ hm
 288
 289end
 290
 291end NumberTheory
 292end IndisputableMonolith
 293