sampledTraceToAnnularTrace

formal source

 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
 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. -/