Gravity Seven Gaps Edge Tensor Sector

The edge tensor sector

In the Recognition Science framework, gravity on a discrete spacetime is studied by assigning numbers to the edges of a triangulated space, a 3D grid of points and links. The simplest approach, the conformal ansatz, assigns one number to each vertex and derives edge values as the average of the two endpoint values. This file examines that ansatz on a specific 5x5x5 periodic grid, a 3-torus, and proves it is a small slice of the full space of possible edge assignments.

The central result is a dimension gap. The conformal ansatz produces at most 125 independent edge assignments, one for each vertex. The full space of edge perturbations has 875 dimensions, one for each edge. The machine-checked library proves this gap, 125 versus 875, and exhibits a concrete edge perturbation that cannot be produced by the conformal ansatz. This witness is a rectangle shear: it puts strain +1 on two opposite edges of a unit square and -1 on the other two, a pattern no vertex-based assignment can generate.

This shear witness is not just non-conformal; it is orthogonal to the entire conformal slice. The framework's library proves this with an inner product, showing the shear is a genuinely new direction in the space of edge perturbations. A second witness, a uniform strain along one axis, is also proved non-conformal and has a nonzero projection onto this orthogonal complement. These are not numerical approximations; they are exact statements in the machine-checked library of formal theorems, with no unproved assumptions.

The significance is structural. The conformal ansatz, while natural, captures only a fraction of the possible geometric distortions. The full decomposition of the 875-dimensional edge space, including the transverse-traceless sector that would correspond to gravitational wave polarizations, remains open. This file establishes the first step: the conformal slice is a proper subspace, and the missing directions are real and explicit.

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

What this page does not claim

The full conformal plus longitudinal plus transverse-traceless decomposition is not proved here. No claim is made about the physical interpretation of the shear witness beyond its mathematical properties. The edge inner product is a modeling choice, not a derived quantity.

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: