module module

`IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHinge`

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

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

IndisputableMonolith.Gravity.SevenGaps.WickActionCertAssembly module_import
IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimit module_import
IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimitFamily module_import
IndisputableMonolith.Gravity.SevenGaps.WickActionEuclidSchlaefli module_import
IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHingeAudit module_import
IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHingeConfinement module_import

depends on (7)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.CampaignLedger module_import
IndisputableMonolith.Gravity.SevenGaps.CausalSimplex4D module_import
IndisputableMonolith.Gravity.SevenGaps.CausalSimplexWick module_import
IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger module_import
IndisputableMonolith.Gravity.SevenGaps.ThreePentCausalConsistency module_import
IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFirst module_import
IndisputableMonolith.Gravity.SevenGaps.WickFourOneAllHinges module_import

declarations in this module (26)

def carccos L106
def pentHingeCosPath L111
def dihedralSumPath L115
def hingeArea L120
def wickActionPath L123
def euclidCos L128
def lorentzCos L132
def lorentzRapidity L136
def lorentzAngleRe L140
def euclidArea L143
def euclidAngle L146
structure WickActionContinuationCert L157
def wick_action_continuation_4d L204
lemma offArccosCut_one_sub_sq_ne_zero L210
lemma im_one_sub_sq L222
lemma re_one_sub_sq L225
lemma carccos_log_arg_mul_conj L229
lemma re_sq_lt_one_of_abs_lt L242
theorem offArccosCut_slitPlane L248
lemma continuousAt_csqrt_of_mem_slitPlane L317
theorem continuousOn_carccos L323
lemma arccos_mem_Ioc_of_abs_lt_one L353
theorem carccos_real_eq_arccos L361
structure WickActionInteriorHingeStatus L393
def wickActionInteriorHingeStatus L411
theorem wickActionInteriorHingeStatus_flags L424