IndisputableMonolith.NumberTheory.LogicErdosStrausRCL
This module supplies logic-native rational representations for the Erdős-Straus conjecture by transporting the classical algebraic reduction into LogicRat structures. Number theorists working inside Recognition Science foundations cite it when moving between classical ℕ results and LogicNat/LogicRat versions. The module consists of predicate definitions and equivalence theorems that link the two settings without new algebraic content.
claimThe module defines a predicate HasRationalErdosStrausReprLogic such that a rational solution exists in the logic setting if and only if it exists classically, via the equivalences reprLogic_iff_classical, reprLogic_of_classical, classical_of_reprLogic, and reprLogic_fromRat_of_classical, all built over the residual equation $c/N = 1/y + 1/z$ with $c = 4x - n$ and $N = nx$.
background
The module imports RationalsFromLogic, which supplies the LogicRat and LogicNat carriers, and ErdosStrausRCL, whose doc-comment records the algebraic reduction behind the RCL attack: after fixing the first denominator x the residual equation becomes c/N = 1/y + 1/z with c = 4x - n and N = nx. These two upstream modules together furnish the setting in which the logic-native representation is expressed. The sibling declarations HasRationalErdosStrausReprLogic, reprLogic_iff_classical and its companions then encode the transport between the classical and logic-native forms of this representation.
proof idea
This is a definition module, no proofs. It introduces the predicate HasRationalErdosStrausReprLogic together with four equivalence theorems that relate the logic-native and classical representations of the same rational solution.
why it matters in Recognition Science
The module feeds LogicErdosStrausBoxPhase, whose doc-comment states that the final theorem transports the existing ℕ box-phase result and returns it as a LogicRat representation via LogicErdosStrausRCL. It therefore supplies the missing logic-native adapter required to close the square-budget box phase inside the Recognition framework.
scope and limits
- Does not prove existence of solutions for arbitrary n.
- Does not compute explicit y and z values.
- Does not address the full Erdős-Straus conjecture beyond the rational-representation step.
- Does not introduce new algebraic identities beyond those in ErdosStrausRCL.