module module moderate

`IndisputableMonolith.Gravity.SevenGaps.EdgeTensorSector`

Packages the vertex-conformal log-strain as an ℝ-linear map from vertex potentials into edge perturbations, then proves finite-rank bounds showing that range is a proper subspace of the full edge space on a 5-periodic torus. Cited by anyone separating conformal scalar modes from shear in the weak-field gravity sector. Argument is linear-algebra bookkeeping: identify the map, compute ranks, and compare dimensions.

claimLet $L:\mathbb{R}^{n_V}\to\mathbb{R}^{n_E}$ be the real-linear conformal strain map sending a vertex potential to the edge log-strain by averaging endpoint values. Then $\operatorname{rank}(\operatorname{im} L)\le n_V$. On the 5-periodic torus one has $n_V<n_E$, hence $\operatorname{rank}(\operatorname{im} L)<\operatorname{rank}(\mathbb{R}^{n_E})$: the conformal sector is a proper subspace of edge perturbations.

background

Track 1.B of the gravity scaffold assigns one scalar potential per graph vertex and induces edge-length (log-strain) variations by averaging the two endpoint potentials. That construction is the conformal, pure-trace slice of the weak-field metric sector. Upstream TensorShearSector records the limitation: the scalar slice cannot represent pure shear and therefore cannot cover transverse-traceless gravitational-wave modes by itself.

This module isolates that conformal piece as an explicit $\mathbb{R}$-linear map from the vertex-potential space into the edge-perturbation space, and equips it with membership and rank lemmas. A concrete 5-periodic torus model supplies equalities for $n_V$ and $n_E$ so the rank comparison becomes numerical rather than schematic.

The setting is finite-dimensional real linear algebra on a discrete graph (or periodic lattice), not continuum GR. Edge perturbations are treated as vectors in $\mathbb{R}^{n_E}$; conformal ones are exactly the image of $L$.

proof idea

Definition layer first: the conformal strain is packaged as a LinearMap from vertex potentials to edge perturbations, with an apply lemma matching the endpoint-average formula. A membership iff characterizes conformal edge perturbations as exactly the range of that map.

Rank layer: finite-dimensional rank of the vertex-potential space and of the edge-perturbation space, plus the general inequality that the conformal range has rank at most $n_V$. On the 5-periodic torus, product equivalences fix $n_V$ and $n_E$, and the encoded edge space inherits the edge rank. Chaining those equalities yields range-rank $\le n_V < n_E$, hence a strict subspace inclusion.

why it matters in Recognition Science

Feeds the Seven-Gaps Campaign Ledger as an imported scoped increment: machine-checked separation of the conformal scalar slice from the residual edge (shear-capable) directions. The ledger style records what was proved in-kernel versus what remains open toward full physical closure, without flipping full-strength QGScopeAudit flags.

In the Recognition gravity program this is the discrete counterpart of splitting metric perturbations into trace and traceless pieces. Without a strict rank gap, one could not argue that Track 1.B misses TT-like modes; the torus comparison supplies that gap on a concrete finite model. It sits under the broader tensor/shear Track 1.D scaffold and supports later claims that a genuine shear sector is needed beyond pure conformal strain.

scope and limits

Does not construct or classify pure shear or TT modes; only bounds the conformal range.
Does not prove a continuum or continuum-limit statement; ranks are finite-graph linear algebra.
Does not flip any full-strength QGScopeAudit closure flag in the campaign ledger.
Does not claim the 5-periodic torus exhausts all physically relevant graphs.
Does not derive Einstein equations or dynamical propagation from the rank gap.

used by (1)

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

IndisputableMonolith.Gravity.SevenGaps.CampaignLedger module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.TensorShearSector module_import

declarations in this module (57)

def conformalStrainLinearMap L101
theorem conformalStrainLinearMap_apply L114
theorem isConformalEdgePerturbation_iff_mem_range L120
theorem finrank_vertexPotential L133
theorem finrank_edgePerturbation L138
theorem conformalRange_finrank_le_nV L145
def periodicEdge5EquivProd L153
theorem periodicTorus5_nV_eq L160
theorem periodicTorus5_nE_eq L168
theorem finrank_encodedEdgePerturbation5 L174
theorem periodicTorus5_conformalRange_finrank_le L180
theorem periodicTorus5_conformalRange_finrank_lt_finrank_edgeSpace L188
theorem periodicTorus5_conformalRange_ne_top L197
theorem periodicTorus5_exists_not_mem_conformalRange L206
theorem periodicTorus5_exists_nonconformal L217
theorem periodicConformalLogSubspace5_endpoint_form L228
theorem periodicConformalLogSubspace5_iff_encodedConformal L240
def faceVertexA L260
def faceVertexB L263
def faceVertexC L266
def faceVertexD L269
def faceEdgeAB L272
def faceEdgeDC L275
def faceEdgeBC L278
def faceEdgeAD L281
theorem faceEdgeAB_endpoints L283
theorem faceEdgeDC_endpoints L286
theorem faceEdgeBC_endpoints L289
theorem faceEdgeAD_endpoints L292
def rectangleShearFace5 L298
theorem rectangleShearFace5_apply_AB L305
theorem rectangleShearFace5_apply_DC L308
theorem rectangleShearFace5_apply_BC L312
theorem rectangleShearFace5_apply_AD L317
theorem rectangleShearFace5_apply_of_ne L323
theorem faceEdgeAB_not_mem_rest L329
theorem faceEdgeDC_not_mem_rest L333
theorem faceEdgeBC_not_mem_rest L337
theorem periodicEdgeInnerProduct5_rectangleShearFace5_left L343
theorem rectangleShearFace5_inner_conformal_eq_zero L376
theorem rectangleShearFace5_inner_self_eq_four L392
theorem rectangleShearFace5_ne_zero L399
theorem rectangleShearFace5_nonzero_in_orthogonal_complement L410
theorem rectangleShearFace5_not_conformal_typed L418
def rectangleShearFace5Encoded L426
theorem rectangleShearFace5Encoded_not_conformal L431
theorem periodicTorus5_exists_nonconformal_constructive L440
def xUniformStrain5 L449
theorem xUniformStrain5_apply_AB L452
theorem xUniformStrain5_apply_DC L456
theorem xUniformStrain5_apply_BC L460
theorem xUniformStrain5_apply_AD L464
theorem xUniformStrain5_not_conformal_typed L471
theorem xUniformStrain5Encoded_not_conformal L496
theorem rectangleShearFace5_inner_xUniformStrain5 L506
theorem xUniformStrain5_nonzero_orthogonal_component L516
theorem periodicTorus5_edge_tensor_sector_beyond_conformal L532