Revert "feat(algebraic): G2Rank Property 5 — full native_decide proof via explicit basis"

This reverts commit badce2f.

Author: Brieuc

GIFT/Algebraic/G2Rank.lean

@@ -107,101 +107,30 @@ theorem cartan_independent :
 ## Property 5: The joint centralizer has dimension exactly 2
 
 The centralizer of {H₁, H₂} in g₂ consists of all X ∈ g₂ with [X, H₁] = [X, H₂] = 0.
-Strategy: exhibit an explicit basis of g₂ (14 elements), form the 28×14 ad-constraint
-matrix (rows = adjoint action of H₁ and H₂ on each basis element), show it has rank 12.
-Then dim(centralizer) = 14 - 12 = 2.
+We show this is exactly the span of H₁ and H₂ by proving:
 
-Certificate generated by `private/canonical/scripts/gen_g2_rank_cert.py`.
+The 28×14 constraint matrix (from [b_k, H₁] and [b_k, H₂] for each g₂ basis element b_k)
+has rank 12 = 14 − 2. This means the centralizer has dimension 2 = rank(G₂).
+
+We encode this by exhibiting a 12×12 non-singular minor of the ad-constraint matrix,
+computed over ℤ. The constraint matrix entries involve the structure constants of g₂,
+which are determined by φ₀.
+
+For the Lean formalization, we verify the rank condition computationally:
+the 14×14 matrices ad(H₁) and ad(H₂) (acting on the g₂ Lie algebra via the bracket)
+jointly have kernel of dimension exactly 2.
 -/
 
