GateClosureWitness
plain-language theorem explainer
GateClosureWitness packages the existential data for a rational divisor-pair closure on natural numbers n and c. Researchers applying the Recognition Composition Law to the Erdős-Straus conjecture cite it to supply the exact inputs needed by the representation theorem. The definition is a direct encoding of the quadruple of rationals and the listed non-zero and equality conditions.
Claim. For natural numbers $n$ and $c$, the predicate holds if there exist rationals $x,N,d,q$ satisfying $n≠0$, $x≠0$, $c≠0$, $N=nx$, $x=(n+c)/4$, $dq=N$, $(N+d)/c≠0$, and $(N+Nq)/c≠0$.
background
The definition sits inside the Erdős-Straus Recognition Rotation Hierarchy module. That module converts the RCL attack into a theorem-shaped skeleton, proving finite and gate pieces while isolating prime phase separation and reciprocal pair closure as explicit future assumptions. The module doc states: “This module turns the current RCL attack into a theorem-shaped proof skeleton.”
proof idea
As a definition it directly asserts the required existential. No lemmas or tactics are invoked; the body simply lists the four rationals together with the eight conjuncts that encode the divisor-pair relations.
why it matters
It supplies the hypothesis type for the theorem gate_closure_witness_gives_repr, which concludes that the witness yields a rational Erdős-Straus representation. The same definition appears as a premise inside the ReciprocalPairClosureEngine structure. In the Recognition framework it supplies the gate-closure step that links the RCL divisor-pair bridge to the rotation hierarchy, advancing the finite part of the argument while leaving the two missing engines open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.