Four-label compositions and signed block incidence

Definition

capacityFourLabelCompositions

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

finitecombinatoricsformalcapacitylinearalgebrapartition-incidence

Represent the eight compositions $1234$ , $1\mid234$ , $12\mid34$ , $123\mid4$ , $1\mid2\mid34$ , $1\mid23\mid4$ , $12\mid3\mid4$ , and $1\mid2\mid3\mid4$ by their explicit block families. For an arbitrary rational signed weight function $w$ on these eight objects, define

(Aw)_B=\sum_P w(P)\mathbf1_{\{B\in P\}}.

The sum is the explicit eight-term block-incidence evaluation. Define $\sigma$ to be $+1$ on $12\mid34$ and the discrete composition, $-1$ on $1\mid2\mid34$ and $12\mid3\mid4$ , and zero on the other four objects. These definitions specify the map and the proposed kernel direction for the four-label classification. No nonnegativity or probability normalization is imposed on $w$ . The bundle uses this fixed eight-constructor representation; it does not itself construct an equivalence with the general endpoint-certified partition representation.

Definition code

import Mathlib
import Definitions.Def_capacityFourLabelAtoms

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.
-/

namespace FormalCapacity.Finite

open Finset

/-- The eight compositions of four ordered labels.  Constructor names record
the non-singleton blocks; `halves` is `12|34`. -/
inductive Composition4
  | whole
  | rightTriple
  | halves
  | leftTriple
  | rightPair
  | middlePair
  | leftPair
  | discrete
  deriving DecidableEq

/-- Blocks of a four-label composition (with zero-based labels). -/
def Composition4.blocks : Composition4 → Finset (Finset Label4)
  | .whole => {{0, 1, 2, 3}}
  | .rightTriple => {{0}, {1, 2, 3}}
  | .halves => {{0, 1}, {2, 3}}
  | .leftTriple => {{0, 1, 2}, {3}}
  | .rightPair => {{0}, {1}, {2, 3}}
  | .middlePair => {{0}, {1, 2}, {3}}
  | .leftPair => {{0, 1}, {2}, {3}}
  | .discrete => {{0}, {1}, {2}, {3}}



/-- Incidence of a block in a composition. -/
def Composition4.blockIndicator (P : Composition4)
    (B : Finset Label4) : ℚ :=
  if B ∈ P.blocks then 1 else 0

/-- First-order block incidence of a signed law on all eight compositions. -/
def composition4FirstOrder (w : Composition4 → ℚ)
    (B : Finset Label4) : ℚ :=
  w .whole * Composition4.blockIndicator .whole B +
  w .rightTriple * Composition4.blockIndicator .rightTriple B +
  w .halves * Composition4.blockIndicator .halves B +
  w .leftTriple * Composition4.blockIndicator .leftTriple B +
  w .rightPair * Composition4.blockIndicator .rightPair B +
  w .middlePair * Composition4.blockIndicator .middlePair B +
  w .leftPair * Composition4.blockIndicator .leftPair B +
  w .discrete * Composition4.blockIndicator .discrete B

/-- The signed square, extended by zero to all eight compositions. -/
def composition4Square : Composition4 → ℚ
  | .halves | .discrete => 1
  | .rightPair | .leftPair => -1
  | _ => 0









end FormalCapacity.Finite

Source

The four-label correlation threshold, Theorem 2.2 and its four-label consequence (2.10). Unpublished research note (2026), N4_BLOCK_CORRELATION_NOTE.md, SHA-256 a9b67c132ca0e0af807fb917ca2322833b84e162c45a4da7329ee88fbe4f1c83. Exact formal source: formal_capacity/FormalCapacity/Finite/IntervalN4.lean, 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