Circuit fragments for affine Boolean forms

One fragment computes a Boolean affine form over arbitrary existing wires. It uses one AND gate per linear coefficient and the shared linear-size parity compiler. Sequential row compilation plus a threshold fragment yields a linear-size circuit deciding whether the complete affine output is zero.

theorem Complexity.PairwiseIndependentHash.AffineCircuit.linearValue_eq_sum_add {width : ℕ} (coefficients input : BitString width) (constant : Bool) : linearValue coefficients input constant = ∑ coordinate : Fin width, coefficients coordinate * input coordinate + constant

The fragment semantics is the usual Boolean-ring dot product plus its constant coefficient.

theorem Complexity.PairwiseIndependentHash.AffineCircuit.zeroValue_eq_decide {width : ℕ} (output : BitString width) : zeroValue output = decide (output = fun (x : Fin width) => false)

The executable all-zero test agrees with extensional equality to the zero bit string.

@[simp]

theorem Complexity.PairwiseIndependentHash.AffineCircuit.length_compileLinearRaw (available : ℕ) {width : ℕ} (coefficientRefs inputRefs : Fin width → ℕ) (constantRef : ℕ) : List.length (compileLinearRaw available coefficientRefs inputRefs constantRef) = linearGateCount width

An affine-form fragment uses exactly four gates per linear coordinate and four additional gates.

theorem Complexity.PairwiseIndependentHash.AffineCircuit.outputWire_eq (available : ℕ) {width : ℕ} (coefficientRefs inputRefs : Fin width → ℕ) (constantRef : ℕ) : outputWire available width = available + List.length (compileLinearRaw available coefficientRefs inputRefs constantRef) - 1

The final gate emitted by affine-form compilation carries its value.

theorem Complexity.PairwiseIndependentHash.AffineCircuit.topologicallyWellFormed_compileLinearRaw (available : ℕ) [NeZero available] {width : ℕ} (coefficientRefs inputRefs : Fin width → ℕ) (constantRef : ℕ) (hcoefficientRefs : ∀ (i : Fin width), coefficientRefs i < available) (hinputRefs : ∀ (i : Fin width), inputRefs i < available) (hconstantRef : constantRef < available) : CircuitCode.RawCircuit.TopologicallyWellFormed available (compileLinearRaw available coefficientRefs inputRefs constantRef)

The fragment is topologically ordered when all source references name pre-existing wires.

theorem Complexity.PairwiseIndependentHash.AffineCircuit.compileLinearRaw_wellFormed (available : ℕ) [NeZero available] {width : ℕ} (coefficientRefs inputRefs : Fin width → ℕ) (constantRef : ℕ) (hcoefficientRefs : ∀ (i : Fin width), coefficientRefs i < available) (hinputRefs : ∀ (i : Fin width), inputRefs i < available) (hconstantRef : constantRef < available) : CircuitCode.RawCircuit.WellFormed available (compileLinearRaw available coefficientRefs inputRefs constantRef)

The compiled affine form is a nonempty well-formed raw circuit fragment.

theorem Complexity.PairwiseIndependentHash.AffineCircuit.evalAux?_compileLinearRaw (available : ℕ) [NeZero available] {width : ℕ} (coefficientRefs inputRefs : Fin width → ℕ) (constantRef : ℕ) (coefficients input : BitString width) (constant : Bool) (wires : Array Bool) (hsize : wires.size = available) (hcoefficientRefs : ∀ (i : Fin width), coefficientRefs i < available) (hinputRefs : ∀ (i : Fin width), inputRefs i < available) (hconstantRef : constantRef < available) (hcoefficients : ∀ (i : Fin width), wires[coefficientRefs i]? = some (coefficients i)) (hinputs : ∀ (i : Fin width), wires[inputRefs i]? = some (input i)) (hconstant : wires[constantRef]? = some constant) : ∃ (result : Array Bool), (compileLinearRaw available coefficientRefs inputRefs constantRef).evalAux? wires = some result ∧ result.size = wires.size + linearGateCount width ∧ (∀ i < wires.size, result[i]? = wires[i]?) ∧ result[outputWire available width]? = some (linearValue coefficients input constant)

Evaluation appends the affine-form value while preserving every existing wire.

@[simp]

theorem Complexity.PairwiseIndependentHash.AffineCircuit.length_compileRowsRaw (available width rowCount : ℕ) (coefficientRefs : Fin rowCount → Fin (width + 1) → ℕ) (inputRefs : Fin width → ℕ) : List.length (compileRowsRaw available width rowCount coefficientRefs inputRefs) = rowCount * linearGateCount width

Sequential row compilation has exact additive size.

@[simp]

theorem Complexity.PairwiseIndependentHash.AffineCircuit.length_compileZeroRaw (available width rowCount : ℕ) (coefficientRefs : Fin rowCount → Fin (width + 1) → ℕ) (inputRefs : Fin width → ℕ) : List.length (compileZeroRaw available width rowCount coefficientRefs inputRefs) = zeroGateCount width rowCount

The full affine-zero fragment has its advertised linear gate count.

theorem Complexity.PairwiseIndependentHash.AffineCircuit.zeroOutputWire_eq (available width rowCount : ℕ) (coefficientRefs : Fin rowCount → Fin (width + 1) → ℕ) (inputRefs : Fin width → ℕ) : zeroOutputWire available width rowCount = available + List.length (compileZeroRaw available width rowCount coefficientRefs inputRefs) - 1

