Goal and scope
Let M be the symmetric integer matrix with first row (2,1) and second row (1,3), and ⟨x,y⟩_M=xᵀMy for x,y∈ℝ². (1) Prove separately that ⟨·,·⟩_M is bilinear, symmetric and positive definite, hence an inner product on ℝ²; positive definiteness is certified universally by the 2-by-2 Sylvester conditions, with both sufficiency and necessity proved in full. (2) Decide why the forms given by N (rows (1,2),(2,1)), P (rows (1,1),(1,1)) and R (rows (2,1),(0,3)) are not inner products.
Works inside the MKO's scope: matrices and vectors are fully specified, with 2-by-2 integer candidate matrices (assumption a1); positive definiteness is checked by exact leading-principal-minor and determinant conditions, not established from finitely many sampled vectors (assumption a2). Bilinearity, symmetry and positive definiteness are three separate obligations. The induced norm (the next node), completeness and the Sylvester criterion for n>2 are not treated, and the canonical MKO and its English edition are not changed.
Main derivation
S01 · definition
Before
\langle\cdot,\cdot\rangle_M\ \text{inner product on}\ \mathbb{R}^2After
\text{bilinear}\ \land\ \text{symmetric}\ \land\ \forall x\neq0:\ \langle x,x\rangle_M>0Conditions: none
Rule: mko_ips_def · Uses: G1, G2, mko_ips_def
Leaf basis: mko_ips_def + def_unfold
By the MKO, an inner product has three separate obligations: bilinear in both slots, symmetric, and positive definite (⟨x,x⟩ strictly positive for every nonzero vector). S03 to S07 prove them one by one, and none can be skipped; each comparison matrix in S12 to S14 lacks one of them.
S02 · equivalent
Before
\langle x,y\rangle_M=x^{T}MyAfter
\langle x,y\rangle_M=2x_1y_1+x_1y_2+x_2y_1+3x_2y_2
Conditions: none
Rule: matrix_product_def · Uses: G2, matrix_product_def
Leaf basis: matrix_product_def + distributive
First My=(2y₁+y₂, y₁+3y₂); multiplying by xᵀ gives x₁(2y₁+y₂)+x₂(y₁+3y₂), which expands into four terms. The coefficients 2, 1, 1, 3 are exactly the entries M_{ij}, attached to x_iy_j.
S03 · equivalent
Before
\langle\alpha x+\beta z,\ y\rangle_M
After
\alpha\langle x,y\rangle_M+\beta\langle z,y\rangle_M
Conditions: none
Rule: mko_bilinear_def · Uses: S02, mko_bilinear_def
Leaf basis: distributive + mul_assoc + mul_comm + finite_sum_rules
Linearity in the first slot: αx+βz has coordinates αx_i+βz_i; substituting into the four terms of S02, each term M_{ij}(αx_i+βz_i)y_j splits by distributivity into αM_{ij}x_iy_j+βM_{ij}z_iy_j, and the terms regroup. x, z, y, α, β are arbitrary, so this is a universal certificate (N1 checks it as a polynomial identity).
S04 · equivalent
Before
\langle x,\ \alpha y+\beta w\rangle_M
After
\alpha\langle x,y\rangle_M+\beta\langle x,w\rangle_M
Conditions: none
Rule: mko_bilinear_def · Uses: S02, mko_bilinear_def
Leaf basis: distributive + mul_assoc + mul_comm + finite_sum_rules
Linearity in the second slot works the same way: each term M_{ij}x_i(αy_j+βw_j) splits into αM_{ij}x_iy_j+βM_{ij}x_iw_j. The second slot must be checked separately: bilinearity is an obligation for each slot.
S05 · implies
Before
\langle y,x\rangle_M=2y_1x_1+y_1x_2+y_2x_1+3y_2x_2
After
\langle y,x\rangle_M=\langle x,y\rangle_M\ \ (\forall x,y)
Conditions: M_{12}=M_{21}
Rule: mul_comm · Uses: S02, G2
Leaf basis: mul_comm + add_comm
After swapping x and y, the term y₁x₂ matches x₂y₁ of the original and y₂x₁ matches x₁y₂; both carry coefficient 1 because M_{12}=M_{21}=1. Commutativity of multiplication then makes the four terms agree one by one. Symmetry relies on M being symmetric.
S06 · definition
Before
q(x)=\langle x,x\rangle_M
After
q(x)=2x_1^2+2x_1x_2+3x_2^2=ax_1^2+2bx_1x_2+cx_2^2\ \ (a,b,c)=(2,1,3)
Conditions: none
Rule: def_intro · Uses: S02
Leaf basis: def_intro + mul_comm + distributive
Put y=x in S02; the terms x₁x₂ and x₂x₁ combine into 2x₁x₂. A general symmetric matrix with rows (a,b),(b,c) gives q=ax₁²+2bx₁x₂+cx₂²; here a=2, b=1, c=3.
S07 · theorem_application
Before
a=2>0,\ \ ac-b^2=6-1=5>0
After
\forall x\neq0:\ q(x)>0
Conditions: a>0; ac-b^2>0
Rule: L_sylvester_suff · Uses: S06
Leaf basis: square_nonneg + order_basics + zero_product
Sylvester conditions: the leading principal minor a=2>0 and the determinant ac−b²=2·3−1²=5>0. By Lemma L_sylvester_suff, q is positive at every nonzero vector. The lemma is proved completely by completing the square in sub-steps S07.1 to S07.3, for all x at once, without samples.
S08 · equivalent
Before
2\,q(x)=2(2x_1^2+2x_1x_2+3x_2^2)
After
2\,q(x)=(2x_1+x_2)^2+5x_2^2
Conditions: none
Rule: distributive · Uses: S06, S07.1
Leaf basis: distributive + power_laws
Substitute a=2, b=1, c=3 into the identity of S07.1: 2q(x)=(2x₁+x₂)²+5x₂². This is the concrete completing-the-square certificate for M: both terms on the right are nonnegative and vanish together only at x=0.
S09 · implies
Before
\text{S03},\ \text{S04},\ \text{S05},\ \text{S07}After
\langle\cdot,\cdot\rangle_M\ \text{is an inner product};\ (\mathbb{R}^2,\langle\cdot,\cdot\rangle_M)\ \text{real inner-product space}Conditions: none
Rule: and_intro_elim · Uses: S01, S03, S04, S05, S07
Leaf basis: and_intro_elim + mko_ips_def
All three obligations are proved: bilinearity (S03, S04), symmetry (S05) and positive definiteness (S07). By the definition in S01, ⟨·,·⟩_M is an inner product on ℝ².
S10 · implies
Before
e_1=(1,0),\ e_2=(0,1),\ x=(1,-1)
After
\langle e_1,e_2\rangle_M=1,\ q(e_1)=2,\ q(e_2)=3,\ q(1,-1)=2-2+3=3
Conditions: none
Rule: numeric_evaluation · Uses: S02, S06
Leaf basis: numeric_evaluation
Exact evaluation: ⟨e₁,e₂⟩_M=M₁₂=1; q(e₁)=a=2 and q(e₂)=c=3; q(1,−1)=2·1+2·1·(−1)+3·1=3>0. Consistent with S08: 2q(1,−1)=(2−1)²+5=6. These values are examples only; positive definiteness is proved in S07.
S11 · implies
Before
\forall x\neq0:\ ax_1^2+2bx_1x_2+cx_2^2>0
After
a>0\ \land\ ac-b^2>0
Conditions: none
Rule: L_sylvester_nec · Uses: S06
Leaf basis: order_basics + mul_inverse_nonzero
The Sylvester conditions are also necessary (Lemma L_sylvester_nec), so for 2-by-2 symmetric matrices they are an exact criterion: positive definite ⇔ a>0 and ac−b²>0. The necessary direction lets a failed condition refute positive definiteness directly (S12, S13). The proof is in sub-steps S11.1 and S11.2.
S12 · implies
Before
N:\ a=1,\ b=2,\ c=1,\ ac-b^2=1-4=-3<0
After
q_N(-2,1)=4-8+1=-3<0\ \Rightarrow\ \langle\cdot,\cdot\rangle_N\ \text{not an inner product}Conditions: none
Rule: contrapositive · Uses: G3, S11
Leaf basis: contrapositive + numeric_evaluation
N is symmetric and bilinear and its diagonal entries 1, 1 are positive, but its determinant is −3<0, so by the contrapositive of L_sylvester_nec it is not positive definite. The witness vector (−b,a)=(−2,1) of S11.2 gives q_N=1·4+4·(−2)·1+1·1=−3<0. Another witness, (1,−1), gives 1−4+1=−2.
S13 · implies
Before
P:\ a=b=c=1,\ ac-b^2=0
After
q_P(x)=(x_1+x_2)^2\ge0,\ q_P(1,-1)=0\ \Rightarrow\ \text{semi-definite, not an inner product}Conditions: none
Rule: contrapositive · Uses: G3, S11
Leaf basis: contrapositive + square_nonneg + numeric_evaluation
P is symmetric and bilinear, with q_P=x₁²+2x₁x₂+x₂²=(x₁+x₂)²≥0, so it is positive semi-definite; but its determinant 0 is not strictly positive, and the nonzero vector (1,−1) gives q_P=0, violating 'strictly positive on nonzero vectors'. Thus this merely positive-semidefinite form, with a nonzero null vector, is not an inner product. Positive-semidefinite in the inclusive sense also includes positive-definite forms, so the conclusion is not that every semidefinite form fails to be an inner product.
S14 · implies
Before
R=\begin{pmatrix}2&1\\0&3\end{pmatrix}After
\langle e_1,e_2\rangle_R=R_{12}=1\neq 0=R_{21}=\langle e_2,e_1\rangle_R\ \Rightarrow\ \text{not symmetric}Conditions: none
Rule: quantifier_negation · Uses: G3, S02
Leaf basis: quantifier_negation + matrix_product_def
xᵀRy is still bilinear (the arguments of S03 and S04 do not use symmetry), but ⟨e₁,e₂⟩_R=R₁₂=1 and ⟨e₂,e₁⟩_R=R₂₁=0, so symmetry fails. Hence R does not define an inner product, whatever its quadratic form does; the three obligations must be checked separately.
S15 · implies
Before
\text{S09},\ \text{S12},\ \text{S13},\ \text{S14}After
M\ \text{inner product};\ N\ \text{indefinite};\ P\ \text{semi-definite};\ R\ \text{not symmetric}Conditions: none
Rule: and_intro_elim · Uses: S09, S12, S13, S14
Leaf basis: and_intro_elim
Combine: M passes all three obligations and is an inner product; N is indefinite (determinant −3); P is only semi-definite (determinant 0); R is not symmetric.
Substeps and lemmas
S07.1 · equivalent
Before
a\,q(x)=a(ax_1^2+2bx_1x_2+cx_2^2)
After
a\,q(x)=(ax_1+bx_2)^2+(ac-b^2)x_2^2
Conditions: none
Rule: distributive · Uses: distributive
Leaf basis: distributive + power_laws + add_inverse
Expand the right side: (ax₁+bx₂)²=a²x₁²+2abx₁x₂+b²x₂², and adding (ac−b²)x₂² gives a²x₁²+2abx₁x₂+acx₂², which is the left side. Multiplying by a instead of dividing keeps the identity valid for every real a (N3).
S07.2 · implies
Before
a>0,\ ac-b^2>0,\ a\,q(x)=(ax_1+bx_2)^2+(ac-b^2)x_2^2
After
a\,q(x)\ge 0\ \Rightarrow\ q(x)\ge 0
Conditions: a>0; ac-b^2>0
Rule: square_nonneg · Uses: S07.1, square_nonneg, order_basics
Leaf basis: square_nonneg + order_basics + mul_inverse_nonzero
Squares are nonnegative, and (ac−b²)>0 times the nonnegative x₂² is nonnegative, so a·q(x)≥0; multiplying by 1/a>0 (the order axioms keep the direction) gives q(x)≥0.
S07.3 · implies
Before
q(x)=0
After
x_2=0\ \land\ x_1=0,\ \text{so}\ x\neq0\Rightarrow q(x)>0Conditions: a>0; ac-b^2>0
Rule: zero_product · Uses: S07.1, S07.2, zero_product
Leaf basis: zero_product + square_nonneg + order_basics + contrapositive
If q(x)=0, the two nonnegative terms sum to 0, so both are 0: (ac−b²)x₂²=0 with ac−b²≠0 gives x₂=0; then (ax₁+bx₂)²=0 gives ax₁=0, and a≠0 gives x₁=0. Contrapositively x≠0 ⇒ q(x)≠0, and with S07.2, q(x)>0. S07.1 to S07.3 together prove Lemma L_sylvester_suff.
S11.1 · implies
Before
x=e_1=(1,0)\neq0
After
q(e_1)=a>0
Conditions: none
Rule: forall_elim · Uses: S06
Leaf basis: forall_elim + mul_zero + numeric_evaluation
Specialize the positivity hypothesis to x=e₁≠0: q(e₁)=a·1+2b·0+c·0=a, so a>0.
S11.2 · implies
Before
x=(-b,a)\neq0
After
q(-b,a)=ab^2-2ab^2+ca^2=a(ac-b^2)>0\ \Rightarrow\ ac-b^2>0
Conditions: a>0
Rule: forall_elim · Uses: S11.1
Leaf basis: forall_elim + order_basics + distributive + mul_inverse_nonzero
Since a>0, the vector (−b,a) has a nonzero second coordinate and is nonzero. Substituting gives a·b²+2b·(−b)·a+c·a²=a(ac−b²) (N6). Positivity gives a(ac−b²)>0, and multiplying by 1/a>0 gives ac−b²>0. S11.1 and S11.2 together prove Lemma L_sylvester_nec.