module module

`IndisputableMonolith.Gravity.Analysis.ReggeTTSymbolSpecificationAudit`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ReggeTTSymbolPreflight module_import

declarations in this module (14)

theorem polEdgeCoeff_mul_left L71
theorem smul_polarization_apply L81
theorem polEdgeCoeff_smul L85
theorem planeWaveEdgeField_smul L97
theorem planeWaveActionProfile_smul L106
theorem ttSecondDifference_smul L119
theorem tendsto_const_mul_punctured L132
theorem TTBlochSymbolIs_smul_of L145
theorem TTBlochSymbolIs_smul L161
def frobeniusSq L179
theorem isTTPolarization_frobenius_pinned L184
theorem frobeniusSq_smul L190
theorem isTTPolarization_smul_iff L204
theorem reggeTT_target_scaling_wellPosed L256