EffectivePrimePhaseInput
plain-language theorem explainer
EffectivePrimePhaseInput packages a bound function with the guarantee that every residual trap n admits a c at most the bound which is an admissible hard gate and yields a nonempty subset-product phase hit. Number theorists closing the residual Erdős-Straus chain inside the Recognition framework cite this interface as the precise distribution input. The declaration is a direct structure definition with no proof obligations or computational content.
Claim. A structure consisting of a function $b : ℕ → ℕ$ and the property that for every $n ∈ ℕ$, if $n$ satisfies the residual trap conditions then there exists $c ≤ b(n)$ such that $c ≡ 3 mod 4$ and the subset-product phase witness for the pair $(n,c)$ is nonempty.
background
The module isolates the exact prime-distribution input required by the residual Erdős-Straus proof. ResidualTrap n holds precisely when $n > 1$, $n ≡ 1 mod 24$, and every prime factor of both $n$ and $(n+3)/4$ is congruent to 1 mod 3. AdmissibleHardGate c asserts $c ≡ 3 mod 4$. SubsetProductPhaseHit n c is the witness structure carrying a divisor-exponent box together with positivity and phase-divisibility conditions.
proof idea
The declaration is a direct structure definition. No lemmas or tactics are invoked; the two fields simply record the bound function and the supplies_generators existence statement.
why it matters
This interface is consumed by erdos_straus_residual_from_effectivePrimePhaseInput to produce the rational Erdős-Straus representation for every trapped n, and it is the target of effectivePrimePhaseInput_of_phaseBudgetEngine. It also supplies the effective_input field of RSPrimePhaseEquidistribution. The structure therefore bridges prime-phase distribution to the residual chain while remaining independent of the bit-rotted PrimeDistributionBridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.