claimroutineinferred_dep
Ambient identity gives critical point
Shows in , so at
produces the critical point of
Claim·§3 The affine-space fibre and the critical point·inside thmNoncoordinate polynomial with affine three-space zero fibre
Statement (paper)
With and interpreted via , one has the polynomial identity in . At in the variable order the values are , , , , , , and consequently .
In plain English
With and , the identity holds in . At in variables one has , , , , and , and therefore .
Why it's here
This is the step that produces the critical point: the cusp and translation identities from the earlier claim give , and at both sides vanish to the order needed to force , because and vanish and vanishes while . The vanishing gradient is what the next claim uses, via Jacobian invertibility, to rule out being a coordinate.
Classified routine:
The identity follows from the earlier cusp and translation identities by substitution. Evaluating and differentiating it at the specified point is a direct calculation.