Gravity Seven Gaps Edge Tensor Sector Periodic Torus5 Conformal Range Finrank Lt

The dimension gap

A three-dimensional grid of points, wrapped around so that it forms a finite periodic torus, like a video game world that loops at its boundaries. On this specific grid, a 5×5×5 torus, there are 125 vertices (corner points) and 875 edges (the lines connecting them). The question at hand is how to describe small distortions, or perturbations, of these edges.

One natural approach is the conformal ansatz: a guess that assigns a single number, a potential, to each vertex, and then defines the distortion of each edge as the average of the potentials at its two endpoints. This is a simple, local rule. The theorem in question, periodicTorus5_conformalRange_finrank_lt_finrank_edgeSpace, proves that this rule is severely limited. The space of all possible edge distortions has 875 dimensions, but the distortions that can be produced by the conformal ansatz occupy a subspace of at most 125 dimensions. The theorem states this gap plainly: 125 is strictly less than 875, so the conformal approach cannot reach most of the possible edge configurations.

The proof is not just an abstract inequality. It constructs a concrete example of a distortion that the conformal ansatz misses: a shear on a single unit square of the torus. This shear, a stretching that pulls the square's edges in opposite directions, is explicitly shown to be impossible to create with any assignment of vertex potentials. In addition, this shear is orthogonal to the entire conformal subspace, meaning it is not just outside it, but completely perpendicular to it. This gives a tangible, geometric witness to the gap.

In the Recognition Science framework, this result is a piece of a larger project to understand the structure of edge perturbations in a discrete model of gravity. The framework's machine-checked library of formal theorems proves this dimension gap on the periodic torus. The result establishes that the conformal ansatz, while a useful starting point, is only a small slice of the full space of possibilities. It does not, however, claim to describe what the missing dimensions look like or how they might be filled.

What this theorem does not claim is equally important. It does not provide a complete orthogonal decomposition of the 875-dimensional edge space. The full splitting into conformal, longitudinal, and transverse-traceless parts remains an open problem. The theorem also does not claim that the conformal ansatz is physically wrong; it only proves that it is incomplete. The missing 750 dimensions are not errors, but unexplored territory.

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

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

What this page does not claim

The theorem does not provide a complete orthogonal decomposition of the edge space. The theorem does not claim that the conformal ansatz is physically incorrect, only incomplete. The theorem does not apply to all possible triangulations, only the specific 5×5×5 periodic torus.

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: