sampledTraceToAnnularTrace_charge_zero
plain-language theorem explainer
The declaration establishes that the annular trace constructed from any zero-winding certificate carries zero charge. Researchers building discrete contour models or budgeted carriers in Recognition Science cite this when replacing synthetic carriers with sampled data. The proof is a direct reflexivity step on the definition of the trace map under the zero-winding condition.
Claim. Let cert be a zero-winding certificate. Then the charge of the annular trace obtained from the sampling map applied to cert satisfies $charge(sampledTraceToAnnularTrace(cert)) = 0$.
background
The Sampled Traces module bridges continuous contour-winding to the discrete AnnularRingSample and AnnularMesh cost framework. SampledRing records phase increments from sampling on 8n equispaced points with winding taken from the contour layer; SampledMesh stacks N concentric rings at radii r_n = R n/(N+1). The map sampledTraceToAnnularTrace converts a ZeroWindingCert into an AnnularTrace whose charge component is the object of study here.
proof idea
The proof is a one-line term that applies reflexivity to the definition of sampledTraceToAnnularTrace on a ZeroWindingCert, which directly forces the charge field to zero.
why it matters
This result feeds the construction of BudgetedCarrier in sampledBudgetedCarrier, replacing synthetic carriers with ones built from actual zero-winding certificates. It completes the charge-zero half of the sampledTrace_to_annularTrace bridge listed in the module documentation and aligns with the framework requirement that zero-winding saturates the topological floor at zero, consistent with the eight-tick octave sampling schedule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.