IndisputableMonolith.Measurement.PathAction

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Recognition Path Action (Minimal Interface)
   6
   7Lightweight interface for recognition paths and their action/weights. Heavy
   8measure-theoretic lemmas (piecewise additivity, domain shifts, etc.) are
   9intentionally omitted to keep the build surface stable for paper exports.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Measurement
  14
  15open Real Complex Cost
  16
  17/-- A recognition path is a time-parameterized positive rate function. -/
  18structure RecognitionPath where
  19  T : ℝ
  20  T_pos : 0 < T
  21  rate : ℝ → ℝ
  22  rate_pos : ∀ t, t ∈ Set.Icc 0 T → 0 < rate t
  23
  24/-- Recognition action C[γ] = ∫ J(r(t)) dt. -/
  25noncomputable def pathAction (γ : RecognitionPath) : ℝ :=
  26  ∫ t in (0)..γ.T, Cost.Jcost (γ.rate t)
  27
  28/-- Positive weight w[γ] = exp(-C[γ]). -/
  29noncomputable def pathWeight (γ : RecognitionPath) : ℝ :=
  30  Real.exp (- pathAction γ)
  31
  32/-- Amplitude bridge 𝒜[γ] = exp(-C[γ]/2) · exp(i φ). -/
  33noncomputable def pathAmplitude (γ : RecognitionPath) (φ : ℝ) : ℂ :=
  34  Complex.exp (- pathAction γ / 2) * Complex.exp (φ * I)
  35
  36/-- Weight is positive. -/
  37lemma pathWeight_pos (γ : RecognitionPath) : 0 < pathWeight γ := by
  38  unfold pathWeight
  39  exact Real.exp_pos _
  40
  41/-- Amplitude modulus squared equals weight. -/
  42theorem amplitude_mod_sq_eq_weight (γ : RecognitionPath) (φ : ℝ) :
  43  ‖pathAmplitude γ φ‖ ^ 2 = pathWeight γ := by
  44  unfold pathAmplitude pathWeight
  45  have h1 : ‖Complex.exp (-(pathAction γ) / 2)‖ = Real.exp (-(pathAction γ) / 2) := by
  46    simpa using Complex.norm_exp_ofReal (-(pathAction γ) / 2)
  47  have h2 := Complex.norm_exp_ofReal_mul_I φ
  48  rw [norm_mul]
  49  simp only [h1, h2, mul_one, sq]
  50  rw [← Real.exp_add]
  51  ring
  52
  53end Measurement
  54end IndisputableMonolith
  55