Actual first phase of the standard-to-affine conversion

Every execution reads a prefix of its right input, extracts from the same masked left input, uses the actual advice correlation breaker, and extracts again. none indexes the honest execution and some i indexes a tampering. Prefixes use false completion, so the program is total without size guards.

The transcript first observes all seed prefixes and mask contributions on the right, then all first extraction outputs on the left, then all advice outputs on the right. Its factors use the existing normalized conditional kernels, including null rows, and retain both original latent variables.

This is the three-stage first phase of Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), Theorem 6.1, printed p.23, with this library's actual matched extractors and advice construction: https://arxiv.org/abs/2110.12652. These definitions impose no statistical guarantee or validity condition on those component programs.

@[reducible, inline]

abbrev Algebraic.Cutwidth.Extractor.AffinePhaseOneCopies (t width : ℕ) : Type

A family containing the honest word and all t tampered words.

Equations

• Algebraic.Cutwidth.Extractor.AffinePhaseOneCopies t width = (Option (Fin t) → Fin width → Bool)

def Algebraic.Cutwidth.Extractor.affinePhaseOneFirstSeed (d L₀ : ℕ) (y : Fin d → Bool) : Fin (matchedBlockSeedBits L₀) → Bool

The initial seed prefix, completed by false bits when necessary.

Equations

• Algebraic.Cutwidth.Extractor.affinePhaseOneFirstSeed d L₀ y i = (List.ofFn y)[↑i]?.getD false

def Algebraic.Cutwidth.Extractor.affinePhaseOneFirstOutput (n d L₀ e₀ : ℕ) (x : Fin n → Bool) (y : Fin d → Bool) : Fin (matchedBlockOutputBits 64 L₀) → Bool

The actual first linear extraction, with output depth sixty-four.

Equations

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

def Algebraic.Cutwidth.Extractor.affinePhaseOneSecondSeed (n d L₀ e₀ L₁ e₁ : ℕ) (x : Fin n → Bool) (y : Fin d → Bool) (advice : List Bool) : Fin (matchedBlockSeedBits L₁) → Bool

The actual advice construction supplies the seed for the final extraction.

Equations

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

def Algebraic.Cutwidth.Extractor.affinePhaseOneOutput (n d h L₀ e₀ L₁ e₁ er : ℕ) (x : Fin n → Bool) (y : Fin d → Bool) (advice : List Bool) : Fin (matchedBlockOutputBits h L₁) → Bool

The actual output of the three-stage first phase.

Equations

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

@[reducible, inline]

abbrev Algebraic.Cutwidth.Extractor.AffinePhaseOneRightMessage (t L₀ : ℕ) : Type

The first right message fixes all prefixes and first mask contributions.

Equations

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

@[reducible, inline]

abbrev Algebraic.Cutwidth.Extractor.AffinePhaseOneRightTranscript (Z : Type u_1) (t L₀ : ℕ) : Type u_1

The original tag and the first right message.

Equations

• Algebraic.Cutwidth.Extractor.AffinePhaseOneRightTranscript Z t L₀ = (Z × Algebraic.Cutwidth.Extractor.AffinePhaseOneRightMessage t L₀)

@[reducible, inline]

abbrev Algebraic.Cutwidth.Extractor.AffinePhaseOneLeftTranscript (Z : Type u_1) (t L₀ : ℕ) : Type u_1

The right transcript followed by all actual first extraction outputs.

Equations

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

@[reducible, inline]

abbrev Algebraic.Cutwidth.Extractor.AffinePhaseOneTranscript (Z : Type u_1) (t L₀ L₁ : ℕ) : Type u_1

The complete first-phase transcript, ending with all advice outputs.

Equations

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

def Algebraic.Cutwidth.Extractor.affinePhaseOneRightMessage {Z : Type u_1} {B : Type u_3} (n d t L₀ e₀ : ℕ) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (z : Z) (b : B) : AffinePhaseOneRightMessage t L₀

The first observation depends only on the original right state.

Equations

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

def Algebraic.Cutwidth.Extractor.affinePhaseOneFirstLeft {Z : Type u_1} {A : Type u_2} (n t L₀ e₀ : ℕ) (x : Z → A → Fin n → Bool) (z : AffinePhaseOneRightTranscript Z t L₀) (a : A) : AffinePhaseOneCopies t (matchedBlockOutputBits 64 L₀)

Once the right message is fixed, every actual first output is left-only.

Equations

