Q2Presentation.Lifting.FoxLedger

source

theorem Q2Presentation.Lifting.kernel_inv_eq_self {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (m : ↥E.N) :

m⁻¹ = m

Elements of an exponent-2 kernel are their own inverses.

source

def Q2Presentation.Lifting.foxShadow {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (q : Marking Yt.Y) (n : Gen → NAdd E) :

GExpr → NAdd E

The additive Fox shadow of a word along a base marking q, evaluated at a kernel-valued perturbation n of the generators. The powOmega2 case uses the uniform exponent (omega2Mod |Y|).val.

Equations

One or more equations did not get rendered due to their size.
Q2Presentation.Lifting.foxShadow E q n Q2Presentation.GExpr.one = 0
Q2Presentation.Lifting.foxShadow E q n (Q2Presentation.GExpr.gen a) = n a
Q2Presentation.Lifting.foxShadow E q n (u.mul v) = (Q2Presentation.Lifting.conjEndN E (v.eval q)) (Q2Presentation.Lifting.foxShadow E q n u) + Q2Presentation.Lifting.foxShadow E q n v
Q2Presentation.Lifting.foxShadow E q n u.inv = (Q2Presentation.Lifting.conjEndN E (u.eval q)⁻¹) (Q2Presentation.Lifting.foxShadow E q n u)
Q2Presentation.Lifting.foxShadow E q n (u.powNat k) = (∑ i ∈ Finset.range k, Q2Presentation.Lifting.conjEndN E (u.eval q) ^ i) (Q2Presentation.Lifting.foxShadow E q n u)

Instances For

source

def Q2Presentation.Lifting.perturb {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (q : Marking Yt.Y) (n : Gen → ↥E.N) :

Marking Yt.Y

The perturbed marking a ↦ q a · n a.

Equations

Q2Presentation.Lifting.perturb E q n a = q a * ↑(n a)

Instances For

source

theorem Q2Presentation.Lifting.mul_mem_pow {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (y : Yt.Y) (m : ↥E.N) (k : ℕ) :

(y * ↑m) ^ k = y ^ k * ↑(Additive.toMul ((∑ i ∈ Finset.range k, conjEndN E y ^ i) (Additive.ofMul m)))

Multiplicative-form power telescope: (y·m)^k = y^k · (Σ conj-telescope). The kernel term is the geometric sum of conjugations applied to m.

source

theorem Q2Presentation.Lifting.eval_perturb {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (q : Marking Yt.Y) (n : Gen → ↥E.N) (w : GExpr) :

w.eval (perturb E q n) = w.eval q * ↑(Additive.toMul (foxShadow E q (fun (a : Gen) => Additive.ofMul (n a)) w))

The Fox ledger (exact first-order law): evaluating any word at a kernel-perturbed marking multiplies the value by the word's Fox shadow.

source

theorem Q2Presentation.Lifting.foxShadow_eq_zero_of_eval_eq {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (q : Marking Yt.Y) (n : Gen → ↥E.N) (w : GExpr) (h1 : w.eval q = 1) (h2 : w.eval (perturb E q n) = 1) :

foxShadow E q (fun (a : Gen) => Additive.ofMul (n a)) w = 0

Row vanishing: if a word dies at both a marking and its perturbation, the perturbation's Fox shadow along that word is zero — the linear condition the relator rows impose on differences of lifts.