claimroutineinferred_dep

Differentiated grid system with radicals

Claim·§8.3 Differentiation and the surviving generic point·inside propNo algebraic configuration with large heights

Statement (paper)

With Ai=∂gi/giA_i=\partial g_i/g_i, Aℓ′=∂hℓ/hℓA'_\ell=\partial h_\ell/h_\ell, Hi=(∂xpi,∂ypi)H_i=(\partial x_{p_i},\partial y_{p_i}), Uℓ=(∂xrℓ,∂yrℓ)U_\ell=(\partial x_{r_\ell},\partial y_{r_\ell}), Lℓ(z,w)=(z−zrℓ)(w−wrℓ)L_\ell(z,w)=(z-z_{r_\ell})(w-w_{r_\ell}) and Riℓ=λiℓ−1−λiℓR_{i\ell}=\lambda_{i\ell}^{-1}-\lambda_{i\ell}, one has 2(pi−rℓ)⋅(Hi−Uℓ)=Riℓ(Ai−Aℓ′)2(p_i-r_\ell)\cdot(H_i-U_\ell)=R_{i\ell}(A_i-A'_\ell), Riℓ 2=Lℓ(pi)(Lℓ(pi)−4)R_{i\ell}^{\,2}=L_\ell(p_i)\bigl(L_\ell(p_i)-4\bigr), and Ai−Aℓ′≠0A_i-A'_\ell\ne0, where the dot is the bilinear expression xu+yvxu+yv without conjugation.

In plain English

Applying the derivation ∂\partial to the grid distance equations gives, for each grid edge, the linear relation 2(pi−rℓ)⋅(Hi−Uℓ)=Riℓ(Ai−Aℓ′)2(p_i-r_\ell)\cdot(H_i-U_\ell)=R_{i\ell}(A_i-A'_\ell), where Riℓ=λiℓ−1−λiℓR_{i\ell}=\lambda_{i\ell}^{-1}-\lambda_{i\ell} satisfies Riℓ2=Lℓ(pi)(Lℓ(pi)−4)R_{i\ell}^2=L_\ell(p_i)(L_\ell(p_i)-4). Moreover Ai−Aℓ′≠0A_i-A'_\ell\ne0, and the dot is the bilinear product xu+yvxu+yv with no conjugation.

Why it's here

Differentiating the distance equation and using the factored form λiℓ=gihℓ−1χiℓ\lambda_{i\ell}=g_i h_\ell^{-1}\chi_{i\ell} with constant χiℓ\chi_{i\ell} (killed by ∂\partial) turns it into a linear system in the row and column quantities HiH_i, UℓU_\ell, AiA_i, Aℓ′A'_\ell with radical coefficients RiℓR_{i\ell}. The nonvanishing of Ai−Aℓ′A_i-A'_\ell comes from ∂λiℓ≠0\partial\lambda_{i\ell}\ne0 for every grid edge. The later claim uses this system and the radical relation to reach a contradiction.
Classified routine:
A direct calculation: apply the derivation to the distance equations, using the factorization from claim-alg-obstruction-4 (constants killed by the derivation) and the nonvanishing of the derivation on grid edges from alg-derivation.

Uses

claimGrid ratios factor through constant defectslemDerivation nonvanishing on all grid edges

Used by

claimUnused sign change contradicts nonzero derivative

Sources

PaperOpen
Section
§8.3 Differentiation and the surviving generic point
Page
—
Label
—
Line
sections/07-algebra.tex:356
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Differentiated linear system with radicals" rests on claim-alg-obstruction-4
  • info
    inferred_dep
    outline: "Differentiated linear system with radicals" rests on alg:derivation