module module high

`IndisputableMonolith.Gravity.ContinuumManifoldEmergence`

Module that equips the continuum limit of the RS lattice with Minkowski structure on R^{1,3}: the quadratic form s^2=-t^2+x^2+y^2+z^2, signature checks, causal trichotomy (timelike/spacelike/lightlike), and the light-cone speed limit. Gravity and continuum-limit workers cite it when lifting discrete J-cost dynamics to Lorentzian geometry. Definitions and elementary algebraic lemmas, not a deep existence proof.

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 ($s^2<0$), spacelike ($s^2>0$), or lightlike ($s^2=0$), with the light cone enforcing a universal speed limit. Signature is $(-+++)$ on the standard basis.

background

Recognition Science forces spatial dimension $D=3$ (DimensionForcing, T8) and a discrete cost landscape whose unique minimum is at the identity of the J-cost $J(x)=\frac12(x+x^{-1})-1$. In log coordinates this is the convex bowl $\cosh t-1$ (Cost.Convexity, T5). DiscretenessForcing records that the cost landscape itself forces a lattice rather than a continuum a priori.

ContinuumLimit (F-014) shows that long-wavelength discrete J-dynamics on $\mathbb{Z}^3$ produce a second-order diffusion equation matching Klein-Gordon structure. The present module supplies the Lorentzian target geometry for that limit: Minkowski space as the flat model manifold, with the standard causal partition and light-cone bound.

Constants supplies the RS time quantum $\tau_0=1$ tick; ZeroParameterGravity is the ambient gravity stack into which the continuum geometry is later wired.

proof idea

Definition-heavy module. The Minkowski form is introduced as an explicit quadratic form on $\mathbb{R}^4$; homogeneity and vanishing at the origin are immediate. Signature lemmas evaluate the form on the four standard basis vectors. Causal predicates (timelike, spacelike, lightlike) are definitional cuts on the sign of $s^2$, and trichotomy is a case split on that sign. The light-cone speed-limit statement is an elementary comparison of spatial and temporal components for null and timelike vectors. No deep analytic or measure-theoretic argument appears here.

why it matters in Recognition Science

Feeds UnifiedLatticeManifoldCorrespondence, which packages the deformed-cubic-lattice / curved-manifold correspondence: sequences of lattices whose Regge action and equations converge to the Einstein-Hilbert action and the EFE on a smooth Lorentzian $(M,g)$. Without a flat Minkowski model, signature, and causal cone, that correspondence has no continuum target.

In the forcing chain this sits downstream of T5 (J-uniqueness), T7 (eight-tick octave), and T8 ($D=3$), and alongside ContinuumLimit's discrete-to-PDE bridge. It is the geometric scaffold that lets zero-parameter gravity talk about continuum Lorentzian manifolds rather than only lattice defects.

scope and limits

Does not construct curved Lorentzian metrics or prove Einstein equations.
Does not derive the Minkowski form from J-cost; it posits the flat model.
Does not treat signature change, Euclidean sections, or complexification.
Does not prove continuum limit convergence; that lives in ContinuumLimit.
Does not address matter coupling or stress-energy on the manifold.

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