pith. sign in
module module high

IndisputableMonolith.NumberTheory.BoundedPhaseVisibility

show as:
view Lean formalization →

This module supplies the Nat-form representation of positive nonidentity reciprocal ledgers together with their bounded phase visibility engine. Number theorists working on the Erdős-Straus residual proof chain cite it for the finite visibility layer that converts a phase budget into an admissible gate guarantee. The module assembles three imported results (SubsetProductPhase, T1PhaseBudgetBound, UniformFailureFloor) into a single coherent interface without introducing new proofs.

claimLet $L$ be a positive nonidentity reciprocal ledger in natural-number form. The associated phase visibility is bounded: failed gates each cost at least $K_θ = J(φ)/45$ while the total T1/RCL budget remains finite, so some admissible gate must succeed.

background

The module belongs to the NumberTheory layer that supports the Erdős-Straus residual proof. It imports SubsetProductPhase, whose doc-comment states that the analytic prime-distribution theorem supplies only a square-budget divisor while the finite layer converts that phase into unit fractions. T1PhaseBudgetBound supplies the third phase-budget theorem: a stable integer ledger with finite T1/RCL budget cannot carry unbounded unresolved finite-phase cost. UniformFailureFloor defines the RS floor scale $K_θ = J(φ)/45$ and proves only its positivity; the claim that every failed finite phase gate costs at least $K_θ$ is kept as an explicit interface.

proof idea

This is a definition module, no proofs. It introduces the Nat-form ledger object, the BoundedVisibilityEngine, and the auxiliary statements BoundedFiniteQuotientPhaseVisibility and failed_gate_count_bounded_at_KTheta by importing the three upstream modules and re-exporting the relevant interfaces.

why it matters in Recognition Science

The module feeds PhaseBudgetEngineFromRS, which converts the recovered-ledger bounded visibility engine into the phase-budget engine consumed by the Erdős-Straus residual proof chain. It also supplies the finite visibility layer required by ResidualGapHonest (which records the honest obstruction that mismatch cost decreases with gate size) and by VisibilityFromFloorBudget (the breakthrough step that derives an admissible gate must succeed given an explicit stable budget plus the $K_θ$ floor).

scope and limits

used by (3)

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 (6)