sampledTraceToAnnularTrace
This definition constructs an AnnularTrace from a ZeroWindingCert by fixing charge at zero and defining the mesh family at each depth N via conversion of the sampled mesh. Researchers replacing synthetic Euler carriers with discrete zero-winding data in the Recognition framework cite it when building budgeted carriers from contour certificates. The construction is a direct structure definition that delegates mesh assembly to mkSampledMesh and uses reflexivity for the charge specification.
claimGiven a zero-winding certificate $cert$, the sampled trace to annular trace is the annular trace $T$ with $T.charge = 0$ whose mesh at each depth $N$ is the annular mesh obtained from the sampled mesh of $cert$ at depth $N$, satisfying the charge specification by reflexivity.
background
The Sampled Traces module bridges the continuous contour-winding layer to the discrete AnnularRingSample and AnnularMesh cost framework. An AnnularTrace is a structure consisting of a fixed integer charge together with a family of AnnularMesh objects at every refinement depth $N$, satisfying that each mesh has exactly that charge. A ZeroWindingCert is a structure recording a center, positive radius, and a ComplexCarrierCert that matches them, certifying zero winding around every interior circle.
proof idea
The definition directly assembles the AnnularTrace structure: charge is set to 0, the mesh function applies mkSampledMesh to the certificate and converts to AnnularMesh at each $N$, and the charge_spec is witnessed by reflexivity. It is a one-line wrapper that applies the sampled mesh constructor and the toAnnularMesh conversion.
why it matters in Recognition Science
This definition supplies the full bridge from a ZeroWindingCert to an AnnularTrace, as listed under key results in the module documentation. It is used to define sampledBudgetedCarrier, which replaces the synthetic eulerBudgetedCarrier with one built from actual zero-winding certificates. In the Recognition framework it supports the transition from continuous contour data to discrete annular cost calculations while preserving zero charge.
scope and limits
- Does not establish any cost bound on the resulting trace.
- Does not compute or verify winding numbers explicitly.
- Does not address certificates with nonzero winding.
- Does not depend on specific numerical values of radius or angular increments beyond those fixed in mkSampledMesh.
formal statement (Lean)
132noncomputable def sampledTraceToAnnularTrace (cert : ZeroWindingCert) :
133 AnnularTrace where
134 charge := 0
proof body
Definition body.
135 mesh := fun N => (mkSampledMesh cert N).toAnnularMesh
136 charge_spec := fun _ => rfl
137
138/-- The annular trace from a cert has charge 0. -/