IndisputableMonolith.NumberTheory.ContourWinding
ContourWinding packages integer winding charges of functions around circles as the continuous counterpart to discrete AnnularRingSample objects. AnalyticTrace and SampledTrace modules cite it to connect continuous contours with sampled cost frameworks in the RS cost-covering architecture. The module supplies definitions for WindingData, zero cases, additivity, reciprocity, and defect relations.
claimWindingData$(r,f)$ records the integer winding charge of a function $f$ around the circle of radius $r$. It satisfies the additive property WindingData$(r,fg)=$ WindingData$(r,f)+$WindingData$(r,g)$, the reciprocal relation, and the defect equality linking winding to charge.
background
The module belongs to the NumberTheory layer. Upstream, Constants fixes the RS time quantum $ au_0=1$ tick. AnnularCost defines the $\phi$-weighted cost phiCost $u:=$ cosh$((\log \phi)– 1 = J(\phi^u)$. CostCoveringBridge outlines the three-layer architecture for the RH cost-covering bridge. EulerCarrierComplex supplies the holomorphic carrier $C(s)= ext{det}_2(I-A(s))^2$ on Re$(s)>1/2$.
From the module doc-comment: "Winding data: packages the integer winding charge of a function around a circle at a given radius. This is the continuous-side object; the discrete AnnularRingSample is its sampled counterpart."
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
AnalyticTrace imports the module to replace the former axiom zeroWindingOfHolNonvanishing by contourWinding from EulerCarrierComplex. SampledTrace imports it to bridge continuous winding to the discrete AnnularMesh cost framework. It supplies the continuous winding step required by the RS topological cost-covering bridge.
scope and limits
- Does not prove holomorphicity or nonvanishing of any carrier function.
- Does not perform discrete sampling of winding data onto annular rings.
- Does not invoke the forcing chain T0-T8 or J-uniqueness.
- Does not compute constants such as $\alpha^{-1}$ or $G$.