equivUnderlying
plain-language theorem explainer
Equivalence between counted histories at bound B (posted complexes with dual-entry state pinned to balanced zero) and ordinary labeled bounded complexes. Anyone proving that pinned history counts equal complex counts, or that the history carrier is the plain carrier, cites this. The maps are the forgetful underlying projection and ofComplex; left inverse uses structure ext plus the canonical-history identity, right inverse is definitional.
Claim. For each bound $B\in\mathbb{N}$, the type of counted histories (posted bounded histories whose dual-entry ledger state equals the balanced zero state) is equivalent to the type of labeled bounded complexes of bound $B$. The forward map forgets the pinned state and retains the complex; the inverse rebuilds the unique counted history over a complex.
background
Module Wave C1 R5 builds the gap-2 gauge-counting measure from a posted-history presentation. A posted bounded history is a labeled bounded complex whose incidence labels live in a posting alphabet tied to a dual-entry ledger state. History relabeling is the gauge redundancy; the class measure is $\nu(c)=(#$ histories presenting $c)/($history gauge volume of $c)$.
Counted histories deliberately carry the dual-entry state but pin it by a Prop field to the canonical balanced zero (debit = credit = 0, mag = 0). That pin keeps dual-entry present without letting free state fields inflate the count. The structure therefore packages a posted history together with the equality of its state to balanced zero.
The equivalence identifies that pinned carrier with the plain labeled complex type used elsewhere in the path-sum / orbit-mass stack. Upstream cost and cosmology identifiers in the dependency graph are ambient imports; the local content is the history-to-complex forgetful map and its inverse.
proof idea
Definitional equivalence, not a heavy tactic proof. Forward map is the underlying projection from a counted history to its bounded complex. Inverse is ofComplex, which rebuilds the unique counted history over a complex.
Left inverse: after CanonicalHistory.ext it remains to check that the history field recovers. That reduces to canonicalHistory of the underlying complex equaling the original posted history, which is the symmetric of the sibling identity toPosted_eq_canonicalHistory (state-canonicality fiber collapses). Right inverse is rfl: ofComplex then underlying is definitionally the identity on complexes.
why it matters
This is the bridge that makes pinned history counting equal complex counting. Downstream, canonical_count_eq_complex_count is exactly Nat.card_congr of this equivalence: after the design pin, dual-entry enrichment contributes no factor. The defect certificate historyCarrier_equiv_plainCarrier re-exports Nonempty of the same equivalence so the author's claim matches the construction.
Inside the module it supplies Finite for counted histories (via Finite.of_equiv of the inverse), and history_class_equiv_mk routes class-fibered counted histories to class-fibered complexes through the same underlying/ofComplex pair. That keeps $\nu$ defined as a pure history-count quotient (see the history-only definitional certificate) while still matching banked orbit/pair counts under GaugeCountingPrinciple, without defining $\nu$ to be gaugeOrbitMass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.