claimroutineinferred_dep

Unused sign change contradicts nonzero derivative

Claim·§8.5 An unused sign change·inside propNo algebraic configuration with large heights

Statement (paper)

With MM, R1,…,RjR_1,\ldots,R_j and M=M(R1,…,Rj)\mathcal M=M(R_1,\ldots,R_j) as above, the equations cannot all hold. In the case where the position rows p−r1,p−r2,p−r3p-r_1,p-r_2,p-r_3 have rank two, Cramer's rule places Hx,Hy,AH_x,H_y,A in M(R1,R2,R3)M(R_1,R_2,R_3), and the automorphism of M\mathcal M changing only the sign of R4R_4 yields A=A4′A=A'_4. In the remaining case where V1=V2V_1=V_2 is a single line, one gets h=v⋅Hh=v\cdot H and AA in M(R1,R2)M(R_1,R_2), and changing only the sign of R3R_3 yields A=A3′A=A'_3. Either way this contradicts .

In plain English

The differentiated linear system relating HH, UU, AA, A′A' and the radicals RℓR_\ell cannot hold simultaneously. Solving it by Cramer's rule puts Hx,Hy,AH_x,H_y,A (or hh and AA) in the field generated by a few radicals, and flipping the sign of one unused radical forces A=Aℓ′A=A'_\ell for some ℓ\ell.

Why it's here

This is the closing step of the obstruction argument. Solving the differentiated grid system from the previous claim shows AA lies in a field M(R1,…,Rj)M(R_1,\ldots,R_j) that does not involve a further radical (R4R_4, or R3R_3 in the line case). Changing that radical's sign is an automorphism fixing AA but flipping A′A', so A=Aℓ′A=A'_\ell, contradicting the nonvanishing of Ai−Aℓ′A_i-A'_\ell and so ruling out the system.”}
Classified routine:
This closing step combines the earlier differentiated grid system with Cramer's rule and the Galois automorphism that flips the sign of a square root, a standard field-theoretic argument. Its new content lies in the setup from the earlier claims, not in this step.

Uses

claimDifferentiated grid system with radicalslemSome grid vertex is generic

Used by

Nothing in the paper

Sources

PaperOpen
Section
§8.5 An unused sign change
Page
—
Label
—
Line
sections/07-algebra.tex:605
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Unused sign change contradicts nonzero derivative" rests on claim-alg-obstruction-5
  • info
    inferred_dep
    outline: "Unused sign change contradicts nonzero derivative" rests on alg:surviving-point