Gravity Analysis Regge Edge Ttattachment4 D Plane Wave Axis Edge Pert Smul

Linearity of edge perturbations

In the framework's discrete model of gravity, the geometry of a 4-torus is studied through its edges, and a ledger (a discrete record of events) tracks how a perturbation on an edge responds to changes in the underlying matrix. The declaration planeWaveAxisEdgePert_smul proves a linearity property: if you scale the matrix by a real number c, the plane-wave edge perturbation scales by the same factor. In symbols, planeWaveAxisEdgePert (c • H) m x a = c * planeWaveAxisEdgePert H m x a. This is the discrete analogue of a familiar continuum fact: doubling the amplitude of a wave doubles its effect on the metric.

This is a formal theorem in the machine-checked library of the framework. It is proved for a specific construction: the perturbation is defined as the edge load (a quadratic form in the displacement) times a cosine phase, evaluated on an axis edge of the 4-torus. The proof unfolds the definition and uses the corresponding linearity of the edge load itself. The theorem is kernel-checked, with no unproved assumptions beyond the standard axioms of the ambient type theory.

In Recognition Science, this lemma is a small but necessary step in a larger campaign. The broader goal is to attach the algebraic decomposition of a 4x4 matrix into transverse-traceless, gauge, and residual parts to plane-wave perturbations on the lattice. This particular theorem establishes that the decomposition respects scaling, a property that must hold for the later steps to be consistent. It does not, by itself, prove the full decomposition, nor does it connect the discrete model to the continuum Einstein-Hilbert action.

What this declaration does not claim is as important as what it proves. It does not show that the discrete model converges to general relativity in the continuum limit. It does not establish that the edge decomposition is complete for all edge classes, only for the axis edges considered here. And it does not claim that the gauge part of the perturbation equals a specific continuum expression like δℓ² = 2 ∂_a ξ_a; the exact lattice identity is different and is proved separately.

theorem planeWaveAxisEdgePert_smul (c : ℝ) (H : Mat4) (m x : Fin 4 → ℝ)
    (a : Fin 4) :
    planeWaveAxisEdgePert (c • H) m x a =
      c * planeWaveAxisEdgePert H m x a := by
  unfold planeWaveAxisEdgePert
  rw [edgeLoad_smul, mul_assoc]

What this page does not claim

This does not prove that the discrete model converges to continuum general relativity. This does not establish the full 4D edge decomposition for all edge classes. This does not claim the gauge part equals the continuum expression δℓ² = 2 ∂_a ξ_a.

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: