IndisputableMonolith.Gravity.AcousticPhaseLevitation

declarations in this module (29)

• structure ExternalPhaseField L63
• def modified_total_potential L76
• def modified_coherence_defect L85
• lemma modified_coherence_defect_expand L93
• lemma modified_coherence_defect_simplify L106
• theorem modified_falling_condition L123
• theorem acoustic_levitation L152
• def equilibrium_acceleration L160
• theorem equilibrium_is_coherent L165
• def effective_gravitational_coupling L179
• def baseline_gravitational_coupling L184
• theorem anti_coherence_reduces_coupling L193
• theorem complete_cancellation_is_levitation L209
• structure LevitationInevitability L220
• theorem levitation_is_inevitable L250
• inductive PhaseFieldSource L261
• theorem any_source_suffices L269
• def weight_reduction_factor L280
• theorem partial_weight_reduction L286
• structure ForcingChainToLevitation L314
• theorem forcing_chain_complete L329
• structure UnconditionalLevitationCert L366
• theorem levitation_unconditional L395
• def antiGravField L419
• theorem antiGravField_cancels L424
• theorem concrete_levitation L435
• theorem levitation_field_exists L442
• structure FullLevitationCert L458
• theorem full_levitation_cert L465