classical_of_reprLogic
plain-language theorem explainer
The theorem shows that a LogicRat satisfying the logic-native Erdős-Straus representation condition maps under the recovery function toRat to a classical rational satisfying the standard representation predicate. Researchers reconstructing classical number theory inside logic-based foundations would cite this transport step when moving results between LogicRat and ℚ. The proof is a direct one-line term that applies the definition of HasRationalErdosStrausReprLogic.
Claim. Let $n$ be a logic rational. If $n$ admits a logic-native Erdős-Straus representation, then the classical rational obtained by applying the recovery map toRat to $n$ admits the classical Erdős-Straus representation.
background
LogicRat is the field of fractions of LogicInt, constructed as the quotient of PreRat by the induced setoid. The map toRat : LogicRat → ℚ is defined by lifting the core projection toRatCore while preserving the equivalence relation. HasRationalErdosStrausReprLogic n is defined exactly as ErdosStrausRCL.HasRationalErdosStrausRepr (toRat n). The module adapts the classical Erdős-Straus rational representation results to the logic-native setting by routing all algebraic content through this recovery map.
proof idea
The proof is the one-line term h. Because HasRationalErdosStrausReprLogic n is literally defined to be ErdosStrausRCL.HasRationalErdosStrausRepr (toRat n), the supplied hypothesis is already the required conclusion.
why it matters
This declaration supplies the forward transport direction in the equivalence between logic-native and classical Erdős-Straus representations. It allows classical results proved over ℚ to be stated inside the LogicRat layer without additional hypotheses. The module positions the lemma as part of the adapter that connects the Recognition Science logic foundation to the existing number-theoretic surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.