Foundation Coupled Recognition Cores Tensor Weyl Monomial Shift Orthogonal

Orthogonality of shifted cores

In quantum mechanics, two states or operators are orthogonal when they have zero overlap, meaning they are perfectly distinguishable in principle. The declaration tensorWeylMonomial_shift_orthogonal proves an analogous fact for a specific family of operators built from the framework's recognition cores. Each core is modeled as a four-level system, a ququart, whose basis states are labeled by the integers 0, 1, 2, 3 with arithmetic taken modulo 4. The operators in question are Weyl monomials, which combine a shift that adds a fixed amount to the label and a phase that multiplies by a power of the imaginary unit i. The theorem states that if two such monomials have different shift amounts, their inner product is exactly zero, regardless of the phase parts. This is the standard orthogonality property that makes the Weyl operators a useful basis for describing operations on a quantum system.

The proof is carried out in the framework's machine-checked library of formal theorems, where every step is verified by a computer. It builds on more basic lemmas: the basis states are orthonormal, shifting by a then subtracting a returns the original state, and the phase factors cancel when the shifts differ. The theorem is stated for a single ququart, but the same argument extends to a system of N coupled cores, where each core has its own label and the shift is applied independently to each. In that setting, the operators act on a space of dimension 4^N, and the orthogonality result still holds for operators with different shift patterns.

In Recognition Science, this result matters because it gives a clean way to separate different recognition operations. The framework models recognition events as discrete records, and the cores are the basic units that carry these records. The orthogonality theorem ensures that shifting a core by one amount produces an operation that is completely distinct from shifting it by another amount, with no leakage between them. This is a structural guarantee, not an empirical one: it follows from the definitions of the shift, the phase, and the inner product, and it is checked by the computer.

The theorem does not claim that these operators are physically realized in any particular experiment, nor does it assign any numerical value to a physical constant. It is a purely mathematical statement about the operators defined in the library. It also does not say anything about the dynamics of recognition, such as how these operators evolve over time or interact with each other. Those questions remain open targets for future work.

/-- Distinct shift labels force Hilbert-Schmidt orthogonality. -/
theorem localWeylMonomial_shift_orthogonal {a a' : Fin 4} (h : a ≠ a') (b b' : Fin 4) :
    localOperatorInner (localWeylMonomial a b) (localWeylMonomial a' b') = 0 := by
  unfold localOperatorInner
  apply Finset.sum_eq_zero
  intro s hs
  rw [localWeylMonomial_basisKet, localWeylMonomial_basisKet]
  have hidx : add4 a s ≠ add4 a' s := by
    intro hEq
    exact h ((add4_eq_add4_iff_left a a' s).mp hEq)
  have hinner :=
    scaled_basisKet_inner
      (Complex.I ^ (b.val * (add4 a s).val))
      (Complex.I ^ (b'.val * (add4 a' s).val))
      (add4 a s) (add4 a' s)
  simpa [localWeylMonomial_basisKet, hidx] using hinner

set_option maxHeartbeats 800000

/-- Adding after shifting the same displacement returns the original configuration. -/
theorem addedConfig_shiftedConfig {N : ℕ} (a s : CoupledCoreIndex N) :
    addedConfig a (shiftedConfig a s) = s := by
  funext x
  exact add4_sub4_cancel_core (s x) (a x)

/-- The standard ququart basis is orthonormal for the explicit finite sum. -/
theorem basisKet_orthonormal (m n : Fin 4) :
    ∑ t : Fin 4, star (basisKet m t) * basisKet n t = if m = n then 1 else 0 := by
  fin_cases m <;> fin_cases n <;> simp [basisKet]

What this page does not claim

This theorem does not claim that the operators correspond to any physical measurement or experiment. It does not assign numerical values to any physical constants. It does not describe how recognition cores evolve or interact over time.

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/CoupledRecognitionCores.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: