Proof of `A fixed-alphabet regular gap reduction for 3-SAT`
groundedproofs/Lax253009Proofs/GapSatisfiability.lean · lax-253009
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Apply the ported Dinur gap amplifier, regularize with its fixed expander family, and number the finite label, vertex, and dart-label spaces. An empty output can occur only on satisfiable inputs and is replaced by one unconstrained vertex of the same fixed degree.