pith. sign in
module module high

IndisputableMonolith.NumberTheory.SubsetProductPhase

show as:
view Lean formalization →

This module defines the SubsetProductPhaseHit structure as a witness that generates target phases via subset products over square-budget divisor boxes. Researchers handling the combinatorial core of the residual Erdős-Straus proof in Recognition Science cite it when linking subset selection to phase conditions modulo c. The module supplies the required definitions and basic equivalences without containing tactic-heavy proofs.

claimA phase-generating subset-product witness consists of a square-budget box divisor $d$ together with a subset $S$ of the complementary factors such that both the product over $S$ and the product over its complement satisfy the divisibility condition landing in phase $-N$ modulo $c$.

background

The module operates inside the NumberTheory domain and imports the Erdős-Straus Box Phase, which isolates the finite combinatorial fragment of the residual Erdős-Straus argument. That upstream module represents a square budget $N^2$ by complementary divisor pairs $(d,e)$ with $d e = N^2$, avoiding explicit prime-exponent enumeration. SubsetProductPhaseHit augments this representation by recording a subset whose product, together with the complementary product, meets the phase target $-N$ modulo $c$.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The structure supplies the witness needed by BoundedPhaseVisibility to bound unresolved-phase persistence, by EffectivePrimePhaseInput to state prime-distribution requirements, and by VisibilityFromFloorBudget to derive admissible-gate success from KTheta floors and T1/RCL budgets. It therefore closes the combinatorial interface between square-budget boxes and phase visibility in the residual Erdős-Straus development.

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)