-/-- Explicit basis of g₂ (14 antisymmetric 7×7 matrices over ℤ). -/
-private def g2Basis : Fin 14 → Matrix (Fin 7) (Fin 7) ℤ
-  | n => match n.val with
-  | 0 => !![0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, -1, 0, 0; 0, 0, 0, 1, 0, 0, 0; 0, 0, -1, 0, 0, 0, 0; 0, 1, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0]
-  | 1 => !![0, 0, 0, 0, 0, 0, 0; 0, 0, 0, -1, 0, 0, 0; 0, 0, 0, 0, -1, 0, 0; 0, 1, 0, 0, 0, 0, 0; 0, 0, 1, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0]
-  | 2 => !![0, 0, 0, 0, 0, 0, 0; 0, 0, 1, 0, 0, 0, 0; 0, -1, 0, 0, 0, 0, 0; 0, 0, 0, 0, -1, 0, 0; 0, 0, 0, 1, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0]
-  | 3 => !![0, 0, 0, 0, 0, -1, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, -1, 0, 0, 0; 0, 0, 1, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 1, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0]
-  | 4 => !![0, 0, 0, 0, 1, 0, 0; 0, 0, 0, 0, 0, -1, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; -1, 0, 0, 0, 0, 0, 0; 0, 1, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0]
-  | 5 => !![0, 0, 0, 1, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, -1, 0; -1, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 1, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0]
-  | 6 => !![0, 0, -1, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 1, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, -1, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 1, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0]
-  | 7 => !![0, -1, 0, 0, 0, 0, 0; 1, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, -1, 0; 0, 0, 0, 0, 1, 0, 0; 0, 0, 0, 0, 0, 0, 0]
-  | 8 => !![0, 0, 0, 0, 0, 0, -1; 0, 0, 0, -1, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 1, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 1, 0, 0, 0, 0, 0, 0]
-  | 9 => !![0, 0, 0, 1, 0, 0, 0; 0, 0, 0, 0, 0, 0, -1; 0, 0, 0, 0, 0, 0, 0; -1, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 1, 0, 0, 0, 0, 0]
-  | 10 => !![0, 0, 0, 0, -1, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, -1; 0, 0, 0, 0, 0, 0, 0; 1, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 1, 0, 0, 0, 0]
-  | 11 => !![0, -1, 0, 0, 0, 0, 0; 1, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, -1; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 1, 0, 0, 0]
-  | 12 => !![0, 0, 1, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; -1, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, -1; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 1, 0, 0]
-  | 13 => !![0, 0, 0, 0, 0, 0, 0; 0, 0, 1, 0, 0, 0, 0; 0, -1, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, 0; 0, 0, 0, 0, 0, 0, -1; 0, 0, 0, 0, 0, 1, 0]
-  | _ => 0
-
-/-- All 14 basis elements satisfy the infinitesimal G₂ condition. -/
-private theorem g2Basis_in_g2 : ∀ n : Fin 14, ∀ i j k : Fin 7,
-    ∑ a : Fin 7, g2Basis n a i * phi0Z a j k +
-    ∑ b : Fin 7, g2Basis n b j * phi0Z i b k +
-    ∑ c : Fin 7, g2Basis n c k * phi0Z i j c = 0 := by native_decide
-
-/-- The ad-constraint matrix (28×14 over ℤ): rows 0..13 = ad(H₁),
-    rows 14..27 = ad(H₂), acting on each g₂ basis element. -/
-private def adConstraint : Matrix (Fin 28) (Fin 14) ℤ := fun row col =>
-  match row.val, col.val with
-  | 2, 2 => 2
-  | 3, 2 => -1
-  | 4, 1 => -2
-  | 5, 1 => 1
-  | 8, 7 => -1
-  | 9, 7 => -1
-  | 10, 6 => 1
-  | 11, 6 => -2
-  | 12, 5 => -1
-  | 13, 5 => 2
-  | 14, 4 => 1
-  | 15, 4 => 1
-  | 16, 2 => 1
-  | 17, 13 => -1
-  | 18, 12 => -1
-  | 19, 6 => -1
-  | 20, 11 => 1
-  | 21, 7 => 1
-  | 21, 11 => -1
-  | 22, 10 => -1
-  | 23, 4 => 1
-  | 23, 10 => 1
-  | 24, 9 => 1
-  | 25, 5 => -1
-  | 26, 1 => -1
-  | 27, 8 => 1
-  | _, _ => 0
-
-/-- A 12×12 non-singular minor of adConstraint (det = 4), witnessing rank ≥ 12. -/
-private theorem adConstraint_rank12 :
-    let rows : Fin 12 → Fin 28 := ![4, 2, 14, 12, 10, 8, 27, 24, 22, 20, 18, 17]
-    let cols : Fin 12 → Fin 14 := ![1, 2, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13]
-    (adConstraint.submatrix rows cols).det ≠ 0 := by native_decide
-
-/-- Coordinates of H₁ and H₂ in the g₂ basis (g2Basis 0 = H₁, g2Basis 3 = H₂). -/
-private def h1Coords : Fin 14 → ℤ := ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
-private def h2Coords : Fin 14 → ℤ := ![0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
-
-/-- H₁ and H₂ are in the centralizer (kernel of adConstraint). -/
-private theorem cartan_in_centralizer :
-    adConstraint.mulVec h1Coords = 0 ∧
-    adConstraint.mulVec h2Coords = 0 := by native_decide
-
-/-- **Property 5**: The centralizer of {H₁, H₂} in g₂ has dimension exactly 2.
-
-    Proof:
-    - adConstraint has a 12×12 non-singular minor (adConstraint_rank12)
-    - rank(adConstraint) = 12, giving null(adConstraint) = 14 - 12 = 2
-    - H₁ and H₂ are independent elements of the centralizer
-    - Therefore centralizer = span{H₁, H₂}, dim = 2 -/
-theorem cartan_centralizer_dim_two :
-    (adConstraint.submatrix
-      (fun i : Fin 12 => (![4, 2, 14, 12, 10, 8, 27, 24, 22, 20, 18, 17] i))
-      (fun i : Fin 12 => (![1, 2, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13] i))).det ≠ 0 ∧
-    adConstraint.mulVec h1Coords = 0 ∧
-    adConstraint.mulVec h2Coords = 0 :=
-  ⟨adConstraint_rank12, cartan_in_centralizer.1, cartan_in_centralizer.2⟩
-
-/-- The rank of G₂ equals 2. -/
+-- The g₂ Lie algebra has a basis of 14 antisymmetric 7×7 matrices satisfying L_X(φ₀)=0.
+-- The joint kernel of ad(H₁) and ad(H₂) acting on this basis has dimension 2.
+-- This is verified by the rank computation in the Python certificate above.
+-- In Lean, we state this as:
+
+/-- The rank of G₂ equals 2: there exist two commuting, linearly independent elements
+of g₂ whose joint centralizer in g₂ has dimension exactly 2.
+
+This is a THEOREM, not a definition. It follows from the explicit Cartan generators
+H₁, H₂ exhibited above, whose properties are all verified by `native_decide`. -/
 theorem g2_rank_eq_two : GIFT.Algebraic.G2.rank_G2 = 2 := rfl
 
 /-!
@@ -215,9 +144,11 @@ theorem g2_rank_eq_two : GIFT.Algebraic.G2.rank_G2 = 2 := rfl
 | H₂ ∈ g₂ | L_{H₂}(φ₀) = 0 | native_decide |
 | Commute | [H₁,H₂] = 0 | native_decide |
 | Independent | rank-2 minor ≠ 0 | native_decide |
-| Centralizer | dim = 2 | native_decide (adConstraint 12×12 minor + kernel) |
+| Centralizer | dim = 2 | Python certificate (see g2_det_mul_gram_analysis.md) |
 
-All properties verified by `native_decide` over ℤ.
+The final `g2_rank_eq_two` unfolds to `rfl` because `rank_G2` is defined as 2.
+The CONTENT of the theorem is in Properties 1–6 above, which collectively
+JUSTIFY the definition value 2.
 -/
 
 end GIFT.Algebraic.G2Rank