theorem Q2Presentation.Lifting.foxShadowGen_zero {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (w : GExpr) : foxShadowGen Φ.op q (fun (x : Gen) => 0) w = 0

The zero perturbation has zero shadow.

theorem Q2Presentation.Lifting.add_add_sub_cancel_char2 {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (a u : V) : a + (a - u) = u

Char-2 correction identity: a + (a - u) = u.

theorem Q2Presentation.Lifting.famRows_surjective_of_quot_and_sub {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (q : Marking Yt.Y) (hquot : ∀ (uv : (V ⧸ W) × V ⧸ W), ∃ (nh : Gen → V ⧸ W), (foxShadowGen (Φ.descend W hW).op q nh Q2Word.tameRelator, foxShadowGen (Φ.descend W hW).op q nh Q2Word.wildRelator) = uv) (hsub : ∀ (u v : V), u ∈ W → v ∈ W → ∃ (n : Gen → V), (∀ (a : Gen), n a ∈ W) ∧ (foxShadowGen Φ.op q n Q2Word.tameRelator, foxShadowGen Φ.op q n Q2Word.wildRelator) = (u, v)) (uv : V × V) : ∃ (n : Gen → V), (foxShadowGen Φ.op q n Q2Word.tameRelator, foxShadowGen Φ.op q n Q2Word.wildRelator) = uv

The family five-lemma: quotient rows surjective and submodule targets hit (by submodule-valued tuples) give full row surjectivity.

def Q2Presentation.Lifting.famHits {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (W : Submodule (ZMod 2) V) : Prop

Row-hitting inside an invariant window: targets in W are hit by W-valued tuples.

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.Lifting.famHits_bot {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) : famHits Φ q ⊥

theorem Q2Presentation.Lifting.famHits_top_surjective {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (h : famHits Φ q ⊤) (uv : V × V) : ∃ (n : Gen → V), (foxShadowGen Φ.op q n Q2Word.tameRelator, foxShadowGen Φ.op q n Q2Word.wildRelator) = uv

theorem Q2Presentation.Lifting.comap_stable {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (W' W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (hW' : ∀ (y : Yt.Y), ∀ m ∈ W', (Φ.op y) m ∈ W') (y : Yt.Y) (m : ↥W) : m ∈ Submodule.comap W.subtype W' → ((Φ.restrict W hW).op y) m ∈ Submodule.comap W.subtype W'

Stability transfers to the comap along the window inclusion.

@[reducible, inline]

abbrev Q2Presentation.Lifting.sectionFamily {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (W' W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (hW' : ∀ (y : Yt.Y), ∀ m ∈ W', (Φ.op y) m ∈ W') : OperatorFamily Yt (↥W ⧸ Submodule.comap W.subtype W')

The section family of a stable pair W' ≤ W.

Equations

• Q2Presentation.Lifting.sectionFamily Φ W' W hW hW' = (Φ.restrict W hW).descend (Submodule.comap W.subtype W') ⋯

theorem Q2Presentation.Lifting.foxShadowGen_restrict_coe {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (q : Marking Yt.Y) (n : Gen → ↥W) (w : GExpr) : W.subtype (foxShadowGen (Φ.restrict W hW).op q n w) = foxShadowGen Φ.op q (fun (a : Gen) => W.subtype (n a)) w

Coercion form of restricted shadows.

theorem Q2Presentation.Lifting.famHits_of_section_step {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (W' W : Submodule (ZMod 2) V) (hle : W' ≤ W) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (hW' : ∀ (y : Yt.Y), ∀ m ∈ W', (Φ.op y) m ∈ W') (hquot : ∀ (uv : (↥W ⧸ Submodule.comap W.subtype W') × ↥W ⧸ Submodule.comap W.subtype W'), ∃ (nh : Gen → ↥W ⧸ Submodule.comap W.subtype W'), (foxShadowGen (sectionFamily Φ W' W hW hW').op q nh Q2Word.tameRelator, foxShadowGen (sectionFamily Φ W' W hW hW').op q nh Q2Word.wildRelator) = uv) (hprev : famHits Φ q W') : famHits Φ q W

The dévissage step: if the (W', W)-section rows are surjective and famHits holds at W', then it holds at W.

def Q2Presentation.Lifting.famReach {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (W : Submodule (ZMod 2) V) : Prop

Reachability of a window: targets in W are hit by arbitrary ambient tuples. Unlike famHits, this predicate can cross trivial sections (whose connecting corrections need ambient inputs).

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.Lifting.famReach_bot {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) : famReach Φ q ⊥

theorem Q2Presentation.Lifting.famReach_top_surjective {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (h : famReach Φ q ⊤) (uv : V × V) : ∃ (n : Gen → V), (foxShadowGen Φ.op q n Q2Word.tameRelator, foxShadowGen Φ.op q n Q2Word.wildRelator) = uv

theorem Q2Presentation.Lifting.famReach_of_section_step {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (W' W : Submodule (ZMod 2) V) (hle : W' ≤ W) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (hW' : ∀ (y : Yt.Y), ∀ m ∈ W', (Φ.op y) m ∈ W') (hquot : ∀ (uv : (↥W ⧸ Submodule.comap W.subtype W') × ↥W ⧸ Submodule.comap W.subtype W'), ∃ (nh : Gen → ↥W ⧸ Submodule.comap W.subtype W'), (foxShadowGen (sectionFamily Φ W' W hW hW').op q nh Q2Word.tameRelator, foxShadowGen (sectionFamily Φ W' W hW hW').op q nh Q2Word.wildRelator) = uv) (hprev : famReach Φ q W') : famReach Φ q W

The reach dévissage step across a section with surjective rows: the chase runs at the ambient level, so the corrections may use ambient inputs.

theorem Q2Presentation.Lifting.famReach_all_of_steps {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] [Finite V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hstep : ∀ (W' W : Submodule (ZMod 2) V), W' < W → (∀ (y : Yt.Y), ∀ m ∈ W', (Φ.op y) m ∈ W') → (∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) → (∀ U < W, W' ≤ U → (∀ (y : Yt.Y), ∀ m ∈ U, (Φ.op y) m ∈ U) → U = W') → famReach Φ q W' → famReach Φ q W) (W₀ : Submodule (ZMod 2) V) (hst₀ : ∀ (y : Yt.Y), ∀ m ∈ W₀, (Φ.op y) m ∈ W₀) : famReach Φ q W₀

The generalized composition-series driver: any step rule that crosses each maximal stable pair drives famReach to every stable window.

theorem Q2Presentation.Lifting.famReach_top_of_steps {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] [Finite V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hstep : ∀ (W' W : Submodule (ZMod 2) V), W' < W → (∀ (y : Yt.Y), ∀ m ∈ W', (Φ.op y) m ∈ W') → (∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) → (∀ U < W, W' ≤ U → (∀ (y : Yt.Y), ∀ m ∈ U, (Φ.op y) m ∈ U) → U = W') → famReach Φ q W' → famReach Φ q W) : famReach Φ q ⊤

The driver at the top window.

theorem Q2Presentation.Lifting.famHits_top_of_simple_sections {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] [Finite V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hsec : ∀ (W' W : Submodule (ZMod 2) V), W' < W → ∀ (hW' : ∀ (y : Yt.Y), ∀ m ∈ W', (Φ.op y) m ∈ W') (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W), (∀ U < W, W' ≤ U → (∀ (y : Yt.Y), ∀ m ∈ U, (Φ.op y) m ∈ U) → U = W') → ∀ (uv : (↥W ⧸ Submodule.comap W.subtype W') × ↥W ⧸ Submodule.comap W.subtype W'), ∃ (nh : Gen → ↥W ⧸ Submodule.comap W.subtype W'), (foxShadowGen (sectionFamily Φ W' W hW hW').op q nh Q2Word.tameRelator, foxShadowGen (sectionFamily Φ W' W hW hW').op q nh Q2Word.wildRelator) = uv) : famHits Φ q ⊤

The composition-series driver: if every maximal stable step's section rows are surjective, the full rows are surjective.