Exact semantics and source accounting for repeated affine rounds

Every finite iterate records the actual round transcripts and preserves both original latent states. Its factored law is exactly a deterministic image of the original law, and the XOR of its side contributions is the actual repeated four-call algorithm. Conditional kernels remain normalized at impossible messages as well as messages of positive mass.

Original source envelopes remain valid throughout. Their total masses are multiplied by the short-message alphabet to powers twice and four times the number of rounds. These exact laws support the iteration in Chattopadhyay--Liao, Extractors for Sum of Two Sources, Theorem 6.1, printed pp.23--25: https://arxiv.org/abs/2110.12652. The statistical subset invariants and parameter choices are proved in Iteration.Extraction and Iteration.Parameters (affineCorrelationBreaker_parameters_dist_le), and the uniform runtime in Affine.Program (affineCorrelationBreakerSelectedEval_mem_FP).

theorem Algebraic.Cutwidth.Extractor.affineRoundsOutput_zero (n d h L e : ℕ) (x : Fin n → Bool) (y : Fin d → Bool) (row : Fin (matchedBlockOutputBits h L) → Bool) : affineRoundsOutput n d h L e 0 x y row = row

Zero rounds return the supplied old row without reading new randomness.

theorem Algebraic.Cutwidth.Extractor.affineRoundsOutput_succ (n d h L e i : ℕ) (x : Fin n → Bool) (y : Fin d → Bool) (row : Fin (matchedBlockOutputBits h L) → Bool) : affineRoundsOutput n d h L e (i + 1) x y row = affineRoundOutput n d h L e x y (affineRoundsOutput n d h L e i x y row)

Each additional round rereads the same original inputs and the preceding actual row.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.iterate_zero {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e : ℕ) : s.iterate e 0 = s

Zero transitions preserve the entire supplied state.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.iterate_succ {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e i : ℕ) : s.iterate e (i + 1) = (s.iterate e i).next e

The next actual state is obtained by the existing one-round observation construction.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.next_probability {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e : ℕ) (hw : IsProbabilityWeight s.weight) (hl : ∀ (z : Z), IsProbabilityWeight (s.left z)) (hr : ∀ (z : Z), IsProbabilityWeight (s.right z)) : IsProbabilityWeight (s.next e).weight ∧ (∀ (z : AffineRoundTranscript Z t L), IsProbabilityWeight ((s.next e).left z)) ∧ ∀ (z : AffineRoundTranscript Z t L), IsProbabilityWeight ((s.next e).right z)

One actual transition preserves all normalized factors.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.iterate_probability {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e i : ℕ) (hw : IsProbabilityWeight s.weight) (hl : ∀ (z : Z), IsProbabilityWeight (s.left z)) (hr : ∀ (z : Z), IsProbabilityWeight (s.right z)) : IsProbabilityWeight (s.iterate e i).weight ∧ (∀ (z : AffineIterationTranscript Z t L i), IsProbabilityWeight ((s.iterate e i).left z)) ∧ ∀ (z : AffineIterationTranscript Z t L i), IsProbabilityWeight ((s.iterate e i).right z)

Every finite actual iterate has normalized transcript and conditional kernels.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.iterate_source {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e i : ℕ) (z : AffineIterationTranscript Z t L i) : (s.iterate e i).source z = s.source (AffineIterationTranscript.origin i z)

The left source map always reads its unchanged original coordinate.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.iterate_mask {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e i : ℕ) (z : AffineIterationTranscript Z t L i) : (s.iterate e i).mask z = s.mask (AffineIterationTranscript.origin i z)

The right mask always reads its unchanged original coordinate.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.iterate_rightWords {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e i : ℕ) (z : AffineIterationTranscript Z t L i) : (s.iterate e i).rightWords z = s.rightWords (AffineIterationTranscript.origin i z)

All right source words remain the original words, including tampered copies.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.transcript_origin {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e i : ℕ) (p : (Z × B) × A) : AffineIterationTranscript.origin i (s.transcript e i p) = p.1.1

The actual accumulated transcript retains its original tag pointwise.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.iterate_factored {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e i : ℕ) (hw : IsProbabilityWeight s.weight) (hl : ∀ (z : Z), IsProbabilityWeight (s.left z)) (hr : ∀ (z : Z), IsProbabilityWeight (s.right z)) : mapWeight (s.lift e i) (factoredWeight s.weight s.left s.right) = factoredWeight (s.iterate e i).weight (s.iterate e i).left (s.iterate e i).right

