pith. sign in
module module high

IndisputableMonolith.NumberTheory.ErdosStrausBoxPhase

show as:
view Lean formalization →

This module defines the divisor exponent-box point for the square budget N² as a pair of complementary divisors d and e. It supplies the basic combinatorial object in the Erdős-Straus attack inside Recognition Science. The module is imported by four downstream modules that handle logic adapters, phase costs, prime distribution, and subset products. It builds directly on the rotation hierarchy to isolate finite gate pieces.

claimA divisor exponent-box point for the square budget $N^2$ is a pair of complementary divisors $(d,e)$ satisfying $de=N^2$.

background

The module belongs to the NumberTheory domain and continues the RCL attack on the Erdős-Straus conjecture. It introduces the divisor exponent-box point as the central object for the square-budget phase. The upstream ErdosStrausRotationHierarchy module states that it turns the RCL attack into a theorem-shaped proof skeleton and isolates the missing engines of prime phase separation and finite subgroup generation.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the box-phase structures that feed LogicErdosStrausBoxPhase (logic-native adapter), PhaseFailureCost (unresolved phase costs), PrimePhaseDistribution (prime phase theorem), and SubsetProductPhase (finite subgroup-generation layer). It advances the finite/gate pieces of the rotation hierarchy toward square-budget closure.

scope and limits

used by (4)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)