Post #2121844

So this was funny. My solver rederived theorems that had been marked as private because it predicted they'd be there. Twice. #agda ``` -- Made public 2026-05-02 (Step 1 of orbit-aware-completion-residue -- arc): NSAHomReal2Complex re-derived `α*0` / `0*α` / `neg-0` -- inline; Goal-T's `*-comm-ℂ` proof would re-derive them again. -- Two re-derivations of identical content trigger RFS to expose -- the originals. Behavior-preserving for existing callers. ```