Pith. sign in
module module high

IndisputableMonolith.Gravity.TensorShearSector

show as:
view Lean formalization →

Defines edge-level length perturbations on a discrete Regge surface: one degree of freedom per global edge, the natural arena for anisotropic shear and transverse-traceless modes. Contrasts this full edge space with the thinner vertex-conformal ansatz (log-strain averaged from endpoint potentials). Supplies the conformal slice, square-forcing lemmas, and a nontrivial rectangular shear witness. Downstream gravity tracks import it for the seven-gaps edge-tensor sector and ledger-to-geometry status.

claimOn a triangulation, an edge perturbation assigns one real length variation to each global edge. The conformal subsector is the image of vertex potentials via the edge log-strain $(\xi_u+\xi_v)/2$. The module records that image, the induced length perturbation, and proves that a nontrivial rectangular shear is not vertex-conformal (while vertex-conformal log-strain on a rectangle forces a square).

background

Recognition gravity works with a nonlinear Regge action on a 3D triangulation. The first-variation target (imported from the Regge first-variation module) is stationarity at the flat conformal potential, via Schläfli cancellation and zero deficit. The scalable mesh model is the periodic Freudenthal torus: typed periodic vertices, edges, and tetrahedra with the incidence partition needed by that variation theorem.

A vertex potential places one scalar at each vertex and induces only isotropic, conformal edge strains. Anisotropic shear and TT modes need a larger surface: one free length per global edge. This module is that surface. It also specializes the periodic model at $N=5$ (periodic vertices, edges, and the $5\times5\times5$ torus) so concrete witnesses can be written down.

Sibling definitions include the conformal edge log-strain, the matching length perturbation (related by a square-root factor times the log-strain), and the predicate that an edge field lies in the conformal image.

proof idea

Mostly a definition module with short comparison lemmas, not a single deep theorem. It introduces the edge-perturbation type, the conformal log-strain map from vertex data, and the induced length perturbation, then proves the algebraic relation between length perturbation and log-strain.

Two geometric facts pin the conformal slice: on a rectangle, vertex-conformal log-strain forces the square geometry; conversely, a nontrivial rectangular shear field fails the vertex-conformal predicate. The $N=5$ periodic torus aliases supply concrete index maps so later files can exhibit an explicit localized shear witness outside the conformal image.

why it matters in Recognition Science

This is the finite Regge surface for modes the vertex-conformal ansatz cannot see. The seven-gaps edge-tensor sector imports it to measure how small the conformal slice is inside full edge space on the actual $5\times5\times5$ periodic Freudenthal 3-torus, and to exhibit the shear complement with a localized witness (using the conformal log-strain map defined here).

The ledger-to-geometry bridge and the Track-7 master handoff integration also import the module, so edge-level shear sits in the honest status path from discrete recognition ledger to hinge geometry and in the fork receipts (stationarity reduction, physical residual/Bianchi interface). Without a clean edge sector, claims that the conformal potential captures the full first-variation story would be incomplete.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (201)

… and 121 more