Exact factors for the complete advice-bit transcript

For arbitrary advice bits, the actual pair of eight-call executions admits normalized conditional kernels for the original sources. Both final outputs are right-only maps of these kernels. The original source envelopes have exact total growth D^8 on the left and C^4 on the right, where D is the short-output cardinality and C the refresh-state cardinality.

This common transcript leaves the final tampered output unobserved. The opposite-bit identity connects observing that output to the transcript used by the checked opposite-advice guarantees. These are the factorization and entropy bookkeeping for the induction in Chattopadhyay--Goyal--Li Lemma 6.9: https://arxiv.org/pdf/1505.00107. The complete advice induction remains a separate theorem.

theorem Algebraic.Cutwidth.Extractor.flipFlopFirstLeft_probability (n L e : ℕ) {Z : Type u_1} {A : Type u_2} [Fintype A] (l : Z → A → ℝ) (x x' : Z → A → Fin n → Bool) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (t : FlipFlopFirstTranscript Z L) : IsProbabilityWeight (flipFlopFirstLeft n L e l x x' t)

The original left kernel is normalized after the first history.

theorem Algebraic.Cutwidth.Extractor.flipFlopFirstRight_probability (L : ℕ) {Z : Type u_1} {B : Type u_2} [Fintype B] (r : Z → B → ℝ) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (t : FlipFlopFirstTranscript Z L) : IsProbabilityWeight (flipFlopFirstRight L r q q' t)

The original right kernel is normalized after the first input pair.

theorem Algebraic.Cutwidth.Extractor.flipFlopFirst_probability (n 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 x' : Z → A → Fin n → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (flipFlopFirstWeight n L e w l r x x' q q') ∧ (∀ (t : FlipFlopFirstTranscript Z L), IsProbabilityWeight (flipFlopFirstLeft n L e l x x' t)) ∧ ∀ (t : FlipFlopFirstTranscript Z L), IsProbabilityWeight (flipFlopFirstRight L r q q' t)

The first actual transcript and both conditional kernels are normalized.

theorem Algebraic.Cutwidth.Extractor.flipFlopTranscript_probability (n m 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 x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b b' : Bool) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (flipFlopTranscriptWeight n m L e w l r x x' y y' q q' b b') ∧ (∀ (t : FlipFlopTranscript Z L), IsProbabilityWeight (flipFlopTranscriptLeft n L e l x x' t)) ∧ ∀ (t : FlipFlopTranscript Z L), IsProbabilityWeight (flipFlopTranscriptRight m L e r y y' q q' b b' t)

The complete actual transcript and both original-source kernels are normalized.

theorem Algebraic.Cutwidth.Extractor.flipFlopTranscript_factored (n m 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 x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b b' : Bool) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : mapWeight (fun (p : (Z × B) × A) => ((flipFlopTranscript n m L e x x' y y' q q' b b' p, p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (flipFlopTranscriptWeight n m L e w l r x x' y y' q q' b b') (flipFlopTranscriptLeft n L e l x x') (flipFlopTranscriptRight m L e r y y' q q' b b')

The actual two-pass transcript factors the original sources exactly.

theorem Algebraic.Cutwidth.Extractor.flipFlopHonestOutput_eq_step (n m L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} (x x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b b' : Bool) (p : (Z × B) × A) : flipFlopHonestOutput m L e y b (flipFlopTranscript n m L e x x' y y' q q' b b' p) p.1.2 = flipFlopStep n m L e (x p.1.1 p.2) (y p.1.1 p.1.2) (q p.1.1 p.1.2) b

The honest right-only output map recovers the actual advice-bit program.

theorem Algebraic.Cutwidth.Extractor.flipFlopTamperedOutput_eq_step (n m L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} (x x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b b' : Bool) (p : (Z × B) × A) : flipFlopTamperedOutput m L e y' b' (flipFlopTranscript n m L e x x' y y' q q' b b' p) p.1.2 = flipFlopStep n m L e (x' p.1.1 p.2) (y' p.1.1 p.1.2) (q' p.1.1 p.1.2) b'

The tampered right-only output map recovers its actual advice-bit program.

theorem Algebraic.Cutwidth.Extractor.flipFlopTranscript_opposite (n m L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} (x x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b : Bool) (p : (Z × B) × A) : (flipFlopTranscript n m L e x x' y y' q q' b (!b) p, flipFlopTamperedOutput m L e y' (!b) (flipFlopTranscript n m L e x x' y y' q q' b (!b) p) p.1.2) = flipFlopOppositeTranscript n m L e x x' y y' q q' b p

Observing the tampered output for opposite bits gives the opposite-advice transcript.

theorem Algebraic.Cutwidth.Extractor.flipFlopTranscriptLeftEnvelope_nonnegative (m L e : ℕ) {Z : Type u_1} {B : Type u_2} [Fintype B] (μ : Z → ℝ) (r : Z → B → ℝ) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b b' : Bool) (nonnegative : ∀ (z : Z), 0 ≤ μ z) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (t : FlipFlopTranscript Z L) : 0 ≤ flipFlopTranscriptLeftEnvelope m L e μ r y y' q q' b b' t

The updated original left-source envelope is nonnegative.

theorem Algebraic.Cutwidth.Extractor.flipFlopTranscriptRightEnvelope_nonnegative (n L e : ℕ) {Z : Type u_1} {A : Type u_2} [Fintype A] (ν : Z → ℝ) (l : Z → A → ℝ) (x x' : Z → A → Fin n → Bool) (nonnegative : ∀ (z : Z), 0 ≤ ν z) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (t : FlipFlopTranscript Z L) : 0 ≤ flipFlopTranscriptRightEnvelope n L e ν l x x' t

The updated original right-source envelope is nonnegative.

theorem Algebraic.Cutwidth.Extractor.flipFlopTranscript_left_envelope (n m 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 x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b b' : 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) (t : FlipFlopTranscript Z L) (x₀ : Fin n → Bool) : flipFlopTranscriptWeight n m L e w l r x x' y y' q q' b b' t * mapWeight (x t.1.1.1.1) (flipFlopTranscriptLeft n L e l x x' t) x₀ ≤ flipFlopTranscriptLeftEnvelope m L e μ r y y' q q' b b' t

The complete actual transcript preserves an explicit original left-source envelope.

theorem Algebraic.Cutwidth.Extractor.flipFlopTranscript_right_envelope (n m 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 x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b b' : Bool) (ν : Z → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (cap : ∀ (z : Z) (y₀ : Fin m → Bool), w z * mapWeight (y z) (r z) y₀ ≤ ν z) (t : FlipFlopTranscript Z L) (y₀ : Fin m → Bool) : flipFlopTranscriptWeight n m L e w l r x x' y y' q q' b b' t * mapWeight (y t.1.1.1.1) (flipFlopTranscriptRight m L e r y y' q q' b b' t) y₀ ≤ flipFlopTranscriptRightEnvelope n L e ν l x x' t

The complete actual transcript preserves an explicit original right-source envelope.

theorem Algebraic.Cutwidth.Extractor.flipFlopTranscriptLeftEnvelope_sum (m L e : ℕ) {Z : Type u_1} {B : Type u_2} [Fintype Z] [Fintype B] (μ : Z → ℝ) (r : Z → B → ℝ) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b b' : Bool) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : ∑ t : FlipFlopTranscript Z L, flipFlopTranscriptLeftEnvelope m L e μ r y y' q q' b b' t = ↑(Fintype.card (Fin (matchedBlockSeedBits L) → Bool)) ^ 8 * ∑ z : Z, μ z

The left envelope pays for all eight short look-ahead messages.

theorem Algebraic.Cutwidth.Extractor.flipFlopTranscriptRightEnvelope_sum (n L e : ℕ) {Z : Type u_1} {A : Type u_2} [Fintype Z] [Fintype A] (ν : Z → ℝ) (l : Z → A → ℝ) (x x' : Z → A → Fin n → Bool) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) : ∑ t : FlipFlopTranscript Z L, flipFlopTranscriptRightEnvelope n L e ν l x x' t = ↑(Fintype.card (Fin (matchedBlockOutputBits 64 L) → Bool)) ^ 4 * ∑ z : Z, ν z

The right envelope pays for the two pairs of right states.