reprLogic_iff_classical
plain-language theorem explainer
The equivalence between the logic-native and classical rational Erdős-Straus representations holds by direct transport through the quotient map from LogicRat to ℚ. Number theorists working in constructive or logic-based foundations cite this adapter when porting classical results. The proof is a one-line reflexivity on the iff, relying on the definitional equality of the two predicates.
Claim. Let $n$ belong to the field of fractions of LogicInt. Then there exist nonzero rationals $x,y,z$ such that $4/n = 1/x + 1/y + 1/z$ after mapping $n$ to classical rationals if and only if the same existence holds directly when the predicate is evaluated on the logic rational $n$.
background
LogicRat is the field of fractions of LogicInt, formed as a quotient of PreRat. The recovery map toRat : LogicRat → ℚ is defined by lifting the core map that respects the setoid. HasRationalErdosStrausRepr on ℚ asserts existence of nonzero rationals x, y, z satisfying 4/n = 1/x + 1/y + 1/z. The sibling definition HasRationalErdosStrausReprLogic states the same predicate after applying toRat to its LogicRat argument. The module adapts the Erdős-Straus representation to logic-native rationals by this transport, as stated in the module doc.
proof idea
The proof is a one-line wrapper that applies Iff.rfl. This succeeds because the logic predicate is defined exactly as the classical predicate composed with toRat, making the two sides of the biconditional definitionally equal.
why it matters
This theorem completes the transport layer that lets classical Erdős-Straus results apply unchanged once a LogicRat is mapped to ℚ. It fills the adapter role described in the module doc for the NumberTheory layer. No downstream uses are recorded, but the declaration ensures consistency between the logic and classical formulations of the representation predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.