mkSampledMesh_charge_zero

formal source

 121  charge_zero := fun _ => rfl
 122
 123/-- The sampled mesh from a cert has charge 0. -/
 124theorem mkSampledMesh_charge_zero (cert : ZeroWindingCert) (N : ℕ) :
 125    ∀ n, ((mkSampledMesh cert N).rings n).winding = 0 :=
 126  (mkSampledMesh cert N).charge_zero
 127
 128/-! ### §5. Bridge to AnnularTrace -/
 129
 130/-- Build an `AnnularTrace` from a `ZeroWindingCert`: a refinement family
 131of zero-charge meshes at every depth N. -/
 132noncomputable def sampledTraceToAnnularTrace (cert : ZeroWindingCert) :
 133    AnnularTrace where
 134  charge := 0
 135  mesh := fun N => (mkSampledMesh cert N).toAnnularMesh
 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