Recovery by a fixed padded XOR fold

The circuit-friendly power-of-two scalar list has one invalid zero slot. Masking that slot by false makes its Boolean sum exactly the punctured-line sum in the high-rate code's recovery theorem.

theorem Algebraic.MassProduction.Nonuniform.PaddedLinePoints.point_injective {width dimension : ℕ} (positive : 0 < width) (target : Fin dimension → BinaryExtension width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) : Function.Injective (point positive target direction)

The underlying affine points, including the target, are all distinct.

theorem Algebraic.MassProduction.Nonuniform.PaddedLinePoints.point_mem_puncturedLine {width dimension : ℕ} (positive : 0 < width) (target : Fin dimension → BinaryExtension width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (slot : Fin (2 ^ width)) (active : valid positive slot = true) : point positive target direction slot ∈ puncturedLine target direction

Every valid scalar slot is on the punctured line.

theorem Algebraic.MassProduction.Nonuniform.PaddedLinePoints.sum_valid_points {width dimension : ℕ} {Value : Type u_1} [AddCommMonoid Value] (positive : 0 < width) (target : Fin dimension → BinaryExtension width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (values : (Fin dimension → BinaryExtension width) → Value) : (∑ slot : Fin (2 ^ width), if valid positive slot = true then values (point positive target direction slot) else 0) = ∑ value ∈ puncturedLine target direction, values value

Zero-masked padded scalar summation equals punctured-line summation.

theorem Algebraic.MassProduction.Nonuniform.PaddedLinePoints.booleanResourceRecovers {width dimension copies : ℕ} {Source : Type u_1} {Suffix : Type u_2} (positive : 0 < width) (code : HighRate.LineCode (BinaryExtension width) (Fin dimension)) (placement : Source ↪ HighRate.InformationBit code copies) (function : Source → Suffix → Bool) (source : Source) (suffix : Suffix) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) : (∑ slot : Fin (2 ^ width), if valid positive slot = true then HighRate.booleanResource positive code placement function (placement source).1 (point positive (↑(placement source).2.1) direction slot) (placement source).2.2 suffix else false) = function source suffix

The padded Boolean fold recovers exactly the original requested source bit.