EffectivePrimePhaseInput
EffectivePrimePhaseInput encodes a bound function together with the guarantee that every residual trap n receives an admissible generator c yielding a nonempty subset-product phase hit. Number theorists working on the residual Erdős-Straus representation in the Recognition Science setting cite this structure as the precise interface between prime-phase supply and the RCL chain. The declaration is a direct structure definition that packages the universal supply condition without further proof obligations.
claimAn effective prime phase input consists of a function $b : ℕ → ℕ$ such that, for every natural number $n$ satisfying the residual trap condition ($n > 1$, $n ≡ 1 mod 24$, all prime factors ≡ 1 mod 3), there exists $c ≤ b(n)$ with $c ≡ 3 mod 4$ and a nonempty subset-product phase hit for the pair $(n, c)$.
background
The module states the exact prime-distribution input required by the residual Erdős-Straus proof and derives PrimePhaseBoxDistribution from it. ResidualTrap identifies integers $n > 1$ with $n ≡ 1 mod 24$ whose prime factors (and those of $(n+3)/4$) are all ≡ 1 mod 3. AdmissibleHardGate requires $c ≡ 3 mod 4$ for the hard class. SubsetProductPhaseHit is the structure witnessing a phase-generating subset product whose divisor-exponent box satisfies the required divisibility conditions modulo $c$ (doc: “A phase-generating subset-product witness. The box field is the square-budget divisor selected by the prime-phase generator.”). Upstream, EightTick.phase supplies the periodic 8-tick phases $kπ/4$ and RiemannHypothesis.Wedge.phase supplies the unimodular complex $e^{iw}$. DomainBootstrap.required supplies the minimal structure needed to state the conditions.
proof idea
This declaration is the definition of the EffectivePrimePhaseInput structure. It directly assembles the bound field and the supplies_generators field that universally quantifies over ResidualTrap and asserts existence of a suitable $c$ and nonempty SubsetProductPhaseHit.
why it matters in Recognition Science
The structure supplies the missing prime-phase input for the residual Erdős-Straus chain. It is consumed by erdos_straus_residual_from_effectivePrimePhaseInput to obtain HasRationalErdosStrausRepr for trapped $n$, by primePhaseBoxDistribution_of_effectivePrimePhaseInput to produce the distribution statement, and by RSPrimePhaseEquidistribution as the intended source from RCL prime-ledger machinery. It therefore occupies the prime-phase supply step that links the eight-tick octave and phase distribution to the Erdős-Straus representation theorem.
scope and limits
- Does not construct or prove existence of any concrete bound function.
- Does not import or depend on the bit-rotted PrimeDistributionBridge module.
- Does not address prime distribution outside the residual trapped class.
- Does not verify the internal details of any SubsetProductPhaseHit beyond nonemptiness.
formal statement (Lean)
27structure EffectivePrimePhaseInput where
28 bound : ℕ → ℕ
29 supplies_generators :
30 ∀ n : ℕ, ResidualTrap n →
31 ∃ c : ℕ, c ≤ bound n ∧ AdmissibleHardGate c ∧ Nonempty (SubsetProductPhaseHit n c)
32
33/-- Effective prime phase supply gives the exact distribution statement
34required by the residual Erdős-Straus chain. -/