If (U∘F)∘K and U∘(F∘K) are equal, the chain is an ordinary category and rung 30 is unnecessary. If they are merely isomorphic, the isomorphism is data, the data must satisfy laws, and everything from chapter 4 onward follows. This chapter asks which, and the answer is not known.
Strict equality of composites is the exception in mathematics, not the rule. It holds for functions between sets. It fails, in the usual sense, for tensor products, for spans, for bimodules, for pasting of cobordisms — anywhere the composite is constructed rather than merely applied. The corpus's operators are constructed: K is described as a gate that fires, F as a fold, U as an unfolding. Constructions of that kind associate up to canonical isomorphism far more often than on the nose.
Once chapter 2 has fixed the category, this is decidable by inspection rather than by argument. Write both bracketings. Ask whether they are the same morphism, or whether there is a comparison morphism between them and it happens to be invertible.
Strict. Volume XIII shrinks to a short chapter recording that the chain is an ordinary monoid of endofunctors, and Part II skips rung 30. That is a good outcome and should be published as one.
Weak. There is an associator, and the corpus has been writing an unbracketed four-fold composite for three years without the data that makes it well-defined. That is a defect of the same class as the others in the record, and the remainder of this volume is its repair.
Run from the geometry repository against its built Mathlib, the file elaborates with zero errors and admits nothing. The decisive line is this one:
rfl closes it. Functor composition does not merely satisfy an associativity
lemma — it associates by computation. The two bracketings are the same term to the
kernel. The same holds one level down for plain endofunctions, where all four bracketings are
identified by rfl as well. MODEL
At levels 0 and 1 the chain requires no coherence data whatsoever. If the
four operators are functions on a type — which is what AXLE currently has, with
PhaseVector := Fin 12 → ℝ and applyG — or endofunctors of a category,
then rung 30 buys the series nothing and this volume is one section long.
Weakness appears only at level 2. Mathlib's bicategory associator has
type (f ≫ g) ≫ h ≅ f ≫ g ≫ h — an isomorphism, never an equation — and the file
proves it invertible in both directions without asserting the two sides equal. So the entire
volume now rests on Chapter 2: are the operators
level-2 objects, or not? Chapter 3 has handed its weight to chapter 2 and has nothing further
to decide.
Nine declarations, no sorryAx. The file admits nothing — and the report contains a
second finding, which belongs to
Chapter 7: the two theorems carrying the whole
content of level 2 report exactly what the deliberately vacuous control reports.
DATA
Verdict delivered: strict at levels 0 and 1, weak at
level 2, with the comparison morphism exhibited as α_ and proved
invertible. AXLE/Vol13_Coherence.lean, green under Lean 4.32.0 against the Mathlib
built in the geometry repository, 2026-08-29. Nine axiom probes, no sorryAx.