• Algebraic.Cutwidth.Extractor.affinePhaseOneFirstLeft n t L₀ e₀ x z a i j = (Algebraic.Cutwidth.Extractor.matchedBlockExtractor n 64 L₀ e₀ (x z.1 a) (z.2.1 i) j ^^ z.2.2 i j)

def Algebraic.Cutwidth.Extractor.affinePhaseOneSecondRight {Z : Type u_1} {B : Type u_3} (d t L₀ L₁ e₁ : ℕ) (ys : Z → B → AffinePhaseOneCopies t d) (advice : Option (Fin t) → List Bool) (z : AffinePhaseOneLeftTranscript Z t L₀) (b : B) : AffinePhaseOneCopies t (matchedBlockSeedBits L₁)

Once the first outputs are fixed, every actual advice output is right-only.

Equations

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

def Algebraic.Cutwidth.Extractor.affinePhaseOneRightTranscript {Z : Type u_1} {B : Type u_3} (n d t L₀ e₀ : ℕ) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (p : Z × B) : AffinePhaseOneRightTranscript Z t L₀

The actual first right transcript retains the original tag.

Equations

• Algebraic.Cutwidth.Extractor.affinePhaseOneRightTranscript n d t L₀ e₀ mask ys p = (p.1, Algebraic.Cutwidth.Extractor.affinePhaseOneRightMessage n d t L₀ e₀ mask ys p.1 p.2)

def Algebraic.Cutwidth.Extractor.affinePhaseOneLeftTranscript {Z : Type u_1} {A : Type u_2} {B : Type u_3} (n d t L₀ e₀ : ℕ) (x : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (p : (Z × B) × A) : AffinePhaseOneLeftTranscript Z t L₀

The actual first extraction outputs extend the first right transcript.

Equations

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

def Algebraic.Cutwidth.Extractor.affinePhaseOneTranscript {Z : Type u_1} {A : Type u_2} {B : Type u_3} (n d t L₀ e₀ L₁ e₁ : ℕ) (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) : AffinePhaseOneTranscript Z t L₀ L₁

The actual advice outputs complete the first-phase transcript.

Equations

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

def Algebraic.Cutwidth.Extractor.affinePhaseOneOutputLeft {Z : Type u_1} {A : Type u_2} (n t h L₀ L₁ er : ℕ) (x : Z → A → Fin n → Bool) (z : AffinePhaseOneTranscript Z t L₀ L₁) (a : A) : AffinePhaseOneCopies t (matchedBlockOutputBits h L₁)

The final extraction's original-left contribution after fixing the transcript.

Equations

• Algebraic.Cutwidth.Extractor.affinePhaseOneOutputLeft n t h L₀ L₁ er x z a i = Algebraic.Cutwidth.Extractor.matchedBlockExtractor n h L₁ er (x z.1.1.1 a) (z.2 i)

def Algebraic.Cutwidth.Extractor.affinePhaseOneOutputRight {Z : Type u_1} {B : Type u_3} (n t h L₀ L₁ er : ℕ) (mask : Z → B → Fin n → Bool) (z : AffinePhaseOneTranscript Z t L₀ L₁) (b : B) : AffinePhaseOneCopies t (matchedBlockOutputBits h L₁)

The final extraction's original-right mask contribution after fixing the transcript.

Equations

• Algebraic.Cutwidth.Extractor.affinePhaseOneOutputRight n t h L₀ L₁ er mask z b i = Algebraic.Cutwidth.Extractor.matchedBlockExtractor n h L₁ er (mask z.1.1.1 b) (z.2 i)

noncomputable def Algebraic.Cutwidth.Extractor.affinePhaseOneRightWeight {Z : Type u_1} {B : Type u_3} (n d t L₀ e₀ : ℕ) [Fintype B] (w : Z → ℝ) (r : Z → B → ℝ) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) : AffinePhaseOneRightTranscript Z t L₀ → ℝ

Transcript weight after the first right observation.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.affinePhaseOneRightKernel {Z : Type u_1} {B : Type u_3} (n d t L₀ e₀ : ℕ) [Fintype B] (r : Z → B → ℝ) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) : AffinePhaseOneRightTranscript Z t L₀ → B → ℝ

Original right states conditioned on their first observation.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.affinePhaseOneLeftWeight {Z : Type u_1} {A : Type u_2} {B : Type u_3} (n d t L₀ e₀ : ℕ) [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) : AffinePhaseOneLeftTranscript Z t L₀ → ℝ

