pith. sign in
module module high

IndisputableMonolith.NumberTheory.AnalyticTrace

show as:
view Lean formalization →

The AnalyticTrace module supplies the sampled Euler CostCoveringPackage for any σ₀ > 1/2, built from zero-winding certificates on the contour rather than synthetic zero-charge traces. Researchers on the analytic RH route in Recognition Science cite it for delivering honest zeta-derived phase data. The module assembles this package from upstream annular J-cost and contour winding results.

claimThe module defines the CostCoveringPackage for the sampled Euler carrier at σ₀ > 1/2, where the package encodes J-cost covering derived from the zero winding number of the holomorphic nonvanishing function on the contour.

background

The module operates in the NumberTheory domain after the RS cost-covering architecture is made realizable. It imports AnnularCost, where phiCost u := cosh((log φ)·u) − 1 = J(φ^u), and ContourWinding, which packages WindingData (center, radius, integer winding charge) and proves zero winding for holomorphic nonvanishing functions. ArgumentPrincipleProved eliminates the argument_principle_sampling axiom, upgrading the analytic route toward honest witnessed ζ⁻¹ phase-family data. Constants supplies the RS time quantum τ₀ = 1 tick.

proof idea

This is a definition module that packages the CostCoveringPackage from the zero-winding certificate. It composes the imported results on annular J-cost, contour winding, and the proved argument principle into a single sampled object for σ₀ > 1/2.

why it matters in Recognition Science

The module feeds HonestPhaseAdmissibility, which defines the admissibility predicate for honest zeta-derived phase data and proves equivalence to the charge-zero conclusion needed by AnalyticTrace.ZeroFreeCriterion. It advances the analytic RH target in the Recognition Science cost-covering bridge, using the zero-winding certificate to narrow the phase-family data.

scope and limits

used by (1)

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

depends on (13)

Lean names referenced from this declaration's body.

declarations in this module (28)