Word support facts

theorem Q2Presentation.Lifting.tame_not_mentions_x0 : mentions Q2Word.tameRelator Gen.x0 = false

theorem Q2Presentation.Lifting.u1_not_mentions_x0 : mentions Q2Word.u1 Gen.x0 = false

theorem Q2Presentation.Lifting.x1conj_not_mentions_x0 : mentions (Q2Word.rconjExpr Q2Word.x1 Q2Word.sigma) Gen.x0 = false

theorem Q2Presentation.Lifting.sigma2_not_mentions_x0 : mentions Q2Word.sigma2 Gen.x0 = false

Triple support vanishing

theorem Q2Presentation.Lifting.heisEval_single_of_not_mentions {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (a : Gen) (x : V) (lam : Module.Dual (ZMod 2) V) (w : GExpr) (hw : mentions w a = false) : (heisEval Φ q (famSingle a x) (famSingle a lam) w).d = 0 ∧ (heisEval Φ q (famSingle a x) (famSingle a lam) w).e = 0 ∧ (heisEval Φ q (famSingle a x) (famSingle a lam) w).z = 0

Words not mentioning a generator have vanishing evaluation triples at pairs supported on it.

Geometric collapse

theorem Q2Presentation.Lifting.op_inv_eq_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (y : Yt.Y) (h : Φ.op y = 1) : Φ.op y⁻¹ = 1

Operator inverses of trivial operators are trivial.

theorem Q2Presentation.Lifting.norm_mul_self {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (T : Module.End (ZMod 2) V) (e : ℕ) (he : T ^ e = 1) (hepos : 0 < e) : (∑ i ∈ Finset.range e, T ^ i) * T = ∑ i ∈ Finset.range e, T ^ i

The odd-order norm absorbs its operator.

theorem Q2Presentation.Lifting.geom_sum_block_collapse {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (T : Module.End (ZMod 2) V) (e m : ℕ) (he : T ^ e = 1) (hm : Odd m) : ∑ i ∈ Finset.range (e * m), T ^ i = ∑ i ∈ Finset.range e, T ^ i

Block collapse: geometric sums over odd multiples of the order equal the norm.

First-order ledger values at x₀-singles

theorem Q2Presentation.Lifting.op_eval_x0tau {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hx0 : Φ.op (q Gen.x0) = 1) : Φ.op ((Q2Word.x0.mul Q2Word.tau).eval q) = Φ.op (q Gen.tau)

The u₀-evaluation operator is the τ-operator.

theorem Q2Presentation.Lifting.fox_u0_single {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hx0 : Φ.op (q Gen.x0) = 1) (e : ℕ) (hepos : 0 < e) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (c : V) : foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.u0 = (∑ i ∈ Finset.range e, Φ.op (q Gen.tau) ^ i) c

The u₀-ledger value: the odd-order norm.

theorem Q2Presentation.Lifting.fox_d0_single {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hx0 : Φ.op (q Gen.x0) = 1) (e : ℕ) (hepos : 0 < e) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (c : V) : foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.d0 = (∑ i ∈ Finset.range e, Φ.op (q Gen.tau) ^ i + 1) c

The d₀-ledger value: P + 1.

theorem Q2Presentation.Lifting.fox_z0_single {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hx0 : Φ.op (q Gen.x0) = 1) (c : V) : foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.z0 = (Φ.op (Q2Word.sigma2.eval q)) c

The z₀-ledger value: the σ₂-transport.