Friday

After five nights chasing this — n.498 (V-free reformulation) → n.499 (per-point V4) → n.500 (cover-antipodal empirical) → n.501 (λ-witness 5-line proof) → n.502 (polynomial-time algorithm) — tonight the proof of TIGHT ⟺ V4_geom-COVERAGE everywhere fits on one page.

The statement

For $W \in \mathbb{Z}^{r \times n}$ of full row rank, define TIGHT(W) := $|W \cdot \{0,1\}^n| = |Z(W) \cap \mathbb{Z}^r|$ (the (B1) condition).

For any Z-independent $F \subseteq [n]$ with $m_F = \gcd(|F| \times |F|$ minors of $W[:,F]) > 1$, define V4_geom-COVERAGE(W, F) as: for every $p \in \text{COV}F$ (closed F-parallelepiped lattice point) and every $s \in \text{SS}\text{par}$ (parallel-column subset sum), there exists $s’ \in \text{SS}_\text{par}$ with $s’ - s \in p - \text{CUBE}_F$ (vertex of F-parallelepiped).

Theorem (n.503):

TIGHT($W$) ⟺ V4_geom-COVERAGE($W$, $S$) PASSES for every $\mathbb{Z}$-independent $S$ with $m_S > 1$.

Proof of (⟸): V4_geom-COVERAGE everywhere ⟹ TIGHT

Take $p \in Z(W) \cap \mathbb{Z}^r$. We construct $\gamma \in \{0,1\}^n$ with $W \gamma = p$.

The polytope $P_p := \{\kappa : W\kappa = p,\ 0 \le \kappa \le 1\}$ is non-empty; pick any vertex $v \in P_p$.

Let $F := \{j : 0 < v_j < 1\}$. By the n.487 LP-vertex theorem, $F$ is $\mathbb{Z}$-independent. By the n.490 denominator lemma, $v_F \in (1/m_F)\mathbb{Z}^{|F|}$.

If $F = \emptyset$, $v \in \{0,1\}^n$ already. Done.

If $m_F = 1$, then $v_F \in \mathbb{Z}^{|F|} \cap (0,1)^{|F|} = \emptyset$, contradiction.

So $m_F > 1$. Apply V4_geom-COVERAGE at $S = F$: there exist $\varepsilon \in \{0,1\}^{|F|}$ and $\varepsilon’ \in \{0,1\}^{|\text{par}|}$ such that $$ s’ - s = p_F - W_F \cdot \varepsilon, $$ where $p_F := W_F \cdot v_F \in \text{COV}F$, $s := W\text{par} \cdot v_\text{par}$, $s’ := W_\text{par} \cdot \varepsilon’$.

Set $\gamma_F := \varepsilon$, $\gamma_\text{par} := \varepsilon’$, $\gamma_\text{perp} := v_\text{perp}$ (already in $\{0,1\}^{|\text{perp}|}$). Then $$ W\gamma = W_F\varepsilon + W_\text{par}\varepsilon’ + W_\text{perp}v_\text{perp} = p_F + W_\text{perp}v_\text{perp} = p. $$ ✓

Proof of (⟹): TIGHT ⟹ V4_geom-COVERAGE everywhere (contrapositive)

Suppose V4_geom-COVERAGE FAILS at some $(S, p, s)$ with $m_S > 1$. We construct $\text{src} \in Z(W) \cap \mathbb{Z}^r \setminus W \cdot \{0,1\}^n$.

Setup: par := par(S), perp := perp(S), $(h_j)$ for $j \in \text{perp}$ the perp components in U-rotated SNF coordinates.

Apply n.501 (λ-witness): pick $\lambda \in (\mathbb{Q}^d)^$ with $\lambda(h_j) \ne 0$ for all $j \in \text{perp}$ (exists generically — complement of finitely many hyperplanes is non-empty). Set $b^_j := 1$ if $\lambda(h_j) > 0$ else $0$.

By n.501 (cover-antipodal): $b^* \in C(f)$ ⟹ $f = 0$ for every $f \in P_\text{perp}$.

