pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.NumberTheory.AnalyticTrace

show as:
view Lean formalization →

The AnalyticTrace module supplies the sampled Euler cost covering package for any σ₀ > 1/2. It is assembled from the zero-winding certificate rather than a synthetic zero-charge trace. Researchers pursuing the analytic route to the Riemann Hypothesis in Recognition Science cite this package. The module combines proved results on annular costs and contour windings into a single realizable object.

claimThe sampled Euler cost-covering package for any real part σ₀ > 1/2, constructed from zero-winding certificates on contours rather than a synthetic zero-charge trace.

background

Recognition Science builds physics from the J-cost functional equation, with J(x) = (x + x^{-1})/2 - 1. The AnnularCost module introduces the phi-weighted cost phiCost(u) := cosh((log φ)·u) - 1 = J(φ^u) together with annular sampling for the topological cost-covering bridge. This module sits inside the NumberTheory domain and imports the CostCoveringBridge architecture whose three-layer structure realizes the RS cost-covering after the budget interface becomes concrete.

proof idea

This is a definition module, no proofs. It assembles the cost covering package by importing and combining the zero-winding certificate from ContourWinding, the upgraded sampling from ArgumentPrincipleProved, the phi-cost machinery from AnnularCost, and the bridge construction from CostCoveringBridge.

why it matters in Recognition Science

This module feeds the HonestPhaseAdmissibility module, which defines the admissibility predicate for honest zeta-derived phase data and proves equivalence to the charge-zero conclusion. It advances the analytic route in Recognition Science by supplying a concrete CostCoveringPackage built from zero-winding data, supporting the T5 J-uniqueness and T8 D=3 landmarks without synthetic assumptions.

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)