Gravity Seven Gaps Edge Tensor Sector Periodic Torus5 Exists Not Mem Conformal R

A narrow slice of strains

A 5 by 5 by 5 grid of points wrapped into a donut shape in three directions, a periodic torus. Each point connects to its neighbors by edges, and each edge can carry a number representing a strain or a stretch. One simple way to assign these edge strains is to start with a number at each vertex and then define the strain on an edge as the average of the two vertex numbers at its ends. This is the conformal ansatz, a common and convenient starting point in geometry.

On this particular torus there are 125 vertices and 875 edges. A theorem proved in the machine-checked library of formal theorems shows that the simple vertex rule can only produce a small fraction of all possible edge strain patterns. The rule's reach is at most 125 dimensions, while the full space of edge strains has 875 dimensions. The declaration periodicTorus5_exists_not_mem_conformalRange states that there exists at least one edge strain pattern that cannot be written as the average of vertex values. This is not an abstract possibility; the proof exhibits a concrete example: a rectangle shear on one face of the torus, where two opposite edges get a strain of +1 and the other two get -1. This pattern is shown to be orthogonal to every pattern the vertex rule can produce.

The result is a dimension count, not a statement about physics. It says that the space of all edge strains is much larger than the space of vertex-derived strains. This gap is a structural fact about this discrete geometry. The proof is fully formal: it contains no gaps, no unproved assumptions, and no hidden hypotheses. The counts of 125 vertices and 875 edges are computed from the definitions, not assumed.

In Recognition Science, this result is part of a broader exploration of how gravity-like theories might emerge from discrete structures. The framework models space as a network of points and edges, and this theorem shows that a natural first guess for assigning strains is too restrictive. The full space of edge strains contains many more possibilities, and understanding that extra freedom is an open target. This particular theorem does not build the complete decomposition of the 875-dimensional space; it only proves that the conformal slice is a proper subspace and exhibits one nonzero vector outside it.

The practical lesson is that a vertex-based description of strain is a genuine restriction, not a harmless simplification. On this torus, it misses most of what is possible. The explicit shear witness provides a concrete handle on the missing part, a starting point for future work on the full structure.

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

/-- Constructive form of `periodicTorus5_exists_nonconformal`: the witness is
explicit. -/
theorem periodicTorus5_exists_nonconformal_constructive :
    ∃ ε : EncodedEdgePerturbation5,
      ¬ IsConformalEdgePerturbation PeriodicTorus5.K ε :=
  ⟨rectangleShearFace5Encoded, rectangleShearFace5Encoded_not_conformal⟩

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

This theorem does not construct the full conformal-plus-longitudinal-plus-TT decomposition of the edge space. It does not claim that the rectangle shear pattern is the only non-conformal edge strain. It makes no statement about the physical interpretation of these strains in a gravitational context.

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: