Projection, collision count, and runtime semantics for binary hashing #
Every short coefficient vector lifts to its polynomial, whose degree is below the explicit modulus. This proves projection surjectivity. The finite field kernel argument gives the collision count. Polynomial remainder and prefix coefficients identify the actual list program with this semantic map.
theorem
Algebraic.Cutwidth.Extractor.Internal.binaryCoefficientPrefix_surjective
{s m : ℕ}
(width : m ≤ 2 * 3 ^ s)
:
theorem
Algebraic.Cutwidth.Extractor.Internal.binaryFieldHash_add
(s m : ℕ)
(a b seed : AdjoinRoot (binaryModulus s))
:
theorem
Algebraic.Cutwidth.Extractor.Internal.binaryFieldHash_zero
(s m : ℕ)
(seed : AdjoinRoot (binaryModulus s))
:
theorem
Algebraic.Cutwidth.Extractor.Internal.binaryFieldHash_collision_count
{s m : ℕ}
[Fintype (AdjoinRoot (binaryModulus s))]
(width : m ≤ 2 * 3 ^ s)
{a b : AdjoinRoot (binaryModulus s)}
(distinct : a ≠ b)
:
{seed : AdjoinRoot (binaryModulus s) | binaryFieldHash s m a seed = binaryFieldHash s m b seed}.card * 2 ^ m = 2 ^ (2 * 3 ^ s)
theorem
Algebraic.Cutwidth.Extractor.Internal.binaryFieldHash_universal
{s m : ℕ}
[Fintype (AdjoinRoot (binaryModulus s))]
(width : m ≤ 2 * 3 ^ s)
:
theorem
Algebraic.Cutwidth.Extractor.Internal.binaryHashBits_correct
(s : ℕ)
(source seed halfDegree outputCount : List Bool)
(half : halfDegree.length = 3 ^ s)
:
(Polynomial.toFn outputCount.length)
(Complexity.BitPolynomial.ofBits (binaryHashBits source seed halfDegree outputCount)) = binaryFieldHash s outputCount.length (BinaryFieldCodec.decode s source) (BinaryFieldCodec.decode s seed)
theorem
Algebraic.Cutwidth.Extractor.Internal.decodedBinaryHash_eq
(s m : ℕ)
(source : List Bool)
(seed : AdjoinRoot (binaryModulus s))
:
theorem
Algebraic.Cutwidth.Extractor.Internal.decodedBinaryHash_addBits
(s m : ℕ)
(a b : List Bool)
(seed : AdjoinRoot (binaryModulus s))
:
decodedBinaryHash s m (Complexity.BitPolynomial.addBits a b) seed = decodedBinaryHash s m a seed + decodedBinaryHash s m b seed
theorem
Algebraic.Cutwidth.Extractor.Internal.decodedBinaryHash_universal
{s m n : ℕ}
[Fintype (AdjoinRoot (binaryModulus s))]
(capacity : n ≤ 2 * 3 ^ s)
(width : m ≤ 2 * 3 ^ s)
:
UniversalHashFamily fun (bits : { bits : List Bool // bits.length = n }) => decodedBinaryHash s m ↑bits
theorem
Algebraic.Cutwidth.Extractor.Internal.decodedBinaryHash_flatStrongSeededExtractor
{s m n K : ℕ}
{ε : ℝ}
[Fintype (AdjoinRoot (binaryModulus s))]
(capacity : n ≤ 2 * 3 ^ s)
(width : m ≤ 2 * 3 ^ s)
(positive : 0 < K)
(error : 0 ≤ ε)
(budget : 2 ^ m ≤ 4 * ε ^ 2 * ↑K)
:
FlatStrongSeededExtractor (fun (bits : { bits : List Bool // bits.length = n }) => decodedBinaryHash s m ↑bits) K ε
theorem
Algebraic.Cutwidth.Extractor.Internal.binaryHashEval_pair
(source seed halfDegree outputCount : List Bool)
:
binaryHashEval (Complexity.pair (Complexity.pair source seed) (Complexity.pair halfDegree outputCount)) = binaryHashBits source seed halfDegree outputCount
theorem
Algebraic.Cutwidth.Extractor.Internal.binaryHashBits_mem_FP
{source seed halfDegree outputCount : List Bool → List Bool}
(hsource : source ∈ Complexity.FP)
(hseed : seed ∈ Complexity.FP)
(hhalf : halfDegree ∈ Complexity.FP)
(hcount : outputCount ∈ Complexity.FP)
:
(fun (z : List Bool) => binaryHashBits (source z) (seed z) (halfDegree z) (outputCount z)) ∈ Complexity.FP