ExtendedObject

formal source

  35  /-- Potential function Φ(h) -/
  36  phi : Position → ℝ
  37
  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-/
  49def total_potential_in_frame (field : ProcessingField) (obj : ExtendedObject) (a : ℝ) (z : ℝ) : ℝ :=
  50  -- Taylor expand phi around h_cm: phi(h_cm) + phi'(h_cm) * z
  51  let phi_grav := field.phi obj.h_cm + (deriv field.phi obj.h_cm) * z
  52  -- Inertial potential from acceleration a (pointing up? a is vertical acceleration)
  53  -- If object accelerates down (a < 0), inertial force is up.
  54  -- Potential Φ_acc such that F = -∇Φ_acc. F_inertial = -a, hence Φ_acc = a * z.
  55  let phi_acc := a * z
  56
  57  phi_grav + phi_acc
  58
  59/-- Coherence Defect: Variance of the potential across the object.
  60    If Potential is flat, Defect is 0.
  61-/
  62def coherence_defect (field : ProcessingField) (obj : ExtendedObject) (a : ℝ) : ℝ :=
  63  -- Difference in potential between Head (z = +extent) and Feet (z = -extent)
  64  let pot_head := total_potential_in_frame field obj a obj.extent
  65  let pot_feet := total_potential_in_frame field obj a (-obj.extent)
  66  abs (pot_head - pot_feet)
  67
  68/-- Helper: expand coherence_defect into explicit arithmetic (no let bindings). -/