actual_prescribed_state_reversal_and_rate_product

Plain-English statement

Independent science ce675a4cfad2d35cc8c4fec2c26979728742ac27. Original six analytic assumptions and actual path definitions. Reversing the strict event tuple gives barPost_j=R(arrive_(n-j)) and barArrive_j=R(post_(n-j)) on all n+1 arcs; products of the n incoming event rates agree. Actual phase reversal and endpoint laws discharge all private premises. Includes n=0,T=0,rank0,zero normals and rates. No all-time right-continuous path equality, survival time substitution, weighted density equality, invariant probability, Markovness, hypocoercivity, errors, expected costs, main results or composition.

Lean statement

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βη := by
  unfold actual_prescribed_state_reversal_statement
  intro c Φ S Rec Hist Δ Prefix m zAt K Path Ψ Γ R rate n T
  obtain ⟨rho, hrho, _, _, _, hend, _⟩ :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ActualEndpointTimeReversal.actual_endpoint_time_reversal_laws
      hα hαβ hV hH hη hβη n T
  obtain ⟨_, _, _, _, _, _, hInv, hS, hR, hRev, hRS, hRate, _⟩ :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseReversalVolume.actual_phase_reversal_volume_laws
      hα hαβ hV hH hη hβη
  refine ⟨rho, hrho, ?_⟩
  intro y r z t grid post arrive A barGrid barPost barArrive
  let d : Fin (n+1) → ℝ := fun j => grid j.succ - grid j.castSucc
  have hg : ∀ j : Fin (n+1), barGrid j.succ - barGrid j.castSucc = d j.rev :=
    reversed_grid_gaps n (T : ℝ) t.val (rho t).val (hrho t)
  have hp (i : Fin n) : post i.succ = S r (arrive i.castSucc) := by
    simp only [post, arrive, grid, zAt, Fin.succ_castSucc,
      Fin.snoc_castSucc, Fin.cons_succ, Fin.induction_succ]
  have hb0 (i : Fin n) : barPost i.succ = S r (barArrive i.castSucc) := by
    simp only [barPost, barArrive, barGrid, zAt, Fin.succ_castSucc,
      Fin.snoc_castSucc, Fin.cons_succ, Fin.induction_succ]
  have hb (i : Fin n) : barPost i.succ =
      S r (Φ y r (d i.castSucc.rev) (barPost i.castSucc)) := by
    rw [hb0]
    change S r (Φ y r (barGrid i.castSucc.succ - barGrid i.castSucc.castSucc)
      (barPost i.castSucc)) = _
    rw [hg]
  have hz : barPost 0 = R (Φ y r (d (Fin.last n)) (post (Fin.last n))) := by
    change R A = R (arrive (Fin.last n))
    congr 1
    simpa only [arrive, d, grid, post, Fin.succ_last, Fin.snoc_last,
      Fin.snoc_castSucc] using hend y r z t
  have hstates := finite_state_reversal n (Φ y r) (S r) R
    (fun q => hS r q) (fun q => hR q) (fun q => hRS r q)
    (fun u q => (hInv y r u q).2) (fun u q => hRev y r u q)
    d post barPost hp hb hz
  have hpair (j : Fin (n+1)) :
      barPost j = R (arrive j.rev) ∧ barArrive j = R (post j.rev) := by
    refine ⟨(hstates j).1, ?_⟩
    change Φ y r (barGrid j.succ - barGrid j.castSucc) (barPost j) = _
    rw [hg]
    exact (hstates j).2
  refine ⟨hpair, ?_⟩
  exact incoming_rate_product n (S r) R (rate r) (fun q => hRate r q)
    post arrive barArrive hp (fun j => (hpair j).2)

#print axioms actual_prescribed_state_reversal_and_rate_product
end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedStateReversal

Open AutoSamplingTheory/ExampleCases/ProximalBPS/ActualPrescribedStateReversal.lean:138published source at ed709a7f320d

Proof architecture

Actual finite PBPS paired-state reversal and rate product; 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.
• `rw` rewrites by an established identity.
• `simp` normalizes through registered definitional and theorem rewrites.
• `refine` instantiates a reusable theorem while leaving explicit subgoals.
• `exact` closes the current goal with an already typed term.
• `simpa` closes the goal after a controlled simplification of a typed result.

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.
• Density statements retain normalization and absolute-continuity prerequisites.