IndisputableMonolith.Gravity.ContinuumManifoldEmergence

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