IndisputableMonolith.Gravity.SevenGaps.Gap6LookalikeReceipt

declarations in this module (28)

• theorem simplex3d_vertex_card_ne_4d L59
• theorem simplex3d_edge_card_ne_4d L64
• theorem lorentzian_continuation_3d_banked L70
• def LorentzianContinuation3DNotAction4DCertificate L79
• theorem lorentzianContinuation3DNotAction4DCertificate L87
• theorem lorentzian_continuation_4d_kinematical_banked L94
• def LorentzianContinuation4DKinematicalNotActionCertificate L105
• theorem lorentzianContinuation4DKinematicalNotActionCertificate L111
• def HingeDataNotActionLevelCertificate L124
• theorem hingeDataNotActionLevelCertificate L138
• def Cm4SignNotActionLevelCertificate L149
• theorem cm4SignNotActionLevelCertificate L156
• def BranchRegularOnNotDeficitSumCertificate L164
• theorem branchRegularOnNotDeficitSumCertificate L181
• theorem interior_hinge_needs_three_pents_banked L188
• theorem two_pent_interior_impossible L195
• def TwoPentNotInteriorActionCertificate L200
• theorem twoPentNotInteriorActionCertificate L205
• def EHRecoveryNotGap6Certificate L216
• theorem ehRecoveryNotGap6Certificate L222
• def Gap6LedgerTerminalGuard L231
• theorem gap6LedgerTerminalGuard L238
• def TypedResidual_gap6_lookalike_decoys_fail L245
• theorem typedResidual_gap6_lookalike_decoys_fail L256
• theorem TypedResidual_gap6_lookalike_decoys_fail_closed L267
• structure Gap6LookalikeReceiptStatus L273
• def gap6LookalikeReceiptStatus L285
• theorem gap6LookalikeReceiptStatus_flags L293