SampledMesh
SampledMesh assembles N concentric sampled rings, each forced to winding number zero. Researchers building discrete zero-charge traces for annular cost calculations in Recognition Science cite the structure when converting contour data to the mesh layer. The definition is a direct record whose single constraint propagates the zero-winding property from each SampledRing.
claimA sampled mesh of size $N$ consists of a map sending each index $n$ in the finite set of size $N$ to a sampled ring of level $n+1$ together with the requirement that every such ring has winding number zero.
background
The Sampled Traces module bridges continuous contour winding to the discrete AnnularRingSample and AnnularMesh cost framework. SampledRing stores a center, positive radius, 8n phase increments on equispaced points, and an integer winding whose value satisfies the sum of increments equaling minus twice pi times the winding, with the winding inherited from the contour layer. SampledMesh aggregates N such rings under the uniform charge-zero constraint. The module adopts the canonical schedule of 8n samples per ring n at radii scaled inside the disk, matching the AnnularRingSample convention.
proof idea
The structure is introduced by direct field declaration. The accompanying toAnnularMesh conversion is a one-line wrapper that maps each ring through toAnnularRingSample, sets charge to zero, and discharges uniform_charge by simp together with the charge_zero hypothesis.
why it matters in Recognition Science
SampledMesh supplies the target type for mkSampledMesh, which builds the mesh from a ZeroWindingCert at fixed radius R/2, and for sampledTraceToAnnularTrace_excess_zero, which shows annular excess vanishes because uniform zero increments saturate the topological floor. It completes the sampled-to-annular bridge inside the module and aligns with the Recognition Science eight-tick sampling schedule.
scope and limits
- Does not prescribe radii or centers of the rings.
- Does not compute annular cost or excess.
- Does not handle nonzero winding cases.
- Does not specify the function being sampled.
formal statement (Lean)
93structure SampledMesh (N : ℕ) where
94 rings : (n : Fin N) → SampledRing (n.val + 1)
95 charge_zero : ∀ n, (rings n).winding = 0
96
97/-- Convert a `SampledMesh` to an `AnnularMesh` with charge 0. -/
98def SampledMesh.toAnnularMesh {N : ℕ} (sm : SampledMesh N) :
99 AnnularMesh N where
100 rings := fun n => (sm.rings n).toAnnularRingSample
proof body
Definition body.
101 charge := 0
102 uniform_charge := fun n => by
103 simp [SampledRing.toAnnularRingSample]
104 exact sm.charge_zero n
105
106/-- The converted mesh has charge 0. -/
107theorem SampledMesh.toAnnularMesh_charge_zero {N : ℕ} (sm : SampledMesh N) :
108 sm.toAnnularMesh.charge = 0 := rfl
109
110/-! ### §4. Constructing sampled meshes from a zero-winding cert -/
111
112/-- Construct a full sampled mesh from a `ZeroWindingCert`.
113Uses a fixed radius `R/2` for all rings (inside the disk). -/