module module high

`IndisputableMonolith.NumberTheory.AnnularCost`

The AnnularCost module defines the φ-cost in logarithmic coordinates as f(u) = cosh((log φ) u) − 1, which equals J(φ^u) via the hyperbolic representation of J. Number theorists building analytic traces and carrier-defect comparisons in the Recognition Science framework cite these definitions for cost bounds on annular samples. The module supplies the core function together with elementary properties such as nonnegativity and quadratic lower bounds, all derived from upstream convexity statements.

claimThe φ-cost in log-coordinates is the function $f(u) = cosh( (log φ) · u ) − 1$, which satisfies $f(u) = J(φ^u)$ where $J(x) = ½(x + x^{-1}) − 1$.

background

This module belongs to the NumberTheory section and imports the RS time quantum τ₀ from Constants together with the J-cost and its convexity properties. The central object is the φ-cost expressed in log-coordinates, which converts the multiplicative J-cost into an additive function on the real line via the identity J(x) = cosh(log x) − 1. The Convexity module supplies the strict convexity of Jlog(t) = cosh t − 1 on ℝ, which is foundational for the J-uniqueness step T5.

proof idea

This is a definition module, no proofs. It introduces phiCost directly from the cosh representation, then records the immediate consequences phiCost_zero, phiCost_symm, phiCost_nonneg, phiCost_quadratic_lb, and the coefficient extractions phiCostLinearCoeff and phiCostQuadraticCoeff.

why it matters in Recognition Science

The definitions feed the analytic infrastructure used by AnalyticTrace, ArgumentPrincipleProved, CarrierBudgetComparison, CirclePhaseLift, ContourWinding, and CostCoveringBridge. These modules assemble the axiom-free RH bridge and the carrier-defect budget comparison on circles, placing the annular cost layer inside the cost-covering architecture that closes the Riemann hypothesis route. The module thereby connects the T5 J-uniqueness result to concrete sampling on the phi-ladder.

scope and limits

Does not prove convexity of the cost function.
Does not treat non-annular contours or higher-dimensional domains.
Does not supply numerical evaluations or explicit bounds beyond the quadratic lower bound.
Does not address the full Riemann hypothesis closure.

used by (10)

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

IndisputableMonolith.NumberTheory.AnalyticTrace module_import
IndisputableMonolith.NumberTheory.ArgumentPrincipleProved module_import
IndisputableMonolith.NumberTheory.CarrierBudgetComparison module_import
IndisputableMonolith.NumberTheory.CirclePhaseLift module_import
IndisputableMonolith.NumberTheory.ContourWinding module_import
IndisputableMonolith.NumberTheory.CostCoveringBridge module_import
IndisputableMonolith.NumberTheory.DefectSampledTrace module_import
IndisputableMonolith.NumberTheory.EulerInstantiation module_import
IndisputableMonolith.NumberTheory.MeromorphicCircleOrder module_import
IndisputableMonolith.NumberTheory.SampledTrace module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Cost.Convexity module_import

declarations in this module (43)

def phiCost L43
theorem phiCost_zero L46
theorem phiCost_symm L50
theorem phiCost_nonneg L54
def kappa L59
theorem kappa_pos L61
theorem phiCost_quadratic_lb L68
theorem phiCost_eq_Jcost L107
theorem phiCost_convexOn L114
def phiCostLinearCoeff L126
def phiCostQuadraticCoeff L130
theorem abs_exp_sub_one_sub_id_le_sq_of_abs_le_one L134
theorem cosh_sub_one_le_sq_of_abs_le_one L140
theorem abs_sinh_le_abs_add_sq_of_abs_le_one L172
theorem phiCost_add_le_phiCost_add_linear_quadratic L210
structure AnnularRingSample L299
def ringCost L305
structure AnnularMesh L309
def annularCost L315
theorem jensen_ring_bound L323
theorem ring_coercivity L368
def topologicalFloor L388
theorem ringCost_ge_topologicalFloor L392
theorem ringCost_le_topologicalFloor_add_linear_quadratic_error L405
def annularTopologicalFloor L464
def annularExcess L468
theorem annular_coercivity L474
theorem harmonic_sum_diverges L498
structure RegularCarrier L520
structure AnnularTrace L527
structure BudgetedCarrier L540
def carrierBudgetScale L549
theorem carrierBudgetScale_nonneg L553
theorem carrier_budget L566
theorem topologicalFloor_nonneg L572
theorem topologicalFloor_zero L579
theorem annularTopologicalFloor_nonneg L584
theorem annularTopologicalFloor_zero L592
theorem annularTopologicalFloor_le_annularCost L600
theorem annularExcess_nonneg L610
theorem topologicalFloor_pos_of_charge_ne_zero L616
theorem annularTopologicalFloor_one_pos_of_charge_ne_zero L638
theorem excess_bounded L648