IndisputableMonolith.NumberTheory.SampledTrace
SampledTrace introduces sampled rings and meshes at level n using 8n equispaced points on the circle, with phase increments and winding inherited from the contour layer. It discretizes the annular cost and Euler carrier objects for trace computations in the RS framework. Researchers building the analytic RH bridge cite it for the sampled-to-annular conversion lemmas. The module supplies definitions and zero-cost transport maps with no deep proofs.
claimA sampled ring at level $n$ consists of $8n$ equispaced points on the unit circle, phase increments from function evaluation at those points, and winding data from the contour winding layer. The associated sampled mesh and budgeted carrier map these objects to annular traces while preserving zero charge and excess.
background
The module sits inside the NumberTheory domain and imports the annular J-cost framework (phiCost u := cosh((log phi) u) - 1 = J(phi^u)), the contour winding package (WindingData records center, radius, and integer winding charge), and the cost-covering bridge architecture. It also draws on the complex Euler carrier C(s) = det2(I - A(s))^2, which is holomorphic and nonvanishing on Re(s) > 1/2. Sampled rings therefore discretize the circle while inheriting zero-holonomy properties already established upstream.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
SampledTrace supplies the discretization layer that feeds AnalyticTrace (the axiom-free RH bridge assembly) and EulerInstantiation (the Euler-product realization of the RS carrier/sensor framework). It completes the sampled-to-annular transport step inside the three-layer cost-covering architecture after the budget interface is realized.
scope and limits
- Does not prove holomorphicity or nonvanishing for the sampled trace itself.
- Does not compute explicit numerical values or bounds on traces.
- Does not address convergence of infinite products or series.
- Does not treat non-equispaced or adaptive sampling schemes.
used by (2)
depends on (5)
declarations in this module (10)
-
structure
SampledRing -
def
mkSampledRing -
structure
SampledMesh -
def
mkSampledMesh -
theorem
mkSampledMesh_charge_zero -
def
sampledTraceToAnnularTrace -
theorem
sampledTraceToAnnularTrace_charge_zero -
theorem
sampledTraceToAnnularTrace_excess_zero -
def
sampledBudgetedCarrier -
theorem
sampledBudgetedCarrier_scale_zero