module module

`IndisputableMonolith.Geometry.FourTetSignedDeficit`

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

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

IndisputableMonolith.Gravity.Analysis.RecognitionMeshGeometricDeficit4D module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.CayleyMengerMatrix module_import
IndisputableMonolith.Geometry.CayleyMengerPolynomial module_import
IndisputableMonolith.Geometry.DihedralCayleyMenger module_import
IndisputableMonolith.Geometry.DihedralDerivatives module_import

declarations in this module (37)

def starSq L109
def starP L122
theorem star_cm3 L128
theorem fourTet_nondegenerate L143
def starMinor34Matrix L158
theorem det_starMinor34 L164
theorem star_minor_34_eq L171
theorem star_cofactor_34 L179
theorem star_minor_33_eq L186
theorem star_cofactor_33 L194
theorem star_minor_44_eq L200
theorem star_cofactor_44 L208
theorem star_denom L215
theorem fourTet_centralDihedralCosine L231
theorem fourTet_regular_sanity L239
theorem star_q L247
def starDeficit L257
theorem starDeficit_convention_note L266
theorem fourTet_deficit_eq L276
theorem starDeficit_eq_arcsin L282
theorem starDeficit_flat L288
theorem starDeficit_odd L294
theorem fourTet_deficit_sign L304
theorem arcsin_le_pi_div_two_mul L320
theorem abs_arcsin_le_abs L337
theorem starDeficit_abs_le L350
theorem star_mesh_bound L359
theorem fourTet_weak_pair L385
lemma is L432
theorem even_ledger_cannot_match_signed_regge L433
theorem even_cannot_match_starDeficit L452
structure FourTetSignedDeficitStatus L464
def status L474
theorem status_signed_deficit_kernel_checked L480
theorem status_weak_field_pair_constructed L483
theorem status_firewall_no_ledger_imports L486
theorem status_n5_torus_extension_closed L490