sampledTraceToAnnularTrace_charge_zero

formal source

 136  charge_spec := fun _ => rfl
 137
 138/-- The annular trace from a cert has charge 0. -/
 139theorem sampledTraceToAnnularTrace_charge_zero (cert : ZeroWindingCert) :
 140    (sampledTraceToAnnularTrace cert).charge = 0 := rfl
 141
 142/-- The annular excess of the sampled trace is 0 on every mesh.
 143This is because each ring uses uniform zero increments, which saturate
 144the topological floor at 0. -/
 145theorem sampledTraceToAnnularTrace_excess_zero (cert : ZeroWindingCert) (N : ℕ) :
 146    annularExcess ((sampledTraceToAnnularTrace cert).mesh N) = 0 := by
 147  unfold annularExcess annularCost annularTopologicalFloor
 148  rw [sub_eq_zero]
 149  apply Finset.sum_congr rfl
 150  intro n _
 151  show ringCost _ = topologicalFloor _ _
 152  unfold sampledTraceToAnnularTrace SampledMesh.toAnnularMesh mkSampledMesh
 153    mkSampledRing SampledRing.toAnnularRingSample
 154  simp only
 155  unfold ringCost topologicalFloor
 156  simp [phiCost_zero, Finset.sum_const_zero]
 157
 158/-! ### §6. Building a BudgetedCarrier from sampled traces -/
 159
 160/-- Build a `BudgetedCarrier` from a `ZeroWindingCert` and carrier regularity data.
 161This replaces the synthetic `eulerBudgetedCarrier` with one built from actual
 162zero-winding certificates. -/
 163noncomputable def sampledBudgetedCarrier
 164    (cert : ZeroWindingCert)
 165    (logDerivBound : ℝ) (hM : 0 < logDerivBound)
 166    (R : ℝ) (hR : 0 < R) :
 167    BudgetedCarrier where
 168  logDerivBound := logDerivBound
 169  logDerivBound_pos := hM