module module

`IndisputableMonolith.Geometry.FreudenthalReggeComponent`

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 (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.CayleyMenger module_import
IndisputableMonolith.Geometry.DihedralAngle module_import
IndisputableMonolith.Gravity.WeakFieldConformalRegge module_import

declarations in this module (21)

abbrev LocalVertex L51
structure ConcreteReggeStar L55
def regularTriangleArea L64
theorem regularTriangleArea_nonneg L67
theorem regularTriangleArea_pos L72
def regularTetrahedralDihedralAngle L80
theorem regularTetrahedralDihedralAngle_eq L83
theorem hasDerivAt_regularTriangleArea L87
theorem hasDerivAt_regularDihedral_uniformScale L104
def regularLocalStar L112
def areaWeight L120
theorem areaWeight_symm L123
theorem areaWeight_nonneg L133
def concreteWeakFieldReggeData L142
def concreteM L146
theorem concreteM_offDiag_eq_neg_areaWeight L151
theorem concreteM_rowSum_zero L160
def concreteReggeComponentComparison L168
theorem concreteReggeSecondVariation_eq_jcostDirichlet L176
structure FreudenthalReggeComponentCert L188
theorem freudenthalReggeComponentCert L201