Exact execution factors of one affine extraction round

The four actual matched calls follow the second-phase construction of Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), Theorem 6.1, printed pp.23--25: https://arxiv.org/abs/2110.12652. The full transcript records right prefix masks, actual prefixes, middle seeds and mask outputs, actual short outputs, and final right seeds in their execution order.

The law is exactly the original factored law with these observations added. Both original latent states are retained, and every conditional kernel is normalized, including impossible messages. These algebraic and probability identities use no statistical guarantee for any component extractor.

theorem Algebraic.Cutwidth.Extractor.affineRoundPrefix_xor (h L : ℕ) (left right : Fin (matchedBlockOutputBits h L) → Bool) : (affineRoundPrefix h L fun (j : Fin (matchedBlockOutputBits h L)) => left j ^^ right j) = fun (j : Fin (matchedBlockSeedBits L)) => affineRoundPrefix h L left j ^^ affineRoundPrefix h L right j

False-completed prefixes commute with pointwise XOR at every row width.

theorem Algebraic.Cutwidth.Extractor.affineRoundPrefixLeftMessage_eq (h t L : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (p : (Z × B) × A) : affineRoundPrefixLeftMessage h t L wl (affineRoundPrefixMaskTranscript h t L wr p.1) p.2 = fun (i : Option (Fin t)) => affineRoundPrefix h L fun (j : Fin (matchedBlockOutputBits h L)) => wl p.1.1 p.2 i j ^^ wr p.1.1 p.1.2 i j

The left prefix message is exactly the prefix of each actual masked previous row.

theorem Algebraic.Cutwidth.Extractor.affineRoundMiddleSeedRight_eq (d h t L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (p : (Z × B) × A) : affineRoundMiddleSeedRight d t L e ys (affineRoundPrefixTranscript h t L wl wr p) p.1.2 = fun (i : Option (Fin t)) => affineRoundMiddleSeed d h L e (ys p.1.1 p.1.2 i) fun (j : Fin (matchedBlockOutputBits h L)) => wl p.1.1 p.2 i j ^^ wr p.1.1 p.1.2 i j

The right-only middle seed is the actual first right extraction.

theorem Algebraic.Cutwidth.Extractor.affineRoundMiddleLeftMessage_eq (d h t L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (p : (Z × B) × A) : affineRoundMiddleLeftMessage h t L e wl (affineRoundMiddleRightTranscript d h t L e wl wr ys p) p.2 = fun (i : Option (Fin t)) => affineRoundMiddleOutput d h L e (ys p.1.1 p.1.2 i) fun (j : Fin (matchedBlockOutputBits h L)) => wl p.1.1 p.2 i j ^^ wr p.1.1 p.1.2 i j

The left middle message is exactly the actual short extraction output.

theorem Algebraic.Cutwidth.Extractor.affineRoundFinalSeedRight_eq (d h t L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (p : (Z × B) × A) : affineRoundFinalSeedRight d t L e ys (affineRoundMiddleTranscript d h t L e wl wr ys p) p.1.2 = fun (i : Option (Fin t)) => affineRoundFinalSeed d h L e (ys p.1.1 p.1.2 i) fun (j : Fin (matchedBlockOutputBits h L)) => wl p.1.1 p.2 i j ^^ wr p.1.1 p.1.2 i j

The right-only final seed is the actual second right extraction.

theorem Algebraic.Cutwidth.Extractor.affineRoundOutput_eq_xor (n d h t L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} (x : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (p : (Z × B) × A) (i : Option (Fin t)) : (affineRoundOutput n d h L e (fun (j : Fin n) => x p.1.1 p.2 j ^^ mask p.1.1 p.1.2 j) (ys p.1.1 p.1.2 i) fun (j : Fin (matchedBlockOutputBits h L)) => wl p.1.1 p.2 i j ^^ wr p.1.1 p.1.2 i j) = fun (j : Fin (matchedBlockOutputBits h L)) => affineRoundOutputLeft n h t L e x (affineRoundTranscript d h t L e wl wr ys p) p.2 i j ^^ affineRoundOutputRight n h t L e mask (affineRoundTranscript d h t L e wl wr ys p) p.1.2 i j

Every actual next row is the XOR of its original-left and original-right contributions.

theorem Algebraic.Cutwidth.Extractor.affineRoundPrefixMask_probability (h t L : ℕ) {Z : Type u_1} {B : Type u_2} [Fintype Z] [Fintype B] (w : Z → ℝ) (r : Z → B → ℝ) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (hw : IsProbabilityWeight w) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affineRoundPrefixMaskWeight h t L w r wr) ∧ ∀ (z : Z × AffineRoundShortMessages t L), IsProbabilityWeight (affineRoundPrefixMaskRight h t L r wr z)

The first right observation has normalized transcript and right kernels.

theorem Algebraic.Cutwidth.Extractor.affineRoundPrefix_probability (h t L : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affineRoundPrefixWeight h t L w l r wl wr) ∧ (∀ (z : AffineRoundPrefixMaskTranscript Z t L × AffineRoundShortMessages t L), IsProbabilityWeight (affineRoundPrefixLeft h t L l wl z)) ∧ ∀ (z : AffineRoundPrefixTranscript Z t L), IsProbabilityWeight (affineRoundPrefixRight h t L r wr z)

After actual prefixes, the transcript and both original-state kernels are normalized.

theorem Algebraic.Cutwidth.Extractor.affineRoundMiddleRight_probability (d h t L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affineRoundMiddleRightWeight d h t L e w l r wl wr ys) ∧ (∀ (z : AffineRoundMiddleRightTranscript Z t L), IsProbabilityWeight (affineRoundPrefixLeft h t L l wl z.1)) ∧ ∀ (z : AffineRoundPrefixTranscript Z t L × AffineRoundShortMessages t L × AffineRoundShortMessages t L), IsProbabilityWeight (affineRoundMiddleRightKernel d h t L e r wr ys z)

Observing the first right seeds and short-row masks preserves normalization.

theorem Algebraic.Cutwidth.Extractor.affineRoundMiddle_probability (d h t L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affineRoundMiddleWeight d h t L e w l r wl wr ys) ∧ (∀ (z : AffineRoundMiddleRightTranscript Z t L × AffineRoundShortMessages t L), IsProbabilityWeight (affineRoundMiddleLeft h t L e l wl z)) ∧ ∀ (z : AffineRoundMiddleTranscript Z t L), IsProbabilityWeight (affineRoundMiddleRightKernel d h t L e r wr ys z.1)

After actual short rows, every conditional kernel remains normalized, including null rows.

theorem Algebraic.Cutwidth.Extractor.affineRoundTranscript_probability (d h t L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affineRoundTranscriptWeight d h t L e w l r wl wr ys) ∧ (∀ (z : AffineRoundTranscript Z t L), IsProbabilityWeight (affineRoundTranscriptLeft h t L e l wl z)) ∧ ∀ (z : AffineRoundMiddleTranscript Z t L × AffineRoundShortMessages t L), IsProbabilityWeight (affineRoundTranscriptRight d h t L e r wr ys z)

The full actual transcript and both original-state kernels are normalized.

theorem Algebraic.Cutwidth.Extractor.affineRoundPrefixMask_factored (h t L : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (hr : ∀ (z : Z) (b : B), 0 ≤ r z b) : mapWeight (fun (p : (Z × B) × A) => ((affineRoundPrefixMaskTranscript h t L wr p.1, p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (affineRoundPrefixMaskWeight h t L w r wr) (fun (z : Z × AffineRoundShortMessages t L) => l z.1) (affineRoundPrefixMaskRight h t L r wr)

Observing right prefix masks preserves the complete original factored law exactly.

theorem Algebraic.Cutwidth.Extractor.affineRoundPrefix_factored (h t L : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (hr : ∀ (z : Z) (b : B), 0 ≤ r z b) : mapWeight (fun (p : (Z × B) × A) => ((affineRoundPrefixTranscript h t L wl wr p, p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (affineRoundPrefixWeight h t L w l r wl wr) (affineRoundPrefixLeft h t L l wl) (affineRoundPrefixRight h t L r wr)

The actual prefix transcript has exactly the displayed original-state factorization.

theorem Algebraic.Cutwidth.Extractor.affineRoundMiddleRight_factored (d h t L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : mapWeight (fun (p : (Z × B) × A) => ((affineRoundMiddleRightTranscript d h t L e wl wr ys p, p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (affineRoundMiddleRightWeight d h t L e w l r wl wr ys) (fun (z : ((Z × AffineRoundShortMessages t L) × AffineRoundShortMessages t L) × AffineRoundShortMessages t L × AffineRoundShortMessages t L) => affineRoundPrefixLeft h t L l wl z.1) (affineRoundMiddleRightKernel d h t L e r wr ys)

The right seeds and short-row masks extend the exact actual factorization.

theorem Algebraic.Cutwidth.Extractor.affineRoundMiddle_factored (d h t L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : mapWeight (fun (p : (Z × B) × A) => ((affineRoundMiddleTranscript d h t L e wl wr ys p, p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (affineRoundMiddleWeight d h t L e w l r wl wr ys) (affineRoundMiddleLeft h t L e l wl) fun (z : (((Z × AffineRoundShortMessages t L) × AffineRoundShortMessages t L) × AffineRoundShortMessages t L × AffineRoundShortMessages t L) × AffineRoundShortMessages t L) => affineRoundMiddleRightKernel d h t L e r wr ys z.1

The actual short rows extend the exact actual factorization.

theorem Algebraic.Cutwidth.Extractor.affineRoundTranscript_factored (d h t L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : mapWeight (fun (p : (Z × B) × A) => ((affineRoundTranscript d h t L e wl wr ys p, p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (affineRoundTranscriptWeight d h t L e w l r wl wr ys) (affineRoundTranscriptLeft h t L e l wl) (affineRoundTranscriptRight d h t L e r wr ys)

The entire executed round transcript has the displayed exact original-state factorization.