session 32: Grassmannian tangent + general dim accounting + probe results

Lean:
- exteriorPower_two_rank: dim(Λ²(M)) = C(dim(M), 2) — general formula
  subsumes rank-2 and rank-3 cases, gives dim(so(d)) = C(d,2)
- exteriorPower_two_of_rank_three: dim(Λ²(R³)) = 3 (write subspace)
- commutator_off_diagonal_range: P·[W,P]·P = 0
- commutator_off_diagonal_kernel: (1-P)·[W,P]·(1-P) = 0
  Together: [W,P] is purely off-diagonal in P-decomposition = Grassmannian tangent
- 44 theorems total, 0 sorry

Probed remaining TODOs:
- Controllability: dimensional accounting done, bracket-generation needs
  algebraic geometry ("generic") — multi-session
- Haar convergence: requires probability on compact groups — not algebraically accessible
- Birth indelibility: requires dynamical systems (unique trajectories) — not algebraically accessible
- Grassmannian: algebraic core done, overlap-specific mapping needs more structure

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

Author: isaacbowen

lean/LeanFoam/ThreeBody.lean

@@ -106,4 +106,49 @@ equality is the core structural fact.
 -- Rather than re-prove this, we note the Mathlib reference and
 -- formalize the structural identity the spec actually uses.
 
+/-!
+### Grassmannian tangent: [W, P] is off-diagonal
+
+The commutator of a write W with a projection P maps range(P) into
+ker(P) and ker(P) into range(P). It has no on-diagonal component.
+This is the algebraic content of the Grassmannian tangent: the
+perturbation lives in Hom(range(P), ker(P)), which IS T_P Gr(k,d).
+
+Spec reference: "three-body mapping" → "vertical structure (containment)
+is a Grassmannian tangent at the observer's slice"
+-/
+
+open Matrix in
+/-- The commutator [W, P] has zero projection onto range(P) → range(P).
+    Equivalently: P · [W, P] · P = 0 for any projection P.
+    The write doesn't map the observer's subspace back into itself. -/
+theorem commutator_off_diagonal_range
+    {n : Type*} [Fintype n] [DecidableEq n]
+    {R : Type*} [CommRing R]
+    (W P : Matrix n n R) (hP : P * P = P) :
+    P * (W * P - P * W) * P = 0 := by
+  have h : P * (W * P - P * W) * P = P * W * (P * P) - (P * P) * W * P := by
+    noncomm_ring
+  rw [h, hP, sub_self]
+
+open Matrix in
+/-- The commutator [W, P] has zero projection onto ker(P) → ker(P).
+    Equivalently: (1 - P) · [W, P] · (1 - P) = 0 for any projection P.
+    The write doesn't map the complement back into itself either.
+
+    Together with commutator_off_diagonal_range: [W, P] is purely
+    off-diagonal in the P-decomposition. It maps range(P) → ker(P) and
+    ker(P) → range(P). This IS the Grassmannian tangent T_P Gr(k,d). -/
+theorem commutator_off_diagonal_kernel
+    {n : Type*} [Fintype n] [DecidableEq n]
+    {R : Type*} [CommRing R]
+    (W P : Matrix n n R) (hP : P * P = P) :
+    (1 - P) * (W * P - P * W) * (1 - P) = 0 := by
+  have hP2 : P * (1 - P) = 0 := by rw [mul_sub, mul_one, hP, sub_self]
+  have hP3 : (1 - P) * P = 0 := by rw [sub_mul, one_mul, hP, sub_self]
+  have h : (1 - P) * (W * P - P * W) * (1 - P) =
+      (1 - P) * W * (P * (1 - P)) - ((1 - P) * P) * W * (1 - P) := by
+    noncomm_ring
+  rw [h, hP2, hP3]; simp
+
 end FoamSpec

lean/LeanFoam/WriteMap.lean

@@ -28,24 +28,27 @@ confined to a 2-plane, up to scalar. Proof: Λ²(2-plane) is 1-dimensional.
 Spec reference: "the writing map", constraint (a)+(b)+(c) → uniqueness.
 -/
 
-/-- For a 2-dimensional free module, dim(Λ²(M)) = 1.
-    The wedge product is the unique alternating 2-form up to scalar. -/
+/-- dim(Λ²(M)) = C(dim(M), 2). The general dimensional accounting for
+    write subspaces and so(d). Specific cases:
+    - dim = 2: C(2,2) = 1 (write uniqueness — the wedge is unique up to scalar)
+    - dim = 3: C(3,2) = 3 (write subspace per R³ observer)
+    - dim = d: C(d,2) = d(d-1)/2 = dim(so(d)) (the full target algebra) -/
+theorem exteriorPower_two_rank
+    (R : Type*) [CommRing R] [Nontrivial R]
+    (M : Type*) [AddCommGroup M] [Module R M]
+    [Module.Free R M] [Module.Finite R M] :
+    Module.finrank R (⋀[R]^2 M) = Nat.choose (Module.finrank R M) 2 := by
+  rw [exteriorPower.finrank_eq]
+
+/-- dim(Λ²(2-plane)) = 1. Write uniqueness: the wedge product is the
+    unique alternating 2-form on a 2-plane, up to scalar. -/
 theorem exteriorPower_two_of_rank_two
     (R : Type*) [CommRing R] [Nontrivial R]
     (M : Type*) [AddCommGroup M] [Module R M]
     [Module.Free R M] [Module.Finite R M]
     (hdim : Module.finrank R M = 2) :
     Module.finrank R (⋀[R]^2 M) = 1 := by
