actual_fixed_reference_event_time_nonaccumulation

Plain-English statement

Independently verified science bbcad09376c51bbf27c0ed4c16be0dc053bb01c5. Actual fixed-reference PBPS A2 event times under the canonical Exp1 product escape every finite horizon almost surely and have finite bounded-horizon index sets, including index0. Original six source analytic binders; no supplied iid/cap/recurrence/divergence provider. Zero cap stops and absorbs; positive cap controls clocks by actual divergent partial sums. No global physical-time path/Markov/invariance/kernel/hypocoercivity/main/error/expected-cost/composition or whole-paper/Goal completion. Aggregate/visual/main/PURIFIED/live remain distinct.

Lean statement

theorem actual_fixed_reference_event_time_nonaccumulation
    {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_event_time_nonaccumulation_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 H : E → E → (E × E) → ℝ := fun y xRef z =>
    (η⁻¹ * ‖z.1 - c y xRef‖ ^ 2 + ‖z.2‖ ^ 2) / 2
  let C : E → E → (E × E) → ℝ := fun y xRef z =>
    Real.sqrt η * (β : ℝ) * Real.sqrt (2 * H y xRef z) *
      (Real.sqrt (2 * η * H y xRef z) + ‖c y xRef - 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 : ℕ in atTop,
      (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) n) ∧
    (∀ t : ℝ≥0, {n : ℕ | eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0)}.Finite)
  -- Reuse the actual deterministic recurrence; no cap or recurrence is supplied.
  rcases ActualFiniteJumpRecursion.actual_fixed_reference_finite_jump_recursion
      hα hαβ hV hH hη hβη with
    ⟨hinit, _, _, _, _, htime, hstop, _, hcap, _⟩
  -- The good event supplies all positive thresholds and divergent actual sums.
  rcases AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws with
    ⟨_, _, _, hgood, hdiv⟩
  intro y xRef z₀
  filter_upwards [hgood, hdiv] with sample hpos hsum
  have hepos (k : ℕ) : 0 < ε sample k :=
    Real.toNNReal_pos.mpr (hpos k).1
  obtain ⟨hC, hinc, hzero⟩ := hcap y xRef z₀ (ε sample)
  have hescape : ∀ t : ℝ≥0, ∀ᶠ n : ℕ in atTop,
      (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) n := by
    -- Zero cap forces the first positive-threshold update to stop; it absorbs.
    by_cases hC0 : C y xRef z₀ = 0
    · have hfirst : record y xRef z₀ (ε sample) 1 = Sum.inr () :=
        hzero hC0 0 (0, z₀) (hinit y xRef z₀ (ε sample)) (hepos 0)
      intro t
      filter_upwards [eventually_ge_atTop (1 : ℕ)] with n hn
      obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hn
      have hs : record y xRef z₀ (ε sample) (1 + k) = Sum.inr () :=
        hstop y xRef z₀ (ε sample) 1 k hfirst
      change (t : WithTop ℝ≥0) < (record y xRef z₀ (ε sample) (1 + k)).elim _ _
      rw [hs]
      exact WithTop.coe_lt_top t
    -- Positive cap: inductively compare every actual clock with partial sums/C.
    · have hCp : 0 < C y xRef z₀ := lt_of_le_of_ne hC (Ne.symm hC0)
      let cap : ℝ≥0 := Real.toNNReal (C y xRef z₀)
      have hcapcoe : (cap : ℝ) = C y xRef z₀ := Real.coe_toNNReal _ hC
      have hcapPos : 0 < cap := Real.toNNReal_pos.mpr hCp
      have hbound (n : ℕ) :
          (((∑ k ∈ Finset.range n, ε sample k) / cap : ℝ≥0) : WithTop ℝ≥0) ≤
            eventTime y xRef z₀ (ε sample) n := by
        induction n with
        | zero => simpa using (htime y xRef z₀ (ε sample)).1.ge
        | succ n ih =>
          have hi := hinc hCp n
          have hterm : Real.toNNReal ((ε sample n : ℝ) / C y xRef z₀) =
              ε sample n / cap := by
            rw [Real.toNNReal_div (ε sample n).coe_nonneg, Real.toNNReal_coe]
          rw [hterm] at hi
          calc
            (((∑ k ∈ Finset.range (n + 1), ε sample k) / cap : ℝ≥0) : WithTop ℝ≥0)
                = (((∑ k ∈ Finset.range n, ε sample k) / cap : ℝ≥0) : WithTop ℝ≥0) +
                    ((ε sample n / cap : ℝ≥0) : WithTop ℝ≥0) := by
                      rw [Finset.sum_range_succ, add_div, WithTop.coe_add]
            _ ≤ eventTime y xRef z₀ (ε sample) n +
                    ((ε sample n / cap : ℝ≥0) : WithTop ℝ≥0) := add_le_add ih le_rfl
            _ ≤ eventTime y xRef z₀ (ε sample) (n + 1) := hi
      intro t
      have hs : ∀ᶠ n : ℕ in atTop,
          (t : ℝ) * C y xRef z₀ < ∑ k ∈ Finset.range n, (ε sample k : ℝ) :=
        hsum.eventually (eventually_gt_atTop ((t : ℝ) * C y xRef z₀))
      filter_upwards [hs] with n hn
      have ht : t < (∑ k ∈ Finset.range n, ε sample k) / cap := by
        apply (NNReal.coe_lt_coe).mp
        push_cast
        rw [hcapcoe]
        exact (lt_div_iff₀ hCp).mpr hn
      exact lt_of_lt_of_le (WithTop.coe_lt_coe.mpr ht) (hbound n)
  refine ⟨hescape, ?_⟩
  -- The bounded-horizon index set is contained in a finite initial interval.
  intro t
  obtain ⟨N, hN⟩ := eventually_atTop.mp (hescape t)
  apply (Set.finite_Iio N).subset
  intro n hn
  exact lt_of_not_ge (fun hge => (not_lt_of_ge hn) (hN n hge))

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualNonaccumulation

Open AutoSamplingTheory/ExampleCases/ProximalBPS/ActualNonaccumulation.lean:64published source at ed709a7f320d

Proof architecture

PBPS global-path prerequisite; no SALD claim

Lean proof walkthrough

• Read the quantified variables and typeclass brackets as part of the mathematical statement; inferred arguments are not missing assumptions.
• `intro` introduces quantified hypotheses into the local proof context.
• `have` creates a named intermediate mathematical fact.
• `calc` records an equality or inequality chain matching a paper calculation.
• `rw` rewrites by an established identity.
• `apply` reduces the goal to the hypotheses of a reusable theorem.
• `refine` instantiates a reusable theorem while leaving explicit subgoals.
• `exact` closes the current goal with an already typed term.

Why the statement has this shape

The declaration is kept at the reusable level recorded by its Registry tags and direct consumers. Explicit measures, spaces, wrappers, and regularity hypotheses expose interfaces that paper notation often infers. A theorem card explains those interfaces but never widens the compiled statement.

Hidden assumptions and non-claims

• Measurability is represented explicitly or must be supplied by a dependency.
• Totalized `fderiv` values must not be read as a differentiability theorem.