pith. sign in
module module high

IndisputableMonolith.NumberTheory.ContourWinding

show as:
view Lean formalization →

The module defines a data structure packaging the integer winding charge of a function around a circle at fixed radius as the continuous counterpart to discrete annular samples. Researchers building the analytic trace in the Recognition Science cost-covering bridge cite it when replacing axiomatic winding assumptions with explicit contour data. The module supplies definitions together with additivity and reciprocity lemmas that follow from the argument principle.

claimLet $W(r,f)$ package the integer charge $n$ such that the contour integral of $f'/f$ around the circle of radius $r$ equals $2 pi i n$.

background

Recognition Science derives all physics from one functional equation whose J-cost satisfies the composition law J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y). The imported AnnularCost module defines the phi-weighted cost as phiCost u := cosh((log phi) u) - 1 = J(phi^u). CostCoveringBridge organizes the three-layer architecture for the Riemann hypothesis once the budget interface is realizable. EulerCarrierComplex supplies the holomorphic nonvanishing carrier C(s) = det2(I - A(s))^2 on Re(s) > 1/2, while Constants fixes the time quantum tau0 = 1 tick.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the continuous winding objects required by AnalyticTrace to assemble the full axiom-free RH bridge after eliminating zeroWindingOfHolNonvanishing via the Euler carrier contour integral. It also feeds SampledTrace to connect continuous data to the discrete AnnularRingSample and AnnularMesh cost framework, advancing the cost-covering architecture toward the Recognition Science constants.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (9)