mkSampledMesh

formal source

 111
 112/-- Construct a full sampled mesh from a `ZeroWindingCert`.
 113Uses a fixed radius `R/2` for all rings (inside the disk). -/
 114noncomputable def mkSampledMesh (cert : ZeroWindingCert) (N : ℕ) :
 115    SampledMesh N where
 116  rings := fun n =>
 117    mkSampledRing cert (n.val + 1) (Nat.succ_pos _)
 118      (cert.radius / 2)
 119      (by linarith [cert.radius_pos])
 120      (by linarith [cert.radius_pos])
 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. -/