classOf_ofComplex
plain-language theorem explainer
The triangulation class of the unique counted history built from a labeled bounded complex K is exactly K's own class under history relabeling. Gauge-counting arguments that move between labeled complexes and CanonicalHistory cite this as a simp bridge. The proof is pure definitional equality (rfl).
Claim. For any bounded complex $K$ on base $B$, if $H$ is the unique counted (state-canonical) history presenting $K$, then the triangulation class of $H$ equals the quotient class of $K$ under the history-relabeling setoid on labeled complexes.
background
Module Wave C1 R5 builds a gauge-counting measure from a posted-history presentation of bounded complexes. A counted history is a labeled bounded complex whose incidence labels come from a dual-entry ledger posting alphabet, with the dual-entry state pinned to the balanced zero state so that only posting/relabel degrees of freedom drive the count.
History relabeling (posting-alphabet gauge) is the equivalence that defines triangulation classes: the class of a history is the quotient of its underlying labeled complex by that setoid. The constructor that turns a labeled complex $K$ into a counted history packages the canonical history of $K$ and records state-canonicity by reflexivity.
The class map on counted histories is then the quotient map applied to the underlying complex. This lemma records that those two constructions compose to the plain quotient class of $K$.
proof idea
One-line definitional proof (rfl). Unfolding the counted-history constructor and the class map yields Quotient.mk of the underlying complex of the canonical history of $K$, which is definitionally $K$. No lemmas are applied.
why it matters
In the gap-2 residual design, the class measure is $\nu(c)=(#$ histories presenting $c)/($history gauge volume of $c)$, proved to satisfy the gauge-counting principle by explicit bijections, and identified with orbit mass only through the iff bridge (never by defining $\nu$ as that mass).
This simp fact keeps class computations on canonically presented histories aligned with the quotient of the labeled complex itself, so later counting identities can rewrite without manual unfolding. No downstream theorems are wired yet in the graph; the lemma is infrastructure for the history-only definitional layer of $\nu$ and the paired non-circularity audits.
It sits in the gravity seven-gaps stack (posted histories, path-sum measure substrate), not in the T0–T8 forcing chain, but supports the discrete gauge-volume bookkeeping those gravity residuals need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.