Prove restricted-run tableaux Conjecture 2a

[DomTheDeveloper]

Goal

Prove the Kauers–Zeilberger asymptotic

G(n) ~ C₁ · 8ⁿ / n⁴, with C₁ > 0,

for three-row ballot words whose maximal constant runs all have length at least two.

New exact mathematics

This branch now contains:

• an equal-weight six-state Markov representation of the restricted-run words;
• an exact martingale corrector and covariance calculation;
• the cone exponent p = 3, hence fixed-endpoint exponent p + d/2 = 4;
• explicit phase-harmonic cubics with leading term x y (x+y);
• a positive phase-harmonic majorant controlling the squared exit location;
• a finite, positive, exact killed harmonic function constructed by exit compensation;
• rational quadratic Poisson correctors replacing the state-independent covariance assumption;
• a finite-phase transfer of the Denisov–Zhang survival argument and Denisov–Wachtel conditioned/fixed-endpoint local-limit argument.

Verification

RestrictedRunTableaux/check_model.py uses exact rational arithmetic and checks:

• all transition probabilities and conditional means;
• stationary distribution and covariance;
• every polynomial harmonic identity coefficient-by-coefficient;
• positivity and reachable-exit signs;
• the quadratic covariance Poisson equations;
• the equal path-weight identity;
• the published initial values of G(n).

It currently prints:

PASS: exact restricted-run Markov-additive checks

Audit status

The finite algebraic and killed-harmonic portions are exact and independently executable. The finite-phase cone bridge transfer is written out in FinitePhaseConeBridge.md; it still needs a careful probability-theory audit before this can be called a completed published proof or ported to Lean/Formal Conjectures.

No sorry, axiom, or hidden assumption is being presented as a verified Lean proof.