Under P(c)=0, construct the finite arithmetic data needed for Q(sqrt2,c), including a valid basis, multiplication and equality procedure; degree bounds derive from P, not an algebraicity oracle.
Method: native-induction. Induction: finite algebraic construction. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.