Foundation Recognition Operator

The recognition operator

A recognition operator is a rule that takes a signal, shifts it, and filters it. In the Recognition Science framework, reality maintains a ledger, a discrete record of events, and each event is an eight-part signal. The operator is the step that advances the ledger: it shifts the signal by one position, then projects it onto a chosen subspace, retaining only the modes the sector allows. This is the engine of an eight-step cycle, and the module that defines it is the foundation on which the framework's later theorems rest.

The operator works on a specific object: Signal8, an eight-dimensional complex vector space. A signal in this space is a list of eight complex numbers, and the operator's first move is a cyclic shift, moving each entry one position forward and wrapping the last entry to the front. The second move is a projection, a linear map that zeros out every frequency mode not marked as kept by the sector. The composition of these two moves, shift then project, is the recognition update. A sector is simply a choice of which modes to keep, and the operator is defined by that choice.

The framework proves two structural facts about this operator. First, the shift preserves the quarter-turn core, the subspace spanned by the four odd-indexed frequency modes, so a signal built from those modes stays in that subspace after shifting. Second, applying the shift four times to any signal in that core negates it: four shifts equal multiplication by minus one. This is the formal seed of the eight-tick cycle, since eight shifts return the signal to itself, and it is what makes the operator a periodic engine rather than a one-shot filter.

In Recognition Science, the operator is the canonical replacement for an older ledger-based API. The current definition carries a compatibility surface: several legacy fields, such as time, bond identifiers, and cost, are defined as constant zero or empty readouts, because the new operator does not use them. This allows older bridge modules to build without reintroducing the retired ledger implementation. The spectral content, the shift and projection, is unchanged; the compatibility layer only prevents stale files from breaking the main foundation imports.

The practical consequence is that the framework's later claims, the golden ratio, the eight-tick cycle, and the forcing of three dimensions, all rest on this operator as their base step. A reader who understands that the operator is a shift followed by a filter, and that four shifts negate the quarter-turn core, has the machinery needed to follow the forcing chain. The operator is not a metaphor; it is a concrete linear map with proved properties, and it is the first rung of the ladder the framework climbs.

@[simp] lemma recognitionUpdate_apply (S : StructuredSector) (f : Signal8) :
    recognitionUpdate S f = sectorProject S (cyclic_shift f) := rfl

/-- 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 odd-mode span is invariant under one-tick propagation. -/
theorem shift_mem_quarterTurnCore {f : Signal8} (hf : f ∈ quarterTurnCore) :
    cyclic_shift f ∈ quarterTurnCore := by
  change shiftLinear f ∈ quarterTurnCore
  refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
  · intro m hm
    rcases hm with ⟨k, hkodd, rfl⟩
    rw [shiftLinear_apply, dft8_shift_eigenvector]
    exact Submodule.smul_mem quarterTurnCore _ (Submodule.subset_span ⟨k, hkodd, rfl⟩)
  · change shiftLinear (0 : Signal8) ∈ quarterTurnCore
    rw [map_zero]
    exact quarterTurnCore.zero_mem
  · intro x y hx hy hpx hpy
    change shiftLinear (x + y) ∈ quarterTurnCore
    rw [map_add]
    exact quarterTurnCore.add_mem hpx hpy
  · intro a x hx hpx
    change shiftLinear (a • x) ∈ quarterTurnCore
    rw [map_smul]
    exact quarterTurnCore.smul_mem a hpx

abbrev LedgerState := Signal8

What this page does not claim

This answer does not claim the operator is a physical measurement device. This answer does not claim the operator derives the fine-structure constant. This answer does not claim the compatibility surface changes the operator's spectral content.

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: