ofComplex
plain-language theorem explainer
From a labeled bounded complex one builds the unique counted history that presents it, with dual-entry ledger state pinned to balanced zero. Gauge-counting and history-class bijections cite this as the canonical section of the underlying-complex forgetful map. The body is a structure constructor: wrap via the canonical posted history and discharge state canonicity by reflexivity.
Claim. Given a labeled bounded complex $K$ of size bound $B$, form the counted history whose posted carrier is the canonical presentation of $K$ (complex $K$ with dual-entry state equal to the balanced zero state on the posting alphabet of $K$). The canonicity proposition holds by construction.
background
Module Wave C1 R5 builds a gauge-counting measure from posted-history presentations of labeled complexes. A posted bounded history pairs a labeled complex with a dual-entry ledger state whose incidence labels live in a posting alphabet. History relabeling is the gauge redundancy; the class measure is history count over history gauge volume.
A counted history (CanonicalHistory) keeps the full posted carrier but requires, as a proposition field, that the dual-entry state equal the balanced zero state (debit = credit = 0, mag = 0). Dual-entry is present and pinned, not erased, so arbitrary state fields cannot inflate the count.
Upstream, canonicalHistory K is the posted history with complex $K$ and that balanced zero state. The present constructor lifts that posted object into the counted type by packaging the canonicity proof.
proof idea
One-line structure constructor. Set the posted carrier field to canonicalHistory K, which already installs $K$ and the balanced zero state. The remaining field state_canonical is the equality of that state with balanced zero; it holds definitionally, so rfl closes it.
why it matters
This is the canonical section of the forgetful map from counted histories to labeled complexes. Downstream, equivUnderlying uses it as invFun, proving counted histories are equivalent to labeled complexes once the state-canonicity fiber collapses. fiber_unique takes ofComplex K as the unique default in that fiber. Class-level counting routes through history_class_equiv_mk, whose inverse again applies ofComplex. Simp lemmas (classOf_ofComplex, toPosted_ofComplex, underlying_ofComplex) make the section transparent in later gauge-volume identities.
In the Seven Gaps gravity stack this underwrites gap-2 residual R5: the history-side measure $\nu(c)$ that is later shown equal to gaugeOrbitMass only via the counting-principle bridge, never by definitional identification. No T0–T8 forcing step is proved here; the declaration is infrastructure for the gauge-counting side of the residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.