module module

`IndisputableMonolith.Foundation.JHessianGoldenMulti`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.CostProjectorGolden module_import

declarations in this module (16)

def innerForm L57
lemma innerForm_apply L64
def costHessianScalar L71
lemma costHessianScalar_pos L76
def costHessianForm L81
lemma costHessianForm_apply L84
def costHessianOperator L91
lemma costHessianForm_self L96
lemma costHessianForm_self_pos L104
lemma costHessianForm_self_ne_zero L113
theorem costHessianOperator_square L121
theorem costHessianOperator_normalized_isProjector L128
theorem costHessianOperator_goldenOperator_sq L138
theorem goldenScalar_forces_phi L150
structure JHessianGoldenMultiCertificate L162
theorem jHessianGoldenMultiCertificate L191