pith. sign in
module module high

IndisputableMonolith.NumberTheory.PhaseBudgetEngineFromRS

show as:
view Lean formalization →

This module supplies the PhaseBudgetEngine that packages the T1/RCL budget, uniform KTheta floor, and finite gate enumeration to guarantee bounded subset-product phase hits for every residual trap. Researchers closing residual traps under RS number theory assumptions would cite it. The module achieves this by importing BoundedPhaseVisibility and PhaseBudgetToErdosStraus then exposing the engine via sibling definitions.

claimThe PhaseBudgetEngine asserts that if a recovered integer ledger has a stable unresolved-phase budget and failed gates obey a uniform $K_Theta$ floor, then every residual trap (positive nonidentity reciprocal ledger) admits a bounded subset-product phase hit.

background

The module operates inside the NumberTheory domain of Recognition Science. It treats residual traps as positive nonidentity reciprocal ledgers and builds the PhaseBudgetEngine as the explicit package that combines the T1/RCL budget with the uniform failure floor and finite gate enumeration. Upstream, BoundedPhaseVisibility states that if a recovered integer ledger has a stable unresolved-phase budget and failed gates have a uniform KTheta floor, then finite phase invisibility cannot persist beyond the supplied bound, with the floor theorem kept explicit as KThetaFailureFloorHypothesis. PhaseBudgetToErdosStraus composes the phase-budget interface with the already-proved Erdős-Straus RCL closure chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the PhaseBudgetEngine required by ErdosStrausResidualClosed, the final residual theorem conditional on the recovered-ledger bounded visibility engine. It also supports MinimalVisibilityEngine, which repackages the bounded visibility engine without the visibility field by turning it into the theorem hits_balanced_phase_of_floor_and_budget. It fills the interface gap between bounded phase visibility and the Erdős-Straus residual closure chain.

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