version bump to v.26.0

[dhsorens]

this draft PR updated CompPoly to 4.26.0 and resolves the dependency issue on ExtTreeMapLemmas (mostly)

addresses #4 by importing the fork of ExtTreeMapLemmas referenced in this pull request; introduces three sorry TODOs (for now) resolved. Ideally, the pull request on ExtTreeMapLemmas should be merged so we don't have to use my personal fork.

[github-actions]

🤖 Gemini PR Summary

This Pull Request performs a major version upgrade for the CompPoly project to v4.26.0. The primary focus is aligning the project with the Lean 4.26.0 toolchain and its associated ecosystem, while resolving critical dependency bottlenecks.

Features

• Toolchain Upgrade: Upgraded the project to Lean version v4.26.0 and synchronized Mathlib dependencies to the corresponding version.
• Dependency Management: Migrated external library references from Std to Batteries across the codebase, following current Lean community standards.

Fixes

• Dependency Resolution (ExtTreeMapLemmas dependency #4): Resolved a blocking issue with ExtTreeMapLemmas by temporarily sourcing a specific fork that includes necessary compatibility fixes.
• Proof Completion: Successfully resolved and removed several sorry placeholders that were introduced during the dependency migration.
• CI/Linting: Updated style-exceptions.txt to include configuration files (lakefile, manifest, etc.), ensuring the CI pipeline passes with the new versioning.

Refactoring

• Proof Modernization: Simplified and optimized proofs in Lawful.lean and MvPolyEquiv.lean by utilizing the grind tactic.
• Naming Conventions: Standardized naming for bitwise induction cases and updated lemma references in Bitwise.lean to maintain alignment with upstream library changes.
• Code Quality: Applied standardized indentation and formatting across modified files.

Documentation

• Licensing: Added standard license headers to source files (e.g., Lawful.lean) to ensure legal compliance and project consistency.

---

Analysis of Changes

Metric	Count
📝 Files Changed	8
✅ Lines Added	48
❌ Lines Removed	43

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

CompPoly/Data/Nat/Bitwise.lean

• Lines 43, 76, 99, 242, 271, 276, 306, 337, 413, 486, 503, 515, 545, 552, 592, 661, 786, 909, 936, 961, 975: "The standard indentation is 2 spaces." (Mathlib Style Guide - Indentation)

CompPoly/Multivariate/Lawful.lean

• Line 7: "The file should then contain a module docstring (delimited by /-! and -/) explaining the content of the file." (Mathlib Documentation Style)
• Lines 89, 130, 137, 210, 211, 220, 221, 222: "The standard indentation is 2 spaces." (Mathlib Style Guide - Indentation)

---

📄 **Per-File Summaries**

• CompPoly/Data/Nat/Bitwise.lean: Updates naming conventions for bitwise induction cases and lemma references to align with standard libraries.
• CompPoly/Multivariate/CMvMonomial.lean: Update the vector import to use the Batteries library instead of Std.
• CompPoly/Multivariate/Lawful.lean: Added a license header, standardized code indentation, and simplified the proof of cast_fromUnlawful using the grind tactic.
• CompPoly/Multivariate/MvPolyEquiv.lean: Update library dependencies from Std to Batteries and refactor a proof step to utilize the grind tactic.
• lake-manifest.json: Update various project dependencies to newer versions, including mathlib v4.26.0, and update the repository URL for ExtTreeMapLemmas.
• lakefile.lean: Update the version of the mathlib dependency and change the source repository for the ExtTreeMapLemmas package.
• lean-toolchain: Update the Lean 4 toolchain version to v4.26.0.
• scripts/style-exceptions.txt: Adds style linting exceptions for project configuration files, including lakefile.lean, lake-manifest.json, and lean-toolchain.

---

Last updated: 2026-01-19 13:39 UTC.

[dhsorens]

all sorrys are resolved now. will lint before merging but keeping it as-is for now for ease of readability

[dhsorens]

@alexanderlhicks @Julek it would be great to have ExtTreeMapLemmas updated to 4.26.0 e.g. as done here or to have a copy of it that we can maintain as part of the org. Want to take the dependency off my personal fork. What makes the most sense? Can we e.g. move it into Verified-zkEVM or something and/or make a plan for it to be merged upstream into Batteries or sth?

UPDATE: after some discussion, we have forked ExtTreeMapLemmas into verified-zkevm and will see how much of it can be upstreamed/deprecated.

[dhsorens]

linting checks now pass on all files, merging and issuing the relevant release tag.