feat(multilinear): add fast/spec equivalence bridge

[eliasjudin]

Summary

Add CompPoly.Multilinear.FastSpecEquiv, introducing:

• CMlPolynomial.partialMobiusSpec, a theorem-local fast/spec intermediate for the Boolean-lattice Möbius transform;
• CMlPolynomial.lagrangeToMono_eq_lagrangeToMonoSpec, identifying the existing butterfly transform with the closed-form specification;
• multilinear regression coverage for the fast/spec equality theorem and the existing round-trip transform laws.

This PR adds proofs autoformalised by @Aristotle-Harmonic.

Motivation

lagrangeToMono was already the fast inverse transform used by the multilinear layer, but the repo still lacked a proof-backed theorem identifying it with the closed-form Möbius specification lagrangeToMonoSpec.

Mathematical content

For v : Vector R (2 ^ n) over an additive commutative group, the new module proves
lagrangeToMono n v = lagrangeToMonoSpec v.

The proof factors the butterfly algorithm through a partial Möbius specification that records the state after processing the higher levels of the Boolean cube. The step theorem shows that one butterfly level exactly updates this partial specification, and the base/final theorems identify the endpoints with the identity vector and lagrangeToMonoSpec respectively.

The resulting public theorem lagrangeToMono_eq_lagrangeToMonoSpec turns the existing fast transform into a proof-backed surface while preserving the existing round-trip relationship with monoToLagrange.

Testing

• ./scripts/update-lib.sh
• ./scripts/check-imports.sh
• ./scripts/lint-style.sh CompPoly/Multilinear/FastSpecEquiv.lean tests/CompPolyTests/Multilinear/FastSpecEquiv.lean tests/CompPolyTests.lean
• python3 ./scripts/check-docs-integrity.py
• lake build
• lake test
• rg -n "sorry|admit|axiom|unsafe" CompPoly.lean CompPoly/**/*.lean tests/**/*.lean

Refs #185

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

[github-actions]

🤖 Gemini PR Summary

Mathematical Formalization

• Fast/Spec Equivalence: Establishes the identity CMlPolynomial.lagrangeToMono_eq_lagrangeToMonoSpec, proving that the optimized butterfly Möbius transform matches its closed-form mathematical specification.
• Partial Möbius Specification: Introduces CMlPolynomial.partialMobiusSpec to model the transformation's intermediate states as it processes levels of the Boolean cube.
• Inductive Modeling: Uses a step theorem to show that each level of the butterfly algorithm correctly updates the partial specification, ultimately reaching the closed-form specification.
• Transform Correctness: Provides formal proof backing for multilinear representation round-trips involving lagrangeToMono and monoToLagrange.

Infrastructure and Refactoring

• Univariate Polynomial Backend: Refactors CPolynomial by replacing the manual powBySq (repeated squaring) implementation with standard Lean Semiring power operators.
• API Standardization: Simplifies npow definitions and associated proofs, such as toPoly_pow.
• Technical Debt: Removes redundant lemmas including pow_is_trimmed, pow_add, and powBySq_eq_pow in favor of standard algebraic machinery.
• Note on Scope: The draft summary describes significant refactors to the univariate CPolynomial infrastructure; however, these changes are not explicitly mentioned in the PR title or body, which focus on multilinear transforms.

Testing and Documentation

• Regression Testing: Adds a new test suite in tests/CompPolyTests/Multilinear/FastSpecEquiv.lean covering concrete decide examples and general theorem instantiations across various ring types.
• Documentation: Updates the "Representations and Bridges" documentation to feature the equivalence theorem as the formal correctness guarantee for the butterfly Möbius transform.
• Integration: Exports the equivalence proofs via the top-level CompPoly scope.

---

Statistics

Metric	Count
📝 Files Changed	9
✅ Lines Added	529
❌ Lines Removed	104

---

Lean Declarations

✏️ **Removed:** 5 declaration(s)

