Pith. sign in
module module moderate

IndisputableMonolith.Gravity.NullConeQuadraticTensorClassAudit

show as:
view Lean formalization →

Audit surface for the null-cone quadratic tensor class: values of a symmetric quadratic form on all Minkowski-null covectors fix the form modulo a multiple of the Minkowski metric. Gravity workers cite it when checking the Phase 5 algebraic prerequisite before geometric tensor work. The module is a thin import-and-audit shell over the finite-dimensional linear-algebra package.

claimAudit of the rigidity statement: if $Q$ is a symmetric bilinear form on $\mathbb{R}^{1,3}$ and the values $Q(k,k)$ are known for every Minkowski-null covector $k$ (i.e.\ $\eta(k,k)=0$ with $\eta=\mathrm{diag}(-1,1,1,1)$), then $Q$ is determined up to $Q \mapsto Q + \lambda\eta$ for $\lambda\in\mathbb{R}$.

background

Phase 5 of the gravity stack needs an algebraic rigidity fact before any geometric Einstein-tensor identification. The imported package states that a real symmetric quadratic form on Minkowski space is fixed, modulo scalar multiples of the metric $\eta=\mathrm{diag}(-1,1,1,1)$, by its restriction to the null cone: knowing $Q(k,k)$ for every null covector $k$ determines $Q$ up to $Q+\lambda\eta$.

That package is explicitly finite-dimensional real linear algebra. It is not yet the independently geometric tensor $G$ required by Phase 5; the upstream module doc marks it as a Tier-A algebraic prerequisite and notes that the geometric step remains separate.

This audit module sits in the Gravity domain and imports only that class module, exposing the null-cone rigidity claim for checklist and dependency review.

proof idea

Definition and audit shell, not a new proof module. It imports NullConeQuadraticTensorClass and surfaces the existing finite-dimensional rigidity package (symmetric forms on null covectors determine the matrix modulo $\eta$) for Phase 5 review. No independent tactic script or term proof lives here; argument structure is inherited from the imported algebraic package.

why it matters in Recognition Science

Phase 5 needs a clean algebraic gate before geometric identification of the gravitational tensor. The audited package supplies that gate: null-cone values fix a symmetric form modulo multiples of $\eta$. Downstream geometric work can then treat the residual $\lambda\eta$ ambiguity separately rather than re-proving linear-algebra rigidity inline.

No further modules currently list this audit as a hard dependency in the supplied graph, so its role is checklist and import hygiene inside Gravity. It keeps the Tier-A algebraic prerequisite visible and separable from the still-open geometric $G$ step flagged in the upstream module documentation.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.