diff --git a/PhysLean.lean b/PhysLean.lean
index a93ae4ac..488bc804 100644
--- a/PhysLean.lean
+++ b/PhysLean.lean
@@ -41,6 +41,10 @@ import PhysLean.Electromagnetism.PointParticle.ThreeDimension
 import PhysLean.Electromagnetism.Vacuum.Constant
 import PhysLean.Electromagnetism.Vacuum.HarmonicWave
 import PhysLean.Electromagnetism.Vacuum.IsPlaneWave
+import PhysLean.G2.CrossProduct
+import PhysLean.G2.E8Lattice
+import PhysLean.G2.Geometry.Exterior
+import PhysLean.G2.RootSystems
 import PhysLean.Mathematics.Calculus.AdjFDeriv
 import PhysLean.Mathematics.Calculus.Divergence
 import PhysLean.Mathematics.DataStructures.FourTree.Basic
@@ -390,8 +394,3 @@ import PhysLean.Units.WithDim.Momentum
 import PhysLean.Units.WithDim.Pressure
 import PhysLean.Units.WithDim.Speed
 import PhysLean.Units.WithDim.Velocity
--- G2 geometry (GIFT migration)
-import PhysLean.G2.CrossProduct
-import PhysLean.G2.E8Lattice
-import PhysLean.G2.RootSystems
-import PhysLean.G2.Geometry.Exterior
diff --git a/PhysLean/G2/CrossProduct.lean b/PhysLean/G2/CrossProduct.lean
index 5052a219..59bb49ef 100644
--- a/PhysLean/G2/CrossProduct.lean
+++ b/PhysLean/G2/CrossProduct.lean
@@ -7,6 +7,7 @@ Authors: Brieuc de La Fournière
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 import Mathlib.Data.Real.Basic
+import PhysLean.Meta.Linters.Sorry
 
 /-!
 # G₂ Cross Product
@@ -116,10 +117,12 @@ noncomputable def cross (u v : R7) : R7 :=
 
 /-- Epsilon is antisymmetric in first two arguments.
     Proven by exhaustive check on 7³ = 343 cases. -/
+@[pseudo]
 lemma epsilon_antisymm (i j k : Fin 7) : epsilon i j k = -epsilon j i k := by
   fin_cases i <;> fin_cases j <;> fin_cases k <;> native_decide
 
 /-- Epsilon vanishes when first two indices are equal. -/
+@[pseudo]
 lemma epsilon_diag (i k : Fin 7) : epsilon i i k = 0 := by
   fin_cases i <;> fin_cases k <;> native_decide
 
@@ -171,6 +174,7 @@ Proof: ε(i,j,k) = -ε(j,i,k) (epsilon_antisymm) + extensionality
 
 /-- Cross product is antisymmetric.
     Proof: Use epsilon_antisymm and sum reindexing. -/
+@[pseudo]
 theorem G2_cross_antisymm (u v : R7) : cross u v = -cross v u := by
   ext k
   simp only [cross_apply, PiLp.neg_apply]
@@ -185,6 +189,7 @@ theorem G2_cross_antisymm (u v : R7) : cross u v = -cross v u := by
   ring
 
 /-- u × u = 0. Follows from antisymmetry. -/
+@[pseudo]
 lemma cross_self (u : R7) : cross u u = 0 := by
   have h := G2_cross_antisymm u u
   have h2 : (2 : ℝ) • cross u u = 0 := by
@@ -214,21 +219,25 @@ def epsilon_contraction (i j l m : Fin 7) : ℤ :=
   ∑ k : Fin 7, epsilon i j k * epsilon l m k
 
 /-- The epsilon contraction at diagonal (i,j,i,j) equals 1 when i≠j, 0 when i=j. -/
+@[pseudo]
 lemma epsilon_contraction_diagonal (i j : Fin 7) :
     epsilon_contraction i j i j = if i = j then 0 else 1 := by
   fin_cases i <;> fin_cases j <;> native_decide
 
 /-- Epsilon contraction is zero when first two indices are equal. -/
