Finite-tuple central-coordinate escape

This is the finite-dimensional algebraic part of packet 7. A tuple of coefficient-left PBW terms with strictly decreasing active degrees is assumed to lie in a right S-submodule. If the submodule is also closed under left multiplication by the central coordinate, the commutator iterates isolate one coordinate at a time. Escape.ad_unit_production supplies the unit at the selected coordinate, and the right-module lemma in EscapeSpan then gives the whole free module.

The theorem deliberately stops at this local span result. It does not claim that a global Stafford correction family supplies the hypotheses.

theorem AlgebraicAnalysis.EscapeAssembly.iterate_commutatorVector_mem {S : Type u_2} [Ring S] {n : ℕ} (H : Submodule Sᵐᵒᵖ (Fin n → S)) (x : S) (hleft : ∀ v ∈ H, (fun (i : Fin n) => x * v i) ∈ H) {v : Fin n → S} (hv : v ∈ H) (k : ℕ) : (EscapeSpan.commutatorVector x)^[k] v ∈ H

def AlgebraicAnalysis.EscapeAssembly.knownCoordinates {n : ℕ} (m : ℕ) : Finset (Fin n)

Coordinates whose index is below the current active degree.

Equations

• AlgebraicAnalysis.EscapeAssembly.knownCoordinates m = {j : Fin n | ↑j < m}

def AlgebraicAnalysis.EscapeAssembly.residualVector {S : Type u_2} [Ring S] {n : ℕ} (v : Fin n → S) (m : ℕ) : Fin n → S

Remove the currently known coordinate contributions from a vector.

Equations

• AlgebraicAnalysis.EscapeAssembly.residualVector v m = v - ∑ j ∈ AlgebraicAnalysis.EscapeAssembly.knownCoordinates m, Pi.single j (v j)

theorem AlgebraicAnalysis.EscapeAssembly.residualVector_apply_lt {S : Type u_2} [Ring S] {n : ℕ} (v : Fin n → S) (m : ℕ) {j : Fin n} (hj : ↑j < m) : residualVector v m j = 0

theorem AlgebraicAnalysis.EscapeAssembly.residualVector_apply_not_lt {S : Type u_2} [Ring S] {n : ℕ} (v : Fin n → S) (m : ℕ) {j : Fin n} (hj : ¬↑j < m) : residualVector v m j = v j

theorem AlgebraicAnalysis.EscapeAssembly.finite_tuple_escape {E : Type u_1} {S : Type u_2} [DivisionRing E] [CharZero E] [Ring S] {n : ℕ} (D : Escape.CentralEscapeData) (p : Fin n → Polynomial E) (hp : ∀ (i : Fin n), p i ≠ 0) (hstrict : StrictAnti fun (i : Fin n) => (p i).natDegree) (H : Submodule Sᵐᵒᵖ (Fin n → S)) (hv : (fun (i : Fin n) => D.normal (p i)) ∈ H) (hleft : ∀ v ∈ H, (fun (i : Fin n) => D.embed D.coordinate * v i) ∈ H) : H = ⊤

The actual finite-tuple escape theorem. The only analytic-looking input is the PBW transport packaged by CentralEscapeData; all module operations are right-sided through Sᵐᵒᵖ.