pith. machine review for the scientific record. sign in
def definition def or abbrev high

GateClosureWitness

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  70def GateClosureWitness (n c : ℕ) : Prop :=

proof body

Definition body.

  71  ∃ x N d q : ℚ,
  72    (n : ℚ) ≠ 0 ∧
  73    x ≠ 0 ∧
  74    (c : ℚ) ≠ 0 ∧
  75    N = (n : ℚ) * x ∧
  76    x = ((n : ℚ) + (c : ℚ)) / 4 ∧
  77    d * q = N ∧
  78    (N + d) / (c : ℚ) ≠ 0 ∧
  79    (N + N * q) / (c : ℚ) ≠ 0
  80
  81/-- The RCL divisor-pair bridge: a gate closure witness gives a rational
  82Erdős-Straus representation. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.