sgl_block_counting

import Definitions.Def_sgl_vote_bridge
import Definitions.Def_sgl_amplification_counting

/-!
# Counting for the block-sampled amplifier

The consecutive-chunk amplifier: the ternary vote over the block sample.
Its counting mirrors the flat-sampled version's — the transport equivalence
is the block equivalence, whose leaf order the cascade machine realises.
-/

namespace SipserGacsLautemann

/-- The consecutive-chunk amplified verifier: the chunk width is read off
the random string's length, so a machine can derive it. -/
def blockAmplifiedVerifier (verifier : List Bool → List Bool → Bool)
    (input random : List Bool) : Bool :=
  ternaryVoteConstruction
    (fun leaf : BitString
        (random.length / 3 ^ amplificationDepth input.length) =>
      verifier input leaf.toList)
    (amplificationDepth input.length)
    (blockTernaryEquiv
      (random.length / 3 ^ amplificationDepth input.length)
      (amplificationDepth input.length)
      (paddedBitStringConstruction
        ((random.length / 3 ^ amplificationDepth input.length) *
          3 ^ amplificationDepth input.length)
        random))

/-- On a full-length random string the derived width is the intended one. -/
theorem blockAmplifiedVerifier_width (randomBits : Nat → Nat)
    (input : List Bool)
    (flat : BitString (amplifiedRandomBitCount randomBits input.length)) :
    flat.toList.length / 3 ^ amplificationDepth input.length =
      randomBits input.length := by
  have hlen : flat.toList.length =
      randomBits input.length * 3 ^ amplificationDepth input.length := by
    simp [BitString.toList, amplifiedRandomBitCount]
  rw [hlen, Nat.mul_comm]
  exact Nat.mul_div_right _ (pow_pos (by decide) _)

theorem blockAmplifiedVerifier_vote (randomBits : Nat → Nat)
    (verifier : List Bool → List Bool → Bool)
    (input : List Bool)
    (flat : BitString (amplifiedRandomBitCount randomBits input.length)) :
    blockAmplifiedVerifier verifier input flat.toList =
      ternaryVoteConstruction
        (fun leaf : BitString (randomBits input.length) =>
          verifier input leaf.toList)
        (amplificationDepth input.length)
        (blockTernaryEquiv (randomBits input.length)
          (amplificationDepth input.length) flat) := by
  unfold blockAmplifiedVerifier
  have hcongr := congrArg
    (fun rb => ternaryVoteConstruction
      (fun leaf : BitString rb => verifier input leaf.toList)
      (amplificationDepth input.length)
      (blockTernaryEquiv rb (amplificationDepth input.length)
        (paddedBitStringConstruction
          (rb * 3 ^ amplificationDepth input.length) flat.toList)))
    (blockAmplifiedVerifier_width randomBits input flat)
  refine hcongr.trans ?_
  show ternaryVoteConstruction
      (fun leaf : BitString (randomBits input.length) =>
        verifier input leaf.toList)
      (amplificationDepth input.length)
      (blockTernaryEquiv (randomBits input.length)
        (amplificationDepth input.length)
        (paddedBitStringConstruction
          (randomBits input.length * 3 ^ amplificationDepth input.length)
          flat.toList)) = _
  rw [show paddedBitStringConstruction
      (randomBits input.length * 3 ^ amplificationDepth input.length)
      flat.toList = flat from paddedBitString_toList flat]

theorem blockAmplifiedVerifier_toList_eq_true_iff
    (randomBits : Nat → Nat)
    (verifier : List Bool → List Bool → Bool)
    (input : List Bool)
    (flat : BitString (amplifiedRandomBitCount randomBits input.length)) :
    blockAmplifiedVerifier verifier input flat.toList = true ↔
      ternaryBad
        (fun leaf : BitString (randomBits input.length) =>
          verifier input leaf.toList = true)
        (amplificationDepth input.length)
        (blockTernaryEquiv (randomBits input.length)
          (amplificationDepth input.length) flat) := by
  rw [blockAmplifiedVerifier_vote randomBits verifier input flat]
  exact ternaryVote_eq_true_iff _ _ _

