IndisputableMonolith.Gravity.Analysis.Regge4DFlatSecondVariation

declarations in this module (30)

• abbrev Mat4 L77
• theorem flat_freudenthal_schlaefli_present L81
• theorem flat_freudenthal_schlaefli_identity L85
• theorem flat_freudenthal_directional_schlaefli_present L89
• theorem flat_freudenthal_directional_schlaefli L94
• theorem flat_freudenthal_seed_angle_hasDerivAt L98
• def schlaefliCandidateZeroMom L107
• def schlaefliCandidateFold L114
• theorem schlaefliCandidateZeroMom_eq L117
• theorem schlaefliCandidateFold_eq L121
• theorem schlaefliCandidate_vanishes_on_axisTTPlus L125
• theorem schlaefliCandidate_vanishes_on_decoyGauge L129
• theorem Freudenthal4SimplexPathwiseSchlaefli_absent L158
• theorem schlaefliN_interface_ready L165
• abbrev NonlinearFlatSecondVariation4D L173
• def Regge4DSchlafliElevationToCandidate L186
• def Regge4DSchlafliFiniteMomentumOpen L194
• def Regge4DSchlafliBridgeOpen L197
• theorem elevation_iff_torus_open L201
• theorem candidate_m2_axisTTPlus_symbolDir L219
• theorem candidate_continuumFace_normalizedTT_symbolDir L225
• theorem eh_target_neg_quarter L232
• theorem candidate_face_ne_eh L239
• def SchlaefliElevationToCandidateClosesEH L251
• theorem schlaefli_elevation_to_candidate_misses_eh_face L255
• def Regge4DSchlafliSecondVariation L261
• structure Regge4DFlatSecondVariationStatus L266
• def regge4DFlatSecondVariationStatus L275
• theorem regge4DFlatSecondVariationStatus_flags L284
• theorem schlafli_does_not_flip_gap L298