minkowski_form_smul
plain-language theorem explainer
The Minkowski quadratic form on ℝ^{1,3} is homogeneous of degree two: scaling all four coordinates by a real factor c multiplies the form by c². Anyone building causal structure, light cones, or the flat-space limit from the discrete ledger cites this elementary scaling identity. The proof is a one-step unfold of the definition followed by ring normalization.
Claim. For all real numbers $c,t,x,y,z$, if $s^2(t,x,y,z) := -t^2 + x^2 + y^2 + z^2$ denotes the Minkowski quadratic form on $\mathbb{R}^{1,3}$, then $s^2(ct, cx, cy, cz) = c^2\, s^2(t,x,y,z)$.
background
This module builds the zero-parameter bridge from discrete Recognition Science ledger sites to a Lorentzian continuum: J-cost lattice to quadratic cost to Laplacian to Lorentzian interval, then Minkowski flat limit, then curved metric from defect and Einstein equations. Lorentzian signature is forced by tick/voxel asymmetry; the spatial metric by J''(1)=1; c by one voxel per tick; D=3 by DimensionForcing.
The Minkowski form is the basic quadratic form on ℝ^{1,3}: $s^2(t,x,y,z) = -t^2 + x^2 + y^2 + z^2$. Sibling lemmas establish its signature (temporal negative, spatial positive), the timelike/spacelike/lightlike trichotomy, and the light-cone speed limit. Homogeneity of degree two is the scaling law needed before those causal statements.
proof idea
One-line tactic proof: unfold the definition of the Minkowski form, then apply ring to normalize both sides of
$-(ct)^2+(cx)^2+(cy)^2+(cz)^2 = c^2(-t^2+x^2+y^2+z^2)$.
No external lemmas are required beyond the definition itself.
why it matters
Homogeneity is bookkeeping for the continuum-emergence chain: without degree-two scaling, the light-cone speed limit and causal trichotomy cannot be stated invariantly under coordinate rescaling of the flat Minkowski chart. The module architecture lists Minkowski form, Lorentzian signature, and causal structure as the first three proved blocks of the N→∞ bridge; this lemma sits under the form itself and underpins the flat-space limit claimed as unconditional.
It does not yet touch curvature, ADM decomposition, or the Einstein equations (later steps in the same module). Framework landmarks in view are T8 (D=3) and the forced c=ℓ₀/τ₀ from one voxel per tick; the form is the algebraic carrier of that signature. No downstream dependents are recorded yet; siblings such as causal trichotomy and light-cone speed limit are the natural consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.