eulerSampledCoveringPackage

formal source

  58
  59/-- The sampled Euler `CostCoveringPackage` for any σ₀ > 1/2.
  60Built from the zero-winding certificate, not from a synthetic zero-charge trace. -/
  61noncomputable def eulerSampledCoveringPackage (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
  62    CostCoveringPackage :=
  63  eulerSampledPackage σ₀ hσ
  64
  65/-! ### §2. Floor coverage iff charge = 0 (proved, not axiomatized) -/
  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