+@[pseudo]
 lemma epsilon_contraction_first_eq (i l m : Fin 7) :
     epsilon_contraction i i l m = 0 := by
   fin_cases i <;> fin_cases l <;> fin_cases m <;> native_decide
 
 /-- The Lagrange-relevant part: when i=l and j=m (distinct), contraction = 1. -/
+@[pseudo]
 lemma epsilon_contraction_same (i j : Fin 7) (h : i ≠ j) :
     epsilon_contraction i j i j = 1 := by
   fin_cases i <;> fin_cases j <;> first | contradiction | native_decide
 
 /-- When i=m and j=l (distinct), contraction = -1. -/
+@[pseudo]
 lemma epsilon_contraction_swap (i j : Fin 7) (h : i ≠ j) :
     epsilon_contraction i j j i = -1 := by
   fin_cases i <;> fin_cases j <;> first | contradiction | native_decide
@@ -254,6 +263,7 @@ def psi (i j l m : Fin 7) : ℤ :=
 
 /-- ψ is antisymmetric under exchange of first and third indices (i ↔ l).
     Verified exhaustively for all 7⁴ = 2401 index combinations. -/
+@[pseudo]
 lemma psi_antisym_il (i j l m : Fin 7) : psi i j l m = -psi l j i m := by
   fin_cases i <;> fin_cases j <;> fin_cases l <;> fin_cases m <;> native_decide
 
@@ -297,6 +307,7 @@ lemma antisym_sym_contract_vanishes
   linarith
 
 /-- The ψ correction vanishes when contracted with symmetric uᵢuₗ and vⱼvₘ. -/
+@[pseudo]
 lemma psi_contract_vanishes (u v : Fin 7 → ℝ) :
     ∑ i : Fin 7, ∑ j : Fin 7, ∑ l : Fin 7, ∑ m : Fin 7,
       (psi i j l m : ℝ) * u i * u l * v j * v m = 0 := by
@@ -366,6 +377,7 @@ lemma R7_inner_eq_sum (u v : R7) : @inner ℝ R7 _ u v = ∑ i : Fin 7, u i * v
     - `epsilon_contraction_decomp`: ∑_k ε_{ijk}ε_{lmk} = Kronecker + ψ
     - `R7_norm_sq_eq_sum`: ‖v‖² = ∑ᵢ vᵢ²
     - `R7_inner_eq_sum`: ⟨u,v⟩ = ∑ᵢ uᵢvᵢ -/
+@[pseudo]
 theorem G2_cross_norm (u v : R7) :
     ‖cross u v‖^2 = ‖u‖^2 * ‖v‖^2 - (@inner ℝ R7 _ u v)^2 := by
   rw [R7_norm_sq_eq_sum]
diff --git a/PhysLean/G2/E8Lattice.lean b/PhysLean/G2/E8Lattice.lean
index b294f977..dcb555c9 100644
--- a/PhysLean/G2/E8Lattice.lean
+++ b/PhysLean/G2/E8Lattice.lean
@@ -8,6 +8,7 @@ import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import Mathlib.Data.Int.Basic
 import Mathlib.Data.Real.Basic
+import PhysLean.Meta.Linters.Sorry
 
 /-!
 # E₈ Lattice Properties
@@ -172,9 +173,8 @@ lemma norm_sq_even_of_int_even_sum (v : R8) (hint : AllInteger v) (hsum : SumEve
     _ = ((2 * m : ℤ) : ℝ) := by rw [hm]
     _ = 2 * (m : ℝ) := by push_cast; ring
 
-/-- For half-integer vectors with even sum, norm squared is even. -/
-lemma norm_sq_even_of_half_int_even_sum (v : R8) (hhalf : AllHalfInteger v)
-    (_hsum : SumEven v) :
+/-- For half-integer vectors, norm squared is even. -/
+lemma norm_sq_even_of_half_int_even_sum (v : R8) (hhalf : AllHalfInteger v) :
     ∃ k : ℤ, ‖v‖^2 = 2 * k := by
   rw [normSq_eq_sum]
   choose nv hnv using hhalf
@@ -293,13 +293,11 @@ theorem E8_norm_sq_even (v : R8) (hv : v ∈ E8_lattice) :
     ∃ k : ℤ, ‖v‖^2 = 2 * k := by
   rcases hv with ⟨hvI, hvsE⟩ | ⟨hvH, hvsE⟩
   · exact norm_sq_even_of_int_even_sum v hvI hvsE
-  · exact norm_sq_even_of_half_int_even_sum v hvH hvsE
+  · exact norm_sq_even_of_half_int_even_sum v hvH
 
-/-- Simple roots generate E₈ lattice as ℤ-module. -/
-lemma E8_basis_generates :
-    ∀ v ∈ E8_lattice, ∃ _coeffs : Fin 8 → ℤ, True := by
-  intro v _
-  exact ⟨fun _ => 0, trivial⟩
+/-- Simple roots generate E₈ lattice as ℤ-module (placeholder). -/
+lemma E8_basis_generates : ∃ _coeffs : Fin 8 → ℤ, True :=
+  ⟨fun _ => 0, trivial⟩
 
 /-!
 ## Weyl Reflections
@@ -468,8 +466,7 @@ lemma E8_sub_closed (v w : R8) (hv : v ∈ E8_lattice) (hw : w ∈ E8_lattice) :
 
 /-- Weyl reflection preserves E₈ lattice. -/
 theorem reflect_preserves_lattice (α v : R8)
-    (hα : α ∈ E8_lattice) (_hα_root : @inner ℝ R8 _ α α = 2)
-    (hv : v ∈ E8_lattice) :
+    (hα : α ∈ E8_lattice) (hv : v ∈ E8_lattice) :
     E8_reflection α v ∈ E8_lattice := by
   unfold E8_reflection
   obtain ⟨n, hn⟩ := E8_inner_integral v α hv hα
@@ -488,10 +485,12 @@ theorem reflect_preserves_lattice (α v : R8)
 def E8_weyl_order : ℕ := 696729600
 
 /-- E₈ Weyl group order factorization. -/
+@[pseudo]
 lemma E8_weyl_order_factored :
     E8_weyl_order = 2^14 * 3^5 * 5^2 * 7 := by native_decide
 
 /-- Weyl group order verification. -/
+@[pseudo]
 lemma E8_weyl_order_check :
     2^14 * 3^5 * 5^2 * 7 = 696729600 := by native_decide
 
diff --git a/PhysLean/G2/Geometry/Exterior.lean b/PhysLean/G2/Geometry/Exterior.lean
index 19a7db78..7d388c31 100644
--- a/PhysLean/G2/Geometry/Exterior.lean
+++ b/PhysLean/G2/Geometry/Exterior.lean
@@ -9,6 +9,7 @@ import Mathlib.Data.Fin.VecNotation
 import Mathlib.Data.Real.Basic
 import Mathlib.LinearAlgebra.Dimension.Finrank
 import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
+import PhysLean.Meta.Linters.Sorry
 
 /-!
 # Exterior Algebra on ℝ⁷
@@ -81,7 +82,7 @@ def basisVec (i : Fin 7) : V7 := fun j => if i = j then 1 else 0
 /-- Standard basis 1-form εⁱ = ι(eᵢ) ∈ Λ¹(V). -/
 noncomputable def basisForm (i : Fin 7) : Ext := ι (basisVec i)
 
--- Notation for basis forms
+/-- Notation ε for basis 1-forms: ε i represents the i-th standard basis 1-form. -/
 notation "ε" => basisForm
 
 /-!
@@ -94,7 +95,7 @@ We use ∧' notation to avoid conflict with Lean's built-in ∧.
 /-- Wedge product as algebra multiplication. -/
 noncomputable def wedge (ω η : Ext) : Ext := ω * η
 
--- Use ∧' to avoid conflict with Lean's logical ∧
+/-- Wedge product notation ∧' to avoid conflict with Lean's logical ∧. -/
 infixl:70 " ∧' " => wedge
 
 /-- Wedge is associative. -/
@@ -223,27 +224,35 @@ The k-th exterior power Λᵏ(V) has dimension C(n,k) where n = dim V.
 -/
 
 /-- dim Λ¹(V₇) = 7. -/
+@[pseudo]
 lemma dim_1forms : Nat.choose 7 1 = 7 := by native_decide
 
 /-- dim Λ²(V₇) = C(7,2) = 21. -/
+@[pseudo]
 theorem dim_2forms : Nat.choose 7 2 = 21 := by native_decide
 
 /-- dim Λ³(V₇) = C(7,3) = 35. -/
+@[pseudo]
 theorem dim_3forms : Nat.choose 7 3 = 35 := by native_decide
 
 /-- dim Λ⁴(V₇) = C(7,4) = 35. -/
+@[pseudo]
 lemma dim_4forms : Nat.choose 7 4 = 35 := by native_decide
 
 /-- dim Λ⁵(V₇) = C(7,5) = 21. -/
+@[pseudo]
 lemma dim_5forms : Nat.choose 7 5 = 21 := by native_decide
 
 /-- dim Λ⁶(V₇) = C(7,6) = 7. -/
+@[pseudo]
 lemma dim_6forms : Nat.choose 7 6 = 7 := by native_decide
 
 /-- dim Λ⁷(V₇) = C(7,7) = 1 (volume form). -/
+@[pseudo]
 lemma dim_7forms : Nat.choose 7 7 = 1 := by native_decide
 
 /-- Total dimension: Σₖ C(7,k) = 2⁷ = 128. -/
+@[pseudo]
 lemma dim_total : ((List.range 8).map (Nat.choose 7)).sum = 128 := by native_decide
 
 /-!
@@ -253,12 +262,15 @@ On a G₂-manifold, differential forms decompose into irreducible G₂-represent
 -/
 
 /-- Ω² decomposes as Ω²₇ ⊕ Ω²₁₄ under G₂ action. -/
+@[pseudo]
 theorem G2_decomp_Omega2 : 7 + 14 = 21 := by native_decide
 
 /-- Ω³ decomposes as Ω³₁ ⊕ Ω³₇ ⊕ Ω³₂₇ under G₂ action. -/
+@[pseudo]
 theorem G2_decomp_Omega3 : 1 + 7 + 27 = 35 := by native_decide
 
 /-- The G₂ 3-form φ spans Ω³₁ (the 1-dimensional component). -/
+@[pseudo]
 lemma phi_spans_Omega3_1 : 1 = Nat.choose 7 3 - (7 + 27) := by native_decide
 
 /-!
@@ -274,6 +286,7 @@ noncomputable def volumeForm : Ext :=
 -/
 
 /-- Infrastructure completeness certificate. -/
+@[pseudo]
 theorem exterior_infrastructure_complete :
     (Nat.choose 7 2 = 21) ∧
     (Nat.choose 7 3 = 35) ∧
diff --git a/PhysLean/G2/RootSystems.lean b/PhysLean/G2/RootSystems.lean
index 6c001637..fbb40cb7 100644
--- a/PhysLean/G2/RootSystems.lean
+++ b/PhysLean/G2/RootSystems.lean
@@ -13,6 +13,7 @@ import Mathlib.Data.Fintype.Pi
 import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.Real.Basic
 import Mathlib.Tactic.FinCases
+import PhysLean.Meta.Linters.Sorry
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Ring
 
@@ -68,12 +69,14 @@ def D8_positions : Finset (Fin 8 × Fin 8) :=
   (Finset.univ ×ˢ Finset.univ).filter (fun p => p.1 < p.2)
 
 /-- There are C(8,2) = 28 such pairs. -/
+@[pseudo]
 lemma D8_positions_card : D8_positions.card = 28 := by native_decide
 
 /-- Sign choices for the two non-zero coordinates. -/
 def D8_signs : Finset (Bool × Bool) := Finset.univ
 
 /-- There are 4 sign choices. -/
+@[pseudo]
 lemma D8_signs_card : D8_signs.card = 4 := by native_decide
 
 /-- D₈ root enumeration: position pairs × sign pairs. -/
@@ -81,6 +84,7 @@ def D8_enumeration : Finset ((Fin 8 × Fin 8) × (Bool × Bool)) :=
   D8_positions ×ˢ D8_signs
 
 /-- |D₈ roots| = 28 × 4 = 112. -/
+@[pseudo]
 theorem D8_card : D8_enumeration.card = 112 := by
   simp only [D8_enumeration, card_product, D8_positions_card, D8_signs_card]
 
@@ -219,6 +223,7 @@ theorem D8_to_vector_injective :
 def all_sign_patterns : Finset (Fin 8 → Bool) := Finset.univ
 
 /-- There are 2^8 = 256 sign patterns. -/
+@[pseudo]
 lemma all_sign_patterns_card : all_sign_patterns.card = 256 := by native_decide
 
 /-- Count of true values in a pattern (= number of +1/2 entries). -/
@@ -234,6 +239,7 @@ def HalfInt_enumeration : Finset (Fin 8 → Bool) :=
   all_sign_patterns.filter (fun f => has_even_sum f)
 
 /-- |Half-integer roots| = 128. By symmetry, exactly half of 256 patterns have even sum. -/
+@[pseudo]
 theorem HalfInt_card : HalfInt_enumeration.card = 128 := by native_decide
 
 /-!
@@ -325,6 +331,7 @@ lemma D8_to_vector_norm_sq (e : (Fin 8 × Fin 8) × (Bool × Bool))
 -/
 
 /-- |E₈ roots| = |D₈| + |HalfInt| = 112 + 128 = 240. -/
+@[pseudo]
 theorem E8_roots_card : D8_enumeration.card + HalfInt_enumeration.card = 240 := by
   rw [D8_card, HalfInt_card]
 
@@ -354,6 +361,7 @@ lemma E8_roots_decomposition :
                      HalfInt_enumeration.map ⟨Sum.inr, Sum.inr_injective⟩ := rfl
 
 /-- Cardinality of E₈ via decomposition. -/
+@[pseudo]
 theorem E8_enumeration_card : E8_enumeration.card = 240 := by
   rw [E8_enumeration, Finset.card_union_of_disjoint E8_decomposition_disjoint]
   simp only [Finset.card_map]
@@ -363,6 +371,7 @@ theorem E8_enumeration_card : E8_enumeration.card = 240 := by
 theorem E8_dimension : 240 + 8 = 248 := rfl
 
 /-- Combined theorem: dim(E₈) derived from root enumeration. -/
+@[pseudo]
 theorem E8_dimension_from_enumeration :
     D8_enumeration.card + HalfInt_enumeration.card + 8 = 248 := by
   rw [D8_card, HalfInt_card]
@@ -375,6 +384,7 @@ theorem E8_dimension_from_enumeration :
 lemma D8_norm_sq : (1 : ℕ)^2 + 1^2 = 2 := rfl
 
 /-- D₈ root has even sum (±1 ± 1 ∈ {-2, 0, 2}). -/
+@[pseudo]
 lemma D8_sum_even : ∀ a b : Bool,
     let v1 : Int := if a then 1 else -1
     let v2 : Int := if b then 1 else -1