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

IndisputableMonolith.NumberTheory.CostCoveringBridge

show as:
view Lean formalization →

The CostCoveringBridge module supplies uniform charged ring samples in which every increment carries an identical phase step, forcing the total winding to equal exactly m. Researchers closing the Riemann Hypothesis via the Recognition Science analytic trace cite it when comparing annular carrier costs to diverging defect topological floors. The module organizes this through a set of sampling definitions and direct cost equalities that link phi-weighted J-cost to topological covering.

claimA uniform charged ring sample is a discretization of the circle in which each arc increment advances the phase by a fixed step, so that the net winding number is precisely the integer $m$.

background

This module sits in the NumberTheory domain and imports the RS time quantum from Constants, the general cost framework from Cost, and the annular machinery from AnnularCost. AnnularCost defines the core object phiCost u := cosh((log φ)·u) − 1 = J(φ^u), the φ-weighted cost function used for ring sampling. These pieces establish the cost-covering bridge that connects carrier budgets to defect topological floors in the analysis of functions such as zeta.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the parent results in AnalyticTrace, ArgumentPrincipleProved, CarrierBudgetComparison, ContourWinding, DefectSampledTrace, EulerInstantiation, MeromorphicCircleOrder, and SampledTrace. It supplies the uniform sampling layer required for the carrier-defect budget comparison in Phase 4a of the RH closure plan, enabling witnessed contradictions for nonzero charge and the removal of earlier axioms in the analytic trace infrastructure.

scope and limits

used by (8)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (15)