gap2PostingCocycleCarrierStatus_flags
plain-language theorem explainer
Boolean status receipt for the Gap-2 posting-cocycle carrier bank: product enrichment and forgetful map are banked, phase-forgetting and non-descent are proved, the STOP-A residual is closed, the bridge residual is defined but open, and neither certified close nor continuum-and-measure is claimed. Gravity auditors of the seven-gap ledger cite it as the frozen flag snapshot. Proof is a single decidable evaluation of the status record.
Claim. The Gap-2 posting-cocycle carrier status record satisfies: enriched product carrier banked $=\mathsf{true}$; forgetful map banked $=\mathsf{true}$; carrier-forgets-phase proved $=\mathsf{true}$; posting phase does not descend $=\mathsf{true}$; carrier-forgets-phase residual closed $=\mathsf{true}$; bridge residual defined-and-open $=\mathsf{true}$; certified close inhabited $=\mathsf{false}$; Gap-2 continuum-and-measure claimed $=\mathsf{false}$.
background
Recognition Science already has an eight-tick recognition-posting cocycle as a period-8 transaction (the T7 octave). Certified Fin-8 phase close wants a tick living on exact path classes. Those sit on different carriers: PairKernel phase is transaction state, while exact complexes and path classes carry only incidence data (edge and tetrahedron vertices).
This module banks the carrier half of that mismatch. It adjoins an external Fin-8 posting phase via product enrichment, supplies forgetful maps that erase the phase coordinate, and proves that the carrier forgets phase while the phase itself does not descend through the forgetful map. A typed residual for that forgetfulness is closed (STOP A receipt). A separate bridge residual for a non-forgetful GE-invariant antipodal link remains open.
The status structure is a concrete boolean ledger of those landings. The upstream definition hard-codes the eight flags; this theorem reifies them as a single conjunction.
proof idea
One-line decidable proof. The tactic decide evaluates each boolean field equality against the concrete status record (enriched product and forgetful map banked; phase-forgetting and non-descent proved; forget residual closed; bridge residual open; certified close and continuum-and-measure both false). No lemmas are invoked beyond decidable equality on Bool.
why it matters
Fills the carrier half of design note D-qg-gap2-posting-cocycle-20260723 inside the Gravity seven-gap ledger. It freezes an honest STOP-A bank: forgetful descent erases the posting coordinate, and the coordinate does not factor through the forgetful map, so one must not invent an incidence hash, mod-2 parity, or product section and call it the posting cocycle.
The closed residual is the carrier-forgets-phase receipt. The still-open bridge residual is the non-forgetful GE-invariant antipodal bridge required before certified Fin-8 phase close can be inhabited. The flags explicitly refuse to flip continuum-and-measure and refuse to claim certified close. Framework landmark: T7 eight-tick octave as the period-8 posting transaction that the enrichment is trying to carry onto exact path classes. No downstream dependents are wired yet; the theorem is the audit snapshot for the bank.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.