sampledTraceToAnnularTrace_excess_zero
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not hold for certificates with nonzero winding.
- Does not compute the numerical value of annular cost, only that excess is zero.
- Does not address the continuous limit of infinite mesh resolution.
- Does not apply to non-equispaced angular sampling schedules.
- Does not depend on specific carrier frequency values.
formal statement (Lean)
145theorem sampledTraceToAnnularTrace_excess_zero (cert : ZeroWindingCert) (N : ℕ) :
146 annularExcess ((sampledTraceToAnnularTrace cert).mesh N) = 0 := by
proof body
Term-mode proof.
147 unfold annularExcess annularCost annularTopologicalFloor
148 rw [sub_eq_zero]
149 apply Finset.sum_congr rfl
150 intro n _
151 show ringCost _ = topologicalFloor _ _
152 unfold sampledTraceToAnnularTrace SampledMesh.toAnnularMesh mkSampledMesh
153 mkSampledRing SampledRing.toAnnularRingSample
154 simp only
155 unfold ringCost topologicalFloor
156 simp [phiCost_zero, Finset.sum_const_zero]
157
158/-! ### §6. Building a BudgetedCarrier from sampled traces -/
159
160/-- Build a `BudgetedCarrier` from a `ZeroWindingCert` and carrier regularity data.
161This replaces the synthetic `eulerBudgetedCarrier` with one built from actual
162zero-winding certificates. -/