pith. sign in
module module high

IndisputableMonolith.NumberTheory.EffectivePrimePhaseInput

show as:
view Lean formalization →

The module supplies the EffectivePrimePhaseInput interface that converts a bounded prime phase supply into a concrete subset-product phase hit for every trapped ledger. Researchers closing the Erdős-Straus conjecture through phase-budget arguments cite it as the bridge between distribution and finite generation layers. The module assembles the two imported interfaces into a single package without new theorems.

claimFor every trapped ledger $L$, a bounded prime phase supply $P$ produces a subset-product phase hit on $L$.

background

The module operates in the Erdős-Straus residual setting of Recognition Science. PrimePhaseDistribution supplies the RCL algebra and finite square-budget closure, naming the distribution statement that instantiates BoundedBalancedSearchEngine. SubsetProductPhase isolates the finite subgroup-generation layer that converts a square-budget divisor phase into the required unit-fraction construction.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the PhaseBudgetEngine package required by PhaseBudgetToErdosStraus, which composes the phase-budget interface with the already-proved Erdős-Straus RCL closure chain. It thereby supplies the missing prime-phase input that turns the T1/RCL budget and finite gate enumeration into a bounded subset-product hit for every residual trap.

scope and limits

used by (1)

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