IndisputableMonolith.Gravity.SevenGaps.EdgeTensorSector

   1import IndisputableMonolith.Gravity.TensorShearSector
   2
   3/-!
   4# Seven-Gaps Lane 3: the edge (tensor) sector beyond the conformal ansatz
   5
   6The vertex-conformal ansatz assigns one scalar per vertex and induces the
   7log-strain `(ξ u + ξ v) / 2` on the edge `{u, v}`
   8(`TensorShearSector.conformalEdgeLogStrain`).  This file measures, on the
   9actual `5 × 5 × 5` periodic Freudenthal 3-torus, how small that conformal
  10slice is inside the full edge-perturbation space, and exhibits the shear
  11complement concretely with an explicit localized witness.
  12
  13## Honest status header
  14
  15* THEOREM (everything below is fully proved: zero `sorry`, zero `admit`, no
  16  new axioms, no hypothesis taken as a silent assumption; no theorem in this
  17  file carries an undischarged hypothesis parameter):
  18  - Linearity: `conformalStrainLinearMap` packages the conformal ansatz as an
  19    `ℝ`-linear map `VertexPotential K →ₗ[ℝ] EdgePerturbation K` agreeing
  20    pointwise with `conformalEdgeLogStrain`
  21    (`conformalStrainLinearMap_apply`); membership in its range is exactly
  22    `IsConformalEdgePerturbation`
  23    (`isConformalEdgePerturbation_iff_mem_range`).
  24  - Rank bound on any finite 3D Regge triangulation:
  25    `conformalRange_finrank_le_nV` (conformal image has finrank at most
  26    `K.nV`), via `finrank_vertexPotential`, `finrank_edgePerturbation`, and
  27    Mathlib's `LinearMap.finrank_range_le`.
  28  - Concrete counts on the `N = 5` torus, computed from the definitions and
  29    not assumed: `periodicTorus5_nV_eq : PeriodicTorus5.K.nV = 125` and
  30    `periodicTorus5_nE_eq : PeriodicTorus5.K.nE = 875`.  Hence the dimension
  31    gap `periodicTorus5_conformalRange_finrank_lt_finrank_edgeSpace`
  32    (conformal rank ≤ 125 < 875 = edge-space dimension), the proper-subspace
  33    facts `periodicTorus5_conformalRange_ne_top` and
  34    `periodicTorus5_exists_not_mem_conformalRange`, and the existence of a
  35    non-conformal edge perturbation `periodicTorus5_exists_nonconformal`.
  36  - Explicit shear witness: `rectangleShearFace5` puts strain `+1` on the two
  37    x-edges and `-1` on the two y-edges of the unit coordinate square of the
  38    torus with corners `(0,0,0), (1,0,0), (1,1,0), (0,1,0)`.  It is not
  39    vertex-conformal, in typed and in encoded edge coordinates
  40    (`rectangleShearFace5_not_conformal_typed`,
  41    `rectangleShearFace5Encoded_not_conformal`).  A second witness, the
  42    uniform x-strain `xUniformStrain5`, is proved non-conformal by direct
  43    reuse of the repo's rectangle obstruction
  44    `nontrivial_rectangle_shear_not_vertexConformal` with `h = 1 ≠ 0 = v`
  45    (`xUniformStrain5_not_conformal_typed`,
  46    `xUniformStrain5Encoded_not_conformal`).
  47  - Orthogonal complement made concrete: `rectangleShearFace5` is orthogonal
  48    to the entire conformal slice with respect to
  49    `periodicEdgeInnerProduct5` (`rectangleShearFace5_inner_conformal_eq_zero`)
  50    and has self inner product `4`
  51    (`rectangleShearFace5_inner_self_eq_four`), so it is a nonzero vector of
  52    the orthogonal complement of the conformal subspace
  53    (`rectangleShearFace5_nonzero_in_orthogonal_complement`).  The uniform
  54    x-strain pairs to `2` against it
  55    (`rectangleShearFace5_inner_xUniformStrain5`), so `xUniformStrain5` has a
  56    nonzero orthogonal projection onto that complement
  57    (`xUniformStrain5_nonzero_orthogonal_component`).
  58* MODEL: the endpoint-average log-strain convention and the unit-weight edge
  59  inner product `periodicEdgeInnerProduct5` are the modeling choices
  60  inherited from `TensorShearSector`; nothing here depends on a choice of
  61  edge lengths or weights.
  62* OPEN: the full conformal ⊕ longitudinal-gauge ⊕ TT orthogonal decomposition
  63  of the 875-dimensional edge space (the projector data of
  64  `TensorShearSector.PeriodicTTProjectorData5`) and the TT polarization count
  65  remain open.  This file proves the conformal slice is a proper subspace and
  66  exhibits a nonzero vector of its orthogonal complement; it does not build
  67  the full splitting.
  68
  69## `decide` usage
  70
  71`decide` is used only for finite `Fin`-literal facts, never for a
  72real-number statement: the four face-edge endpoint computations
  73(`faceEdgeAB_endpoints`, `faceEdgeDC_endpoints`, `faceEdgeBC_endpoints`,
  74`faceEdgeAD_endpoints`), pairwise distinctness of the four face edges (inside
  75the `rectangleShearFace5_apply_*` value lemmas), the displacement facts
  76inside `xUniformStrain5_apply_*`, and the three `Finset` non-membership facts
  77(`faceEdgeAB_not_mem_rest`, `faceEdgeDC_not_mem_rest`,
  78`faceEdgeBC_not_mem_rest`) used to expand the four-term inner-product sum.
  79The pre-existing `PeriodicTorus5` itself uses `by decide` for `2 < 5` at its
  80definition site in `TensorShearSector`.
  81-/
  82
  83namespace IndisputableMonolith
  84namespace Gravity
  85namespace SevenGaps
  86namespace EdgeTensorSector
  87
  88open Geometry.ReggeTriangulation3D
  89open Geometry.ReggeHessian3D
  90open Geometry.PeriodicFreudenthalTorus
  91open TensorShearSector
  92
  93set_option maxRecDepth 65536
  94
  95noncomputable section
  96
  97/-! ## 1. The conformal ansatz as a linear map -/
  98
  99/-- The vertex-conformal log-strain map, packaged as an `ℝ`-linear map from
 100vertex potentials to edge perturbations. -/
 101def conformalStrainLinearMap (K : Triangulation3D) :
 102    VertexPotential K →ₗ[ℝ] EdgePerturbation K where
 103  toFun ξ := conformalEdgeLogStrain K ξ
 104  map_add' ξ η := by
 105    funext e
 106    simp only [conformalEdgeLogStrain, Pi.add_apply]
 107    ring
 108  map_smul' a ξ := by
 109    funext e
 110    simp only [conformalEdgeLogStrain, Pi.smul_apply, smul_eq_mul,
 111      RingHom.id_apply]
 112    ring
 113
 114@[simp] theorem conformalStrainLinearMap_apply
 115    (K : Triangulation3D) (ξ : VertexPotential K) :
 116    conformalStrainLinearMap K ξ = conformalEdgeLogStrain K ξ := rfl
 117
 118/-- The conformal subspace predicate of `TensorShearSector` is exactly
 119membership in the range of the linear map. -/
 120theorem isConformalEdgePerturbation_iff_mem_range
 121    (K : Triangulation3D) (ε : EdgePerturbation K) :
 122    IsConformalEdgePerturbation K ε ↔
 123      ε ∈ LinearMap.range (conformalStrainLinearMap K) := by
 124  constructor
 125  · rintro ⟨ξ, hξ⟩
 126    exact LinearMap.mem_range.mpr ⟨ξ, hξ.symm⟩
 127  · intro hmem
 128    obtain ⟨ξ, hξ⟩ := LinearMap.mem_range.mp hmem
 129    exact ⟨ξ, hξ.symm⟩
 130
 131/-! ## 2. Rank bound on an arbitrary finite triangulation -/
 132
 133theorem finrank_vertexPotential (K : Triangulation3D) :
 134    Module.finrank ℝ (VertexPotential K) = K.nV := by
 135  show Module.finrank ℝ (Fin K.nV → ℝ) = K.nV
 136  simp [Module.finrank_fintype_fun_eq_card]
 137
 138theorem finrank_edgePerturbation (K : Triangulation3D) :
 139    Module.finrank ℝ (EdgePerturbation K) = K.nE := by
 140  show Module.finrank ℝ (Fin K.nE → ℝ) = K.nE
 141  simp [Module.finrank_fintype_fun_eq_card]
 142
 143/-- The conformal image inside the edge-perturbation space has dimension at
 144most the number of vertices. -/
 145theorem conformalRange_finrank_le_nV (K : Triangulation3D) :
 146    Module.finrank ℝ (LinearMap.range (conformalStrainLinearMap K)) ≤ K.nV := by
 147  have h := LinearMap.finrank_range_le (conformalStrainLinearMap K)
 148  exact h.trans (finrank_vertexPotential K).le
 149
 150/-! ## 3. Concrete counts and the dimension gap on the `N = 5` torus -/
 151
 152/-- The typed periodic edges are exactly base-vertex × displacement pairs. -/
 153def periodicEdge5EquivProd : PeriodicEdge5 ≃ PeriodicVertex5 × Fin 7 where
 154  toFun e := (e.base, e.disp)
 155  invFun p := ⟨p.1, p.2⟩
 156  left_inv _ := rfl
 157  right_inv _ := rfl
 158
 159/-- Computed from the definitions: the `5 × 5 × 5` torus has 125 vertices. -/
 160theorem periodicTorus5_nV_eq : PeriodicTorus5.K.nV = 125 := by
 161  show Fintype.card PeriodicVertex5 = 125
 162  simp [PeriodicVertex5, Vertex]
 163
 164/-- Computed from the definitions: the `5 × 5 × 5` torus has
 165`125 * 7 = 875` positive-displacement edges.  The proof routes through the
 166canonical edge equivalence `PeriodicTorus5.edgeEquiv`, avoiding any deep
 167unfolding of the encoded torus. -/
 168theorem periodicTorus5_nE_eq : PeriodicTorus5.K.nE = 875 := by
 169  have h : Fintype.card (Fin PeriodicTorus5.K.nE) = Fintype.card PeriodicEdge5 :=
 170    Fintype.card_congr PeriodicTorus5.edgeEquiv
 171  rw [Fintype.card_fin, Fintype.card_congr periodicEdge5EquivProd] at h
 172  simpa [PeriodicVertex5, Vertex] using h
 173
 174theorem finrank_encodedEdgePerturbation5 :
 175    Module.finrank ℝ EncodedEdgePerturbation5 = 875 := by
 176  have h : Module.finrank ℝ EncodedEdgePerturbation5 = PeriodicTorus5.K.nE :=
 177    finrank_edgePerturbation PeriodicTorus5.K
 178  exact h.trans periodicTorus5_nE_eq
 179
 180theorem periodicTorus5_conformalRange_finrank_le :
 181    Module.finrank ℝ
 182      (LinearMap.range (conformalStrainLinearMap PeriodicTorus5.K)) ≤ 125 := by
 183  have h := conformalRange_finrank_le_nV PeriodicTorus5.K
 184  exact h.trans periodicTorus5_nV_eq.le
 185
 186/-- Dimension gap: the conformal slice (rank ≤ 125) is strictly smaller than
 187the 875-dimensional edge-perturbation space of the `N = 5` torus. -/
 188theorem periodicTorus5_conformalRange_finrank_lt_finrank_edgeSpace :
 189    Module.finrank ℝ
 190        (LinearMap.range (conformalStrainLinearMap PeriodicTorus5.K)) <
 191      Module.finrank ℝ EncodedEdgePerturbation5 := by
 192  have h1 := periodicTorus5_conformalRange_finrank_le
 193  have h2 := finrank_encodedEdgePerturbation5
 194  omega
 195
 196/-- The conformal image is a proper subspace of the edge space. -/
 197theorem periodicTorus5_conformalRange_ne_top :
 198    LinearMap.range (conformalStrainLinearMap PeriodicTorus5.K) ≠ ⊤ := by
 199  intro htop
 200  have hlt := periodicTorus5_conformalRange_finrank_lt_finrank_edgeSpace
 201  rw [htop, finrank_top] at hlt
 202  exact lt_irrefl _ hlt
 203
 204/-- Some edge perturbation of the `N = 5` torus lies outside the conformal
 205image. -/
 206theorem periodicTorus5_exists_not_mem_conformalRange :
 207    ∃ ε : EncodedEdgePerturbation5,
 208      ε ∉ LinearMap.range (conformalStrainLinearMap PeriodicTorus5.K) := by
 209  by_contra h
 210  apply periodicTorus5_conformalRange_ne_top
 211  rw [Submodule.eq_top_iff']
 212  intro ε
 213  by_contra hε
 214  exact h ⟨ε, hε⟩
 215
 216/-- Existence form in the language of `IsConformalEdgePerturbation`. -/
 217theorem periodicTorus5_exists_nonconformal :
 218    ∃ ε : EncodedEdgePerturbation5,
 219      ¬ IsConformalEdgePerturbation PeriodicTorus5.K ε := by
 220  obtain ⟨ε, hε⟩ := periodicTorus5_exists_not_mem_conformalRange
 221  exact ⟨ε, fun hc =>
 222    hε ((isConformalEdgePerturbation_iff_mem_range PeriodicTorus5.K ε).mp hc)⟩
 223
 224/-! ## Bridges between encoded and typed conformal descriptions -/
 225
 226/-- Typed endpoint form of a conformal perturbation: some vertex potential
 227`φ` on typed torus vertices realizes it by endpoint averaging. -/
 228theorem periodicConformalLogSubspace5_endpoint_form
 229    (c : PeriodicEdgePerturbation5)
 230    (hc : PeriodicConformalLogSubspace5 c) :
 231    ∃ φ : PeriodicVertex5 → ℝ,
 232      ∀ e : PeriodicEdge5, c e = (φ e.endpoints.1 + φ e.endpoints.2) / 2 := by
 233  obtain ⟨ξ, rfl⟩ := hc
 234  refine ⟨fun v => ξ (periodicVertexEquiv5.symm v), fun e => ?_⟩
 235  unfold encodedToPeriodicEdgePerturbation5 conformalEdgeLogStrain
 236  rw [periodicTorus5_edgeVerts_symm_eq_endpoints]
 237
 238/-- The typed conformal slice corresponds exactly to the encoded conformal
 239predicate across the canonical edge equivalence. -/
 240theorem periodicConformalLogSubspace5_iff_encodedConformal
 241    (c : PeriodicEdgePerturbation5) :
 242    PeriodicConformalLogSubspace5 c ↔
 243      IsConformalEdgePerturbation PeriodicTorus5.K
 244        (periodicToEncodedEdgePerturbation5 c) := by
 245  constructor
 246  · rintro ⟨ξ, rfl⟩
 247    refine ⟨ξ, ?_⟩
 248    funext i
 249    simp [periodicToEncodedEdgePerturbation5, encodedToPeriodicEdgePerturbation5]
 250  · rintro ⟨ξ, hξ⟩
 251    refine ⟨ξ, ?_⟩
 252    funext e
 253    have h := congrFun hξ (PeriodicTorus5.edgeEquiv.symm e)
 254    simpa [periodicToEncodedEdgePerturbation5,
 255      encodedToPeriodicEdgePerturbation5] using h
 256
 257/-! ## 4. Explicit shear witness on one coordinate square of the torus -/
 258
 259/-- Corner `(0,0,0)` of the witness square. -/
 260def faceVertexA : PeriodicVertex5 := (0, 0, 0)
 261
 262/-- Corner `(1,0,0)` of the witness square. -/
 263def faceVertexB : PeriodicVertex5 := (1, 0, 0)
 264
 265/-- Corner `(1,1,0)` of the witness square. -/
 266def faceVertexC : PeriodicVertex5 := (1, 1, 0)
 267
 268/-- Corner `(0,1,0)` of the witness square. -/
 269def faceVertexD : PeriodicVertex5 := (0, 1, 0)
 270
 271/-- Bottom x-edge `A → B` (displacement class 0 = `+x`). -/
 272def faceEdgeAB : PeriodicEdge5 := { base := faceVertexA, disp := 0 }
 273
 274/-- Top x-edge `D → C`. -/
 275def faceEdgeDC : PeriodicEdge5 := { base := faceVertexD, disp := 0 }
 276
 277/-- Right y-edge `B → C` (displacement class 1 = `+y`). -/
 278def faceEdgeBC : PeriodicEdge5 := { base := faceVertexB, disp := 1 }
 279
 280/-- Left y-edge `A → D`. -/
 281def faceEdgeAD : PeriodicEdge5 := { base := faceVertexA, disp := 1 }
 282
 283theorem faceEdgeAB_endpoints :
 284    faceEdgeAB.endpoints = (faceVertexA, faceVertexB) := by decide
 285
 286theorem faceEdgeDC_endpoints :
 287    faceEdgeDC.endpoints = (faceVertexD, faceVertexC) := by decide
 288
 289theorem faceEdgeBC_endpoints :
 290    faceEdgeBC.endpoints = (faceVertexB, faceVertexC) := by decide
 291
 292theorem faceEdgeAD_endpoints :
 293    faceEdgeAD.endpoints = (faceVertexA, faceVertexD) := by decide
 294
 295/-- The rectangle/shear pattern embedded on one face of one cube of the
 296torus: strain `+1` on the two opposite x-edges, `-1` on the two opposite
 297y-edges, `0` on all other 871 edges. -/
 298def rectangleShearFace5 : PeriodicEdgePerturbation5 := fun e =>
 299  if e = faceEdgeAB then 1
 300  else if e = faceEdgeDC then 1
 301  else if e = faceEdgeBC then -1
 302  else if e = faceEdgeAD then -1
 303  else 0
 304
 305theorem rectangleShearFace5_apply_AB : rectangleShearFace5 faceEdgeAB = 1 := by
 306  simp [rectangleShearFace5]
 307
 308theorem rectangleShearFace5_apply_DC : rectangleShearFace5 faceEdgeDC = 1 := by
 309  have h : faceEdgeDC ≠ faceEdgeAB := by decide
 310  simp [rectangleShearFace5, h]
 311
 312theorem rectangleShearFace5_apply_BC : rectangleShearFace5 faceEdgeBC = -1 := by
 313  have h1 : faceEdgeBC ≠ faceEdgeAB := by decide
 314  have h2 : faceEdgeBC ≠ faceEdgeDC := by decide
 315  simp [rectangleShearFace5, h1, h2]
 316
 317theorem rectangleShearFace5_apply_AD : rectangleShearFace5 faceEdgeAD = -1 := by
 318  have h1 : faceEdgeAD ≠ faceEdgeAB := by decide
 319  have h2 : faceEdgeAD ≠ faceEdgeDC := by decide
 320  have h3 : faceEdgeAD ≠ faceEdgeBC := by decide
 321  simp [rectangleShearFace5, h1, h2, h3]
 322
 323theorem rectangleShearFace5_apply_of_ne (e : PeriodicEdge5)
 324    (h1 : e ≠ faceEdgeAB) (h2 : e ≠ faceEdgeDC)
 325    (h3 : e ≠ faceEdgeBC) (h4 : e ≠ faceEdgeAD) :
 326    rectangleShearFace5 e = 0 := by
 327  simp [rectangleShearFace5, h1, h2, h3, h4]
 328
 329theorem faceEdgeAB_not_mem_rest :
 330    faceEdgeAB ∉ ({faceEdgeDC, faceEdgeBC, faceEdgeAD} : Finset PeriodicEdge5) := by
 331  decide
 332
 333theorem faceEdgeDC_not_mem_rest :
 334    faceEdgeDC ∉ ({faceEdgeBC, faceEdgeAD} : Finset PeriodicEdge5) := by
 335  decide
 336
 337theorem faceEdgeBC_not_mem_rest :
 338    faceEdgeBC ∉ ({faceEdgeAD} : Finset PeriodicEdge5) := by
 339  decide
 340
 341/-- The 875-term inner product against the face shear collapses to its four
 342supported edges. -/
 343theorem periodicEdgeInnerProduct5_rectangleShearFace5_left
 344    (η : PeriodicEdgePerturbation5) :
 345    periodicEdgeInnerProduct5 rectangleShearFace5 η =
 346      η faceEdgeAB + η faceEdgeDC - η faceEdgeBC - η faceEdgeAD := by
 347  have hsubset :
 348      ({faceEdgeAB, faceEdgeDC, faceEdgeBC, faceEdgeAD} :
 349        Finset PeriodicEdge5) ⊆ Finset.univ :=
 350    Finset.subset_univ _
 351  have hzero : ∀ e ∈ (Finset.univ : Finset PeriodicEdge5),
 352      e ∉ ({faceEdgeAB, faceEdgeDC, faceEdgeBC, faceEdgeAD} :
 353        Finset PeriodicEdge5) →
 354      rectangleShearFace5 e * η e = 0 := by
 355    intro e _ he
 356    simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at he
 357    rw [rectangleShearFace5_apply_of_ne e he.1 he.2.1 he.2.2.1 he.2.2.2,
 358      zero_mul]
 359  have hsum := Finset.sum_subset hsubset hzero
 360  unfold periodicEdgeInnerProduct5
 361  rw [← hsum]
 362  rw [Finset.sum_insert faceEdgeAB_not_mem_rest,
 363    Finset.sum_insert faceEdgeDC_not_mem_rest,
 364    Finset.sum_insert faceEdgeBC_not_mem_rest,
 365    Finset.sum_singleton]
 366  rw [rectangleShearFace5_apply_AB, rectangleShearFace5_apply_DC,
 367    rectangleShearFace5_apply_BC, rectangleShearFace5_apply_AD]
 368  ring
 369
 370/-! ## 5. The face shear is a nonzero vector of the conformal orthogonal
 371complement -/
 372
 373/-- The face shear is orthogonal to the entire conformal slice: around the
 374square the endpoint averages telescope,
 375`(φA+φB) + (φD+φC) - (φB+φC) - (φA+φD) = 0`. -/
 376theorem rectangleShearFace5_inner_conformal_eq_zero
 377    (c : PeriodicEdgePerturbation5) (hc : PeriodicConformalLogSubspace5 c) :
 378    periodicEdgeInnerProduct5 rectangleShearFace5 c = 0 := by
 379  obtain ⟨φ, hφ⟩ := periodicConformalLogSubspace5_endpoint_form c hc
 380  have hAB : c faceEdgeAB = (φ faceVertexA + φ faceVertexB) / 2 := by
 381    rw [hφ faceEdgeAB, faceEdgeAB_endpoints]
 382  have hDC : c faceEdgeDC = (φ faceVertexD + φ faceVertexC) / 2 := by
 383    rw [hφ faceEdgeDC, faceEdgeDC_endpoints]
 384  have hBC : c faceEdgeBC = (φ faceVertexB + φ faceVertexC) / 2 := by
 385    rw [hφ faceEdgeBC, faceEdgeBC_endpoints]
 386  have hAD : c faceEdgeAD = (φ faceVertexA + φ faceVertexD) / 2 := by
 387    rw [hφ faceEdgeAD, faceEdgeAD_endpoints]
 388  rw [periodicEdgeInnerProduct5_rectangleShearFace5_left c,
 389    hAB, hDC, hBC, hAD]
 390  ring
 391
 392theorem rectangleShearFace5_inner_self_eq_four :
 393    periodicEdgeInnerProduct5 rectangleShearFace5 rectangleShearFace5 = 4 := by
 394  rw [periodicEdgeInnerProduct5_rectangleShearFace5_left,
 395    rectangleShearFace5_apply_AB, rectangleShearFace5_apply_DC,
 396    rectangleShearFace5_apply_BC, rectangleShearFace5_apply_AD]
 397  norm_num
 398
 399theorem rectangleShearFace5_ne_zero :
 400    rectangleShearFace5 ≠ (fun _ => 0) := by
 401  intro h
 402  have h1 := congrFun h faceEdgeAB
 403  rw [rectangleShearFace5_apply_AB] at h1
 404  exact one_ne_zero h1
 405
 406/-- Deliverable 5 (orthogonal split, witness form): the face shear is a
 407nonzero edge perturbation orthogonal to the whole conformal subspace, so the
 408orthogonal complement of the conformal slice inside the 875-dimensional edge
 409space contains a concrete nonzero vector. -/
 410theorem rectangleShearFace5_nonzero_in_orthogonal_complement :
 411    (∀ c : PeriodicEdgePerturbation5, PeriodicConformalLogSubspace5 c →
 412      periodicEdgeInnerProduct5 rectangleShearFace5 c = 0) ∧
 413    rectangleShearFace5 ≠ (fun _ => 0) :=
 414  ⟨rectangleShearFace5_inner_conformal_eq_zero, rectangleShearFace5_ne_zero⟩
 415
 416/-- The face shear is not vertex-conformal (typed coordinates): if it were,
 417orthogonality to itself would force its self inner product `4` to vanish. -/
 418theorem rectangleShearFace5_not_conformal_typed :
 419    ¬ PeriodicConformalLogSubspace5 rectangleShearFace5 := by
 420  intro hc
 421  have h0 := rectangleShearFace5_inner_conformal_eq_zero rectangleShearFace5 hc
 422  rw [rectangleShearFace5_inner_self_eq_four] at h0
 423  norm_num at h0
 424
 425/-- The face shear pushed to encoded `Fin PeriodicTorus5.K.nE` indices. -/
 426def rectangleShearFace5Encoded : EncodedEdgePerturbation5 :=
 427  periodicToEncodedEdgePerturbation5 rectangleShearFace5
 428
 429/-- Deliverable 4 (encoded form): an explicit edge perturbation of the
 430`N = 5` periodic Freudenthal torus with no vertex-conformal realization. -/
 431theorem rectangleShearFace5Encoded_not_conformal :
 432    ¬ IsConformalEdgePerturbation PeriodicTorus5.K rectangleShearFace5Encoded :=
 433  fun h =>
 434    rectangleShearFace5_not_conformal_typed
 435      ((periodicConformalLogSubspace5_iff_encodedConformal
 436        rectangleShearFace5).mpr h)
 437
 438/-- Constructive form of `periodicTorus5_exists_nonconformal`: the witness is
 439explicit. -/
 440theorem periodicTorus5_exists_nonconformal_constructive :
 441    ∃ ε : EncodedEdgePerturbation5,
 442      ¬ IsConformalEdgePerturbation PeriodicTorus5.K ε :=
 443  ⟨rectangleShearFace5Encoded, rectangleShearFace5Encoded_not_conformal⟩
 444
 445/-! ## Second witness: the uniform x-strain, via the rectangle obstruction -/
 446
 447/-- Unit strain on every `+x` edge, zero on the other six displacement
 448classes: a globally anisotropic (pure-shear-type) perturbation. -/
 449def xUniformStrain5 : PeriodicEdgePerturbation5 := fun e =>
 450  if e.disp = 0 then 1 else 0
 451
 452theorem xUniformStrain5_apply_AB : xUniformStrain5 faceEdgeAB = 1 := by
 453  have h : faceEdgeAB.disp = 0 := rfl
 454  simp [xUniformStrain5, h]
 455
 456theorem xUniformStrain5_apply_DC : xUniformStrain5 faceEdgeDC = 1 := by
 457  have h : faceEdgeDC.disp = 0 := rfl
 458  simp [xUniformStrain5, h]
 459
 460theorem xUniformStrain5_apply_BC : xUniformStrain5 faceEdgeBC = 0 := by
 461  have h : faceEdgeBC.disp ≠ 0 := by decide
 462  simp [xUniformStrain5, h]
 463
 464theorem xUniformStrain5_apply_AD : xUniformStrain5 faceEdgeAD = 0 := by
 465  have h : faceEdgeAD.disp ≠ 0 := by decide
 466  simp [xUniformStrain5, h]
 467
 468/-- The uniform x-strain is not vertex-conformal: instantiating the four
 469conformal endpoint averages on the witness square gives `h = 1`, `v = 0`, and
 470the rectangle obstruction of `TensorShearSector` forbids `h ≠ v`. -/
 471theorem xUniformStrain5_not_conformal_typed :
 472    ¬ PeriodicConformalLogSubspace5 xUniformStrain5 := by
 473  intro hc
 474  obtain ⟨φ, hφ⟩ := periodicConformalLogSubspace5_endpoint_form xUniformStrain5 hc
 475  have hAB : xUniformStrain5 faceEdgeAB = (φ faceVertexA + φ faceVertexB) / 2 := by
 476    rw [hφ faceEdgeAB, faceEdgeAB_endpoints]
 477  have hDC : xUniformStrain5 faceEdgeDC = (φ faceVertexD + φ faceVertexC) / 2 := by
 478    rw [hφ faceEdgeDC, faceEdgeDC_endpoints]
 479  have hBC : xUniformStrain5 faceEdgeBC = (φ faceVertexB + φ faceVertexC) / 2 := by
 480    rw [hφ faceEdgeBC, faceEdgeBC_endpoints]
 481  have hAD : xUniformStrain5 faceEdgeAD = (φ faceVertexA + φ faceVertexD) / 2 := by
 482    rw [hφ faceEdgeAD, faceEdgeAD_endpoints]
 483  rw [xUniformStrain5_apply_AB] at hAB
 484  rw [xUniformStrain5_apply_DC] at hDC
 485  rw [xUniformStrain5_apply_BC] at hBC
 486  rw [xUniformStrain5_apply_AD] at hAD
 487  refine nontrivial_rectangle_shear_not_vertexConformal 1 0 one_ne_zero
 488    ⟨φ faceVertexA, φ faceVertexB, φ faceVertexC, φ faceVertexD,
 489      ?_, ?_, ?_, ?_⟩
 490  · linarith
 491  · linarith
 492  · linarith
 493  · linarith
 494
 495/-- Encoded form of the uniform x-strain non-conformality. -/
 496theorem xUniformStrain5Encoded_not_conformal :
 497    ¬ IsConformalEdgePerturbation PeriodicTorus5.K
 498        (periodicToEncodedEdgePerturbation5 xUniformStrain5) :=
 499  fun h =>
 500    xUniformStrain5_not_conformal_typed
 501      ((periodicConformalLogSubspace5_iff_encodedConformal
 502        xUniformStrain5).mpr h)
 503
 504/-- The uniform x-strain pairs to `2` against the conformal-orthogonal face
 505shear. -/
 506theorem rectangleShearFace5_inner_xUniformStrain5 :
 507    periodicEdgeInnerProduct5 rectangleShearFace5 xUniformStrain5 = 2 := by
 508  rw [periodicEdgeInnerProduct5_rectangleShearFace5_left,
 509    xUniformStrain5_apply_AB, xUniformStrain5_apply_DC,
 510    xUniformStrain5_apply_BC, xUniformStrain5_apply_AD]
 511  norm_num
 512
 513/-- The uniform x-strain has a nonzero orthogonal projection onto the
 514complement of the conformal subspace: it pairs nontrivially with a vector
 515(`rectangleShearFace5`) that annihilates the whole conformal slice. -/
 516theorem xUniformStrain5_nonzero_orthogonal_component :
 517    ∃ t : PeriodicEdgePerturbation5,
 518      (∀ c : PeriodicEdgePerturbation5, PeriodicConformalLogSubspace5 c →
 519        periodicEdgeInnerProduct5 t c = 0) ∧
 520      periodicEdgeInnerProduct5 t xUniformStrain5 ≠ 0 := by
 521  refine ⟨rectangleShearFace5,
 522    rectangleShearFace5_inner_conformal_eq_zero, ?_⟩
 523  rw [rectangleShearFace5_inner_xUniformStrain5]
 524  norm_num
 525
 526/-! ## Capstone -/
 527
 528/-- Lane 3 capstone: on the `N = 5` periodic Freudenthal torus the conformal
 529slice has rank at most 125 inside the 875-dimensional edge space, and the gap
 530is realized by an explicit localized face shear with no vertex-conformal
 531realization. -/
 532theorem periodicTorus5_edge_tensor_sector_beyond_conformal :
 533    Module.finrank ℝ
 534        (LinearMap.range (conformalStrainLinearMap PeriodicTorus5.K)) ≤ 125 ∧
 535      Module.finrank ℝ EncodedEdgePerturbation5 = 875 ∧
 536      ¬ IsConformalEdgePerturbation PeriodicTorus5.K rectangleShearFace5Encoded :=
 537  ⟨periodicTorus5_conformalRange_finrank_le,
 538    finrank_encodedEdgePerturbation5,
 539    rectangleShearFace5Encoded_not_conformal⟩
 540
 541end
 542
 543end EdgeTensorSector
 544end SevenGaps
 545end Gravity
 546end IndisputableMonolith
 547