Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

ReferenceCarryingKernel: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Actual reference-carrying recursive Markov transition
ASTIS mathematical exposition

Actual reference-carrying recursive Markov transition

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ReferenceCarryingKernel.reference_carrying_kernel · theorem · Teaching coverage

Statement

For every state,v>0 and bplus=b+1/v. N,out and update are jointly measurable. For every state/sample/noise triple,the actual stopped gradient-square is at most (alpha+bplus)*d and every earlier iterate strictly exceeds it; grad F_p(w)=grad V(w)+bplus*(w-uplus). The true source potential satisfies W_p(w)=F_p(w)+b*v^(-1)/(2*(b+v^(-1)))*norm(u-y)^2,so their gradients and all GD iterates from x with step1/(beta+bplus) coincide. The scaled reference sqrt(beta+bplus)*out has gradient-square at most d/((beta+bplus)/(alpha+bplus)) for F_p(./sqrt(beta+bplus)). There exists an actual Markov state transition P with P(s)=dirac(s) when theta<=b,and otherwise P(s)=update(s,.)#(M(s) x G). Its single-step reference-deleted marginal is dirac(project(s)) in the first branch and oldUpdate(s,.)#(M(s) x G) in the second.

\[P(s)=\begin{cases}\delta_s,&\theta\le b,\\ \mathrm{update}(s,\cdot)_\#(M(s)\otimes G),&b<\theta,\end{cases}\qquad \|\nabla F_p(\mathrm{out}(p))\|^2\le(\alpha+b^+)d.\]

All objects and hypotheses

  • E is a finite-dimensional real inner-product space with its Borel structure and d=dim(E)>0. V:E->R is C2; 0<alpha<=beta and alpha*norm(w)^2<=D2V(x)[w,w]<=beta*norm(w)^2 for every x,w.
  • The complete retained state is s=(b,u,xref,k,h) in NNReal x E x E x Nat x (Nat->E). The precision b is nonnegative; u and xref are original-coordinate points; k is a count and h a padded most-recent-first observation history. No admissibility or valid-history invariant is assumed for the old state.
  • eta,tau are measurable positive real functions of the complete retained state. M is an actual Markov kernel from that state to E, interpreted as the current sampler output in ORIGINAL coordinates BEFORE the fresh noise; no sampler accuracy or moment property is assumed. The supplied threshold theta is a nonnegative precision threshold.
  • For s and fresh pair (x,z), v(s)=(eta(s)+tau(s))/(beta+b), bplus=b+toNNReal(1/v(s)), y=x+sqrt(tau(s)/(beta+b))*z and uplus=(bplus)^(-1)*(b*u+v(s)^(-1)*y). The theorem proves v>0 and the real equality bplus=b+1/v, so toNNReal does not truncate.
  • F_p(w)=V(w)+bplus/2*norm(w-uplus)^2 and W_p(w)=V(w)+b/2*norm(w-u)^2+1/(2v)*norm(w-y)^2 for p=(s,(x,z)). Let T_p(w)=w-(beta+bplus)^(-1)*grad F_p(w), q_n(p)=norm(grad F_p(T_p^n(x)))^2. N(p) is the least n with q_n(p)<=(alpha+bplus)*d if one exists,otherwise zero. out(p)=T_p^N(p)(x),starting at the pre-noise x.
  • update(p)=(bplus,uplus,out(p),k+1,hplus), where hplus(0)=y and hplus(n+1)=h(n). project(s)=(b,u,k,h) removes only the reference. oldUpdate(p)=(bplus,uplus,k+1,hplus). G denotes the standard Gaussian probability on E; the product M(s) x G means the new noise is independent conditional on the complete state.

Mathematical proof

1. Keep coordinates,positive scales and the actual state update explicit

The state carries the old original-coordinate reference even though it may be arbitrary. M(s) is already in original coordinates. The fresh independent noise forms y,while the GD initial point remains x. Positive beta+b and eta+tau imply v>0; the real coercion of bplus is exactly b+1/v,so the nonnegative-real representation does not alter the precision.

\[v=\frac{\eta+\tau}{\beta+b}>0,\quad y=x+\sqrt{\frac\tau{\beta+b}}z,\quad b^+=b+v^{-1},\quad u^+=(b^+)^{-1}(bu+v^{-1}y).\]
Corresponding Lean step

reference_carrying_kernel: hbeta,hv,hbp,hbp0,hvm,hbpm,hobsm,hcm

2. Prove every finite iterate jointly measurable

For any measurable state space,precision b(s),center u(s),initial state and step may all vary measurably. The true base gradient is continuous by C2. Induct on iterations of the explicit genuine regularized gradient; measurable addition,scalar multiplication and composition prove the full state-to-iterate map measurable.

\[x_{n+1}(s)=x_n(s)-\gamma(s)\bigl(\nabla V(x_n(s))+b(s)(x_n(s)-u(s))\bigr).\]
Corresponding Lean step

state_iterates; variable_reference: hgrad,hgV,hTeq,hm,hq,hevent

3. Use the strict terminal witness for the actual first inner hit

At positive bplus,the parent terminal theorem with A=1/bplus gives a finite point hitting d*bplus. Since d*bplus<=(alpha+bplus)*d,this is an existence witness for the actual inner rule. firstIndex takes the least actual hit; measurable_find and Measurable.find give the index and stopped output. Minimality gives strict failure before N. No W2 or moment premise is used,and no equality with the terminal stopping output is claimed.

\[db^+\le(\alpha+b^+)d,\quad N=\min\{n:q_n\le(\alpha+b^+)d\},\quad q_j>(\alpha+b^+)d\ (j<N).\]
Corresponding Lean step

firstIndex; stopped_family; variable_reference: ht,hs; TerminalReferenceGradientDescent.terminal_reference_gradient_descent

4. Match the source quadratic update by a genuine constant identity

Complete the square in the two true quadratic terms. The difference C depends on state and observation but not on the iteration position. Frechet derivatives ignore this additive constant,so the gradients agree and hence every finite GD iterate is identical. The start remains the same pre-noise x.

\[W_p(w)=F_p(w)+C_p,\quad C_p=\frac{b v^{-1}}{2(b+v^{-1})}\|u-y\|^2,\quad \nabla W_p=\nabla F_p.\]
Corresponding Lean step

quadratic_source_alignment: he,hg,hh; reference_carrying_kernel: hsrc; fderiv_add_const

5. Certify the next normalized reference without changing stored coordinates

The actual reference stored by update is out in original coordinates. Apply the chain rule to F(./sqrt(cplus)),where cplus=beta+bplus. The scaled gradient is cplus^(-1/2) times the original gradient. The proved first-hit threshold therefore gives d/((beta+bplus)/(alpha+bplus)) for the scaled reference.

\[\left\|\nabla\bigl[F_p(\cdot/\sqrt{c^+})\bigr](\sqrt{c^+}\,\mathrm{out})\right\|^2\le\frac{(\alpha+b^+)d}{c^+}=\frac{d}{c^+/(\alpha+b^+)}.\]
Corresponding Lean step

scaled_reference_bound; reference_carrying_kernel: hFd,hp

6. Carry the true reference and observation history together

Combine the measurable precision,center and stopped-reference maps with count increment. For each history coordinate,use the two cases n=0 and n+1 to prove measurability of prepending y. This yields a measurable full update,not just a measurable center with an untracked reference.

\[\mathrm{update}(s,x,z)=(b^+,u^+,\mathrm{out},k+1,h^+),\quad h^+(0)=y,\quad h^+(n+1)=h(n).\]
Corresponding Lean step

reference_carrying_kernel: hNm,hom,hum; measurable_pi_lambda

7. Construct the actual Markov transition and absorbing branch

Take Q=M times the constant standard-Gaussian kernel. Retain the starting state through id times Q and push through the measurable update. Each operation preserves Markov normalization. The measurable set theta<=b selects the identity kernel; its complement uses the constructed continuation kernel. Expanding the kernel map gives the displayed statewise measure formula.

\[Q=M\times G,\quad C=(\mathrm{id}\times Q).\mathrm{map}(\mathrm{update}),\quad P=\mathbf1_{\{\theta\le b\}}\mathrm{id}+\mathbf1_{\{b<\theta\}}C.\]
Corresponding Lean step

reference_carrying_kernel: Q,hQ,C,hC,hCs,D,hD,P,hP,hPs; Kernel.map_apply; Kernel.prod_apply; Kernel.piecewise_apply

8. Project only the one-step marginal

Map each P(s) by project. A stopped dirac stays the projected dirac. Otherwise map-composition removes the reference coordinate from the actual full update,leaving precisely oldUpdate. The identity is at each enhanced state; M,eta,tau may still depend on its reference. No projected-chain Markovness,history invariant or source stopping-depth claim follows.

\[\mathrm{project}_\#P(s)=\begin{cases}\delta_{\mathrm{project}(s)},&\theta\le b,\\ \mathrm{oldUpdate}(s,\cdot)_\#(M(s)\otimes G),&b<\theta.\end{cases}\]
Corresponding Lean step

reference_carrying_kernel: hproj,final projection cases; Measure.map_dirac'; Measure.map_map

Lean statement · reference_carrying_kernel

Actual variable-state first-hit reference,source quadratic trajectory identity,normalized admissibility,enhanced Markov transition and one-step projected marginal.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem reference_carrying_kernel {V : E → ℝ} {α β : ℝ≥0}
    (hα : 0 < α) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x w : E, (α:ℝ)*‖w‖^2 ≤ fderiv ℝ (fderiv ℝ V) x w w ∧
      fderiv ℝ (fderiv ℝ V) x w w ≤ (β:ℝ)*‖w‖^2)
    (hd : 0 < (Module.finrank ℝ E : ℝ))
    (η τ : RefState E → ℝ) (hη : Measurable η) (hτ : Measurable τ)
    (hη0 : ∀ s, 0 < η s) (hτ0 : ∀ s, 0 < τ s)
    (M : Kernel (RefState E) E) [IsMarkovKernel M] (threshold : ℝ≥0) :
    let d : ℝ := Module.finrank ℝ E
    let v := fun s : RefState E => (η s+τ s)/((β:ℝ)+s.1)
    let bp := fun s : RefState E => s.1+Real.toNNReal (v s)⁻¹
    let obs := fun p : RefState E × (E × E) => p.2.1+Real.sqrt (τ p.1/((β:ℝ)+p.1.1)) • p.2.2
    let center := fun p : RefState E × (E × E) => (bp p.1:ℝ)⁻¹ •
      ((p.1.1:ℝ) • p.1.2.1+(v p.1)⁻¹ • obs p)
    let F := fun p x => V x+(bp p.1:ℝ)/2*‖x-center p‖^2
    let W := fun p x => V x+(p.1.1:ℝ)/2*‖x-p.1.2.1‖^2+(v p.1)⁻¹/2*‖x-obs p‖^2
    let T := fun p x => x-((β:ℝ)+bp p.1)⁻¹ • gradient (F p) x
    let q := fun n p => ‖gradient (F p) ((T p)^[n] p.2.1)‖^2
    let N := firstIndex q (fun p => ((α:ℝ)+bp p.1)*d)
    let out := fun p => (T p)^[N p] p.2.1
    let update := fun p : RefState E × (E × E) =>
      (bp p.1,center p,out p,p.1.2.2.2.1+1,fun n => Nat.casesOn n (obs p) p.1.2.2.2.2)
    let project := fun s : RefState E => (s.1,s.2.1,s.2.2.2.1,s.2.2.2.2)
    let oldUpdate := fun p : RefState E × (E × E) =>
      (bp p.1,center p,p.1.2.2.2.1+1,fun n => Nat.casesOn n (obs p) p.1.2.2.2.2)
    (∀ s, 0 < v s ∧ (bp s:ℝ)=(s.1:ℝ)+(v s)⁻¹) ∧
    Measurable N ∧ Measurable out ∧ Measurable update ∧
    (∀ p, q (N p) p ≤ ((α:ℝ)+bp p.1)*d ∧
      (∀ j < N p, ((α:ℝ)+bp p.1)*d < q j p) ∧
      (∀ x, gradient (F p) x=gradient V x+(bp p.1:ℝ) • (x-center p)) ∧
      (∀ x, W p x=F p x+
        (p.1.1:ℝ)*(v p.1)⁻¹/(2*((p.1.1:ℝ)+(v p.1)⁻¹))*‖p.1.2.1-obs p‖^2) ∧
      (∀ x, gradient (W p) x=gradient (F p) x) ∧
      (∀ n, (fun x => x-((β:ℝ)+bp p.1)⁻¹ • gradient (W p) x)^[n] p.2.1 =
        (T p)^[n] p.2.1) ∧
      ‖gradient (fun x => F p ((Real.sqrt ((β:ℝ)+bp p.1))⁻¹ • x))
          (Real.sqrt ((β:ℝ)+bp p.1) • out p)‖^2 ≤
        d/(((β:ℝ)+bp p.1)/((α:ℝ)+bp p.1))) ∧
    ∃ P : Kernel (RefState E) (RefState E), IsMarkovKernel P ∧
      (∀ s, P s=if threshold ≤ s.1 then Measure.dirac s else
        ((M s).prod (stdGaussian E)).map (fun z => update (s,z))) ∧
      (∀ s, (P s).map project=if threshold ≤ s.1 then Measure.dirac (project s) else
        ((M s).prod (stdGaussian E)).map (fun z => oldUpdate (s,z)))

Exact module and namespace context

Lean proof · reference_carrying_kernel

Measurable iteration and least hitting,strict terminal witness,quadratic completion and genuine derivatives,chain rule,product-kernel pushforward and measurable absorption.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem reference_carrying_kernel {V : E → ℝ} {α β : ℝ≥0}
    (hα : 0 < α) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x w : E, (α:ℝ)*‖w‖^2 ≤ fderiv ℝ (fderiv ℝ V) x w w ∧
      fderiv ℝ (fderiv ℝ V) x w w ≤ (β:ℝ)*‖w‖^2)
    (hd : 0 < (Module.finrank ℝ E : ℝ))
    (η τ : RefState E → ℝ) (hη : Measurable η) (hτ : Measurable τ)
    (hη0 : ∀ s, 0 < η s) (hτ0 : ∀ s, 0 < τ s)
    (M : Kernel (RefState E) E) [IsMarkovKernel M] (threshold : ℝ≥0) :
    let d : ℝ := Module.finrank ℝ E
    let v := fun s : RefState E => (η s+τ s)/((β:ℝ)+s.1)
    let bp := fun s : RefState E => s.1+Real.toNNReal (v s)⁻¹
    let obs := fun p : RefState E × (E × E) => p.2.1+Real.sqrt (τ p.1/((β:ℝ)+p.1.1)) • p.2.2
    let center := fun p : RefState E × (E × E) => (bp p.1:ℝ)⁻¹ •
      ((p.1.1:ℝ) • p.1.2.1+(v p.1)⁻¹ • obs p)
    let F := fun p x => V x+(bp p.1:ℝ)/2*‖x-center p‖^2
    let W := fun p x => V x+(p.1.1:ℝ)/2*‖x-p.1.2.1‖^2+(v p.1)⁻¹/2*‖x-obs p‖^2
    let T := fun p x => x-((β:ℝ)+bp p.1)⁻¹ • gradient (F p) x
    let q := fun n p => ‖gradient (F p) ((T p)^[n] p.2.1)‖^2
    let N := firstIndex q (fun p => ((α:ℝ)+bp p.1)*d)
    let out := fun p => (T p)^[N p] p.2.1
    let update := fun p : RefState E × (E × E) =>
      (bp p.1,center p,out p,p.1.2.2.2.1+1,fun n => Nat.casesOn n (obs p) p.1.2.2.2.2)
    let project := fun s : RefState E => (s.1,s.2.1,s.2.2.2.1,s.2.2.2.2)
    let oldUpdate := fun p : RefState E × (E × E) =>
      (bp p.1,center p,p.1.2.2.2.1+1,fun n => Nat.casesOn n (obs p) p.1.2.2.2.2)
    (∀ s, 0 < v s ∧ (bp s:ℝ)=(s.1:ℝ)+(v s)⁻¹) ∧
    Measurable N ∧ Measurable out ∧ Measurable update ∧
    (∀ p, q (N p) p ≤ ((α:ℝ)+bp p.1)*d ∧
      (∀ j < N p, ((α:ℝ)+bp p.1)*d < q j p) ∧
      (∀ x, gradient (F p) x=gradient V x+(bp p.1:ℝ) • (x-center p)) ∧
      (∀ x, W p x=F p x+
        (p.1.1:ℝ)*(v p.1)⁻¹/(2*((p.1.1:ℝ)+(v p.1)⁻¹))*‖p.1.2.1-obs p‖^2) ∧
      (∀ x, gradient (W p) x=gradient (F p) x) ∧
      (∀ n, (fun x => x-((β:ℝ)+bp p.1)⁻¹ • gradient (W p) x)^[n] p.2.1 =
        (T p)^[n] p.2.1) ∧
      ‖gradient (fun x => F p ((Real.sqrt ((β:ℝ)+bp p.1))⁻¹ • x))
          (Real.sqrt ((β:ℝ)+bp p.1) • out p)‖^2 ≤
        d/(((β:ℝ)+bp p.1)/((α:ℝ)+bp p.1))) ∧
    ∃ P : Kernel (RefState E) (RefState E), IsMarkovKernel P ∧
      (∀ s, P s=if threshold ≤ s.1 then Measure.dirac s else
        ((M s).prod (stdGaussian E)).map (fun z => update (s,z))) ∧
      (∀ s, (P s).map project=if threshold ≤ s.1 then Measure.dirac (project s) else
        ((M s).prod (stdGaussian E)).map (fun z => oldUpdate (s,z))) := by
  classical
  intro d v bp obs center F W T q N out update project oldUpdate
  have hβ : 0 < (β:ℝ) := lt_of_lt_of_le (show 0 < (α:ℝ) from hα) (show (α:ℝ) ≤ β from hαβ)
  have hv (s : RefState E) : 0 < v s :=
    div_pos (add_pos (hη0 s) (hτ0 s)) (add_pos_of_pos_of_nonneg hβ s.1.coe_nonneg)
  have hbp (s : RefState E) : (bp s:ℝ)=(s.1:ℝ)+(v s)⁻¹ := by
    simp only [bp,NNReal.coe_add,Real.coe_toNNReal _ (inv_pos.mpr (hv s)).le]
  have hbp0 (s : RefState E) : 0 < (bp s:ℝ) := by
    rw [hbp]
    exact add_pos_of_nonneg_of_pos s.1.coe_nonneg (inv_pos.mpr (hv s))
  have hvm : Measurable v := by dsimp [v]; fun_prop
  have hbpm : Measurable bp := by dsimp [bp]; fun_prop
  have hobsm : Measurable obs := by dsimp [obs]; fun_prop
  have hcm : Measurable center := by dsimp [center]; fun_prop
  have hbpm' : Measurable (fun p : RefState E × (E × E) => (bp p.1:ℝ)) := by fun_prop
  have href := variable_reference hV hH hαβ hd hbpm' (fun p => hbp0 p.1) hcm
    (by fun_prop : Measurable (fun p : RefState E × (E × E) => p.2.1))
  have hNm : Measurable N := href.1
  have hom : Measurable out := href.2.1
  have hum : Measurable update := by
    dsimp [update]
    apply Measurable.prodMk (by fun_prop)
    apply Measurable.prodMk hcm
    apply Measurable.prodMk hom
    apply Measurable.prodMk (by fun_prop)
    apply measurable_pi_lambda
    intro n
    cases n <;> fun_prop
  have hproj : Measurable project := by dsimp [project]; fun_prop
  refine ⟨fun s => ⟨hv s,hbp s⟩,hNm,hom,hum,?_,?_⟩
  · intro p
    have hp := href.2.2.2 p
    have hs := quadratic_source_alignment V p.1.1.coe_nonneg (inv_pos.mpr (hv p.1)) p.1.2.1 (obs p)
    have hsrc :
        (∀ x, W p x=F p x+(p.1.1:ℝ)*(v p.1)⁻¹/(2*((p.1.1:ℝ)+(v p.1)⁻¹))*‖p.1.2.1-obs p‖^2) ∧
        (∀ x, gradient (W p) x=gradient (F p) x) ∧
        ∀ (h : ℝ) (n : ℕ) (x : E),
          (fun z => z-h • gradient (W p) z)^[n] x=(fun z => z-h • gradient (F p) z)^[n] x := by
      simpa only [F,W,center,hbp] using hs
    refine ⟨hp.1,hp.2,href.2.2.1 p,hsrc.1,hsrc.2.1,fun n => hsrc.2.2 _ n _,?_⟩
    have hFd : Differentiable ℝ (F p) :=
      (hV.add (contDiff_const.mul ((contDiff_id.sub contDiff_const).norm_sq (𝕜:=ℝ)))).differentiable
        (by norm_num)
    exact scaled_reference_bound hFd (add_pos_of_pos_of_nonneg hβ (bp p.1).coe_nonneg) hp.1
  · let Q : Kernel (RefState E) (E × E) := M ×ₖ Kernel.const _ (stdGaussian E)
    have hQ : IsMarkovKernel Q := by dsimp [Q]; infer_instance
    let C := (Kernel.id ×ₖ Q).map update
    have hC : IsMarkovKernel C := Kernel.IsMarkovKernel.map _ hum
    have hCs (s : RefState E) : C s=((M s).prod (stdGaussian E)).map (fun z => update (s,z)) := by
      dsimp only [C]
      rw [Kernel.map_apply _ hum,Kernel.prod_apply,Kernel.id_apply,Measure.dirac_prod,
        Measure.map_map hum (by fun_prop)]
      simp only [Q,Kernel.prod_apply,Kernel.const_apply]
      rfl
    let D : Set (RefState E) := {s | threshold ≤ s.1}
    have hD : MeasurableSet D := measurableSet_le measurable_const (by fun_prop)
    let P := Kernel.piecewise hD Kernel.id C
    have hP : IsMarkovKernel P := by dsimp [P]; infer_instance
    have hPs (s : RefState E) : P s=if threshold ≤ s.1 then Measure.dirac s else
        ((M s).prod (stdGaussian E)).map (fun z => update (s,z)) := by
      simp only [P,Kernel.piecewise_apply,D,mem_ofPred_eq,Kernel.id_apply,hCs]
    refine ⟨P,hP,hPs,fun s => ?_⟩
    rw [hPs]
    by_cases hs : threshold ≤ s.1
    · rw [if_pos hs,if_pos hs,Measure.map_dirac' hproj]
    · have hm : Measurable (fun z : E × E => update (s,z)) := hum.comp measurable_prodMk_left
      rw [if_neg hs,if_neg hs,Measure.map_map hproj hm]
      rfl

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ReferenceCarryingKernel

Exact module and namespace context

Scope and omitted-condition boundaries

  • Actual single-step enhanced Markov program,not a sampler-accuracy or cost theorem. M outputs and stored reference are in original coordinates. theta is supplied: positive theta corresponds to A<=Abar iff b>=1/Abar; exact source threshold and finite reachability remain open. theta=0 immediately absorbs. Terminal self-loop neither runs FORS nor returns a final sample. Old reference admissibility and valid initial history are not required. General beta and coordinate-free positive dimension extend the normalized source; alpha,eta,tau are positive,b may be zero. Since M,eta,tau can depend on the deleted reference,one-step projection does not imply that the whole projected process is Markov. No conditional precision,query count,tail,full Gibbs normalization or either main result is concluded.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • measurable_find
  • Measurable.find
  • fderiv_add_const
  • ProbabilityTheory.Kernel.map_apply
  • ProbabilityTheory.Kernel.prod_apply
  • ProbabilityTheory.Kernel.piecewise_apply
  • MeasureTheory.Measure.map_map

Mathematical sources

  • SPHMC Algorithm3.3 and Section6.3 actual next reference — Actual single-step enhanced Markov program,not a sampler-accuracy or cost theorem. M outputs and stored reference are in original coordinates. theta is supplied: positive theta corresponds to A<=Abar iff b>=1/Abar; exact source threshold and finite reachability remain open. theta=0 immediately absorbs. Terminal self-loop neither runs FORS nor returns a final sample. Old reference admissibility and valid initial history are not required. General beta and coordinate-free positive dimension extend the normalized source; alpha,eta,tau are positive,b may be zero. Since M,eta,tau can depend on the deleted reference,one-step projection does not imply that the whole projected process is Markov. No conditional precision,query count,tail,full Gibbs normalization or either main result is concluded.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.