IndisputableMonolith.NumberTheory.ErdosStrausRCL
Module supplies rational Erdős-Straus representations adapted to the Recognition Composition Law. Researchers attacking the conjecture via RCL cite these definitions and modular lemmas. The module assembles a predicate for rational representations together with explicit construction functions for factor pairs and divisor gates.
claimA positive rational $r$ admits a rational Erdős-Straus representation when there exist positive rationals $x,y,z$ such that $4/r = 1/x + 1/y + 1/z$. The corresponding integer statement requires $x,y,z$ to be positive naturals.
background
Recognition Science applies the J-cost function and the Recognition Composition Law to number-theoretic problems. This module introduces the predicate that certifies a rational admits an Erdős-Straus decomposition over the rationals. It records explicit constructions for balanced factor pairs, residual squares, and gate divisor pairs, plus modular classification lemmas for residues five and nine modulo twelve.
proof idea
The module is a definition module. It declares the representation predicate and supplies construction lemmas for balanced factor pairs, residual squares, and gate divisor pairs. Separate lemmas handle the five-mod-twelve and nine-mod-twelve cases for both rationals and naturals, together with a thirteen-mod-twentyfour statement.
why it matters in Recognition Science
These rational representations supply the base layer for the Erdős-Straus Recognition Rotation Hierarchy, which converts the RCL attack into a theorem-shaped skeleton by proving finite and gate pieces while isolating prime phase separation. The same content is transported by the Logic Erdős-Straus RCL adapter to the LogicRat setting. The module therefore advances the RCL attack on the conjecture by furnishing the rational interface.
scope and limits
- Does not prove the Erdős-Straus conjecture in full.
- Does not produce natural-number witnesses for the integer version.
- Does not resolve prime phase separation across residual quotients.
- Restricts to specific modular classes and rational decompositions.
used by (2)
declarations in this module (10)
-
def
HasRationalErdosStrausRepr -
theorem
repr_of_balanced_factor_pair -
theorem
repr_of_residual_square -
theorem
repr_of_gate_divisor_pair -
theorem
repr_c3_of_divisor_pair -
theorem
erdos_straus_five_mod_twelve -
theorem
erdos_straus_nine_mod_twelve -
theorem
erdos_straus_nat_five_mod_twelve -
theorem
erdos_straus_nat_nine_mod_twelve -
theorem
erdos_straus_thirteen_mod_twentyfour