parities_flip_under_tick_reversal
plain-language theorem explainer
Every one of the nine independent ℤ₂ ledger parities flips under the combined conjugation and tick-reversal map. Anyone assembling the nine-parity master theorem, vacuum-page constraints, or the 2⁹ configuration count cites this. The argument is pure ℤ/2ℤ arithmetic: adding 1 is never the identity on a bit.
Claim. For every parity vector $v$ (a map from the nine parity indices into $\mathbb{Z}/2\mathbb{Z}$) and every parity index $p$, the conjugated tick-reversed value satisfies $v(p)+1 \neq v(p)$ in $\mathbb{Z}/2\mathbb{Z}$.
background
The NineParities module records the independent ℤ₂ symmetries of the double-entry recognition ledger under conjugation and tick reversal. The nine indices split as four spacetime parities (charge-parity, $B-L$, hypercharge, tick), three color Cartan sign flips, and two generation-mixing signs; their exact count is the content of Tesla's "magnificence of the 9" in the RS reading.
A parity vector assigns a bit in $\mathbb{Z}/2\mathbb{Z}$ to each index. The conjugated tick-reversal operation is defined pointwise by $v \mapsto (p \mapsto v(p)+1)$. The fundamental tick $\tau_0=1$ is the RS time quantum; one octave is eight ticks, but only the algebraic flip under the combined map is needed here.
Upstream, the operation is introduced precisely so that "ALL nine parities flip (0 ↔ 1)." This lemma discharges that claim for an arbitrary vector and index.
proof idea
Unfold the conjugated tick-reversal definition to replace the left-hand side by $v(p)+1$. Assume equality $v(p)+1 = v(p)$ for contradiction. Subtract $v(p)$ on both sides in $\mathbb{Z}/2\mathbb{Z}$ to obtain $1=0$, which is false. The whole argument is a short tactic script driven by simp on the definition and on the ring of characteristic 2; no external lemmas beyond the definition of the operation are required.
why it matters
This is clause (2) of the module's key theorems and the second conjunct of nine_parities_master, the master statement that the ledger carries exactly nine independent ℤ₂ parities which all flip under conjugation plus tick reversal, all vanish on the scalar vacuum page, decompose as 4+3+2, span $\mathbb{Z}_2^9$, and yield a $2^9=512$-state configuration space.
In the broader Recognition framework the flip law is the discrete symmetry that pairs admissible ledger pages with their conjugates; without it the vacuum-page vanishing theorem and the independence count would not close. It sits downstream of the forcing chain's eight-tick octave (T7) only insofar as tick reversal is the time-orientation piece of that octave; the proof itself is purely algebraic over $\mathbb{Z}/2\mathbb{Z}$ and does not invoke J-cost uniqueness or dimension forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.