erdos_straus_residual_from_phaseBudget_logic
plain-language theorem explainer
The theorem shows that a logic-native phase-budget engine solving residual traps for naturals lifts the classical residual result to recovered rationals. Researchers working on the Erdős-Straus conjecture inside Recognition Science cite it to confirm that the phase-budget solver remains valid after logic recovery of inputs. The proof is a one-line wrapper that applies the transport lemma reprLogic_fromRat_of_classical to the classical residual theorem instantiated on the engine's classical component.
Claim. Let $E$ be a logic-native phase-budget engine. For a logic natural number $n$ such that the classical natural number obtained by the forward map satisfies the residual trap condition ($n>1$, $n≡1 mod 24$, and all prime factors congruent to 1 mod 3, including for $(n+3)/4$), the recovered rational admits a rational Erdős-Straus representation in the logic sense.
background
LogicNat is the inductive type with constructors identity (zero-cost element) and step, representing the orbit forced by the Law of Logic; toNat counts iterations to recover the classical natural number. fromRat is the inverse map sending a classical rational back to a LogicRat. ResidualTrap is the predicate on naturals requiring $n>1$, $n mod 24 =1$, and all prime factors of both $n$ and $(n+3)/4$ congruent to 1 mod 3. HasRationalErdosStrausReprLogic is the logic-native version of the Erdős-Straus rational representation property, defined by transporting the classical predicate via toRat. PhaseBudgetEngineLogic is the structure wrapping a classical PhaseBudgetEngine with a LogicNat bound and a compatibility proof that the bound commutes with toNat.
proof idea
The term-mode proof applies the transport theorem reprLogic_fromRat_of_classical (which lifts any classical HasRationalErdosStrausRepr to the corresponding logic version on fromRat) to the result of the classical theorem erdos_straus_residual_from_phaseBudget. The classical theorem is instantiated on engine.classical_engine together with the given residual trap hypothesis hn.
why it matters
This declaration completes the logic-native bridge for the residual-trap case of the Erdős-Straus rotation hierarchy, allowing the existing phase-budget engine to be used directly on recovered-rational inputs. It sits inside the NumberTheory layer that packages classical solvers behind LogicNat and LogicRat carriers, supporting the larger program of reading number-theoretic statements in the logic foundation. The module doc states that the final residual theorem can now be read as a recovered-rational theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.