IndisputableMonolith.RRF.Theorems.OctaveTransfer

   1import IndisputableMonolith.RRF.Core.Octave
   2
   3/-!
   4# RRF Theorems: Octave Transfer
   5
   6Theorems about how properties transfer between octaves.
   7
   8Key insight: If two octaves are "equivalent" (have isometric strain functions),
   9then their equilibrium structures are the same. This is how "the same pattern"
  10manifests at different scales.
  11
  12## Main Results
  13
  14- `equilibria_transfer`: Equivalent octaves have corresponding equilibria
  15- `morphism_preserves_order`: Octave morphisms preserve strain ordering
  16-/
  17
  18
  19namespace IndisputableMonolith
  20namespace RRF.Theorems
  21
  22open RRF.Core
  23
  24/-! ## Morphism Properties -/
  25
  26variable {O₁ O₂ : Octave}
  27
  28/-- Octave morphisms are monotone with respect to strain ordering. -/
  29theorem morphism_preserves_order (f : OctaveMorphism O₁ O₂)
  30    {x y : O₁.State} (hxy : O₁.strain.weaklyBetter x y) :
  31    O₂.strain.weaklyBetter (f.map x) (f.map y) :=
  32  f.preserves_order x y hxy
  33
  34/-- Composition of morphisms preserves ordering. -/
  35theorem comp_preserves_order {O₃ : Octave}
  36    (g : OctaveMorphism O₂ O₃) (f : OctaveMorphism O₁ O₂)
  37    {x y : O₁.State} (hxy : O₁.strain.weaklyBetter x y) :
  38    O₃.strain.weaklyBetter ((OctaveMorphism.comp g f).map x)
  39                            ((OctaveMorphism.comp g f).map y) :=
  40  (OctaveMorphism.comp g f).preserves_order x y hxy
  41
  42/-! ## Equivalence Properties -/
  43
  44/-- Octave equivalences preserve equilibria exactly. -/
  45theorem equiv_equilibria_iff (e : OctaveEquiv O₁ O₂)
  46    (x : O₁.State) :
  47    O₁.strain.isBalanced x ↔ O₂.strain.isBalanced (e.toFun.map x) := by
  48  simp only [StrainFunctional.isBalanced]
  49  rw [e.strain_eq x]
  50
  51/-- Octave equivalences preserve well-posedness. -/
  52theorem equiv_wellPosed (e : OctaveEquiv O₁ O₂) :
  53    O₁.wellPosed ↔ O₂.wellPosed := by
  54  constructor
  55  · intro ⟨x, hx⟩
  56    use e.toFun.map x
  57    rw [← equiv_equilibria_iff e x]
  58    exact hx
  59  · intro ⟨y, hy⟩
  60    use e.invFun.map y
  61    -- Use the inverse strain preservation directly
  62    simp only [StrainFunctional.isBalanced] at *
  63    rw [e.strain_eq_inv y]
  64    exact hy
  65
  66/-! ## Transfer Lemmas for Channels -/
  67
  68/-- If two octaves have equivalent channels, their quality orderings agree. -/
  69theorem channel_quality_transfer
  70    {i₁ : O₁.channels.Index} {i₂ : O₂.channels.Index}
  71    (f : OctaveMorphism O₁ O₂)
  72    (hchan : ∀ x : O₁.State,
  73      (O₂.channels.channel i₂).stateQuality (f.map x) =
  74      (O₁.channels.channel i₁).stateQuality x) :
  75    ∀ x y : O₁.State,
  76      (O₁.channels.channel i₁).stateQuality x ≤
  77      (O₁.channels.channel i₁).stateQuality y →
  78      (O₂.channels.channel i₂).stateQuality (f.map x) ≤
  79      (O₂.channels.channel i₂).stateQuality (f.map y) := by
  80  intro x y hxy
  81  rw [hchan x, hchan y]
  82  exact hxy
  83
  84/-! ## The "Same Pattern, Different Scale" Principle -/
  85
  86/-- Two octaves manifest the same pattern if they're equivalent. -/
  87def samePattern (O₁ O₂ : Octave) : Prop :=
  88  Nonempty (OctaveEquiv O₁ O₂)
  89
  90theorem samePattern_refl (O : Octave) : samePattern O O :=
  91  ⟨OctaveEquiv.refl O⟩
  92
  93theorem samePattern_symm {O₁ O₂ : Octave} (h : samePattern O₁ O₂) :
  94    samePattern O₂ O₁ :=
  95  let ⟨e⟩ := h
  96  ⟨OctaveEquiv.symm e⟩
  97
  98end RRF.Theorems
  99end IndisputableMonolith
 100