CostCoveringPackage

formal source

 115This is the honest replacement for the former naked axiom. Any consumer of the
 116bridge must now supply a concrete `BudgetedCarrier` witness for the realized
 117carrier trace. -/
 118structure CostCoveringPackage where
 119  carrier : BudgetedCarrier
 120
 121/-- The remaining topological step in the RH bridge: the defect topological
 122floor must be controlled by the same carrier scale. -/
 123def DefectTopologicalFloorCovered (pkg : CostCoveringPackage) (sensor : DefectSensor) : Prop :=
 124  ∀ N : ℕ, annularTopologicalFloor N sensor.charge ≤ carrierBudgetScale pkg.carrier
 125
 126/-! ### §4. The conditional Riemann Hypothesis -/
 127
 128/-- The uniform charge ring sample exactly saturates the topological floor. -/
 129theorem uniformRingSample_cost_eq_topologicalFloor (n : ℕ) (m : ℤ) :
 130    ringCost (uniformRingSample n m) = topologicalFloor (n + 1) m := by
 131  unfold ringCost topologicalFloor uniformRingSample
 132  simp [Finset.sum_const, nsmul_eq_mul]
 133
 134/-- The uniform charge mesh has zero annular excess. -/
 135theorem uniformChargeMesh_excess_zero (N : ℕ) (m : ℤ) :
 136    annularExcess (uniformChargeMesh N m) = 0 := by
 137  unfold annularExcess annularCost annularTopologicalFloor
 138  rw [sub_eq_zero]
 139  apply Finset.sum_congr rfl
 140  intro n _
 141  simpa [uniformChargeMesh] using uniformRingSample_cost_eq_topologicalFloor n.val m
 142
 143/-- A zero of ζ in the critical strip with Re > 1/2 would create
 144    a defect with unbounded annular cost, violating cost-covering.
 145
 146    This is the key contradiction lemma. -/
 147theorem defect_cost_unbounded (sensor : DefectSensor)
 148    (hm : sensor.charge ≠ 0) :