This record deposits the M9 ξ₀-covariance results for polynomial continued fractions (PCFs) b (n) =βd nᵈ+…, with the SIARC four-way epistemic discipline made explicit. M9. 0 (object level). Each deposited family admits the invariant triple (Δd, ‖Δ‖Pet, ξ₀) with Borel-singularity radius ξ₀ (b) =d/βd^1/d; a map of objects, no morphism action asserted. M9. 1 (ξ₀ affine-reindexing covariance). For φ (n) =αn+γ, ξ₀ (b∘φ) =α⁻¹·ξ₀ (b), shift-invariant; grounded on the βd-only slope-1/d Newton-polygon edge and numerically VERIFIED for the computed pairs d∈2, 3, 4, α∈2, 3, γ∈0, 1. All-d lift M9. 1⁺. The algebraic core is symbolically derived (d-free) for all d≥2 — the edge polynomial χd (c) =1+ (−1) ^d+1 (βd/dᵈ) cᵈ (only βd on the edge) and the α⁻¹ covariance — carried by a symbolic-in-d leading-symbol lemma (not the d≤6 numerics, which only corroborate). “Symbolically derived” is a grade strictly weaker than the corpus's machine-checked PROVEN (a Lean axiom cone propext, Classical. choice, Quot. sound, zero sorry): there is no Lean formalization here, and the lemma's general-k step is a hand induction (k=0. . 8 machine-checked in sympy). The analytic edge⇒Borel-radius step references standard asymptotics literature (Wasow §19 sectorial-existence theory; Birkhoff–Trjitzinsky Borel-summability) and remains cited-conditional — it is NOT discharged here. \"VERIFIED\" is restricted to the computed (d, βd, φ) ; no d≥7 claim. Artifacts: a symbolic+numeric derivation script (lemma31ₑdgederivation. py), its raw output and results JSON, a derivation note, and an AEAL provenance ledger.
Papanokechi (Thu,) studied this question.