The companion's Pellet and Newton-Kantorovich soundness both bottom out in Hex.taylor, whose committed shape is an in-place double List.foldl over Array.setIfInBounds (HexRoots/Taylor.lean). Proving (taylor p z).getD k _ = Σ_{j ≥ k} binom(j,k)·aⱼ·z^{j−k} (equivalently the (p.comp (X + z)).coeff k cast) through the fold is a substantial burden to leave to the companion. Phase-2 downstream review proposed committing a characterization lemma (or an equivalent structural reformulation plus semantic lemma) in hex-roots so the companion cites it. Proof-ergonomics only; the data-level def is correct and audited.
🤖 Prepared with Claude Code
The companion's Pellet and Newton-Kantorovich soundness both bottom out in
Hex.taylor, whose committed shape is an in-place doubleList.foldloverArray.setIfInBounds(HexRoots/Taylor.lean). Proving(taylor p z).getD k _ = Σ_{j ≥ k} binom(j,k)·aⱼ·z^{j−k}(equivalently the(p.comp (X + z)).coeff kcast) through the fold is a substantial burden to leave to the companion. Phase-2 downstream review proposed committing a characterization lemma (or an equivalent structural reformulation plus semantic lemma) in hex-roots so the companion cites it. Proof-ergonomics only; the data-level def is correct and audited.🤖 Prepared with Claude Code