Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Extractor.CorrelationBreaker.Affine.Round.Defs

The actual extraction round in the affine construction #

Starting with a previous long row, the round extracts from the original right source using the row prefix, extracts a short row using that seed, extracts again from the same original right source, and finally extracts the next long row from the original left input. All four calls are actual matched extractors. Short seeds and outputs share the depth-twenty-four width; the long-row depth is an arbitrary semantic parameter.

This is the second-phase round in Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), proof of Theorem 6.1, printed pp.23--25: https://arxiv.org/abs/2110.12652. The total prefix uses false completion. No numerical guard or statistical assertion is built into these definitions.

source
def Algebraic.Cutwidth.Extractor.affineRoundPrefix (h L : ℕ) (row : Fin (matchedBlockOutputBits h L) → Bool) :
Fin (matchedBlockSeedBits L) → Bool

The previous row's seed-width prefix, completed with false bits when necessary.

Equations
Instances For
    source
    def Algebraic.Cutwidth.Extractor.affineRoundMiddleSeed (d h L e : ℕ) (y : Fin d → Bool) (row : Fin (matchedBlockOutputBits h L) → Bool) :
    Fin (matchedBlockSeedBits L) → Bool

    The first right-source call uses the prefix of the actual previous row.

    Equations
    Instances For
      source
      def Algebraic.Cutwidth.Extractor.affineRoundMiddleOutput (d h L e : ℕ) (y : Fin d → Bool) (row : Fin (matchedBlockOutputBits h L) → Bool) :
      Fin (matchedBlockSeedBits L) → Bool

      The short linear extraction rereads the actual previous long row.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Algebraic.Cutwidth.Extractor.affineRoundFinalSeed (d h L e : ℕ) (y : Fin d → Bool) (row : Fin (matchedBlockOutputBits h L) → Bool) :
        Fin (matchedBlockSeedBits L) → Bool

        The second right-source call rereads the original right word.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Algebraic.Cutwidth.Extractor.affineRoundOutput (n d h L e : ℕ) (x : Fin n → Bool) (y : Fin d → Bool) (row : Fin (matchedBlockOutputBits h L) → Bool) :
          Fin (matchedBlockOutputBits h L) → Bool

          The next long row is extracted from the original left input with the actual final seed.

          Equations
          Instances For