pith. sign in
module module high

IndisputableMonolith.NumberTheory.SampledTrace

show as:
view Lean formalization →

SampledTrace defines sampled rings and meshes at level n using 8n equispaced points on circles, with phase increments from function evaluation and winding inherited from ContourWinding. It discretizes the annular J-cost layer to support the RS cost-covering bridge. Researchers building the axiom-free analytic trace for the Riemann hypothesis would cite these objects. The module is purely definitional.

claimA sampled ring at level $n$ consists of the $8n$ equispaced points $\omega_k = \exp(2\pi i k/(8n))$ on the unit circle, equipped with a phase-increment map from function evaluation and winding charge from $WindingData$.

background

The module operates inside the NumberTheory domain of Recognition Science. It imports the RS time quantum $\tau_0 = 1$ tick from Constants, the $\phi$-weighted cost $\mathrm{phiCost}(u) := \cosh((\log\phi)\cdot u) - 1 = J(\phi^u)$ from AnnularCost, and $WindingData$ (center, radius, integer winding charge) from ContourWinding.

Sampled constructions discretize the annular sampling and contour winding machinery so that the carrier/sensor framework from CostCoveringBridge can be realized at finite resolution before lifting to the complex Euler carrier on $\mathrm{Re}(s) > 1/2$.

From AnnularCost: 'The $\phi$-weighted cost function and annular sampling machinery for the RS topological cost-covering bridge.'

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

SampledTrace supplies the discrete sampling layer imported by AnalyticTrace to assemble the full RH bridge after former axioms are replaced by EulerCarrierComplex.contourWinding. It also supports EulerInstantiation, which shows the Euler product of $\zeta(s)$ instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge. The module completes the sampled stage of the three-layer cost-covering architecture.

scope and limits

used by (2)

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

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (10)