Actual affine rounds double the retained-subset capacity #
The invariant holds for all subsets up to a specified cardinality, including
empty subsets. Splitting a larger set and applying the actual four-call
round proves the same invariant at the new transcript with doubled capacity
and error 2ρ + 8 * 2⁻ᵉ. The finite entropy reserves are uniform in the set.
theorem
Algebraic.Cutwidth.Extractor.AffineRowInvariant.mono
(h t L : ℕ)
{Z : Type u_1}
{A : Type u_2}
[Fintype Z]
[Fintype A]
{w : Z → ℝ}
{l : Z → A → ℝ}
{wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)}
{k k' : ℕ}
{ρ ρ' : ℝ}
(invariant : AffineRowInvariant h t L w l wl k ρ)
(capacity : k' ≤ k)
(error : ρ ≤ ρ')
:
AffineRowInvariant h t L w l wl k' ρ'
Decrease the retained-subset capacity and increase the allowed discrepancy.
theorem
Algebraic.Cutwidth.Extractor.affineRound_doubles_invariant
(n d h t L e k kx ky : ℕ)
{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 : Z → A → Fin n → Bool)
(wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L))
(ys : Z → B → AffinePhaseOneCopies t d)
(μ ν : Z → ℝ)
{ρ : ℝ}
(size : matchedBlockSeedBits L ≤ matchedBlockOutputBits h L)
(right_length : Nat.clog 2 (d + 1) ≤ L)
(row_length : Nat.clog 2 (matchedBlockOutputBits h L + 1) ≤ L)
(room : 64 ≤ L)
(short_error : e + 24 + 2 ≤ L)
(final_length : Nat.clog 2 (n + 1) ≤ L)
(final_error : e + h + 2 ≤ L)
(final_budget : (h + 1) * (e + 2 * h + Nat.clog 2 (L + 1) + 4) ≤ L)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(left_nonnegative : ∀ (z : Z), 0 ≤ μ z)
(right_nonnegative : ∀ (z : Z), 0 ≤ ν z)
(left_cap : ∀ (z : Z) (x₀ : Fin n → Bool), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(right_cap : ∀ (z : Z) (y₀ : Fin d → Bool), w z * mapWeight (fun (b : B) => ys z b none) (r z) y₀ ≤ ν z)
(first : 2 ^ 62 * L + (t + t + 1) * matchedBlockSeedBits L + e ≤ ky)
(merge : 2 ^ 62 * L + (t + t + 1) * matchedBlockSeedBits L + e ≤ matchedBlockOutputBits h L)
(recover : 2 ^ 62 * L + (t + 3 * (t + 1)) * matchedBlockSeedBits L + e ≤ ky)
(final : 2 ^ (2 * h + 14) * L + t * matchedBlockOutputBits h L + 2 * (t + 1) * matchedBlockSeedBits L + e ≤ kx)
(left_mass : ∑ z : Z, μ z ≤ (2 ^ kx)⁻¹)
(right_mass : ∑ z : Z, ν z ≤ (2 ^ ky)⁻¹)
(old : AffineRowInvariant h t L w l wl k ρ)
:
AffineRowInvariant h t L (affineRoundTranscriptWeight d h t L e w l r wl wr ys) (affineRoundTranscriptLeft h t L e l wl)
(affineRoundOutputLeft n h t L e x) (2 * k) (2 * ρ + 8 * (2 ^ e)⁻¹)
One actual four-call round doubles capacity with its explicit dyadic error.