IndisputableMonolith.Gravity.Analysis.Regge4DContinuumPreflight

declarations in this module (68)

• abbrev Mat4 L78
• abbrev Wave4 L79
• def torusSide L84
• theorem torusSide_ge_three L86
• abbrev IntMode4 L90
• def realMode L93
• def waveNormSq L97
• theorem waveNormSq_eq_momentumSq L100
• def momentumNormSq L104
• theorem momentumNormSq_eq L107
• structure CanonicalFreudenthalTorus4D L122
• def frobeniusNormSq L133
• def IsTTPolarization4D L138
• def axisTTPlusNormalized L142
• theorem frobeniusNormSq_smul L145
• theorem frobeniusNormSq_axisTTPlus L155
• theorem inv_sqrt_two_sq L160
• lemma smul_preserves_transverse L163
• theorem frobeniusNormSq_axisTTPlusNormalized L175
• theorem axisTTPlusNormalized_isTT L181
• theorem axisTTPlusNormalized_isTTPolarization L190
• def axisTTCrossNormalized L195
• theorem frobeniusNormSq_axisTTCross L198
• theorem frobeniusNormSq_axisTTCrossNormalized L203
• theorem axisTTCrossNormalized_isTT L209
• theorem axisTTCrossNormalized_isTTPolarization L218
• def einsteinHilbertTTCoefficient4D L229
• def einsteinHilbertQuadratic4D L237
• theorem einsteinHilbertQuadratic4D_on_normalized L240
• theorem einsteinHilbertTTCoefficient4D_eq L247
• theorem kappa_einstein_ne_zero L250
• def pureGaugeFamily L256
• def FiniteSymbolSequence L262
• def finiteTransportedSymbol L269
• theorem finiteTransportedSymbol_eq L272
• def finiteTransportedSymbolSequence L278
• abbrev finiteExactReggeSymbol L283
• abbrev finiteExactReggeSymbolSequence L285
• abbrev exactFlatCrossTermFold L288
• theorem finiteExactReggeSymbol_eq L292
• def finiteExactMidpointBlochSymbol L299
• def finiteExactMidpointBlochSymbolSequence L303
• def discreteExactReggeContinuumFaceCoeff L309
• theorem discreteExactReggeContinuumFaceCoeff_eq L312
• def continuumEHScaleExplicitFace L318
• theorem continuumEHScaleExplicitFace_eq L321
• theorem discreteBookkeeping_recovers_frozen_EH L327
• theorem continuumEH_unitF_face_eq_frozen L336
• def Regge4DContinuumSymbolIs L347
• def Regge4DDiscreteBookkeepingContinuumSymbolIs L356
• theorem continuumSymbolIs_unique L365
• theorem continuumSymbolIs_iff L371
• def Regge4DContinuumEHTarget L384
• def Regge4DContinuumGaugeZeroTarget L392
• def S_RS_converges_EH_4d L399
• def edge_tt_decomposition L405
• theorem decoy_provisional_weight_fails_gauge L418
• theorem decoy_one_orbit_m2_is_not_continuum_target L428
• def wrongMeshPowerWeight L438
• def correctTorusDensityWeight L440
• theorem decoy_wrong_mesh_power_side3 L444
• theorem decoy_wrong_mesh_power L449
• def ArbitraryPullbackExcluded L467
• theorem decoy_arbitrary_pullback_excluded L470
• structure Regge4DContinuumPreflightStatus L475
• def regge4DContinuumPreflightStatus L487
• theorem regge4DContinuumPreflightStatus_flags L498
• theorem continuum_target_hypothesis_nonvacuous L513