theorem blockAmplifiedVerifier_toList_eq_false_iff
    (randomBits : Nat → Nat)
    (verifier : List Bool → List Bool → Bool)
    (input : List Bool)
    (flat : BitString (amplifiedRandomBitCount randomBits input.length)) :
    blockAmplifiedVerifier verifier input flat.toList = false ↔
      ternaryBad
        (fun leaf : BitString (randomBits input.length) =>
          verifier input leaf.toList = false)
        (amplificationDepth input.length)
        (blockTernaryEquiv (randomBits input.length)
          (amplificationDepth input.length) flat) := by
  rw [blockAmplifiedVerifier_vote randomBits verifier input flat]
  exact ternaryVote_eq_false_iff _ _ _

theorem acceptingCard_blockAmplifiedVerifier
    (randomBits : Nat → Nat)
    (verifier : List Bool → List Bool → Bool)
    (input : List Bool) :
    acceptingCard (blockAmplifiedVerifier verifier)
        input (amplifiedRandomBitCount randomBits input.length) =
      badCard
        (ternaryBad
          (fun leaf : BitString (randomBits input.length) =>
            verifier input leaf.toList = true)
          (amplificationDepth input.length)) := by
  classical
  change badCard
      (fun flat : BitString
          (amplifiedRandomBitCount randomBits input.length) =>
        blockAmplifiedVerifier verifier input flat.toList =
          true) = _
  calc
    badCard
        (fun flat : BitString
            (amplifiedRandomBitCount randomBits input.length) =>
          blockAmplifiedVerifier verifier input flat.toList =
            true)
        =
      badCard
        (fun flat =>
          ternaryBad
            (fun leaf : BitString (randomBits input.length) =>
              verifier input leaf.toList = true)
            (amplificationDepth input.length)
            (blockTernaryEquiv (randomBits input.length)
              (amplificationDepth input.length) flat)) :=
      badCard_congr fun flat =>
        blockAmplifiedVerifier_toList_eq_true_iff randomBits verifier
          input flat
    _ = _ :=
      badCard_comp_equiv
        (blockTernaryEquiv (randomBits input.length)
          (amplificationDepth input.length))
        (ternaryBad
          (fun leaf : BitString (randomBits input.length) =>
            verifier input leaf.toList = true)
          (amplificationDepth input.length))

theorem rejectingCard_blockAmplifiedVerifier
    (randomBits : Nat → Nat)
    (verifier : List Bool → List Bool → Bool)
    (input : List Bool) :
    rejectingCard (blockAmplifiedVerifier verifier)
        input (amplifiedRandomBitCount randomBits input.length) =
      badCard
        (ternaryBad
          (fun leaf : BitString (randomBits input.length) =>
            verifier input leaf.toList = false)
          (amplificationDepth input.length)) := by
  classical
  change badCard
      (fun flat : BitString
          (amplifiedRandomBitCount randomBits input.length) =>
        blockAmplifiedVerifier verifier input flat.toList =
          false) = _
  calc
    badCard
        (fun flat : BitString
            (amplifiedRandomBitCount randomBits input.length) =>
          blockAmplifiedVerifier verifier input flat.toList =
            false)
        =
      badCard
        (fun flat =>
          ternaryBad
            (fun leaf : BitString (randomBits input.length) =>
              verifier input leaf.toList = false)
            (amplificationDepth input.length)
            (blockTernaryEquiv (randomBits input.length)
              (amplificationDepth input.length) flat)) :=
      badCard_congr fun flat =>
        blockAmplifiedVerifier_toList_eq_false_iff randomBits verifier
          input flat
    _ = _ :=
      badCard_comp_equiv
        (blockTernaryEquiv (randomBits input.length)
          (amplificationDepth input.length))
        (ternaryBad
          (fun leaf : BitString (randomBits input.length) =>
            verifier input leaf.toList = false)
          (amplificationDepth input.length))

