IndisputableMonolith.Masses.GenerationTorsionBridge

declarations in this module (43)

• def cubeGeometricTorsion L66
• lemma cubeGeoTorsion_first L71
• lemma cubeGeoTorsion_second L73
• lemma cubeGeoTorsion_third L75
• theorem cubeGeoTorsion_values L78
• theorem cubeGeoTorsion_eq_generationTorsion L90
• theorem cubeGeoTorsion_second_eq L103
• theorem cubeGeoTorsion_third_eq L109
• theorem cubeGeoTorsion_matches_tau_0 L117
• theorem cubeGeoTorsion_matches_tau_1 L122
• theorem cubeGeoTorsion_matches_tau_2 L127
• theorem second_gen_is_passive_edges L136
• theorem third_gen_is_Epass_plus_F L141
• theorem endogenous_matches_crystallographic L146
• theorem gen3_minus_gen2_is_faces L152
• structure CubeAdmissibleTorsion L166
• theorem cubeGeoTorsion_admissible L172
• theorem generationTorsion_admissible L178
• theorem cubeAdmissible_unique L183
• theorem cubeAdmissible_forces_canonical L196
• theorem cubeAdmissible_ordered L209
• def phiRatioConfig L223
• theorem phi_zpow_eq_one_iff L228
• def GroundStateCompatibleTorsion L262
• theorem groundStateCompatible_forces_ground_zero L267
• structure IncrementalCubeTorsion L289
• theorem cubeAdmissible_iff_incremental L297
• theorem cubeGeoTorsion_incremental L318
• theorem generationTorsion_incremental L322
• theorem incremental_forces_canonical L326
• def generationSlotCount L333
• theorem generationSlotCount_eq_three L336
• theorem generationSlotCount_eq_loopCount L340
• structure CubeGenerationFiltration L354
• theorem generationTorsion_has_cube_filtration L361
• theorem cubeFiltration_forces_canonical L368
• def canonicalLoopExcitation L376
• structure MinimalLoopExcitation L384
• theorem canonicalLoopExcitation_minimal L391
• theorem minimalLoopExcitation_unique L400
• theorem one_new_independent_loop_per_generation_step L420
• theorem minimalLoopExcitation_matches_generation_slots L427
• theorem rsLedger_torsion_from_cube L437