IndisputableMonolith.Unification.SpacetimeEmergence

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