PostingTransactionForcedExactTick
plain-language theorem explainer
A Prop asserting that a class-level Fin-8 tick map is forced by posting phases on continuum histories: every history phase equals the tick of its forgotten exact path class. Gap2 continuum work cites it as the provenance hypothesis linking history-level phases to class ticks. Pure definitional Prop; the body is that quantified equality.
Claim. Given continuum posting-history data $P$ and a class-level tick map $\tau$ assigning to each exact path class an element of $\mathrm{Fin}\,8$, the forced-tick condition holds when, for every shell $n$ and every history $h$ at that shell, the phase of $h$ equals $\tau$ applied to the exact path class obtained by forgetting $h$.
background
This module banks an equal-strength continuum package on actual posting histories after the Gap2 cocycle-carrier stop, not a forgetful product enrichment. The carrier structure supplies, per shell $n$, a finite type of histories, a forgetful map to exact path classes, a Fin-8 phase on each history, a history mass, and two substantive Prop slots (generation by an actual period-8 posting transaction, and history gauge invariance).
The eight-tick octave is the fundamental RS evolution period (T7): phases live in $\mathrm{Fin},8$, matching the discrete tick lattice with $\tau_0=1$. The class-level tick map $\tau$ is the object one wants to recover from history phases once histories forget to path classes. The doc-comment states the provenance reading: the class-level tick is forced by the posting phase on histories that forget to that class.
proof idea
Definitional Prop, not a proved theorem. The body is a single universal quantifier: for all shells $n$ and all histories $h$ in the carrier at $n$, equality of the history phase with $\tau$ on the forgotten path class. No lemmas are applied; inhabiting the Prop later is attachment work for a downstream session.
why it matters
Names the provenance hypothesis that the character bridge and the pushforward obligation both need. Downstream, the exact-character bridge structure packages a class-level tick together with fiberwise character pushforward and a decoy-escape clause; the named obligation states that forced tick plus mass pushforward imply the bridge's character-pushforward field, and is banked uninhabited so later sessions can discharge it without widening the API.
In the Gap2 residual stack this is the clean interface between history-level Fin-8 phases and class-level ticks on the eight-tick octave, without flipping the continuum-and-measure gate or gluing an unconstrained product. It does not close the typed residuals for attachment or continuum close; those remain OPEN.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.