Foundation Coupled Recognition Cores Local Weyl Monomial Phase Orthogonal

A clean separation of phases

A ququart is a quantum system with four distinguishable states, the natural extension of a qubit's two. In the Recognition Science framework, each local recognition core is modeled as a ququart carrying a discrete phase. The declaration in question proves a clean separation: two operators that differ only in their phase factor, applied to the same shift, have zero overlap. In plain terms, if you take the same state and give it two different phase rotations, the resulting states are perfectly distinguishable, with no interference between them.

The proof is a theorem in the framework's machine-checked library of formal theorems, anchored in the file CoupledRecognitionCores.lean. It states that for any shift a and any two distinct phase labels b and b', the inner product of the two corresponding Weyl monomial operators is zero. The inner product here is the standard quantum mechanical measure of overlap: zero means the operators act on completely orthogonal directions in the state space. The result holds for all four possible shifts and all pairs of distinct phases, so it is not a special case but a general property of the local model.

This orthogonality is what makes the phase label a reliable carrier of information. In the coupled-core picture, where many ququarts are linked, the same property extends to the tensor product space: the framework's library also proves that the full coupled space has dimension 4^N for N cores, and that the local operators embed into it. The phase-orthogonality theorem is the local guarantee that no information is lost when the phase is used to encode a degree of freedom.

What the declaration does not claim is equally important. It does not say that the phase and shift operators commute in the ordinary sense; in fact, the library proves the opposite, that they satisfy the Weyl relation with a factor of the imaginary unit i. It does not claim that the phase label has any physical meaning beyond the mathematical model, nor that this orthogonality survives when the cores are coupled with interactions that break the local structure. It is a theorem about the local algebra, not about the full dynamics of the universe.

The consequence for the framework is that the local phase is a clean, independent degree of freedom, one that can be measured without ambiguity. For the general reader, the takeaway is simpler: in this model, a phase is not a decoration but a distinguishable feature, and the mathematics guarantees that distinction.

/-- Equal shifts but distinct phase labels are orthogonal in the one-core Weyl family. -/
theorem localWeylMonomial_phase_orthogonal (a : Fin 4) {b b' : Fin 4} (h : b ≠ b') :
    localOperatorInner (localWeylMonomial a b) (localWeylMonomial a b') = 0 := by
  unfold localOperatorInner
  have hs : ∀ s : Fin 4,
      ∑ t : Fin 4,
        star ((localWeylMonomial a b (basisKet s)) t) *
          (localWeylMonomial a b' (basisKet s)) t =
        (-Complex.I) ^ (b.val * (add4 a s).val) *
          Complex.I ^ (b'.val * (add4 a s).val) := by
    intro s
    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] using hinner
  rw [Fin.sum_univ_four]
  rw [hs 0, hs 1, hs 2, hs 3]
  fin_cases a <;> fin_cases b <;> fin_cases b' <;>
    simp at h <;>
    simp [add4, neg_I_pow, Complex.I_pow_eq_pow_mod] <;>
    ring_nf <;> simp [I_pow_five]
set_option maxHeartbeats 200000

/-- The local quarter-turn core is modeled as a ququart carrier. -/
abbrev QuquartState := Fin 4 → ℂ

/-- Pointwise Weyl relation `ZX ψ = i XZ ψ`. -/
lemma ququartWeyl_relation_apply (ψ : QuquartState) :
    ququartZ (ququartX ψ) = (Complex.I : ℂ) • ququartX (ququartZ ψ) := by
  ext m
  fin_cases m
  · simp [ququartZ, ququartX, prev4]
    symm
    have hI : Complex.I * Complex.I = (-1 : ℂ) := by
      have h := Complex.I_sq; rw [sq] at h; exact h
    calc
      -(Complex.I * (Complex.I * ψ 3)) = -((Complex.I * Complex.I) * ψ 3) := by ring
      _ = -((-1) * ψ 3) := by rw [hI]
      _ = ψ 3 := by ring
  · simp [ququartZ, ququartX, prev4]
  · simp [ququartZ, ququartX, prev4]
    have hI : Complex.I * Complex.I = (-1 : ℂ) := by
      have h := Complex.I_sq; rw [sq] at h; exact h
    calc
      -ψ 1 = (-1 : ℂ) * ψ 1 := by ring
      _ = (Complex.I * Complex.I) * ψ 1 := by rw [hI]
      _ = Complex.I * (Complex.I * ψ 1) := by ring
  · simp [ququartZ, ququartX, prev4, Complex.I_sq]

/-- The dimension of the coupled-core index space is exactly `4^N`. -/
theorem coupledCoreIndex_card (N : ℕ) :
    Fintype.card (CoupledCoreIndex N) = 4 ^ N := by
  simp [CoupledCoreIndex]

What this page does not claim

The phase and shift operators commute in the ordinary sense; the library proves the opposite Weyl relation. The phase label has a physical meaning beyond the mathematical model. The orthogonality survives when the cores are coupled with interactions that break the local structure.

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: