AdmissibleHardGate
plain-language theorem explainer
AdmissibleHardGate encodes the modular condition on residual gates for the hard class n ≡ 1 mod 4 in the Erdős-Straus rotation hierarchy. Number theorists examining the finite gate pieces of the Recognition Science attack on the conjecture cite this predicate when building bounded search structures. The definition consists of a single modular arithmetic equality that directly supports the divisibility arguments in downstream lemmas.
Claim. A natural number $c$ is an admissible hard gate if and only if $c ≡ 3 mod 4$. For any $n ≡ 1 mod 4$, this condition ensures that $n + c$ is divisible by 4.
background
The Erdős-Straus Recognition Rotation Hierarchy module converts the RCL attack into a proof skeleton by isolating finite gate pieces and two missing engines: prime phase separation across admissible residual quotients and reciprocal pair closure once phase support appears. The hard class consists of integers n congruent to 1 modulo 4. AdmissibleHardGate supplies the exact condition on the residual gate c that makes the quotient posting an integer.
proof idea
The declaration is a one-line definition that sets the predicate to the equality c modulo 4 equals 3. No tactics or lemmas are applied; the body is the direct statement of the congruence.
why it matters
This predicate is the hypothesis in admissible_gate_posts, which proves the divisibility 4 divides n + c under the hard class assumption. It parametrizes the bound_ok fields in BoundedSearchEngine and BoundedBalancedSearchEngine, as well as the supplies_generators in EffectivePrimePhaseInput. Within the Recognition framework it closes the gate condition for the rotation hierarchy without new axioms, leaving only the phase separation engines as open structure fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.