Apollonius' problem has eight solutions in generic position. While formalizing it in MachLib we assumed the obvious general-position condition — three equal circles, comfortably separated. That assumption is false. At the exact locus d² = 8ρ² one of the four solution classes loses its leading coefficient, its quadratic becomes linear, and the count drops to seven. Nothing in the picture degenerates. A live exhibit lets you cross the locus yourself.
We named a proof obligation about how fast a shallow exp–log expression can approach zero. It fit the lower-depth results and it looked right. It was false — and false at exactly one scale. Replacing a linear term by an exponential one yields a statement that is machine-checked, and the implication between the two is machine-checked as well. So the correction is not 'whatever the prover would accept': the stronger form is formally refuted, the weaker is formally proved, and their relationship is a theorem.
We lifted an earlier machine-checked finiteness proof, whose only mean-value axiom is rolle, from one hardcoded tower of iterated exponentials to arbitrary exponential-type Pfaffian chains at every depth — with one honest hypothesis we do not round off: positivity.
The only operation in SuperBEST costing more than 3 nodes was general-domain addition at 11n. It now costs 2 nodes, and a Lean lower bound shows no single F16 operator does it. (This post also called the table complete; it was not.)
ELSb(0, x) = exp(0 − ln(x)) = 1/x. One node. SuperBEST v4: 18 nodes total, 75.3% savings. The reciprocal was never a division problem.
Why sin(x) cannot be expressed as a finite real EML tree. Every real EML tree is real-analytic with finitely many zeros.
Under strict principal-branch semantics, i is unreachable from {eml, 1}. Lean-verified. Depth-6 closest approach: 0.99999524.