Exact source-envelope accounting for one affine round #
Original left and right source coordinates retain joint mass envelopes
through every actual observation. If S is the cardinality of all honest
and tampered short messages, the complete left total is multiplied by
S^2, and the complete right total by S^4. Opposite-side observations
preserve envelope totals exactly. Null conditional rows are included.
These finite bounds implement the transcript entropy accounting in Chattopadhyay--Liao, Theorem 6.1, printed pp.23--25: https://arxiv.org/abs/2110.12652. They neither supply nor assume a statistical security guarantee for the round's extractor calls.
theorem
Algebraic.Cutwidth.Extractor.affineRoundPrefixMask_left_envelope
(h t L : ℕ)
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(x : Z → A → X)
(μ : Z → ℝ)
(hr : ∀ (z : Z) (b : B), 0 ≤ r z b)
(cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(z : AffineRoundPrefixMaskTranscript Z t L)
(x₀ : X)
:
affineRoundPrefixMaskWeight h t L w r wr z * mapWeight (x z.1) (l z.1) x₀ ≤ affineRoundPrefixMaskLeftEnvelope h t L μ r wr z
The first right observation scales the original-left envelope by its message probability.
theorem
Algebraic.Cutwidth.Extractor.affineRoundPrefixMask_right_envelope
(h t L : ℕ)
{Z : Type u_1}
{B : Type u_2}
{Y : Type u_3}
[Fintype B]
(w : Z → ℝ)
(r : Z → B → ℝ)
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(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 : AffineRoundPrefixMaskTranscript Z t L)
(y₀ : Y)
:
affineRoundPrefixMaskWeight h t L w r wr z * mapWeight (y z.1) (affineRoundPrefixMaskRight h t L r wr z) y₀ ≤ ξ z.1
The original-right source is bounded by the copied envelope after its prefix masks are observed.
theorem
Algebraic.Cutwidth.Extractor.affineRoundPrefix_left_envelope
(h t L : ℕ)
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(x : Z → A → X)
(μ : Z → ℝ)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(z : AffineRoundPrefixTranscript Z t L)
(x₀ : X)
:
affineRoundPrefixWeight h t L w l r wl wr z * mapWeight (x z.1.1) (affineRoundPrefixLeft h t L l wl z) x₀ ≤ affineRoundPrefixLeftEnvelope h t L μ r wr z
Actual prefixes copy the original-left envelope over their message alphabet.
theorem
Algebraic.Cutwidth.Extractor.affineRoundPrefix_right_envelope
(h t L : ℕ)
{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 → ℝ)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(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 : AffineRoundPrefixTranscript Z t L)
(y₀ : Y)
:
affineRoundPrefixWeight h t L w l r wl wr z * mapWeight (y z.1.1) (affineRoundPrefixRight h t L r wr z) y₀ ≤ affineRoundPrefixRightEnvelope h t L ξ l wl z
The opposite-side prefix observation preserves the weighted original-right bound.
theorem
Algebraic.Cutwidth.Extractor.affineRoundMiddleRight_left_envelope
(d h t L e : ℕ)
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(ys : Z → B → AffinePhaseOneCopies t d)
(x : Z → A → X)
(μ : Z → ℝ)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(z : AffineRoundMiddleRightTranscript Z t L)
(x₀ : X)
:
affineRoundMiddleRightWeight d h t L e w l r wl wr ys z * mapWeight (x z.1.1.1) (affineRoundPrefixLeft h t L l wl z.1) x₀ ≤ affineRoundMiddleRightLeftEnvelope d h t L e μ r wr ys z
First right seeds and short-row masks preserve the original-left source bound.
theorem
Algebraic.Cutwidth.Extractor.affineRoundMiddleRight_right_envelope
(d h t 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 → ℝ)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(ys : Z → B → AffinePhaseOneCopies t d)
(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 : AffineRoundMiddleRightTranscript Z t L)
(y₀ : Y)
:
affineRoundMiddleRightWeight d h t L e w l r wl wr ys z * mapWeight (y z.1.1.1) (affineRoundMiddleRightKernel d h t L e r wr ys z) y₀ ≤ affineRoundMiddleRightRightEnvelope h t L ξ l wl z
The paired middle-right observation copies the original-right source envelope.
theorem
Algebraic.Cutwidth.Extractor.affineRoundMiddle_left_envelope
(d h t L e : ℕ)
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(ys : Z → B → AffinePhaseOneCopies t d)
(x : Z → A → X)
(μ : Z → ℝ)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(z : AffineRoundMiddleTranscript Z t L)
(x₀ : X)
:
affineRoundMiddleWeight d h t L e w l r wl wr ys z * mapWeight (x z.1.1.1.1) (affineRoundMiddleLeft h t L e l wl z) x₀ ≤ affineRoundMiddleLeftEnvelope d h t L e μ r wr ys z
Actual short rows copy the original-left source envelope a second time.
theorem
Algebraic.Cutwidth.Extractor.affineRoundMiddle_right_envelope
(d h t 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 → ℝ)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(ys : Z → B → AffinePhaseOneCopies t d)
(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 : AffineRoundMiddleTranscript Z t L)
(y₀ : Y)
:
affineRoundMiddleWeight d h t L e w l r wl wr ys z * mapWeight (y z.1.1.1.1) (affineRoundMiddleRightKernel d h t L e r wr ys z.1) y₀ ≤ affineRoundMiddleRightEnvelope h t L e ξ l wl z
The short-row observation preserves the weighted original-right bound.
theorem
Algebraic.Cutwidth.Extractor.affineRoundTranscript_left_envelope
(d h t L e : ℕ)
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(ys : Z → B → AffinePhaseOneCopies t d)
(x : Z → A → X)
(μ : Z → ℝ)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(z : AffineRoundTranscript Z t L)
(x₀ : X)
:
affineRoundTranscriptWeight d h t L e w l r wl wr ys z * mapWeight (x z.1.1.1.1.1) (affineRoundTranscriptLeft h t L e l wl z) x₀ ≤ affineRoundTranscriptLeftEnvelope d h t L e μ r wr ys z
The full actual transcript bounds the unchanged original-left source coordinates.
theorem
Algebraic.Cutwidth.Extractor.affineRoundTranscript_right_envelope
(d h t 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 → ℝ)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(ys : Z → B → AffinePhaseOneCopies t d)
(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 : AffineRoundTranscript Z t L)
(y₀ : Y)
:
affineRoundTranscriptWeight d h t L e w l r wl wr ys z * mapWeight (y z.1.1.1.1.1) (affineRoundTranscriptRight d h t L e r wr ys z) y₀ ≤ affineRoundTranscriptRightEnvelope h t L e ξ l wl z
The full actual transcript bounds the unchanged original-right source coordinates.
theorem
Algebraic.Cutwidth.Extractor.affineRoundPrefixMaskLeftEnvelope_sum
(h t L : ℕ)
{Z : Type u_1}
{B : Type u_2}
[Fintype Z]
[Fintype B]
(μ : Z → ℝ)
(r : Z → B → ℝ)
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(hr : ∀ (z : Z), ∑ b : B, r z b = 1)
:
∑ z : Z × AffineRoundShortMessages t L, affineRoundPrefixMaskLeftEnvelope h t L μ r wr z = ∑ z : Z, μ z
The first right observation preserves the original-left envelope total exactly.
theorem
Algebraic.Cutwidth.Extractor.affineRoundPrefixLeftEnvelope_sum
(h t L : ℕ)
{Z : Type u_1}
{B : Type u_2}
[Fintype Z]
[Fintype B]
(μ : Z → ℝ)
(r : Z → B → ℝ)
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(hr : ∀ (z : Z), ∑ b : B, r z b = 1)
:
∑ z : AffineRoundPrefixTranscript Z t L, affineRoundPrefixLeftEnvelope h t L μ r wr z = ↑(Fintype.card (AffineRoundShortMessages t L)) * ∑ z : Z, μ z
The actual prefix family charges one short-message alphabet to the left total.
theorem
Algebraic.Cutwidth.Extractor.affineRoundPrefixRightEnvelope_sum
(h t L : ℕ)
{Z : Type u_1}
{A : Type u_2}
[Fintype Z]
[Fintype A]
(ξ : Z → ℝ)
(l : Z → A → ℝ)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(hl : ∀ (z : Z), ∑ a : A, l z a = 1)
:
∑ z : AffineRoundPrefixMaskTranscript Z t L × AffineRoundShortMessages t L,
affineRoundPrefixRightEnvelope h t L ξ l wl z = ↑(Fintype.card (AffineRoundShortMessages t L)) * ∑ z : Z, ξ z
Through the prefix stage, the right total pays only for its prefix-mask family.
theorem
Algebraic.Cutwidth.Extractor.affineRoundMiddleRightLeftEnvelope_sum
(d h t L e : ℕ)
{Z : Type u_1}
{B : Type u_2}
[Fintype Z]
[Fintype B]
(μ : Z → ℝ)
(r : Z → B → ℝ)
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(ys : Z → B → AffinePhaseOneCopies t d)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
∑ z : AffineRoundPrefixTranscript Z t L × AffineRoundShortMessages t L × AffineRoundShortMessages t L,
affineRoundMiddleRightLeftEnvelope d h t L e μ r wr ys z = ↑(Fintype.card (AffineRoundShortMessages t L)) * ∑ z : Z, μ z
The paired right message preserves the preceding original-left envelope total.
theorem
Algebraic.Cutwidth.Extractor.affineRoundMiddleRightRightEnvelope_sum
(h t L : ℕ)
{Z : Type u_1}
{A : Type u_2}
[Fintype Z]
[Fintype A]
(ξ : Z → ℝ)
(l : Z → A → ℝ)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(hl : ∀ (z : Z), ∑ a : A, l z a = 1)
:
∑ z : AffineRoundMiddleRightTranscript Z t L, affineRoundMiddleRightRightEnvelope h t L ξ l wl z = ↑(Fintype.card (AffineRoundShortMessages t L)) ^ 3 * ∑ z : Z, ξ z
The paired right message gives a cubic short-message factor in the right total.
theorem
Algebraic.Cutwidth.Extractor.affineRoundMiddleLeftEnvelope_sum
(d h t L e : ℕ)
{Z : Type u_1}
{B : Type u_2}
[Fintype Z]
[Fintype B]
(μ : Z → ℝ)
(r : Z → B → ℝ)
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(ys : Z → B → AffinePhaseOneCopies t d)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
∑ z : AffineRoundMiddleTranscript Z t L, affineRoundMiddleLeftEnvelope d h t L e μ r wr ys z = ↑(Fintype.card (AffineRoundShortMessages t L)) ^ 2 * ∑ z : Z, μ z
Through the actual short rows, the original-left total pays two short-message families.
theorem
Algebraic.Cutwidth.Extractor.affineRoundMiddleRightEnvelope_sum
(h t L e : ℕ)
{Z : Type u_1}
{A : Type u_2}
[Fintype Z]
[Fintype A]
(ξ : Z → ℝ)
(l : Z → A → ℝ)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
:
∑ z : AffineRoundMiddleRightTranscript Z t L × AffineRoundShortMessages t L,
affineRoundMiddleRightEnvelope h t L e ξ l wl z = ↑(Fintype.card (AffineRoundShortMessages t L)) ^ 3 * ∑ z : Z, ξ z
Actual short rows preserve the cubic original-right envelope total.
theorem
Algebraic.Cutwidth.Extractor.affineRoundTranscriptLeftEnvelope_sum
(d h t L e : ℕ)
{Z : Type u_1}
{B : Type u_2}
[Fintype Z]
[Fintype B]
(μ : Z → ℝ)
(r : Z → B → ℝ)
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(ys : Z → B → AffinePhaseOneCopies t d)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
∑ z : AffineRoundMiddleTranscript Z t L × AffineRoundShortMessages t L,
affineRoundTranscriptLeftEnvelope d h t L e μ r wr ys z = ↑(Fintype.card (AffineRoundShortMessages t L)) ^ 2 * ∑ z : Z, μ z
The complete round multiplies the original-left envelope total by the square alphabet size.
theorem
Algebraic.Cutwidth.Extractor.affineRoundTranscriptRightEnvelope_sum
(h t L e : ℕ)
{Z : Type u_1}
{A : Type u_2}
[Fintype Z]
[Fintype A]
(ξ : Z → ℝ)
(l : Z → A → ℝ)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
:
∑ z : AffineRoundTranscript Z t L, affineRoundTranscriptRightEnvelope h t L e ξ l wl z = ↑(Fintype.card (AffineRoundShortMessages t L)) ^ 4 * ∑ z : Z, ξ z
The complete round multiplies the original-right envelope total by the fourth power alphabet size.
theorem
Algebraic.Cutwidth.Extractor.affineRoundPrefixLeftEnvelope_nonnegative
(h t L : ℕ)
{Z : Type u_1}
{B : Type u_2}
[Fintype B]
(μ : Z → ℝ)
(r : Z → B → ℝ)
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(nonnegative : ∀ (z : Z), 0 ≤ μ z)
(hr : ∀ (z : Z) (b : B), 0 ≤ r z b)
(z : AffineRoundPrefixTranscript Z t L)
:
Nonnegative original-left envelopes remain nonnegative after the prefix stage.
theorem
Algebraic.Cutwidth.Extractor.affineRoundPrefixRightEnvelope_nonnegative
(h t L : ℕ)
{Z : Type u_1}
{A : Type u_2}
[Fintype A]
(ξ : Z → ℝ)
(l : Z → A → ℝ)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(nonnegative : ∀ (z : Z), 0 ≤ ξ z)
(hl : ∀ (z : Z) (a : A), 0 ≤ l z a)
(z : AffineRoundPrefixTranscript Z t L)
:
Nonnegative original-right envelopes remain nonnegative after the prefix stage.
theorem
Algebraic.Cutwidth.Extractor.affineRoundMiddleRightLeftEnvelope_nonnegative
(d h t L e : ℕ)
{Z : Type u_1}
{B : Type u_2}
[Fintype B]
(μ : Z → ℝ)
(r : Z → B → ℝ)
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(ys : Z → B → AffinePhaseOneCopies t d)
(nonnegative : ∀ (z : Z), 0 ≤ μ z)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(z : AffineRoundMiddleRightTranscript Z t L)
:
The middle-right update preserves the original-left envelope sign, including null rows.
theorem
Algebraic.Cutwidth.Extractor.affineRoundMiddleRightRightEnvelope_nonnegative
(h t L : ℕ)
{Z : Type u_1}
{A : Type u_2}
[Fintype A]
(ξ : Z → ℝ)
(l : Z → A → ℝ)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(nonnegative : ∀ (z : Z), 0 ≤ ξ z)
(hl : ∀ (z : Z) (a : A), 0 ≤ l z a)
(z : AffineRoundMiddleRightTranscript Z t L)
:
The copied middle-right original-right envelope is nonnegative.
theorem
Algebraic.Cutwidth.Extractor.affineRoundMiddleLeftEnvelope_nonnegative
(d h t L e : ℕ)
{Z : Type u_1}
{B : Type u_2}
[Fintype B]
(μ : Z → ℝ)
(r : Z → B → ℝ)
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(ys : Z → B → AffinePhaseOneCopies t d)
(nonnegative : ∀ (z : Z), 0 ≤ μ z)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(z : AffineRoundMiddleTranscript Z t L)
:
The original-left envelope remains nonnegative after the actual short outputs.
theorem
Algebraic.Cutwidth.Extractor.affineRoundMiddleRightEnvelope_nonnegative
(h t L e : ℕ)
{Z : Type u_1}
{A : Type u_2}
[Fintype A]
(ξ : Z → ℝ)
(l : Z → A → ℝ)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(nonnegative : ∀ (z : Z), 0 ≤ ξ z)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(z : AffineRoundMiddleTranscript Z t L)
:
The original-right envelope remains nonnegative after the actual short outputs.
theorem
Algebraic.Cutwidth.Extractor.affineRoundTranscriptLeftEnvelope_nonnegative
(d h t L e : ℕ)
{Z : Type u_1}
{B : Type u_2}
[Fintype B]
(μ : Z → ℝ)
(r : Z → B → ℝ)
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(ys : Z → B → AffinePhaseOneCopies t d)
(nonnegative : ∀ (z : Z), 0 ≤ μ z)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(z : AffineRoundTranscript Z t L)
:
The full original-left envelope is nonnegative at every transcript.
theorem
Algebraic.Cutwidth.Extractor.affineRoundTranscriptRightEnvelope_nonnegative
(h t L e : ℕ)
{Z : Type u_1}
{A : Type u_2}
[Fintype A]
(ξ : Z → ℝ)
(l : Z → A → ℝ)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(nonnegative : ∀ (z : Z), 0 ≤ ξ z)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(z : AffineRoundTranscript Z t L)
:
The full original-right envelope is nonnegative at every transcript.
The honest and tampered short-message family has the exact Boolean cardinality.