pith. sign in
module module high

IndisputableMonolith.NumberTheory.SubsetProductPhase

show as:
view Lean formalization →

Module SubsetProductPhase defines a phase-generating subset-product witness on top of the Erdős-Straus square-budget box. The witness records a selected divisor box together with divisibility conditions that place both generated and complementary divisors in the target phase -N modulo c. Downstream modules on bounded visibility and effective prime input cite this structure to close phase-invisibility arguments. The module consists of definitions plus linking lemmas.

claimA subset-product phase witness consists of a square-budget divisor box together with divisors d and e satisfying d · e = box, d ≡ -N (mod c), and e ≡ -N (mod c).

background

The module sits inside the NumberTheory domain and imports ErdosStrausBoxPhase, whose doc-comment states: 'This module isolates the finite combinatorial part of the residual Erdős-Straus proof. For a square budget N², a divisor exponent box is represented by a complementary pair (d,e) with d·e = N².'

SubsetProductPhase augments that box with explicit phase conditions on the generated divisor and its complement. These conditions ensure both land in the target phase -N modulo c, supplying the combinatorial object needed for later visibility and prime-phase arguments.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The witness supplies the combinatorial layer that feeds BoundedPhaseVisibility (stable unresolved-phase budget plus uniform KTheta floor), EffectivePrimePhaseInput (prime-distribution input implying PrimePhaseBoxDistribution), and VisibilityFromFloorBudget (the breakthrough step deriving that an admissible gate must succeed). It thereby closes the finite part of the residual Erdős-Straus argument inside the Recognition Science forcing chain.

scope and limits

used by (3)

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