admissible_gate_posts
plain-language theorem explainer
Admissible gate posts establishes that if n is congruent to 1 modulo 4 and c is an admissible hard gate then 4 divides n plus c. Number theorists building the Erdős-Straus rotation hierarchy would cite it as the basic closure fact for the hard class. The proof is a one-line wrapper that unfolds the gate predicate and applies the omega tactic to confirm the divisibility.
Claim. If $n ≡ 1 mod 4$ and $c ≡ 3 mod 4$, then $4$ divides $n + c$.
background
The module develops the Erdős-Straus Recognition Rotation Hierarchy as a theorem-shaped proof skeleton for the RCL attack. It isolates two missing engines: prime phase separation across admissible residual quotients and reciprocal pair closure, without new axioms. AdmissibleHardGate is the predicate requiring c modulo 4 equals 3, the admissible residual gate for the hard class n modulo 4 equals 1. The supplied doc-comment states that c congruent to 3 modulo 4 is exactly the condition making n plus c divisible by 4 in the hard class.
proof idea
The proof is a one-line wrapper. It unfolds AdmissibleHardGate to obtain c modulo 4 equals 3, then applies Nat.dvd_of_mod_eq_zero together with the omega tactic to deduce that n plus c is divisible by 4.
why it matters
This result closes the basic gate posting step in the rotation hierarchy and directly enables the representation of gate divisor pairs in repr_of_gate_divisor_pair. It supplies the finite/gate piece of the Erdős-Straus skeleton, leaving prime phase separation and reciprocal pair closure as open structure fields. In the Recognition Science framework it supports the RCL composition law by ensuring consistent residual quotients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.