Integral lifting of the nonzero-product Leibniz equations (Theorem 9.1(3))

thm:integral-partial-lifting(3) and lem:one-sided-path-coefficients (integral-partial-lifts.tex). The equations eq:partial-leibniz-group are encoded by IsSol: a coefficient d r for each ray, zero on unshiftable rays, with d t = ε_L d r + ε_R d s on every nonzero product rs = t with shiftable output.

Deviation: only part (3) is used (cor:zero-supported-coverage), and it is proved directly: from a solution modulo two we build an integer solution, by the coefficient formulas of the proof of Theorem 9.1 — the two-sided part from a lift ω of its restriction to the two-sided rays (the freeness of W_χ, from the induction hypothesis, enters only here), the coefficients of generating one-sided rays by the first-arrow recursion (lem:one-sided-path-coefficients, with paths replaced by unique first arrows), canonical integer lifts X_a, and Y_b read off from the rows (Lemma 9.5).

def MultiplicativeBasisDeformations.RaySys.Sys.IsSol {V R L : Type} [AddCommGroup L] [DecidableEq L] [DecidableEq V] [Fintype R] (S : Sys V R L) (χ : L) {M : Type u_1} [AddCommGroup M] (d : R → M) : Prop

The nonzero-product Leibniz equations (eq:partial-leibniz-group).

The first-arrow recursion

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.fstA {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) : R

A chosen first arrow (an ordinary left divisor) of a nonidentity ray.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.fstRest {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) : R

The rest of a ray after its chosen first arrow.

