erdos_straus_residual_from_phaseBudget
plain-language theorem explainer
A phase-budget engine supplies a bound and admissible hard gates with nonempty subset-product phase hits for every residual trap n. This guarantees a rational Erdős-Straus representation for such n. Number theorists closing the residual class under Recognition Science phase-budget assumptions cite this result. The proof is a direct one-line wrapper that converts the engine to an effective prime phase input and applies the corresponding theorem.
Claim. Given a phase-budget engine supplying a bound function and, for every residual trap n, an admissible hard gate c with nonempty subset-product phase hit, and given n > 1 with n ≡ 1 (mod 24) whose prime factors and those of (n+3)/4 are all ≡ 1 (mod 3), there exist nonzero rationals x, y, z such that 4/n = 1/x + 1/y + 1/z.
background
The module composes the phase-budget interface with the already-proved Erdős-Straus RCL closure chain. A PhaseBudgetEngine is the structure whose bound and supplies_hit fields assert that T1/RCL budget facts plus finite gate enumeration produce a bounded subset-product phase hit for every residual trap. ResidualTrap n requires 1 < n, n mod 24 = 1, and all prime factors of both n and (n+3)/4 congruent to 1 mod 3. HasRationalErdosStrausRepr (n : ℚ) asserts existence of nonzero rationals x, y, z satisfying the three-term sum identity for 4/n.
proof idea
This is a term-mode one-line wrapper. It applies erdos_straus_residual_from_effectivePrimePhaseInput to the EffectivePrimePhaseInput obtained by effectivePrimePhaseInput_of_phaseBudgetEngine engine, together with the hypothesis hn.
why it matters
This theorem supplies the phase-budget engine case for solving residual trapped classes. It is invoked by erdos_straus_residual_closed to obtain conditional residual closure once a bounded visibility engine is supplied, and by erdos_straus_residual_from_minimal_engine for the minimal visibility engine. It completes the bridge from the T1/RCL stable-budget interface to an explicit gate witness, as stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.