floorCovered_iff_charge_zero

formal source

  66
  67/-- The defect topological floor is covered by the sampled Euler package
  68if and only if the sensor charge is 0. -/
  69theorem floorCovered_iff_charge_zero (σ₀ : ℝ) (hσ : 1/2 < σ₀)
  70    (sensor : DefectSensor) :
  71    DefectTopologicalFloorCovered (eulerSampledCoveringPackage σ₀ hσ) sensor ↔
  72      sensor.charge = 0 :=
  73  eulerSampledFloorCovered_iff_charge_zero σ₀ hσ sensor
  74
  75/-! ### §3. Carrier-side RH obstruction (no axioms) -/
  76
  77/-- A DefectSensor with charge ≠ 0 can never have its floor covered by
  78the sampled Euler package. The defect floor grows as m² log N while the
  79carrier budget is 0. -/
  80theorem carrier_side_obstruction (sensor : DefectSensor) (hm : sensor.charge ≠ 0) :
  81    ¬ DefectTopologicalFloorCovered
  82        (eulerSampledCoveringPackage sensor.realPart sensor.in_strip.1) sensor :=
  83  not_DefectTopologicalFloorCovered _ sensor hm
  84
  85/-- If floor coverage holds for the sampled package, the charge must be 0. -/
  86theorem charge_zero_of_covered (σ₀ : ℝ) (hσ : 1/2 < σ₀)
  87    (sensor : DefectSensor)
  88    (hcover : DefectTopologicalFloorCovered (eulerSampledCoveringPackage σ₀ hσ) sensor) :
  89    sensor.charge = 0 :=
  90  (floorCovered_iff_charge_zero σ₀ hσ sensor).mp hcover
  91
  92/-! ### §4. Zero-free criterion (analytic route target) -/
  93
  94/-- The zero-free criterion for the pure analytic route.
  95
  96This structure packages the honest analytic target: witnessed ζ⁻¹ defect data
  97in the strip gives an honest phase-family package, and analytic estimates then
  98force the corresponding defect charge to vanish.
  99