Gravity Seven Gaps Edge Tensor Sector Rectangle Shear Face5 Nonzero In Orthogona

The shear witness

A 5 by 5 by 5 grid of points wrapped into a torus, so that moving 5 steps in any direction returns you to the start. This grid has 125 points and 875 edges connecting neighboring points. A strain assigns a number to each edge, describing how that edge stretches or compresses. One natural family of strains assigns a single value to each point and derives edge strains as the average of the two endpoint values; call this the conformal family. The framework's machine-checked library of formal theorems proves that this conformal family occupies at most 125 dimensions of the 875-dimensional space of all possible edge strains, so the conformal strains form a proper subspace with a large orthogonal complement.

To make that abstract gap concrete, the declaration rectangleShearFace5_nonzero_in_orthogonal_complement exhibits a specific strain pattern: put +1 on the two horizontal edges of the unit square with corners (0,0,0), (1,0,0), (1,1,0), (0,1,0), and put -1 on the two vertical edges of that same square. This pattern, called a rectangle shear, is not in the conformal family, and it is orthogonal to every conformal strain under the standard inner product. The declaration proves the pattern is nonzero, so it is a concrete witness that the orthogonal complement is nonempty. A second witness, a uniform strain along the x-direction, also has a nonzero projection onto that complement, showing the gap is not an artifact of one specially chosen pattern.

In Recognition Science, this result matters because it sharpens the picture of what edge perturbations are possible on a periodic lattice. The conformal ansatz, assigning one scalar per vertex, is a natural starting point, but the theorem shows it leaves room for genuinely different deformations. The shear witness is a building block for understanding the full structure of the edge space, though the complete orthogonal decomposition into conformal, longitudinal, and transverse-traceless parts remains an open target. The declaration does not claim that this shear pattern is physically realized in any gravitational setting, nor that the full decomposition is complete. It establishes one precise fact: the conformal slice is a proper subspace, and here is a nonzero vector orthogonal to it.

theorem periodicTorus5_conformalRange_finrank_le :
    Module.finrank ℝ
      (LinearMap.range (conformalStrainLinearMap PeriodicTorus5.K)) ≤ 125 := by
  have h := conformalRange_finrank_le_nV PeriodicTorus5.K
  exact h.trans periodicTorus5_nV_eq.le

/-- The face shear is orthogonal to the entire conformal slice: around the
square the endpoint averages telescope,
`(φA+φB) + (φD+φC) - (φB+φC) - (φA+φD) = 0`. -/
theorem rectangleShearFace5_inner_conformal_eq_zero
    (c : PeriodicEdgePerturbation5) (hc : PeriodicConformalLogSubspace5 c) :
    periodicEdgeInnerProduct5 rectangleShearFace5 c = 0 := by
  obtain ⟨φ, hφ⟩ := periodicConformalLogSubspace5_endpoint_form c hc
  have hAB : c faceEdgeAB = (φ faceVertexA + φ faceVertexB) / 2 := by
    rw [hφ faceEdgeAB, faceEdgeAB_endpoints]
  have hDC : c faceEdgeDC = (φ faceVertexD + φ faceVertexC) / 2 := by
    rw [hφ faceEdgeDC, faceEdgeDC_endpoints]
  have hBC : c faceEdgeBC = (φ faceVertexB + φ faceVertexC) / 2 := by
    rw [hφ faceEdgeBC, faceEdgeBC_endpoints]
  have hAD : c faceEdgeAD = (φ faceVertexA + φ faceVertexD) / 2 := by
    rw [hφ faceEdgeAD, faceEdgeAD_endpoints]
  rw [periodicEdgeInnerProduct5_rectangleShearFace5_left c,
    hAB, hDC, hBC, hAD]
  ring

theorem rectangleShearFace5_ne_zero :
    rectangleShearFace5 ≠ (fun _ => 0) := by
  intro h
  have h1 := congrFun h faceEdgeAB
  rw [rectangleShearFace5_apply_AB] at h1
  exact one_ne_zero h1

/-- The uniform x-strain is not vertex-conformal: instantiating the four
conformal endpoint averages on the witness square gives `h = 1`, `v = 0`, and
the rectangle obstruction of `TensorShearSector` forbids `h ≠ v`. -/
theorem xUniformStrain5_not_conformal_typed :
    ¬ PeriodicConformalLogSubspace5 xUniformStrain5 := by
  intro hc
  obtain ⟨φ, hφ⟩ := periodicConformalLogSubspace5_endpoint_form xUniformStrain5 hc
  have hAB : xUniformStrain5 faceEdgeAB = (φ faceVertexA + φ faceVertexB) / 2 := by
    rw [hφ faceEdgeAB, faceEdgeAB_endpoints]
  have hDC : xUniformStrain5 faceEdgeDC = (φ faceVertexD + φ faceVertexC) / 2 := by
    rw [hφ faceEdgeDC, faceEdgeDC_endpoints]
  have hBC : xUniformStrain5 faceEdgeBC = (φ faceVertexB + φ faceVertexC) / 2 := by
    rw [hφ faceEdgeBC, faceEdgeBC_endpoints]
  have hAD : xUniformStrain5 faceEdgeAD = (φ faceVertexA + φ faceVertexD) / 2 := by
    rw [hφ faceEdgeAD, faceEdgeAD_endpoints]
  rw [xUniformStrain5_apply_AB] at hAB
  rw [xUniformStrain5_apply_DC] at hDC
  rw [xUniformStrain5_apply_BC] at hBC
  rw [xUniformStrain5_apply_AD] at hAD
  refine nontrivial_rectangle_shear_not_vertexConformal 1 0 one_ne_zero
    ⟨φ faceVertexA, φ faceVertexB, φ faceVertexC, φ faceVertexD,
      ?_, ?_, ?_, ?_⟩
  · linarith
  · linarith
  · linarith
  · linarith

What this page does not claim

The rectangle shear pattern is a physically realized gravitational deformation. The full orthogonal decomposition of the edge space is complete. The conformal family is the only natural or useful family of edge strains.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/SevenGaps/EdgeTensorSector.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: