IndisputableMonolith.Gravity.SevenGaps.DynamicStructureFunctionBlocker

declarations in this module (20)

• def PhaseSpaceConstant L44
• def FixedBackgroundRepresents L49
• theorem fixed_background_represents_only_constant L55
• theorem exists_fixed_background_iff_phaseSpaceConstant L65
• def concreteDynamicInverseMetric L82
• def zeroPhasePoint L86
• def unitConfigurationPoint L90
• theorem concreteDynamicInverseMetric_pos L94
• theorem concreteDynamicInverseMetric_witness L102
• theorem concreteDynamicInverseMetric_not_constant L109
• theorem no_fixed_background_represents_concrete L119
• def HamWHasBackgroundStructureFunction L130
• theorem HamW_has_background_structure_function L138
• def BackgroundWeightedContinuumReach L143
• theorem background_weighted_continuum_reach L155
• structure PhaseSpaceDependentHamiltonianConstruction L170
• def backgroundHamiltonianConstruction L184
• def PhaseSpaceDependentDiracPremise L195
• def Gap5DynamicDiracAndHKTRigidityTarget L203
• theorem gap5_background_weight_blocker L210