theorem Q2Presentation.Lifting.markedAug_of_ops_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hone : ∀ (y : Yt.Y), Φ.op y = 1) : markedAug Φ q = ⊥

The marked window of a trivial family is zero.

theorem Q2Presentation.Lifting.diamond_trivial {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hone : ∀ (y : Yt.Y), Φ.op y = 1) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (u v : V) (huv : u + v ∈ markedAug Φ q) : ∃ (n : Gen → V), (famRowsMap Φ q) n = (u, v)

(♦) at trivial families: the marked window is hit by τ-slot tuples.

theorem Q2Presentation.Lifting.cup_famSingle_trivial {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hone : ∀ (y : Yt.Y), Φ.op y = 1) (h4 : (omega2Mod (Nat.card Yt.Y)).val % 4 = 1) (e : Gen → Module.Dual (ZMod 2) V) (v₀ : V) (h₀ : Gen) : cupForm Φ q (famSingle h₀ v₀) e = ∑ g : Gen, ((trivEval 1 Q2Word.tameRelator).zC g h₀ + (trivEval 1 Q2Word.wildRelator).zC g h₀) * (e g) v₀

The trivial cup pairing against a single-slot tuple contracts the mirror matrix column.

theorem Q2Presentation.Lifting.dualPairingFaithful_trivial {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hone : ∀ (y : Yt.Y), Φ.op y = 1) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (h4 : (omega2Mod (Nat.card Yt.Y)).val % 4 = 1) : dualPairingFaithful Φ q

Dual-pairing faithfulness at trivial families (the antidiagonal of the relator mirror matrix).