feat: statement of FRI-Binius

Author: chung-thai-nguyen

ArkLib.lean

@@ -127,7 +127,22 @@ import ArkLib.OracleReduction.Security.RoundByRound
 import ArkLib.OracleReduction.Security.SpecialSoundness
 import ArkLib.OracleReduction.Security.StateRestoration
 import ArkLib.OracleReduction.VectorIOR
-import ArkLib.ProofSystem.Binius.Basic
+import ArkLib.ProofSystem.Binius.BinaryBasefold.CommitmentPhase
+import ArkLib.ProofSystem.Binius.BinaryBasefold.CoreInteractionPhase
+import ArkLib.ProofSystem.Binius.BinaryBasefold.General
+import ArkLib.ProofSystem.Binius.BinaryBasefold.Prelude
+import ArkLib.ProofSystem.Binius.BinaryBasefold.QueryPhase
+import ArkLib.ProofSystem.Binius.FRIBinius.BatchingPhase
+import ArkLib.ProofSystem.Binius.FRIBinius.CoreInteractionPhase
+import ArkLib.ProofSystem.Binius.FRIBinius.FinalizationPhase
+import ArkLib.ProofSystem.Binius.FRIBinius.General
+import ArkLib.ProofSystem.Binius.FRIBinius.Prelude
+import ArkLib.ProofSystem.Binius.FRIBinius.QueryPhase
+import ArkLib.ProofSystem.Binius.RingSwitching.BatchingPhase
+import ArkLib.ProofSystem.Binius.RingSwitching.CoreInteractionPhase
+import ArkLib.ProofSystem.Binius.RingSwitching.FinalizationPhase
+import ArkLib.ProofSystem.Binius.RingSwitching.General
+import ArkLib.ProofSystem.Binius.RingSwitching.Prelude
 import ArkLib.ProofSystem.Component.CheckClaim
 import ArkLib.ProofSystem.Component.DoNothing
 import ArkLib.ProofSystem.Component.NoInteraction

ArkLib/Data/FieldTheory/AdditiveNTT/AdditiveNTT.lean

@@ -666,6 +666,24 @@ noncomputable def sDomain_basis (i : Fin r) (h_i : i < ℓ + R_rate) :
   -- We map the basis of Vᵢ through our isomorphism to get the desired basis for S⁽ⁱ⁾.
   exact V_i_basis.map iso
 
+noncomputable instance fintype_sDomain (i : Fin r) : Fintype (sDomain 𝔽q h_Fq_char_prime h_Fq_card_gt_1 β hβ_lin_indep ℓ R_rate h_ℓ_add_R_rate i) := by
+  exact Fintype.ofFinite (sDomain 𝔽q h_Fq_char_prime h_Fq_card_gt_1 β hβ_lin_indep ℓ R_rate h_ℓ_add_R_rate i)
+
+-- The cardinality of the subspace `S⁽ⁱ⁾` is `|𝔽q|^(l + R - i)`, which follows from its dimension.
+lemma sDomain_card (hβ_lin_indep : LinearIndependent 𝔽q β)
+  (i : Fin r) (h_i : i < ℓ + R_rate):
+    Fintype.card (sDomain 𝔽q h_Fq_char_prime h_Fq_card_gt_1 β hβ_lin_indep ℓ R_rate h_ℓ_add_R_rate i) = (Fintype.card 𝔽q)^(ℓ + R_rate - i) := by
+  -- The cardinality of a vector space V is |F|^(dim V).
+  rw [Module.card_eq_pow_finrank (K := 𝔽q) (V := sDomain 𝔽q h_Fq_char_prime h_Fq_card_gt_1 β hβ_lin_indep ℓ R_rate h_ℓ_add_R_rate i)]
+  -- We need to show that the finrank of sDomain is ℓ + R_rate - i
+  -- This follows from the fact that sDomain has a basis of size ℓ + R_rate - i
+  -- We can use the basis we constructed
+  let b := sDomain_basis 𝔽q h_Fq_char_prime h_Fq_card_gt_1 β hβ_lin_indep ℓ R_rate h_ℓ_add_R_rate i h_i
+  -- The finrank equals the cardinality of the basis
+  rw [Module.finrank_eq_card_basis b]
+  -- The basis has cardinality ℓ + R_rate - i
+  simp only [Fintype.card_fin]
+
 /-! ### 2. Intermediate Novel Polynomial Bases `Xⱼ⁽ⁱ⁾`  and evaluation polynomials `P⁽ⁱ⁾`-/
 
 /-- `∀ i ∈ {0, ..., ℓ}`, The `i`-th order subspace vanishing polynomials `Ŵₖ⁽ⁱ⁾`,