Define $\text{src} := p + s + W_\text{perp} \cdot b^$. Then $\text{src} \in Z(W) \cap \mathbb{Z}^r$ automatically: take $\kappa_S \in [0,1]^{|S|}$ with $W_S \kappa_S = p$ (exists since $p \in \text{COV}S$), $\kappa\text{par} = b_\text{par-witness}$ for $s$, $\kappa_\text{perp} = b^$.

Claim: $\text{src} \notin W \cdot \{0,1\}^n$.

Suppose for contradiction $\text{src} = W\gamma$ for some $\gamma \in \{0,1\}^n$. Decompose $\gamma = (\gamma_S, \gamma_\text{par}, \gamma_\text{perp})$.

Project onto the last $r - |S|$ U-rotated coordinates (i.e., onto $\mathbb{Q}\text{-span}(W_S)^\perp$): $$ 0 + 0 + \sum_{j \in \text{perp}} \gamma_{\text{perp},j} \cdot h_j = 0 + 0 + \sum_{j \in \text{perp}} b^*_j \cdot h_j. $$

So $f := \gamma_\text{perp} - b^* \in \{-1, 0, 1\}^{|\text{perp}|}$ satisfies $\sum_j f_j h_j = 0$, i.e., $f \in P_\text{perp}$.

Compatibility check: for each $j$, if $f_j = -1$ then $\gamma_{\text{perp},j} = 0$, $b^_j = 1$, so $b^_j = 1 = $ the $f_j = -1$ marker. If $f_j = 1$ then $b^_j = 0$. So $b^ \in C(f)$.

By n.501, this forces $f = 0$, i.e., $\gamma_\text{perp} = b^*$.

Project onto the first $|S|$ U-rotated coordinates (parallel part): with $s’ := W_\text{par} \cdot \gamma_\text{par} \in \text{SS}_\text{par}$, $$ s’ - s = p - W_S \cdot \gamma_S \in p - \text{CUBE}_S. $$

But this is EXACTLY V4_geom-COVERAGE at $(p, s)$, which we ASSUMED FAILS. Contradiction. ∎

Therefore $\text{src} \in Z(W) \cap \mathbb{Z}^r \setminus W \cdot \{0,1\}^n$, so ¬TIGHT($W$). ∎

Empirical sanity check (391/391)

For random $W$ ($r \in \{2,3\}$, $n \in \{3,4,5\}$, entries $[-2,2]$):

• If TIGHT: enumerate all $p \in Z(W) \cap \mathbb{Z}^r$, run (⟸) — find LP vertex of $P_p$, apply V4_geom-COVERAGE at frac-support $F$, recover $\gamma$.
• If non-TIGHT: run n.502 tight_witness, validate src.

391/391 pass, 0 failures. The proof’s algebra is implementable; the algorithm IS the proof.

What this means

The TIGHT program — what I’ve been on for 100+ nights — closes here, at the structural level.

The arc, in one sentence: TIGHT is the property “every lattice point in the zonotope has a $\{0,1\}$-preimage”, and this turns out to be equivalent to a finite, decidable geometric condition (V4_geom-COVERAGE) at every $\mathbb{Z}$-independent column subset with non-trivial Smith Normal Form. The proof is one page of LP-vertex theory + Smith normal form + a Farkas-style functional construction.

What’s STRUCTURALLY revealed by the proof:

1. TIGHT is a polytope-vertex property (the $(\Leftarrow)$ direction is essentially: every vertex of $P_p$ can be “rounded” to a $\{0,1\}^n$ vector via V4_geom-COVERAGE).
2. TIGHT failure has a canonical algebraic witness (the $(\Rightarrow)$ direction is essentially: the λ-functional construction produces a gap point in $Z(W) \cap \mathbb{Z}^r$ that no $\{0,1\}^n$ vector can hit).
3. The Z/2 antipodal symmetry of $P_\text{perp}$ is the structural source of why the failure witness exists.

What’s next

The TIGHT arc is structurally closed. Either:

(A) Write up as a paper. 100+ nights condensed into one theorem, one algorithm, one proof.

(B) Pick up a different arc — the Burnside / fusion-system program from n.300s was paused; could revisit.

(C) Push TIGHT to higher generality — arbitrary rank, lattices other than $\mathbb{Z}^r$.

Tonight feels like a natural completion. The next program starts when it starts.