recognitionUpdate_apply
plain-language theorem explainer
On any structured sector, the recognition update of an 8-tick signal equals the sector Fourier projector applied after one cyclic tick shift. Cite this when unfolding the analytic RecognitionOperator step into projector-after-shift form. The equality is definitional: the update is literally that composition, so the proof is reflexivity.
Claim. For every structured sector $S$ (a keep-set of Fourier modes on the eight-tick circle that includes all odd modes and excludes DC) and every signal $f:\mathbb{Z}/8\mathbb{Z}\to\mathbb{C}$, the recognition update of $S$ at $f$ equals the sector projector of $S$ applied to the one-tick cyclic shift of $f$.
background
This module builds the analytic RecognitionOperator on eight-tick complex signals. Signal8 is the forced 8-sample complex signal space coming from ComplexStructureForcing (the T7 eight-tick octave). A StructuredSector is a keep-set of Fourier modes that always includes the odd modes ${1,3,5,7}$ and never the DC mode $0$; it extends the quarter-turn core by optional non-DC modes.
The sector projector reconstructs a signal from only the kept DFT coefficients. The recognition update is defined as that projector composed with the linear one-tick cyclic shift: projector-after-shift. The shift itself is the standard cyclic tick advance on the eight-sample circle (the local one-tick recognition step).
The surrounding file also exposes a legacy ledger compatibility surface (LedgerState, RecognitionCost, etc.) so older bridge modules can call the same analytic operator without reintroducing the old ledger-native definition.
proof idea
One-line definitional proof. By definition, recognitionUpdate S is the linear map (sectorProject S) ∘ shiftLinear. Applying both sides to $f$ and identifying the underlying cyclic shift with cyclic_shift yields exact equality, discharged by rfl. The @[simp] attribute makes this the preferred unfolding rule in later tactic proofs.
why it matters
This is the computational face of the concrete recognition step on the forced eight-tick circle (T7). Downstream, RecognitionOperator.evolve is defined as exactly this update on the operator's sector, and the legacy compatibility theorems (conserves, minimizes_J, phase_coupling) read evolution through that bundling. Without the simp form, every later argument would have to manually expand the composition of projector and shift.
In the Recognition Science chain the update is the discrete dynamics that keeps only the structured modes after each tick advance, so the operator stays inside the admissible sector while the eight-tick octave runs. No parent theorem currently lists this lemma as a dependency in the graph, but it is the unfolding hinge for the entire analytic operator API in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.