toPosted_ofComplex
plain-language theorem explainer
For any bounded complex, the posted carrier of its unique counted history equals the canonical history presentation (zero dual-entry state, own incidence as postings). Authors of the gap-2 gauge-counting measure cite this when collapsing counted-history projections back to the canonical presentation. The equality is pure definitional reduction (rfl).
Claim. For every bounded complex $K$ on the bichromatic interface $B$, the posted history extracted from the unique counted history of $K$ equals the canonical history of $K$: the same complex with balanced zero dual-entry state ($\mathrm{debit}=\mathrm{credit}=\mathrm{mag}=0$) and $K$'s own incidence as the posting presentation.
background
Module Wave C1 R5 builds the gauge-counting measure from a posted-history presentation. A posted bounded history is a labeled bounded complex whose incidence indices are posting-alphabet elements of 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)$, proved to satisfy the gauge-counting principle by explicit bijections, never by defining $\nu$ to be orbit mass.
The dual-entry columns anchor the substrate reading but are pinned to the canonical balanced zero state so that arbitrary state fields cannot inflate history counts. The canonical history of a labeled complex $K$ is exactly that package: $K$ itself plus the balanced zero state. The unique counted history of $K$ is the structure whose posted carrier is that canonical history (with a Prop witness that the state is canonical). The posted-carrier projection simply returns that underlying posted history.
proof idea
One-line definitional equality. By construction the unique counted history of $K$ stores the canonical history of $K$ as its posted carrier field, and the posted-carrier projection is the abbreviation that reads that field. Unfolding both sides yields identical terms, so rfl closes the goal. Marked @[simp] for downstream reduction.
why it matters
Sits in the gap-2 residual R5 stack (gauge-counting measure from posted-history presentation). It is the simp bridge that lets proofs treat the posted projection of a counted history as the canonical presentation without unfolding structure fields by hand. That keeps the counting layer honest: histories carry dual-entry state but pin it to balanced zero, so the count is driven by posting/relabel degrees of freedom rather than free state fields. No downstream consumers are wired yet in the graph; the lemma is infrastructure for the $\nu$-build and the paired non-circularity rfl audits (nuBuild history-only certificates) described in the module design. It does not itself touch T0–T8 forcing, RCL, or the mass ladder; its role is local to the gravity seven-gaps gauge measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.