Gravity Seven Gaps Edge Tensor Sector Periodic Torus5 Edge Tensor Sector Beyond

The shear complement

A three-dimensional grid that wraps around on itself, a 5 by 5 by 5 torus made of 125 points and 875 connecting edges. A conformal distortion, one that changes lengths but not angles, can be described by assigning a single number to each point. The framework's library of machine-checked formal theorems proves that this conformal slice is a proper subspace: it has dimension at most 125, while the full space of edge distortions has dimension 875. The gap is real, not an artifact of a particular choice of edge lengths or weights.

The library then exhibits a concrete distortion that lives outside the conformal slice. The ledger, a discrete record of events, here records strain values on edges: the chosen example puts strain +1 on two opposite edges of a unit square and -1 on the other two, a pure shear that changes angles without changing area. This rectangle shear is proved non-conformal, and it is orthogonal to every conformal distortion under the standard inner product. A second example, a uniform stretch along one axis, also falls outside the conformal slice and has a nonzero projection onto the orthogonal complement.

In Recognition Science, the framework models gravity through such edge perturbations on a triangulated space. This file establishes that the conformal ansatz, a natural first guess for describing distortions, is far too narrow to capture the full range of possibilities. The result is a theorem, fully proved with no unproved assumptions, but it is a statement about a specific finite model, not a general physical law.

What the declaration does not claim is equally important. It does not build the full orthogonal decomposition of the 875-dimensional edge space into conformal, longitudinal, and transverse-traceless parts; that splitting remains open. It does not claim that the rectangle shear represents a physically realizable gravitational wave or any specific physical process. It establishes a mathematical fact about a finite model, a concrete demonstration that the conformal slice is not the whole story.

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

/-- Computed from the definitions: the `5 × 5 × 5` torus has 125 vertices. -/
theorem periodicTorus5_nV_eq : PeriodicTorus5.K.nV = 125 := by
  show Fintype.card PeriodicVertex5 = 125
  simp [PeriodicVertex5, Vertex]

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 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

/-- 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 full conformal plus longitudinal-gauge plus transverse-traceless decomposition is not constructed. The rectangle shear is not claimed to represent a physically realizable gravitational wave. The result does not extend beyond the specific 5 by 5 by 5 periodic torus unless separately proved.

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: