Fraenkel's two conjectures on the P-positions of the $N$-heap Wythoff game (Conjecture 1 $\Rightarrow$ Conjecture 2), for all $N\ge3$

In the $N$-heap Wythoff game ($N\ge2$ heaps of sizes $p_1\le\dots\le p_N$) a move either removes any positive number of tokens from a single heap, or removes $a_i\ge0$ from heap $i$ for every $i$ simultaneously subject to $\sum_i a_i>0$ and $a_1\oplus\cdots\oplus a_N=0$ (where $\oplus$ is nim-sum); the last player to move wins ($N=2$ is classical Wythoff Nim). Fix the smallest $N-2$ heap sizes $K=(A^1,\dots,A^{N-2})$ and let $(A^1,\dots,A^{N-2},A^{N-1}_n,A^N_n)$, $n=0,1,2,\dots$, enumerate the P-positions with these first coordinates, ordered by $A^{N-1}_n$. Fraenkel conjectures: (Conjecture 1) there exist a finite set $T=T(K)$ and an index $m(K)$ with $A^{N-1}_n=\operatorname{mex}\big(\{A^{N-1}_i,A^N_i:0\le i<n\}\cup T\big)$ and $A^N_n=A^{N-1}_n+n$ for all $n\ge m(K)$; (Conjecture 2) $A^{N-1}_n=\lfloor n\varphi\rfloor+\varepsilon_n+a$ where $\varphi=(1+\sqrt5)/2$, $\varepsilon_n\in\{-1,0,1\}$, and $a=a(K)$, for all $n\ge M(K)$. Prove both for all $N\ge3$.

Acceptance. ADVANCES (each is an independent, publishable target): a proof of Conjecture 1 (which implies Conjecture 2) for a new $(N,K)$ family not covered by Sun-Zeilberger -- canonically $N=3$ with first heap in the range $11..K'$ for some new $K'>10$, or $N=4$ with a fixed small $K$ -- accompanied by a machine-checkable certificate. Walnut/Buchi-automaton constructions are accepted as proof when the automata and decision-procedure output are supplied and re-runnable, as are Lean-checkable finite certificates. FULLY RESOLVES: a uniform-in-$N$ proof of both conjectures for all $N\ge3$. Numerical verification of the P-position formulas for finitely many $n$, without a periodicity / automatic-sequence proof, does NOT qualify.