• theorem powBySq_eq_pow (p : CPolynomial.Raw R) : ∀ n : ℕ, powBySq p n = p ^ n in CompPoly/Univariate/Raw/Proofs.lean
• theorem pow_add (p : CPolynomial.Raw R) (a b : ℕ) : in CompPoly/Univariate/Raw/Proofs.lean
• def powBySq [Semiring R] [BEq R] (p : CPolynomial.Raw R) : Nat → CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean
• lemma val_pow [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Univariate/Basic.lean
• lemma pow_is_trimmed (p : CPolynomial.Raw R) (n : ℕ) : in CompPoly/Univariate/Raw/Proofs.lean

✏️ **Added:** 1 declaration(s)

• theorem lagrangeToMono_eq_lagrangeToMonoSpec in CompPoly/Multilinear/FastSpecEquiv.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The following violations of the style guide were identified:

• Module Layout: The file CompPoly/Multilinear/FastSpecEquiv.lean violates the rule: "keep the first user-facing correctness theorem next to the definition it justifies." The theorem lagrangeToMono_eq_lagrangeToMonoSpec justifies lagrangeToMono, which is defined in CompPoly/Multilinear/Basic.lean.
• Empty Lines: The following lines in CompPoly/Multilinear/FastSpecEquiv.lean violate the rule: "Avoid empty lines inside definitions or proofs."
  • Lines 95, 99, and 109 (inside partialMobiusSpec_base)
  • Lines 269, 271, 307, 345, and 353 (inside partialMobiusSpec_zero_eq_spec)
• Delimiters:
  • CompPoly/Multilinear/FastSpecEquiv.lean:51: Violates "Avoid using ; to separate tactics unless writing short, single-line tactic sequences." (The sequence involves multiple nested by_cases and is relatively complex).
  • CompPoly/Univariate/Basic.lean:820: Violates "Avoid parentheses where possible." ((X ^ n) should be X ^ n).
• Tactic Mode:
  • CompPoly/Univariate/Basic.lean:804: Violates "Place by at the end of the line preceding the tactic block."
  • CompPoly/Univariate/Basic.lean:805: Violates "Place by at the end of the line preceding the tactic block."
• Indentation:
  • CompPoly/Univariate/Basic.lean:806: Violates "Use 2 spaces for indentation." (Indented 6 spaces instead of 2 or 4).
• Functions:
  • CompPoly/Univariate/Basic.lean:838: Violates "Prefer fun x ↦ ... over λ x, ...." (Uses => instead of the standard ↦).
• Headers:
  • tests/CompPolyTests/Multilinear/FastSpecEquiv.lean:2: Violates "Use standard file headers including copyright..." (The year is listed as 2026).

---

📄 **Per-File Summaries**

• CompPoly.lean: This change updates the main library file to import the CompPoly.Multilinear.FastSpecEquiv module. It integrates new functionality related to fast specialization equivalence for multilinear polynomials into the library's top-level scope.
• CompPoly/Univariate/Basic.lean: This change refactors the Semiring instance for CPolynomial to use the standard power operator for npow instead of Raw.powBySq, simplifying the associated proofs. It removes the now-redundant val_pow lemma and updates the proof of C_mul_X_pow_eq_monomial to align with these structural changes. No sorry or admit placeholders were introduced.
• CompPoly/Univariate/Raw/Ops.lean: This change simplifies the polynomial operations by removing the powBySq definition, which implemented exponentiation via repeated squaring. The remaining pow definition's documentation was updated to reflect this removal, and the author list was adjusted.
• CompPoly/Univariate/Raw/Proofs.lean: This change removes the RepeatedSquaring section, which contained theorems relating powBySq to standard exponentiation and lemmas regarding power operations for CPolynomial.Raw. The removal includes the pow_is_trimmed, pow_add, and powBySq_eq_pow proofs, and updates the file's author list. No new sorry or admit placeholders were introduced.
• CompPoly/Univariate/ToPoly/Equiv.lean: This change simplifies the proof of the toPoly_pow lemma by replacing manual value expansions with the change tactic and the pow_succ_right theorem. No new theorems or sorry placeholders are introduced.
• docs/wiki/representations-and-bridges.md: This update documents the correctness proof for the butterfly Möbius transform used in multilinear polynomial representations. It adds references to the FastSpecEquiv.lean file and highlights the lagrangeToMono_eq_lagrangeToMonoSpec theorem as the primary proof of equivalence between the fast implementation and its specification.
• tests/CompPolyTests.lean: This change expands the test suite by importing the FastSpecEquiv multilinear test module. No new theorems, definitions, or placeholders were added to this file.
• tests/CompPolyTests/Multilinear/FastSpecEquiv.lean: This new test file provides regression tests verifying the equivalence between the fast butterfly Möbius transform (lagrangeToMono) and its closed-form specification. It utilizes concrete examples solved via decide, general theorem instantiations for various ring types, and round-trip property checks; no sorry or admit placeholders are present.
• CompPoly/Multilinear/FastSpecEquiv.lean: This file proves the equivalence between the butterfly-based Möbius transform (lagrangeToMono) and its closed-form specification (lagrangeToMonoSpec). It introduces a partialMobiusSpec definition to model intermediate transform states and provides an inductive proof of correctness across all butterfly levels without any sorry placeholders.

---

Last updated: 2026-04-08 12:22 UTC.

[dhsorens]

hey @eliasjudin , thanks for this PR! I believe this was recently merged with #193 , but I don't think we have the test suite, so we can merge this if you refactor the tests to reflect the merged changes?