Gravity Seven Gaps Edge Tensor Sector X Uniform Strain5 Nonzero Orthogonal Compo

A concrete non-conformal strain

In the Recognition Science framework, a ledger (a discrete record of events) on a 5×5×5 periodic grid assigns a real number to each of the 875 edges. One simple assignment is the uniform x-strain: put the number 1 on every edge pointing in the x-direction and 0 on all others. The question is whether this assignment can be reproduced by a conformal ansatz, a scheme that assigns one scalar per vertex and derives edge values by averaging endpoint scalars. The declaration xUniformStrain5_nonzero_orthogonal_component proves it cannot.

The proof works by exhibiting a second perturbation, the rectangle shear, which puts +1 on two x-edges and -1 on two y-edges of a unit square. This rectangle shear is itself non-conformal, and it is orthogonal to every conformal perturbation under the standard edge inner product. The uniform x-strain pairs to a nonzero value (specifically 2) against this rectangle shear. Since the uniform x-strain has a nonzero projection onto the orthogonal complement of the conformal subspace, it cannot lie in that subspace. The framework's machine-checked library of formal theorems verifies this chain completely, with no unproved assumptions.

What this establishes is concrete: the conformal slice is a proper subspace of the full 875-dimensional edge space. The uniform x-strain is a specific, simple vector outside it, and the rectangle shear is a specific vector in the complement. This is a structural fact about the space of edge perturbations, not a claim about any particular physical system.

What it does not claim: the declaration does not build the full orthogonal decomposition of the edge space into conformal, longitudinal-gauge, and transverse-traceless parts. That decomposition remains open. It also does not claim that the uniform x-strain is physically preferred or that it has any special role in gravity; it is a mathematical witness, not a physical prediction.

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

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

What this page does not claim

The full conformal ⊕ longitudinal-gauge ⊕ TT decomposition is built. The uniform x-strain is physically preferred or has a special role in gravity. The conformal slice is the only proper subspace of the edge space.

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: