Gravity Seven Gaps Edge Tensor Sector Periodic Edge Inner Product5 Rectangle She

The shear witness

The declaration periodicEdgeInnerProduct5_rectangleShearFace5_left is a proved fact about a specific geometric object called rectangleShearFace5, a ledger (a discrete record of events) that assigns strain values to the edges of a 5 by 5 by 5 periodic grid. The grid is a three-dimensional torus: opposite faces are identified, so an edge leaving one side re-enters on the other. The declaration states that when you take the inner product of this rectangle-shaped strain with any other strain on the grid, the result is a simple sum: the value on one pair of opposite edges plus the value on the other pair, with a minus sign for the two vertical edges. In plain terms, it gives you a formula for how the rectangle shear interacts with everything else.

This formula is not an isolated curiosity. It is the computational heart of a larger proof. The rectangle shear puts strain +1 on two horizontal edges and -1 on two vertical edges of a unit square. The declaration's formula lets the library show that this rectangle shear is orthogonal to the entire conformal slice, the subspace of strains that come from assigning a single number to each vertex. That orthogonality means the rectangle shear cannot be reproduced by any vertex-based description. It is a genuinely new direction in the space of all edge strains, a nonzero vector pointing outside the conformal subspace. The library proves this with no unproved assumptions: the declaration is a theorem, not a definition or a hypothesis.

In Recognition Science, this matters because the framework models gravity through such edge perturbations on a lattice. The declaration establishes that the conformal slice, the smooth vertex-based strains, is a proper subspace of the full 875-dimensional edge space. It exhibits one concrete vector, the rectangle shear, that lies outside it. The declaration itself does not claim to build the full orthogonal decomposition of the edge space, nor does it claim that the rectangle shear is the only such vector. It proves one fact: a specific formula for the inner product of the rectangle shear with any other strain. That formula is the key to the orthogonality result, but it is not the whole story of the edge space's structure.

/-- The 875-term inner product against the face shear collapses to its four
supported edges. -/
theorem periodicEdgeInnerProduct5_rectangleShearFace5_left
    (η : PeriodicEdgePerturbation5) :
    periodicEdgeInnerProduct5 rectangleShearFace5 η =
      η faceEdgeAB + η faceEdgeDC - η faceEdgeBC - η faceEdgeAD := by
  have hsubset :
      ({faceEdgeAB, faceEdgeDC, faceEdgeBC, faceEdgeAD} :
        Finset PeriodicEdge5) ⊆ Finset.univ :=
    Finset.subset_univ _
  have hzero : ∀ e ∈ (Finset.univ : Finset PeriodicEdge5),
      e ∉ ({faceEdgeAB, faceEdgeDC, faceEdgeBC, faceEdgeAD} :
        Finset PeriodicEdge5) →
      rectangleShearFace5 e * η e = 0 := by
    intro e _ he
    simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at he
    rw [rectangleShearFace5_apply_of_ne e he.1 he.2.1 he.2.2.1 he.2.2.2,
      zero_mul]
  have hsum := Finset.sum_subset hsubset hzero
  unfold periodicEdgeInnerProduct5
  rw [← hsum]
  rw [Finset.sum_insert faceEdgeAB_not_mem_rest,
    Finset.sum_insert faceEdgeDC_not_mem_rest,
    Finset.sum_insert faceEdgeBC_not_mem_rest,
    Finset.sum_singleton]
  rw [rectangleShearFace5_apply_AB, rectangleShearFace5_apply_DC,
    rectangleShearFace5_apply_BC, rectangleShearFace5_apply_AD]
  ring

/-- 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 declaration does not build the full conformal plus longitudinal-gauge plus transverse-traceless decomposition of the edge space. The declaration does not claim the rectangle shear is the only non-conformal vector. The declaration does not prove the rectangle shear is physically realized; it only proves a mathematical fact about a defined object.

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: