pith. sign in
module module high

IndisputableMonolith.NumberTheory.HonestPhaseBudgetBridge

show as:
view Lean formalization →

The HonestPhaseBudgetBridge module shows that the zeta-derived phase family lies exactly on the topological floor, with annular excess identically zero at every mesh depth. Recognition Science researchers assembling the axiom-free Riemann Hypothesis bridge cite it when moving from phase sampling to carrier-defect budget comparisons. The module realizes this by importing the defect sampled trace construction and the meromorphic circle order bridge.

claimThe zeta-derived phase family has annular excess identically zero on every mesh depth, placing it on the topological floor.

background

This module belongs to the NumberTheory domain and supplies the honest phase budget bridge. It draws on DefectSampledTrace, which realizes annular meshes attached to the phase-sampling construction for a hypothetical zeta defect after Axiom 1 is eliminated, and on MeromorphicCircleOrder, which bridges Mathlib meromorphic-order machinery to the RS annular cost framework via the local factorization $f(z) = (z - ho)^n \cdot g(z)$ with $g$ analytic and $g( ho) eq 0$. The setting supports the transition to carrier budget comparisons on the same circles around a hypothetical zero.

proof idea

This is a bridging module. It imports DefectSampledTrace and MeromorphicCircleOrder to realize the zero-excess property stated in the module doc-comment; no internal proof body is present at the module level.

why it matters in Recognition Science

The module feeds AnalyticTrace, which assembles the full RH bridge with former axioms replaced by contour winding results, and CarrierBudgetComparison, which formalizes the Phase 4a strategy of bounding carrier cost while defect topological floor diverges to obtain a contradiction for nonzero charge. It supplies the zero-excess property required for the honest phase family in the RH closure plan.

scope and limits

used by (2)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (9)