reprLogic_fromRat_of_classical
plain-language theorem explainer
The theorem shows that a classical rational Erdős-Straus representation on n lifts directly to the logic-native representation on fromRat n. Workers bridging classical number theory into the logic layer of Recognition Science cite it when transporting results across the Rat-LogicRat interface. The proof is a one-line simpa that unfolds the logic representation definition and invokes the round-trip equality toRat (fromRat n) = n.
Claim. Let $n$ be rational. Suppose there exist nonzero rationals $x,y,z$ such that $4/n = 1/x + 1/y + 1/z$. Then the logic-native rational obtained by applying fromRat to $n$ satisfies the corresponding logic-native Erdős-Straus representation condition.
background
LogicErdosStrausRCL adapts the classical Erdős-Straus rational representation to the logic setting. The classical predicate HasRationalErdosStrausRepr (n : ℚ) asserts existence of nonzero rationals x, y, z obeying 4/n = 1/x + 1/y + 1/z. Its logic counterpart HasRationalErdosStrausReprLogic (m : LogicRat) is defined by transporting via toRat: it holds precisely when the classical predicate holds on toRat m. The map fromRat : ℚ → LogicRat is the inverse construction that builds a LogicRat from numerator and denominator integers; the supporting theorem toRat_fromRat states that toRat (fromRat q) = q for every rational q.
proof idea
The proof is a one-line wrapper. It applies simpa with the definitions of HasRationalErdosStrausReprLogic and the round-trip lemma toRat_fromRat, reducing the goal to the supplied classical hypothesis h.
why it matters
This declaration closes the transport step that lets classical Erdős-Straus results enter the logic-native layer. It is invoked directly by box_phase_hit_gives_repr_logic to obtain HasRationalErdosStrausReprLogic from a phase hit, and by erdos_straus_residual_from_phaseBudget_logic to handle residual traps inside the phase-budget engine. The step sits inside the broader program of recovering rational arithmetic inside the logic foundation before feeding into the Recognition Composition Law and the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.