Signed-Incidence Structure
A Structural Note on Compositional Verification
The total-unimodularity step has a Lean proof; field-independent rank follows by the written nonzero-minor argument.
Abstract
A short structural note supplying three facts used repeatedly in the Bulla corpus: (i) each row of the coboundary matrix has at most one +1 and one −1; (ii) the coherence fee is field-independent as a difference of two totally-unimodular ranks; and (iii) pairwise endpoint coupling is bounded by rank 2 on every (edge, dimension) block. A negative corollary records that any partition-style typed repair constraint is structurally wrong: enforcing it makes fee-zero repair impossible in 151 of 240 nonzero-fee compositions on the real-schema corpus.
Evidence and record
Which field-independent rank results follow from signed-incidence structure?
Signed-incidence row structure → totally unimodular → field-independent fee; pairwise endpoint coupling bounded by rank 2; partition-style typed repair structurally fails
Lean support is the signed-incidence determinant/total-unimodularity step in the completed archived source. The named fee_field_independent declaration concludes True; the field-rank consequence is a written nonzero-minor argument, not that declaration.
A counterexample under the paper's exact hypotheses.
not requested
- formalizes Column-Matroid Backbone