IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidence4D

declarations in this module (36)

• abbrev Mat4 L43
• def orbitMeanLocalKernel L48
• theorem orbitMeanLocalKernel_t11 L51
• theorem orbitMeanLocalKernel_t11_eq_assembled_mean L56
• theorem orbitMeanLocalKernel_smul_star L61
• def transportedOrbitMeanLocal L66
• def slotOrbitMeanLocalKer L69
• theorem slotOrbitMeanLocalKer_eq_scaled L73
• def meanLocalSlotTerm L89
• theorem meanLocalSlotTerm_eq_scaled L96
• def blochFoldOrbitMeanLocal L123
• theorem blochFoldOrbitMeanLocal_eq_scaled L127
• def blochFoldAllMeanLocal L135
• theorem blochFoldAllMeanLocal_eq_distinctHinge L138
• def m2MeanLocalOrbitSlotCoeff L146
• theorem m2MeanLocalOrbitSlotCoeff_eq_scaled L156
• def m2MeanLocalOrbitMoment L187
• theorem m2MeanLocalOrbitMoment_eq_scaled L191
• def m2MeanLocalAllOrbitMoment L198
• theorem m2MeanLocalAllOrbitMoment_eq_distinctHinge L201
• theorem m2MeanLocalAllOrbitMoment_smul L209
• def cubeTranslateOffset L219
• def t11MemberOffset L228
• def addBase L234
• def transportedT11Member L237
• def permOffset L242
• def phasedT11PositionResolved L247
• def t11PositionResolvedSlotTerm L256
• theorem t11_member_sum_eq_fullStar L264
• def Regge4DPathBPositionResolvedClosesEH L275
• theorem Regge4DPathBPositionResolvedClosesEH_status_open L278
• theorem meanLocal_inherits_distinctHinge_on_any L284
• structure ReggeBlochLocalIncidence4DStatus L290
• def reggeBlochLocalIncidence4DStatus L296
• theorem reggeBlochLocalIncidence4DStatus_flags L302
• theorem does_not_flip_gap_action_recovery L309