AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhysicalTimeCover

import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualNonaccumulation
import AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct
import Mathlib.Topology.Order.WithTop

/-! Actual PBPS finite physical-time interval coverage.
PBPS arXiv2609.06905v1 Appendix A.1 between-jump formula.
Source standing analytic conditions and exact stopped recurrence are retained.
Actual inputs use the canonical Exp(1) product. No supplied stochastic/cap/time
certificate and no global physical-time process, Markov or invariance claim. -/
namespace AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhysicalTimeCover
open InnerProductSpace MeasureTheory ProbabilityTheory Filter
open scoped ContDiff NNReal ENNReal Topology Interval BigOperators
noncomputable section
set_option autoImplicit false

private def actual_fixed_reference_physical_time_cover_statement
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ) * ‖v‖ ^ 2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) : Prop :=
    let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
    let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun sample k => Real.toNNReal (sample k)
    let c : E → E → E := fun y xRef => y - η • gradient V xRef
    let Φ : E → E → ℝ → (E × E) → (E × E) := fun y xRef t z =>
      (c y xRef + Real.cos t • (z.1 - c y xRef) +
          (Real.sqrt η * Real.sin t) • z.2,
       (-Real.sin t / Real.sqrt η) • (z.1 - c y xRef) + Real.cos t • z.2)
    let S : E → (E × E) → (E × E) := fun xRef z =>
      (z.1, z.2 - (2 * inner ℝ z.2 (gradient V z.1 - gradient V xRef) /
        ‖gradient V z.1 - gradient V xRef‖ ^ 2) • (gradient V z.1 - gradient V xRef))
    let rate : E → (E × E) → ℝ := fun xRef z =>
      Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V xRef))
    let Λ : E → E → (E × E) → ℝ≥0 → ℝ := fun y xRef z t =>
      ∫ s in (0 : ℝ)..(t : ℝ), rate xRef (Φ y xRef s z)
    let τ : E → E → (E × E) → ℝ≥0 → WithTop ℝ≥0 := fun y xRef z e =>
      MeasureTheory.hittingAfter
        (fun t : ℝ≥0 => fun a : (E × E) × (E × E) × ℝ≥0 =>
          Λ a.1.1 a.1.2 a.2.1 t - (a.2.2 : ℝ))
        (Set.Ici (0 : ℝ)) 0 ((y, xRef), z, e)
    let next : E → E → ℝ≥0 → ((ℝ≥0 × (E × E)) ⊕ Unit) →
        ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef e r =>
      match r with
      | Sum.inr _ => Sum.inr ()
      | Sum.inl a =>
        if τ y xRef a.2 e = ⊤ then Sum.inr () else
          Sum.inl (a.1 + (τ y xRef a.2 e).untopD 0,
            S xRef (Φ y xRef (((τ y xRef a.2 e).untopD 0 : ℝ≥0) : ℝ) a.2))
    let record : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ →
        ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef z₀ e n =>
      Nat.rec (Sum.inl (0, z₀)) (fun k r => next y xRef (e k) r) n
    let eventTime : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ → WithTop ℝ≥0 :=
      fun y xRef z₀ e n => (record y xRef z₀ e n).elim
        (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
    ∀ y xRef : E, ∀ z₀ : E × E, ∀ᵐ sample ∂P,
      (∀ t : ℝ≥0, ∃! n : ℕ,
        eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) ∧
        (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1)) ∧
      (∀ t : ℝ≥0, ∀ n : ℕ,
        eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) →
        (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1) →
        ∃! a : ℝ≥0 × (E × E),
          record y xRef z₀ (ε sample) n = Sum.inl a ∧ a.1 ≤ t ∧
          ((t - a.1 : ℝ≥0) : WithTop ℝ≥0) < τ y xRef a.2 (ε sample n))


