pith. sign in
module module high

IndisputableMonolith.NumberTheory.PrimePhaseDistribution

show as:
view Lean formalization →

The PrimePhaseDistribution module defines prime phase distribution over square-budget divisor boxes for the residual Erdős-Straus problem. It asserts that every residual trapped n admits a bounded admissible gate c whose divisor box meets the balanced phase condition. Number theorists using Recognition Science cost functions cite this for the conjecture's combinatorial core. The module assembles the claim directly from the imported box phase and prime cost spectrum structures.

claimFor every residual trapped integer $n$, there exists a bounded admissible gate $c$ such that a divisor box point hits the required balanced phase.

background

This module sits in the NumberTheory domain and imports two upstream modules. The Erdős-Straus Square-Budget Box Phase module isolates the finite combinatorial part of the residual Erdős-Straus proof by representing a divisor exponent box via a complementary pair $(d,e)$ with $d*e=N^2$. The Prime Cost Spectrum module extends the J-cost function to the arithmetic function $c(n):=∑_{p^k∥n}k·J(p)=∑_p v_p(n)·J(p)$. The local setting supplies the prime phase distribution input needed to close the residual case.

proof idea

This module collects the PrimePhaseBoxDistribution definition together with the RSPrimePhaseBoxTheorem and its corollaries. It assembles the distribution property by combining the divisor box representation from the box phase module with the prime cost spectrum, without internal tactic steps beyond the imported structures.

why it matters in Recognition Science

This module supplies the prime phase distribution required by the EffectivePrimePhaseInput module, which states the exact input for the residual Erdős-Straus proof and shows it implies PrimePhaseBoxDistribution. It fills the combinatorial phase step that connects the square-budget boxes to the overall Recognition Science treatment of the conjecture.

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