theorem blockTernary_card (randomBitCount depth : Nat) :
    Fintype.card (TernarySample (BitString randomBitCount) depth) =
      Fintype.card (BitString (randomBitCount * 3 ^ depth)) :=
  (Fintype.card_congr (blockTernaryEquiv randomBitCount depth)).symm

/-- **The node's conclusion, given a polynomial-time block amplifier.** -/
theorem bounded_error_verifier_amplification_of_dpt_block
    (language : Language)
    (randomBits : Nat → Nat)
    (verifier : List Bool → List Bool → Bool)
    (hrandomBits : PolynomiallyBounded randomBits)
    (hboundedError :
      ∀ input : List Bool,
        (input ∈ language →
          3 * acceptingCard verifier input (randomBits input.length) ≥
            2 * Fintype.card
              (BitString (randomBits input.length))) ∧
        (input ∉ language →
          3 * rejectingCard verifier input (randomBits input.length) ≥
            2 * Fintype.card
              (BitString (randomBits input.length))))
    (hamplifiedVerifier :
      DecidesInPolynomialTime
        (fun input : Fin 2 → List Bool =>
          blockAmplifiedVerifier verifier
            (input 0) (input 1) = true)) :
    ∃ (amplifiedRandomBits : Nat → Nat)
        (amplifiedVerifier : List Bool → List Bool → Bool),
      PolynomiallyBounded amplifiedRandomBits ∧
      DecidesInPolynomialTime
        (fun input : Fin 2 → List Bool =>
          amplifiedVerifier (input 0) (input 1) = true) ∧
      ∀ input : List Bool,
        (input ∈ language →
          2 ^ (input.length + 1) *
              rejectingCard amplifiedVerifier input
                (amplifiedRandomBits input.length) ≤
            Fintype.card
              (BitString (amplifiedRandomBits input.length))) ∧
        (input ∉ language →
          2 ^ (input.length + 1) *
              acceptingCard amplifiedVerifier input
                (amplifiedRandomBits input.length) ≤
            Fintype.card
              (BitString (amplifiedRandomBits input.length))) := by
  refine
    ⟨amplifiedRandomBitCount randomBits,
      blockAmplifiedVerifier verifier,
      polynomiallyBounded_amplifiedRandomBitCount hrandomBits,
      hamplifiedVerifier, ?_⟩
  intro input
  constructor
  · intro hmember
    rw [rejectingCard_blockAmplifiedVerifier]
    have hthird :
        3 * badCard
            (fun random : BitString (randomBits input.length) =>
              verifier input random.toList = false) ≤
          Fintype.card (BitString (randomBits input.length)) := by
      rw [badCard_rejecting]
      exact rejectingCard_third_of_accepting_two_thirds verifier input
        (randomBits input.length) ((hboundedError input).1 hmember)
    have hbound := ternaryBad_amplified_bound
      (fun random : BitString (randomBits input.length) =>
        verifier input random.toList = false)
      hthird input.length
    rw [blockTernary_card] at hbound
    exact hbound
  · intro hnonmember
    rw [acceptingCard_blockAmplifiedVerifier]
    have hthird :
        3 * badCard
            (fun random : BitString (randomBits input.length) =>
              verifier input random.toList = true) ≤
          Fintype.card (BitString (randomBits input.length)) := by
      rw [badCard_accepting]
      exact acceptingCard_third_of_rejecting_two_thirds verifier input
        (randomBits input.length) ((hboundedError input).2 hnonmember)
    have hbound := ternaryBad_amplified_bound
      (fun random : BitString (randomBits input.length) =>
        verifier input random.toList = true)
      hthird input.length
    rw [blockTernary_card] at hbound
    exact hbound

end SipserGacsLautemann