ActualPrescribedStateReversal: mathematical reading route

Mathematical statement

Let E be a finite-dimensional real inner-product space with its Borel sigma algebra, including dimension zero. Let V:E→R, alpha,beta≥0 and eta in R. Assume alpha>0, alpha≤beta, V is C2, alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for every x,v in E, eta>0 and beta*eta≤1. For y,r in E put c=y-eta grad V(r), h_r(x)=grad V(x)-grad V(r), R(x,p)=(x,-p), Phi_(y,r,u)(x,p)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p), S_r(x,p)=(x,p-(2<p,h_r(x)>/||h_r(x)||^2)h_r(x)). Real division by zero is zero, so a zero normal gives the identity bounce. Let ell=volume_E tensor volume_E, with canonical Hilbert-space Lebesgue measure. For every integer n≥0 and horizon T≥0, let Delta_n(T) consist of real tuples 0<t_0<...<t_(n-1)<T. Equivalently, prepending 0 produces a strictly increasing tuple and every entry is less than T. Let Prefix_n(T) be this subtype and m_n,T the comap of Lebesgue measure on R^n under its inclusion. This is unnormalized simplex volume. For n=0 the tuple is empty and its zero-dimensional volume is one; for T=0 and n>0 the subtype is empty. Write q_0=0 and q_(j+1)=t_j. Starting at z_0=z, define z_(j+1)=S_r(Phi_(y,r,t_j-q_j)(z_j)) for 0≤j<n. Define records K_j=(q_j,z_j), each embedded in the live branch of (R_nonnegative x (E x E)) plus a cemetery symbol. For a general history of n+1 such records, the path reconstruction Psi at s in [0,T] starts from z and visits records in increasing index order: a live record (a,w) replaces the accumulator by Phi_(y,r,s-a)(w) exactly when a≤s; future records and cemetery records leave it unchanged. Here s-a is nonnegative subtraction. Define Gamma_(y,r,z,t)=Psi(K), the actual finite prescribed path; thus its value at an event is the post-bounce value. Let A_(y,r)(z,t)=Gamma_(y,r,z,t)(T). Define lambda_r(x,p)=sqrt(eta) max(0,<p,grad V(x)-grad V(r)>). For every finite n≥0 and T≥0 there exists rho:Prefix(n,T)→Prefix(n,T) with (rho(t))_i=T-t_(n-1-i). This witness is produced, not assumed. For every y,r,z and t in Prefix(n,T), form the grid a=(0,t_0,...,t_(n-1),T), indexed from0 through n+1. Set post_j=zAt(y,r,z,n,T,t,j) and arrive_j=Phi_(a_(j+1)-a_j)(post_j) for j=0,...,n. Set A=Gamma(y,r,z,n,T,t)(T), the actual terminal state. Form the reversed grid abar=(0,rho(t)_0,...,rho(t)_(n-1),T), set barPost_j=zAt(y,r,R(A),n,T,rho(t),j), and barArrive_j=Phi_(abar_(j+1)-abar_j)(barPost_j). For every j=0,...,n, barPost_j=R(arrive_(n-j)) and barArrive_j=R(post_(n-j)). Moreover product over i=0,...,n-1 of lambda_r(barArrive_i) equals product over i=0,...,n-1 of lambda_r(arrive_i). The last arrival arrive_n is the actual terminal state and is not one of the n event-rate factors. Reversal on the n+1 arcs is j→n-j; reversal on the n events is i→n-1-i. Per-event rate equality is proved internally; the public conclusion exports the paired states and product equality. The theorem covers n=0 (one flow arc and empty products equal1), T=0, rank-zero spaces, zero reflection normals and zero rates. No division by a rate or positivity of a prescribed event rate is assumed. The original six analytic assumptions are the only analytic premises; reversal identities, inverse maps, terminal identification and incoming-rate matching are derived from actual producers. The exact unnormalized simplex measure m is retained in the literal interface but is unused in these pointwise deterministic conclusions. This is the finite-state and incoming-rate component of the Appendix A.1 reversal proof. At a genuine event the right-continuous post-event value reverses to the original incoming value, not the original post-event value. No equality of the two right-continuous trajectories at all times is claimed. Survival time substitution, weighted density equality, stationary invariance, restart/Markovness, hypocoercivity, implementation errors, actual expected costs, main results and PBPS/SPHMC composition remain separate.

