recognitionUpdate_eq_shift_on_quarterTurnCore
plain-language theorem explainer
On the quarter-turn core (span of odd DFT modes of an 8-tick signal), the projector-after-shift recognition update equals the bare cyclic shift, for every structured sector. Anyone citing the analytic operator core or the T7/T8-to-operator bridge needs this identity. The proof unfolds the update and applies the sector projector identity after noting the shift preserves the core.
Claim. Let $S$ be a structured sector (odd modes kept, DC excluded) and let $f$ be an 8-tick complex signal in the quarter-turn core (the $\mathbb{C}$-span of the odd DFT modes). Then the recognition update of $f$ under $S$ equals the bare cyclic shift: $\mathrm{Update}_S(f)=Tf$, where $(Tf)(k)=f(k+1\bmod 8)$. The equality is independent of which non-DC modes $S$ keeps beyond the odds.
background
The ambient space is Signal8: complex-valued functions on the eight-tick circle. The cyclic shift $T$ advances the reading index by one tick, $(Tf)(k)=f(k+1\bmod 8)$; it is the discrete time-evolution generator of the eight-tick octave (T7). The quarter-turn core is the $\mathbb{C}$-span of the odd DFT modes ${1,3,5,7}$.
A structured sector extends that core by a finite set of kept modes that must include every odd index and exclude the DC mode $k=0$. The recognition update is the projector-followed-by-shift rule associated to such a sector: shift first, then project onto the sector's kept modes.
The module builds the analytic Recognition Operator on this 8-tick signal space (importing ComplexStructureForcing). Upstream, sectorProject_eq_id_on_quarterTurnCore already says the sector projector acts as the identity on the core, and the shift maps the core into itself.
proof idea
Term-mode after a single unfold. Unfold recognitionUpdate to expose the projector-after-shift composite. The goal becomes: the sector projector applied to $Tf$ equals $Tf$. Invoke shift_mem_quarterTurnCore on the hypothesis $f\in$ quarter-turn core to place $Tf$ in the core, then apply sectorProject_eq_id_on_quarterTurnCore for the given sector. No case splits and no sector-dependent algebra remain.
why it matters
This is the quarter-turn commit step of the analytic operator core. Downstream, operator_core_holds packages it as quarter_turn_commit, and the one-line wrapper RecognitionOperator.evolve_eq_shift_on_quarterTurnCore lifts it to the bundled operator record (evolve collapses to bare shift on the core). That package is what t7_t8_to_operator_bridge_holds consumes: once T7 (eight-tick octave) and T8 ($D=3$) are forced, the bridge supplies the operator core.
In framework terms it says the recognition dynamics on the odd-mode core is unitary and sector-independent: pure eight-tick shift, matching the T7 period $2^3$. Without this identity the projector-after-shift rule would retain sector dependence on the core and the forcing chain could not close the operator bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.