Real bilinear form: proving bilinearity slot by slot from x^T A y, with exact evaluation

Goal and scope

Let A=[[1,2],[−1,3]] and B(x,y)=x^T A y for x, y∈ℝ². Prove separately that B is linear in the first slot and in the second slot (bilinear); evaluate exactly B(x,y)=7 and B(y,x)=−20 for x=(2,−1), y=(1,4), showing that bilinearity does not require symmetry; and prove that the black-box function f(x,y)=x1y1+(x2³−x2)y2 passes some additivity samples but is not bilinear.

Stays inside the MKO: the numeric checks use an integer-coefficient matrix, compatible dimensions and safe integer coordinates (assumption a1); the general bilinearity certificate permits arbitrary real coordinates and scalars, and a fixed real matrix; matrix expansion is a universal algebraic certificate of bilinearity, and finite samples cannot prove that an arbitrary black-box function is bilinear (assumption a2). Symmetry, positive definiteness, nondegeneracy and inner products appear only as contrasts and are not proved here. The canonical MKO and its English edition are not changed.

Givens and symbols

• matrix_product_def
• distributive
• finite_sum_rules
• vector_space_axioms
• linear_map_def

• G1 — A=[[1,2],[−1,3]], that is a11=1, a12=2, a21=−1, a22=3. x and y are column vectors of ℝ² (2×1), and B(x,y)=x^T A y.
• G2 — Example: x=(2,−1), y=(1,4), x′=(1,1), α=3, β=−2.
• G3 — Black box for contrast: f(x,y)=x1y1+(x2³−x2)y2.

• A=(a_{ij}) — the 2×2 integer matrix [[1,2],[−1,3]]
• B(x,y)=x^{T}Ay — the bilinear form given by A
• x,\ x',\ y,\ y' — vectors in ℝ²
• \alpha,\ \beta — real coefficients
• f — the black-box function used for contrast

Rules and sources

• matrix_product_def · prerequisite — Matrix product: for A of size m×n and B of size n×p, (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}. Matrix multiplication is in general not commutative.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• finite_sum_rules · prerequisite — Finite sums: Σ_{i=1}^{0} a_i=0 and Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}; Σ(a_i+b_i)=Σa_i+Σb_i; Σ c·a_i=c·Σa_i.
• vector_space_axioms · prerequisite — Vector space axioms (over ℝ or another field F): vectors form a commutative group under addition; scalar multiplication satisfies a(u+v)=au+av, (a+b)u=au+bu, (ab)u=a(bu) and 1u=u.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• mko_bilinear_def · cited — B:V×V→R is bilinear when fixing either input leaves a linear map in the other. This slice uses the integer-coefficient matrix formula B(x,y)=x^T A y as a universal coordinate certificate and for exact evaluation. · mko-real-bilinear-form
• linear_map_def · prerequisite — A map L:ℝ²→ℝ is linear if L(αu+βu′)=αL(u)+βL(u′) for all u, u′∈ℝ² and α, β∈ℝ.
• L_slot2 · lemma — For every fixed x∈ℝ², y↦B(x,y)=Σ_iΣ_j x_i a_ij y_j is linear: B(x,αy+βy′)=αB(x,y)+βB(x,y′).

Main derivation

B\ \text{bilinear}

\forall y:\ x\mapsto B(x,y)\ \text{linear}\ \land\ \forall x:\ y\mapsto B(x,y)\ \text{linear}

x^{T}Ay\ \ (1\times2)(2\times2)(2\times1)

B(x,y)=\sum_{i=1}^{2}\sum_{j=1}^{2}x_i\,a_{ij}\,y_j

\sum_{i,j}x_i\,a_{ij}\,y_j

x_1y_1+2x_1y_2-x_2y_1+3x_2y_2

