module module high

`IndisputableMonolith.Gravity.ContinuumManifoldEmergence`

Defines the Minkowski quadratic form on R^{1,3} and the causal trichotomy (timelike, spacelike, lightlike) used when discrete RS gravity is matched to a continuum Lorentzian manifold. Gravity and continuum-limit workers cite it to fix signature, cones, and the light-cone speed bound before Regge or Einstein matching. Content is definitional plus short algebraic lemmas on scaling, zeros, and signature components.

claimOn $\mathbb{R}^{1,3}$, the Minkowski quadratic form is $s^2(t,x,y,z)=-t^2+x^2+y^2+z^2$. Vectors are classified as timelike, spacelike, or lightlike by the sign of $s^2$, the three cases are exhaustive and mutually exclusive, and the light cone enforces a finite propagation-speed bound.

background

Recognition Science builds continuum physics from discrete J-cost dynamics on a lattice. The cost $J(x)=\frac12(x+x^{-1})-1$ (equivalently $J(e^t)=\cosh t-1$) is strictly convex with a unique minimum at the identity; DiscretenessForcing records that this bowl forces discrete structure, while ContinuumLimit shows long-wavelength lattice dynamics recover a second-order wave/diffusion equation of Klein-Gordon type. DimensionForcing supplies the companion fact that spatial dimension $D=3$ is forced (linking and related arguments), so the natural continuum arena is four-dimensional spacetime rather than an arbitrary $D+1$.

This gravity module sits on that foundation and on ZeroParameterGravity. It fixes the standard Lorentzian quadratic form on $\mathbb{R}^{1,3}$ and the elementary causal vocabulary (temporal vs spatial signature components, timelike/spacelike/lightlike predicates, trichotomy, light-cone speed limit) needed before one can speak of continuum manifolds, cones, or Regge-to-Einstein limits.

proof idea

Definition-first module, not a deep existence proof. It introduces the Minkowski form as a quadratic function on four real coordinates, then records scaling and zero identities by direct expansion. Signature lemmas evaluate the form on the standard basis vectors. Causal predicates are sign conditions on that form; trichotomy is a case split on the sign of $s^2$. The light-cone speed-limit statement is an elementary consequence of the null cone of the same quadratic form. No heavy tactics or external analytic machinery beyond algebra on $\mathbb{R}$.

why it matters in Recognition Science

Continuum manifold language is a prerequisite for the deformed-cubic-lattice / curved-manifold correspondence packaged in UnifiedLatticeManifoldCorrespondence: given a smooth Lorentzian $(M,g)$, one wants lattices whose Regge action and equations converge to the Einstein-Hilbert action and EFE. That program needs a fixed Minkowski signature, causal cones, and a finite signal speed before curvature, edge lengths, or dihedral data are introduced.

In the broader RS chain the module bridges Foundation continuum and dimension results (smooth long-wavelength limit; $D=3$) into the Gravity domain, so zero-parameter gravitational claims can be stated against a Lorentzian continuum rather than only a discrete ledger. It does not itself derive Einstein equations; it standardizes the geometric background those later correspondences assume.

scope and limits

Does not derive the Einstein field equations or a full continuum action principle.
Does not construct curved metrics; only the flat Minkowski form on R^{1,3}.
Does not prove D=3 or discreteness; those are imported from Foundation modules.
Does not treat matter coupling, horizons, or global causal structure beyond local cones.
Does not supply Regge calculus or lattice-to-manifold convergence proofs.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.UnifiedLatticeManifoldCorrespondence module_import

depends on (7)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Cost.Convexity module_import
IndisputableMonolith.Foundation.ContinuumLimit module_import
IndisputableMonolith.Foundation.DimensionForcing module_import
IndisputableMonolith.Foundation.DiscretenessForcing module_import
IndisputableMonolith.Gravity.ZeroParameterGravity module_import

declarations in this module (43)

def minkowski_form L82
theorem minkowski_form_smul L85
theorem minkowski_form_zero L90
theorem signature_temporal L100
theorem signature_spatial_x L105
theorem signature_spatial_y L110
theorem signature_spatial_z L115
def is_timelike L125
def is_spacelike L128
def is_lightlike L131
theorem causal_trichotomy L135
theorem light_cone_speed_limit L145
theorem timelike_iff L151
theorem spacelike_iff L157
theorem null_ray_x L162
theorem null_ray_diagonal L166
structure FiniteLattice L178
theorem spacing_monotone L206
theorem resolution_achievable L214
def physical_interval L234
theorem physical_interval_expand L237
theorem physical_interval_temporal L243
theorem physical_interval_spatial L249
theorem jcost_is_euclidean_metric L266
theorem metric_normalization L272
theorem spatial_isotropy L277
theorem jcost_neighbor_is_laplacian L281
theorem laplacian_convergence_N L302
theorem laplacian_error_identity L313
def adm_interval L332
theorem adm_is_minkowski L337
theorem adm_temporal_timelike L343
theorem adm_spatial_spacelike L350
def weak_field_interval L370
theorem weak_field_flat_limit L374
theorem weak_field_coupling L379
theorem weak_field_correction_bound L384
theorem weak_field_temporal_negative L403
theorem weak_field_spatial_positive L411
theorem spatial_dim_is_3 L424
theorem spacetime_dim L426
structure ContinuumLimitCert L433
theorem continuum_limit_certificate L482