underlying_ofComplex
plain-language theorem explainer
Round-trip identity: building a canonical history from a bounded complex and reading off its underlying complex recovers the original complex. Anyone simplifying posted-history constructions in the gap-2 gauge-counting measure will cite it. The proof is pure definitional equality (`rfl`).
Claim. For every bounded complex $K$ on the fixed base $B$, if $H$ is the canonical history constructed from $K$, then the underlying bounded complex of $H$ equals $K$.
background
This module builds the Wave C1 R5 gauge-counting measure from a posted-history presentation. A posted bounded history is a labeled bounded complex whose incidence indices live in a posting alphabet tied to a dual-entry ledger state; history relabeling is the posting-level gauge redundancy. The class measure is $\nu(c)=(#$ histories presenting $c)/($history gauge volume of $c)$, proved to satisfy the gauge-counting principle by explicit bijections, never by defining $\nu$ to be orbit mass.
CanonicalHistory packages a bounded complex together with the posting data needed for that count. The constructor that lifts a plain bounded complex $K$ into that package, and the projection that forgets posting data back to the underlying complex, are definitional inverses on the complex component. The base $B$ is the ambient complex parameter of the section; dual-entry state is pinned to the balanced zero state so that counted histories do not inflate by free ledger fields.
proof idea
One-line definitional proof: rfl. By construction, the canonical-history lift stores $K$ as its underlying field, so projecting that field is judgmentally equal to $K$. Marked @[simp] so the round-trip fires in simplification.
why it matters
Sits in the gap-2 residual R5 stack (gauge-counting measure from posted histories). The identity keeps the history presentation honest: every bounded complex embeds into the canonical-history carrier without changing the geometric substrate that the measure counts. Downstream gauge-volume and $\nu$-build arguments rely on being able to move between bare complexes and posted histories without residue on the complex side. No used_by edges are recorded yet; the lemma is infrastructure for the history-relabeling and measure sections that follow in the same module. It does not itself touch T0–T8 or the RCL; it is pure carrier hygiene for the gravity seven-gaps gauge count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.