The final gate of full affine-zero compilation carries its decision.

theorem Complexity.PairwiseIndependentHash.AffineCircuit.topologicallyWellFormed_compileZeroRaw (available width rowCount : ℕ) [NeZero available] (coefficientRefs : Fin rowCount → Fin (width + 1) → ℕ) (inputRefs : Fin width → ℕ) (hcoefficientRefs : ∀ (row : Fin rowCount) (coordinate : Fin (width + 1)), coefficientRefs row coordinate < available) (hinputRefs : ∀ (coordinate : Fin width), inputRefs coordinate < available) : CircuitCode.RawCircuit.TopologicallyWellFormed available (compileZeroRaw available width rowCount coefficientRefs inputRefs)

The full affine-zero fragment is topologically ordered when all matrix and input references name pre-existing wires.

theorem Complexity.PairwiseIndependentHash.AffineCircuit.compileZeroRaw_wellFormed (available width rowCount : ℕ) [NeZero available] (coefficientRefs : Fin rowCount → Fin (width + 1) → ℕ) (inputRefs : Fin width → ℕ) (hcoefficientRefs : ∀ (row : Fin rowCount) (coordinate : Fin (width + 1)), coefficientRefs row coordinate < available) (hinputRefs : ∀ (coordinate : Fin width), inputRefs coordinate < available) : CircuitCode.RawCircuit.WellFormed available (compileZeroRaw available width rowCount coefficientRefs inputRefs)

The full affine-zero builder produces a nonempty well-formed raw circuit.

theorem Complexity.PairwiseIndependentHash.AffineCircuit.evalAux?_compileZeroRaw (available width rowCount : ℕ) [NeZero available] (coefficientRefs : Fin rowCount → Fin (width + 1) → ℕ) (inputRefs : Fin width → ℕ) (coefficients : Fin rowCount → BitString (width + 1)) (input : BitString width) (wires : Array Bool) (hsize : wires.size = available) (hcoefficientRefs : ∀ (row : Fin rowCount) (coordinate : Fin (width + 1)), coefficientRefs row coordinate < available) (hinputRefs : ∀ (coordinate : Fin width), inputRefs coordinate < available) (hcoefficients : ∀ (row : Fin rowCount) (coordinate : Fin (width + 1)), wires[coefficientRefs row coordinate]? = some (coefficients row coordinate)) (hinputs : ∀ (coordinate : Fin width), wires[inputRefs coordinate]? = some (input coordinate)) : ∃ (result : Array Bool), (compileZeroRaw available width rowCount coefficientRefs inputRefs).evalAux? wires = some result ∧ result.size = wires.size + zeroGateCount width rowCount ∧ (∀ i < wires.size, result[i]? = wires[i]?) ∧ result[zeroOutputWire available width rowCount]? = some (zeroValue fun (row : Fin rowCount) => linearValue (fun (coordinate : Fin width) => coefficients row coordinate.castSucc) input (coefficients row (Fin.last width)))

Evaluation preserves the incoming prefix and decides whether every compiled affine form vanishes.

theorem Complexity.PairwiseIndependentHash.AffineCircuit.eval?_compileZeroRaw (available width rowCount : ℕ) [NeZero available] (coefficientRefs : Fin rowCount → Fin (width + 1) → ℕ) (inputRefs : Fin width → ℕ) (hcoefficientRefs : ∀ (row : Fin rowCount) (coordinate : Fin (width + 1)), coefficientRefs row coordinate < available) (hinputRefs : ∀ (coordinate : Fin width), inputRefs coordinate < available) (input : BitString available) : (compileZeroRaw available width rowCount coefficientRefs inputRefs).eval? input.toList = some (zeroValue fun (row : Fin rowCount) => linearValue (fun (coordinate : Fin width) => input ⟨coefficientRefs row coordinate.castSucc, ⋯⟩) (fun (coordinate : Fin width) => input ⟨inputRefs coordinate, ⋯⟩) (input ⟨coefficientRefs row (Fin.last width), ⋯⟩))

Direct raw evaluation returns the all-zero decision for the affine forms selected from the primary input wires.

theorem Complexity.PairwiseIndependentHash.AffineCircuit.linearValue_affineRow {domainWidth rangeWidth : ℕ} (seed : BitString (affineSeedWidth domainWidth rangeWidth)) (input : BitString domainWidth) (row : Fin rangeWidth) : linearValue (fun (coordinate : Fin domainWidth) => affineRows seed row coordinate.castSucc) input (affineRows seed row (Fin.last domainWidth)) = affineEval seed input row

Specializing the generic affine form to one row of the standard seed matrix agrees with affineEval.

theorem Complexity.PairwiseIndependentHash.AffineCircuit.zeroValue_affineEval {domainWidth rangeWidth : ℕ} (seed : BitString (affineSeedWidth domainWidth rangeWidth)) (input : BitString domainWidth) : (zeroValue fun (row : Fin rangeWidth) => linearValue (fun (coordinate : Fin domainWidth) => affineRows seed row coordinate.castSucc) input (affineRows seed row (Fin.last domainWidth))) = decide (affineEval seed input = fun (x : Fin rangeWidth) => false)

The all-zero value of the compiled matrix rows is exactly the affine zero-cell predicate.