IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbol4D

declarations in this module (28)

• abbrev Mat4 L35
• abbrev Wave4 L36
• abbrev CouplingIdx L37
• def edgeStrain L41
• def couplingPhase L44
• def couplingWeight L47
• def couplingWeightIdx L50
• def couplingPhaseIdx L53
• def exactMidpointBlochSymbol L58
• def exactMidpointBlochM2 L63
• def exactMidpointBlochSymbolZero L68
• theorem couplingPhase_smul L81
• theorem couplingPhaseIdx_smul L87
• theorem couplingPhase_zero L93
• theorem couplingPhaseIdx_zero L98
• theorem exactMidpointBlochSymbol_zero_eq L103
• theorem sum_w_cos_sub_sum_w L109
• theorem centered_eq_irred L119
• theorem m2_eq_irred L129
• theorem tendsto_exactMidpointBloch_centered_div_sq L137
• theorem tendsto_exactMidpointBloch_m2_div L155
• structure ExactBlochSymbolStatus L170
• def exactBlochSymbolStatus L178
• theorem exactBlochSymbolStatus_flags L186
• theorem gate_passes_with_discrete_bookkeeping L195
• theorem gate_passes_under_restatement_C L204
• theorem abstract_centered_tendsto_available L211
• def typedResidual_exact_bloch_fin1208_specialize L218