In the following, we define distances for smooth ReedSolomon codes wrt power and fiber domains, as per Section 4.3.1, [ACFY24]. We have generalized the definitions for a generic i to present (i,k)-wise distance measures. This modification is necessary to support following lemmas from Section 4.3.2. The definitions from Section 4.3.1 correspond to i = 0.

def BlockRelDistance.indexPowT {F : Type u_1} [Field F] {ι : Type u_2} (S : Finset ι) (φ : ι ↪ F) (k : ℕ) : Type u_1

The 2^k-th power images over an embedding φ : ι ↪ F and a finite set of elements S : Finset ι.

In particular, it returns the set of field elements y ∈ F for which there exists x ∈ S such that y = (φ x)^(2ᵏ). It models the image of the map x ↦ (φ x)^(2ᵏ) restricted to S. Semantically: indexPowT S φ k = { (φ x)^(2ᵏ) | x ∈ S } ⊆ F.

Equations

• BlockRelDistance.indexPowT S φ k = { y : F // ∃ x ∈ S, y = φ x ^ 2 ^ k }

def BlockRelDistance.powFiberT {F : Type u_1} [Field F] {ι : Type u_2} (i : ℕ) {k : ℕ} {S : Finset ι} {φ : ι ↪ F} (S' : Finset (indexPowT S φ i)) (φ' : indexPowT S φ i ↪ F) (y : indexPowT S φ k) : Type u_1

For i ≤ k, the generic 2^(k-i)-th power fiber over y ∈ indexPowT S φ k. For φ' : ι^(2ⁱ) → F, this defines the preimage of y under the map x^(2ⁱ) ↦ x^(2ᵏ) restricted to x^(2ⁱ) ∈ S'.

It returns the subset S' of elements of type ι^(2ⁱ) such that (x^(2ⁱ))^(2^(k-i)) = x^(2^k) = y. Example i = 0 : powFiberT 0 k S' φ' y = { x ∈ S' | (x)^(2^k) = y }. Example i = 1 : powFiberT 1 k S' φ' y = { x^2 ∈ S' | (x^2)^(2^(k-1)) = y }.

Equations

• BlockRelDistance.powFiberT i S' φ' y = { x : BlockRelDistance.indexPowT S φ i // x ∈ S' ∧ φ' x ^ 2 ^ (k - i) = ↑y }

def BlockRelDistance.block {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] (i : ℕ) {k : ℕ} {S : Finset ι} {φ : ι ↪ F} (S' : Finset (indexPowT S φ i)) (φ' : indexPowT S φ i ↪ F) (z : indexPowT S φ k) [DecidableEq F] [DecidableEq ι] [ReedSolomon.Smooth φ] : Type u_1

Definition 4.16 For ι be a smooth evaluation domain, k be a folding parameter, z ∈ (ι^(2ᵏ)), Block is the set of elements { y ∈ S', y ^ 2^(k-i) = z }, for S' : Finset ι^(2ⁱ).

Equations

• BlockRelDistance.block i S' φ' z = BlockRelDistance.powFiberT i S' φ' z

class BlockRelDistance.DecidableBlockDisagreement {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] (i k : ℕ) {S : Finset ι} {φ : ι ↪ F} [DecidableEq F] [DecidableEq ι] [ReedSolomon.Smooth φ] (f : indexPowT S φ i → F) (S' : Finset (indexPowT S φ i)) (φ' : indexPowT S φ i ↪ F) : Type u_1

The class DecidableBlockDisagreement provides a decidability instance for testing pointwise inequality of two functions f, g : ι^(2ⁱ) → F on elements of block i k S' φ' z, for all z ∈ LpowT S' φ' k.

This class abstracts the decidability condition required to determine whether two functions disagree on any point in the preimage of z under the map x^(2ⁱ) ↦ x^(2ᵏ) over the evaluation domain φ' : ι^(2ⁱ) ↪ F. This is useful in defining sets of such z.

• dec_inst (z : indexPowT S φ k) (g : indexPowT S φ i → F) : Decidable (∃ (y : block i S' φ' z), f ↑y ≠ g ↑y)

noncomputable def BlockRelDistance.disagreementSet {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] (i k : ℕ) {S : Finset ι} {φ : ι ↪ F} [DecidableEq F] [DecidableEq ι] [ReedSolomon.Smooth φ] (f : indexPowT S φ i → F) (S' : Finset (indexPowT S φ i)) (φ' : indexPowT S φ i ↪ F) [(i : ℕ) → Fintype (indexPowT S φ i)] [h : DecidableBlockDisagreement i k f S' φ'] (g : indexPowT S φ i → F) : Finset (indexPowT S φ k)

Let C be a smooth ReedSolomon code C = RS[F, ι^(2ⁱ), φ', m] and f,g : ι^(2ⁱ) → F, then the (i,k)-wise block relative distance is defined as Δᵣ(i, k, f, S', φ', g) = |{z ∈ ι ^ 2^k : ∃ y ∈ Block(i,k,S',φ',z) f(y) ≠ g(y)}| / |ι^(2^k)|.

Below, we define a disagreementSet(i,k,f,S',φ') as a map (g → Finset (indexPow S φ k)) using the class DecidableBlockDisagreement, to filter a finite subset of the Finset (indexPow S φ k), as per {z ∈ ι ^ 2^k : ∃ y ∈ Block(i,k,S',φ',z) f(y) ≠ g(y)} for a given g.

Equations

• BlockRelDistance.disagreementSet i k f S' φ' g = {z : BlockRelDistance.indexPowT S φ k | decide (∃ (y : BlockRelDistance.block i S' φ' z), f ↑y ≠ g ↑y) = true}

noncomputable def BlockRelDistance.blockRelDistance {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] (i k : ℕ) {S : Finset ι} {φ : ι ↪ F} [DecidableEq F] [DecidableEq ι] [ReedSolomon.Smooth φ] (f : indexPowT S φ i → F) (S' : Finset (indexPowT S φ i)) (φ' : indexPowT S φ i ↪ F) [(i : ℕ) → Fintype (indexPowT S φ i)] [h : DecidableBlockDisagreement i k f S' φ'] (g : indexPowT S φ i → F) : NNReal

Definition 4.17 Given the disagreementSet from above, we obtain the block relative distance as |disagreementSet|/ |ι ^ (2^k|.

Equations

• BlockRelDistance.blockRelDistance i k f S' φ' g = ↑(BlockRelDistance.disagreementSet i k f S' φ' g).card / ↑(Fintype.card (BlockRelDistance.indexPowT S φ k))

def BlockRelDistance.«termΔᵣ(_,_,_,_,_,_)» : Lean.ParserDescr

notation Δᵣ(i, k, f, S', φ', g) is the (i,k)-wise block relative distance.

Equations

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

noncomputable def BlockRelDistance.minBlockRelDistance {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] (i k : ℕ) {S : Finset ι} {φ : ι ↪ F} [DecidableEq F] [DecidableEq ι] [ReedSolomon.Smooth φ] (f : indexPowT S φ i → F) (S' : Finset (indexPowT S φ i)) (φ' : indexPowT S φ i ↪ F) (Set : Set (indexPowT S φ i → F)) [(i : ℕ) → Fintype (indexPowT S φ i)] [h : DecidableBlockDisagreement i k f S' φ'] : NNReal

For the set S ⊆ F^ι, we define the minimum block relative distance wrt set S.

Equations

• BlockRelDistance.minBlockRelDistance i k f S' φ' Set = sInf {d : NNReal | ∃ g ∈ Set, BlockRelDistance.blockRelDistance i k f S' φ' g = d}

def BlockRelDistance.«termΔₛ(_,_,_,_,_,_)» : Lean.ParserDescr

notation Δₛ(i, k, f, S', φ', Set) denotes the minimum block relative distance wrt Set.

Equations

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

noncomputable def BlockRelDistance.listBlockRelDistance {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] (i k : ℕ) {S : Finset ι} {φ : ι ↪ F} {φ' : indexPowT S φ i ↪ F} {m : ℕ} [DecidableEq F] [DecidableEq ι] [ReedSolomon.Smooth φ] (f : indexPowT S φ i → F) (S' : Finset (indexPowT S φ i)) [(i : ℕ) → Fintype (indexPowT S φ i)] [DecidableEq (indexPowT S φ i)] [ReedSolomon.Smooth φ'] (C : Set (indexPowT S φ i → F)) (hcode : C = ↑(ReedSolomon.smoothCode φ' m)) (δ : NNReal) [h : DecidableBlockDisagreement i k f S' φ'] : Set (indexPowT S φ i → F)

Definition 4.18 For a smooth ReedSolomon code C = RS[F, ι^(2ⁱ), φ', m], proximity parameter δ ∈ [0,1] function f : ι^(2ⁱ) → F, we define the following as the list of codewords of C δ-close to f, i.e., u ∈ C such that Δᵣ(i, k, f, S', φ', u) ≤ δ.

Equations

• BlockRelDistance.listBlockRelDistance i k f S' C hcode δ = {u : BlockRelDistance.indexPowT S φ i → F | u ∈ C ∧ BlockRelDistance.blockRelDistance i k f S' φ' u ≤ δ}

def BlockRelDistance.«termΛᵣ(_,_,_,_,_,_,_)» : Lean.ParserDescr

Λᵣ(i, k, f, S', C, hcode, δ) denotes the list of codewords of C δ-close to f, wrt to the block relative distance.

Equations

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

theorem BlockRelDistance.blockRelDistance_le_hammingDistance {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [Pow ι ℕ] (i k : ℕ) {S : Finset ι} {φ : ι ↪ F} {φ' : indexPowT S φ i ↪ F} {m : ℕ} [DecidableEq F] [DecidableEq ι] [ReedSolomon.Smooth φ] (f g : indexPowT S φ i → F) (S' : Finset (indexPowT S φ i)) [(i : ℕ) → Fintype (indexPowT S φ i)] [DecidableEq (indexPowT S φ i)] [ReedSolomon.Smooth φ'] (C : Set (indexPowT S φ i → F)) (hcode : C = ↑(ReedSolomon.smoothCode φ' m)) (δ : NNReal) [h : DecidableBlockDisagreement i k f S' φ'] (hBound : ↑δᵣ(f, g) ≤ ↑(blockRelDistance i k f S' φ' g)) {δ✝ : NNReal} (hδLe : δ✝ ≤ 1) : let listHamming := ListDecodable.relHammingBall C f ↑δ✝; let listBlock := listBlockRelDistance i k f S' C hcode δ✝; listBlock ⊆ listHamming

Claim 4.19 For a smooth ReedSolomon code C = RS[F, ι^(2ⁱ), m], codewords f, g : ι^(2ⁱ) → F, we have that the relative Hamming distance δᵣ(f,g) is bounded by the block relative distance Δᵣ(i, k, f, S', φ', g). As a result, we have Λᵣ(i, k, f, S', C, hcode, δ) is bounded by Λ(f, C, δ) (list of codewords of C δ-close to f, wrt relative Hamming distance)