structure
definition
def or abbrev
ExtendedObject
show as:
view Lean formalization →
formal statement (Lean)
38structure ExtendedObject where
39 h_cm : Position
40 extent : ℝ
41 extent_pos : extent > 0
42
43/-! ## Frame Dependent Refresh Rate -/
44
45/-- Total Potential in a frame accelerating with `a` at position `h` (relative to CM).
46 Φ_tot(z) ≈ Φ_grav(h_cm + z) + a * z
47 (Linear approximation for local frame)
48-/
used by (28)
-
acoustic_levitation -
anti_coherence_reduces_coupling -
antiGravField_cancels -
any_source_suffices -
baseline_gravitational_coupling -
complete_cancellation_is_levitation -
concrete_levitation -
effective_gravitational_coupling -
equilibrium_acceleration -
equilibrium_is_coherent -
FullLevitationCert -
levitation_field_exists -
LevitationInevitability -
modified_coherence_defect -
modified_coherence_defect_expand -
modified_coherence_defect_simplify -
modified_falling_condition -
modified_total_potential -
partial_weight_reduction -
UnconditionalLevitationCert -
weight_reduction_factor -
coherence_defect -
coherence_defect_expand -
coherence_defect_simplify -
falling_restores_coherence -
total_potential_in_frame -
coherence_defect_of_combined -
SuperpositionJustification