postingPhase_mk
plain-language theorem explainer
Reading the adjoined Fin-8 posting phase from a posting-enriched exact path class recovers the phase used to build it. Gap-2 cocycle and gravity workers cite this when unpacking the product carrier that bridges transaction-state phase to exact path classes. The equality is pure definitional reflexivity on the structure field.
Claim. For every $n \in \mathbb{N}$, every exact path class $c$ of complexity $n$, and every tick $p \in \mathrm{Fin}\,8$, the posting-phase projection of the enriched pair $\langle c, p \rangle$ equals $p$.
background
The module supplies the carrier half of the Gap-2 posting-cocycle program. The RS eight-tick recognition-posting cocycle already exists as a period-8 transaction on PairKernel state, while certified Fin-8 phase close wants a tick on exact path classes. Those live on different carriers: transaction state versus incidence-only complexes.
ExactPathClass n is the exact complexity shell: combinatorially distinct exact complexes of complexity exactly $n$, written as a dependent sum over shell signatures of the quotient of the exact labeled class by global equivalence. It carries edge and tetrahedron incidence, not a posting phase.
Rather than invent an incidence hash or fake section, the module adjoins an external $\mathrm{Fin},8$ posting coordinate, forming a product enrichment. The projection named here simply reads that second field; the forgetful map erases it. Module policy prefers this STOP A residual bank over a spurious descent.
proof idea
One-line rfl. By definition the posting-phase reader returns the structure field, and the enriched constructor packages $\langle c, p \rangle$ with that field equal to $p$, so the equality holds definitionally with no lemmas or rewriting.
why it matters
Anchors the projection half of the product enrichment for D-qg-gap2-posting-cocycle-20260723. It pairs with the forgetful constructor identity and feeds the closed STOP A residual that forgetful descent erases the posting coordinate, plus the companion fact that the coordinate itself does not factor through forget. The Fin-8 phase is the eight-tick octave (forcing chain T7) sitting on the exact shell rather than on PairKernel transaction state.
Downstream graph is empty for this lemma; siblings on the same carrier carry the load. The open residual remains the non-forgetful GE-invariant antipodal bridge needed for certified close. Explicitly does not flip continuum-and-measure Gap-2 status, and refuses fake incidence-derived cocycles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.