module module high

`IndisputableMonolith.Unification.SpacetimeEmergence`

This module assembles the emergence of 4D spacetime with one temporal dimension and three spatial dimensions from the J-cost and phi-ladder structure. Researchers tracing the forcing chain from a single distinction to physical spacetime would cite it. The module collects explicit equalities and signature results by importing and combining dimension forcing, phi forcing, and octave duality lemmas.

claimTemporal dimension equals 1 (octave advance); spatial dimension equals 3; spacetime dimension equals 4 with Lorentzian signature induced by the 8-tick cycle.

background

The module operates in the Unification domain and imports Constants (tau_0 equals 1 tick), Cost, DimensionForcing (D equals 3 forced by topological and self-similar arguments), PhiForcing (phi forced as self-similar fixed point in discrete ledger with J-cost), ZeroParameterGravity (gravity as curvature from defect distributions), QuantumGravityOctaveDuality (kappa_einstein * hbar equals 8 from the 8-tick cycle), and YangMillsMassGap. It uses the Recognition Composition Law and the eight-tick octave (T7) to fix time as the canonical orbit advance.

proof idea

This is a definition module that states dimension equalities and assembles upstream lemmas; no internal proofs are supplied beyond the imported results on D equals 3 and the octave lock.

why it matters in Recognition Science

The module supplies the spacetime dimension and signature facts required by the master forcing-chain theorem in RealityFromDistinction, which derives the full chain from existence of one distinction on an inhabited carrier K to light cone, time orbit, and phi-derived constants. It closes the T7-T8 segment of the forcing chain (T0 to T8) by fixing D equals 3 and temporal advance equals 1.

scope and limits

Does not derive the metric from the J-cost functional beyond octave counting.
Does not address extensions to higher or variable dimensions.
Does not compute explicit curvature or defect dynamics.
Does not link to mass ladder or alpha band results.

used by (1)

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

IndisputableMonolith.Foundation.RealityFromDistinction module_import

depends on (7)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.DimensionForcing module_import
IndisputableMonolith.Foundation.PhiForcing module_import
IndisputableMonolith.Gravity.ZeroParameterGravity module_import
IndisputableMonolith.Unification.QuantumGravityOctaveDuality module_import
IndisputableMonolith.Unification.YangMillsMassGap module_import

declarations in this module (46)

def temporal_dim L62
def spatial_dim L65
def spacetime_dim L68
theorem spacetime_dim_eq_four L71
theorem octave_matches_spatial L75
theorem Jcost_near_identity L81
theorem spatial_cost_positive L87
theorem spatial_metric_at_identity L94
theorem negative_eigenvalue_count L146
theorem positive_eigenvalue_count L153
theorem lorentzian_signature L162
theorem lorentzian_from_det L176
abbrev Displacement L182
def interval L185
def spatial_norm_sq L188
def temporal_sq L192
theorem interval_eq_spatial_minus_temporal L195
theorem lightlike_iff_speed_c L202
theorem timelike_iff_subluminal L207
theorem spacelike_iff_superluminal L212
theorem pure_temporal_is_timelike L219
theorem pure_spatial_is_spacelike L229
theorem equal_displacement_is_lightlike L239
def proper_time_sq L251
theorem proper_time_sq_eq_neg_interval L254
theorem proper_time_sq_pos_of_timelike L259
def velocity_sq L264
theorem proper_time_from_velocity L268
theorem timelike_iff_subluminal_velocity L278
theorem energy_momentum_relation L294
theorem rest_energy_is_mass L299
theorem massless_at_speed_c L303
theorem minimum_rest_mass_is_gap L308
theorem arrow_of_time L315
theorem not_euclidean L321
theorem not_split_signature L322
theorem not_three_temporal L323
theorem not_1_2_signature L324
theorem not_1_4_signature L325
theorem signature_unique L328
theorem mass_gap_is_spatial_minimum L337
theorem mass_gap_from_phi L341
theorem mass_gap_bounds L344
structure SpacetimeEmergenceCert L353
theorem spacetime_emergence_cert L374
theorem spacetime_emergence_cert_nonempty L390