The unique hidden direction on four-label compositions

Proved

FormalCapacity.Finite.composition4_firstOrder_zero_iff

by ryanshin · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

finitecombinatoricsformalcapacitylinearalgebrapartition-incidence

Let $\mathcal C_4$ be the eight explicitly represented compositions $1234$ , $1\mid234$ , $12\mid34$ , $123\mid4$ , $1\mid2\mid34$ , $1\mid23\mid4$ , $12\mid3\mid4$ , and $1\mid2\mid3\mid4$ . For $w:\mathcal C_4\to\mathbb Q$ , put $(Aw)_B=\sum_{P\in\mathcal C_4}w(P)\mathbf1_{\{B\in P\}}$ and

\sigma=\delta_{12\mid34}+\delta_{1\mid2\mid3\mid4}-\delta_{1\mid2\mid34}-\delta_{12\mid3\mid4}.

Then

\bigl(\forall B\subseteq\{1,2,3,4\},\ (Aw)_B=0\bigr)\quad\Longleftrightarrow\quad\exists t\in\mathbb Q,\ w=t\sigma.

This identifies the full invisible subspace of the explicitly encoded eight-composition incidence map, rather than only exhibiting one relation. Signed weights may be negative and need not sum to one. The formal conclusion is an existential scalar characterization; it does not add a separate equivalence with the general interval-partition representation.

Preamble

import Mathlib
import Definitions.Def_capacityFourLabelAtoms
import Definitions.Def_capacityFourLabelCompositions

set_option autoImplicit false

/-!
# The unique hidden direction on four ordered labels

There are eight interval partitions (compositions) of four ordered labels.
This file writes all eight down and proves directly that the kernel of their
first-order interval-block incidence map is the single line generated by

`12|34 + 1|2|3|4 - 1|2|34 - 12|3|4`.

Thus the signed square from `N4.lean` is not merely an example: among signed
laws on all four-label compositions it is the unique invisible direction,
up to scale.
-/

open FormalCapacity.Finite

open Finset

Formal statement

theorem FormalCapacity.Finite.composition4_firstOrder_zero_iff
    (w : Composition4 → ℚ) :
    (∀ B : Finset Label4, composition4FirstOrder w B = 0) ↔
      ∃ t : ℚ, w = t • composition4Square := by
  sorry

Source

The four-label correlation threshold, four-label kernel consequence (2.10) of Theorem 2.2. Unpublished research note (2026), N4_BLOCK_CORRELATION_NOTE.md, SHA-256 a9b67c132ca0e0af807fb917ca2322833b84e162c45a4da7329ee88fbe4f1c83. Exact formal source: formal_capacity/FormalCapacity/Finite/IntervalN4.lean, lines 133–145, declaration FormalCapacity.Finite.composition4_firstOrder_zero_iff, source-file SHA-256 035e93f3c39d26eb75171329697836a0fd913862701b1b720dd27c570f8e84eb. Local source archive; no public repository URL or commit is asserted. Upload checked with Lean 4.33.1 and Mathlib 0df444a360eaa60ab8c11dca51a86af692955474.

View graph