`DefectSensor`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.CostCoveringBridge
domain: NumberTheory
line: 103 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.CostCoveringBridge on GitHub at line 103.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 100
 101/-- A defect sensor at a point ρ: the field ζ(s)⁻¹ has a pole of
 102    order m at ρ (where m is the multiplicity of the zero of ζ). -/
 103structure DefectSensor where
 104  /-- The multiplicity of the zero (= order of the pole of ζ⁻¹). -/
 105  charge : ℤ
 106  /-- The real part of the zero location. -/
 107  realPart : ℝ
 108  /-- The zero is in the right half of the critical strip. -/
 109  in_strip : 1/2 < realPart ∧ realPart < 1
 110
 111/-! ### §3. The explicit cost-covering package -/
 112
 113/-- An explicit carrier package for the RS cost-covering bridge.
 114
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.