The central-coordinate escape kernel

This file contains the part of the central-coordinate escape argument which is independent of the later Stafford module bookkeeping. The coefficient ring is a division ring E; normal is the coefficient-left PBW normal form for a differential Ore extension S; and commutator is the additive map w ↦ w x - x w. The only Ore-specific input needed by the kernel is the transport identity

normal (derivative p) = commutator (normal p).

The resulting theorem says that iterating ad(x) by the PBW degree produces the nonzero scalar d! · lc(p), hence a unit. The hypotheses are explicit so that a later concrete Ore-stage file must prove the transport identity rather than hiding it behind an axiom.

No module-span, simplicity, denominator, or geometric statement is included: those are separate packet obligations.

def AlgebraicAnalysis.Escape.commutator {S : Type u_2} [Ring S] (x : S) : S →+ S

The additive commutator map with a fixed right-hand coordinate x.

The orientation is the one used in the escape argument: adₓ(w) = w x - x w.

Equations

• AlgebraicAnalysis.Escape.commutator x = { toFun := fun (w : S) => w * x - x * w, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AlgebraicAnalysis.Escape.commutator_apply {S : Type u_2} [Ring S] (x w : S) : (commutator x) w = w * x - x * w

structure AlgebraicAnalysis.Escape.CentralEscapeData {E : Type u_1} {S : Type u_2} [DivisionRing E] [Ring S] : Type (max u_1 u_2)

Correct central-coordinate PBW data for a differential Ore stage.

• normal : Polynomial E ≃+ S

  Coefficient-left normal form for the Ore stage.

• embed : E →+* S

  Ring embedding of coefficients into the Ore stage.

• coordinate : E

  The central coefficient coordinate used by the commutator.

• normal_C (a : E) : self.normal (Polynomial.C a) = self.embed a
• embed_isUnit {a : E} : a ≠ 0 → IsUnit (self.embed a)
• ad_normal_derivative (p : Polynomial E) : (commutator (self.embed self.coordinate)) (self.normal p) = self.normal (Polynomial.derivative p)

theorem AlgebraicAnalysis.Escape.CentralEscapeData.iterate_commutator_normal {E : Type u_1} {S : Type u_2} [DivisionRing E] [Ring S] (D : CentralEscapeData) (p : Polynomial E) (k : ℕ) : (⇑(commutator (D.embed D.coordinate)))^[k] (D.normal p) = D.normal ((⇑Polynomial.derivative)^[k] p)

theorem AlgebraicAnalysis.Escape.CentralEscapeData.iterate_derivative_natDegree {E : Type u_1} [DivisionRing E] (p : Polynomial E) : (⇑Polynomial.derivative)^[p.natDegree] p = Polynomial.C (p.natDegree.factorial • p.leadingCoeff)

theorem AlgebraicAnalysis.Escape.CentralEscapeData.factorial_leadingCoeff_ne_zero {E : Type u_1} [DivisionRing E] [CharZero E] {p : Polynomial E} (hp : p ≠ 0) : p.natDegree.factorial • p.leadingCoeff ≠ 0

theorem AlgebraicAnalysis.Escape.CentralEscapeData.regular_action_injective {E : Type u_1} {S : Type u_2} [DivisionRing E] [Ring S] [CharZero E] (D : CentralEscapeData) (action : S →+* AddMonoid.End E) (haction : ∀ (a c : E), (action (D.embed a)) c = a * c) : Function.Injective ⇑action

Faithfulness of a differential-operator action from central-coordinate PBW data. The action only needs to agree with left multiplication on the coefficient embedding; iterated commutators then recover a nonzero leading coefficient of every nonzero normal polynomial.

theorem AlgebraicAnalysis.Escape.CentralEscapeData.ad_degree_reduction {E : Type u_1} {S : Type u_2} [DivisionRing E] [Ring S] (D : CentralEscapeData) {p : Polynomial E} (hpositive : p.natDegree ≠ 0) : (Polynomial.derivative p).natDegree < p.natDegree ∧ (commutator (D.embed D.coordinate)) (D.normal p) = D.normal (Polynomial.derivative p)

One commutator lowers a nonconstant PBW polynomial's degree.

theorem AlgebraicAnalysis.Escape.CentralEscapeData.ad_unit_production {E : Type u_1} {S : Type u_2} [DivisionRing E] [Ring S] (D : CentralEscapeData) [CharZero E] {p : Polynomial E} (hp : p ≠ 0) : IsUnit ((⇑(commutator (D.embed D.coordinate)))^[p.natDegree] (D.normal p))

Iterated ad(x) produces a nonzero coefficient, hence a unit.

Axiom report for the proof-critical kernel.