IndisputableMonolith.Masses.TorsionForcing

declarations in this module (38)

• theorem hamiltonian_cycle_on_Q3 L89
• theorem cycle_period_eq_vertices L94
• def passiveAtLevel L111
• theorem passiveAtLevel_0 L117
• theorem passiveAtLevel_1 L118
• theorem passiveAtLevel_2 L119
• theorem passiveAtLevel_3 L120
• theorem passiveAtLevel_matches_passiveCoupling L123
• theorem rcl_additive_torsion L139
• theorem rcl_jcost_of_sum L144
• theorem jcost_ground L149
• theorem jcost_positive_of_nonzero L153
• structure CouplingProfile L173
• def CWPrerequisite L188
• theorem face_has_edge_boundary L195
• def all_profiles L204
• theorem all_profiles_complete L207
• theorem cw_prerequisite_forces_three L215
• theorem faces_without_edges_violates_cw L222
• def profileTorsion L235
• theorem profileTorsion_ground L239
• theorem profileTorsion_edges L242
• theorem profileTorsion_edges_faces L246
• theorem admissible_torsion_values L252
• theorem six_is_not_admissible L263
• def RCLForcedTorsion L283
• theorem generationTorsion_is_rcl_forced L292
• theorem rcl_forced_torsion_unique L318
• theorem rcl_forced_torsion_exists_unique L337
• theorem rcl_forced_implies_cubeAdmissible L349
• theorem rcl_forced_implies_incremental L356
• theorem rcl_forced_implies_filtration L363
• theorem cw_prerequisite_is_essential L372
• theorem forced_torsion_ordered L382
• theorem forced_jcost_ordering L385
• theorem rsLedger_torsion_from_rcl L400
• structure TorsionForcingCert L434
• theorem torsion_forcing_certificate L448