Transcript weight after additionally observing all first extraction outputs.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.affinePhaseOneLeftKernel {Z : Type u_1} {A : Type u_2} (n t L₀ e₀ : ℕ) [Fintype A] (l : Z → A → ℝ) (x : Z → A → Fin n → Bool) : AffinePhaseOneLeftTranscript Z t L₀ → A → ℝ

Original left states conditioned on the actual first extraction outputs.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.affinePhaseOneTranscriptWeight {Z : Type u_1} {A : Type u_2} {B : Type u_3} (n d t L₀ e₀ L₁ e₁ : ℕ) [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) : AffinePhaseOneTranscript Z t L₀ L₁ → ℝ

The complete transcript weight, conditioning only the original side variables.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.affinePhaseOneTranscriptLeft {Z : Type u_1} {A : Type u_2} (n t L₀ e₀ L₁ : ℕ) [Fintype A] (l : Z → A → ℝ) (x : Z → A → Fin n → Bool) (z : AffinePhaseOneTranscript Z t L₀ L₁) : A → ℝ

The original left kernel after all three observations.

Equations

• Algebraic.Cutwidth.Extractor.affinePhaseOneTranscriptLeft n t L₀ e₀ L₁ l x z = Algebraic.Cutwidth.Extractor.affinePhaseOneLeftKernel n t L₀ e₀ l x z.1

noncomputable def Algebraic.Cutwidth.Extractor.affinePhaseOneTranscriptRight {Z : Type u_1} {B : Type u_3} (n d t L₀ e₀ L₁ e₁ : ℕ) [Fintype B] (r : Z → B → ℝ) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (advice : Option (Fin t) → List Bool) : AffinePhaseOneTranscript Z t L₀ L₁ → B → ℝ

The original right kernel after all three observations.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.affinePhaseOneRightLeftEnvelope {Z : Type u_1} {B : Type u_3} (n d t L₀ e₀ : ℕ) [Fintype B] (μ : Z → ℝ) (r : Z → B → ℝ) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) : AffinePhaseOneRightTranscript Z t L₀ → ℝ

A left-source envelope after the first right observation.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.affinePhaseOneLeftEnvelope {Z : Type u_1} {B : Type u_3} (n d t L₀ e₀ : ℕ) [Fintype B] (μ : Z → ℝ) (r : Z → B → ℝ) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (z : AffinePhaseOneLeftTranscript Z t L₀) : ℝ

A left-source envelope after the right and left observations.

Equations

• Algebraic.Cutwidth.Extractor.affinePhaseOneLeftEnvelope n d t L₀ e₀ μ r mask ys z = Algebraic.Cutwidth.Extractor.affinePhaseOneRightLeftEnvelope n d t L₀ e₀ μ r mask ys z.1

noncomputable def Algebraic.Cutwidth.Extractor.affinePhaseOneRightEnvelope {Z : Type u_1} {A : Type u_2} (n t L₀ e₀ : ℕ) [Fintype A] (ξ : Z → ℝ) (l : Z → A → ℝ) (x : Z → A → Fin n → Bool) : AffinePhaseOneLeftTranscript Z t L₀ → ℝ

A right-source envelope after the right and left observations.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.affinePhaseOneTranscriptLeftEnvelope {Z : Type u_1} {B : Type u_3} (n d t L₀ e₀ L₁ e₁ : ℕ) [Fintype B] (μ : Z → ℝ) (r : Z → B → ℝ) (mask : Z → B → Fin n → Bool) (ys : Z → B → AffinePhaseOneCopies t d) (advice : Option (Fin t) → List Bool) : AffinePhaseOneTranscript Z t L₀ L₁ → ℝ

The final left-source envelope keeps the probabilities of both right observations.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.affinePhaseOneTranscriptRightEnvelope {Z : Type u_1} {A : Type u_2} (n t L₀ e₀ L₁ : ℕ) [Fintype A] (ξ : Z → ℝ) (l : Z → A → ℝ) (x : Z → A → Fin n → Bool) (z : AffinePhaseOneTranscript Z t L₀ L₁) : ℝ

The final right-source envelope copies the previous envelope to every advice output.

Equations

• Algebraic.Cutwidth.Extractor.affinePhaseOneTranscriptRightEnvelope n t L₀ e₀ L₁ ξ l x z = Algebraic.Cutwidth.Extractor.affinePhaseOneRightEnvelope n t L₀ e₀ ξ l x z.1