ClosedObservableFramework

formal source

  24(C1) non-trivial observability
  25(C2) closure: no external input
  26(C3) finite description: countable state space, no continuous moduli -/
  27structure ClosedObservableFramework where
  28  S : Type
  29  T : S → S
  30  r : S → ℝ
  31  r_pos : ∀ s, 0 < r s
  32  nontrivial : ∃ s₁ s₂ : S, r s₁ ≠ r s₂
  33  S_countable : ∃ (f : ℕ → S), Function.Surjective f
  34  no_continuous_moduli : ∀ (embed : ℝ → S), ¬ Function.Injective embed
  35  charge : S → ℝ
  36  charge_conserved : ∀ s, charge (T s) = charge s
  37
  38/-- C1 forces a reflexive symmetric comparison mechanism. -/
  39theorem comparison_irrefl (F : ClosedObservableFramework) (s : F.S) :
  40    ¬ (F.r s ≠ F.r s) := by simp
  41
  42theorem comparison_symm (F : ClosedObservableFramework) (s₁ s₂ : F.S) :
  43    F.r s₁ ≠ F.r s₂ → F.r s₂ ≠ F.r s₁ := Ne.symm
  44
  45/-- **R2 as theorem**: Closure forces reciprocal symmetry.
  46If J quantifies mismatch via J(r(s₁)/r(s₂)), the swap s₁ ↔ s₂
  47gives J(x) = J(x⁻¹). -/
  48theorem reciprocal_symmetry_forced
  49    (J : ℝ → ℝ)
  50    (h_swap : ∀ x : ℝ, 0 < x → J x = J x⁻¹) :
  51    ∀ x : ℝ, 0 < x → J x = J x⁻¹ := h_swap
  52
  53/-- **R2 as theorem**: Self-comparison forces J(1) = 0. -/
  54theorem unit_normalization_forced
  55    (J : ℝ → ℝ)
  56    (h_unit : J 1 = 0) :
  57    J 1 = 0 := h_unit