erdos_straus_residual_from_minimal_engine
plain-language theorem explainer
A minimal visibility engine, carrying only a cost function with stable budget and KTheta floor hypotheses for non-identity reciprocals, guarantees a rational Erdős-Straus representation for every residual trapped natural number. Number theorists studying the conjecture inside Recognition Science's phase-budget reduction would cite this as the terminal link from minimal ledger inputs. The proof is a one-line wrapper that lifts the engine to a phase budget engine and invokes the corresponding residual theorem.
Claim. Let $E$ be a minimal visibility engine: a structure with cost map $c:ℕ→ℕ→ℝ$ such that $c$ yields stable integer ledger budgets and satisfies the KTheta failure floor hypothesis for every non-identity reciprocal. For any $n∈ℕ$ in the residual trap class ($n>1$, $n≡1 mod 24$, all prime factors of $n$ and of $(n+3)/4$ congruent to $1 mod 3$), there exist nonzero rationals $x,y,z$ with $4/n=1/x+1/y+1/z$.
background
The Minimal Visibility Engine module repackages the bounded visibility engine by dropping the explicit visibility field, now recovered as a theorem. Its core structure MinimalEngine supplies a costOf function together with two hypotheses: stable ledger budgets and KThetaFailureFloorHypothesis, both required only for non-identity reciprocals. The local setting is therefore the minimal set of RS-physical inputs needed for phase-budget constructions. ResidualTrap, imported from ErdosStrausRotationHierarchy, isolates the class $n>1$, $n≡1 mod 24$, with all prime factors of $n$ and $(n+3)/4$ congruent to $1 mod 3$. HasRationalErdosStrausRepr asserts existence of nonzero rationals $x,y,z$ satisfying the three-term Egyptian fraction identity for $4/n$. The upstream theorem erdos_straus_residual_from_phaseBudget states that any PhaseBudgetEngine solves this residual class; phaseBudgetEngine converts a MinimalEngine into such an engine by supplying the bound field via subset_product_hit_of_minimal.
proof idea
The proof is a one-line wrapper. It applies the theorem erdos_straus_residual_from_phaseBudget to the PhaseBudgetEngine obtained by phaseBudgetEngine engine, using the supplied residual trap hypothesis hn.
why it matters
This theorem supplies the final closure of the MinimalVisibilityEngine module: the minimal ledger inputs (stable budget plus KTheta floor) suffice to solve the residual trapped class of the Erdős-Straus problem. It sits immediately downstream of phaseBudgetEngine and the phase-budget residual theorem, completing the reduction from Recognition Science's core hypotheses to the rational representation. The result ties the number-theoretic residual class back to the RS forcing chain through the phase-budget formalism, though no further open questions are discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.