IndisputableMonolith.Papers.DraftV1

declarations in this module (28)

• theorem injectivity_of_observable_map L36
• theorem refinement L43
• def syncPeriod L55
• lemma syncPeriod_def L57
• theorem syncPeriod_eq_mul L61
• theorem synchronization_selection_principle L71
• theorem syncPeriod_3_eq_360 L119
• theorem sync_resource_functional_minimized L128
• def apsidalAngle L148
• theorem kepler_selection_principle L153
• def ConstraintS L207
• def ConstraintK L211
• theorem constraintS_forces_D3 L216
• theorem constraintS_iff_D3 L223
• def AlexanderDualityForCircleHypothesis L245
• def LinkingInvariantHypothesis L250
• def RGConditionsForDualityHypothesis L258
• theorem rg_conditions_for_duality L260
• def CentralPotentialDerivationHypothesis L265
• theorem rg_derivation_of_central_potentials L267
• def RobustnessHypothesis L272
• theorem robustness_of_D3_signature L274
• def AlexanderDualityApplies L279
• def LinkingSelectionPrincipleHypothesis L286
• theorem linking_selection_principle L289
• theorem dimensional_rigidity_main L298
• theorem dimensional_rigidity_full_forward L309
• theorem no_higher_dimensional_alternative L317