B(\alpha x+\beta x',y)

\sum_{i,j}(\alpha x_i+\beta x'_i)\,a_{ij}\,y_j

\sum_{i,j}(\alpha x_i+\beta x'_i)\,a_{ij}\,y_j

\sum_{i,j}\left(\alpha\,x_i a_{ij} y_j+\beta\,x'_i a_{ij} y_j\right)

\sum_{i,j}\left(\alpha\,x_i a_{ij} y_j+\beta\,x'_i a_{ij} y_j\right)

\alpha B(x,y)+\beta B(x',y)

B(x,\alpha y+\beta y')

\alpha B(x,y)+\beta B(x,y')

\text{slot 1 linear (S06)},\ \text{slot 2 linear (S07)}

B\ \text{is a bilinear form on}\ \mathbb{R}^2

B(x,y)=x^{T}(Ay),\ x=(2,-1),\ y=(1,4)

B(x,y)=7

B(y,x)=y^{T}(Ax),\ Ax=(1\cdot2+2\cdot(-1),\ -1\cdot2+3\cdot(-1))

Ax=(0,-5),\ B(y,x)=1\cdot0+4\cdot(-5)=-20

B(x,y)=7,\ B(y,x)=-20

B\ \text{bilinear but not symmetric}

\alpha x+\beta x'=(4,-5)

B((4,-5),y)=-19=3\cdot7+(-2)\cdot20

x=x'=(0,1),\ y=(0,1)

f(x+x',y)=6\neq0=f(x,y)+f(x',y)

x_2,\ x'_2,\ x_2+x'_2\in\{-1,0,1\}

f(x+x',y)=f(x,y)+f(x',y)\ \text{on these samples}

Substeps and lemmas

B(x,\alpha y+\beta y')

\sum_{i,j}x_i\,a_{ij}\,(\alpha y_j+\beta y'_j)

\sum_{i,j}x_i\,a_{ij}\,(\alpha y_j+\beta y'_j)

\sum_{i,j}\left(\alpha\,x_i a_{ij} y_j+\beta\,x_i a_{ij} y'_j\right)

\sum_{i,j}\left(\alpha\,x_i a_{ij} y_j+\beta\,x_i a_{ij} y'_j\right)

\alpha B(x,y)+\beta B(x,y')

Ay=\begin{pmatrix}1&2\\-1&3\end{pmatrix}\begin{pmatrix}1\\4\end{pmatrix}

\begin{pmatrix}9\\11\end{pmatrix}

x^{T}(Ay)=(2,-1)\begin{pmatrix}9\\11\end{pmatrix}

2\cdot9+(-1)\cdot11=7

Reverse audits

• S14 · premise_audit · G3, S13 — This step only records that the samples pass; the conclusion 'not bilinear' comes from S13.
• S13 · premise_audit · G3, contradiction, linear_map_def — Linearity is a universal statement, and one counterexample refutes it.
• S12 · premise_audit · S06, numeric_evaluation — The general conclusion comes from S06; this step checks one instance (N9).
• S11 · premise_audit · S08, S09, S10 — One unequal pair of values refutes symmetry (a universal statement); bilinearity is unaffected.
• S10 · premise_audit · matrix_product_def, numeric_evaluation — Exact integer computation (N7).
• S09.2 · inverse_equivalence · matrix_product_def, numeric_evaluation — Both sides are the same number.
• S09.1 · inverse_equivalence · matrix_product_def, numeric_evaluation — Both sides are the same vector.
• S09 · premise_audit · S02, matrix_product_def — Exact integer computation, cross-checked by the expansion of S03 (N13).
• S08 · sufficient_goal_reduction · S01, S06, S07, forall_intro — Goal G: B is bilinear. Sufficient condition H: each slot is linear; H⇒G by S01. H is proved forwards in S04 to S07 as a universal algebraic certificate, not a sample.
• S07.3 · inverse_equivalence · finite_sum_rules — Splitting sums and pulling out constants can be reversed; this sub-step does not use L_slot2.
• S07.2 · inverse_equivalence · distributive, mul_comm — Expanding and factoring are inverse; this sub-step does not use L_slot2.
• S07.1 · inverse_equivalence · vector_space_axioms, matrix_product_def — Substituting the coordinates of the same vector is two-way; this sub-step does not use L_slot2.
• S07 · premise_audit · S02, L_slot2 — It needs only the double-sum form of S02 and the lemma.
• S06 · inverse_equivalence · finite_sum_rules — Splitting sums and pulling out constants can be reversed, so the step is two-way.
• S05 · inverse_equivalence · distributive — Expanding and factoring are inverse, so the step is two-way.
• S04 · inverse_equivalence · vector_space_axioms, matrix_product_def — Substituting the coordinates of the same vector keeps the two sides equal, two-way.
• S03 · inverse_equivalence · finite_sum_rules — Writing out a finite sum term by term rewrites equal values, so the step is two-way.
• S02 · inverse_equivalence · matrix_product_def, distributive — Both are expressions of the same number, so the step is two-way.
• S01 · premise_audit · mko_bilinear_def, linear_map_def — This step only unfolds the definition; the two slots are checked separately later (S04 to S06, S07).

Error controls and negative controls

Symmetry is not bilinearity

The mistake named by the MKO is to declare bilinearity or an inner product after checking only B(x,y)=B(y,x). g(x,y)=(x1y1)² is symmetric, but g(2e1,e1)=4≠2=2g(e1,e1), so it is not bilinear. Conversely B here is bilinear but not symmetric (7≠−20). B(x,x)=x1²+x1x2+3x2²=(x1+x2/2)²+(11/4)x2² is positive for x≠0, yet B is not an inner product because it is not symmetric.

Check each slot separately; bilinear is not linear in the pair

A is not symmetric, so the second slot cannot be obtained from the first by swapping (S07 proves it separately). Bilinear also does not mean B(x+x′,y+y′)=B(x,y)+B(x′,y′): the correct expansion has the cross terms B(x,y′)+B(x′,y). For example x=x′=y=y′=e1: B(2e1,2e1)=4 while B(e1,e1)+B(e1,e1)=2.

Black-box samples are not enough

f passes additivity on every sample with x2, x′2, x2+x′2∈{−1,0,1} (S14), yet fails at (0,1)+(0,1) (S13). MKO assumption a2: matrix expansion is a universal certificate, and finite samples cannot prove an arbitrary black-box function bilinear.

• g(x,y)=(x1y1)² is symmetric, so it is a bilinear form → reject — g(2e1,e1)=4 while 2g(e1,e1)=2.
• Since B(x,y)=7≠−20=B(y,x), x^T A y is not a bilinear form → reject — Bilinearity does not require symmetry; S04 to S08 prove B bilinear.
• Bilinear means B(x+x′,y+y′)=B(x,y)+B(x′,y′) → reject — With x=x′=y=y′=e1 the left side is 4 and the right side 2; the cross terms are missing.
• f passed several additivity tests such as x=(1,1), x′=(2,−1), so f is bilinear → reject — f((0,2),(0,1))=6 while f((0,1),(0,1))+f((0,1),(0,1))=0.

Result and limitations

B(x,y)=x^T A y=x1y1+2x1y2−x2y1+3x2y2 is linear in the first slot and in the second slot (a universal algebraic certificate), so it is a bilinear form; a fixed real matrix gives such a bilinear map on compatible coordinate spaces, using a square matrix for a form on one space. B(x,y)=7 and B(y,x)=−20, so B is bilinear but not symmetric, and not an inner product. The black box f(x,y)=x1y1+(x2³−x2)y2 looks additive on samples with x2∈{−1,0,1}, but f((0,2),(0,1))=6≠0, so it is not bilinear.

• The completed square for B(x,x) in the error controls is checked as a polynomial identity by N14; the general theory of positive definiteness and inner products is not treated.
• N2 and N3 are grid checks of multilinear identities of degree at most 1 per variable (not necessarily total degree at most 1), which decide those identities; N9 is only one instance.

Verification and source binding

15 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: e1078dee19a7ff2ca3fc623044adf902aaf5c6edb8681d13aaaa972aa31c4f49
• original source SHA-256: 1412fb7e13e4018d6967accecdadadcf60832aad360e17ead14a7174bc1399a7
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)