release: v3.4.6 — Lean 4.29.0 + Mathlib v4.29.0 upgrade

Toolchain bump with Mathlib breaking change adaptations.
Build: 8378 jobs, 0 errors, 0 sorry, 7 axioms.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: Brieuc

README.md

@@ -77,4 +77,4 @@ For extended observables, publications, and detailed analysis:
 
 [Changelog](contrib/CHANGELOG.md) | [MIT License](LICENSE)
 
-*GIFT Core v3.4.5*
+*GIFT Core v3.4.6*

contrib/CHANGELOG.md

@@ -5,6 +5,21 @@ All notable changes to GIFT Core will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [3.4.6] - 2026-03-31
+
+### Summary
+
+**Lean 4.29.0 + Mathlib v4.29.0 upgrade.** Toolchain bumped from v4.27.0. Adapts to Mathlib breaking changes: `SimpleGraph.loopless` → `Std.Irrefl`, `inner` takes explicit `𝕜`, `EuclideanSpace.*` → `PiLp.*` deprecations, `noncomputable` for `RCLike.toInnerProductSpaceReal`. Build: 8378 jobs, 0 errors, 0 sorry, 7 axioms.
+
+### Changed
+
+- **lean-toolchain**: v4.27.0 → v4.29.0
+- **lakefile.lean**: Mathlib + doc-gen4 pinned to v4.29.0, `require mathlib` moved last (dep resolution)
+- **Quaternions.lean**, **GraphTheory.lean**: `.loopless v` → `.loopless.irrefl v` (Std.Irrefl change)
+- **InnerProductSpace.lean**, **E8Lattice.lean**: `EuclideanSpace.*` → `PiLp.*`, `simp [inner, mul_comm]`
+- **G2CrossProduct.lean**: `inner` instance path fix via direct `inner` unfold
+- **DifferentialForms.lean**: `ConstantForms` marked `noncomputable`
+
 ## [3.4.5] - 2026-03-31
 
 ### Summary

contrib/docs/GIFT_STATUS.md

@@ -1,6 +1,6 @@
 # GIFT Framework Status
 
-**Version**: 3.4.5
+**Version**: 3.4.6
 **Date**: 2026-03-31
 **Proof Systems**: Lean 4 (v4.27.0 + Mathlib v4.27.0)
 

contrib/docs/USAGE.md

@@ -1,6 +1,6 @@
 # giftpy Usage Guide
 
-Complete documentation for the `giftpy` Python package (v3.4.5).
+Complete documentation for the `giftpy` Python package (v3.4.6).
 
 ## Installation
 

contrib/docs/index.md

@@ -15,4 +15,4 @@ This directory contains documentation for the GIFT Core formal verification proj
 
 ## Version
 
-GIFT Core v3.4.5
+GIFT Core v3.4.6

contrib/python/gift_core/__init__.py

@@ -4,7 +4,7 @@
 All values proven in Lean 4.
 460+ certified relations, 11 published axioms, modular certificate structure.
 
-v3.4.5 Features:
+v3.4.6 Features:
 - Certificate Modularization: Foundations / Predictions / Spectral pillars
 - Spectral Theory: algebraic ratio dim(G₂)/H* = 14/99, TCS bounds, Yang-Mills connection
 - Computed Spectrum: Q₂₂ signature (3,19), SD/ASD gap >2000×

contrib/python/gift_core/_version.py

@@ -1 +1 @@
-__version__ = "3.4.5"
+__version__ = "3.4.6"

contrib/python/gift_core/constants/__init__.py

@@ -1,5 +1,5 @@
 """
-GIFT Constants Package (v3.4.5).
+GIFT Constants Package (v3.4.6).
 
 All certified constants organized by theme:
 - algebra: E8, G2, F4, E6, E7, Weyl group