minkowski_form
plain-language theorem explainer
Defines the flat Minkowski quadratic form s² = −t² + x² + y² + z² on ℝ^{1,3}. Every causal and continuum-limit argument in this module cites it as the reference interval. The body is a direct four-term polynomial; no proof obligations.
Claim. The Minkowski quadratic form on $\mathbb{R}^{1,3}$ is $s^2(t,x,y,z) = -t^2 + x^2 + y^2 + z^2$.
background
This module builds the zero-parameter bridge from discrete Recognition Science ledger sites to a Lorentzian continuum. The chain runs J-cost lattice → quadratic cost → Laplacian → Lorentzian interval → Minkowski flat limit → curved metric from defect → Einstein equations.
The Minkowski form is the first architectural step: the reference interval on $\mathbb{R}^{1,3}$ with signature $(-,+,+,+)$. Downstream predicates (timelike, spacelike, lightlike) are literally the sign of this form. Lorentzian signature itself is forced by tick/voxel asymmetry; $D=3$ spatial dimensions by DimensionForcing; $c=\ell_0/\tau_0$ by one voxel per tick.
Unlike the phenomenological ILG time-kernel, nothing here is fit to data. The form is the flat-space target that ADM with unit lapse and identity spatial metric must recover, and that weak-field defect perturbations must preserve as Lorentzian.
proof idea
Pure definition: the right-hand side is the four-term quadratic polynomial $-t^2+x^2+y^2+z^2$. No lemmas, tactics, or hypotheses. Homogeneity of degree 2 is recorded in the immediately following lemma via scaling.
why it matters
This is the reference interval for the entire continuum-emergence stack. Causal trichotomy classifies every displacement by the sign of the form; the three predicates is_timelike, is_spacelike, is_lightlike are thin wrappers around it. The light-cone speed limit and ContinuumLimitCert's Tier-1 signature fields (temporal negative, spatial positive) quote it directly.
On the gravity side, adm_is_minkowski proves that unit-lapse, identity-spatial ADM collapses exactly to this form, anchoring the flat limit before defect curvature and the Einstein equations. Framework landmarks: T8 ($D=3$), forced $c=1$ voxel/tick, and the zero-parameter gravity coupling from ZeroParameterGravity all sit on top of this interval as the Minkowski background.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.