Exact first-phase execution factors and source envelopes

The actual prefix, matched extraction, advice construction, and final matched extraction have an exact alternating transcript over the original left and right states. All kernels are normalized, including null rows. The XOR equations connect the executed masked program to the side-local maps used in that transcript.

The original left envelope pays for all first extraction outputs. The original right envelope pays for all initial seed-and-mask messages and all advice outputs. Opposite-side observations preserve envelope totals. These are exact execution and counting laws, with no statistical premise or conclusion about the component programs.

The message order follows Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), first phase of Theorem 6.1, printed p.23, using the observation rule of Lemma 3.25, printed p.15: https://arxiv.org/abs/2110.12652.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneFirstOutput_xor (n d L₀ e₀ : ℕ) (x mask : Fin n → Bool) (y : Fin d → Bool) : affinePhaseOneFirstOutput n d L₀ e₀ (fun (j : Fin n) => x j ^^ mask j) y = fun (j : Fin (matchedBlockOutputBits 64 L₀)) => affinePhaseOneFirstOutput n d L₀ e₀ x y j ^^ affinePhaseOneFirstOutput n d L₀ e₀ mask y j

The actual first extractor splits a masked input into its two XOR contributions.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneFirstLeft_eq (n d 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) (ys : Z → B → AffinePhaseOneCopies t d) (p : (Z × B) × A) : affinePhaseOneFirstLeft n t L₀ e₀ x (affinePhaseOneRightTranscript n d t L₀ e₀ mask ys p.1) p.2 = fun (i : Option (Fin t)) => affinePhaseOneFirstOutput n d 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)

Fixing the first right message makes every actual first output left-only.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneSecondRight_eq (n d t L₀ e₀ 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) (ys : Z → B → AffinePhaseOneCopies t d) (advice : Option (Fin t) → List Bool) (p : (Z × B) × A) : affinePhaseOneSecondRight d t L₀ L₁ e₁ ys advice (affinePhaseOneLeftTranscript n d t L₀ e₀ x mask ys p) p.1.2 = fun (i : Option (Fin t)) => affinePhaseOneSecondSeed n d L₀ e₀ 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) (advice i)

Fixing all first outputs makes every actual advice output right-only.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneOutput_eq_xor (n d t h L₀ e₀ L₁ e₁ er : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} (x : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (advice : Option (Fin t) → List Bool) (p : (Z × B) × A) (i : Option (Fin t)) : affinePhaseOneOutput n d h L₀ e₀ L₁ e₁ er (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) (advice i) = fun (j : Fin (matchedBlockOutputBits h L₁)) => affinePhaseOneOutputLeft n t h L₀ L₁ er x (affinePhaseOneTranscript n d t L₀ e₀ L₁ e₁ x mask ys advice p) p.2 i j ^^ affinePhaseOneOutputRight n t h L₀ L₁ er mask (affinePhaseOneTranscript n d t L₀ e₀ L₁ e₁ x mask ys advice p) p.1.2 i j

The actual final output is the XOR of its original-left and mask contributions.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneRight_probability (n d t L₀ e₀ : ℕ) {Z : Type u_1} {B : Type u_2} [Fintype Z] [Fintype B] (w : Z → ℝ) (r : Z → B → ℝ) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (hw : IsProbabilityWeight w) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affinePhaseOneRightWeight n d t L₀ e₀ w r mask ys) ∧ ∀ (z : AffinePhaseOneRightTranscript Z t L₀), IsProbabilityWeight (affinePhaseOneRightKernel n d t L₀ e₀ r mask ys z)

The first right observation has a normalized transcript and normalized right rows.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneLeft_probability (n d 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 → ℝ) (x : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affinePhaseOneLeftWeight n d t L₀ e₀ w l r x mask ys) ∧ (∀ (z : AffinePhaseOneLeftTranscript Z t L₀), IsProbabilityWeight (affinePhaseOneLeftKernel n t L₀ e₀ l x z)) ∧ ∀ (z : AffinePhaseOneLeftTranscript Z t L₀), IsProbabilityWeight (affinePhaseOneRightKernel n d t L₀ e₀ r mask ys z.1)

The first two observations have normalized transcript and original-state kernels.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneTranscript_probability (n d t L₀ e₀ 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 → ℝ) (x : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (advice : Option (Fin t) → List Bool) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affinePhaseOneTranscriptWeight n d t L₀ e₀ L₁ e₁ w l r x mask ys advice) ∧ (∀ (z : AffinePhaseOneTranscript Z t L₀ L₁), IsProbabilityWeight (affinePhaseOneTranscriptLeft n t L₀ e₀ L₁ l x z)) ∧ ∀ (z : AffinePhaseOneTranscript Z t L₀ L₁), IsProbabilityWeight (affinePhaseOneTranscriptRight n d t L₀ e₀ L₁ e₁ r mask ys advice z)

