IndisputableMonolith.Gravity.Analysis.ReggeNormalizationDerived4D

declarations in this module (32)

• abbrev Wave4 L58
• theorem frobSq_eq L62
• theorem momentumSq_eq L64
• def reggeFace L71
• def reggeNormalization L75
• theorem reggeFace_eq L77
• theorem reggeFace_eq_dictionary L88
• theorem regge_normalization_pinned L99
• theorem frobeniusNormSq_axisTTPlus L112
• theorem waveNormSq_axisWave L115
• theorem witness_nonzero L118
• theorem dictionary_witness_value L124
• theorem rho_one_fails L133
• theorem rho_pinned_at_witness L141
• theorem tetrahedron_deficit_sum L156
• theorem octahedron_deficit_sum L160
• def sphereEHIntegral L164
• theorem regge_constant_from_gauss_bonnet L167
• theorem gauss_bonnet_refutes_rho_one L174
• theorem phaseAverage_sin_sq L190
• def lagrangianDensityOfPhase L198
• theorem lagrangian_route_same_face L201
• theorem two_routes_differ_pointwise L210
• theorem discreteBookkeepingFactor_is_inverse_regge L231
• theorem frozen_preflight_is_the_eh_integral_face L241
• theorem exact_unit_coefficient_is_the_regge_face L252
• def NormalizationGateDischarged L270
• theorem normalizationGateDischarged L280
• def Step7Cert L289
• theorem step7Cert L299
• def typedResidual_arc2_normalization L310
• def typedResidual_naming_defect L321