Actual states and transcripts of repeated affine rounds

Each state keeps the original left and right latent variables. A transition only observes the actual round messages, conditions the corresponding kernels, and computes the next row contributions. The original source maps are lifted along the previous-transcript projection. No new randomness, probability certificate, or extraction guarantee is part of a state.

The deterministic row iteration follows Chattopadhyay--Liao, Extractors for Sum of Two Sources, Theorem 6.1, printed pp.23--25: https://arxiv.org/abs/2110.12652.

def Algebraic.Cutwidth.Extractor.affineRoundsOutput (n d h L e : ℕ) : ℕ → (Fin n → Bool) → (Fin d → Bool) → (Fin (matchedBlockOutputBits h L) → Bool) → Fin (matchedBlockOutputBits h L) → Bool

Iterate actual rounds, rereading the same original source words at every step.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Cutwidth.Extractor.affineRoundsOutput n d h L e 0 x✝² x✝¹ x✝ = x✝

def Algebraic.Cutwidth.Extractor.affineRoundOrigin {Z : Type u_1} {t L : ℕ} (z : AffineRoundTranscript Z t L) : Z

Forget exactly the five observations added during one round.

Equations

• Algebraic.Cutwidth.Extractor.affineRoundOrigin z = z.1.1.1.1.1

def Algebraic.Cutwidth.Extractor.AffineIterationTranscript (Z : Type u) (t L : ℕ) : ℕ → Type u

The complete finite transcript after a specified number of actual rounds.

Equations

• Algebraic.Cutwidth.Extractor.AffineIterationTranscript Z t L 0 = Z
• Algebraic.Cutwidth.Extractor.AffineIterationTranscript Z t L i.succ = Algebraic.Cutwidth.Extractor.AffineRoundTranscript (Algebraic.Cutwidth.Extractor.AffineIterationTranscript Z t L i) t L

@[instance_reducible]

instance Algebraic.Cutwidth.Extractor.instFintypeAffineIterationTranscript {Z : Type u_1} [Fintype Z] (t L i : ℕ) : Fintype (AffineIterationTranscript Z t L i)

Finite initial transcripts remain finite under every finite number of observations.

Equations

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

def Algebraic.Cutwidth.Extractor.AffineIterationTranscript.origin {Z : Type u_1} {t L : ℕ} (i : ℕ) : AffineIterationTranscript Z t L i → Z

Project the complete accumulated transcript to its original tag.

Equations

• Algebraic.Cutwidth.Extractor.AffineIterationTranscript.origin 0 z = z
• Algebraic.Cutwidth.Extractor.AffineIterationTranscript.origin i.succ z = Algebraic.Cutwidth.Extractor.AffineIterationTranscript.origin i (Algebraic.Cutwidth.Extractor.affineRoundOrigin z)

structure Algebraic.Cutwidth.Extractor.AffineIterationState (n d h t L : ℕ) (Z : Type u_1) (A : Type u_2) (B : Type u_3) : Type (max (max u_1 u_2) u_3)

Actual factors and side maps, with both original latent state spaces unchanged.

• weight : Z → ℝ

  The current transcript's marginal weight.

• left : Z → A → ℝ

  The conditional weighting of the original left latent variable.

• right : Z → B → ℝ

  The conditional weighting of the original right latent variable.

• source : Z → A → Fin n → Bool

  The original left source word at the current transcript.

• mask : Z → B → Fin n → Bool

  The original right contribution to the masked left source word.

• rightWords : Z → B → AffinePhaseOneCopies t d

  All original right words, with the honest copy indexed by none.

• leftRows : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)

  The current long rows' original-left contributions.

• rightRows : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)

  The current long rows' original-right contributions.

noncomputable def Algebraic.Cutwidth.Extractor.AffineIterationState.next {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 : ℕ) : AffineIterationState n d h t L (AffineRoundTranscript Z t L) A B

Execute one round's actual observations and next-row computations.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.AffineIterationState.iterate {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 : ℕ) : AffineIterationState n d h t L (AffineIterationTranscript Z t L i) A B

The actual evolving factor state after a fixed number of rounds.

Equations

• s.iterate e 0 = s
• s.iterate e i.succ = (s.iterate e i).next e

noncomputable def Algebraic.Cutwidth.Extractor.AffineIterationState.transcript {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 × B) × A → AffineIterationTranscript Z t L i

The complete transcript computed from one fixed original pair of latent states.

Equations

• One or more equations did not get rendered due to their size.
• s.transcript e 0 x✝ = x✝.1.1

noncomputable def Algebraic.Cutwidth.Extractor.AffineIterationState.lift {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 Z t L i × B) × A

Reindex the original law by its actual transcript without discarding either latent state.

Equations

• s.lift e i p = ((s.transcript e i p, p.1.2), p.2)

noncomputable def Algebraic.Cutwidth.Extractor.AffineIterationState.leftEnvelope {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 : ℕ) (μ : Z → ℝ) (i : ℕ) : AffineIterationTranscript Z t L i → ℝ

Evolve the original-left joint envelope by the actual message probabilities.

Equations

• One or more equations did not get rendered due to their size.
• s.leftEnvelope e μ 0 = μ

noncomputable def Algebraic.Cutwidth.Extractor.AffineIterationState.rightEnvelope {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 : ℕ) (ν : Z → ℝ) (i : ℕ) : AffineIterationTranscript Z t L i → ℝ

Evolve the original-right joint envelope through the same actual observations.

Equations

• s.rightEnvelope e ν 0 = ν
• s.rightEnvelope e ν i.succ = Algebraic.Cutwidth.Extractor.affineRoundTranscriptRightEnvelope h t L e (s.rightEnvelope e ν i) (s.iterate e i).left (s.iterate e i).leftRows