Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

f~ is multilinear, agrees with f at every point of {0,1}n, is degree-nonincreasing when nonzero, and is the unique multilinear polynomial with that agreement

Statement

For every polynomial fF[x1,,xn], its multilinear reduction f~ is multilinear, agrees with f at every point of the cube {0,1}n, satisfies degf~degf whenever f~0, and is the unique multilinear polynomial with that agreement.

Facts & Assumptions

Given: a polynomial fF[x1,,xn].

[F1]

The multilinear reduction replaces each monomial xt by the squarefree monomial xsupp(t) (Multilinear polynomials and the reduction xi2xi on the cube).

[L2]

A polynomial with each variable degree below 2 that vanishes on the whole cube is the zero polynomial (If degxiP<Si for each i and P vanishes on S1××Sn, then P=0).

Proof

technique · direct
1.1

For a{0,1}n and every positive integer k, aik=ai. Hence each monomial xt and its reduction xsupp(t) have the same value at a, so summing the monomials in [F1] gives f~(a)=f(a). Every reduced monomial is squarefree and has degree supp(t)iti, so f~ is multilinear and has no larger total degree than f whenever the two are nonzero.

F1algebra
2.1

If g is another multilinear polynomial agreeing with f on the cube, then gf~ is multilinear and vanishes on the cube. By [L2], it is the zero polynomial. So g=f~, proving uniqueness.

L2step 1.1

Remarks

  • Uniqueness is what later turns a pointwise identity on the cube into a linear independence statement about multilinear monomials.

Depends on

Used by

Dependency tree · two levels

16 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources