Gravity Tensor Shear Sector

Shear in the metric

In general relativity, the weak field of gravity is not a single number but a small distortion of geometry at each point. That distortion splits into distinct kinds: a uniform scaling part, a part that stretches along one axis while squeezing along another, and wavelike parts that travel. The shear part, the stretch-and-squeeze, is what transverse-traceless gravitational waves are made of. A metric that only records a single scale at each point cannot represent shear at all; it is like trying to describe a rectangle with only its area.

The classical picture comes from the early twentieth century. Albert Einstein's 1915 field equations describe how matter curves spacetime, and in 1916 he predicted that accelerating masses would send ripples through that curvature. In 1918 he worked out the details of these waves, showing they have two independent polarizations, both of them shear-like distortions. The modern description of these waves uses the transverse-traceless gauge, a choice of coordinates that isolates the purely shear part of the metric. A gravitational wave passing through a ring of particles stretches it along one axis and squeezes it along the perpendicular axis, then reverses. That is shear in action, and no scalar field can produce it.

In Recognition Science, the framework models spacetime as a discrete grid of points connected by edges, and it assigns a length to each edge. The framework's library, a machine-checked collection of formal theorems, first tried to describe weak-field gravity by giving each vertex a single potential and averaging endpoint values to get edge lengths. That scalar slice cannot represent shear, so it cannot cover gravitational waves. The tensor shear sector starts a new track: it gives each edge its own independent length perturbation, the natural discrete analogue of a shear mode.

The module proves a specific obstruction. If you assign a scalar potential to each vertex and define edge lengths by averaging the two endpoint potentials, then on a rectangle the two opposite edge lengths are forced to be equal. The theorem states that if the average of the top and bottom potentials equals the average of the left and right potentials, and similarly for the other pair, then the two averages must be the same. In plain terms, a vertex-conformal ansatz cannot produce a rectangle that is longer than it is wide; it always yields a square. That is the elementary reason why shear needs edge-level degrees of freedom.

Beyond that obstruction, the module sets up a target: to decompose any periodic edge perturbation into three orthogonal parts, a conformal part, a gauge part, and a transverse-traceless part. The target is defined for a periodic grid of five vertices per side, and the library proves that if certain data about the gauge map and its Gram matrix are supplied, the decomposition exists. The Gram matrix is the table of inner products between the gauge generators; a range criterion on it is enough to guarantee the orthogonal split. This is the discrete analogue of the standard decomposition of a metric perturbation in continuum general relativity.

The consequence is that the framework now has a vocabulary for shear, and with it a path toward gravitational waves on a discrete grid. The rectangle obstruction is a clean, checkable fact: a scalar-per-vertex model is provably too poor to describe a stretched rectangle. The edge-level perturbations and the decomposition target are the first steps toward a fuller tensor sector, one that can in principle carry transverse-traceless modes. The physical bridge from these discrete modes to continuum gravitational waves remains open, but the algebraic scaffolding is in place.

/-- Rectangle obstruction in first-order log strains.  If a quadrilateral's two
opposite horizontal edges have conformal log-strain `h` and its two opposite
vertical edges have conformal log-strain `v`, then `h = v`.  Hence a nontrivial
rectangle/shear mode cannot be vertex-conformal. -/
theorem vertexConformal_rectangle_log_strain_forces_square
    (ξa ξb ξc ξd h v : ℝ)
    (hab : (ξa + ξb) / 2 = h)
    (hcd : (ξc + ξd) / 2 = h)
    (hbc : (ξb + ξc) / 2 = v)
    (hda : (ξd + ξa) / 2 = v) :
    h = v := by
  linarith

/-- Honest Track 1.D decomposition target with TT interpreted as finite
orthogonality to the conformal and gauge subspaces.  The remaining mathematical
load is the construction of the three projectors. -/
def PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5
    (GaugePotential : Type) (gaugeMap : GaugePotential → PeriodicEdgePerturbation5) : Prop :=
  ∃ split : RawEdgePerturbationSplitting PeriodicEdge5,
    (∀ ε, PeriodicConformalLogSubspace5 (split.conformalPart ε)) ∧
    (∀ ε, PeriodicGaugeSubspace5 GaugePotential gaugeMap (split.gaugePart ε)) ∧
    (∀ ε, PeriodicTTOrthogonal5 GaugePotential gaugeMap (split.ttPart ε))

/-- The concrete longitudinal TT decomposition target is closed by the proved
finite Gram range theorem. -/
theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_provedGramRangeCriterion :
    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5
      (PeriodicLongitudinalGaugeIdx5 → ℝ) periodicLongitudinalGaugeMap5 :=
  periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramRangeCriterionData
    periodicTTGramRangeCriterionData5_proved

What this page does not claim

The module does not prove that gravitational waves exist on the discrete grid. The module does not derive the speed or dispersion relation of any discrete wave mode. The physical bridge from discrete edge perturbations to continuum gravitational waves is not established.

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/TensorShearSector.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: