Foundation Recognition Operator Recognition Update Eq Shift On Quarter Turn Core

The quarter-turn update

The recognition update is the rule by which a recognition event advances the state of a system: it shifts the signal one step and then projects onto the sector the observer keeps. In the framework's 8-tick cycle, the update is a linear map on an 8-dimensional complex signal space, written recognitionUpdate S f = sectorProject S (cyclic_shift f). The declaration recognitionUpdate_eq_shift_on_quarterTurnCore is a definitional shorthand: it states that, on the quarter-turn core, applying the recognition update is the same as applying the shift alone. The quarter-turn core is the subspace spanned by the odd Fourier modes, modes 1, 3, 5, and 7, and the theorem sectorProject_eq_id_on_quarterTurnCore proves that the projection is the identity there, so the equality holds by definition.

The content that matters is the theorem behind the definition. On the quarter-turn core, four successive shifts multiply the signal by -1, so eight shifts return it to itself: shift_four_eq_neg_on_quarterTurnCore proves cyclicShiftIter 4 f = -f for f in the core. This is the quarter-turn structure: the update cycles through four states before negating, and through eight before repeating. The recognition update inherits this behavior on the core, because the projection does not disturb the signal there. The framework's library, a machine-checked collection of formal theorems, records this as a proved fact about the linear algebra of the 8-tick cycle.

What the declaration does not claim is just as important. It does not assert that the recognition update is a quarter-turn on all signals; on the full 8-dimensional space, the projection generally discards even modes, so the update is not a pure rotation. It does not claim that the quarter-turn core is the only subspace with this property, nor that the update is physically realized as a rotation in spacetime. The equality is a statement about the algebraic structure of the signal space, not about geometry or dynamics. The recognition-to-linking bridge, which would connect this algebraic cycle to physical three-dimensional space, remains open.

/-- The concrete recognition update is projector-after-shift. -/
def recognitionUpdate (S : StructuredSector) : Signal8 →ₗ[ℂ] Signal8 :=
  (sectorProject S).comp shiftLinear

/-- Every structured-sector projector fixes the quarter-turn core pointwise. -/
theorem sectorProject_eq_id_on_quarterTurnCore (S : StructuredSector) :
    ∀ {f : Signal8}, f ∈ quarterTurnCore → sectorProject S f = f := by
  intro f hf
  refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
  · intro m hm
    rcases hm with ⟨k, hkodd, rfl⟩
    have hk : k ∈ S.keepModes := S.odd_modes_included hkodd
    simpa [sectorProject_mode, hk] using sectorProject_mode S k
  · exact map_zero (sectorProject S)
  · intro x y hx hy hpx hpy
    calc
      sectorProject S (x + y) = sectorProject S x + sectorProject S y := by
        exact map_add (sectorProject S) x y
      _ = x + y := by rw [hpx, hpy]
  · intro a x hx hpx
    calc
      sectorProject S (a • x) = a • sectorProject S x := by
        exact map_smul (sectorProject S) a x
      _ = a • x := by rw [hpx]

/-- Four shifts act as `-I` on the quarter-turn core. This is the concrete
`P^4 = -I` statement used in the paper. -/
theorem shift_four_eq_neg_on_quarterTurnCore {f : Signal8} (hf : f ∈ quarterTurnCore) :
    cyclicShiftIter 4 f = -f := by
  refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
  · intro m hm
    rcases hm with ⟨k, hkodd, rfl⟩
    rw [cyclicShiftIter_mode, odd_mode_fourth_eigenvalue k hkodd]
    ext t
    simp
  · ext t
    simp [cyclicShiftIter, cyclic_shift]
  · intro x y hx hy hpx hpy
    calc
      cyclicShiftIter 4 (x + y) = cyclicShiftIter 4 x + cyclicShiftIter 4 y := cyclicShiftIter_add 4 x y
      _ = -x + -y := by rw [hpx, hpy]
      _ = (-1 : ℂ) • x + (-1 : ℂ) • y := by simp
      _ = (-1 : ℂ) • (x + y) := by rw [smul_add]
      _ = -(x + y) := by
            ext t
            simp [smul_eq_mul]
  · intro a x hx hpx
    calc
      cyclicShiftIter 4 (a • x) = a • cyclicShiftIter 4 x := cyclicShiftIter_smul 4 a x
      _ = a • (-x) := by rw [hpx]
      _ = -(a • x) := by simp

What this page does not claim

The recognition update is a quarter-turn on all signals in the 8-dimensional space. The quarter-turn core is the only subspace with this property. The algebraic quarter-turn structure is physically realized as a spatial rotation.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/RecognitionOperator.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: