Boolean packing and recovery for the high-rate code

An offline injection places source bits into the information coordinates of several copies of the high-rate code. Each resource is an ordinary Boolean function of the shorter suffix. Summing its selected basis coordinate along a punctured line recovers the requested original Boolean value.

These are semantic recovery theorems. A circuit-size bound additionally requires the runtime lookup, scheduling, and routing circuits.

@[reducible, inline]

abbrev Algebraic.MassProduction.HighRate.InformationBit {width dimension : ℕ} (code : LineCode (BinaryExtension width) (Fin dimension)) (copies : ℕ) : Type

One information bit is identified by its code copy, information point, and binary coordinate inside the field symbol.

Equations

• Algebraic.MassProduction.HighRate.InformationBit code copies = (Fin copies × ↑code.information × Fin width)

noncomputable def Algebraic.MassProduction.HighRate.informationBit {width dimension copies : ℕ} {Source : Type u_1} (code : LineCode (BinaryExtension width) (Fin dimension)) (placement : Source ↪ InformationBit code copies) (values : Source → Bool) (position : InformationBit code copies) : Bool

Fill unused information bits with false. The injection makes occupied positions unambiguous.

Equations

• Algebraic.MassProduction.HighRate.informationBit code placement values position = if occupied : ∃ (source : Source), placement source = position then values (Classical.choose occupied) else false

theorem Algebraic.MassProduction.HighRate.informationBitAtPlacement {width dimension copies : ℕ} {Source : Type u_1} (code : LineCode (BinaryExtension width) (Fin dimension)) (placement : Source ↪ InformationBit code copies) (values : Source → Bool) (source : Source) : informationBit code placement values (placement source) = values source

Every occupied position contains exactly its assigned source bit.

noncomputable def Algebraic.MassProduction.HighRate.informationMessage {width dimension copies : ℕ} {Source : Type u_1} (widthPositive : 0 < width) (code : LineCode (BinaryExtension width) (Fin dimension)) (placement : Source ↪ InformationBit code copies) (values : Source → Bool) (copy : Fin copies) : ↑code.information → BinaryExtension width

Pack one code copy's information symbols in the fixed binary basis.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.MassProduction.HighRate.booleanResource {width dimension copies : ℕ} {Source : Type u_1} {Suffix : Type u_2} (widthPositive : 0 < width) (code : LineCode (BinaryExtension width) (Fin dimension)) (placement : Source ↪ InformationBit code copies) (function : Source → Suffix → Bool) (copy : Fin copies) (point : Fin dimension → BinaryExtension width) (bit : Fin width) (suffix : Suffix) : Bool

A Boolean resource function at one codeword coordinate and one basis bit.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.MassProduction.HighRate.booleanResourceRecovers {width dimension copies : ℕ} {Source : Type u_1} {Suffix : Type u_2} (widthPositive : 0 < width) (code : LineCode (BinaryExtension width) (Fin dimension)) (placement : Source ↪ InformationBit code copies) (function : Source → Suffix → Bool) (source : Source) (suffix : Suffix) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) : ∑ point ∈ puncturedLine (↑(placement source).2.1) direction, booleanResource widthPositive code placement function (placement source).1 point (placement source).2.2 suffix = function source suffix

Each requested bit is the XOR of Boolean resource values on any punctured recovery line through its information point.

theorem Algebraic.MassProduction.HighRate.resourceIncidence_injective {dimension : ℕ} {K : Type u_1} {Request : Type u_2} {Copy : Type u_3} [Field K] [Finite K] (targets : Request → Fin dimension → K) (directions : Request → Projectivization K (Fin dimension → K)) (copy : Request → Copy) (disjoint : ∀ (left right : Request), copy left = copy right → left ≠ right → Disjoint (puncturedLine (targets left) (directions left)) (puncturedLine (targets right) (directions right))) : Function.Injective fun (incidence : Request × { scalar : K // scalar ≠ 0 }) => (copy incidence.1, targets incidence.1 + ↑incidence.2 • (directions incidence.1).rep)

Distinct requests with disjoint recovery lines cannot compete for a resource in the same code copy.