No finite C*-Smale mean-value constant at degree three

Over the fixed connected algebra C([0,1],C), no finite constant controls the first-order Smale norm divided difference for all split monic cubics. For every proposed constant, a continuous cubic family has an invertible test derivative and exactly two existing critical elements, both violating the bound. The full quantified theorem is proved in Lean. This is a stronger infinite-constant theorem, not the first refutation of the scalar or C*-constant-one conjecture, which was publicly refuted before this work. AI-assisted preprint by Myeongjin Kang, with no affiliation. Internal AI review is not external journal peer review. The accompanying Lean certificate covers the precise scoped main statement; inspect the formal endpoint, assumptions and provenance in the supporting package. Prior-art investigations are documented bounded searches, not worldwide-priority certification. Original prose is offered under CC BY 4.0 and original code/Lean under MIT; third-party rights and existing notices are preserved. The public supporting ZIP contains original proof sources and verification evidence, with bibliographic links and hashes instead of redistributed third-party source manuscripts. Recorded prior-art/source-access limits: Marginal-parameter-refinement objection explicitly weighed by parent and two independent reviews; full quantifier and fixed-connected-algebra infinity theorem deemed substantive; Bounded DuckDuckGo/registry/arXiv/selection literature screen; no worldwide-priority guarantee; Exa429, no exhaustive subscription-index search; public scalar proofs not re-audited and not dependencies