theorem actual_prescribed_state_reversal_and_rate_product
    {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_prescribed_state_reversal_statement hα hαβ hV hH hη hβη

private def actual_prescribed_state_reversal_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 := by
  classical
  exact
    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 Rec := (ℝ≥0 × (E × E)) ⊕ Unit
    let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
    let Δ : (n : ℕ) → ℝ≥0 → Set (Fin n → ℝ) := fun n T =>
      {t | StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < (T : ℝ)}
    let Prefix : (n : ℕ) → ℝ≥0 → Type := fun n T => {t : Fin n → ℝ // t ∈ Δ n T}
    let m : (n : ℕ) → (T : ℝ≥0) → Measure (Prefix n T) := fun n T =>
      Measure.comap (fun t : Prefix n T => t.val) (volume : Measure (Fin n → ℝ))
    let zAt : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → Fin (n + 1) → (E × E) := fun y xRef z₀ n T t =>
      Fin.induction z₀ (fun i z =>
        S xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc) z))
    let K : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → Hist n := fun y xRef z₀ n T t j =>
      Sum.inl (Real.toNNReal ((Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) j), zAt y xRef z₀ n T t j)
    let Path : ℝ≥0 → Type _ := fun T => {s : ℝ≥0 // s ≤ T} → E × E
    let Ψ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Hist n → Path T :=
      fun y xRef z₀ n T h s =>
        Fin.foldl (n + 1) (fun z j => (h j).elim
          (fun a => if a.1 ≤ s.val then Φ y xRef ((s.val - a.1 : ℝ≥0) : ℝ) a.2 else z)
          (fun _ => z)) z₀
    let Γ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Prefix n T → Path T :=
      fun y xRef z₀ n T t => Ψ y xRef z₀ n T (K y xRef z₀ n T t)
    let R : E × E → E × E := fun z => (z.1, -z.2)
    let rate : E → E × E → ℝ := fun r z =>
      Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V r))
    ∀ n : ℕ, ∀ T : ℝ≥0, ∃ rho : Prefix n T → Prefix n T,
      (∀ t : Prefix n T, ∀ i : Fin n, (rho t).val i = (T : ℝ) - t.val i.rev) ∧
      ∀ y r : E, ∀ z : E × E, ∀ t : Prefix n T,
        let grid : Fin (n+2) → ℝ := Fin.snoc (Fin.cons (0 : ℝ) t.val) (T : ℝ)
        let post : Fin (n+1) → E × E := zAt y r z n T t
        let arrive : Fin (n+1) → E × E := fun j =>
          Φ y r (grid j.succ - grid j.castSucc) (post j)
        let A : E × E := Γ y r z n T t ⟨T, le_rfl⟩
        let barGrid : Fin (n+2) → ℝ := Fin.snoc (Fin.cons (0 : ℝ) (rho t).val) (T : ℝ)
        let barPost : Fin (n+1) → E × E := zAt y r (R A) n T (rho t)
        let barArrive : Fin (n+1) → E × E := fun j =>
          Φ y r (barGrid j.succ - barGrid j.castSucc) (barPost j)
        (∀ j : Fin (n+1), barPost j = R (arrive j.rev) ∧ barArrive j = R (post j.rev)) ∧
        (∏ i : Fin n, rate r (barArrive i.castSucc)) =
          ∏ i : Fin n, rate r (arrive i.castSucc)

Proof roadmap

1. 1Reverse each finite incoming and post-event state

   The private finite-array lemma first combines momentum reversal with the inverse flow to obtain Phi_u(R(Phi_u q))=R q. The reversed initial state is the reversal of the final arrival. Induct over reversed events. The flow identity turns the paired reversed post-state into the reversal of the original post-state. The next reversed bounce is S R S applied to the original arrival, which equals R because S is involutive and commutes with R. The Fin casts convert arc reversal into event reversal exactly. These algebraic premises are internal and are supplied by actual PBPS laws below.

2. 2Pair incoming event rates and permute the finite product

   At reversed event i, the state identity gives barArrive_i=R(post_(n-i))=R(S(arrive_(n-1-i))). The actual rate identity lambda(R S q)=lambda(q) pairs the corresponding incoming rates. Apply the permutation Fin.rev to reindex the product. No factor is cancelled, so zero rates are included; with no events both products are1. The individual rate pairing is an internal step, while the public result exposes the product.

3. 3Match the lengths of reversed flow arcs

   Prepend zero and append T to both event tuples. The coordinate equation rho(t)_i=T-t_(n-1-i) gives abar_j=T-a_(n+1-j) and abar_(j+1)=T-a_(n-j). Subtract to obtain the original arc length at index n-j. The first and last grid entries are checked separately by finite cases, so the one-arc n=0 case remains valid. This is an adapter for the actual grid representation; it invokes no private declaration from another module.

4. 4Obtain actual reversal maps and the actual terminal state

   Apply the verified actual endpoint/time theorem to obtain rho, its coordinate formula and A=Phi_(T-a_n)(z_n). Apply the actual phase-reversal theorem to obtain both flow inverses, the involutions S and R, their commutation and lambda(R S q)=lambda(q). Introduce the literal actual post/arrival arrays and use the grid adapter to identify every reverse arc length. Nothing is supplied as an extra theorem hypothesis.

5. 5Discharge every finite-array premise from the actual recursion

   Unfold the actual finite state recursion at successor indices. It gives post_(i+1)=S(arrive_i) and barPost_(i+1)=S(barArrive_i). Replace the reversed arc length by the matched original length. The actual terminal formula identifies the reversed initial state R(A) with R(arrive_n). Thus the private induction receives proved actual recurrences and endpoint data, including all zero cases.

6. 6Assemble the actual state and incoming-product conclusions

   Invoke finite state reversal with the actual harmonic flow, bounce, momentum reversal and proved recurrences. Re-express its reversed-length flow as the literal barArrive array using the grid identity. This proves both state equalities. Supply the actual rate identity and state equalities to the finite-product lemma to obtain the product conclusion. The proof keeps incoming and post-event states separate; path reversal away from events and survival-integral substitution are later dependencies.