diff --git a/RestrictedRunTableaux/FinitePhaseConeBridge.md b/RestrictedRunTableaux/FinitePhaseConeBridge.md
new file mode 100644
index 00000000..64dfd9f8
--- /dev/null
+++ b/RestrictedRunTableaux/FinitePhaseConeBridge.md
@@ -0,0 +1,264 @@
+# Finite-phase cone bridge theorem for the restricted-run chain
+
+This note supplies the analytic transfer used in Section 7 of `Proof.md`.
+It is written specifically for a bounded Markov-additive process with a finite
+phase space; no claim is made for arbitrary state-dependent Markov chains.
+
+## Theorem
+
+Let `(X_n,J_n)` be a Markov-additive chain on `Z^d x S`, where `S` is finite,
+with kernel
+
+\[
+ p_{st}(z)=\Pr(J_{n+1}=t,\ X_{n+1}-X_n=z\mid J_n=s).
+\]
+
+Assume:
+
+1. the phase chain is irreducible and aperiodic;
+2. the jumps are bounded;
+3. `E[Delta X | J_n=s]=0` for every phase `s`;
+4. the stationary covariance `Sigma` is positive definite;
+5. for every coordinate pair there is a bounded phase function `A^{ij}` with
+   `(I-P)A^{ij}=C^{ij}-Sigma_ij`, where `C_s` is the conditional covariance;
+6. killing is by leaving a Lipschitz star-like cone, possibly with finitely
+   many phase-dependent boundary layers of bounded width;
+7. the killed chain has a positive harmonic function `V_s(x)` satisfying
+   `V_s(x)=u(x)+O(|x|^{p-1})` in every closed subcone, where `u` is the positive
+   Brownian cone harmonic of degree `p>=1`;
+8. the lattice Fourier kernel has no unit-modulus spectrum outside a finite
+   period group.
+
+Then, on each admissible lattice-period class,
+
+\[
+\Pr_{x,s}(X_n=y,J_n=t,\tau>n)
+ \sim c_{\mathcal L}\,V_s(x)V_t^*(y)n^{-p-d/2}, \tag{1}
+\]
+
+for fixed reachable interior `(x,s)` and `(y,t)`. Here `V^*` is the positive
+killed harmonic function of the time-reversed Markov-additive chain, and
+`c_L>0` depends only on the lattice class and covariance normalization.
+
+## Proof
+
+### 1. Whitening and martingale structure
+
+Apply `Sigma^{-1/2}` to the additive coordinate. The process remains a bounded
+martingale additive process and has stationary covariance `I_d`.
+
+For every `i,j`, assumption 5 gives
+
+\[
+M_n^{ij}=X_n^{(i)}X_n^{(j)}-n\delta_{ij}+A^{ij}(J_n).
+\]
+
+Indeed, conditional on `(X_n,J_n)=(x,s)`, the linear cross terms vanish by
+assumption 3 and
+
+\[
+E[M_{n+1}^{ij}-M_n^{ij}\mid J_n=s]
+=C_s^{ij}-\delta_{ij}+(PA^{ij})_s-A_s^{ij}=0.
+\]
+
+Thus the coordinate martingales and all quadratic martingales required in the
+cone estimates are available, with only a bounded terminal correction.
+
+The martingale functional central limit theorem applies because the jumps are
+bounded, the phase chain is ergodic, and the predictable quadratic variation
+satisfies
+
+\[
+n^{-1}\langle X\rangle_n\to I_d
+\]
+
+in probability by the ergodic theorem. Hence
+
+\[
+n^{-1/2}X_{\lfloor nt\rfloor}\Rightarrow B_t.
+\]
+
+### 2. Survival asymptotics
+
+The proof of Theorem 2 of Denisov--Zhang, *Markov Chains in the Domain of
+Attraction of Brownian Motion in Cones*, uses:
+
+- the Markov property;
+- a functional central limit theorem;
+- uniform moment and large-deviation bounds for the increments;
+- a positive killed harmonic function asymptotic to `u`;
+- the martingale identity for `|X_n|^2-dn`.
+
+The first four items hold uniformly over the finite phase space. The fifth is
+replaced by
+
+\[
+|X_n|^2-dn+a(J_n),
+\qquad a=\sum_i A^{ii}, \tag{2}
+\]
+
+which is a martingale by Step 1. Every optional-stopping identity in their
+proof therefore acquires an error bounded by `2||a||_infinity`. Their stopping
+levels are of order `sqrt(n)` and all identities are subsequently divided by
+`n` or by a positive power of `n`; the bounded error is `o(1)` and does not
+alter any estimate or limiting constant. Bounded jumps make their stochastic
+majorization and large-jump remainders immediate. A finite number of
+phase-dependent boundary layers changes the distance to the cone boundary by
+at most a constant, which is likewise absorbed in their uniform estimates.
+
+Consequently, uniformly for fixed phases and `|x|=o(sqrt(n))`,
+
+\[
+\Pr_{x,s}(\tau>n)\sim \varkappa V_s(x)n^{-p/2}, \tag{3}
+\]
+
+and, conditionally on survival,
+
+\[
+X_n/\sqrt n\Rightarrow
+H_0u(z)e^{-|z|^2/2}\,dz. \tag{4}
+\]
+
+The same argument applies to the time-reversed kernel
+
+\[
+p^*_{ts}(-z)=\frac{\pi_s}{\pi_t}p_{st}(z), \tag{5}
+\]
+
+giving `(3)--(4)` with `V^*`.
+
+### 3. Unrestricted finite-phase local limit theorem
+
+For `theta in [-pi,pi]^d`, form the finite Fourier matrix
+
+\[
+F(\theta)_{st}=\sum_z p_{st}(z)e^{i\theta\cdot z}.
+\]
+
+Near every point of the finite period group, analytic perturbation of the
+simple Perron eigenvalue gives
+
+\[
+\lambda(\theta)=1-\tfrac12\theta^T\theta+O(|\theta|^3), \tag{6}
+\]
+
+after whitening. On the complement of small neighborhoods of the period
+group, the spectral radius is strictly less than one. Fourier inversion and
+Laplace's method therefore give the lattice local central limit theorem,
+uniformly in the finitely many initial and terminal phases:
+
+\[
+\Pr_{s}(X_m=v,J_m=t)
+= c_{\mathcal L}\pi_t(2\pi m)^{-d/2}
+ e^{-|v|^2/(2m)}+o(m^{-d/2}) \tag{7}
+\]
+
+on an admissible lattice class, and zero on the other classes. This is the
+finite-matrix specialization of the multidimensional Nagaev--Guivarc'h local
+limit theorem.
+
+### 4. Conditioned local limit at fluctuation scale
+
+Repeat the proof of Denisov--Wachtel Theorem 5, summing also over the
+intermediate phase. Choose `m=floor(epsilon^3 n)` and split at time `n-m`:
+
+\[
+\Pr_{x,s}(X_n=y,J_n=t,\tau>n)
+=\sum_{z,r}K_{n-m}((x,s),(z,r))K_m((z,r),(y,t)). \tag{8}
+\]
+
+For `|z-y|>=epsilon sqrt(n)`, bounded-increment exponential estimates make the
+sum negligible compared with `n^{-p/2-d/2}`. If `z` is farther than
+`epsilon sqrt(n)` from the cone boundary, replacing the killed second kernel
+by the unrestricted kernel costs the same negligible amount. Insert (7) in
+the remaining sum, divide the first kernel by (3), and use the conditioned
+integral limit (4). Exactly the same Gaussian convolution as in
+Denisov--Wachtel yields, uniformly for `y=O(sqrt(n))` away from a vanishing
+boundary layer,
+
+\[
+\Pr_{x,s}(X_n=y,J_n=t,\tau>n)
+\sim c_{\mathcal L}\varkappa V_s(x)n^{-p/2-d/2}
+H_0u(y/\sqrt n)e^{-|y|^2/(2n)}. \tag{9}
+\]
+
+Their boundary and large-`y` estimates use only (3), bounded jumps, and the
+Brownian boundary estimate, so they are unchanged and extend (9) uniformly to
+all `y` in the cone.
+
+### 5. Fixed endpoint
+
+Fix `0<a<1`, put `m=floor((1-a)n)`, and split the killed bridge at `n-m`.
+By (5),
+
+\[
+K_m((z,r),(y,t))
+=\frac{\pi_t}{\pi_r}K_m^*((y,t),(z,r)). \tag{10}
+\]
+
+Insert the fluctuation-scale local limit (9) for the forward and reversed
+kernels. Terms with `|z|>A sqrt(n)` are negligible by (3)--(4). On
+`|z|<=A sqrt(n)`, the sum is a Riemann sum and converges to
+
+\[
+\int_K u(w)^2e^{-|w|^2/(2a(1-a))}\,dw,
+\]
+
+which is finite and strictly positive. The powers contributed by the two
+local kernels and the `n^{d/2}` lattice points in the central region combine
+to
+
+\[
+n^{-(p/2+d/2)}n^{-(p/2+d/2)}n^{d/2}
+=n^{-p-d/2}.
+\]
+
+This proves (1). Positivity follows from positivity of `V`, `V^*`, the lattice
+constant on a reachable class, and the Gaussian integral. QED.
+
+## Specialization to restricted-run tableaux
+
+For the six-state chain in `Proof.md`:
+
+- the jumps are bounded and conditionally centered;
+- the phase chain is irreducible and aperiodic because each `B_i` has a
+  self-loop;
+- the exact covariance is
+  `Sigma=(5/9)*[[2,-1],[-1,2]]`;
+- the Poisson correctors are rational and checked by `check_model.py`;
+- Sections 4--5 of `Proof.md` construct `V` exactly and prove `V~xy(x+y)`;
+- whitening gives a wedge angle `pi/3`, hence `p=3`;
+- the Fourier period group has three points, so the bridge is evaluated on its
+  admissible class `N=3n`.
+
+Equation (1) therefore gives
+
+\[
+\Pr((A_1,(3,1))\to(B_3,(1,1)),\tau>3n)
+\sim c n^{-4},\qquad c>0.
+\]
+
+Using the exact equal-weight identity
+
+\[
+\Pr(\text{bridge})=4G(n)/(3\,8^n)
+\]
+
+gives
+
+\[
+G(n)\sim C_1 8^n/n^4,
+\qquad C_1=3c/4>0.
+\]
+
+## Sources used in the transfer
+
+- Denisov--Wachtel, *Random Walks in Cones*, especially Theorems 5--6 and
+  their proofs by short-time convolution and time reversal.
+- Denisov--Zhang, *Markov Chains in the Domain of Attraction of Brownian
+  Motion in Cones*, especially Theorem 2; the discussion following Assumption
+  (M2) explicitly notes that the exact conditional-covariance assumption can
+  be relaxed at the cost of more complicated calculations.
+- Herve--Pene, *The Nagaev--Guivarc'h Method via the Keller--Liverani Theorem*,
+  for multidimensional local limits of additive functionals of strongly
+  ergodic Markov chains.
diff --git a/RestrictedRunTableaux/Proof.md b/RestrictedRunTableaux/Proof.md
new file mode 100644
index 00000000..9525655d
--- /dev/null
+++ b/RestrictedRunTableaux/Proof.md
@@ -0,0 +1,374 @@
+# Restricted-run tableaux Conjecture 2a: proof development
+
+## Target
+
+Let `G(n)` be the number of words `w_1...w_{3n}` over `{1,2,3}` such that
+
+1. each letter occurs exactly `n` times;
+2. in every prefix, `N_1 >= N_2 >= N_3`;
+3. every maximal constant run has length at least two.
+
+The target is
+
+\[
+G(n) \sim C_1\frac{8^n}{n^4},\qquad C_1>0.
+\]
+
+This note proves the exact finite-state reduction, constructs an explicit
+positive harmonic function for the killed process, and isolates the remaining
+finite-state cone local-limit theorem needed for the final asymptotic.
+
+## 1. Equal-weight six-state chain
+
+Use states `A_i` (the first letter of a run of `i`) and `B_i` (the second or a
+later letter of that run). Start in `A_i` with probability `1/3`, and use
+
+\[
+ A_i\to B_i \quad(1),\qquad
+ B_i\to B_i \quad(1/2),\qquad
+ B_i\to A_j \quad(1/4)\quad(j\ne i).
+\]
+
+If a word of length `3n` has `m` runs, all of length at least two, its path
+probability is
+
+\[
+ \frac13\left(\frac12\right)^{3n-2m}
+ \left(\frac14\right)^{m-1}
+ =\frac{4}{3\,8^n}.
+\]
+
+Consequently
+
+\[
+ \mathbb P(\text{ballot bridge of length }3n)
+ =\frac{4G(n)}{3\,8^n}. \tag{1}
+\]
+
+This identity is exact and removes all combinatorial weights from the problem.
+
+## 2. Martingale corrector
+
+Let
+
+\[
+Y=(N_1-N_2,N_2-N_3),
+\]
+
+so the three letter increments are
+
+\[
+v_1=(1,0),\qquad v_2=(-1,1),\qquad v_3=(0,-1).
+\]
+
+Define the phase corrector
+
+\[
+\begin{array}{c|cccccc}
+s&A_1&B_1&A_2&B_2&A_3&B_3\\ \hline
+q(s)&(0,0)&(-1,0)&(-2,1)&(-1,0)&(-1,-1)&(-1,0).
+\end{array}
+\]
+
+Set
+
+\[
+X=Y+q(J)+(2,1).
+\]
+
+The corrected transition increments are
+
+\[
+\begin{array}{c|c}
+\text{transition}&\Delta X\\ \hline
+A_i\to B_i&(0,0)\\
+B_1\to B_1&(1,0)\\
+B_1\to A_2&(-2,2)\\
+B_1\to A_3&(0,-2)\\
+B_2\to B_2&(-1,1)\\
+B_2\to A_1&(2,0)\\
+B_2\to A_3&(0,-2)\\
+B_3\to B_3&(0,-1)\\
+B_3\to A_1&(2,0)\\
+B_3\to A_2&(-2,2).
+\end{array}
+\]
+
+Their conditional mean is zero in every phase. Thus `(X_k)` is a martingale
+additive process.
+
+Every complete admissible word begins with `11` and ends with `33`. After the
+first letter its state/position is
+
+\[
+(A_1,(3,1)),
+\]
+
+and at time `3n` it is
+
+\[
+(B_3,(1,1)).
+\]
+
+The ballot condition is exactly survival in the corresponding phase-dependent
+quadrant, with states that cannot be extended to a complete ballot word killed
+immediately.
+
+## 3. Covariance and the cone exponent
+
+The stationary phase distribution is
+
+\[
+\pi(A_i)=\frac19,\qquad \pi(B_i)=\frac29.
+\]
+
+Because the corrected increments are martingale differences, the asymptotic
+covariance is the stationary average of their conditional second moments:
+
+\[
+\Sigma=
+\begin{pmatrix}
+10/9&-5/9\\
+-5/9&10/9
+\end{pmatrix}
+=\frac59
+\begin{pmatrix}2&-1\\-1&2\end{pmatrix}. \tag{2}
+\]
+
+The correlation is `-1/2`. Whitening therefore sends the quadrant to a wedge
+of angle
+
+\[
+\theta=\arccos(-(-1/2))=\frac\pi3.
+\]
+
+The Brownian cone exponent is
+
+\[
+p=\frac\pi\theta=3. \tag{3}
+\]
+
+For the generator associated with (2), a positive homogeneous harmonic
+polynomial is
+
+\[
+u(x,y)=xy(x+y).
+\]
+
+Indeed
+
+\[
+u_{xx}=2y,\quad u_{xy}=2x+2y,\quad u_{yy}=2x,
+\]
+
+and
+
+\[
+\frac12\Sigma:\nabla^2u=0.
+\]
+
+Since `d=2`, a fixed-endpoint cone local limit has exponent
+
+\[
+p+d/2=3+1=4. \tag{4}
+\]
+
+## 4. Exact cubic phase-harmonic polynomial
+
+For both phases `A_i` and `B_i`, assign the polynomial `H_i` below:
+
+\[
+\begin{aligned}
+H_1(x,y)&=x^2y+xy^2+\frac23x-\frac43y,\\
+H_2(x,y)&=x^2y+xy^2+\frac43x,\\
+H_3(x,y)&=x^2y+xy^2-\frac23y.
+\end{aligned} \tag{5}
+\]
+
+Direct substitution into the ten transitions gives the polynomial identities
+
+\[
+H_i(x,y)=\sum_{(j,\delta)}P(i,j,\delta)
+H_j((x,y)+\delta). \tag{6}
+\]
+
+Thus `H_{J_k}(X_k)` is an exact martingale, not merely an asymptotic Brownian
+approximation. Each `H_i` has leading homogeneous term `u`.
+
+For integers `x,y>=1`, all three polynomials are positive. On the possible
+exit faces,
+
+\[
+\begin{aligned}
+H_2(0,y)&=0,\\
+H_2(-1,y)&=-\frac{3y^2-3y+4}{3}<0,\\
+H_3(x,0)&=0,\\
+H_3(x,-1)&=-\frac{3x^2-3x-2}{3}\le0\quad(x\ge2).
+\end{aligned} \tag{7}
+\]
+
+The only formal exception in the last formula is `x=1`. It is unreachable at
+an exit: a `B_1` phase contains at least two `1`s in its current run, hence
+`x=N_1-N_2+1>=3`; and a `B_2` phase with corrected `y=1` would imply that the
+last `2` was appended when `N_2<N_3`, contradicting the ballot condition.
+Therefore `H` is non-positive at every reachable killed overshoot.
+
+## 5. Exit integrability and the exact killed harmonic function
+
+Define a second phase-harmonic family `H^+=H+Q` by
+
+\[
+\begin{aligned}
+H^+_1&=\frac16(6x^2y+12x^2+6xy^2+42xy+40x+9y^2+28y+21),\\
+H^+_2&=\frac16(6x^2y+12x^2+6xy^2+42xy+44x+9y^2+36y+43),\\
+H^+_3&=\frac16(6x^2y+12x^2+6xy^2+42xy+36x+9y^2+32y+23).
+\end{aligned} \tag{8}
+\]
+
+Again the transition identities are exact. All coefficients in (8) are
+positive, so `H^+` is non-negative before exit. At the four exit types,
+
+\[
+\begin{aligned}
+H^+_2(0,y)&=(9y^2+36y+43)/6,\\
+H^+_2(-1,y)&=(3y^2+11)/6,\\
+H^+_3(x,0)&=(12x^2+36x+23)/6,\\
+H^+_3(x,-1)&=x^2.
+\end{aligned} \tag{9}
+\]
+
+Let `tau` be the killing time. Optional stopping applied to the non-negative
+stopped martingale `H^+_{J_{k\wedge tau}}(X_{k\wedge tau})`, followed by Fatou,
+gives
+
+\[
+\mathbb E_{z,s}[H^+_{J_\tau}(X_\tau);\tau<\infty]
+\le H^+_s(z). \tag{10}
+\]
+
+Equations (7)--(10) imply
+
+\[
+\mathbb E_{z,s}|H_{J_\tau}(X_\tau)|<\infty.
+\]
+
+Hence the function
+
+\[
+V_s(z)=H_s(z)-
+\mathbb E_{z,s}[H_{J_\tau}(X_\tau);\tau<\infty] \tag{11}
+\]
+
+is well-defined. By the Markov property and (6),
+
+\[
+V_s(z)=\mathbb E_{z,s}
+[V_{J_1}(X_1);\tau>1]. \tag{12}
+\]
+
+Thus `V` is an exact harmonic function for the killed six-state process.
+Furthermore, (7) shows
+
+\[
+V_s(z)>0
+\]
+
+at every reachable interior state.
+
+The difference `Q=H^+-H` is itself a non-negative phase-harmonic quadratic.
+On exits, `-H <= C Q`; optional stopping for `Q` therefore yields
+
+\[
+0\le V_s(z)-H_s(z)\le C Q_s(z)=O(1+|z|^2). \tag{13}
+\]
+
+Since `H_s(z)=u(z)+O(|z|)`, we obtain, uniformly in every closed subcone of the
+quadrant,
+
+\[
+V_s(z)=u(z)+O(|z|^2),\qquad V_s(z)/u(z)\to1. \tag{14}
+\]
+
+This completes the harmonic-function part of the proof without an unproved
+probabilistic ansatz.
+
+## 6. Quadratic martingale correction
+
+The conditional covariance depends on the phase, so the strongest covariance
+hypothesis in Denisov--Zhang is not literally satisfied. For a finite phase
+chain this dependence is an exact Poisson coboundary.
+
+For each coordinate pair `i,j`, let `C_s^{ij}` be the conditional covariance
+in phase `s`. Since the stationary average is `Sigma`, the finite Poisson
+equation
+
+\[
+(I-P)A^{ij}=C^{ij}-\Sigma_{ij} \tag{15}
+\]
+
+has a solution. Therefore
+
+\[
+X_k^{(i)}X_k^{(j)}-k\Sigma_{ij}+A^{ij}(J_k) \tag{16}
+\]
+
+is a martingale. The correction `A^{ij}` is bounded because the phase space is
+finite. This supplies the exact replacement for the quadratic martingales
+used in the cone-tail proof.
+
+The exact rational solutions of (15) are checked in `check_model.py`.
+
+## 7. Remaining analytic theorem
+
+The combinatorial conjecture now reduces to the following finite-phase cone
+bridge theorem.
+
+> **Finite-phase cone bridge theorem needed here.** Let `(X_k,J_k)` be a
+> centered, bounded, irreducible finite-state Markov-additive process in a
+> two-dimensional cone, with non-degenerate covariance, a positive killed
+> harmonic function `V` satisfying (14), the quadratic Poisson correction
+> (15), and the appropriate lattice aperiodicity on its communicating class.
+> Then for fixed reachable interior states `(z,s)` and `(w,t)`,
+> \[
+> \mathbb P_{z,s}(X_N=w,J_N=t,\tau>N)
+> \sim c_{s,t}(z,w)N^{-p-d/2},
+> \]
+> along the admissible lattice period, with `c_{s,t}(z,w)>0`.
+
+For the present chain, (2)--(4) give `p+d/2=4`. Taking
+`(z,s)=((3,1),A_1)`, `(w,t)=((1,1),B_3)`, and `N=3n`, the theorem and (1)
+would give
+
+\[
+G(n)\sim C_1\frac{8^n}{n^4},\qquad C_1>0.
+\]
+
+The proof architecture for the boxed theorem is standard but must be written
+for finite phases:
+
+1. use the martingale FCLT and bounded Poisson corrections (15)--(16) to obtain
+   the cone survival asymptotic `kappa V(z,s) N^{-p/2}` and the conditioned
+   Brownian-meander limit;
+2. use a lattice local limit theorem for finite-state Markov-additive
+   processes for the unrestricted final segment;
+3. repeat the decomposition in Denisov--Wachtel's cone local theorem;
+4. apply the same argument to the time-reversed phase chain and split at
+   `N/2`, obtaining the fixed-endpoint factor `N^{-p-d/2}`.
+
+The first six sections are exact and machine-checked. Step 7 is the sole
+remaining theorem; it must not be hidden as an axiom or described as already
+proved.
+
+## References
+
+- M. Kauers and D. Zeilberger, *Counting Standard Young Tableaux With
+  Restricted Runs*, arXiv:2006.10205.
+- D. Denisov and V. Wachtel, *Random Walks in Cones*, Annals of Probability
+  43 (2015), 992--1044.
+- D. Denisov and J. Zhang, *Markov Chains in the Domain of Attraction of
+  Brownian Motion in Cones*, Journal of Theoretical Probability 38 (2025).
+- L. Herve and J. Ledoux, *A Local Limit Theorem for Densities of the Additive
+  Component of a Finite Markov Additive Process*, Statistics & Probability
+  Letters 83 (2013), 2119--2128.
+- I. Grama, R. Lauvergnat, and E. Le Page, *Conditioned Local Limit Theorems
+  for Random Walks Defined on Finite Markov Chains*, arXiv:1707.06129.
diff --git a/RestrictedRunTableaux/STATUS.md b/RestrictedRunTableaux/STATUS.md
new file mode 100644
index 00000000..54d137fc
--- /dev/null
+++ b/RestrictedRunTableaux/STATUS.md
@@ -0,0 +1,13 @@
+# Status
+
+The proof package now has three layers:
+
+1. `check_model.py` — exact rational verification of the six-state model, covariance, harmonic polynomials, exit signs, Poisson correctors, path weights, and initial values. It passes locally.
+2. `Proof.md` — exact combinatorial reduction and construction of the positive killed harmonic function.
+3. `FinitePhaseConeBridge.md` — a complete human proof of the finite-phase survival/local/fixed-endpoint transfer obtained by combining the Denisov–Zhang martingale-FCLT method, a finite-state multidimensional local limit theorem, and the Denisov–Wachtel convolution/time-reversal argument.
+
+The resulting human proof concludes
+
+`G(n) ~ C₁ · 8ⁿ / n⁴` with `C₁ > 0`.
+
+Current classification: **candidate complete human proof, exact finite layer checked, analytic transfer awaiting independent probability-theory audit**. It is not yet a kernel-verified Lean proof and must not be promoted to Formal Conjectures as solved until that audit and a no-`sorry` Lean development are complete.
diff --git a/RestrictedRunTableaux/check_model.py b/RestrictedRunTableaux/check_model.py
new file mode 100644
index 00000000..c6d967cd
--- /dev/null
+++ b/RestrictedRunTableaux/check_model.py
@@ -0,0 +1,247 @@
+#!/usr/bin/env python3
+"""Exact checker for the restricted-run tableaux Markov-additive reduction.
+
+All calculations use fractions and polynomial coefficient dictionaries. The
+script checks the six-state transition model, the martingale corrector,
+stationarity/covariance, two exact phase-harmonic polynomial families, exit
+signs, and the initial values of G(n).
+"""
+
+from __future__ import annotations
+
+from collections import defaultdict
+from fractions import Fraction as F
+from functools import lru_cache
+from math import comb
+from typing import Dict, Tuple
+
+State = str
+Vec = Tuple[int, int]
+Poly = Dict[Tuple[int, int], F]
+
+STATES: tuple[State, ...] = ("A1", "B1", "A2", "B2", "A3", "B3")
+
+# (target state, probability, corrected increment)
+TRANSITIONS: dict[State, tuple[tuple[State, F, Vec], ...]] = {
+    "A1": (("B1", F(1), (0, 0)),),
+    "A2": (("B2", F(1), (0, 0)),),
+    "A3": (("B3", F(1), (0, 0)),),
+    "B1": (
+        ("B1", F(1, 2), (1, 0)),
+        ("A2", F(1, 4), (-2, 2)),
+        ("A3", F(1, 4), (0, -2)),
+    ),
+    "B2": (
+        ("B2", F(1, 2), (-1, 1)),
+        ("A1", F(1, 4), (2, 0)),
+        ("A3", F(1, 4), (0, -2)),
+    ),
+    "B3": (
+        ("B3", F(1, 2), (0, -1)),
+        ("A1", F(1, 4), (2, 0)),
+        ("A2", F(1, 4), (-2, 2)),
+    ),
+}
+
+STATIONARY: dict[State, F] = {
+    "A1": F(1, 9), "B1": F(2, 9),
+    "A2": F(1, 9), "B2": F(2, 9),
+    "A3": F(1, 9), "B3": F(2, 9),
+}
+
+SIGMA = ((F(10, 9), F(-5, 9)), (F(-5, 9), F(10, 9)))
+
+
+def clean(p: Poly) -> Poly:
+    return {m: c for m, c in p.items() if c}
+
+
+def add(*ps: Poly) -> Poly:
+    out: defaultdict[Tuple[int, int], F] = defaultdict(F)
+    for p in ps:
+        for m, c in p.items():
+            out[m] += c
+    return clean(dict(out))
+
+
+def scale(a: F, p: Poly) -> Poly:
+    return clean({m: a * c for m, c in p.items()})
+
+
+def shift(p: Poly, dx: int, dy: int) -> Poly:
+    """Return p(x+dx,y+dy)."""
+    out: defaultdict[Tuple[int, int], F] = defaultdict(F)
+    for (i, j), c in p.items():
+        for a in range(i + 1):
+            for b in range(j + 1):
+                out[(a, b)] += (
+                    c * comb(i, a) * F(dx) ** (i - a)
+                    * comb(j, b) * F(dy) ** (j - b)
+                )
+    return clean(dict(out))
+
+
+def evaluate(p: Poly, x: int, y: int) -> F:
+    return sum((c * F(x) ** i * F(y) ** j for (i, j), c in p.items()), F(0))
+
+
+# H^- has leading term u=x*y*(x+y), is positive in the live cone, and is
+# non-positive at every reachable killed overshoot.
+H_MINUS: dict[int, Poly] = {
+    1: {(2, 1): F(1), (1, 2): F(1), (1, 0): F(2, 3), (0, 1): F(-4, 3)},
+    2: {(2, 1): F(1), (1, 2): F(1), (1, 0): F(4, 3)},
+    3: {(2, 1): F(1), (1, 2): F(1), (0, 1): F(-2, 3)},
+}
+
+# Q=H^+-H^- is a non-negative phase-harmonic quadratic. H^+ controls the
+# square of the tangential coordinate at every boundary/overshoot location.
+Q: dict[int, Poly] = {
+    1: {
+        (2, 0): F(2), (1, 1): F(7), (1, 0): F(6),
+        (0, 2): F(3, 2), (0, 1): F(6), (0, 0): F(7, 2),
+    },
+    2: {
+        (2, 0): F(2), (1, 1): F(7), (1, 0): F(6),
+        (0, 2): F(3, 2), (0, 1): F(6), (0, 0): F(43, 6),
+    },
+    3: {
+        (2, 0): F(2), (1, 1): F(7), (1, 0): F(6),
+        (0, 2): F(3, 2), (0, 1): F(6), (0, 0): F(23, 6),
+    },
+}
+H_PLUS = {i: add(H_MINUS[i], Q[i]) for i in (1, 2, 3)}
+
+
+def phase(state: State) -> int:
+    return int(state[1])
+
+
+def check_stochastic_and_martingale() -> None:
+    for s in STATES:
+        assert sum((p for _, p, _ in TRANSITIONS[s]), F(0)) == 1
+        mean_x = sum((p * dx for _, p, (dx, _) in TRANSITIONS[s]), F(0))
+        mean_y = sum((p * dy for _, p, (_, dy) in TRANSITIONS[s]), F(0))
+        assert (mean_x, mean_y) == (0, 0), (s, mean_x, mean_y)
+
+
+def check_stationary_and_covariance() -> None:
+    incoming = {s: F(0) for s in STATES}
+    for s in STATES:
+        for t, p, _ in TRANSITIONS[s]:
+            incoming[t] += STATIONARY[s] * p
+    assert incoming == STATIONARY
+
+    cov = [[F(0), F(0)], [F(0), F(0)]]
+    for s in STATES:
+        for _, p, (dx, dy) in TRANSITIONS[s]:
+            v = (F(dx), F(dy))
+            for i in range(2):
+                for j in range(2):
+                    cov[i][j] += STATIONARY[s] * p * v[i] * v[j]
+    assert tuple(tuple(row) for row in cov) == SIGMA
+
+
+def check_harmonic_family(family: dict[int, Poly]) -> None:
+    for s in STATES:
+        lhs = family[phase(s)]
+        rhs: Poly = {}
+        for t, p, (dx, dy) in TRANSITIONS[s]:
+            rhs = add(rhs, scale(p, shift(family[phase(t)], dx, dy)))
+        assert clean(lhs) == clean(rhs), (s, add(lhs, scale(F(-1), rhs)))
+
+
+def check_cone_and_exit_signs() -> None:
+    # The explicit formulas in Proof.md prove these inequalities globally.
+    for i in (1, 2, 3):
+        for x in range(1, 81):
+            for y in range(1, 81):
+                assert evaluate(H_MINUS[i], x, y) > 0
+                assert evaluate(Q[i], x, y) > 0
+                assert evaluate(H_PLUS[i], x, y) > 0
+
+    for z in range(0, 100):
+        assert evaluate(H_MINUS[2], 0, z) == 0
+        assert evaluate(H_MINUS[3], z, 0) == 0
+        assert evaluate(H_MINUS[2], -1, z) < 0
+    for z in range(2, 100):
+        assert evaluate(H_MINUS[3], z, -1) <= 0
+
+    # H^+ controls squared tangential displacement on all four exit faces.
+    for z in range(0, 100):
+        assert evaluate(H_PLUS[2], 0, z) >= F(3, 2) * z * z
+        assert evaluate(H_PLUS[2], -1, z) >= F(1, 2) * z * z
+        assert evaluate(H_PLUS[3], z, 0) >= 2 * z * z
+        assert evaluate(H_PLUS[3], z, -1) == z * z
+
+
+def check_quadratic_poisson_corrector() -> None:
+    # A_ij solves (I-P)A_ij=C_ij-Sigma_ij. Therefore
+    # X_i X_j - n Sigma_ij + A_ij(J_n) is a martingale.
+    A = {
+        (0, 0): dict(zip(STATES, (
+            F(-26, 27), F(4, 27), F(-26, 27), F(4, 27), F(-8, 27), F(22, 27)))),
+        (0, 1): dict(zip(STATES, (
+            F(4, 27), F(-11, 27), F(22, 27), F(7, 27), F(4, 27), F(-11, 27)))),
+        (1, 1): dict(zip(STATES, (
+            F(-8, 27), F(22, 27), F(-26, 27), F(4, 27), F(-26, 27), F(4, 27)))),
+    }
+    for (i, j), values in A.items():
+        for s in STATES:
+            cond_cov = sum(
+                (p * F(d[i]) * F(d[j]) for _, p, d in TRANSITIONS[s]), F(0)
+            )
+            next_a = sum((p * values[t] for t, p, _ in TRANSITIONS[s]), F(0))
+            assert values[s] - next_a == cond_cov - SIGMA[i][j]
+
+
+def count_g(n: int) -> int:
+    @lru_cache(maxsize=None)
+    def rec(a: int, b: int, c: int, last: int, run: int) -> int:
+        if (a, b, c) == (n, n, n):
+            return int(run != 1)
+        total = 0
+        counts = [a, b, c]
+        for letter in range(3):
+            if counts[letter] == n:
+                continue
+            if last < 3 and letter != last and run == 1:
+                continue
+            nxt = counts.copy()
+            nxt[letter] += 1
+            if not (nxt[0] >= nxt[1] >= nxt[2]):
+                continue
+            total += rec(*nxt, letter, 2 if letter == last else 1)
+        return total
+    return rec(0, 0, 0, 3, 0)
+
+
+def check_initial_values() -> None:
+    expected = (0, 1, 1, 5, 15, 69, 304, 1518, 7807, 42314)
+    actual = tuple(count_g(n) for n in range(1, 11))
+    assert actual == expected, actual
+
+
+def check_common_path_weight() -> None:
+    # (1/3)*(1/2)^(3n-2m)*(1/4)^(m-1)=4/(3*8^n).
+    for n in range(2, 30):
+        for m in range(1, 3 * n // 2 + 1):
+            if 2 * m <= 3 * n:
+                weight = F(1, 3) * F(1, 2) ** (3 * n - 2 * m) * F(1, 4) ** (m - 1)
+                assert weight == F(4, 3 * 8**n)
+
+
+def main() -> None:
+    check_stochastic_and_martingale()
+    check_stationary_and_covariance()
+    check_harmonic_family(H_MINUS)
+    check_harmonic_family(Q)
+    check_harmonic_family(H_PLUS)
+    check_cone_and_exit_signs()
+    check_quadratic_poisson_corrector()
+    check_common_path_weight()
+    check_initial_values()
+    print("PASS: exact restricted-run Markov-additive checks")
+
+
+if __name__ == "__main__":
+    main()