Claim Ledger

The coherence fee decomposes additively over named semantic dimensions: fee(G) = Σ feeσ(G), exactly, under the Dimension-Field Disjointness hypothesis. The per-dimension fee profile is a vector-valued severity invariant whose ℓ¹ norm is the total fee.

Verified on 1,596 compositions (full pairwise closure of 57-manifest registry) and 703 real-schema compositions. One-line matroid-direct-sum proof under DFD.

For every Bulla composition G, fee(G) = corank of the observable column set in the linear matroid on the columns of the full coboundary matrix. The fee is a matroid corank, not merely a rank difference.

Structural identity verified on 703 compositions. Seven load-bearing corollaries cover repair filtrations, leverage conservation, the rank-H¹ identity, and termination bounds.

The fee equals the difference of cokernel dimensions: fee(G) = dim H¹(δ_obs) − dim H¹(δ_full). Proven both on paper (two-line rank-nullity argument) and in Lean 4 against Mathlib, with no sorry and standard axioms only.

Requires column-compression hypothesis and finite-dimensional ℚ-coefficients. Both hold for every Bulla composition under the current coboundary construction.

rank K(G) = fee(G) on all compositions, and Σ ℓⱼ = fee(G) (leverage conservation). Verified in exact rational arithmetic on 703 compositions with zero violations.

Lean-formalized: witness_gram_rank_eq_fee and leverage_conservation theorems, both Aristotle-closed.

Under Dimension-Field Disjointness, the witness Gram block factors as the Schur complement of the dimension-carrier-graph Laplacian with observable vertices grounded. The leverage prediction matches observed values exactly on 240 non-trivial compositions.

Empirically 240/240 under DFD. Lean formalization of the Kron-reduction theorem deferred.

The pairwise fee admits an exact decomposition: fee(A, B) = U(A) + U(B) + B(A, B), where U(X) is a per-server invariant computable from X’s schema alone. On 703 compositions, 96.4% have B = 0.

703-composition real-schema corpus. 7 of 38 servers are unilateral carriers. Algorithmic consequence: O(N) precomputation replaces O(N²) full sweep.

Predicate invention under sheaf constraints decomposes into distinct topological, conservativity, and definability gates. The obstruction to gluing is borne by an H¹-class under the paper’s descent setup.

Finite-site / spine regime. Stated hypotheses still matter at the perimeter. Lean formalized in SCPI/Torsor.lean and SCPI/Conservativity.lean.

Schema discovery admits the stronger functorial and universality surface sketched in the paper and Lean statements.

Depends on SchemaDiscovery.lean closure and stronger categorical proof burden.

Bilateral validity can coexist with cycle failure in real compositions. The obstruction dimension predicts the minimum typed bridge burden required for repair.

Strongest in the A05 minimality witness and nearby cases. Two live non-isomorphic β₁=2 families with selective repair.

Among functionally matched candidates that all pass local validation, fee-aware qualification reduces downstream procurement regret under externally anchored holdout cases, without using post-reveal outcomes as input to selection.

Finance consequence artifact: six holdout cases across four consequence types. Fee-aware rule reduces regret from 57.23 to 33.96, outperforming local baseline and naive checklist rival. Still synthetic in construction.

Spanning-tree BFS diagnostic for H¹ vanishing, formalized in Lean 4. The corrected theorem requires a spanning hypothesis (every edge’s endpoints are tree-connected). The pre-correction statement was falsified by an explicit counterexample.

About SpanningTreeDecomp (sub-class with h_span hypothesis), not TreeDecomp in general. Closed against Lean v4.28.0 + Mathlib.

For a connected graph satisfying nV − 1 ≤ nE, the condition nE − (nV − 1) = 0 iff nE + 1 = nV. The v1 statement was correctly negated by the proof assistant with an explicit counterexample; the corrected statement adds the spanning hypothesis.

Three theorems formalizing the cohomological gap identity for Bulla compositions: fee_h1_additive (unconditional), fee_eq_h1_difference (under column compression), and range_obs_le_range_full (supporting lemma). All closed with no sorry and standard axioms only.

The regime-independent rank identity rank K(G) = fee(G) and the trace-of-idempotent = rank theorem (foundation of leverage conservation), both formalized and closed.

Five frontier LLMs (GPT-4o, Claude Sonnet 4, Opus 4, Codex 5.2, Gemini 3.1 Pro) achieve negative R² and near-zero Spearman ρ on composition-failure ranking under standard and guided-CoT prompting.

5 models, 3 providers, N=18–50 per model. 932 instances, 7 families, 3 provenance tiers.

Pre-computed restriction matrices with explicit arithmetic instructions at N=50 across all 5 models. Claude achieves ρ = 0.80, GPT-4o ρ = 0.39, while R² remains deeply negative for all.

At repair budget K=1, structural prescriptions achieve 11–29% improvement vs. 8–26% for alternatives. At K=3, structural leads on every family. Methods converge only at K=8.

932 instances, deterministic symbolic executor.

For every depth bound d, there exist arbitrarily large compositions that are locally d-valid yet globally incoherent. The separation is spectral: above a critical composition size, the connection Laplacian’s spectral gap closes and bounded probes become indistinguishable from null.

Theorem A (graph separation), Theorem B (abstract version). Empirical spectral experiment on 500 graphs across 7 scales confirms the spectral indistinguishability finding.

Whether a hidden field is a blind spot depends on the composition partner, not the field alone. Constructive proof: the same file_reader tool has fee=1 (blind spot on path) when composed with data_loader, but fee=0 (no blind spot) when composed with event_logger. Bulla computes this exactly from schemas.

Theorems 1–2 with constructive proof on 8-composition synthetic ecology. Ground truth independently validated: 1.000 precision, 0.985 recall on 20-composition stratified sample (573 predictions, 0 false positives, 9 missed homonym collisions).

Frontier LLMs recover the non-local hiddenness predicate with 88% accuracy under structured relational prompts but collapse to 46% under flat representations, reverting to lexical heuristics with timestamp as the dominant false positive. Two independent factors gate the effect: relational framing (+33pp) and convention-specific task language (+33pp). Server names and tool descriptions contribute negligibly (−8pp).

Synthetic ecology: 8 compositions × 3 conditions × 3 repeats (Claude Sonnet 4). Context ablation: 4 conditions × 12 filesystem compositions. April 2026.

On the same synthetic ecology benchmark, Claude Sonnet 4 achieves higher precision (55% vs 17%) but loses recall under flat prompts (50%), while GPT-4o maintains 100% recall but produces 3× more false positives. Different training distributions produce different precision/robustness tradeoffs on the same non-local predicate. Neither model achieves exact computation.

Synthetic ecology cross-model replication: 8 compositions × 3 conditions × 3 repeats per model. April 2026.

The settled core (coherence fee, matroid backbone, SCPI gates) extends to heterogeneous agent agreement via enriched and distributed claims. Enriched Laplacian-cohomology bridge and quantale-enriched H¹ are real frontier targets.

Edge-local mechanistic interpretability (SAE, probing, CKA, attention) cannot detect cyclic compositional failures that require global topological information. Structural diagnostic achieves ρ=1.0 in every condition; best interpretability baseline never exceeds ρ=0.758. Cross-model replication on GPT-2 Small and Gemma 2 2B.

240+ compositions, two open-weight models (GPT-2 Small, Gemma 2 2B). April 2026.