historyCarrier_equiv_plainCarrier
plain-language theorem explainer
For every bound B, the canonical history carrier is type-equivalent to the plain path-sum bounded complex. Gap2 auditors cite this when checking that the history enrichment adds no new carrier structure. The proof is a one-line term packaging the construction's own underlying equivalence.
Claim. For every natural number $B$, the type of canonical history carriers at bound $B$ is equivalent to the type of plain path-sum bounded complexes at bound $B$: the equivalence class is nonempty.
background
Gap2 tracks whether a gauge-counting measure on orbit mass can be derived from ledger substrate rather than postulated. Wave C1 R6 briefly flipped related status flags to true by binding them to a history-based discharge; both flags were later retracted. The module records that the witness theorem remains true, but reading it as a derivation from new history structure is wrong.
The history construction packages a carrier CanonicalHistory B meant to look like an enriched counting object. The plain side is PathSumMeasure.BoundedComplex B, the ordinary bounded complex used by the path-sum measure. The module's defect thesis is that history is presentation sugar: inert under enrichment parameters, equal as a measure to the pre-existing orbit mass, and carrier-equivalent to the plain complex.
Upstream, the gauge-orbit mass already satisfies the counting principle via MeasureSubstrateBlocker.gaugeOrbitMass_satisfies, which predates the history module. The open obligation remains: derive the gauge-counting principle from substrate strictly richer than counting.
proof idea
One-line term proof. It packages CanonicalHistory.equivUnderlying into a Nonempty witness of a type equivalence CanonicalHistory B ≃ PathSumMeasure.BoundedComplex B. No further tactics, no new algebraic work: the construction already ships the equivalence between its history carrier and the plain bounded complex, and this theorem re-exports that fact at the status-binding layer.
why it matters
This is one leg of the 2026-07-26 defect certificate for Gap2 measure-status binding. Together with parameter-inertness of the history measure and the identity that the history measure equals the old orbit mass, it shows the history story is a true presentation theorem about an object already defined, not a derivation of gauge counting from ledger substrate.
Downstream it is used at the Gap2 posting-layer floor (Gap2PostingLayerFloor.mass), where relabeling invariance plus the counting principle forces Gibbs weights and leaves no free enrichment that could derive the principle. In the Recognition gravity stack this closes a false-positive status path without withdrawing the underlying orbit-mass theorem, and keeps the real open problem in view: obtain GaugeCountingPrinciple from structure richer than counting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.