IndependentRecognizers

formal source

  90
  91/-- Two recognizers are **independent** if each provides information the other doesn't.
  92    This means: ∃ configs distinguished by r₁ but not r₂, and vice versa. -/
  93def IndependentRecognizers {E₁ E₂ : Type*} [EventSpace E₁] [EventSpace E₂]
  94    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) : Prop :=
  95  (∃ c₁ c₂, r₁.R c₁ ≠ r₁.R c₂ ∧ r₂.R c₁ = r₂.R c₂) ∧
  96  (∃ c₁ c₂, r₁.R c₁ = r₁.R c₂ ∧ r₂.R c₁ ≠ r₂.R c₂)
  97
  98/-- If recognizers are independent, their composite strictly refines both. -/
  99theorem independent_strict_refines {E₁ E₂ : Type*} [EventSpace E₁] [EventSpace E₂]
 100    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
 101    (h : IndependentRecognizers r₁ r₂) :
 102    ¬IsSeparating r₁ ∧ ¬IsSeparating r₂ →
 103      (∃ c₁ c₂, r₁.R c₁ = r₁.R c₂ ∧ (r₁ ⊗ r₂).R c₁ ≠ (r₁ ⊗ r₂).R c₂) := by
 104  intro ⟨_, _⟩
 105  obtain ⟨⟨_, _, _, _⟩, ⟨c₃, c₄, heq, hne⟩⟩ := h
 106  use c₃, c₄, heq
 107  simp only [composite_R_eq]
 108  intro hcontra
 109  rw [Prod.mk.injEq] at hcontra
 110  exact hne hcontra.2
 111
 112/-! ## Physical Interpretation: Spacetime Dimension -/
 113
 114/-- **WHY SPACETIME IS 4-DIMENSIONAL**
 115
 116    In Recognition Geometry, dimension = minimum separating family size.
 117
 118    Spacetime is 4D because exactly 4 independent recognizers are needed:
 119
 120    • x-recognizer: distinguishes left from right
 121    • y-recognizer: distinguishes front from back
 122    • z-recognizer: distinguishes up from down
 123    • t-recognizer: distinguishes before from after