-  rw [exteriorPower.finrank_eq, hdim]
-  native_decide
-
-/-- Specialization to ℝ. -/
-theorem write_map_unique_real
-    (V : Type*) [AddCommGroup V] [Module ℝ V]
-    [Module.Free ℝ V] [Module.Finite ℝ V]
-    (hdim : Module.finrank ℝ V = 2) :
-    Module.finrank ℝ (⋀[ℝ]^2 V) = 1 :=
-  exteriorPower_two_of_rank_two ℝ V hdim
+  rw [exteriorPower_two_rank, hdim]; native_decide
 
 /-!
 ## 2. Trace Zero — Writes Live in su(d)
@@ -97,7 +100,27 @@ theorem write_skew_symmetric {n : Type*} [Fintype n] [DecidableEq n]
   simp [transpose_sub, transpose_vecMulVec]
 
 /-!
-## 4. Stacked Write Trace
+## 4. Write Subspace Dimension
+
+The write subspace for an R³ observer is Λ²(R³), which is 3-dimensional.
+This is the bottleneck: each observer can only write in 3 of the d²
+Lie algebra dimensions per step.
+
+Spec reference: "the writing map" → "the write subspace is exactly
+3-dimensional per observer — the exterior algebra Λ²(R³)"
+-/
+
+/-- dim(Λ²(R³)) = 3. The write subspace per R³ observer is 3-dimensional. -/
+theorem exteriorPower_two_of_rank_three
+    (R : Type*) [CommRing R] [Nontrivial R]
+    (M : Type*) [AddCommGroup M] [Module R M]
+    [Module.Free R M] [Module.Finite R M]
+    (hdim : Module.finrank R M = 3) :
+    Module.finrank R (⋀[R]^2 M) = 3 := by
+  rw [exteriorPower_two_rank, hdim]; native_decide
+
+/-!
+## 5. Stacked Write Trace
 
 For complex vectors (stacked observer), the write d⊗m† − m⊗d† has
 nonzero trace. Unlike the real case (write_traceless), the stacked

lean/README.md

@@ -8,8 +8,8 @@ Mechanically verified results from [the measurement solution](../README.md). Eac
 
 | theorem | spec reference | statement |
 |---------|---------------|-----------|
+| `exteriorPower_two_rank` | writing map / controllability | dim(Λ²(M)) = C(dim(M), 2) — general dimensional accounting |
 | `exteriorPower_two_of_rank_two` | writing map: uniqueness | dim(Λ²(2-plane)) = 1 |
-| `write_map_unique_real` | writing map: uniqueness | specialization to R |
 | `write_traceless` | writing map: su(d) | tr(d⊗m - m⊗d) = 0 |
 | `write_skew_symmetric` | writing map: Lie algebra | (d⊗m - m⊗d)^T = -(d⊗m - m⊗d) |
 | `stacked_write_trace` | group: generative orthogonality | tr(d⊗m† - m⊗d†) = cross dot-product difference |
@@ -49,6 +49,8 @@ Mechanically verified results from [the measurement solution](../README.md). Eac
 | `mediation_factors` | three-body: mediation | M = P_A * Pi_B * P_C^T (associativity) |
 | `bypass_decomposition` | three-body: bypass | O_AC = M + bypass |
 | `roundtrip_symmetric` | three-body: round-trip | (M * M^T)^T = M * M^T |
+| `commutator_off_diagonal_range` | three-body: Grassmannian tangent | P * [W,P] * P = 0 (range → range component vanishes) |
+| `commutator_off_diagonal_kernel` | three-body: Grassmannian tangent | (1-P) * [W,P] * (1-P) = 0 (kernel → kernel component vanishes) |
 
 **Dynamics.lean** — frame recession under sequential writes.
 
@@ -67,11 +69,11 @@ Mechanically verified results from [the measurement solution](../README.md). Eac
 
 The following spec claims have computational verification (Python tests) but no Lean proof:
 
-- Controllability (so(d) generated by writes) — `test_controllability.py`
-- Haar convergence (L → 1/√2 of max) — derived in spec from convergence theorem for random walks on compact groups
-- Birth indelibility (no echo state property) — `test_echo_state.py`
-- Stacking mechanism (real ops closed in so(d)) — `test_stacking_mechanism.py`
-- Grassmannian vertical structure — `test_grassmannian_vertical.py`
+- Controllability (so(d) generated by writes) — partially formalized: dimensional accounting (`exteriorPower_two_rank` gives dim = C(n,2)), per-observer subspace is 3D. Remaining: brackets of generic observers span so(d). `test_controllability.py`
+- Haar convergence (L → 1/√2 of max) — requires probability theory on compact groups (convergence theorem for random walks). Not algebraically accessible.
+- Birth indelibility (no echo state property) — requires dynamical systems theory (unique trajectories on compact manifolds, state-dependent attractors). Not algebraically accessible. `test_echo_state.py`
+- Stacking mechanism — partially formalized: so(d) closure (`commutator_skew_of_skew`), J²=-I even dim (`even_dim_of_complex_structure`), write in so(d) (`write_skew_symmetric`), stacked trace purely imaginary (`stacked_write_trace`, `dotProduct_star_conj`). Remaining: stacked pair generates su(d) (controllability-adjacent)
+- Grassmannian vertical structure — partially formalized: [W,P] is off-diagonal in P-decomposition (`commutator_off_diagonal_range`, `commutator_off_diagonal_kernel`). Remaining: tangent maps Knowable → Unknown specifically (requires overlap matrix structure). `test_grassmannian_vertical.py`
 
 ## Building