Lesson 2.1 · Chapter 2: The knot test
The knot test
Erase any variable. Does the binding disappear, or does a smaller constraint survive?
From John Cullen’s knotlab guide
Explore the idea
Erase a variable and inspect what remains
Erasing means forgetting: a visible state is allowed whenever at least one choice of the erased bit completes it. It does not mean setting that bit to zero.
If A and B, then c
Visible bits: A, B, c
7 of 8 visible states allowed: a constraint remains.
Original relation: a logical knot—constrained as a whole, free after every erasure.
The setting. Read a system of constraints as the set of joint states it allows. Auxiliary "witness" variables may appear, and are quantified away. Nothing outside the constraints, such as an executor or a scheduler, may supply an input. A verdict depends only on the allowed states, never on how the constraints are written.
Each loop contributes an open distinction. The contact is one more variable,
c. Erasing a loop forgets it: its variable is no longer constrained by
anything.
The test. A relation over the loops' distinctions and the contact is a knot when:
- K1, binding: it is constrained as a whole;
- K2, loss on erasure: forgetting any one variable, a loop's or the contact's, leaves the others unconstrained;
- K3, coexistence: some joint state is allowed (K2 already implies it).
In short: constrained as a whole, unconstrained in every part, like Borromean rings. Forgetting the contact must free the loops too, so loops tied directly to each other do not count.
Knots and non-knots. Six relations against the test:
| Relation | Knot? | Why |
|---|---|---|
¬A ∨ ¬B ∨ c (the atom: if A and B, then c) | yes | excludes one state; every pair is free |
A ⊕ B ⊕ c = 0 (parity) | yes | excludes four states; every pair is free |
| not-all-equal(A, B, c) | yes | excludes 000 and 111; every pair is free |
(¬A ∨ c) ∧ (¬B ∨ c) (a common hub) | no | forget B, and A still forces c |
A ≠ B, with c unused | no | forget c, and A and B stay tied |
c = A ⊕ B with A fixed true | no | A is not open, so it is constrained alone |
PYTHONPATH=tools python3 -m knotlab check --cnf "~A ~B c" --loops A B --contact c
PYTHONPATH=tools python3 -m knotlab check --cnf "~A c; ~B c" --loops A B --contact c
The first command reports a knot. The second reports a hub, and explains which
binding survives each erasure. Proved (Lean): ForgettingKernel.lean
(atom_isKnot, parity_isKnot, hub_not_knot, tied_not_knot).