refactor(PolyTime): replace remaining projection chains across PolyTime modules (#1764)

Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean

@@ -112,7 +112,7 @@ formulas (`leafDensityRatio k N * N < ψ.length`, including `[[]]` at `N = 0`) t
 `sparseCNFDeclaredCounter` backed by `branchedPolyCounter`. -/
 def branchedSparseCNFDeclaredCounter (k N₀_leaf N₀_top N₀_branch : ℕ)
     (branchEval : BranchEvalInput → ℕ) (x : (Unit × ℕ) × CNF ℕ) : ℕ :=
-  let N := x.1.2; let B := leafDensityRatio k N; let ψ := x.2
+  let ((_, N), ψ) := x; let B := leafDensityRatio k N
   if validDeclaredInput k N ψ && decide (B * N < ψ.length) then countCNFExhaustive (N, ψ)
   else sparseCNFDeclaredCounter Prod.snd (fun p : Unit × ℕ => leafDensityRatio k p.2)
     k (max 1 N₀_leaf) (branchedPolyCounter k N₀_top N₀_branch branchEval) x
@@ -236,7 +236,8 @@ theorem computableInPolyTime_leafDensityRatio (k : ℕ) :
 /-- **Unconditional declared-range output cap**: `branchedSparseCNFDeclaredCounter ≤ 2 ^ x.1.2`. -/
 theorem branchedSparseCNFDeclaredCounter_le_two_pow (k N₀_leaf N₀_top N₀_branch : ℕ)
     (branchEval : BranchEvalInput → ℕ) (x : (Unit × ℕ) × CNF ℕ) :
-    branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch branchEval x ≤ 2 ^ x.1.2 := by
+    let ((_, N), _) := x
+    branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch branchEval x ≤ 2 ^ N := by
   unfold branchedSparseCNFDeclaredCounter; dsimp only; split_ifs
   · rw [countCNFExhaustive_eq_modelCountOn_range, CNF.modelCountOn]
     refine (Finset.card_filter_le _ _).trans ?_
@@ -311,7 +312,7 @@ theorem branchedSparseCNFDeclaredCounter_exhaustive_eq_modelCountOn
     (k N₀_leaf N₀_top N₀_branch : ℕ) (c : Unit) (N : ℕ) (ψ : CNF ℕ)
     (hw : ∀ cl ∈ ψ, cl.length ≤ k) (hsub : ψ.vars.toFinset ⊆ Finset.range N) :
     branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch
-        (fun inp => countSystemExhaustive (inp.1.1, inp.2.2.2)) ((c, N), ψ) =
+        (fun ((n', _), _, _, eqs') => countSystemExhaustive (n', eqs')) ((c, N), ψ) =
       ψ.modelCountOn (Finset.range N) :=
   branchedSparseCNFDeclaredCounter_eq_modelCountOn
     (fun n' eqs' _ => countSystemExhaustive_eq_rootCount n' eqs') c N ψ hw hsub
@@ -322,7 +323,7 @@ theorem branchedSparseCNFLeafCounter_exhaustive_eq_modelCount
     (k N₀_leaf N₀_top N₀_branch : ℕ) (c : Unit) (N : ℕ) (ψ : CNF ℕ)
     (hw : ∀ cl ∈ ψ, cl.length ≤ k) (hsub : ψ.vars.toFinset ⊆ Finset.range N) :
     branchedSparseCNFLeafCounter k N₀_leaf N₀_top N₀_branch
-        (fun inp => countSystemExhaustive (inp.1.1, inp.2.2.2)) ((c, N), ψ) =
+        (fun ((n', _), _, _, eqs') => countSystemExhaustive (n', eqs')) ((c, N), ψ) =
       ψ.modelCount :=
   branchedSparseCNFLeafCounter_eq_modelCount
     (fun n' eqs' _ => countSystemExhaustive_eq_rootCount n' eqs') c N ψ hw hsub
@@ -988,15 +989,17 @@ theorem exists_threshold_branchedSparseCNF_time_bound (k N₀_top N₀_branch :
     (hbr_time : BranchPolylogTimeBound N₀_branch cBranch) :
     ∃ N_min : ℕ, 16384 ≤ N_min ∧ ∀ N₀_leaf : ℕ, N_min ≤ N₀_leaf →
       ∃ C_t d_t A_t : ℕ, 1 ≤ A_t ∧
-        ∀ x : (Unit × ℕ) × CNF ℕ, x.2.length ≤ leafOccBound k x.1.2 * x.1.2 + 1 →
-          ((branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch
-              cBranch hbound).time x : ℝ) ≤
-            (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t *
-              (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) ∧
-          ((branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch
-              cBranch hbound).time x : ℝ) ≤
-            (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t *
-              (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) := by
+        ∀ x : (Unit × ℕ) × CNF ℕ,
+          let ((_, N), ψ) := x
+          ψ.length ≤ leafOccBound k N * N + 1 →
+            ((branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch
+                cBranch hbound).time x : ℝ) ≤
+              (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t *
+                (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale N) ∧
+            ((branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch
+                cBranch hbound).time x : ℝ) ≤
+              (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t *
+                (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale N) := by
   obtain ⟨N_sys, C_sys, d_sys, A_sys, hNsys16, hSysT⟩ :=
     polySys_time_bound_of_branchPolylog k N₀_top N₀_branch cBranch hbound hbr_time
   obtain ⟨C_B, hCB⟩ := exists_leafDensityRatio_le_mul_clog_pow k; set β_B := 2 * (max 2 k - 1)
@@ -1156,15 +1159,17 @@ theorem exists_branchedSparseCNF_time_bound (k N₀_branch : ℕ)
     (hs_br : PolyBounded (fun x => (encBranchEvalInput x).length) cBranch.space)
     (hbr_time : BranchPolylogTimeBound N₀_branch cBranch) :
     ∃ N₀_leaf N₀_top C_t d_t A_t : ℕ, 1 ≤ A_t ∧
-      ∀ x : (Unit × ℕ) × CNF ℕ, x.2.length ≤ leafOccBound k x.1.2 * x.1.2 + 1 →
-        ((branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch
-            cBranch hbound).time x : ℝ) ≤
-          (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t *
-            (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) ∧
-        ((branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch
-            cBranch hbound).time x : ℝ) ≤
-          (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t *
-            (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) := by
+      ∀ x : (Unit × ℕ) × CNF ℕ,
+        let ((_, N), ψ) := x
+        ψ.length ≤ leafOccBound k N * N + 1 →
+          ((branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch
+              cBranch hbound).time x : ℝ) ≤
+            (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t *
+              (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale N) ∧
+          ((branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch
+              cBranch hbound).time x : ℝ) ≤
+            (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t *
+              (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale N) := by
   obtain ⟨N_min, _, hBound⟩ :=
     exists_threshold_branchedSparseCNF_time_bound k 0 N₀_branch cBranch hbound hs_br hbr_time
   obtain ⟨C_t, d_t, A_t, hA, hT⟩ := hBound N_min le_rfl

Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean

@@ -93,8 +93,9 @@ def IsCompiledSparseSystem (k N maxEqs maxTerms : ℕ) (sys : List (List (List 
 /-- Evaluates `polyCounter (N, compileParitySystemBounded k ψ rows)` when `rows.length ≤ 6 * N`. -/
 def compiledRowCounter (k : ℕ) (polyCounter : ℕ × List (List (List ℕ)) → ℕ)
     (q : (ℕ × CNF ℕ) × List (List Bool)) : ℕ :=
-  if decide (q.2.length ≤ 6 * q.1.1) then
-    polyCounter (q.1.1, compileParitySystemBounded k q.1.2 q.2)
+  let nψ := q.1
+  if decide (q.2.length ≤ 6 * nψ.1) then
+    polyCounter (nψ.1, compileParitySystemBounded k nψ.2 q.2)
   else 0
 
 /-- Deterministic Section 6.3 fast path: initial Tanner rows via `initialTestsRows`, `3 * N` rounds

Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean

@@ -1222,7 +1222,7 @@ theorem computableInPolyTime_varDegree :
 binary, result in `encOption encNat`) is polynomial-time. -/
 theorem computableInPolyTime_findHeavyVar :
     ComputableInPolyTime
-      (fun p : (ℕ × ℕ) × List (List (List ℕ)) => findHeavyVar p.1.1 p.1.2 p.2)
+      (fun (((n, b), sys) : (ℕ × ℕ) × List (List (List ℕ))) => findHeavyVar n b sys)
       (encPair (encPair encUnary encNat) encSys) (encOption encNat) := by
   have hdeg := computableInPolyTime_varDegree
   have hrange : ComputableInPolyTime
@@ -1235,7 +1235,7 @@ theorem computableInPolyTime_findHeavyVar :
     binary_lt' ((fst _ _).fst'.snd')
       (unary_to_binary.comp (hdeg.comp ((snd _ _).prod ((fst _ _).snd'))))
   have hfind := findWithInput (test := fun x v => decide (x.1.2 < varDegree v x.2)) hrange hpred
-  refine hfind.of_enc_eq fun p => congrArg (encOption encNat) ?_
+  refine hfind.of_enc_eq fun ⟨⟨_, _⟩, _⟩ => congrArg (encOption encNat) ?_
   rw [List.map_id']; rfl
 
 @[fun_prop]
@@ -1250,9 +1250,11 @@ theorem computableInPolyTime_findHeavyVar_apply {α : Type} {encIn : α ↪ List
 /-- Substituting `x_v = val` into a sparse `𝔽₂` equation (`restrictEquation`) is polynomial-time. -/
 theorem computableInPolyTime_restrictEquation :
     ComputableInPolyTime
-      (fun p : (ℕ × Bool) × List (List ℕ) => restrictEquation p.1.1 p.1.2 p.2)
-      (encPair (encPair encNat encBool) encEq) encEq := by
-  unfold restrictEquation; fun_prop
+      (fun (((v, val), eq) : (ℕ × Bool) × List (List ℕ)) => restrictEquation v val eq)
+      (encPair (encPair encNat encBool) encEq) encEq :=
+  (by unfold restrictEquation; fun_prop :
+    ComputableInPolyTime (fun p : (ℕ × Bool) × List (List ℕ) => restrictEquation p.1.1 p.1.2 p.2)
+      (encPair (encPair encNat encBool) encEq) encEq).of_enc_eq fun ⟨⟨_, _⟩, _⟩ => rfl
 
 @[fun_prop]
 theorem computableInPolyTime_restrictEquation_apply {α : Type} {encIn : α ↪ List Bool}
@@ -1267,10 +1269,14 @@ theorem computableInPolyTime_restrictEquation_apply {α : Type} {encIn : α ↪
 /-- Substituting `x_v = val` across a sparse `𝔽₂` system (`restrictSystem`) is polynomial-time. -/
 theorem computableInPolyTime_restrictSystem :
     ComputableInPolyTime
-      (fun p : (ℕ × Bool) × List (List (List ℕ)) => restrictSystem p.1.1 p.1.2 p.2)
+      (fun (((v, val), sys) : (ℕ × Bool) × List (List (List ℕ))) => restrictSystem v val sys)
       (encPair (encPair encNat encBool) encSys) encSys :=
-  mapWithInput (snd (encPair encNat encBool) encSys)
-    (computableInPolyTime_restrictEquation.comp (((fst _ _).fst').prod (snd _ _)))
+  (mapWithInput
+    (f := fun x a =>
+      (fun (((v, val), eq) : (ℕ × Bool) × List (List ℕ)) => restrictEquation v val eq) (x.1, a))
+    (snd (encPair encNat encBool) encSys)
+    (computableInPolyTime_restrictEquation.comp (((fst _ _).fst').prod (snd _ _)))).of_enc_eq
+    fun ⟨⟨_, _⟩, _⟩ => rfl
 
 @[fun_prop]
 theorem computableInPolyTime_restrictSystem_apply {α : Type} {encIn : α ↪ List Bool}

Complexity/Computability/PolyTime/Int/Jet.lean

@@ -274,8 +274,12 @@ local notation "encJet" => encList encIntBin
   unfold add; fun_prop
 
 theorem computableInPolyTime_add :
-    ComputableInPolyTime (fun p : (ℕ × List ℤ) × List ℤ => add p.1.1 p.1.2 p.2)
-      (encPair (encPair encUnary encJet) encJet) encJet := by fun_prop
+    ComputableInPolyTime
+      (fun (((J, a), b) : (ℕ × List ℤ) × List ℤ) => add J a b)
+      (encPair (encPair encUnary encJet) encJet) encJet :=
+  (by fun_prop :
+    ComputableInPolyTime (fun p : (ℕ × List ℤ) × List ℤ => add p.1.1 p.1.2 p.2) _ _).of_enc_eq
+    fun ⟨⟨_, _⟩, _⟩ => rfl
 
 @[fun_prop] theorem computableInPolyTime_sub' {γ : Type} {encIn : γ ↪ List Bool}
     {J : γ → ℕ} {a b : γ → List ℤ} (hJ : ComputableInPolyTime J encIn encUnary)
@@ -288,8 +292,12 @@ theorem computableInPolyTime_add :
       (((ha.comp hx).listGetDWithInput hk 0).prod ((hb.comp hx).listGetDWithInput hk 0)))
 
 theorem computableInPolyTime_sub :
-    ComputableInPolyTime (fun p : (ℕ × List ℤ) × List ℤ => sub p.1.1 p.1.2 p.2)
-      (encPair (encPair encUnary encJet) encJet) encJet := by fun_prop
+    ComputableInPolyTime
+      (fun (((J, a), b) : (ℕ × List ℤ) × List ℤ) => sub J a b)
+      (encPair (encPair encUnary encJet) encJet) encJet :=
+  (by fun_prop :
+    ComputableInPolyTime (fun p : (ℕ × List ℤ) × List ℤ => sub p.1.1 p.1.2 p.2) _ _).of_enc_eq
+    fun ⟨⟨_, _⟩, _⟩ => rfl
 
 @[fun_prop] theorem computableInPolyTime_subConst' {γ : Type} {encIn : γ ↪ List Bool}
     {J : γ → ℕ} {c : γ → ℤ} {a : γ → List ℤ} (hJ : ComputableInPolyTime J encIn encUnary)
@@ -299,8 +307,12 @@ theorem computableInPolyTime_sub :
     ((ComputableInPolyTime.snoc encIntBin).comp ((ComputableInPolyTime.const []).prod hc)) ha
 
 theorem computableInPolyTime_subConst :
-    ComputableInPolyTime (fun p : (ℕ × ℤ) × List ℤ => subConst p.1.1 p.1.2 p.2)
-      (encPair (encPair encUnary encIntBin) encJet) encJet := by fun_prop
+    ComputableInPolyTime
+      (fun (((J, c), a) : (ℕ × ℤ) × List ℤ) => subConst J c a)
+      (encPair (encPair encUnary encIntBin) encJet) encJet :=
+  (by fun_prop :
+    ComputableInPolyTime (fun p : (ℕ × ℤ) × List ℤ => subConst p.1.1 p.1.2 p.2) _ _).of_enc_eq
+    fun ⟨⟨_, _⟩, _⟩ => rfl
 
 /-- Plain polynomial-time combinator for folding `Cslib.mulZJet` over `xs` from
 `Cslib.truncZJet J [1]`, given a polynomial bound `K` on the bit-sizes of the step factors' `ℓ₁`
@@ -311,7 +323,7 @@ theorem computableInPolyTime_foldl_mulZJet {γ α : Type} {encIn : γ ↪ List B
     (hJ : ComputableInPolyTime J encIn encUnary) (hδ : ComputableInPolyTime δ encIn encIntBin)
     (hxs : ComputableInPolyTime xs encIn (encList encA))
     (hfac : ComputableInPolyTime
-      (fun q : ((ℕ × ℤ) × List ℤ) × α => factor q.1.1.1 q.1.1.2 q.2)
+      (fun (((J, δ), _), a) => factor J δ a)
       (encPair (encPair (encPair encUnary encIntBin) encJet) encA) encJet)
     {K : γ → ℕ} (hK : PolyBounded (fun x => (encIn x).length) K)
     (hsz : ∀ x, ∀ a ∈ xs x,
@@ -325,7 +337,8 @@ theorem computableInPolyTime_foldl_mulZJet {γ α : Type} {encIn : γ ↪ List B
       (encPair (encPair (encPair encUnary encIntBin) encJet) encA) encUnary := by fun_prop
   have hqAcc : ComputableInPolyTime (fun q : ((ℕ × ℤ) × List ℤ) × α => q.1.2)
       (encPair (encPair (encPair encUnary encIntBin) encJet) encA) encJet := by fun_prop
-  have hstep := Cslib.computableInPolyTime_mulZJet hqJ hqAcc hfac
+  have hstep := Cslib.computableInPolyTime_mulZJet hqJ hqAcc
+    (hfac.of_enc_eq (g := fun q => factor q.1.1.1 q.1.1.2 q.2) fun ⟨⟨⟨_, _⟩, _⟩, _⟩ => rfl)
   refine ComputableInPolyTime.foldlWith (encA := encA)
     (par := fun x => (J x, δ x)) (list := xs) (init := fun x => Cslib.truncZJet (J x) [1])
     (step := fun par acc a => Cslib.mulZJet par.1 acc (factor par.1 par.2 a))

Complexity/Computability/PolyTime/Int/Table.lean

@@ -174,13 +174,30 @@ theorem computableInPolyTime_rowEntry {rows : α → List (List ℤ)} {i j : α
     (((ComputableInPolyTime.listGetD (encA := encList encIntBin) []).comp
       (hrows.prod hi)).prod hj))
 
+/-- Input triple `((x, i), j)` for `computableInPolyTime_tabulateTable`: outer context `x`, row
+index `i`, and column index `j`. -/
+abbrev TableIndex (α : Type) : Type := (α × ℕ) × ℕ
+
+/-- Context-and-row pair `(x, i)` of a `TableIndex`. -/
+abbrev TableIndex.rowCtx (p : TableIndex α) : α × ℕ := p.1
+
+/-- Outer context `x` of a `TableIndex`. -/
+abbrev TableIndex.ctx (p : TableIndex α) : α := p.rowCtx.1
+
+/-- Row index `i` of a `TableIndex`. -/
+abbrev TableIndex.row (p : TableIndex α) : ℕ := p.rowCtx.2
+
+/-- Column index `j` of a `TableIndex`. -/
+abbrev TableIndex.col (p : TableIndex α) : ℕ := p.2
+
 /-- Tabulating an `r × c` table of binary integers from unary dimensions `(r, c)` is computable
 in polynomial time. -/
 @[fun_prop]
 theorem computableInPolyTime_tabulateTable {r c : α → ℕ} {g : α → ℕ → ℕ → ℤ}
     (hr : ComputableInPolyTime r encIn encUnary)
     (hc : ComputableInPolyTime c encIn encUnary)
-    (hg : ComputableInPolyTime (fun p : (α × ℕ) × ℕ => g p.1.1 p.1.2 p.2)
+    (hg : ComputableInPolyTime
+      (fun p : TableIndex α => g p.ctx p.row p.col)
       (encPair (encPair encIn encUnary) encUnary) encIntBin) :
     ComputableInPolyTime (fun x => tabulateTable (r x) (c x) (g x))
       encIn (encList (encList encIntBin)) :=