`PhaseFieldSource`

definition

show as: view math explainer →

module: IndisputableMonolith.Gravity.AcousticPhaseLevitation
domain: Gravity
line: 261 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Gravity.AcousticPhaseLevitation on GitHub at line 261.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 258/-- Classification of external phase field generation mechanisms.
 259    All three historical sources involve rotation + phase coherence,
 260    which in RS terms generates the required ∇Φ_ext. -/
 261inductive PhaseFieldSource where
 262  | acoustic_standing_wave    -- classical acoustic radiation pressure
 263  | rotating_superconductor   -- Podkletnov / Li: SC phase coherence + rotation
 264  | rotating_magnetic_array   -- Searl: magnetic phase-locked rotation
 265  deriving DecidableEq, Repr
 266
 267/-- Any phase field source that generates an ExternalPhaseField with
 268    ∇Φ_ext opposing ∇Φ_grav produces a levitation effect. -/
 269theorem any_source_suffices
 270    (_source : PhaseFieldSource) (field : ProcessingField)
 271    (ext : ExternalPhaseField) (obj : ExtendedObject)
 272    (h_cancel : deriv ext.psi obj.h_cm = -(deriv field.phi obj.h_cm)) :
 273    modified_coherence_defect field ext obj 0 = 0 :=
 274  acoustic_levitation field ext obj h_cancel
 275
 276/-! ## 7. Partial Levitation and Weight Reduction -/
 277
 278/-- Weight reduction factor: ratio of effective to baseline coupling.
 279    0 = full levitation, 1 = no effect. -/
 280def weight_reduction_factor
 281    (field : ProcessingField) (ext : ExternalPhaseField) (obj : ExtendedObject)
 282    (_h_baseline_ne : baseline_gravitational_coupling field obj ≠ 0) : ℝ :=
 283  effective_gravitational_coupling field ext obj / baseline_gravitational_coupling field obj
 284
 285/-- Partial anti-coherence gives partial weight reduction (value in [0,1]). -/
 286theorem partial_weight_reduction
 287    (field : ProcessingField) (ext : ExternalPhaseField) (obj : ExtendedObject)
 288    (g : ℝ) (hg : deriv field.phi obj.h_cm = g) (hg_pos : g > 0)
 289    (e : ℝ) (he : deriv ext.psi obj.h_cm = e) (he_neg : e ≤ 0) (he_bound : -e ≤ g) :
 290    weight_reduction_factor field ext obj (by
 291      unfold baseline_gravitational_coupling; rw [hg]; exact ne_of_gt (abs_pos.mpr (ne_of_gt hg_pos)))

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.