erdos_straus_residual_closed
plain-language theorem explainer
This theorem shows that every integer n in the residual trap class admits a rational Erdős-Straus representation once a bounded visibility engine for recovered ledgers is supplied. Number theorists examining the Erdős-Straus conjecture inside Recognition Science would cite it as the terminal closure for the trapped subclass. The proof is a one-line term that converts the visibility engine into a phase-budget engine and invokes the phase-budget residual solver.
Claim. Let $E$ be a bounded visibility engine for recovered integer ledgers. For any integer $n>1$ with $n≡1 mod 24$ whose prime factors (and those of $(n+3)/4$) are all congruent to 1 mod 3, there exist nonzero rationals $x,y,z$ such that $4/n=1/x+1/y+1/z$.
background
BoundedVisibilityEngine is the structure supplying a bound function, a cost-of function, and a stability predicate that guarantees stable integer ledger budgets for non-identity reciprocals. ResidualTrap collects the arithmetic conditions $n>1$, $n mod 24=1$, and the requirement that all prime factors of both $n$ and $(n+3)/4$ lie in the 1 mod 3 class. HasRationalErdosStrausRepr asserts the existence of three nonzero rationals whose reciprocals sum to 4/n. The module supplies the final residual theorem conditional on a recovered-ledger bounded visibility engine. The upstream phaseBudgetEngine_of_boundedVisibilityEngine converts the visibility engine into the PhaseBudgetEngine required by the residual solver, while erdos_straus_residual_from_phaseBudget states that any phase-budget engine solves the trapped class.
proof idea
The proof is a one-line term wrapper. It first applies phaseBudgetEngine_of_boundedVisibilityEngine to the supplied engine to obtain a PhaseBudgetEngine, then feeds that engine together with the ResidualTrap hypothesis into erdos_straus_residual_from_phaseBudget.
why it matters
The declaration completes the residual closure step in the Erdős-Straus chain inside Recognition Science. It sits downstream of the rotation hierarchy that isolates the trapped class and upstream of any full conjecture resolution that would absorb the residual case. The result is conditional on the bounded visibility engine recovered from ledger budgets, leaving open the question of whether the engine itself can be constructed uniformly without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.