HasRationalErdosStrausReprLogic
plain-language theorem explainer
The definition adapts the classical rational Erdős-Straus representation to logic-native rationals. Researchers working in the Recognition Science logic foundation cite it when moving results between LogicRat and the classical rational surface. It is a direct one-line wrapper that applies the classical predicate after the toRat recovery map.
Claim. Let $n$ be an element of the logic rationals. Then $n$ admits a rational Erdős-Straus representation if there exist nonzero classical rationals $x,y,z$ such that $4/ι(n)=1/x+1/y+1/z$, where $ι$ denotes the recovery map from logic rationals to classical rationals.
background
LogicRat is the field of fractions of LogicInt. The map toRat recovers the corresponding element of ℚ. The classical predicate HasRationalErdosStrausRepr asserts existence of three nonzero rationals $x,y,z$ satisfying $4/n=1/x+1/y+1/z$ for a classical rational $n$ (from ErdosStrausRCL).
proof idea
One-line wrapper that applies the classical HasRationalErdosStrausRepr predicate to the image of the input under toRat.
why it matters
This definition supplies the logic-native interface for rational Erdős-Straus representations. It is used by box_phase_hit_gives_repr_logic and by the equivalence reprLogic_iff_classical together with the transport theorems classical_of_reprLogic and reprLogic_of_classical. It bridges the classical number-theoretic statement to the logic layer that supports phase-budget and box-phase constructions in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.