pith. sign in
module module high

IndisputableMonolith.NumberTheory.CarrierBudgetComparison

show as:
view Lean formalization →

Module CarrierBudgetComparison introduces the SharedCircleFamilyPair structure to record a carrier sampled family paired with a defect family on identical concentric circles, enabling direct annular cost comparisons. Researchers working on the RS cost-covering bridge for the Riemann hypothesis cite it for establishing bounded carrier budgets against unbounded defect costs. The module supplies the pairing definition plus lemmas that derive contradictions under shared-phase zero-charge conditions.

claimThe module defines a structure recording a carrier sampled family and a defect family on the same set of concentric circles around a common center, together with comparison results showing bounded carrier annular cost versus unbounded defect cost under zero-charge conditions.

background

This module sits inside the Recognition Science cost-covering bridge for the Riemann hypothesis. It draws on the annular J-cost framework in which phiCost u is defined as cosh((log φ)·u) − 1, equivalently J(φ^u). The CirclePhaseLift supplies continuous-phase infrastructure bridging complex analysis to discrete annular meshes, while DefectSampledTrace realizes the meshes attached to a hypothetical zeta defect. Constants supplies the base time quantum τ₀ = 1 tick.

proof idea

This is a definition module with supporting lemmas. It first defines the SharedCircleFamilyPair structure that enforces identical circles for carrier and defect families. Subsequent lemmas apply the annular cost definitions to obtain bounded carrier cost for zero-charge cases, unbounded defect cost, and the resulting budget contradiction.

why it matters in Recognition Science

The module supplies the concrete pairing and comparison tools required by the cost-covering architecture in CostCoveringBridge. It instantiates the Euler product framework from EulerInstantiation into explicit carrier-defect pairs on shared circles, advancing the elimination of Axiom 2 in the RH proof path. It directly supports the budget contradiction step that closes the carrier-defect comparison.

scope and limits

depends on (8)

Lean names referenced from this declaration's body.

declarations in this module (10)