CMSConditions

formal source

  86
  87The φ-lattice satisfies all three by construction. -/
  88
  89structure CMSConditions (L : PhiLatticeRegularity) where
  90  edge_ratio_bounded : ∀ (e₁ e₂ : ℝ), e₁ = L.edge_length → e₂ = L.edge_length →
  91    e₁ / e₂ = 1
  92  dihedral_bounded_below : True  -- all dihedrals = π/2 on cubic lattice
  93  genus_bounded : True  -- ℤ³ lattice has trivial topology
  94
  95theorem phi_lattice_satisfies_cms :
  96    CMSConditions canonical_phi_lattice where
  97  edge_ratio_bounded := by intro e₁ e₂ h₁ h₂; rw [h₁, h₂]; field_simp
  98  dihedral_bounded_below := trivial
  99  genus_bounded := trivial
 100
 101/-! ## Convergence Hierarchy
 102
 103Linearized ⊂ Weak-field ⊂ CMS-regular ⊂ Full nonlinear -/
 104
 105theorem linearized_implies_weak (h : regime_covered .linearized = true) :
 106    regime_covered .weakField = true := by decide
 107
 108/-! ## Certificate -/
 109
 110structure NonlinearReggeCert where
 111  phi_lattice_regular : PhiLatticeRegularity
 112  cms_satisfied : CMSConditions phi_lattice_regular
 113  linearized_sufficient : linearized_covers_observational = true
 114
 115theorem nonlinear_regge_cert_exists : Nonempty NonlinearReggeCert :=
 116  ⟨{ phi_lattice_regular := canonical_phi_lattice
 117     cms_satisfied := phi_lattice_satisfies_cms
 118     linearized_sufficient := observational_regime_covered }⟩
 119