IndisputableMonolith.Gravity.UnifiedLatticeManifoldCorrespondence

declarations in this module (27)

• structure WeakFieldData L89
• theorem one_plus_h_pos L100
• theorem one_plus_h_lt_two L109
• structure LatticeRefinement L126
• def spacing L133
• theorem spacing_pos L135
• theorem spacing_ne_zero L140
• theorem spacing_eventually_small L144
• def prescribedEdgeLength L158
• theorem prescribedEdgeLength_pos L161
• theorem prescribedEdgeLength_sq L166
• theorem prescribedEdgeLength_flat L172
• theorem perBondActionDeviation L194
• theorem relativeActionDeviation L201
• theorem actionDeviation_tendsto_zero L207
• theorem discreteRegge_eq_neg_lattice_laplacian L219
• theorem latticeLaplacian_to_continuum L230
• theorem discreteRegge_to_linearizedEFE L245
• theorem reggeCoupling_eq_einsteinCoupling L254
• theorem einsteinCoupling_closed_form L260
• theorem reggeCoupling_pos L265
• theorem einsteinCoupling_pos L268
• structure UnifiedCorrespondenceCert L293
• theorem unifiedCorrespondence L344
• theorem exists_lattice_refinement_for_weak_field L389
• structure NonlinearUnifiedCert L409
• theorem nonlinearUnified_of_cms L425