IndisputableMonolith.NumberTheory.HonestPhaseAdmissibility

   1import IndisputableMonolith.NumberTheory.AnalyticTrace
   2
   3/-!
   4# Honest Phase Admissibility
   5
   6Route C narrows the analytic RH target to honest zeta-derived phase data.  This
   7module defines the admissibility predicate for that data and proves that it is
   8equivalent to the charge-zero conclusion needed by `AnalyticTrace.ZeroFreeCriterion`.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace NumberTheory
  13
  14open AnalyticTrace
  15
  16/-- Honest phase data is admissible when its realized sampled family has finite
  17recognition budget, i.e. bounded total annular J-cost. -/
  18structure HonestPhaseAdmissible (zfd : ZetaPhaseFamilyData) : Prop where
  19  finiteRecognitionBudget :
  20    RealizedDefectAnnularCostBounded (zfd.phaseFamily.toSampledFamily)
  21
  22/-- Admissible honest phase data has zero charge. -/
  23theorem charge_zero_of_honestPhaseAdmissible
  24    (zfd : ZetaPhaseFamilyData) (hadm : HonestPhaseAdmissible zfd) :
  25    zfd.sensor.charge = 0 :=
  26  honestPhaseFamily_charge_zero_of_costBounded zfd hadm.finiteRecognitionBudget
  27
  28/-- Honest phase admissibility is equivalent to zero charge.  The reverse
  29direction uses the already-proved bounded-excess theorem for honest phase data. -/
  30theorem honestPhaseAdmissible_iff_charge_zero (zfd : ZetaPhaseFamilyData) :
  31    HonestPhaseAdmissible zfd ↔ zfd.sensor.charge = 0 := by
  32  constructor
  33  · intro hadm
  34    exact charge_zero_of_honestPhaseAdmissible zfd hadm
  35  · intro hzero
  36    exact ⟨(honestPhaseFamily_cost_bounded_iff_charge_zero zfd).mpr hzero⟩
  37
  38/-- A global admissibility bridge for all honest zeta phase data. -/
  39structure HonestPhaseAdmissibilityBridge where
  40  admissible : ∀ zfd : ZetaPhaseFamilyData, HonestPhaseAdmissible zfd
  41
  42/-- A global admissibility bridge gives the direct charge-zero bridge used in
  43`AnalyticTrace`. -/
  44def chargeZeroBridge_of_admissibilityBridge
  45    (hb : HonestPhaseAdmissibilityBridge) :
  46    HonestPhaseChargeZeroBridge where
  47  charge_zero_of_honest_phase := fun zfd =>
  48    charge_zero_of_honestPhaseAdmissible zfd (hb.admissible zfd)
  49
  50/-- Conversely, a direct charge-zero bridge gives admissibility, since zero
  51charge plus bounded excess gives bounded total cost. -/
  52def admissibilityBridge_of_chargeZeroBridge
  53    (hb : HonestPhaseChargeZeroBridge) :
  54    HonestPhaseAdmissibilityBridge where
  55  admissible := fun zfd =>
  56    (honestPhaseAdmissible_iff_charge_zero zfd).2
  57      (hb.charge_zero_of_honest_phase zfd)
  58
  59/-- The admissibility bridge and the charge-zero bridge are equivalent. -/
  60theorem honestPhaseAdmissibilityBridge_iff_chargeZeroBridge :
  61    HonestPhaseAdmissibilityBridge ↔ HonestPhaseChargeZeroBridge :=
  62  ⟨chargeZeroBridge_of_admissibilityBridge,
  63   admissibilityBridge_of_chargeZeroBridge⟩
  64
  65/-- A global honest-phase admissibility bridge gives a `ZeroFreeCriterion`. -/
  66noncomputable def zeroFreeCriterion_of_honestPhaseAdmissibility
  67    (hb : HonestPhaseAdmissibilityBridge) :
  68    ZeroFreeCriterion :=
  69  zeroFreeCriterion_of_honestPhaseChargeZeroBridge
  70    (chargeZeroBridge_of_admissibilityBridge hb)
  71
  72/-- A global honest-phase admissibility bridge proves the analytic RH core. -/
  73theorem direct_rh_from_honestPhaseAdmissibility
  74    (hb : HonestPhaseAdmissibilityBridge) :
  75    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False :=
  76  rh_from_zero_free_criterion
  77    (zeroFreeCriterion_of_honestPhaseAdmissibility hb)
  78
  79/-! ## Carrier admissibility insertion point -/
  80
  81/-- Carrier-side admissibility specialized to actual witnessed zeta sensors.
  82This is the narrow Route C bridge: whenever a witnessed zero produces honest
  83phase-family data, the Euler carrier admits that phase data with finite
  84recognition budget. -/
  85structure WitnessedHonestPhaseAdmissibilityBridge where
  86  admissible_of_honest_phase :
  87    ∀ (sensor : WitnessedDefectSensor) (zfd : ZetaPhaseFamilyData),
  88      zfd.sensor = sensor.toDefectSensor → HonestPhaseAdmissible zfd
  89
  90/-- A witnessed admissibility bridge proves the witnessed RH core. -/
  91theorem witnessed_rh_from_honestPhaseAdmissibility
  92    (hb : WitnessedHonestPhaseAdmissibilityBridge) :
  93    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False := by
  94  intro sensor hm
  95  obtain ⟨zfd, hzsensor, _hzfamily⟩ :=
  96    honest_argument_principle_phase_family sensor hm
  97  have hadm : HonestPhaseAdmissible zfd :=
  98    hb.admissible_of_honest_phase sensor zfd hzsensor
  99  have hz : zfd.sensor.charge = 0 :=
 100    charge_zero_of_honestPhaseAdmissible zfd hadm
 101  have hs : sensor.toDefectSensor.charge = 0 := by
 102    simpa [hzsensor] using hz
 103  exact hm (by simpa using hs)
 104
 105/-- Conversely, the witnessed RH core makes the admissibility bridge true,
 106because each honest phase package then has zero charge, hence bounded total
 107cost by the already-proved excess bound. -/
 108def witnessedHonestPhaseAdmissibilityBridge_of_rh
 109    (hrh : ∀ sensor : WitnessedDefectSensor, sensor.charge = 0) :
 110    WitnessedHonestPhaseAdmissibilityBridge where
 111  admissible_of_honest_phase := by
 112    intro sensor zfd hzsensor
 113    have hcharge_sensor : sensor.charge = 0 := hrh sensor
 114    have hcharge_zfd : zfd.sensor.charge = 0 := by
 115      simpa [hzsensor] using hcharge_sensor
 116    exact (honestPhaseAdmissible_iff_charge_zero zfd).2 hcharge_zfd
 117
 118/-- The witnessed admissibility bridge is equivalent to the witnessed RH core.
 119This is the honest audit: deriving carrier admissibility for all witnessed
 120honest phase data is not a routine estimate; it is RH in Route C form. -/
 121theorem witnessedHonestPhaseAdmissibilityBridge_iff_rh :
 122    WitnessedHonestPhaseAdmissibilityBridge ↔
 123      (∀ sensor : WitnessedDefectSensor, sensor.charge = 0) := by
 124  constructor
 125  · intro hb sensor
 126    by_contra hm
 127    exact witnessed_rh_from_honestPhaseAdmissibility hb sensor hm
 128  · exact witnessedHonestPhaseAdmissibilityBridge_of_rh
 129
 130/-- A witnessed admissibility bridge also provides a direct charge-zero bridge
 131for the actual phase data associated with witnessed sensors. -/
 132theorem direct_rh_from_witnessedAdmissibilityBridge
 133    (hb : WitnessedHonestPhaseAdmissibilityBridge) :
 134    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False :=
 135  witnessed_rh_from_honestPhaseAdmissibility hb
 136
 137end NumberTheory
 138end IndisputableMonolith
 139