@@ -2257,4 +2275,67 @@ theorem additiveNTT_correctness
   simp_rw [Nat.sub_right_comm] -- ℓ - 1 - ↑i = ℓ - ↑i - 1
 
 end AlgorithmCorrectness
+
+section DomainBijection
+/-!
+## Domain-Index Bijections
+
+Bijections between elements in `S^(i)` and `Fin (2^(ℓ + R_rate - i))` for use in
+Binary Basefold protocol implementations.
+-/
+
+/-- Convert an element of `S^(i)` to its index in `Fin (2^(ℓ + R_rate - i))`.
+This uses the basis representation of elements in the domain. -/
+noncomputable def sDomainToFin (i : Fin r) (h_i : i < ℓ + R_rate)
+  (x : sDomain 𝔽q h_Fq_char_prime h_Fq_card_gt_1 β hβ_lin_indep ℓ R_rate h_ℓ_add_R_rate i) :
+  Fin (2^(ℓ + R_rate - i.val)) := by
+  -- Get the basis representation of x
+  let basis := sDomain_basis 𝔽q h_Fq_char_prime h_Fq_card_gt_1 β hβ_lin_indep ℓ R_rate h_ℓ_add_R_rate i h_i
+  let coeffs := basis.repr x
+  -- Convert the coefficients to a natural number (binary interpretation)
+  let nat_val: ℕ := Finsupp.sum coeffs (fun j c =>
+    sorry -- if c = 0 then 0 else 2^j.val
+  )
+  -- Return as Fin
+  exact ⟨nat_val % (2^(ℓ + R_rate - i.val)), by
+    apply Nat.mod_lt
+    apply Nat.pow_pos
+    norm_num⟩
+
+/-- Convert an index in `Fin (2^(ℓ + R_rate - i))` to an element of `S^(i)`.
+This is the inverse of `sDomainToFin`. -/
+noncomputable def finToSDomain (i : Fin r) (h_i : i < ℓ + R_rate)
+  (idx : Fin (2^(ℓ + R_rate - i.val))) :
+  sDomain 𝔽q h_Fq_char_prime h_Fq_card_gt_1 β hβ_lin_indep ℓ R_rate h_ℓ_add_R_rate i := by
+  -- Get the basis
+  let basis := sDomain_basis 𝔽q h_Fq_char_prime h_Fq_card_gt_1 β hβ_lin_indep ℓ R_rate h_ℓ_add_R_rate i h_i
+  -- Convert the index to binary coefficients
+  let coeffs : Fin (ℓ + R_rate - i.val) → 𝔽q := fun j =>
+    if (idx.val / 2^j.val) % 2 = 1 then 1 else 0
+  -- Construct the element using the basis
+  exact basis (by
+    sorry
+    -- Finsupp.ofSupportFinite coeffs (by
+    -- The support is finite since we're working with Fin
+    -- apply Set.finite_lt_nat))
+  )
+
+/-- The bijection between `S^(i)` and `Fin (2^(ℓ + R_rate - i))`. -/
+noncomputable def sDomainFinEquiv (i : Fin r) (h_i : i < ℓ + R_rate) :
+  (sDomain 𝔽q h_Fq_char_prime h_Fq_card_gt_1 β hβ_lin_indep ℓ R_rate h_ℓ_add_R_rate i) ≃
+  Fin (2^(ℓ + R_rate - i.val)) := {
+  toFun := sDomainToFin 𝔽q h_Fq_char_prime h_Fq_card_gt_1 β hβ_lin_indep ℓ R_rate h_ℓ_add_R_rate i h_i,
+  invFun := finToSDomain 𝔽q h_Fq_char_prime h_Fq_card_gt_1 β hβ_lin_indep ℓ R_rate h_ℓ_add_R_rate i h_i,
+  left_inv := by
+    intro x
+    -- This requires proving that finToSDomain (sDomainToFin x) = x
+    sorry,
+  right_inv := by
+    intro idx
+    -- This requires proving that sDomainToFin (finToSDomain idx) = idx
+    sorry
+}
+
+end DomainBijection
+
 end AdditiveNTT

ArkLib/Data/FieldTheory/AdditiveNTT/NovelPolynomialBasis.lean

@@ -1419,7 +1419,7 @@ def toCoeffsVec (ℓ : Nat) : L⦃<2^ℓ⦄[X] →ₗ[L] CoeffVecSpace L ℓ whe
 non-zero diagonal entries are linearly independent. -/
 lemma linearIndependent_rows_of_lower_triangular_ne_zero_diag
   {n : ℕ} {R : Type*} [Field R] (A : Matrix (Fin n) (Fin n) R)
-  (h_lower_triangular: A.BlockTriangular ⇑OrderDual.toDual) (h_diag: ∀ i, A i i ≠ 0) :
+  (h_lower_triangular : A.BlockTriangular ⇑OrderDual.toDual) (h_diag : ∀ i, A i i ≠ 0) :
   LinearIndependent R A := by -- This follows from the fact that such a matrix is invertible
   -- because its determinant is non-zero.
   have h_det : A.det ≠ 0 := by
@@ -1428,12 +1428,65 @@ lemma linearIndependent_rows_of_lower_triangular_ne_zero_diag
     intro i _; exact h_diag i
   exact Matrix.linearIndependent_rows_of_det_ne_zero (A := A) h_det
 
+/-- The change-of-basis matrix from the novel basis to the monomial basis.
+Aⱼᵢ = coeff of Xⁱ in novel basis vector 𝕏ⱼ. novel_coeffs * A = monomial_coeffs -/
 noncomputable def changeOfBasisMatrix (hF₂ : Fintype.card 𝔽q = 2)
   (hβ_lin_indep : LinearIndependent 𝔽q β)
   (ℓ : Nat) (h_ℓ : ℓ ≤ r) : Matrix (Fin (2^ℓ)) (Fin (2^ℓ)) L :=
     fun j i => (toCoeffsVec (L := L) (ℓ := ℓ) (
       basisVectors 𝔽q β hβ_lin_indep hF₂ ℓ h_ℓ j)) i
 
+theorem changeOfBasisMatrix_lower_triangular (hF₂ : Fintype.card 𝔽q = 2)
+  (hβ_lin_indep : LinearIndependent 𝔽q β) (ℓ : Nat) (h_ℓ : ℓ ≤ r) :
+  (changeOfBasisMatrix 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ).BlockTriangular ⇑OrderDual.toDual := by
+  intro i j hij
+  dsimp only [toCoeffsVec, basisVectors, LinearMap.coe_mk, AddHom.coe_mk, changeOfBasisMatrix]
+  -- ⊢ (Xⱼ β ℓ ↑i).coeff ↑j = 0
+  have deg_X : (Xⱼ 𝔽q β ℓ h_ℓ i).degree = i :=
+    degree_Xⱼ 𝔽q β hβ_lin_indep hF₂ ℓ h_ℓ i
+  have h_i_lt_j : i < j := by
+    simp only [OrderDual.toDual_lt_toDual] at hij
+    exact hij
+  have h_res: (Xⱼ 𝔽q β ℓ h_ℓ i).coeff j = 0 := by
+    apply coeff_eq_zero_of_natDegree_lt -- we don't use coeff_eq_zero_of_degree_lt
+    -- because p.natDegree returns a value of type ℕ instead of WithBot ℕ as in p.degree
+    rw [natDegree_eq_of_degree_eq_some (degree_Xⱼ 𝔽q β hβ_lin_indep hF₂ ℓ h_ℓ i)]
+    norm_cast -- auto resolve via h_i_lt_j
+  exact h_res
+
+theorem changeOfBasisMatrix_diag_ne_zero (hF₂ : Fintype.card 𝔽q = 2)
+  (hβ_lin_indep : LinearIndependent 𝔽q β) (ℓ : Nat) (h_ℓ : ℓ ≤ r) :
+  (∀ i, (changeOfBasisMatrix 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ) i i ≠ 0) := by
+  intro i
+  dsimp [changeOfBasisMatrix, toCoeffsVec, basisVectors]
+  have h_deg : (Xⱼ 𝔽q β ℓ h_ℓ i).degree = i := degree_Xⱼ 𝔽q β hβ_lin_indep hF₂ ℓ h_ℓ i
+  apply coeff_ne_zero_of_eq_degree
+  norm_cast
+
+/-- The determinant of the change-of-basis matrix is non-zero. -/
+theorem changeOfBasisMatrix_det_ne_zero (hF₂ : Fintype.card 𝔽q = 2)
+  (hβ_lin_indep : LinearIndependent 𝔽q β) (ℓ : Nat) (h_ℓ : ℓ ≤ r) :
+  (changeOfBasisMatrix 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ).det ≠ 0 := by
+  let A := changeOfBasisMatrix 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ
+  -- Use the fact that A is lower-triangular with non-zero diagonal
+  rw [Matrix.det_of_lowerTriangular A]
+  · -- The determinant of a lower-triangular matrix is
+    -- the product of diagonal entries: ⊢ ∏ i, A i i ≠ 0
+    let res := changeOfBasisMatrix_diag_ne_zero 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ
+    exact prod_ne_zero_iff.mpr fun a a_1 ↦ res a
+  · -- A is lower-triangular
+    exact changeOfBasisMatrix_lower_triangular 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ
+
+/-- The change-of-basis matrix is invertible, this is required by the proofs
+ of inversion between monomial and novel polynomial basis coefficients. -/
+noncomputable instance changeOfBasisMatrix_invertible (hF₂ : Fintype.card 𝔽q = 2)
+  (hβ_lin_indep : LinearIndependent 𝔽q β) (ℓ : Nat) (h_ℓ : ℓ ≤ r) :
+  Invertible (changeOfBasisMatrix 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ) := by
+  let h_A_invertible: Invertible (changeOfBasisMatrix 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ) := by
+    refine (changeOfBasisMatrix 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ).invertibleOfIsUnitDet ?_
+    (expose_names; exact Ne.isUnit (changeOfBasisMatrix_det_ne_zero 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ))
+  exact h_A_invertible
+
 /--
 The coefficient vectors of the novel basis polynomials are linearly independent.
 This is proven by showing that the change-of-basis matrix to the monomial basis
@@ -1448,29 +1501,9 @@ lemma coeff_vectors_linear_independent (hF₂ : Fintype.card 𝔽q = 2)
   -- Apply the lemma about triangular matrices.
   apply linearIndependent_rows_of_lower_triangular_ne_zero_diag A
   · -- ⊢ A.BlockTriangular ⇑OrderDual.toDual => Prove the matrix A is lower-triangular.
-    intro i j hij
-    dsimp only [toCoeffsVec, basisVectors, LinearMap.coe_mk, AddHom.coe_mk, A]
-    -- ⊢ (Xⱼ β ℓ ↑i).coeff ↑j = 0
-    have deg_X : (Xⱼ 𝔽q β ℓ h_ℓ i).degree = i :=
-      degree_Xⱼ 𝔽q β hβ_lin_indep hF₂ ℓ h_ℓ i
-    have h_i_lt_j : i < j := by
-      simp only [OrderDual.toDual_lt_toDual] at hij
-      exact hij
-    have h_res: (Xⱼ 𝔽q β ℓ h_ℓ i).coeff j = 0 := by
-      apply coeff_eq_zero_of_natDegree_lt -- we don't use coeff_eq_zero_of_degree_lt
-      -- because p.natDegree returns a value of type ℕ instead of WithBot ℕ as in p.degree
-      rw [natDegree_eq_of_degree_eq_some (degree_Xⱼ 𝔽q β hβ_lin_indep hF₂ ℓ h_ℓ i)]
-      norm_cast -- auto resolve via h_i_lt_j
-    exact h_res
+    exact changeOfBasisMatrix_lower_triangular 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ
   · -- ⊢ ∀ (i : Fin (2 ^ ℓ)), A i i ≠ 0 => All diagonal entries are non-zero.
