pith. sign in
module module high

IndisputableMonolith.NumberTheory.PrimePhaseDistribution

show as:
view Lean formalization →

The module defines prime phase distributions over square-budget divisor boxes for trapped residuals. Researchers extending Recognition Science arithmetic functions to Erdős-Straus residuals cite it to link cost spectra with balanced phase gates. Its content assembles the combinatorial box representation with the prime cost extension to assert admissible gate existence.

claimFor every residual trapped $n$, there exists a bounded admissible gate $c$ such that a divisor box point $(d,e)$ with $d e = N^2$ hits the required balanced phase, where the phase is determined by the arithmetic cost function $c(n) = sum_p v_p(n) J(p)$.

background

The module sits inside the Recognition Science number theory layer that extends the J-cost from positive reals to natural numbers. Upstream PrimeCostSpectrum states: 'For each n ≥ 1 we define c(n) := Σ_{p^k ‖ n} k · J(p) = Σ_p v_p(n) · J(p)'. The companion ErdosStrausBoxPhase isolates the finite part: 'For a square budget N², a divisor exponent box is represented by a complementary pair (d,e) with d*e = N²'.

proof idea

This is a definition module, no proofs. It assembles the distribution by importing the divisor-box combinatorics and the prime cost spectrum, then states the existence claim for balanced phase points under the residual trapping condition.

why it matters in Recognition Science

The module supplies the exact prime-distribution input required by EffectivePrimePhaseInput for the residual Erdős-Straus proof. It feeds the implication that the stated distribution yields PrimePhaseBoxDistribution. The construction closes the combinatorial bridge between the J-cost spectrum and the square-budget phase constraints.

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)