Blueprint: the converse audit

The third part of the axiom audit: the chord diagram of a boundary pairing, the super Gram identity, the interface lift, and the converse itself. The prose between pins says what each step contributes; read Blueprint.lean first for the forward direction.

Chords of the boundary pairing

A subset's boundary flags pair up into chords; the involution that records them, extended by the identity off the used labels, is what the Koszul sign is read from.

The Gram identity

The connection matrix of a parameter with a super Gram factorization has bounded rank, which is the converse's engine.

The interface lift

Transition data carried up the gluing interface one cut at a time and back down: the lift, the two glue branches, and the round trip on directions and on the matching.

The base sum and the converse

The subset sum over the composition's base, its independence of the free bits, and the theorems of record.

Definition 5, evaluated

The paper's worked example: the loop graph against the functional whose mixed partition function is the characteristic polynomial. Its value θ − 2 fixes the loop's two incidences, the Eulerian condition, the circuit sign and the η-convention all at once; adjoining a free circle sends the same functional to 0, which fixes the loop/free-circle distinction.