module module

`IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianSymbol4D`

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

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.Analysis.Regge4DContinuumPreflight module_import
IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochM2Rayleigh4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianNormGate4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianSymbol4DAudit module_import
IndisputableMonolith.Gravity.Analysis.SRSConvergesEH4D module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ReggeBlochStarEdgeOriginsM2Eval4D module_import

declarations in this module (53)

structure ExactFlatHessianSymbol L100
def exactFlatHessianSymbol L105
theorem exactFlatHessianSymbol_not_fold L110
def einsteinHilbertTTCoefficient4D L117
theorem einsteinHilbertTTCoefficient4D_eq L119
def measuredTTNormCoeffN6 L126
theorem measuredTTNormCoeffN6_near_quarter L128
def measuredTTRelErrVsOracleN6 L133
theorem measuredTTRelErrVsOracleN6_lt_1e4 L135
def measuredGaugeBatteryPassN6 L140
theorem measuredGaugeBatteryPassN6_true L142
def measuredSameShellTTIsotropyN6 L147
theorem measuredSameShellTTIsotropyN6_true L149
def measuredSmallKAlphaSymbolDir L154
theorem measuredSmallKAlphaSymbolDir_near_quarter L156
def exactHessianM2UnitFrobeniusTTCoeff L169
theorem exactHessianM2UnitFrobeniusTTCoeff_eq L171
def exactHessianM2AxisTTPlusCoeff L175
theorem exactHessianM2AxisTTPlusCoeff_eq L177
theorem exactHessianM2AxisTTPlus_eq_EH L180
def exactHessianM2GaugeCoeff L185
theorem exactHessianM2GaugeCoeff_eq L187
theorem exactHessianM2_unitF_times_two_eq_axisTTPlus L192
def exactHessianM2IsotropicOnTT L200
theorem exactHessianM2IsotropicOnTT_true L202
def ExactHessianAlgebraicM2TablePresent L208
theorem exactHessianAlgebraicM2Table_absent L210
def exactHessianM2CUniqueValues L215
theorem exactHessianM2CUniqueValues_eq L217
def ExactHessianTTIsotropyTarget L228
theorem ExactHessianTTIsotropyTarget_closed L231
def ExactHessianGaugeZeroTarget L238
theorem ExactHessianGaugeZeroTarget_algebraic_face L241
def ExactHessianS_RS_converges_EH_4d L246
theorem ExactHessianS_RS_converges_EH_4d_closed L249
def ExactHessianNormalizationGatePass L254
theorem exactHessianNormalizationGatePass_true L256
theorem exact_unitFrobenius_ne_frozen_EH L259
theorem exactHessian_m2_div_identity L266
theorem exactHessian_m2_div_identity_punctured L272
def ExactHessianEdgeOriginsM2Banked L286
theorem ExactHessianEdgeOriginsM2Banked_closed L292
theorem exactHessian_m2_axisTTPlus_symbolDir L299
theorem exactHessian_m2_axisTTCross_symbolDir L304
theorem exactHessian_m2_decoyGauge_symbolDir L309
theorem exactHessian_m2_gaugeM1100E2_symbolDir L313
structure ExactHessianSymbolStatus L319
def exactHessianSymbolStatus L328
theorem exactHessianSymbolStatus_flags L337
theorem exact_hessian_algebraic_face_banked L348
theorem exact_hessian_srs_still_open L356
def ExactHessianResidualOpen L362
theorem exact_hessian_residual_open L367