set_option maxHeartbeats 800000 in
theorem actual_fixed_reference_physical_time_cover
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ) * ‖v‖ ^ 2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) :
    actual_fixed_reference_physical_time_cover_statement hα hαβ hV hH hη hβη := by
  classical
  let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
  let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun sample k => Real.toNNReal (sample k)
  let c : E → E → E := fun y xRef => y - η • gradient V xRef
  let Φ : E → E → ℝ → (E × E) → (E × E) := fun y xRef t z =>
    (c y xRef + Real.cos t • (z.1 - c y xRef) +
        (Real.sqrt η * Real.sin t) • z.2,
     (-Real.sin t / Real.sqrt η) • (z.1 - c y xRef) + Real.cos t • z.2)
  let S : E → (E × E) → (E × E) := fun xRef z =>
    (z.1, z.2 - (2 * inner ℝ z.2 (gradient V z.1 - gradient V xRef) /
      ‖gradient V z.1 - gradient V xRef‖ ^ 2) • (gradient V z.1 - gradient V xRef))
  let rate : E → (E × E) → ℝ := fun xRef z =>
    Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V xRef))
  let Λ : E → E → (E × E) → ℝ≥0 → ℝ := fun y xRef z t =>
    ∫ s in (0 : ℝ)..(t : ℝ), rate xRef (Φ y xRef s z)
  let τ : E → E → (E × E) → ℝ≥0 → WithTop ℝ≥0 := fun y xRef z e =>
    MeasureTheory.hittingAfter
      (fun t : ℝ≥0 => fun a : (E × E) × (E × E) × ℝ≥0 =>
        Λ a.1.1 a.1.2 a.2.1 t - (a.2.2 : ℝ))
      (Set.Ici (0 : ℝ)) 0 ((y, xRef), z, e)
  let next : E → E → ℝ≥0 → ((ℝ≥0 × (E × E)) ⊕ Unit) →
      ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef e r =>
    match r with
    | Sum.inr _ => Sum.inr ()
    | Sum.inl a =>
      if τ y xRef a.2 e = ⊤ then Sum.inr () else
        Sum.inl (a.1 + (τ y xRef a.2 e).untopD 0,
          S xRef (Φ y xRef (((τ y xRef a.2 e).untopD 0 : ℝ≥0) : ℝ) a.2))
  let record : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ →
      ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef z₀ e n =>
    Nat.rec (Sum.inl (0, z₀)) (fun k r => next y xRef (e k) r) n
  let eventTime : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ → WithTop ℝ≥0 :=
    fun y xRef z₀ e n => (record y xRef z₀ e n).elim
      (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
  change ∀ y xRef : E, ∀ z₀ : E × E, ∀ᵐ sample ∂P,
    (∀ t : ℝ≥0, ∃! n : ℕ,
      eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) ∧
      (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1)) ∧
    (∀ t : ℝ≥0, ∀ n : ℕ,
      eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) →
      (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1) →
      ∃! a : ℝ≥0 × (E × E),
        record y xRef z₀ (ε sample) n = Sum.inl a ∧ a.1 ≤ t ∧
        ((t - a.1 : ℝ≥0) : WithTop ℝ≥0) < τ y xRef a.2 (ε sample n))
  -- Exact deterministic initialization/monotonicity and guarded live-record updates.
  rcases ActualFiniteJumpRecursion.actual_fixed_reference_finite_jump_recursion
      hα hαβ hV hH hη hβη with
    ⟨_, hstep, _, _, _, htime, _, _, _, _⟩
  have hinput := ActualNonaccumulation.actual_fixed_reference_event_time_nonaccumulation
    hα hαβ hV hH hη hβη
  intro y xRef z₀
  filter_upwards [hinput y xRef z₀] with sample hgood
  have hzero : eventTime y xRef z₀ (ε sample) 0 = 0 :=
    (htime y xRef z₀ (ε sample)).1
  have hmono : Monotone (eventTime y xRef z₀ (ε sample)) :=
    (htime y xRef z₀ (ε sample)).2
  constructor
  · -- The first clock strictly above t has an initialized finite predecessor.
    intro t
    obtain ⟨N, hN⟩ := eventually_atTop.mp (hgood.1 t)
    have hex : ∃ k : ℕ, (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) k :=
      ⟨N, hN N le_rfl⟩
    let k : ℕ := Nat.find hex
    have hk : (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) k :=
      Nat.find_spec hex
    have hkpos : 0 < k := by
      by_contra h
      have hk0 : k = 0 := Nat.eq_zero_of_not_pos h
      rw [hk0, hzero] at hk
      exact (not_lt_of_ge (show (0 : WithTop ℝ≥0) ≤ t from bot_le)) hk
    let n : ℕ := k - 1
    have hsucc : n + 1 = k := by dsimp [n]; omega
    have hlow : eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) := by
      apply le_of_not_gt
      exact Nat.find_min hex (by change k - 1 < k; omega)
    have hupp : (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1) := by
      simpa only [hsucc] using hk
    refine ⟨n, ⟨hlow, hupp⟩, ?_⟩
    -- Monotonicity makes distinct half-open event intervals disjoint.
    intro m hm
    apply le_antisymm
    · by_contra h
      have hnm : n + 1 ≤ m := by omega
      exact (not_lt_of_ge ((hmono hnm).trans hm.1)) hupp
    · by_contra h
      have hmn : m + 1 ≤ n := by omega
      exact (not_lt_of_ge ((hmono hmn).trans hlow)) hm.2
  · -- A clock below finite t cannot be a stopped record.
    intro t n hlow hupp
    cases hr : record y xRef z₀ (ε sample) n with
    | inr u =>
      have hevent : eventTime y xRef z₀ (ε sample) n = ⊤ := by
        change (record y xRef z₀ (ε sample) n).elim _ _ = ⊤
        rw [hr]
        rfl
      rw [hevent] at hlow
      exact False.elim ((not_le_of_gt (WithTop.coe_lt_top t)) hlow)
    | inl a =>
      have haClock : eventTime y xRef z₀ (ε sample) n = (a.1 : WithTop ℝ≥0) := by
        change (record y xRef z₀ (ε sample) n).elim _ _ = _
        rw [hr]
        rfl
      have hat : a.1 ≤ t := WithTop.coe_le_coe.mp (by
        rw [← haClock]
        exact hlow)
      refine ⟨a, ⟨rfl, hat, ?_⟩, ?_⟩
      · -- Infinite wait keeps the last live arc available at every finite offset.
        by_cases hwtop : τ y xRef a.2 (ε sample n) = ⊤
        · simp only [hwtop, WithTop.coe_lt_top]
        -- Finite wait: the actual next clock is a.time plus that same wait.
        · let q : ℝ≥0 := (τ y xRef a.2 (ε sample n)).untop hwtop
          have hq : (q : WithTop ℝ≥0) = τ y xRef a.2 (ε sample n) :=
            WithTop.coe_untop _ _
          have hn : record y xRef z₀ (ε sample) (n + 1) =
              Sum.inl (a.1 + (τ y xRef a.2 (ε sample n)).untopD 0,
                S xRef (Φ y xRef (((τ y xRef a.2 (ε sample n)).untopD 0 : ℝ≥0) : ℝ) a.2)) :=
            ((hstep y xRef z₀ (ε sample) n).2 a hr).2 hwtop
          rw [← hq] at hn ⊢
          have hnTime : eventTime y xRef z₀ (ε sample) (n + 1) =
              ((a.1 + q : ℝ≥0) : WithTop ℝ≥0) := by
            change (record y xRef z₀ (ε sample) (n + 1)).elim _ _ = _
            rw [hn]
            rfl
          have hsmall : t < a.1 + q := WithTop.coe_lt_coe.mp (by
            simpa only [hnTime] using hupp)
          exact WithTop.coe_lt_coe.mpr ((tsub_lt_iff_right hat).mpr (by
            simpa only [add_comm] using hsmall))
      · -- The stored record is a function; injectivity gives uniqueness.
        intro b hb
        exact Sum.inl.inj hb.1.symm

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhysicalTimeCover