feat: add KoalaBear extension and multilinear shift semantics

[eliasjudin]

Formalizes a kernel-checked degree-five KoalaBear extension, arbitrary-commutative-ring evaluation bridges, explicit Boolean-cube endianness, and terminal-successor multilinear shift semantics in Lean 4.

No CompPoly formalization remains incomplete; ArkLib still needs to update its pinned CompPoly revision and Lean toolchain before consuming these APIs.

Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun

[github-actions]

🤖 PR Summary

KoalaBear Field Extension & Multilinear Shift Semantics

Mathematical Formalization

• Field Extension (CompPoly/Fields/KoalaBear/Ext5.lean): Defines ext5Poly = X^5 + X^2 - 1 as an irreducible polynomial over the KoalaBear prime field, proving irreducibility via Rabin's criterion (irreducible_of_rabin_5) using explicit trace and coprimality certificates. Constructs the degree-5 extension Field as AdjoinRoot ext5Poly, provides a PowerBasis, coordinate model V = F_p^5 with explicit operations (vadd, vmul, vsq, comp), a mulCoords function, and embed_mulCoords correctness theorem.
• Multilinear Shift Kernel (CompPoly/Multilinear/Next.lean): Introduces nextIndex (terminal-successor map on the Boolean hypercube), nextHat (closed-form interpolation kernel), nextHatCarry (carry-chain expression), and shiftColumn (shift operator). Proves multilinearity of nextHat, equivalence of forms (nextHat_eq_carry), cube-point indicator property (nextHat_cubePoint), and the core identity shift_eq_sum.
• Coordinate Semantics (CompPoly/Multilinear/Semantics.lean): Defines big-endian bit decomposition (toBE), equality kernel eqHat, cube points in little-endian (cubePointLE) and big-endian (cubePoint) conventions. Proves eqHat_cubePointLE, cubePoint_eq_reverse_cubePointLE, eqHat_reverse, eqHat_append, and mleEval (big-endian MLE). Establishes equivalence to existing CompPoly evaluation via mleEval_eq_eval_reverse, Kronecker delta property (eqHat_cubePoint_delta), value reproduction (mleEval_cubePoint), uniqueness (mleEval_ext), and table equality criterion (mleEval_eq_iff).
• Transform Equivalence (CompPoly/Multilinear/Equiv.lean): Adds theorems connecting coefficient evaluation to multivariate polynomial evaluation (CMlPolynomial.eval_toMvPolynomial) and proves the equivalence of monomial coefficients and Boolean-hypercube table representations (eval_monoToLagrange, eval_lagrangeToMono, eval_toMvPolynomial), supported by new private lemmas.

Infrastructure

• Module Imports (CompPoly.lean, CompPoly/Fields/KoalaBear.lean): Updated to import new Ext5 and multilinear semantics modules.
• Documentation (docs/wiki/repo-map.md, docs/wiki/representations-and-bridges.md): Updated to reference new Semantics.lean and Next.lean files, describing coordinate conventions and shift semantics.

No sorries or admits appear in any changed file.

---

Statistics

Metric	Count
📝 Files Changed	9
✅ Lines Added	1511
❌ Lines Removed	6

---

Lean Declarations

✏️ Added: 111 declaration(s)

CompPoly/Fields/KoalaBear/Ext5.lean (52)

• abbrev Field : Type
• def mulCoords (a b : Fin 5 → KoalaBear.Field) : Fin 5 → KoalaBear.Field
• instance instCharPAdjoin : CharP (AdjoinRoot ext5Poly) KoalaBear.fieldSize
• instance instNontrivialAdjoin : Nontrivial (AdjoinRoot ext5Poly)
• noncomputable def basis : Module.Basis (Fin 5) KoalaBear.Field Field
• noncomputable def coords : Field ≃ₗ[KoalaBear.Field] (Fin 5 → KoalaBear.Field)
• noncomputable def embed : (Fin 5 → KoalaBear.Field) ≃ₗ[KoalaBear.Field] Field
• noncomputable def ext5Poly : Polynomial KoalaBear.Field
• noncomputable def powerBasis : PowerBasis KoalaBear.Field Field
• private abbrev V
• private def cC : V
• private def comp (v w : V) : V
• private def gVec : V
• private def hVec : V
• private def scal (c : KoalaBear.Field) : V
• private def vadd (u v : V) : V
• private def ve1 : V
• private def vmul (u v : V) : V
• private def vone : V
• private def vsq (v : V) : V
• private lemma exists_factor_le_two_of_reducible.{u} {R : Type u} [_root_.Field R]
• private lemma irreducible_of_rabin_5 (P : Polynomial KoalaBear.Field)
• private noncomputable def toA (v : V) : AdjoinRoot ext5Poly
• private noncomputable def vPoly (v : V) : Polynomial KoalaBear.Field
• private theorem dvd_X_pow_sub_cPoly :
• private theorem embed_eq_toA (c : Fin 5 → KoalaBear.Field) :
• private theorem ext5Poly_coprime :
• private theorem ext5Poly_trace :
• private theorem frob_toA (v : V) :
• private theorem gVec_mul_hVec : vmul gVec hVec = vone
• private theorem isCoprime_gPoly : IsCoprime (vPoly gVec) ext5Poly
• private theorem pow2_correct (k : ℕ) :
• private theorem root_pow_fieldSize :
• private theorem root_rel :
• private theorem toA_add (u v : V) : toA (vadd u v) = toA u + toA v
• private theorem toA_comp (v w : V) :
• private theorem toA_eq_mk (v : V) : toA v = AdjoinRoot.mk ext5Poly (vPoly v)
• private theorem toA_mul (u v : V) : toA (vmul u v) = toA u * toA v
• private theorem toA_scal (c : KoalaBear.Field) :
• private theorem toA_sq (v : V) : toA (vsq v) = (toA v) ^ 2
• private theorem toA_ve1 : toA ve1 = AdjoinRoot.root ext5Poly
• private theorem toA_vone : toA vone = 1
• private theorem trace_root :
• private theorem vPoly_gVec : vPoly gVec = vPoly cC - X
• theorem basis_apply (i : Fin 5) :
• theorem embed_apply (c : Fin 5 → KoalaBear.Field) :
• theorem embed_bijective : Function.Bijective embed
• theorem embed_mulCoords (a b : Fin 5 → KoalaBear.Field) :
• theorem ext5Poly_irreducible : Irreducible ext5Poly
• theorem ext5Poly_natDegree : ext5Poly.natDegree = 5
• theorem ext5Poly_ne_zero : ext5Poly ≠ 0
• theorem powerBasis_dim : powerBasis.dim = 5

CompPoly/Multilinear/Equiv.lean (8)

• private def basisChangeFactor (x : Vector R n) (j : Fin (2 ^ n))
• private theorem finFunctionFinEquiv_symm_apply_two (i : Fin (2 ^ n)) (j : Fin n) :
• private theorem submask_lagrange_eq_factor_prod
• private theorem submask_lagrange_sum (x : Vector R n) (j : Fin (2 ^ n)) :
• private theorem sum_basisChangeFactor (x : Vector R n) (j : Fin (2 ^ n))
• theorem eval_lagrangeToMono (p : CMlPolynomialEval R n) (x : Vector R n) :
• theorem eval_monoToLagrange (p : CMlPolynomial R n) (x : Vector R n) :
• theorem eval_toMvPolynomial (p : CMlPolynomialEval R n) (x : Vector R n) :

CompPoly/Multilinear/Next.lean (30)

• def carryPrefix [CommRing R] (x y : Vector R n) (k : Fin n) : R
• def carrySuffix [CommRing R] (x y : Vector R n) (k : Fin n) : R
• def nextHat [CommRing R] (x y : Vector R n) : R
• def nextHatCarry [CommRing R] (x y : Vector R n) : R
• def nextIndex (n : Nat) (i : Fin (2 ^ n)) : Fin (2 ^ n)
• def shiftColumn (v : CMlPolynomialEval R n) : CMlPolynomialEval R n
• private def evenIndex (i : Fin (2 ^ n)) : Fin (2 ^ (n + 1))
• private def oddIndex (i : Fin (2 ^ n)) : Fin (2 ^ (n + 1))
• private def terminalIndex (n : ℕ) : Fin (2 ^ n)
• private theorem carryPrefix_push_castSucc [CommRing R]
• private theorem carryPrefix_push_last [CommRing R] (x y : Vector R n) (a b : R) :
• private theorem carrySuffix_push_castSucc [CommRing R]
• private theorem carrySuffix_push_last [CommRing R] (x y : Vector R n) (a b : R) :
• private theorem cubePoint_evenIndex [CommRing R] (i : Fin (2 ^ n)) :
• private theorem cubePoint_oddIndex [CommRing R] (i : Fin (2 ^ n)) :
• private theorem cubePoint_terminal [CommRing R] :
• private theorem eqHat_cubePoint_terminal [CommRing R] (x : Vector R n) :
• private theorem eqHat_push [CommRing R] (x y : Vector R n) (a b : R) :
• private theorem nextHatCarry_push [CommRing R] (x y : Vector R n) (a b : R) :
• private theorem nextHat_push [CommRing R] (x y : Vector R n) (a b : R) :
• private theorem nextIndex_evenIndex (i : Fin (2 ^ n)) :
• private theorem nextIndex_oddIndex (i : Fin (2 ^ n)) :
• private theorem not_succ_lt_iff_eq_terminal (i : Fin (2 ^ n)) :
• private theorem sum_eqHat_cubePoint_mul_eqHat_cubePoint [CommRing R]
• private theorem sum_even_odd {S : Type*} [AddCommMonoid S]
• theorem nextHat_cubePoint [CommRing R] (i j : Fin (2 ^ n)) :
• theorem nextHat_eq_carry [CommRing R] (x y : Vector R n) :
• theorem nextHat_left_mle [CommRing R] (y : Vector R n) :
• theorem nextHat_right_mle [CommRing R] (x : Vector R n) :
• theorem shift_eq_sum [CommRing R] (v : CMlPolynomialEval R n) (x : Vector R n) :

CompPoly/Multilinear/Semantics.lean (21)

• def cubePoint [Zero R] [One R] (n : ℕ) (i : Fin (2 ^ n)) : Vector R n
• def cubePointLE [Zero R] [One R] (n : ℕ) (i : Fin (2 ^ n)) : Vector R n
• def eqHat [CommRing R] (z w : Vector R n) : R
• def mleEval [CommRing R] (v : CMlPolynomialEval R n) (z : Vector R n) : R
• def toBE (n i : ℕ) : Vector Bool n
• private theorem match_bool_zero_one [Zero R] [One R] (b : Bool) :
• theorem cubePoint_eq_reverse_cubePointLE [CommRing R] (i : Fin (2 ^ n)) :
• theorem eqHat_append [CommRing R] {m : ℕ}
• theorem eqHat_cubePointLE [CommRing R] (z : Vector R n) (i : Fin (2 ^ n)) :
• theorem eqHat_cubePoint_delta [CommRing R] (i j : Fin (2 ^ n)) :
• theorem eqHat_cubePoint_eqLE [CommRing R] (z : Vector R n) (i : Fin (2 ^ n)) :
• theorem eqHat_interpolation [CommRing R]
• theorem eqHat_interpolationLE [CommRing R]
• theorem eqHat_reverse [CommRing R] (z w : Vector R n) :
• theorem mleEval_cubePoint [CommRing R]
• theorem mleEval_eq_eval_reverse [CommRing R]
• theorem mleEval_eq_iff [CommRing R] (v w : CMlPolynomialEval R n) :
• theorem mleEval_ext [CommRing R] {v w : CMlPolynomialEval R n}
• theorem toBE_getElem (n i : ℕ) (k : ℕ) (hk : k < n) :
• theorem toBE_msb (n i : ℕ) (hn : 0 < n) :
• theorem toBE_zero (n : ℕ) : toBE n 0 = Vector.replicate n false

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff adds three new files and modifies several existing files. Overall, the code follows the style guide well, but there are a few violations and areas for improvement mostly related to formatting and empty lines in proofs.

---

📄 **Per-File Summaries**

