Alterna

This page is the chapter for a deposit that had four inbound citations and no home: “Alternating Forms Vanish Beyond Dimension: A Mechanized Proof in Lean 4 with Application to Contact Integrability,” 10.5281/zenodo.20710023, deposited 16 June 2026. Metadata verified against the Zenodo record on 2026-08-12.

1.  The theorem

The Lean 4 proof is twelve lines and rests on two Mathlib lemmas: AlternatingMap.map_linearDependent and LinearIndependent.fintype_card_le_finrank. The argument is the obvious one once stated: $m$ vectors in a rank-$n$ module with $m > n$ are linearly dependent, and an alternating map kills any linearly dependent tuple.

It is not a deep theorem. It is a correctly scoped one, and that is the point of the paper — the value is in what it is then applied to, and in the honesty about where the application stops.

2.  The application: $N_J$ on the Reeb direction

On the dm³ contact 3-manifold with $\alpha = dz - r^2\,d\theta$, the operator algebra forces an almost complex structure $J$ with $J^2 = -\mathrm{id}$ (Ch 15 · The Complex Turn). Its integrability obstruction is the Nijenhuis tensor

$N_J(X,Y) = [JX,JY] - J[JX,Y] - J[X,JY] - [X,Y]$

$N_J$ is alternating and bilinear, so $m = 2$. The Reeb-orbit direction $\mathrm{span}(R_\alpha)$ — the attractor $\Gamma$ — has rank $n = 1$. Since $2 > 1$, Alterna applies pointwise:

That is the whole of level 1. It is true, it is proved, and it is a dimension count — which is exactly how the deposit describes it.

3.  Two corollaries that do not follow

Until 2026-08-12, Ch 15's Theorem 15.2 drew two further conclusions from this vanishing. Both are false, and both fail for the same elementary reason: parity.

The underlying fact: a $J$-invariant subspace is even-dimensional. If $v \in T$ and $Jv \in T$ with $J^2 = -\mathrm{id}$, then $\{v, Jv\}$ are linearly independent, so $\dim \geq 2$. A one-dimensional line cannot be $J$-invariant at all.

4.  The three-level integrability tower

The deposit is explicit that it closes one level and names what the others need. Restating it here so no downstream page has to guess:

Level 2 is where the mathematics actually is. The moment the distribution has rank 2, the inequality $m > n$ turns into $m = n$ and Alterna is silent. Whether $N_J$ vanishes on $\xi$ is a real question about the interaction of the fold operator $F$ with the Reeb flow, and it is not answered by this deposit.

5.  A name collision worth recording

“Alternating vanishing” is not a unique phrase. In August 2026 an external language model, asked about this corpus, produced an “Alternating Vanishing Theorem” concerning the 2-adic valuation $\lambda_3(x) = v_2(3x+1)$ and the vanishing of its dyadic gradient $\nabla_k \lambda_3$ on residue classes of $\mathbb{Z}_2$. That is a different object entirely — number theory, not multilinear algebra.

It also does not hold as stated. Its claim that the gradient is non-zero on the complementary class $U_k(2^{k-1}-1)$ fails for every $k \geq 3$; by its own argument $v_2 = 1$ on both classes, so the gradient vanishes on both. Checked by exhaustive enumeration:

The salvageable content is that last line, and it is standard Collatz arithmetic: half of all odd numbers drop by exactly one factor of two. There is no alternating hierarchy across scales $k$ — a single mod-4 condition does all the work.

The precedent, stated exactly. Two different statements in this corpus shared the number 5.3 for four months. Vol I §5.3 asserts chain-level non-commutativity — the operators $C, K, F, U$ do not commute, the sequence is order-dependent. It asserts no mechanism, it is true, and it is kernel-verified in Theorem53NonCommutativity.lean. Lemma 5.3 in book4/chIV-orthogonality.html carried the same number and a different claim: it upgraded the abstract statement into a specific mechanism — a gate acting on a pointwise fold, producing a $\delta$ boundary term. That upgrade is invalid. Chapters citing “5.3” inherited whichever they assumed; five carrier files were repaired between 18 and 20 July 2026, and each had to be read to determine which 5.3 it meant before it could be fixed.

What the mechanism actually is. A label is a pointer, and prose resolves pointers by assumption rather than by lookup. Nothing in the act of writing “by 5.3” forces the writer to visit the referent. So a collision does not produce an error — it produces a fork, silently, at every citation site, and the fork is invisible to the author as well as the reader. This is why the cost is not the false statement but the re-reading: repair requires resolving every pointer by hand, and the number of pointers grows while the collision stands.

Why a name is worse than a number. A numeric collision is at least a detectable condition: two things numbered 5.3 in one corpus can be found by searching the corpus. A name collision need not be contained by the corpus at all. “Alterna” here denotes the multilinear-algebra result; elsewhere it denotes something else, and the version outside is the unsound one. No search over this repository can detect a collision whose other half lives outside it — detection requires knowing the outside, which is not a property any tool here has.

That asymmetry changes the available repair. In the 5.3 case both statements were inside the corpus, so a correction could reach both and the collision could be ended. Here only one half is reachable. This paper can state what Alterna is; it cannot revise what the name means elsewhere. A collision that cannot be ended can only be disambiguated at every point of use — which is what §6 is, and why each row of it carries a status rather than a bare link.

The discipline this yields, offered as method rather than as local housekeeping:

This paper carried the last defect until 22 August 2026. The passage above originally cited the 5.3 collision by linking this repository's working ledger at its live path. That file is rewritten by every working session; on 21–22 August it was split in two, and the cited section survived by accident of how the split was scoped. Had it moved, this link would have pointed at a file that no longer contained what it cites, and nothing would have reported an error — a link to a live path cannot fail on a missing section. The citation is now pinned to an immutable commit: the 5.3 collision, as of 8855044. The general form of that defect — a claim bound to an artifact that moves underneath it — is WP73.

6.  Where this is cited

7.  How to cite