Mathematical workbench

Square laboratory

Control an arbitrary square through E, x, and y, or obtain these coordinates from a parametric family.

Red–red

BDEFJ

E841x816y24
Matrix 3 × 3 · valuesΣ = 2 523
A1 657
B49
C817
D1
E841
F1 681
G865
H1 633
J25

a brick-red frame marks a value that is a perfect square

Magic invariantall 8 line sums agree
Declared maskBDEFJ · confirmed
Actual result5/9 squares
Nondegeneracy9 pairwise-distinct entries

Family BDEFJ

Theorem and complete proof

General theory of the 4/9 and 5/9 orbits

Statement

Under the assumptions below, the formulas define an integral magic square of order 3 in which at least all 5 cells of the BDEFJ mask are squares of integers. Other cells are allowed to be squares as well.

{B,D,E,F,J}{P:MP(E,x,y)=rP2}\{B,D,E,F,J\}\subseteq\{P:\mathcal M_P(E,x,y)=r_P^2\}

The parameters a, b, c, and d are arbitrary integers. Every auxiliary root introduced below is therefore integral.

Initial system and elimination of E, x, y

For every marked cell, introduce an integral root and substitute the corresponding Magic3 linear form. This gives the system:

{Ex+y=qB2,Exy=qD2,E=qE2,E+x+y=qF2,Ex=qJ2.\left\{\begin{aligned}E-x+y&=q_B^2,\\E-x-y&=q_D^2,\\E&=q_E^2,\\E+x+y&=q_F^2,\\E-x&=q_J^2.\end{aligned}\right.

The coefficient matrix of E, x, and y has rank 3. Eliminating them therefore leaves 2 independent homogeneous quadratic equations in the roots. The equations are derived and parametrized below.

Derivation of the root parametrization

Introduce the following auxiliary integers:

k1=a2b2+2ab,k2=c2d2+2cd,u0=k1k2k_1=a^2-b^2+2ab,\qquad k_2=c^2-d^2+2cd,\qquad u_0=k_1k_2u1=(c2+d2)k1,u2=(2cd+d2c2)k1u_1=(c^2+d^2)k_1,\qquad u_2=(2cd+d^2-c^2)k_1v1=(a2+b2)k2,v2=(2ab+b2a2)k2v_1=(a^2+b^2)k_2,\qquad v_2=(2ab+b^2-a^2)k_2

Define the declared cell values as the following explicit squares:

(B,D,E,F,J)=(v22,u02,u12,u22,v12)(B,D,E,F,J)=(v_2^2,u_0^2,u_1^2,u_2^2,v_1^2)

Apply the same arithmetic-progression identity to (d,c) and (b,a). One endpoint root in both progressions is u₀=k₁k₂, so their square values glue into a single five-cell mask.

u02+u22=2u12,u02+v22=2v12u_0^2+u_2^2=2u_1^2,\qquad u_0^2+v_2^2=2v_1^2D+F=2E,B+D=2JD+F=2E,\qquad B+D=2J

Start with two copies of the red conic r²+t²=2s². Each rational root triple comes from the standard two-parameter chart. To make the triples share one cell, multiply the first triple by the distinguished root of the second and the second by the distinguished root of the first; these cross-multipliers are k₁ and k₂. The common root then agrees identically, and permuting the other four roots gives the declared mask.

Reconstruction of the magic square

Use the standard three-coordinate form:

M(E,x,y)=(E+xEx+yEyExyEE+x+yE+yE+xyEx)\mathcal M(E,x,y)=\begin{pmatrix} E+x & E-x+y & E-y\\ E-x-y & E & E+x+y\\ E+y & E+x-y & E-x \end{pmatrix}

Set the coordinates equal to the following linear combination of the square values already constructed:

(E,x,y)=(E,EJ,BJ)(E,x,y)=(E,\,E-J,\,B-J)

The general linear lemma is applied directly: when the selected cell-form matrix has rank 3, its value vector lies in the image exactly when every vector in the left kernel annihilates it. The left kernel has dimension one for four cells and two for five cells. The colored identities above form precisely such a basis, while the displayed formulas for E, x, and y give the unique preimage.

LS(E,x,y)T=(qP2)PS,kerLST=R1,,R2L_S(E,x,y)^T=(q_P^2)_{P\in S},\qquad \ker L_S^T=\langle R_1,\ldots,R_{2}\rangle

Now substitute the coordinates into the nine Magic3 linear forms. Therefore

πBDEFJ ⁣(M(E,x,y))=(B,D,E,F,J){n2:nZ}5\pi_{BDEFJ}\!\left(\mathcal M(E,x,y)\right)=(B,D,E,F,J)\in\{n^2:n\in\mathbb Z\}^{5}

By the Magic3 form itself, every row, every column, and both diagonals sum to 3E. We have therefore obtained the required family of magic squares with square-valued mask BDEFJ. This proves the claim.

Color lemmas used in this proof

Light-red arithmetic progression

D+F=2ED+F=2E

A red triple means the linear condition U + W = 2V on three cells whose values are all perfect squares.

r=a2+2ab+b2,s=a2+b2,t=a2+2abb2r=-a^2+2ab+b^2,\qquad s=a^2+b^2,\qquad t=a^2+2ab-b^2r2+t2=2s2r^2+t^2=2s^2(U,V,W)=(k2r2,k2s2,k2t2)U+W=2V(U,V,W)=(k^2r^2,\,k^2s^2,\,k^2t^2)\Longrightarrow U+W=2V

In this mask, the lemma variables are replaced by cells D, E, F; its conclusion is exactly the cell relation displayed above.

General statement and proof

Dark-red arithmetic progression

B+D=2JB+D=2J

A red triple means the linear condition U + W = 2V on three cells whose values are all perfect squares.

r=a2+2ab+b2,s=a2+b2,t=a2+2abb2r=-a^2+2ab+b^2,\qquad s=a^2+b^2,\qquad t=a^2+2ab-b^2r2+t2=2s2r^2+t^2=2s^2(U,V,W)=(k2r2,k2s2,k2t2)U+W=2V(U,V,W)=(k^2r^2,\,k^2s^2,\,k^2t^2)\Longrightarrow U+W=2V

In this mask, the lemma variables are replaced by cells B, D, J; its conclusion is exactly the cell relation displayed above.

General statement and proof

Coverage completeness

Status: complete coverage. Completeness here refers to rational root vectors; integral representatives are obtained by clearing denominators and applying a common scale.

Broadest guaranteed subset

The entire set of rational root vectors satisfying the two quadrics for this mask, including the zero vector. Integral solutions are understood projectively: after clearing denominators, up to root signs and common scale.

(qP)PSVS(Q),qD0(q_P)_{P\in S}\in V_S(\mathbb Q),\qquad q_D\ne0qD=0(qP)PS=0q_D=0\Longrightarrow(q_P)_{P\in S}=0

Inverse construction

When q_D≠0, invert both red conics by their standard complete parametrization and use the cross-multipliers to align their scales at the shared root. When q_D=0, the corresponding red relation over Q forces the adjacent roots to vanish: a shared middle root uses a sum of two squares, while a shared endpoint uses the irrationality of √2. The second red relation then also gives the zero vector.

What remains outside the guarantee

There are no uncovered rational branches. A possible zero denominator in the inverse chart is removed by changing root signs or forces the entire root vector to be zero; the formula also produces the zero vector.

Exc(ΦS)=\operatorname{Exc}(\Phi_S)=\varnothing

Completeness is proved over the rational solutions of both quadrics.

The text reconstructs a legacy parametrization; its machine certificate has not yet been migrated to proof-core.legacy_red_red_bdefj