Gravity Seven Gaps Edge Tensor Sector Periodic Torus5 Exists Nonconformal Constr

A concrete shear witness

In three-dimensional geometry, a common simplifying assumption is that a distortion of a shape can be described by scaling near each point, an approach called a conformal ansatz. On a discrete grid, this means assigning a single number to each vertex and deriving the strain on every edge from those vertex numbers. The theorem periodicTorus5_exists_nonconformal_constructive proves that on a specific periodic 5x5x5 torus, this assumption leaves out most of the possible edge distortions.

The torus in question is a 5x5x5 periodic grid with 125 vertices and 875 edges, a standard triangulation of a three-dimensional torus. The conformal ansatz, assigning one scalar per vertex, can generate at most 125 independent edge distortions. Since the full space of edge distortions has 875 dimensions, the conformal slice is a proper subspace. The theorem goes further than proving existence: it constructs an explicit example of a non-conformal edge perturbation, called rectangleShearFace5.

This witness is a shear on a single unit square face of the torus. It puts strain +1 on the two edges running in the x-direction and strain -1 on the two edges running in the y-direction of that face. The machine-checked proof verifies that this pattern cannot arise from any assignment of scalars to vertices, even though it is a perfectly valid edge perturbation. The same file also proves that this shear is orthogonal to the entire conformal subspace, meaning it is not merely non-conformal but entirely perpendicular to it.

Recognition Science, the framework that produced this result, models physical structure through a discrete ledger of recognition events. Here, the framework's machine-checked library of formal theorems establishes a concrete fact about the geometry of edge perturbations on a periodic torus. The result is proved with zero axioms beyond the standard logical ones, and the witness is explicit: one can write down the exact pattern of strains on the 875 edges.

What this theorem does not claim is equally important. It does not provide a complete orthogonal decomposition of the 875-dimensional edge space into conformal, longitudinal, and transverse-traceless parts. That full splitting remains an open target. The theorem also does not claim that the conformal ansatz is useless; it merely shows that it is incomplete. The shear witness is a concrete counterexample to the idea that all edge distortions can be captured by vertex scalings, and it opens the door to studying the full space of perturbations.

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

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

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

What this page does not claim

The theorem does not provide the full conformal, longitudinal, and transverse-traceless orthogonal decomposition of the edge space. The theorem does not claim that the conformal ansatz is physically incorrect, only that it is incomplete on this torus. The theorem does not establish any property of the full 875-dimensional space beyond the existence of a non-conformal perturbation.

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: