Blueprint: the axiom audit #
Every main theorem of the development carries a pinned
#print axioms line: an axiom set drifting from the whitelist
[propext, Classical.choice, Quot.sound] is a compile error, not a
reading exercise.
How to read it. The sections group the categorical, Schur and
coordinate inputs to the forward theorem. The factorial mainline is
audited in BlueprintFactorial.lean.
Each pin names one theorem; the section it sits in says what that
theorem contributes. The converse is audited in
BlueprintConverse.lean, the symmetric-group input in
BlueprintSchur.lean, and the statement surface — every definition
the summits are phrased in — in BlueprintStatement.lean.
Hook vanishing and the power sums #
A tower whose hook-confined characters vanish has vanishing super power sums, which is what makes the trace zeta rational.
Hook confinement and nilpotent traces #
Exponentially bounded growth confines the surviving Young diagrams to a hook, nilpotents then have vanishing trace, and the trace criterion makes every endomorphism algebra semisimple.
The classical bases #
The symplectic and orthonormal standard bases the super model is written in.
Definition 5 and its transport #
The mixed partition value of an edge subset, and its invariance under a fragment equivalence.
The hypothesis class #
The edge-rank hypothesis bounds the dimension of a row span; the literature bounds the ranks of the finite submatrices of the connection matrix. The two are the same condition.
The gluing calculus #
Gluing a list of label pairs: permuting the list, appending, normalising an interface, and the existence of transition data.
Coordinates and the standard model #
Contraction families, the standard form and copairing, and the coordinates a nondegenerate pairing gives.
Gluing across a disjoint union #
The glue list distributes over a disjoint union and commutes with swaps and folds — the associativity engine of the category.
The exact pairing #
The self-duality of the standard model, and that it is braided.
The trace calculus #
Closing a fragment against the strand bundle: relabels cross it, tensors absorb, and permutation fragments compose.
The braided envelope #
The Karoubi and matrix envelopes inherit the braiding and its symmetry.
The skein category #
Linear, monoidal and rigid structure on the skein category, and the trace map it carries.
The coordinate model #
The fibre functor's image of a star, the standard model it is identified with, and the transport between them.
The master colour sum #
The parameter as a sum over colourings: the star coordinates, the diagonal cap pairing, every sign family, and the reindexing that turns the sum into Definition 5.
Deligne's hypotheses for the envelope #
Each hypothesis of the cited theorem, discharged for the concrete envelope, and the package they assemble into.