All three actual observations have normalized transcript and original-state kernels.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneRight_factored (n d 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 → ℝ) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (hr : ∀ (z : Z) (b : B), 0 ≤ r z b) : mapWeight (fun (p : (Z × B) × A) => ((affinePhaseOneRightTranscript n d t L₀ e₀ mask ys p.1, p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (affinePhaseOneRightWeight n d t L₀ e₀ w r mask ys) (fun (z : AffinePhaseOneRightTranscript Z t L₀) => l z.1) (affinePhaseOneRightKernel n d t L₀ e₀ r mask ys)

The first observed law is exactly the original law with its right message retained.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneLeft_factored (n d 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 → ℝ) (x : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (hr : ∀ (z : Z) (b : B), 0 ≤ r z b) : mapWeight (fun (p : (Z × B) × A) => ((affinePhaseOneLeftTranscript n d t L₀ e₀ x mask ys p, p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (affinePhaseOneLeftWeight n d t L₀ e₀ w l r x mask ys) (affinePhaseOneLeftKernel n t L₀ e₀ l x) fun (z : AffinePhaseOneLeftTranscript Z t L₀) => affinePhaseOneRightKernel n d t L₀ e₀ r mask ys z.1

Both first observations preserve the actual joint law of the original latent states.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneTranscript_factored (n d t L₀ e₀ 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 → ℝ) (x : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (advice : Option (Fin t) → List Bool) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : mapWeight (fun (p : (Z × B) × A) => ((affinePhaseOneTranscript n d t L₀ e₀ L₁ e₁ x mask ys advice p, p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (affinePhaseOneTranscriptWeight n d t L₀ e₀ L₁ e₁ w l r x mask ys advice) (affinePhaseOneTranscriptLeft n t L₀ e₀ L₁ l x) (affinePhaseOneTranscriptRight n d t L₀ e₀ L₁ e₁ r mask ys advice)

The complete actual first-phase transcript has the displayed exact factorization.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneRight_left_envelope (n d t L₀ e₀ : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (μ : Z → ℝ) (hr : ∀ (z : Z) (b : B), 0 ≤ r z b) (cap : ∀ (z : Z) (x₀ : Fin n → Bool), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (z : AffinePhaseOneRightTranscript Z t L₀) (x₀ : Fin n → Bool) : affinePhaseOneRightWeight n d t L₀ e₀ w r mask ys z * mapWeight (x z.1) (l z.1) x₀ ≤ affinePhaseOneRightLeftEnvelope n d t L₀ e₀ μ r mask ys z

The first right message scales the original-left envelope by its message probability.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneRight_right_envelope (n d t L₀ e₀ : ℕ) {Z : Type u_1} {B : Type u_2} {Y : Type u_3} [Fintype B] (w : Z → ℝ) (r : Z → B → ℝ) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (y : Z → B → Y) (ξ : Z → ℝ) (hw : ∀ (z : Z), 0 ≤ w z) (hr : ∀ (z : Z) (b : B), 0 ≤ r z b) (cap : ∀ (z : Z) (y₀ : Y), w z * mapWeight (y z) (r z) y₀ ≤ ξ z) (z : AffinePhaseOneRightTranscript Z t L₀) (y₀ : Y) : affinePhaseOneRightWeight n d t L₀ e₀ w r mask ys z * mapWeight (y z.1) (affinePhaseOneRightKernel n d t L₀ e₀ r mask ys z) y₀ ≤ ξ z.1

The original-right source pays for the first right message by copying its envelope.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneLeft_left_envelope (n d 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 → ℝ) (x : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (μ : Z → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (cap : ∀ (z : Z) (x₀ : Fin n → Bool), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (z : AffinePhaseOneLeftTranscript Z t L₀) (x₀ : Fin n → Bool) : affinePhaseOneLeftWeight n d t L₀ e₀ w l r x mask ys z * mapWeight (x z.1.1) (affinePhaseOneLeftKernel n t L₀ e₀ l x z) x₀ ≤ affinePhaseOneLeftEnvelope n d t L₀ e₀ μ r mask ys z

The original-left source pays for the family of first extraction outputs.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneLeft_right_envelope (n d t L₀ e₀ : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} {Y : Type u_4} [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (y : Z → B → Y) (ξ : Z → ℝ) (hw : ∀ (z : Z), 0 ≤ w z) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (hr : ∀ (z : Z) (b : B), 0 ≤ r z b) (cap : ∀ (z : Z) (y₀ : Y), w z * mapWeight (y z) (r z) y₀ ≤ ξ z) (z : AffinePhaseOneLeftTranscript Z t L₀) (y₀ : Y) : affinePhaseOneLeftWeight n d t L₀ e₀ w l r x mask ys z * mapWeight (y z.1.1) (affinePhaseOneRightKernel n d t L₀ e₀ r mask ys z.1) y₀ ≤ affinePhaseOneRightEnvelope n t L₀ e₀ ξ l x z

Observing the first extraction outputs preserves the right-source envelope total.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneTranscript_left_envelope (n d t L₀ e₀ 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 → ℝ) (x : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (advice : Option (Fin t) → List Bool) (μ : Z → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (cap : ∀ (z : Z) (x₀ : Fin n → Bool), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (z : AffinePhaseOneTranscript Z t L₀ L₁) (x₀ : Fin n → Bool) : affinePhaseOneTranscriptWeight n d t L₀ e₀ L₁ e₁ w l r x mask ys advice z * mapWeight (x z.1.1.1) (affinePhaseOneTranscriptLeft n t L₀ e₀ L₁ l x z) x₀ ≤ affinePhaseOneTranscriptLeftEnvelope n d t L₀ e₀ L₁ e₁ μ r mask ys advice z

The complete transcript preserves the displayed original-left source bound.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneTranscript_right_envelope (n d t L₀ e₀ L₁ e₁ : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} {Y : Type u_4} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (advice : Option (Fin t) → List Bool) (y : Z → B → Y) (ξ : Z → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (cap : ∀ (z : Z) (y₀ : Y), w z * mapWeight (y z) (r z) y₀ ≤ ξ z) (z : AffinePhaseOneTranscript Z t L₀ L₁) (y₀ : Y) : affinePhaseOneTranscriptWeight n d t L₀ e₀ L₁ e₁ w l r x mask ys advice z * mapWeight (y z.1.1.1) (affinePhaseOneTranscriptRight n d t L₀ e₀ L₁ e₁ r mask ys advice z) y₀ ≤ affinePhaseOneTranscriptRightEnvelope n t L₀ e₀ L₁ ξ l x z

The complete transcript preserves the displayed original-right source bound.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneRightLeftEnvelope_sum (n d t L₀ e₀ : ℕ) {Z : Type u_1} {B : Type u_2} [Fintype Z] [Fintype B] (μ : Z → ℝ) (r : Z → B → ℝ) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (hr : ∀ (z : Z), ∑ b : B, r z b = 1) : ∑ z : AffinePhaseOneRightTranscript Z t L₀, affinePhaseOneRightLeftEnvelope n d t L₀ e₀ μ r mask ys z = ∑ z : Z, μ z

A normalized right kernel preserves the first original-left envelope total.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneLeftEnvelope_sum (n d t L₀ e₀ : ℕ) {Z : Type u_1} {B : Type u_2} [Fintype Z] [Fintype B] (μ : Z → ℝ) (r : Z → B → ℝ) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (hr : ∀ (z : Z), ∑ b : B, r z b = 1) : ∑ z : AffinePhaseOneLeftTranscript Z t L₀, affinePhaseOneLeftEnvelope n d t L₀ e₀ μ r mask ys z = ↑(Fintype.card (AffinePhaseOneCopies t (matchedBlockOutputBits 64 L₀))) * ∑ z : Z, μ z

The left-envelope total pays exactly the number of first output families.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneRightEnvelope_sum (n t L₀ e₀ : ℕ) {Z : Type u_1} {A : Type u_2} [Fintype Z] [Fintype A] (ξ : Z → ℝ) (l : Z → A → ℝ) (x : Z → A → Fin n → Bool) (hl : ∀ (z : Z), ∑ a : A, l z a = 1) : ∑ z : AffinePhaseOneLeftTranscript Z t L₀, affinePhaseOneRightEnvelope n t L₀ e₀ ξ l x z = ↑(Fintype.card (AffinePhaseOneRightMessage t L₀)) * ∑ z : Z, ξ z

The right-envelope total after two stages pays exactly the first right-message size.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneTranscriptLeftEnvelope_sum (n d t L₀ e₀ L₁ e₁ : ℕ) {Z : Type u_1} {B : Type u_2} [Fintype Z] [Fintype B] (μ : Z → ℝ) (r : Z → B → ℝ) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (advice : Option (Fin t) → List Bool) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : ∑ z : AffinePhaseOneTranscript Z t L₀ L₁, affinePhaseOneTranscriptLeftEnvelope n d t L₀ e₀ L₁ e₁ μ r mask ys advice z = ↑(Fintype.card (AffinePhaseOneCopies t (matchedBlockOutputBits 64 L₀))) * ∑ z : Z, μ z

The final left-envelope total pays only the first output-family alphabet.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneTranscriptRightEnvelope_sum (n t L₀ e₀ L₁ : ℕ) {Z : Type u_1} {A : Type u_2} [Fintype Z] [Fintype A] (ξ : Z → ℝ) (l : Z → A → ℝ) (x : Z → A → Fin n → Bool) (hl : ∀ (z : Z), ∑ a : A, l z a = 1) : ∑ z : AffinePhaseOneTranscript Z t L₀ L₁, affinePhaseOneTranscriptRightEnvelope n t L₀ e₀ L₁ ξ l x z = ↑(Fintype.card (AffinePhaseOneCopies t (matchedBlockSeedBits L₁))) * ↑(Fintype.card (AffinePhaseOneRightMessage t L₀)) * ∑ z : Z, ξ z

The final right-envelope total pays both right-message alphabets.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneLeftEnvelope_nonnegative (n d t L₀ e₀ : ℕ) {Z : Type u_1} {B : Type u_2} [Fintype B] (μ : Z → ℝ) (r : Z → B → ℝ) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (nonnegative : ∀ (z : Z), 0 ≤ μ z) (hr : ∀ (z : Z) (b : B), 0 ≤ r z b) (z : AffinePhaseOneLeftTranscript Z t L₀) : 0 ≤ affinePhaseOneLeftEnvelope n d t L₀ e₀ μ r mask ys z

Nonnegative original-left envelopes remain nonnegative after the first two stages.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneRightEnvelope_nonnegative (n t L₀ e₀ : ℕ) {Z : Type u_1} {A : Type u_2} [Fintype A] (ξ : Z → ℝ) (l : Z → A → ℝ) (x : Z → A → Fin n → Bool) (nonnegative : ∀ (z : Z), 0 ≤ ξ z) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (z : AffinePhaseOneLeftTranscript Z t L₀) : 0 ≤ affinePhaseOneRightEnvelope n t L₀ e₀ ξ l x z

Nonnegative original-right envelopes remain nonnegative after the first two stages.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneTranscriptLeftEnvelope_nonnegative (n d t L₀ e₀ L₁ e₁ : ℕ) {Z : Type u_1} {B : Type u_2} [Fintype B] (μ : Z → ℝ) (r : Z → B → ℝ) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (advice : Option (Fin t) → List Bool) (nonnegative : ∀ (z : Z), 0 ≤ μ z) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (z : AffinePhaseOneTranscript Z t L₀ L₁) : 0 ≤ affinePhaseOneTranscriptLeftEnvelope n d t L₀ e₀ L₁ e₁ μ r mask ys advice z

The final original-left envelope is nonnegative, including null transcript rows.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneTranscriptRightEnvelope_nonnegative (n t L₀ e₀ L₁ : ℕ) {Z : Type u_1} {A : Type u_2} [Fintype A] (ξ : Z → ℝ) (l : Z → A → ℝ) (x : Z → A → Fin n → Bool) (nonnegative : ∀ (z : Z), 0 ≤ ξ z) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (z : AffinePhaseOneTranscript Z t L₀ L₁) : 0 ≤ affinePhaseOneTranscriptRightEnvelope n t L₀ e₀ L₁ ξ l x z

The final original-right envelope is nonnegative, including null transcript rows.

theorem Algebraic.Cutwidth.Extractor.card_affinePhaseOneCopies (t width : ℕ) : Fintype.card (AffinePhaseOneCopies t width) = (2 ^ width) ^ (t + 1)

There are exactly this many families of honest and tampered Boolean words.

theorem Algebraic.Cutwidth.Extractor.card_affinePhaseOneRightMessage (t L₀ : ℕ) : Fintype.card (AffinePhaseOneRightMessage t L₀) = (2 ^ (matchedBlockSeedBits L₀ + matchedBlockOutputBits 64 L₀)) ^ (t + 1)

The first right message contains all seed prefixes and all mask outputs.