theorem MultiplicativeBasisDeformations.RaySys.Sys.fstA_spec {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {r : R} (h : r ≠ S.P.e (S.P.src r)) : S.OL r (S.fstA r)

theorem MultiplicativeBasisDeformations.RaySys.Sys.fstRest_spec {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {r : R} (h : r ≠ S.P.e (S.P.src r)) : S.rr (S.fstA r) * S.rr (S.fstRest r) = S.rr r

def MultiplicativeBasisDeformations.RaySys.Sys.DLf {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (ω X : R → ℤ) : ℕ → R → ℤ

The recursion with fuel.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.DL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (ω X : R → ℤ) (r : R) : ℤ

The coefficient of a generating left-sided ray (eq:one-sided-path-coefficients): d_r = [p] + X_a for the two-sided prefix p and the first left-sided arrow a.

theorem MultiplicativeBasisDeformations.RaySys.Sys.dim2_of_TL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {r : R} (hT : S.TL χ r) : S.Dim2 r

theorem MultiplicativeBasisDeformations.RaySys.Sys.rest_TL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {r a w : R} (hr : S.IsGen r) (hT : S.TL χ r) (ha : S.Ord a) (hB : S.TB χ a) (hw : S.rr a * S.rr w = S.rr r) : S.IsGen w ∧ S.TL χ w ∧ S.P.deg (S.P.wt w) < S.P.deg (S.P.wt r)

The rest after a two-sided first arrow of a generating left-sided ray is generating and left-sided, of smaller degree.

theorem MultiplicativeBasisDeformations.RaySys.Sys.DLf_succ {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (ω X : R → ℤ) (n : ℕ) (r : R) : S.DLf χ ω X (n + 1) r = if S.TB χ (S.fstA r) then ω (S.fstA r) + S.DLf χ ω X n (S.fstRest r) else X (S.fstA r)

theorem MultiplicativeBasisDeformations.RaySys.Sys.DLf_eq_DL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω X : R → ℤ) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {r : R} (hr : S.IsGen r) (hT : S.TL χ r) (n : ℕ) (hn : (S.P.deg (S.P.wt r)).toNat + 1 ≤ n) : S.DLf χ ω X n r = S.DL χ ω X r

Fuel independence.

theorem MultiplicativeBasisDeformations.RaySys.Sys.DL_eq {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω X : R → ℤ) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {r a w : R} (hr : S.IsGen r) (hT : S.TL χ r) (ha : S.OL r a) (hw : S.rr a * S.rr w = S.rr r) : S.DL χ ω X r = if S.TB χ a then ω a + S.DL χ ω X w else X a

The first-arrow recursion.

theorem MultiplicativeBasisDeformations.RaySys.Sys.DL_prod {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω X : R → ℤ) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (hω : ∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) {r u v : R} (hr : S.IsGen r) (hT : S.TL χ r) (huv : S.rr u * S.rr v = S.rr r) (hu0 : u ≠ S.P.e (S.P.src u)) : (S.TL χ u → S.DL χ ω X r = S.DL χ ω X u) ∧ (S.TB χ u → S.DL χ ω X r = ω u + S.DL χ ω X v)

Lemma 9.4 (lem:one-sided-path-coefficients), product equations with generating left-sided output: d_t = d_r for a left-sided first factor, d_t = d_r + d_s for a two-sided one.

Endpoint layers of one-sided rays

theorem MultiplicativeBasisDeformations.RaySys.Sys.layer_TL_exists {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hprim : Prim χ) {t : R} (hT : S.TL χ t) : ∃ (i : ℕ) (t0 : R), S.IsGen t0 ∧ S.TL χ t0 ∧ S.rr t = S.qh χ (S.P.src t) ^ i * S.rr t0

A left-sided ray is a layer of a generating left-sided ray.

theorem MultiplicativeBasisDeformations.RaySys.Sys.layer_TL_unique {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) {t t0 t1 : R} {i j : ℕ} (hT : S.TL χ t) (h0 : S.IsGen t0) (h1 : S.IsGen t1) (hi : S.rr t = S.qh χ (S.P.src t) ^ i * S.rr t0) (hj : S.rr t = S.qh χ (S.P.src t) ^ j * S.rr t1) : i = j ∧ t0 = t1

Uniqueness of the layer decomposition.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.qr {V R L : Type} [AddCommGroup L] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : V) : R

A chosen local generator ray at x.

theorem MultiplicativeBasisDeformations.RaySys.Sys.qr_spec {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} (h : S.q x ≠ 0) : S.rr (S.qr x) = S.q x

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.DR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (ω Y : R → ℤ) (r : R) : ℤ

The coefficient of a generating right-sided ray, by the last-arrow recursion.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.DD {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (ω X Y : R → ℤ) (t : R) : ℤ

The integer coefficients (eq:one-sided-path-coefficients, eq:proper-successor-coefficients): ω on two-sided rays, j[q̂] + d_{r₀} on layers of generating one-sided rays, zero on unshiftable rays.

theorem MultiplicativeBasisDeformations.RaySys.Sys.DD_TB {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (ω X Y : R → ℤ) {t : R} (h : S.TB χ t) : S.DD χ ω X Y t = ω t

theorem MultiplicativeBasisDeformations.RaySys.Sys.DD_unshift {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (ω X Y : R → ℤ) {t : R} (h : ¬S.Shift χ t) : S.DD χ ω X Y t = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.DD_TL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (ω X Y : R → ℤ) (hχ : 0 < S.P.deg χ) {t t0 : R} {i : ℕ} (hT : S.TL χ t) (h0 : S.IsGen t0) (hi : S.rr t = S.qh χ (S.P.src t) ^ i * S.rr t0) : S.DD χ ω X Y t = ↑i * ω (S.qr (S.P.src t)) + S.DL χ ω X t0

theorem MultiplicativeBasisDeformations.RaySys.Sys.tr_nonlocal {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {t : R} (hT : S.TR χ t) : S.P.src t ≠ S.P.tgt t

theorem MultiplicativeBasisDeformations.RaySys.Sys.toOp_qh_pow {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (x : V) (n : ℕ) : S.P.toOp (S.qh χ x ^ n) = S.op.qh χ x ^ n

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_layer {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {t t0 : R} {j : ℕ} (h : S.rr t = S.rr t0 * S.qh χ (S.P.tgt t) ^ j) : S.op.rr t = S.op.qh χ (S.op.P.src t) ^ j * S.op.rr t0

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_layer' {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {t t0 : R} {j : ℕ} (h : S.op.rr t = S.op.qh χ (S.op.P.src t) ^ j * S.op.rr t0) : S.rr t = S.rr t0 * S.qh χ (S.P.tgt t) ^ j

theorem MultiplicativeBasisDeformations.RaySys.Sys.tr_factor {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {r r0 : R} {i : ℕ} (hT : S.TR χ r) (h : S.rr r = S.rr r0 * S.qh χ (S.P.tgt r) ^ i) (hr0 : r0 ≠ S.P.e (S.P.src r0)) : S.TR χ r0

theorem MultiplicativeBasisDeformations.RaySys.Sys.layer_TR_unique {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) {t t0 t1 : R} {i j : ℕ} (hT : S.TR χ t) (h0 : S.IsGen t0) (h1 : S.IsGen t1) (hi : S.rr t = S.rr t0 * S.qh χ (S.P.tgt t) ^ i) (hj : S.rr t = S.rr t1 * S.qh χ (S.P.tgt t) ^ j) : i = j ∧ t0 = t1

theorem MultiplicativeBasisDeformations.RaySys.Sys.layer_TR_exists {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hprim : Prim χ) {t : R} (hT : S.TR χ t) : ∃ (j : ℕ) (t0 : R), S.IsGen t0 ∧ S.TR χ t0 ∧ S.rr t = S.rr t0 * S.qh χ (S.P.tgt t) ^ j

theorem MultiplicativeBasisDeformations.RaySys.Sys.DD_TR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (ω X Y : R → ℤ) (hχ : 0 < S.P.deg χ) {t t0 : R} {j : ℕ} (hT : S.TR χ t) (h0 : S.IsGen t0) (hj : S.rr t = S.rr t0 * S.qh χ (S.P.tgt t) ^ j) : S.DD χ ω X Y t = S.DR χ ω Y t0 + ↑j * ω (S.qr (S.P.tgt t))

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_qr {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : V) : S.op.qr x = S.qr x

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_DD {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (ω X Y : R → ℤ) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (t : R) : S.op.DD χ ω Y X t = S.DD χ ω X Y t

The coefficients are self-dual under A₀ ↦ A₀ᵒᵖ, exchanging X and Y.

Two-sided rays

theorem MultiplicativeBasisDeformations.RaySys.Sys.tb_comm {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {u : R} (hB : S.TB χ u) : S.q (S.P.src u) * S.rr u = S.rr u * S.q (S.P.tgt u)

A two-sided ray commutes with the local generators.

theorem MultiplicativeBasisDeformations.RaySys.Sys.qr_TB {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {x : V} (h2 : S.q x ^ 2 ≠ 0) (hs : S.Supp χ x) : S.TB χ (S.qr x)

The local generator is two-sided when its square survives.

theorem MultiplicativeBasisDeformations.RaySys.Sys.ω_qpow {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (ω : R → ℤ) (hω : ∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) {u : R} (hu : S.TB χ u) (n : ℕ) {t : R} : S.TB χ t → S.q (S.P.src u) ^ n * S.rr u = S.rr t → ω t = ↑n * ω (S.qr (S.P.src u)) + ω u

ω along local powers of a two-sided ray: [q̂^n u] = n[q̂] + [u].

theorem MultiplicativeBasisDeformations.RaySys.Sys.eq_BL_gen {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω X Y : R → ℤ) (hω : ∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {r0 s0 t : R} (hr0 : S.IsGen r0) (hB : S.TB χ r0) (hs0 : S.IsGen s0) (hL : S.TL χ s0) (h : S.rr r0 * S.rr s0 = S.rr t) (ht : S.Shift χ t) : S.DD χ ω X Y t = ω r0 + S.DL χ ω X s0

Theorem 9.1, cases 2 and 3: generating inputs of types B, L.

theorem MultiplicativeBasisDeformations.RaySys.Sys.hω_op {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (ω : R → ℤ) (hω : ∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) (r s t : R) : S.op.TB χ r → S.op.TB χ s → S.op.TB χ t → S.op.rr r * S.op.rr s = S.op.rr t → ω t = ω r + ω s

theorem MultiplicativeBasisDeformations.RaySys.Sys.DR_eq {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω Y : R → ℤ) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {r b w : R} (hr : S.IsGen r) (hT : S.TR χ r) (hb : S.OR r b) (hw : S.rr w * S.rr b = S.rr r) : S.DR χ ω Y r = if S.TB χ b then ω b + S.DR χ ω Y w else Y b

The last-arrow recursion (the dual of DL_eq).

theorem MultiplicativeBasisDeformations.RaySys.Sys.DR_prod {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω Y : R → ℤ) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (hω : ∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) {r u v : R} (hr : S.IsGen r) (hT : S.TR χ r) (huv : S.rr u * S.rr v = S.rr r) (hv0 : v ≠ S.P.e (S.P.src v)) : (S.TR χ v → S.DR χ ω Y r = S.DR χ ω Y v) ∧ (S.TB χ v → S.DR χ ω Y r = S.DR χ ω Y u + ω v)

Lemma 9.4, dual: product equations with generating right-sided output.

theorem MultiplicativeBasisDeformations.RaySys.Sys.rest_TR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {r b w : R} (hr : S.IsGen r) (hT : S.TR χ r) (hb : S.Ord b) (hB : S.TB χ b) (hw : S.rr w * S.rr b = S.rr r) : S.IsGen w ∧ S.TR χ w ∧ S.P.deg (S.P.wt w) < S.P.deg (S.P.wt r)

theorem MultiplicativeBasisDeformations.RaySys.Sys.tb_factor {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {t f : R} {n : ℕ} (hB : S.TB χ t) (h : S.rr t = S.qh χ (S.P.src t) ^ n * S.rr f) (hf0 : f ≠ S.P.e (S.P.src f)) : S.TB χ f

A nonidentity factor f of a two-sided t = q̂^n f is two-sided.

theorem MultiplicativeBasisDeformations.RaySys.Sys.ω_powq {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (ω : R → ℤ) (hω : ∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) {u t : R} (hu : S.TB χ u) (n : ℕ) (ht : S.TB χ t) (h : S.rr u * S.q (S.P.tgt u) ^ n = S.rr t) : ω t = ω u + ↑n * ω (S.qr (S.P.tgt u))

ω along local powers on the right.

theorem MultiplicativeBasisDeformations.RaySys.Sys.nondeep_eq {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω X Y : R → ℤ) (hRC2 : ∀ (a b : R) (x : V), S.NdRow χ a b x → X a + Y b = 2 * ω (S.qr x)) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {x : V} {e l : R} (hN : S.NondeepRet χ x e l) : S.DL χ ω X e + S.DR χ ω Y l = 2 * ω (S.qr x)

The coefficient equation of a nondeep return (eq:nondeep-coefficient-row).

theorem MultiplicativeBasisDeformations.RaySys.Sys.crown_eq {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω X Y : R → ℤ) (hRC1 : ∀ (a b f : R), S.CrownRow χ a b f → X a + Y b = ω f) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (hω : ∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) {r0 s0 t : R} (hr0 : S.IsGen r0) (hTr : S.TL χ r0) (hs0 : S.IsGen s0) (hTs : S.TR χ s0) (h : S.rr r0 * S.rr s0 = S.rr t) (hg : S.IsGen t) (hBt : S.TB χ t) : ω t = S.DL χ ω X r0 + S.DR χ ω Y s0

Theorem 9.1, case 2, crown rows: generating inputs of types L, R with generating two-sided output (eq:generating-crown-row, after stripping two-sided prefixes and suffixes).

theorem MultiplicativeBasisDeformations.RaySys.Sys.eq_LR_gen {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω X Y : R → ℤ) (hRC2 : ∀ (a b : R) (x : V), S.NdRow χ a b x → X a + Y b = 2 * ω (S.qr x)) (hRC1 : ∀ (a b f : R), S.CrownRow χ a b f → X a + Y b = ω f) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (hω : ∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) {r0 s0 t : R} (hr0 : S.IsGen r0) (hTr : S.TL χ r0) (hs0 : S.IsGen s0) (hTs : S.TR χ s0) (h : S.rr r0 * S.rr s0 = S.rr t) (hBt : S.TB χ t) : ω t = S.DL χ ω X r0 + S.DR χ ω Y s0

Theorem 9.1, cases 2 and 4: generating inputs of types L, R with two-sided output.

theorem MultiplicativeBasisDeformations.RaySys.Sys.layer_TB_exists {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hprim : Prim χ) {t : R} (hB : S.TB χ t) (hl : S.P.src t ≠ S.P.tgt t) : ∃ (i : ℕ) (t0 : R), S.IsGen t0 ∧ S.TB χ t0 ∧ S.rr t = S.qh χ (S.P.src t) ^ i * S.rr t0

A two-sided ray is a layer of a generating two-sided ray.

theorem MultiplicativeBasisDeformations.RaySys.Sys.DD_qpow_TL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (ω X Y : R → ℤ) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {t t' : R} {m : ℕ} (hT : S.TL χ t) (hT' : S.TL χ t') (h : S.rr t = S.qh χ (S.P.src t') ^ m * S.rr t') : S.DD χ ω X Y t = ↑m * ω (S.qr (S.P.src t')) + S.DD χ ω X Y t'

The coefficient of a local power of a left-sided ray.

theorem MultiplicativeBasisDeformations.RaySys.Sys.ω_local {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (ω : R → ℤ) (hω : ∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) {r : R} {i : ℕ} (hB : S.TB χ r) (hr : S.rr r = S.q (S.P.src r) ^ i) : ω r = ↑i * ω (S.qr (S.P.src r))

ω of a local two-sided ray.

theorem MultiplicativeBasisDeformations.RaySys.Sys.eq_TL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω X Y : R → ℤ) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (hω : ∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) {r s t : R} (hr0 : r ≠ S.P.e (S.P.src r)) (hs0 : s ≠ S.P.e (S.P.src s)) (h : S.rr r * S.rr s = S.rr t) (hT : S.TL χ t) : (S.TL χ r → S.DD χ ω X Y t = S.DD χ ω X Y r) ∧ (S.TB χ r → S.DD χ ω X Y t = S.DD χ ω X Y r + S.DD χ ω X Y s)

Theorem 9.1, products with left-sided output (cases 1, 2, 3, 5).

theorem MultiplicativeBasisDeformations.RaySys.Sys.eq_TB {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω X Y : R → ℤ) (hRC2 : ∀ (a b : R) (x : V), S.NdRow χ a b x → X a + Y b = 2 * ω (S.qr x)) (hRC1 : ∀ (a b f : R), S.CrownRow χ a b f → X a + Y b = ω f) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (hω : ∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) {r s t : R} (hr0 : r ≠ S.P.e (S.P.src r)) (hs0 : s ≠ S.P.e (S.P.src s)) (h : S.rr r * S.rr s = S.rr t) (hBt : S.TB χ t) : S.DD χ ω X Y t = S.DD χ ω X Y r + S.DD χ ω X Y s

Theorem 9.1, products with two-sided output (cases 2, 4, 5).

theorem MultiplicativeBasisDeformations.RaySys.Sys.eq_TR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω X Y : R → ℤ) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (hω : ∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) {r s t : R} (hr0 : r ≠ S.P.e (S.P.src r)) (hs0 : s ≠ S.P.e (S.P.src s)) (h : S.rr r * S.rr s = S.rr t) (hT : S.TR χ t) : (S.TR χ s → S.DD χ ω X Y t = S.DD χ ω X Y s) ∧ (S.TB χ s → S.DD χ ω X Y t = S.DD χ ω X Y r + S.DD χ ω X Y s)

Theorem 9.1, products with right-sided output (the dual of eq_TL).

theorem MultiplicativeBasisDeformations.RaySys.Sys.isSol_DD {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω X Y : R → ℤ) (hRC2 : ∀ (a b : R) (x : V), S.NdRow χ a b x → X a + Y b = 2 * ω (S.qr x)) (hRC1 : ∀ (a b f : R), S.CrownRow χ a b f → X a + Y b = ω f) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (hω : ∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) : S.IsSol χ (S.DD χ ω X Y)

The integer coefficients solve all nonzero-product Leibniz equations (proof of Theorem 9.1, α well defined).

Solutions modulo two

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_isSol {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {M : Type u_1} [AddCommGroup M] {d : R → M} (hd : S.IsSol χ d) : S.op.IsSol χ d

theorem MultiplicativeBasisDeformations.RaySys.Sys.sol_TL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {M : Type u_1} [AddCommGroup M] {d : R → M} (hd : S.IsSol χ d) {r s t : R} (hr0 : r ≠ S.P.e (S.P.src r)) (hs0 : s ≠ S.P.e (S.P.src s)) (h : S.rr r * S.rr s = S.rr t) (hT : S.TL χ t) : (S.TL χ r → d t = d r) ∧ (S.TB χ r → d t = d r + d s)

The equations of a solution for products with left-sided output.

theorem MultiplicativeBasisDeformations.RaySys.Sys.sol_TB {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {M : Type u_1} [AddCommGroup M] {d : R → M} (hd : S.IsSol χ d) {r s t : R} (hr0 : r ≠ S.P.e (S.P.src r)) (hs0 : s ≠ S.P.e (S.P.src s)) (h : S.rr r * S.rr s = S.rr t) (hB : S.TB χ t) : d t = d r + d s

The equations of a solution for products with two-sided output.

theorem MultiplicativeBasisDeformations.RaySys.Sys.DL_mod {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω X : R → ℤ) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {d : R → ZMod 2} (hd : S.IsSol χ d) (hωd : ∀ (r : R), S.TB χ r → ↑(ω r) = d r) (hXd : ∀ (a : R), ↑(X a) = d a) {r : R} (hr : S.IsGen r) (hT : S.TL χ r) : ↑(S.DL χ ω X r) = d r

The recursion of DL computes any solution modulo two.

theorem MultiplicativeBasisDeformations.RaySys.Sys.sol_layer {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {M : Type u_1} [AddCommGroup M] {d : R → M} (hd : S.IsSol χ d) {t0 : R} (hT0 : S.TL χ t0) (i : ℕ) {t : R} : S.TL χ t → S.rr t = S.qh χ (S.P.src t0) ^ i * S.rr t0 → d t = i • d (S.qr (S.P.src t0)) + d t0

A solution along local powers of a left-sided ray: d(q̂^i t₀) = i d(q̂) + d(t₀).

theorem MultiplicativeBasisDeformations.RaySys.Sys.DD_mod_TL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω X Y : R → ℤ) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {d : R → ZMod 2} (hd : S.IsSol χ d) (hωd : ∀ (r : R), S.TB χ r → ↑(ω r) = d r) (hXd : ∀ (a : R), ↑(X a) = d a) {r : R} (hT : S.TL χ r) : ↑(S.DD χ ω X Y r) = d r

The coefficients reduce to a given solution modulo two on left-sided rays.

theorem MultiplicativeBasisDeformations.RaySys.Sys.DD_mod {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω X Y : R → ℤ) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {d : R → ZMod 2} (hd : S.IsSol χ d) (hωd : ∀ (r : R), S.TB χ r → ↑(ω r) = d r) (hXd : ∀ (a : R), ↑(X a) = d a) (hYd : ∀ (b : R), ↑(Y b) = d b) (r : R) : ↑(S.DD χ ω X Y r) = d r

The coefficients reduce to a given solution modulo two (βα = id in the proof of Theorem 9.1).

theorem MultiplicativeBasisDeformations.RaySys.Sys.sol_TR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {M : Type u_1} [AddCommGroup M] {d : R → M} (hd : S.IsSol χ d) {r s t : R} (hr0 : r ≠ S.P.e (S.P.src r)) (hs0 : s ≠ S.P.e (S.P.src s)) (h : S.rr r * S.rr s = S.rr t) (hT : S.TR χ t) (hTs : S.TR χ s) : d t = d s

The equations of a solution for products with right-sided output.

theorem MultiplicativeBasisDeformations.RaySys.Sys.crown_row_sol {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {M : Type u_1} [AddCommGroup M] {d : R → M} (hd : S.IsSol χ d) {a b f : R} (hr : S.CrownRow χ a b f) : d f = d a + d b

A crown row holds for every solution.

theorem MultiplicativeBasisDeformations.RaySys.Sys.nd_row_sol {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {d : R → ZMod 2} (hd : S.IsSol χ d) {a b : R} {x : V} (hr : S.NdRow χ a b x) : d a + d b = 0

A nondeep row holds modulo two for every solution.

The lift

def MultiplicativeBasisDeformations.RaySys.Sys.Xc {R : Type} (d : R → ZMod 2) (a : R) : ℤ

The canonical integer lift of the variable X_a.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.Yc {V R L : Type} [AddCommGroup L] [Fintype V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (ω : R → ℤ) (d : R → ZMod 2) (b : R) : ℤ

The variable Y_b, read off from a row containing it (eq:crown-coefficient-group).

theorem MultiplicativeBasisDeformations.RaySys.Sys.Xc_mod {R : Type} [Fintype R] [DecidableEq R] (d : R → ZMod 2) (a : R) : ↑(Xc d a) = d a

theorem MultiplicativeBasisDeformations.RaySys.Sys.rc1 {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω : R → ℤ) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {d : R → ZMod 2} (hd : S.IsSol χ d) (a b f : R) : S.CrownRow χ a b f → Xc d a + S.Yc χ ω d b = ω f

theorem MultiplicativeBasisDeformations.RaySys.Sys.rc2 {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω : R → ℤ) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {d : R → ZMod 2} (hd : S.IsSol χ d) (a b : R) (x : V) : S.NdRow χ a b x → Xc d a + S.Yc χ ω d b = 2 * ω (S.qr x)

theorem MultiplicativeBasisDeformations.RaySys.Sys.Yc_mod {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (ω : R → ℤ) (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {d : R → ZMod 2} (hd : S.IsSol χ d) (hωd : ∀ (r : R), S.TB χ r → ↑(ω r) = d r) (b : R) : ↑(S.Yc χ ω d b) = d b

theorem MultiplicativeBasisDeformations.RaySys.Sys.integral_lifting {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (hW : ∀ (w : R → ZMod 2), (∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → w t = w r + w s) → ∃ (ω : R → ℤ), (∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) ∧ ∀ (r : R), S.TB χ r → ↑(ω r) = w r) {d : R → ZMod 2} (hd : S.IsSol χ d) : ∃ (D : R → ℤ), S.IsSol χ D ∧ ∀ (r : R), ↑(D r) = d r

Theorem 9.1(3) (thm:integral-partial-lifting): every solution modulo two of the nonzero-product Leibniz equations lifts to an integer solution. The hypothesis hW is the lifting property of W_χ = W(Q_χ) (free by Lemma 9.2 and the induction hypothesis of Prop 8.3).