A uniform linear binary hash and its strong extraction guarantee

Multiplication modulo the explicit binary trinomial followed by coefficient truncation is universal at every output width within the field width. The actual bit-list evaluator computes that same map and belongs to FP uniformly in its source, seed, modulus half-degree, and requested output width.

For every fixed input length within field capacity, decoding is injective. The retained-seed leftover-hash lemma therefore applies directly to the computed output on flat sources. The seed has one field element's width; this is a building block for shorter-seed constructions. Source credits for the standard multiplication and truncation method are in Hashing.Field.Defs.

theorem Algebraic.Cutwidth.Extractor.binaryCoefficientPrefix_surjective {s m : ℕ} (width : m ≤ 2 * 3 ^ s) : Function.Surjective ⇑(binaryCoefficientPrefix s m)

Every coefficient vector shorter than the modulus degree is represented.

theorem Algebraic.Cutwidth.Extractor.binaryFieldHash_add (s m : ℕ) (a b seed : AdjoinRoot (binaryModulus s)) : binaryFieldHash s m (a + b) seed = binaryFieldHash s m a seed + binaryFieldHash s m b seed

Every fixed-seed binary field hash preserves source addition.

theorem Algebraic.Cutwidth.Extractor.binaryFieldHash_zero (s m : ℕ) (seed : AdjoinRoot (binaryModulus s)) : binaryFieldHash s m 0 seed = 0

Every fixed-seed binary field hash sends zero to zero.

theorem Algebraic.Cutwidth.Extractor.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)

Distinct field inputs collide on exactly a reciprocal-output fraction of seeds.

theorem Algebraic.Cutwidth.Extractor.binaryFieldHash_universal {s m : ℕ} [Fintype (AdjoinRoot (binaryModulus s))] (width : m ≤ 2 * 3 ^ s) : UniversalHashFamily (binaryFieldHash s m)

Coefficient-prefix multiplication is a universal family.

theorem Algebraic.Cutwidth.Extractor.binaryField_decode_inj_of_length (s n : ℕ) (capacity : n ≤ 2 * 3 ^ s) (a b : List Bool) (ha : a.length = n) (hb : b.length = n) (same : BinaryFieldCodec.decode s a = BinaryFieldCodec.decode s b) : a = b

Decoding is injective on each fixed source length within field capacity.

theorem Algebraic.Cutwidth.Extractor.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)

The actual multiply/reduce/take program computes the binary field hash.

theorem Algebraic.Cutwidth.Extractor.decodedBinaryHash_eq (s m : ℕ) (source : List Bool) (seed : AdjoinRoot (binaryModulus s)) : decodedBinaryHash s m source seed = binaryFieldHash s m (BinaryFieldCodec.decode s source) seed

The decoded program at a canonical field seed is the semantic hash.

theorem Algebraic.Cutwidth.Extractor.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

The actual decoded hash preserves padded source XOR, including unequal lengths.

theorem Algebraic.Cutwidth.Extractor.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

The actual program is universal on fixed-length sources within capacity.

theorem Algebraic.Cutwidth.Extractor.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 ε

The actual program strongly extracts whenever the sharp leftover-hash budget holds.

theorem Algebraic.Cutwidth.Extractor.binaryHashBits_length (s : ℕ) (source seed halfDegree outputCount : List Bool) (half : halfDegree.length = 3 ^ s) : (binaryHashBits source seed halfDegree outputCount).length = min outputCount.length (2 * 3 ^ s)

A valid field modulus gives the requested prefix, capped at the field width.

theorem Algebraic.Cutwidth.Extractor.binaryHashEval_pair (source seed halfDegree outputCount : List Bool) : binaryHashEval (Complexity.pair (Complexity.pair source seed) (Complexity.pair halfDegree outputCount)) = binaryHashBits source seed halfDegree outputCount

The evaluator reads the four runtime words from their paired encoding.

theorem Algebraic.Cutwidth.Extractor.binaryHashEval_length_le (z : List Bool) : (binaryHashEval z).length ≤ z.length

Even malformed paired inputs have output length at most the input length.

theorem Algebraic.Cutwidth.Extractor.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

Runtime binary hashing is uniformly polynomial-time in all four operands.

theorem Algebraic.Cutwidth.Extractor.binaryHashEval_mem_FP : binaryHashEval ∈ Complexity.FP

A single polynomial-time machine computes the paired runtime hash.