• CompPoly.lean: Added imports for CompPoly.Fields.KoalaBear.Ext5 and CompPoly.Multilinear.Next, CompPoly.Multilinear.Semantics, bringing new field extension and multilinear semantics modules into scope.
• CompPoly/Fields/KoalaBear.lean: Added an import of CompPoly.Fields.KoalaBear.Ext5 and updated the authors list to include Aristotle (Harmonic) and Elias Judin.
• CompPoly/Fields/KoalaBear/Ext5.lean: This file defines a degree-5 extension of the KoalaBear field as AdjoinRoot ext5Poly, where ext5Poly = X^5 + X^2 - 1. It provides a coordinate model V = F_p^5 with explicit addition, multiplication, squaring, and composition (vadd, vmul, vsq, comp), together with an interpretation map toA : V → AdjoinRoot ext5Poly and proofs that these operations lift the quotient ring structure (toA_mul, toA_add, toA_sq, toA_comp). The file proves irreducibility of ext5Poly via Rabin's criterion (irreducible_of_rabin_5), supplying a trace certificate (ext5Poly_trace, showing ext5Poly ∣ X^(card^5) - X) and a no-linear-factor certificate (ext5Poly_coprime, showing X^p - X coprime to ext5Poly) – the latter relies on explicit coordinate tuples cC, gVec, hVec and their properties (root_pow_fieldSize, frob_toA). It then instantiates Fact (Irreducible ext5Poly), defines the extension field Field as AdjoinRoot ext5Poly, builds a PowerBasis (dimension 5) and a Fin 5-indexed basis, provides linear equivalences embed and coords, and gives an executable coordinate multiplication mulCoords together with a correctness theorem embed_mulCoords.
• CompPoly/Multilinear/Equiv.lean: The file's import changed from CompPoly.Multilinear.Basic to CompPoly.Multilinear.TransformEquiv, and two new authors were added. Several private lemmas (finFunctionFinEquiv_symm_apply_two, basisChangeFactor, sum_basisChangeFactor, submask_lagrange_eq_factor_prod, submask_lagrange_sum) were introduced to support three new theorems: CMlPolynomial.eval_toMvPolynomial (evaluation of the associated multivariate polynomial agrees with coefficient evaluation) and, for CMlPolynomialEval, eval_monoToLagrange (changing monomial coefficients to Boolean-hypercube evaluations preserves evaluation), eval_lagrangeToMono (recovering monomial coefficients from a hypercube table preserves its multilinear-extension evaluation), and eval_toMvPolynomial (evaluating the multivariate polynomial recovered from a hypercube table agrees with multilinear-extension evaluation).
• CompPoly/Multilinear/Next.lean: This new file defines the multilinear nextHat kernel on the Boolean hypercube and proves the shift identity shift_eq_sum. It introduces nextIndex (the terminal-successor map), terminalIndex, and nextHat (a closed-form interpolation kernel), along with nextHatCarry (an equivalent carry-chain expression) and shiftColumn (the operator that shifts a column by nextIndex). The main theorems show that nextHat is multilinear in each argument (nextHat_left_mle, nextHat_right_mle), that it equals the carry-chain expression (nextHat_eq_carry), that on Boolean cube points it is the indicator of the successor relation (nextHat_cubePoint), and the central shift identity shift_eq_sum. The file contains no sorry or admit.
• CompPoly/Multilinear/Semantics.lean: Added CompPoly/Multilinear/Semantics.lean, a new file that defines big-endian bit decomposition (toBE), the multilinear equality kernel eqHat (closed product form), and cube points in both little-endian (cubePointLE) and big-endian (cubePoint) coordinate conventions. It proves identities linking these: eqHat_cubePointLE relates eqHat on little-endian points to CompPolyʼs existing lagrangeBasis; cubePoint_eq_reverse_cubePointLE and eqHat_reverse show the big-endian point is the reverse of the little-endian one and that eqHat is invariant under reversing both vectors; eqHat_append factorizes over concatenated vectors. It then defines mleEval, the big-endian multilinear extension evaluation, and proves mleEval_eq_eval_reverse (equivalence to CompPoly evaluation on the reversed point), eqHat_cubePoint_delta (Kronecker delta property on big-endian cube points), mleEval_cubePoint (reproduction of stored values), mleEval_ext (uniqueness of MLE from its evaluations), and mleEval_eq_iff (equivalence of pointwise equality to equality of tables). The file contains no sorry or admit and establishes the core semantics bridging big-endian and little-endian coordinate conventions for multilinear extensions.
• docs/wiki/repo-map.md: Two changes were made in docs/wiki/repo-map.md. For the multilinear subdirectory, the entry now specifies that 'coordinate semantics live in Semantics.lean; the terminal-successor kernel and shifted tables live in Next.lean'. For the fields subdirectory, the list of starting points was expanded from 'concrete fields' to 'concrete fields, field extensions'.
• docs/wiki/representations-and-bridges.md: The multilinear row of the summary table now lists CompPoly/Multilinear/Semantics.lean as an additional file, and two new paragraphs introduce the content of Semantics.lean (defines little-endian and big-endian Boolean-cube points, proves the reversal theorem between CompPoly evaluation and big-endian multilinear evaluation, and notes that coordinate conventions must be chosen explicitly) and Next.lean (defines the terminal-successor relation, its closed carry-chain form, shifted evaluation tables, and the shift identity in big-endian coordinates).
• 1 file(s) filtered as noise (lockfiles, generated, or trivial): CompPoly/Fields/README.md

---

Last updated: 2026-07-10 15:42 UTC.