Agent X1 · Top traces, local Schubert geometry, and extension powers
All three assigned erroneous steps have proved corrected replacements: top-component trace is separated from full fibre/IC coefficients; the SL2 nilpotent cone is local; and the unsupported even-power inference is removed. The nonsplit counterexample remains proved; the split function failure remains proved for every extension, and its categorical half remains conditional on exactly (O1)–(O3).