gate_ladder_forced
plain-language theorem explainer
If n ≡ 1 mod 4 and 4x = n + c holds for natural numbers n, c, x, then c ≡ 3 mod 4. Number theorists extending the Erdős-Straus conjecture inside the Recognition Science rotation hierarchy cite this to fix admissible residual gates for the hard class. The proof is a direct unfolding of AdmissibleHardGate followed by arithmetic resolution.
Claim. If $n ≡ 1 mod 4$ and there exists a natural number $x$ such that $4x = n + c$, then $c ≡ 3 mod 4$.
background
The module develops the Erdős-Straus Recognition Rotation Hierarchy as a theorem-shaped proof skeleton for the current RCL attack. It proves finite and gate pieces while isolating two missing number-theoretic engines: prime phase separation across admissible residual quotients and reciprocal pair closure once sufficient phase support appears. No new axioms are introduced; the engines remain explicit structure fields for future supply.
proof idea
The proof unfolds the definition of AdmissibleHardGate (c % 4 = 3) and applies the omega tactic to resolve the arithmetic from the hypotheses n % 4 = 1 and 4x = n + c.
why it matters
This fills one of the finite/gate pieces required by the Erdős-Straus Recognition Rotation Hierarchy. It constrains residual gates precisely when n lies in the hard class n ≡ 1 mod 4. The module isolates the two missing engines (prime phase separation and reciprocal pair closure) that this gate condition prepares for; the open question remains supplying those engines as structure fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.