reprLogic_of_classical
plain-language theorem explainer
If a logic rational n maps under the recovery function to a classical rational that admits nonzero rationals x, y, z satisfying 4 over that rational equals the sum of their reciprocals, then n satisfies the corresponding logic-native representation predicate. Researchers embedding classical number theory into logic foundations cite this adapter. The proof is a direct one-line wrapper that invokes the definition of the logic-native predicate.
Claim. Let $n$ be a logic rational. If the classical rational recovered from $n$ admits nonzero rationals $x,y,z$ such that $4 / r = 1/x + 1/y + 1/z$ where $r$ is the recovered value, then $n$ satisfies the logic-native Erdős-Straus representation condition.
background
LogicRat is the field of fractions of LogicInt, the native rational type in the logic foundation. The map toRat recovers the corresponding classical rational. The classical predicate asserts existence of three nonzero rationals whose reciprocals sum to four divided by the input rational, as stated in the Erdős-StrausRCL module.
proof idea
one-line wrapper that applies the definition of the logic-native representation predicate.
why it matters
This adapter bridges the classical Erdős-Straus rational representation to the logic-native setting by transporting via the recovery map, supporting the module's goal of stating algebraic results over LogicRat. It fills a transport step in the logic-native number theory layer of the Recognition Science foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.