The whole iterated factored law is exactly the original law with its actual transcript.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.iterate_rows_eq {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e i : ℕ) (p : (Z × B) × A) (j : Option (Fin t)) : (fun (k : Fin (matchedBlockOutputBits h L)) => (s.iterate e i).leftRows (s.transcript e i p) p.2 j k ^^ (s.iterate e i).rightRows (s.transcript e i p) p.1.2 j k) = affineRoundsOutput n d h L e i (fun (k : Fin n) => s.source p.1.1 p.2 k ^^ s.mask p.1.1 p.1.2 k) (s.rightWords p.1.1 p.1.2 j) fun (k : Fin (matchedBlockOutputBits h L)) => s.leftRows p.1.1 p.2 j k ^^ s.rightRows p.1.1 p.1.2 j k

Every honest or tampered masked row is the actual repeated semantic output.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.leftEnvelope_cap {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e i : ℕ) (μ : Z → ℝ) (hw : IsProbabilityWeight s.weight) (hl : ∀ (z : Z), IsProbabilityWeight (s.left z)) (hr : ∀ (z : Z), IsProbabilityWeight (s.right z)) (cap : ∀ (z : Z) (x₀ : Fin n → Bool), s.weight z * mapWeight (s.source z) (s.left z) x₀ ≤ μ z) (z : AffineIterationTranscript Z t L i) (x₀ : Fin n → Bool) : (s.iterate e i).weight z * mapWeight ((s.iterate e i).source z) ((s.iterate e i).left z) x₀ ≤ s.leftEnvelope e μ i z

The evolving left envelope bounds the unchanged original-left source masses.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.rightEnvelope_cap {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e i : ℕ) (ν : Z → ℝ) (hw : IsProbabilityWeight s.weight) (hl : ∀ (z : Z), IsProbabilityWeight (s.left z)) (hr : ∀ (z : Z), IsProbabilityWeight (s.right z)) (cap : ∀ (z : Z) (y₀ : Fin d → Bool), s.weight z * mapWeight (fun (b : B) => s.rightWords z b none) (s.right z) y₀ ≤ ν z) (z : AffineIterationTranscript Z t L i) (y₀ : Fin d → Bool) : (s.iterate e i).weight z * mapWeight (fun (b : B) => (s.iterate e i).rightWords z b none) ((s.iterate e i).right z) y₀ ≤ s.rightEnvelope e ν i z

The evolving right envelope bounds the original honest right-word masses.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.leftEnvelope_nonnegative {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e i : ℕ) (μ : Z → ℝ) (hw : IsProbabilityWeight s.weight) (hl : ∀ (z : Z), IsProbabilityWeight (s.left z)) (hr : ∀ (z : Z), IsProbabilityWeight (s.right z)) (nonnegative : ∀ (z : Z), 0 ≤ μ z) (z : AffineIterationTranscript Z t L i) : 0 ≤ s.leftEnvelope e μ i z

Nonnegative original-left envelopes remain nonnegative at every transcript.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.rightEnvelope_nonnegative {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e i : ℕ) (ν : Z → ℝ) (hw : IsProbabilityWeight s.weight) (hl : ∀ (z : Z), IsProbabilityWeight (s.left z)) (hr : ∀ (z : Z), IsProbabilityWeight (s.right z)) (nonnegative : ∀ (z : Z), 0 ≤ ν z) (z : AffineIterationTranscript Z t L i) : 0 ≤ s.rightEnvelope e ν i z

Nonnegative original-right envelopes remain nonnegative at every transcript.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.leftEnvelope_sum {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e i : ℕ) (μ : Z → ℝ) (hw : IsProbabilityWeight s.weight) (hl : ∀ (z : Z), IsProbabilityWeight (s.left z)) (hr : ∀ (z : Z), IsProbabilityWeight (s.right z)) : ∑ z : AffineIterationTranscript Z t L i, s.leftEnvelope e μ i z = ↑(Fintype.card (AffineRoundShortMessages t L)) ^ (2 * i) * ∑ z : Z, μ z

Each actual round multiplies the left-envelope total by the squared message alphabet.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.rightEnvelope_sum {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e i : ℕ) (ν : Z → ℝ) (hw : IsProbabilityWeight s.weight) (hl : ∀ (z : Z), IsProbabilityWeight (s.left z)) (hr : ∀ (z : Z), IsProbabilityWeight (s.right z)) : ∑ z : AffineIterationTranscript Z t L i, s.rightEnvelope e ν i z = ↑(Fintype.card (AffineRoundShortMessages t L)) ^ (4 * i) * ∑ z : Z, ν z

Each actual round multiplies the right-envelope total by the fourth-power message alphabet.