IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D

declarations in this module (57)

• def maskOf L63
• def classBit L66
• def classDisp L70
• def classDispSq L74
• def classWeightNat L78
• theorem classWeightNat_pos L84
• theorem classDisp_ne_zero L87
• theorem classDispSq_eq_weight L108
• def classCoeff L118
• def classMidpointPhase L123
• def planeWaveClassPert L128
• theorem classCoeff_add L131
• theorem classCoeff_smul L135
• theorem classCoeff_neg L139
• theorem classCoeff_sub L143
• theorem planeWaveClassPert_add L147
• theorem planeWaveClassPert_smul L153
• def finiteTTBilinear L162
• def finiteTTQuadratic L169
• theorem finiteTTQuadratic_eq_bilinear L172
• theorem finiteTTBilinear_symm L177
• theorem finiteTTBilinear_add_left L182
• theorem finiteTTBilinear_smul_left L188
• theorem finiteTTQuadratic_add L194
• theorem finiteTTQuadratic_smul L208
• theorem finiteTTQuadratic_neg L217
• theorem classCoeff_gaugePart L224
• theorem finiteTTQuadratic_gaugePart L234
• def axisGaugeVector L245
• theorem classCoeff_gaugePart_axis L251
• def hasBit0 L267
• theorem sum_hasBit0 L269
• theorem finiteTTQuadratic_gaugePart_axisWave L273
• theorem finiteTTQuadratic_gaugePart_axisWave_ne_zero L287
• theorem classCoeff_axisTTPlus L294
• theorem classCoeff_axisTTCross L303
• def axisTTPlusSqNat L312
• theorem classCoeff_axisTTPlus_sq L315
• theorem sum_axisTTPlusSqNat L321
• theorem finiteTTQuadratic_axisTTPlus L325
• theorem finiteTTQuadratic_axisTTPlus_ne_zero L330
• theorem finiteTTQuadratic_axisTTPlus_isTT_seed L335
• def crossNat L343
• theorem sum_crossNat L349
• theorem finiteTTBilinear_axisTTPlus_gauge L353
• theorem finiteTTQuadratic_not_gauge_invariant_on_axisTTPlus L371
• def decoyGauge L382
• theorem finiteTTQuadratic_decoyGauge L384
• def decoyTrace L389
• theorem classCoeff_decoyTrace L391
• theorem classCoeff_decoyTrace_sq L397
• theorem sum_weightSqNat L401
• theorem finiteTTQuadratic_decoyTrace L405
• theorem decoy_values_distinct L414
• theorem classDisp_axis0 L424
• theorem classCoeff_axis0 L428
• theorem planeWaveClassPert_axis0 L433