repr_c3_of_divisor_pair
plain-language theorem explainer
repr_c3_of_divisor_pair shows that a nonzero rational n admits a rational Erdős-Straus representation whenever x is fixed to (n+3)/4, N equals n times x, and a divisor pair d q equals N satisfies the two derived nonzeroness conditions. Number theorists reducing the Erdős-Straus conjecture via rational ledger splits would cite this gate-3 case for the n ≡ 1 mod 4 family. The proof is a one-line wrapper that specializes the general gate-divisor-pair lemma to c = 3 after a trivial norm_num check.
Claim. Let $n, x, N, d, q$ be nonzero rationals satisfying $N = n x$, $x = (n + 3)/4$, $d q = N$, $(N + d)/3 ≠ 0$, and $N(1 + q)/3 ≠ 0$. Then there exist nonzero rationals $x', y, z$ such that $4/n = 1/x' + 1/y + 1/z$.
background
The module records the algebraic reduction behind the RCL attack on the Erdős-Straus conjecture. After the first denominator x is chosen, the residual equation becomes c/N = 1/y + 1/z where c = 4x - n and N = n x. Clearing denominators produces the balanced factor-pair condition (c y - N)(c z - N) = N², the discrete ledger form of the reciprocal split.
proof idea
One-line wrapper that applies repr_of_gate_divisor_pair with the gate constant c specialized to 3. The only auxiliary step is the norm_num verification that 3 ≠ 0.
why it matters
The result is invoked by erdos_straus_nat_nine_mod_twelve to obtain explicit natural-number witnesses for every n = 12k + 9. It supplies the dominant hard-class gate for n ≡ 1 mod 4 inside the RCL ledger reduction, as stated in the module documentation. Within the Recognition monolith this supplies a concrete algebraic identity that aligns with the composition-law reductions used throughout the number-theory layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.