The statement surface, pinned #
Reading a formalization means reading what its theorems say, and that reduces to the handful of definitions their statements are phrased in. This module lists exactly those definitions and pins each one's type, and then pins the type of every theorem of record.
For the development's own definitions this is a signature audit.
Each anonymous example turns a change to a pinned type into a compile
error, so nothing enters or leaves a summit statement unnoticed; but
a type is not a meaning, and a definition can be rewritten while
keeping it — EdgeRankBounded would still read
(ClosedFragment → ℂ) → ℕ → Prop whatever it bounded. Reading the
summits therefore means reading the linked definitions, which is
what the file lists them for. For the one definition where a
convention could silently be wrong — mixedPartition, which carries
the circuit sign, the Eulerian condition and the odd-colour
bookkeeping — the last section pins a value instead of a type.
Deligne's theorem is pinned by content, as is every predicate its
hypothesis list is phrased in. The corollary definitions are likewise
pinned by content so the meaning of rank, minimum and prescribed
dimensions is visible. Blueprint.lean and its parts then pin what
the summits depend on.
The main definitions live in RS/Definitions.lean, the
self-contained statement surface that the comparator certification
trusts. RS/DimensionDefinitions.lean adds the growth, minimum and
prescribed-dimension surface and imports only that main surface.
The model #
A fragment is a flag (half-edge) graph over a label type; a closed
fragment is one with no boundary labels, and Fragment.Equiv is
isomorphism of fragments.
Mixed partition functions #
MixedFunctional k ℓ is a vertex functional with k even and 2ℓ
odd colours, mixedPartition is Definition 5 of Regts–Sevenster on
the flag model, and the two predicates say that a parameter is such
a partition function, with and without a bound on the dimensions.
The total bound is pinned by content: its witness bounds the sum of both dimensions and evaluates to the original parameter.
Edge-connection rank #
EdgeRankBounded f R says the connection pairings of f have rank
at most R ^ t at every arity t; EdgeRankParameter R packages a
normalized, isomorphism-invariant parameter with that bound.
The statements and Deligne's theorem #
Deligne's theorem, unfolded #
A type is not a meaning, so DeligneTheoremStatement is pinned by
content as well as by name: its hypothesis list, and the definition
of every predicate that list is phrased in. An auditor compares
what follows with Deligne's Théorème 0.6 and §0.1; a change to any
of it is a compile error. The statement is proved in
RS/Classical/Deligne/, so the pin fixes the meaning of a theorem
of this tree rather than of an assumption.
The theorems of record #
The converse carries no hypothesis; the forward direction and the characterization carry Deligne's theorem and nothing else.
The definition, evaluated #
A pinned type says nothing about a convention, and mixedPartition
is where the conventions are: the circuit sign, the Eulerian
condition, a loop's two incidences at its vertex, the difference
between a loop and a free circle, and the η-convention through
which distinct odd colourings reach a common basis vector.
The accompanying paper's worked example fixes all five at once.
Against the functional charPolyFunctional θ, whose mixed partition
function is the characteristic polynomial det(θ I − A_G) on graphs
without free circles, the one-vertex one-loop graph has A_L = (2)
and so must evaluate to θ − 2. It does
(RS/Novel/Skein/LoopExample.lean); a sign error in any one of the
five would change the number. Adjoining a free circle sends the
same functional to 0, since k − 2ℓ = 0 here — the same graph,
worth θ − 2 with a loop and 0 with a circle.