IndisputableMonolith.Gravity.Analysis.ReggeTTSymbolPreflight

declarations in this module (55)

• abbrev EdgeField L175
• def flatEdgeField L179
• def tetSqEdgesOfField L184
• def tetDihedralAngleOfField L191
• def edgeAngleContributionOfField L199
• def deficitOfField L207
• def trueReggeAction L215
• theorem tetSqEdgesOfField_flat L222
• theorem edgeAngleContributionOfField_flat L233
• theorem deficitOfField_flatEdgeField L249
• theorem trueReggeAction_flatEdgeField L270
• def typedConformalEdgeField L288
• theorem periodicDispSqEdge_nonneg L293
• theorem canonical_tet_eq L298
• theorem canonical_tetVerts_eq L304
• theorem canonical_edgeInTet_eq L314
• theorem conformalTetSqEdges_eq_typedField L323
• theorem deficitAngle_conformal_eq L362
• theorem hingeMeasure_conformal_eq L382
• theorem reggeAction_conformal_eq L397
• theorem typedConformalEdgeField_zero L406
• theorem reggeAction_zeroPotential_eq_zero L414
• theorem frozen_identification L436
• theorem frozen_identification_stencil L464
• def vertCoord L485
• def polEdgeCoeff L493
• def commensurateMomentum L498
• def edgeMidpointPhase L503
• def planeWaveEdgeField L508
• def planeWaveActionProfile L516
• def ttSecondDifference L524
• def TTBlochSymbolIs L533
• def momentumNormSq L539
• instance instNeZeroAddThree L542
• def ReggeTTContinuumSymbolIs L552
• def IsTTPolarization L561
• def reggeTTContinuumCoefficient L571
• def ReggeTTContinuumIsotropyTarget L581
• theorem planeWaveEdgeField_zero_amplitude L589
• theorem planeWaveActionProfile_zero L597
• theorem ttSecondDifference_even L604
• theorem polEdgeCoeff_neg L612
• theorem planeWaveEdgeField_neg_polarization L622
• theorem ttSecondDifference_neg_polarization L634
• def axisWaveVector L651
• def axisTTPolarizationPlus L659
• def axisTTPolarizationCross L667
• theorem sqrt_two_mul_self L672
• theorem inv_sqrt_two_sq L675
• theorem axisTTPolarizationPlus_isTT L679
• theorem axisTTPolarizationCross_isTT L697
• theorem axisWaveVector_ne_zero L716
• structure ReggeTTSymbolPreflightStatus L734
• def reggeTTSymbolPreflightStatus L759
• theorem status_flags_grounded L771