IndisputableMonolith.Gravity.Analysis.Regge4DTransportedAlgebraicCloser

declarations in this module (31)

• abbrev Mat4 L65
• theorem finiteTransportedSymbol_eq_blochFoldAllDistinctHinge L71
• theorem finiteTransportedSymbol_eq_blochFoldAll L78
• theorem continuumSymbolIs_unique_limit L84
• theorem finiteTransportedSymbol_eq_orbit_sum L89
• def finiteTransportedT11Symbol L99
• theorem finiteTransportedT11Symbol_eq L102
• theorem finiteTransportedSymbol_smul L109
• theorem finiteTransportedSymbol_zero L116
• theorem t11_foldAlong_m2_tendsto_axisTTPlus L123
• theorem t11_foldAlong_m2_tendsto_decoyGauge L128
• theorem t11_m2Symbol_axisTTPlus L132
• theorem t11_m2Symbol_decoyGauge L136
• def symbolDirIntMode L141
• theorem symbolDir_normSq L144
• theorem realMode_symbolDirIntMode L149
• def oneOrbitRayNormalizedCoeff L158
• theorem oneOrbitRayNormalizedCoeff_axisTTPlus L161
• theorem oneOrbit_ray_normalized_ne_eh_coefficient L166
• theorem oneOrbit_m2_ne_eh_coefficient L172
• def Regge4DTransportedTTIsotropyOpen L181
• def Regge4DTransportedGaugeZeroOpen L185
• def Regge4DTransportedAreaMatchOpen L189
• theorem Regge4DTransportedAreaMatchOpen_holds L192
• theorem blochFoldOrbit_t11_eq_blochFold11 L197
• def Regge4DTransportedAlgebraicCloserTarget L202
• theorem transported_targets_eq_preflight L205
• structure Regge4DTransportedAlgebraicCloserStatus L212
• def regge4DTransportedAlgebraicCloserStatus L226
• theorem regge4DTransportedAlgebraicCloserStatus_flags L238
• theorem banked_does_not_inhabit_eh_or_flip_gap L260