Gravity Analysis Regge Edge Ttattachment4 D Witness Edge Load Tt Ne Zero

The witness edge load

In the framework's study of how gravity might emerge from a discrete lattice, the declaration witness_edgeLoad_tt_ne_zero pins down one concrete fact: for a particular chosen plane wave and a particular symmetric matrix on a 4-torus, the edge loading along the second axis is not zero. The edge loading is a quadratic form, a sum over pairs of indices of the matrix entry times the displacement components: edgeLoad H d = Σᵢⱼ Hᵢⱼ dᵢ dⱼ. The witness uses the transverse-traceless projection of the matrix, the part that remains after removing gauge and trace components, and evaluates it on the unit displacement along axis 2. The theorem states this value is nonzero, and the proof is a direct computation from the definitions, with no gaps and no extra axioms.

The point of the witness is to show the transverse-traceless part is not vacuous on a plane-wave edge loading. A companion theorem, witness_tt_edge_ne_zero, extends the statement to the full plane-wave perturbation: the edge load times a cosine phase factor is also nonzero at the midpoint. Together they demonstrate that the transverse-traceless sector produces a genuine signal in this lattice setting, not a zero that would make the decomposition trivial. The proof chain relies on earlier results: the edge load of a symmetric matrix along an axis equals the diagonal entry, the transverse-traceless projection of a transverse-traceless matrix is itself, and the chosen witness matrix is transverse-traceless with respect to the chosen wave.

What the declaration does not claim is as important as what it proves. It does not establish that the full edge decomposition, the 4D Regge action, or the recovery of continuum Einstein-Hilbert gravity from this lattice works. Those targets remain open. It does not prove that the framework's action converges to general relativity in four dimensions. It does not claim that the edge loading is nonzero for every transverse-traceless matrix or every wave; the witness is one specific example. The gauge part of the decomposition, by contrast, has a separate exact identity relating it to a discrete Lie derivative, but that identity is not invoked here. The witness is a single, machine-checked data point in a larger campaign to understand how gravity might arise from a discrete ledger of recognition events.

theorem witness_edgeLoad_tt_ne_zero :
    edgeLoad (ttProject witnessWave witnessH) (axisDisp 2) ≠ 0 := by
  rw [witness_ttProject_eq, edgeLoad_axis]
  simp [witnessH, axisTTPlus]

theorem witness_tt_edge_ne_zero :
    planeWaveAxisEdgePert (ttProject witnessWave witnessH) witnessWave
        witnessBase 2 ≠ 0 := by
  unfold planeWaveAxisEdgePert
  rw [witness_ttProject_eq, edgeLoad_axis]
  simp [witnessH, witnessWave, witnessBase, axisTTPlus, axisMidpointPhase,
    axisWave, Real.cos_zero]

theorem edgeLoad_axis (H : Mat4) (a : Fin 4) :
    edgeLoad H (axisDisp a) = H a a := by
  unfold edgeLoad axisDisp
  simp [Finset.sum_ite_eq']

theorem ttProject_eq_of_isTT (m : Fin 4 → ℝ) (H : Mat4)
    (hTT : IsTT m H) (hm : momentumSq m ≠ 0) :
    ttProject m H = H := by
  unfold ttProject
  rw [gaugeCorrected_eq_of_isTT m H hTT hm,
    residualTrace_eq_zero_of_isTT m H hTT hm]
  simp

theorem witness_isTT : IsTT witnessWave witnessH :=
  axisTTPlus_isTT

What this page does not claim

The full 4D Regge action or continuum Einstein-Hilbert recovery is not proved by this witness. The edge loading is not shown to be nonzero for all transverse-traceless matrices or all plane waves. The witness does not establish convergence of the framework's action to general relativity in four dimensions.

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/Analysis/ReggeEdgeTTAttachment4D.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: