Foundation Recognition Operator Two Beat Square Eq Neg On Quarter Turn Core

The quarter-turn core

The declaration twoBeat_square_eq_neg_on_quarterTurnCore concerns an eight-component signal, a list of eight complex numbers that the framework uses as its basic unit of information. Among all such signals, the quarter-turn core is the subspace spanned by the four odd-indexed Fourier modes, the components that oscillate fastest. The theorem states that applying a cyclic shift, moving each component one position forward and wrapping the last to the front, four times in succession to any signal in this core produces the negative of the original signal. In symbols, for every f in the core, cyclicShiftIter 4 f = -f.

The result is a consequence of the underlying structure of the discrete Fourier transform. A cyclic shift multiplies each Fourier mode by a power of the eighth root of unity, omega8. For the odd modes, shifting four times multiplies by (omega8^4)^k, which equals (-1)^k. Since k is odd, this is -1, so each odd mode is negated. The proof is a direct computation in the framework's machine-checked library of formal theorems, meaning it is verified by a computer program that checks every step against the rules of logic.

The theorem is a structural fact about the recognition operator, the map that the framework uses to update a signal in one step of its eight-tick cycle. The recognition operator first shifts the signal and then projects it onto a chosen sector. Because the sector projection leaves the quarter-turn core unchanged, the four-step negation property carries over to the full recognition operator. This means that after four ticks of the cycle, any signal confined to the core is inverted, a symmetry that the framework's later results about eight-tick cycles and three-dimensional space rely upon.

In Recognition Science, this fact is part of the chain that forces the number of spatial dimensions. The framework models the recognition process as a discrete ledger, a record of events that updates in ticks. The eight-tick cycle, with this quarter-turn symmetry, is what the framework's proofs use to derive the number 2^3, and from that the three dimensions of space. The theorem itself does not mention space or dimensions; it is a lemma about linear algebra on an eight-dimensional complex vector space.

What the theorem does not claim is any physical statement about actual space or time. It does not assert that physical signals are eight-component complex numbers, nor that the universe literally performs cyclic shifts. The framework's identification of this mathematical structure with physical reality is a separate modeling choice, not a proved theorem. The declaration only establishes a fact about a particular mathematical object, the quarter-turn core, within the framework's formal system.

/-- 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

/-- The quarter-turn core is the span of the odd DFT modes. -/
def quarterTurnCore : Submodule ℂ Signal8 :=
  Submodule.span ℂ {m | ∃ k : Fin 8, Odd k.val ∧ m = dft8_mode k}

/-- 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]

What this page does not claim

The theorem makes no claim about physical space or time. The theorem does not assert that physical signals are eight-component complex numbers. The theorem does not establish that the recognition operator is the only operator satisfying the four-step negation property.

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: