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

IndisputableMonolith.NumberTheory.BoundedPhaseVisibility

show as:
view Lean formalization →

The module supplies the bounded visibility engine for positive non-identity reciprocal ledgers in natural-number form. It is cited by the phase-budget engine and visibility-from-floor arguments inside the Erdős-Straus residual chain. The construction assembles the subset-product phase layer, the T1/RCL budget bound, and the uniform KTheta failure floor to guarantee that some admissible gate succeeds.

claimLet $r$ be a positive non-identity reciprocal expressed in Nat form. Then the accumulated finite-phase cost of $r$ is bounded by the T1/RCL budget together with the uniform failure floor $K_Theta = J(φ)/45$, so that an admissible gate must succeed.

background

The module sits inside the NumberTheory domain and imports three upstream modules. SubsetProductPhase isolates the finite subgroup-generation layer that converts a square-budget divisor phase into unit-fraction constructions for the Erdős-Straus residual proof. T1PhaseBudgetBound states that a stable integer ledger carrying a finite T1/RCL budget cannot sustain unbounded unresolved finite-phase cost. UniformFailureFloor defines the RS floor scale $K_Theta = J(φ)/45$ and proves only its positivity, leaving the uniform lower bound on each failed gate as an explicit interface.

proof idea

This is a definition module, no proofs. It assembles the three imported modules into the statements NonIdentityReciprocal, BoundedFiniteQuotientPhaseVisibility, and BoundedVisibilityEngine that are consumed downstream.

why it matters in Recognition Science

The module supplies the recovered-ledger bounded visibility engine turned into the phase-budget engine for the Erdős-Straus residual proof in PhaseBudgetEngineFromRS. It supplies the visibility guarantee required by VisibilityFromFloorBudget, where failed gates accumulate $K_Theta$ until the T1 budget forces success. It records the honest obstruction treated in ResidualGapHonest and thereby touches the missing prime/divisor distribution theorem needed for an actual phase match.

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)