-    intro i
-    dsimp [A, toCoeffsVec, basisVectors]
-    -- `A i i` is the `i`-th (also the leading) coefficient of `Xⱼ`, which is non-zero.
-    have h_deg : (Xⱼ 𝔽q β ℓ h_ℓ i).degree = i := degree_Xⱼ 𝔽q β hβ_lin_indep hF₂ ℓ h_ℓ i
-    have h_natDegree : (Xⱼ 𝔽q β ℓ h_ℓ i).natDegree = i := natDegree_eq_of_degree_eq_some h_deg
-    have deg_X : (Xⱼ 𝔽q β ℓ h_ℓ i).degree = i := degree_Xⱼ 𝔽q β hβ_lin_indep hF₂ ℓ h_ℓ i
-    apply coeff_ne_zero_of_eq_degree -- (hn : degree p = n) : coeff p n ≠ 0
-    norm_cast
+    exact fun i ↦ changeOfBasisMatrix_diag_ne_zero 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ i
 
 /-- The basis vectors are linearly independent over `L`. -/
 theorem basisVectors_linear_independent (hF₂ : Fintype.card 𝔽q = 2) (ℓ : Nat) (h_ℓ : ℓ ≤ r) :
@@ -1524,4 +1557,63 @@ theorem novelPolynomialBasis_is_basisVectors (hF₂ : Fintype.card 𝔽q = 2) (
     = basisVectors 𝔽q β hβ_lin_indep hF₂ ℓ h_ℓ := by
   simp only [novelPolynomialBasis, Basis.coe_mk]
 
+/-- Convert monomial coefficients to novel polynomial basis coefficients.
+Using row vectors: n = m * A⁻¹.
+-/
+noncomputable def monomialToNovelCoeffs (hF₂ : Fintype.card 𝔽q = 2)
+  (hβ_lin_indep : LinearIndependent 𝔽q β)
+  (ℓ : ℕ) (h_ℓ : ℓ ≤ r) (monomial_coeffs : Fin (2 ^ ℓ) → L) : Fin (2^ℓ) → L :=
+  let A := changeOfBasisMatrix 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ
+  -- We need A to be invertible to use A⁻¹. This is implicitly handled by Lean
+  -- when A⁻¹ is used, but we will rely on the determinant proof later.
+  Matrix.vecMul monomial_coeffs A⁻¹
+
+/-- Convert novel polynomial basis coefficients to monomial coefficients.
+Using row vectors: m = n * A.
+-/
+noncomputable def novelToMonomialCoeffs (hF₂ : Fintype.card 𝔽q = 2)
+  (hβ_lin_indep : LinearIndependent 𝔽q β)
+  (ℓ : ℕ) (h_ℓ : ℓ ≤ r) (novel_coeffs : Fin (2 ^ ℓ) → L) : Fin (2^ℓ) → L :=
+  let A := changeOfBasisMatrix 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ
+  Matrix.vecMul novel_coeffs A
+
+/-- The conversion functions are inverses of each other. (Monomial -> Novel -> Monomial) -/
+theorem monomialToNovel_novelToMonomial_inverse (hF₂ : Fintype.card 𝔽q = 2)
+  (hβ_lin_indep : LinearIndependent 𝔽q β) (ℓ : ℕ) (h_ℓ : ℓ ≤ r) :
+  ∀ coeffs : Fin (2^ℓ) → L,
+    novelToMonomialCoeffs 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ
+    (monomialToNovelCoeffs 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ coeffs) = coeffs := by
+  intro coeffs
+  -- Unfold the definitions and the let bindings.
+  unfold monomialToNovelCoeffs novelToMonomialCoeffs
+  dsimp only
+  -- Let A be the change of basis matrix.
+  let A := changeOfBasisMatrix 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ
+  -- Goal: (coeffs * A⁻¹) * A = coeffs
+  -- Use associativity of vecMul: (v * M) * N = v * (M * N).
+  rw [Matrix.vecMul_vecMul]
+  -- Goal: coeffs * (A⁻¹ * A) = coeffs, We need A⁻¹ * A = I. This requires det(A) ≠ 0.
+  -- Use Matrix.nonsing_inv_mul (A⁻¹ * A = I).
+  rw [Matrix.nonsing_inv_mul A (Matrix.isUnit_det_of_invertible A)]
+  -- Goal: coeffs * 1 = coeffs
+  rw [Matrix.vecMul_one]
+
+/-- The conversion functions are inverses of each other. (Novel -> Monomial -> Novel) -/
+theorem novelToMonomial_monomialToNovel_inverse (hF₂ : Fintype.card 𝔽q = 2)
+  (hβ_lin_indep : LinearIndependent 𝔽q β) (ℓ : ℕ) (h_ℓ : ℓ ≤ r) :
+  ∀ coeffs : Fin (2^ℓ) → L,
+    monomialToNovelCoeffs 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ
+      (novelToMonomialCoeffs 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ coeffs) = coeffs := by
+  intro coeffs
+  -- Unfold the definitions and the let bindings.
+  unfold novelToMonomialCoeffs monomialToNovelCoeffs
+  dsimp only
+  let A := changeOfBasisMatrix 𝔽q β hF₂ hβ_lin_indep ℓ h_ℓ
+  -- Goal: (coeffs * A) * A⁻¹ = coeffs
+  rw [Matrix.vecMul_vecMul]
+  -- Goal: coeffs * (A * A⁻¹) = coeffs, we need A * A⁻¹ = I.
+  rw [Matrix.mul_nonsing_inv A (Matrix.isUnit_det_of_invertible A)]
+  -- Goal: coeffs * 1 = coeffs
+  rw [Matrix.vecMul_one]
+
 end AdditiveNTT

ArkLib/Data/Nat/Bitwise.lean

@@ -1203,4 +1203,48 @@ lemma getBit_of_binaryFinMapToNat {n : ℕ} (m : Fin n → ℕ) (h_binary: ∀ j
           simp only [ite_eq_right_iff, one_ne_zero, imp_false, ne_eq]
           omega
 
+/-- Middle bits: take `len` bits starting at `offset` from `n`. -/
+def getMiddleBits (offset len n : ℕ) : ℕ :=
+  getLowBits (numLowBits:=len) (n:=n >>> offset)
+
+/-- Bit-level characterization of middle bits. -/
+lemma getBit_of_middleBits {n offset len k : ℕ} :
+  getBit k (getMiddleBits offset len n) =
+    if k < len then getBit (k + offset) n else 0 := by
+  unfold getMiddleBits
+  -- use existing lemmas
+  rw [getBit_of_lowBits, getBit_of_shiftRight]
+
+/-- Middle bits are strictly less than `2^len`. -/
+lemma getMiddleBits_lt_two_pow {n offset len : ℕ} :
+  getMiddleBits offset len n < 2 ^ len := by
+  unfold getMiddleBits
+  exact getLowBits_lt_two_pow (n := n >>> offset) len
+
+/-- Middle bits as a modulus form. -/
+lemma getMiddleBits_eq_mod {n offset len : ℕ} :
+  getMiddleBits offset len n = (n >>> offset) % (2 ^ len) := by
+  unfold getMiddleBits
+  exact getLowBits_eq_mod_two_pow (n := n >>> offset) (numLowBits := len)
+
+/-- Concatenate high (length m) and low (length n) using shifts. -/
+def joinBits {n m : ℕ} (low : Fin (2 ^ n)) (high : Fin (2 ^ m)) : Fin (2 ^ (m+n)) :=
+  ⟨(high.val <<< n) ||| low.val, by sorry⟩
+
+/-- Low n bits of joinBits are exactly low. -/
+lemma getLowBits_joinBits {n m : ℕ} (low : Fin (2 ^ n)) (high : Fin (2 ^ m)) :
+  getLowBits n (joinBits low high).val = low.val := by
+  sorry
+
+/-- Dropping low n bits by shifting right recovers high. -/
+lemma getHighBits_no_shl_joinBits {n m : ℕ} (low : Fin (2 ^ n)) (high : Fin (2 ^ m)) :
+  getHighBits_no_shl n (joinBits low high).val = high.val := by
+  sorry
+
+/-- Bit characterization: below cut use low, above cut use high. -/
+lemma getBit_joinBits {n m k : ℕ} (low : Fin (2 ^ n)) (high : Fin (2 ^ m)) :
+  getBit k (joinBits low high).val =
+    if k < n then getBit k low.val else getBit (k - n) high.val := by
+  sorry
+
 end Nat