sampledTraceToAnnularTrace_excess_zero
plain-language theorem explainer
The theorem shows that annular excess vanishes for every mesh level derived from a sampled trace under a zero-winding certificate. Researchers building discrete contour models or budgeted carriers in Recognition Science cite it to confirm saturation of the topological floor. The proof reduces excess to a sum of ring costs via unfolding the sampling maps, applies sum congruence, and simplifies with the zero phi-cost identity.
Claim. For any zero-winding certificate $c$ and natural number $N$, the annular excess of the $N$-level mesh obtained by sampling the certified trace equals zero: annular excess of the sampled mesh at resolution $N$ is identically zero.
background
The SampledTrace module bridges continuous contour winding to the discrete annular cost framework. SampledRing records phase increments at 8n equispaced points on a circle with winding taken from the contour layer; SampledMesh stacks N such rings at radii proportional to n/(N+1). The conversion sampledTraceToAnnularTrace turns a zero-winding certificate into an AnnularTrace whose mesh is costed by annularCost and annularExcess. Annular excess is defined as the difference between annular cost and the topological floor; the zero-winding property forces uniform zero increments on every ring, which saturate that floor at zero.
proof idea
The term proof first unfolds annularExcess, annularCost and annularTopologicalFloor, rewrites the difference to zero, and applies Finset.sum_congr. It then unfolds the sampled trace construction through mkSampledMesh, SampledRing.toAnnularRingSample and the ring cost map. Simplification invokes phiCost_zero together with the identity that the sum of zeros is zero, yielding equality of ring cost and topological floor on each component.
why it matters
This result feeds directly into the construction of sampledBudgetedCarrier, which replaces synthetic eulerBudgetedCarrier with one built from actual zero-winding certificates. It completes the bridge from the contour-winding layer to the annular cost framework inside NumberTheory, ensuring zero excess for uniform zero increments. The eight-tick sampling schedule (8n points) aligns with the octave structure of the Recognition framework, confirming that zero-winding traces produce meshes whose cost exactly meets the topological floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.