The Yellowstone permutation: Conjecture 7 for all n reduced to a riser law on a finite range, the normality and entry times of primes, and a run certificate

Conjecture 7 for all n is not proved in this manuscript. For the Yellowstone permutation a (OEIS A098550), Conjecture 7 asserts a(n) <= (pi/2) n ln n for n >= 2; the earlier manuscripts of the series prove it for n >= n_0 with an ineffective n_0. This manuscript collects, as one account with proof sketches and references to the program's notes, the results on the conjecture for all n. (1) A certified computation (RC) of a(1), ..., a(N0), N0 = 8.3*10^10, by two programs whose hashes agree at 830 checkpoints on one machine; (RC) is a run certificate, not a proof, and gives Conjecture 7 for n <= N0. (2) A reduction: Conjecture 7 for all n follows from (RC), a hypothesis (NL) on primes (every prime r > 40,631,100,479 is normal, i.e. enters as 2r followed two steps later by r, and has entry index n_r >= 1.01 r), the riser law (S_LR) for t in the finite range [N0, e^143) only (e^143 is about 10^62), and computed tables (DATA; certified except one floating-point table; one interval re-certification assumes the platform libm within 4 ulp). (NL) quantifies over all large primes, so this is not a finite-range reduction; only the height input has been confined to a finite range. (3) A height theorem: under the hypotheses of the program's Lemma LIN-ROUGH, a(n) <= (pi/2) n ln n at every composite-anchored step with ln n >= 143 (certified cells up to ln n = 10^7 and an analytic tail beyond), proved by forcing too many risers. (4) From (RC) and refereed lemmas alone, every prime in (40,631,100,479, 4.105*10^10] is normal, and no prime in (40,631,100,479, 4.2583*10^10] enters as 3r. (5) For primes p > 40,631,100,479 with q_p = 2, under normality of the primes below p, the run data and the floating-point table of GIILE, the entry bound (LE*) holds at every such p <= 1.6503*10^11 for every entry mask, and below 10^300 a failure needs a "core lock" of consecutive entry masks. (6) With no normality, run or stock input, n_P >= 0.7444 P for every prime P > exp(2*10^452); this proof has no numerics referee, uses floating-point data, two of its inputs were refereed only once, and the threshold rests on a stated modification of the proofs (the exact band parameter H). The manuscript also records where the height method stops: its yield cap is at most 0.863 at N0 and exceeds 1 stably only from ln n about 29.4 (uncertified double-precision values), so this family of bounds cannot reach N0. Open: (S_LR) on [N0, e^143); normality beyond 4.105*10^10; (LE*) on (1.6503*10^11, 10^300] in the core-locked case and on (10^300, exp(2*10^452)] for entry masks of small density; and hence Conjecture 7 for all n. AI-assistance and review status: The mathematical content was produced by AI agents (Anthropic Claude) in the author's research program on OEIS A098550, and the text was written by AI writer and fixer agents from the program's internal notes, synthesis and referee records. Each theorem marked as proved rests on unpublished program notes with two independent AI proof referees (separate Claude instances that had not written the text under review) and, where there are numerics, one AI numerics referee, with the exceptions stated in the manuscript (inputs refereed once; the effective top entry law has no numerics referee). The assembled version 1.0 was checked as a whole by two further AI referees, REF-616 (mathematics and fidelity to the sources) and REF-617 (citations, status claims and wording); their fixes were applied by an AI fixer agent, and the fixed text was verified by one more AI referee, REF-618 (READY WITH FIXES, no new mathematical error). REF-618's remaining wording and citation fixes were applied in the release copy without a further referee pass. Details are in the title-page footnote and the section "Limitations and verification" of the manuscript. All referee reports cited are AI-generated. No part has been reviewed by a human mathematician. Dependencies: Part I (doi:10.5281/zenodo.23437783), Part II (doi:10.5281/zenodo.23449375), Part III (doi:10.5281/zenodo.23557280), the manuscript on the linear prime frontier (doi:10.5281/zenodo.23558450), the manuscript on limsup R(t)/t < 1 (doi:10.5281/zenodo.23604646), the manuscript on limsup R(t)/t <= 0.68605 (doi:10.5281/zenodo.23604811), and classical results (Rosser-Schoenfeld, Robin, Dusart, Selberg's upper sieve, Legendre's count, Bonferroni's inequalities). The run certificate RUN-CERT and the program notes (among them C7GEYSER, GIILINR, GIIWGTH, GIICASEB, GIILOWER, GIIFLOW, GIISCALE, GIIDOWN, GIIANCH, GIIQ3, GIIARRIV, GIITOPB, GIIROOM, GIIMSEQ, GIIEFFLE, GIINORM, GIILE, and the synthesis GIISYN) are internal, unpublished program notes and are not published with this manuscript.