From c347e6d423e6700aa6ffd4775db03e40de56acf8 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 31 Oct 2026 06:57:41 +0000 Subject: [PATCH 1/3] refactor(PolyTime): replace remaining projection chains across PolyTime modules (#1764) --- .../CNF/BranchedSparseCNFCounter.lean | 53 +++++++++------- .../PolyTime/CNF/SparseCNFLeafCounter.lean | 5 +- .../PolyTime/CNF/SparsePolyCompile.lean | 14 +++-- .../Computability/PolyTime/Int/Jet.lean | 25 +++++--- .../Computability/PolyTime/Int/Table.lean | 5 +- .../Computability/PolyTime/JetArray.lean | 60 ++++++++++++++----- .../LinearAlgebra/BooleanMeasurements.lean | 3 +- .../ReplacementDesignBuilder.lean | 14 +++-- .../PolyTime/ParityFactorEval.lean | 19 ++++-- 9 files changed, 134 insertions(+), 64 deletions(-) diff --git a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean b/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean index 100ae21c74..139f31c20b 100644 --- a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean +++ b/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 cN := x.1; let N := cN.2; let B := leafDensityRatio k N; let ψ := x.2 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 cN := x.1 + branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch branchEval x ≤ 2 ^ cN.2 := by unfold branchedSparseCNFDeclaredCounter; dsimp only; split_ifs · rw [countCNFExhaustive_eq_modelCountOn_range, CNF.modelCountOn] refine (Finset.card_filter_le _ _).trans ?_ @@ -311,7 +312,9 @@ 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 inp => + let nk := inp.1; let t := inp.2; let b := t.2 + countSystemExhaustive (nk.1, b.2)) ((c, N), ψ) = ψ.modelCountOn (Finset.range N) := branchedSparseCNFDeclaredCounter_eq_modelCountOn (fun n' eqs' _ => countSystemExhaustive_eq_rootCount n' eqs') c N ψ hw hsub @@ -322,7 +325,9 @@ 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 inp => + let nk := inp.1; let t := inp.2; let b := t.2 + countSystemExhaustive (nk.1, b.2)) ((c, N), ψ) = ψ.modelCount := branchedSparseCNFLeafCounter_eq_modelCount (fun n' eqs' _ => countSystemExhaustive_eq_rootCount n' eqs') c N ψ hw hsub @@ -988,15 +993,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 cN := x.1 + x.2.length ≤ leafOccBound k cN.2 * cN.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 cN.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 cN.2) := 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 +1163,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 cN := x.1 + x.2.length ≤ leafOccBound k cN.2 * cN.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 cN.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 cN.2) := 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 diff --git a/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean b/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean index e5cd7f1798..7f7c78bd9e 100644 --- a/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean +++ b/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 diff --git a/Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean b/Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean index 5a7c62acd5..aae519efb2 100644 --- a/Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean +++ b/Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean @@ -1222,7 +1222,9 @@ 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 p : (ℕ × ℕ) × List (List (List ℕ)) => + let nb := p.1 + findHeavyVar nb.1 nb.2 p.2) (encPair (encPair encUnary encNat) encSys) (encOption encNat) := by have hdeg := computableInPolyTime_varDegree have hrange : ComputableInPolyTime @@ -1250,9 +1252,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) + (fun p : (ℕ × Bool) × List (List ℕ) => + let vval := p.1 + restrictEquation vval.1 vval.2 p.2) (encPair (encPair encNat encBool) encEq) encEq := by - unfold restrictEquation; fun_prop + unfold restrictEquation; dsimp only; fun_prop @[fun_prop] theorem computableInPolyTime_restrictEquation_apply {α : Type} {encIn : α ↪ List Bool} @@ -1267,7 +1271,9 @@ 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 p : (ℕ × Bool) × List (List (List ℕ)) => + let vval := p.1 + restrictSystem vval.1 vval.2 p.2) (encPair (encPair encNat encBool) encSys) encSys := mapWithInput (snd (encPair encNat encBool) encSys) (computableInPolyTime_restrictEquation.comp (((fst _ _).fst').prod (snd _ _))) diff --git a/Complexity/Computability/PolyTime/Int/Jet.lean b/Complexity/Computability/PolyTime/Int/Jet.lean index 56a47d1e23..975a34f439 100644 --- a/Complexity/Computability/PolyTime/Int/Jet.lean +++ b/Complexity/Computability/PolyTime/Int/Jet.lean @@ -274,8 +274,11 @@ 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 p : (ℕ × List ℤ) × List ℤ => + let ja := p.1 + add ja.1 ja.2 p.2) + (encPair (encPair encUnary encJet) encJet) encJet := by dsimp only; fun_prop @[fun_prop] theorem computableInPolyTime_sub' {γ : Type} {encIn : γ ↪ List Bool} {J : γ → ℕ} {a b : γ → List ℤ} (hJ : ComputableInPolyTime J encIn encUnary) @@ -288,8 +291,11 @@ 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 p : (ℕ × List ℤ) × List ℤ => + let ja := p.1 + sub ja.1 ja.2 p.2) + (encPair (encPair encUnary encJet) encJet) encJet := by dsimp only; fun_prop @[fun_prop] theorem computableInPolyTime_subConst' {γ : Type} {encIn : γ ↪ List Bool} {J : γ → ℕ} {c : γ → ℤ} {a : γ → List ℤ} (hJ : ComputableInPolyTime J encIn encUnary) @@ -299,8 +305,11 @@ 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 p : (ℕ × ℤ) × List ℤ => + let jc := p.1 + subConst jc.1 jc.2 p.2) + (encPair (encPair encUnary encIntBin) encJet) encJet := by dsimp only; fun_prop /-- 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 +320,9 @@ 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 q : ((ℕ × ℤ) × List ℤ) × α => + let pacc := q.1; let par := pacc.1 + factor par.1 par.2 q.2) (encPair (encPair (encPair encUnary encIntBin) encJet) encA) encJet) {K : γ → ℕ} (hK : PolyBounded (fun x => (encIn x).length) K) (hsz : ∀ x, ∀ a ∈ xs x, diff --git a/Complexity/Computability/PolyTime/Int/Table.lean b/Complexity/Computability/PolyTime/Int/Table.lean index 6c76fc53e9..b6b2f6ea9e 100644 --- a/Complexity/Computability/PolyTime/Int/Table.lean +++ b/Complexity/Computability/PolyTime/Int/Table.lean @@ -180,7 +180,10 @@ in polynomial time. -/ 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 : (α × ℕ) × ℕ => + let xi := p.1 + g xi.1 xi.2 p.2) (encPair (encPair encIn encUnary) encUnary) encIntBin) : ComputableInPolyTime (fun x => tabulateTable (r x) (c x) (g x)) encIn (encList (encList encIntBin)) := diff --git a/Complexity/Computability/PolyTime/JetArray.lean b/Complexity/Computability/PolyTime/JetArray.lean index 4c9cb52f7f..8ca7fce16f 100644 --- a/Complexity/Computability/PolyTime/JetArray.lean +++ b/Complexity/Computability/PolyTime/JetArray.lean @@ -918,54 +918,82 @@ theorem zeroJet_polytime : /-- Direct polynomial-time certificate for `constJet`. -/ theorem constJet_polytime : - ComputableInPolyTime (fun p : (ℕ × ℕ) × ℤ => constJet p.1.1 p.1.2 p.2) - (encPair (encPair encUnary encUnary) encIntBin) (encList (encList encIntBin)) := by fun_prop + ComputableInPolyTime + (fun p : (ℕ × ℕ) × ℤ => + let dims := p.1 + constJet dims.1 dims.2 p.2) + (encPair (encPair encUnary encUnary) encIntBin) (encList (encList encIntBin)) := by + dsimp only; fun_prop /-- Direct polynomial-time certificate for `addJet`. -/ theorem addJet_polytime : ComputableInPolyTime - (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => addJet p.1.1.1 p.1.1.2 p.1.2 p.2) + (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => + let da := p.1; let dims := da.1 + addJet dims.1 dims.2 da.2 p.2) (encPair (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin))) (encList (encList encIntBin)) := by fun_prop + (encList (encList encIntBin))) (encList (encList encIntBin)) := by + dsimp only; fun_prop /-- Direct polynomial-time certificate for `negJet`. -/ theorem negJet_polytime : - ComputableInPolyTime (fun p : (ℕ × ℕ) × List (List ℤ) => negJet p.1.1 p.1.2 p.2) + ComputableInPolyTime + (fun p : (ℕ × ℕ) × List (List ℤ) => + let dims := p.1 + negJet dims.1 dims.2 p.2) (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin)) := by fun_prop + (encList (encList encIntBin)) := by + dsimp only; fun_prop /-- Direct polynomial-time certificate for `subJet`. -/ theorem subJet_polytime : ComputableInPolyTime - (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => subJet p.1.1.1 p.1.1.2 p.1.2 p.2) + (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => + let da := p.1; let dims := da.1 + subJet dims.1 dims.2 da.2 p.2) (encPair (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin))) (encList (encList encIntBin)) := by fun_prop + (encList (encList encIntBin))) (encList (encList encIntBin)) := by + dsimp only; fun_prop /-- Direct polynomial-time certificate for `smulJet`. -/ theorem smulJet_polytime : ComputableInPolyTime - (fun p : ((ℕ × ℕ) × ℤ) × List (List ℤ) => smulJet p.1.1.1 p.1.1.2 p.1.2 p.2) + (fun p : ((ℕ × ℕ) × ℤ) × List (List ℤ) => + let dc := p.1; let dims := dc.1 + smulJet dims.1 dims.2 dc.2 p.2) (encPair (encPair (encPair encUnary encUnary) encIntBin) (encList (encList encIntBin))) - (encList (encList encIntBin)) := by fun_prop + (encList (encList encIntBin)) := by + dsimp only; fun_prop /-- Direct polynomial-time certificate for `shiftZJet`. -/ theorem shiftZJet_polytime : - ComputableInPolyTime (fun p : (ℕ × ℕ) × List (List ℤ) => shiftZJet p.1.1 p.1.2 p.2) + ComputableInPolyTime + (fun p : (ℕ × ℕ) × List (List ℤ) => + let dims := p.1 + shiftZJet dims.1 dims.2 p.2) (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin)) := by fun_prop + (encList (encList encIntBin)) := by + dsimp only; fun_prop /-- Direct polynomial-time certificate for `shiftVJet`. -/ theorem shiftVJet_polytime : - ComputableInPolyTime (fun p : (ℕ × ℕ) × List (List ℤ) => shiftVJet p.1.1 p.1.2 p.2) + ComputableInPolyTime + (fun p : (ℕ × ℕ) × List (List ℤ) => + let dims := p.1 + shiftVJet dims.1 dims.2 p.2) (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin)) := by fun_prop + (encList (encList encIntBin)) := by + dsimp only; fun_prop /-- Direct polynomial-time certificate for `convJet`. -/ theorem convJet_polytime : ComputableInPolyTime - (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => convJet p.1.1.1 p.1.1.2 p.1.2 p.2) + (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => + let da := p.1; let dims := da.1 + convJet dims.1 dims.2 da.2 p.2) (encPair (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin))) (encList (encList encIntBin)) := by fun_prop + (encList (encList encIntBin))) (encList (encList encIntBin)) := by + dsimp only; fun_prop end PolyTime diff --git a/Complexity/Computability/PolyTime/LinearAlgebra/BooleanMeasurements.lean b/Complexity/Computability/PolyTime/LinearAlgebra/BooleanMeasurements.lean index cfd6309382..f96d6cfd86 100644 --- a/Complexity/Computability/PolyTime/LinearAlgebra/BooleanMeasurements.lean +++ b/Complexity/Computability/PolyTime/LinearAlgebra/BooleanMeasurements.lean @@ -284,9 +284,10 @@ noncomputable def searchCertificate {encC : C ↪ List Bool} (ht : ComputableInPolyTime targetOf encC (encList encIntBin)) : NativeCertificate (search matOf targetOf) (encPair encC encUnary) (encOption encBits) := let h := exists_computableInO_search hM ht + let hspec := h.choose_spec.choose_spec.2 { time := fun p => (2 ^ p.2 + 1) * h.choose p space := h.choose_spec.choose - computes := h.choose_spec.choose_spec.2.2 } + computes := hspec.2 } /-- The exported certificate's actual charged workspace is polynomial in the full input. -/ theorem polyBounded_searchCertificate_space {encC : C ↪ List Bool} diff --git a/Complexity/Computability/PolyTime/LinearAlgebra/ReplacementDesignBuilder.lean b/Complexity/Computability/PolyTime/LinearAlgebra/ReplacementDesignBuilder.lean index d42c1b4b83..555ff294f6 100644 --- a/Complexity/Computability/PolyTime/LinearAlgebra/ReplacementDesignBuilder.lean +++ b/Complexity/Computability/PolyTime/LinearAlgebra/ReplacementDesignBuilder.lean @@ -220,10 +220,11 @@ def finToScopeIncidence (n_free : ℕ) (scopes : List (List ℕ)) (i : Fin (scopeIncidencesList n_free scopes).length) : ScopeIncidence (listScopeFamily n_free scopes) := have hm := mem_scopeIncidencesList.mp (List.getElem_mem i.2) + have hmv := hm.2 ⟨⟨(scopeIncidencesList n_free scopes)[i.1].1, hm.1⟩, - ⟨⟨(scopeIncidencesList n_free scopes)[i.1].2, hm.2.1⟩, by + ⟨⟨(scopeIncidencesList n_free scopes)[i.1].2, hmv.1⟩, by rw [mem_listScopeFamily] - simpa only [Fin.getElem_fin, List.getD_eq_getElem _ _ hm.1] using hm.2.2⟩⟩ + simpa only [Fin.getElem_fin, List.getD_eq_getElem _ _ hm.1] using hmv.2⟩⟩ theorem bijective_finToScopeIncidence (n_free : ℕ) (scopes : List (List ℕ)) : Function.Bijective (finToScopeIncidence n_free scopes) := by @@ -524,9 +525,12 @@ def ReplacementDesignData.equivTuple : ReplacementDesignData ≃ ReplacementDesi (d.copyCount, d.placements, d.measurementMatrix), (d.groupMeasurementMatrices, d.denom, d.replacementRows)) invFun t := - { varGroups := t.1.1, factorGroups := t.1.2.1, incidences := t.1.2.2, - copyCount := t.2.1.1, placements := t.2.1.2.1, measurementMatrix := t.2.1.2.2, - groupMeasurementMatrices := t.2.2.1, denom := t.2.2.2.1, replacementRows := t.2.2.2.2 } + let g1 := t.1; let g12 := g1.2 + let g2 := t.2; let g21 := g2.1; let g212 := g21.2 + let g22 := g2.2; let g222 := g22.2 + { varGroups := g1.1, factorGroups := g12.1, incidences := g12.2, + copyCount := g21.1, placements := g212.1, measurementMatrix := g212.2, + groupMeasurementMatrices := g22.1, denom := g222.1, replacementRows := g222.2 } left_inv d := by cases d; rfl right_inv _ := rfl diff --git a/Complexity/Computability/PolyTime/ParityFactorEval.lean b/Complexity/Computability/PolyTime/ParityFactorEval.lean index c2b9cdde7f..add42a785b 100644 --- a/Complexity/Computability/PolyTime/ParityFactorEval.lean +++ b/Complexity/Computability/PolyTime/ParityFactorEval.lean @@ -136,7 +136,8 @@ def polyMul (p q : List ℤ) : List ℤ := mulZJet (p.length + q.length) p q /-- Single Horner-division step for monic division by $Y^2 - Y$. -/ def ParityFactorEval.divModByHStep (state : List ℤ × (ℤ × ℤ)) (c : ℤ) : List ℤ × (ℤ × ℤ) := - (state.2.2 :: state.1, (c, state.2.1 + state.2.2)) + let ab := state.2 + (ab.2 :: state.1, (c, ab.1 + ab.2)) /-- Monic division of `p` by $h(Y) = Y^2 - Y$ with linear remainder `(a, b)`. -/ def divModByH (p : List ℤ) : List ℤ × (ℤ × ℤ) := @@ -231,9 +232,10 @@ theorem polyNorm1_polyMul_le (p q : List ℤ) : /-- Polynomial division identity for `divModByH` dividing by $X^2 - X$. -/ theorem ofCoeffList_divModByH (p : List ℤ) : + let rem := (divModByH p).2 ofCoeffList p = ofCoeffList (divModByH p).1 * (X ^ 2 - X) + - (C (divModByH p).2.1 + C (divModByH p).2.2 * X) := by + (C rem.1 + C rem.2 * X) := by induction p with | nil => simp only [divModByH, List.reverse_nil, List.foldl_nil, ofCoeffList_nil, zero_mul, map_zero, add_zero] @@ -269,7 +271,8 @@ private lemma foldl_divModByHStep_bounds (w : List ℤ) : /-- Linear remainder magnitude bound for `divModByH` ([OpenAI2026ETH], Lemma B.1). -/ theorem natAbs_divModByH_snd_le (p : List ℤ) : - (divModByH p).2.1.natAbs ≤ polyNorm1 p ∧ (divModByH p).2.2.natAbs ≤ polyNorm1 p := by + let rem := (divModByH p).2 + rem.1.natAbs ≤ polyNorm1 p ∧ rem.2.natAbs ≤ polyNorm1 p := by have h := (foldl_divModByHStep_bounds p.reverse).2.1; rw [polyNorm1_reverse] at h change (divModByH p).2.1.natAbs + (divModByH p).2.2.natAbs ≤ polyNorm1 p at h; omega @@ -283,8 +286,9 @@ theorem polyNorm1_divModByH_fst_le (p : List ℤ) : /-- `divModByH` computes the exact monic quotient and remainder on division by `Polynomial.hPoly = X ^ 2 - X`. -/ theorem divByMonic_and_modByMonic_hPoly_ofCoeffList (p : List ℤ) : + let rem := (divModByH p).2 ofCoeffList p /ₘ hPoly = ofCoeffList (divModByH p).1 ∧ - ofCoeffList p %ₘ hPoly = C (divModByH p).2.1 + C (divModByH p).2.2 * X := by + ofCoeffList p %ₘ hPoly = C rem.1 + C rem.2 * X := by refine div_modByMonic_unique _ _ monic_hPoly ⟨?_, ?_⟩ · rw [hPoly, ofCoeffList_divModByH p]; ring · have hr : C (divModByH p).2.1 + C (divModByH p).2.2 * X = @@ -1341,9 +1345,12 @@ private theorem parityFactorCols_polytime {J ℓ : α → ℕ} {Δ : α → ℤ} and binary $(\Delta, \text{yJet})$. -/ theorem evalParityFactorJet_polytime : ComputableInPolyTime - (fun p : (ℕ × ℕ) × (ℤ × List ℤ) => evalParityFactorJet p.1.1 p.1.2 p.2.1 p.2.2) + (fun p : (ℕ × ℕ) × (ℤ × List ℤ) => + let dims := p.1; let dy := p.2 + evalParityFactorJet dims.1 dims.2 dy.1 dy.2) (encPair (encPair encUnary encUnary) (encPair encIntBin (encList encIntBin))) - (encList (encList encIntBin)) := by fun_prop + (encList (encList encIntBin)) := by + dsimp only; fun_prop end PolyTime From addb33a8088c35327f85ae9ea7c81f53dd39522a Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 31 Oct 2026 13:05:49 +0000 Subject: [PATCH 2/3] Refactor intermediate projection lets to direct pattern matching and accessors (#1764) --- .../CNF/BranchedSparseCNFCounter.lean | 30 +++--- .../PolyTime/CNF/SparsePolyCompile.lean | 28 +++--- .../Computability/PolyTime/Int/Jet.lean | 30 +++--- .../Computability/PolyTime/Int/Table.lean | 19 +++- .../Computability/PolyTime/JetArray.lean | 95 +++++++++++-------- .../LinearAlgebra/BooleanMeasurements.lean | 3 +- .../ReplacementDesignBuilder.lean | 18 ++-- .../PolyTime/ParityFactorEval.lean | 12 ++- 8 files changed, 131 insertions(+), 104 deletions(-) diff --git a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean b/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean index 139f31c20b..a343a0a4be 100644 --- a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean +++ b/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 cN := x.1; let N := cN.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,8 +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 ℕ) : - let cN := x.1 - branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch branchEval x ≤ 2 ^ cN.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 ?_ @@ -312,9 +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 => - let nk := inp.1; let t := inp.2; let b := t.2 - countSystemExhaustive (nk.1, b.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 @@ -325,9 +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 => - let nk := inp.1; let t := inp.2; let b := t.2 - countSystemExhaustive (nk.1, b.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 @@ -994,16 +990,16 @@ theorem exists_threshold_branchedSparseCNF_time_bound (k N₀_top N₀_branch : ∃ N_min : ℕ, 16384 ≤ N_min ∧ ∀ N₀_leaf : ℕ, N_min ≤ N₀_leaf → ∃ C_t d_t A_t : ℕ, 1 ≤ A_t ∧ ∀ x : (Unit × ℕ) × CNF ℕ, - let cN := x.1 - x.2.length ≤ leafOccBound k cN.2 * cN.2 + 1 → + 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 cN.2) ∧ + (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 cN.2) := by + (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) @@ -1164,16 +1160,16 @@ theorem exists_branchedSparseCNF_time_bound (k N₀_branch : ℕ) (hbr_time : BranchPolylogTimeBound N₀_branch cBranch) : ∃ N₀_leaf N₀_top C_t d_t A_t : ℕ, 1 ≤ A_t ∧ ∀ x : (Unit × ℕ) × CNF ℕ, - let cN := x.1 - x.2.length ≤ leafOccBound k cN.2 * cN.2 + 1 → + 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 cN.2) ∧ + (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 cN.2) := by + (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 diff --git a/Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean b/Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean index aae519efb2..e7885b62e5 100644 --- a/Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean +++ b/Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean @@ -1222,9 +1222,7 @@ theorem computableInPolyTime_varDegree : binary, result in `encOption encNat`) is polynomial-time. -/ theorem computableInPolyTime_findHeavyVar : ComputableInPolyTime - (fun p : (ℕ × ℕ) × List (List (List ℕ)) => - let nb := p.1 - findHeavyVar nb.1 nb.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 @@ -1237,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] @@ -1252,11 +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 ℕ) => - let vval := p.1 - restrictEquation vval.1 vval.2 p.2) - (encPair (encPair encNat encBool) encEq) encEq := by - unfold restrictEquation; dsimp only; 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} @@ -1271,12 +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 ℕ)) => - let vval := p.1 - restrictSystem vval.1 vval.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} diff --git a/Complexity/Computability/PolyTime/Int/Jet.lean b/Complexity/Computability/PolyTime/Int/Jet.lean index 975a34f439..d772169a39 100644 --- a/Complexity/Computability/PolyTime/Int/Jet.lean +++ b/Complexity/Computability/PolyTime/Int/Jet.lean @@ -275,10 +275,11 @@ local notation "encJet" => encList encIntBin theorem computableInPolyTime_add : ComputableInPolyTime - (fun p : (ℕ × List ℤ) × List ℤ => - let ja := p.1 - add ja.1 ja.2 p.2) - (encPair (encPair encUnary encJet) encJet) encJet := by dsimp only; fun_prop + (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) @@ -292,10 +293,11 @@ theorem computableInPolyTime_add : theorem computableInPolyTime_sub : ComputableInPolyTime - (fun p : (ℕ × List ℤ) × List ℤ => - let ja := p.1 - sub ja.1 ja.2 p.2) - (encPair (encPair encUnary encJet) encJet) encJet := by dsimp only; fun_prop + (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) @@ -306,10 +308,11 @@ theorem computableInPolyTime_sub : theorem computableInPolyTime_subConst : ComputableInPolyTime - (fun p : (ℕ × ℤ) × List ℤ => - let jc := p.1 - subConst jc.1 jc.2 p.2) - (encPair (encPair encUnary encIntBin) encJet) encJet := by dsimp only; fun_prop + (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' `ℓ₁` @@ -321,7 +324,8 @@ theorem computableInPolyTime_foldl_mulZJet {γ α : Type} {encIn : γ ↪ List B (hxs : ComputableInPolyTime xs encIn (encList encA)) (hfac : ComputableInPolyTime (fun q : ((ℕ × ℤ) × List ℤ) × α => - let pacc := q.1; let par := pacc.1 + let step := q.1 + let par := step.1 factor par.1 par.2 q.2) (encPair (encPair (encPair encUnary encIntBin) encJet) encA) encJet) {K : γ → ℕ} (hK : PolyBounded (fun x => (encIn x).length) K) diff --git a/Complexity/Computability/PolyTime/Int/Table.lean b/Complexity/Computability/PolyTime/Int/Table.lean index b6b2f6ea9e..1a08504fbd 100644 --- a/Complexity/Computability/PolyTime/Int/Table.lean +++ b/Complexity/Computability/PolyTime/Int/Table.lean @@ -174,6 +174,21 @@ 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 := (α × ℕ) × ℕ + +/-- Outer context `x` of a `TableIndex`. -/ +abbrev TableIndex.ctx (p : TableIndex α) : α := + let xi := p.1; xi.1 + +/-- Row index `i` of a `TableIndex`. -/ +abbrev TableIndex.row (p : TableIndex α) : ℕ := + let xi := p.1; xi.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] @@ -181,9 +196,7 @@ theorem computableInPolyTime_tabulateTable {r c : α → ℕ} {g : α → ℕ (hr : ComputableInPolyTime r encIn encUnary) (hc : ComputableInPolyTime c encIn encUnary) (hg : ComputableInPolyTime - (fun p : (α × ℕ) × ℕ => - let xi := p.1 - g xi.1 xi.2 p.2) + (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)) := diff --git a/Complexity/Computability/PolyTime/JetArray.lean b/Complexity/Computability/PolyTime/JetArray.lean index 8ca7fce16f..b07230990b 100644 --- a/Complexity/Computability/PolyTime/JetArray.lean +++ b/Complexity/Computability/PolyTime/JetArray.lean @@ -919,81 +919,96 @@ theorem zeroJet_polytime : /-- Direct polynomial-time certificate for `constJet`. -/ theorem constJet_polytime : ComputableInPolyTime - (fun p : (ℕ × ℕ) × ℤ => - let dims := p.1 - constJet dims.1 dims.2 p.2) - (encPair (encPair encUnary encUnary) encIntBin) (encList (encList encIntBin)) := by - dsimp only; fun_prop + (fun (((J, ℓ), c) : (ℕ × ℕ) × ℤ) => constJet J ℓ c) + (encPair (encPair encUnary encUnary) encIntBin) (encList (encList encIntBin)) := + (by fun_prop : + ComputableInPolyTime (fun p : (ℕ × ℕ) × ℤ => constJet p.1.1 p.1.2 p.2) + (encPair (encPair encUnary encUnary) encIntBin) (encList (encList encIntBin))).of_enc_eq + fun ⟨⟨_, _⟩, _⟩ => rfl /-- Direct polynomial-time certificate for `addJet`. -/ theorem addJet_polytime : ComputableInPolyTime - (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => - let da := p.1; let dims := da.1 - addJet dims.1 dims.2 da.2 p.2) + (fun ((((J, ℓ), a), b) : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ)) => addJet J ℓ a b) (encPair (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin))) (encList (encList encIntBin)) := by - dsimp only; fun_prop + (encList (encList encIntBin))) (encList (encList encIntBin)) := + (by fun_prop : + ComputableInPolyTime + (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => addJet p.1.1.1 p.1.1.2 p.1.2 p.2) + (encPair (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) + (encList (encList encIntBin))) (encList (encList encIntBin))).of_enc_eq + fun ⟨⟨⟨_, _⟩, _⟩, _⟩ => rfl /-- Direct polynomial-time certificate for `negJet`. -/ theorem negJet_polytime : ComputableInPolyTime - (fun p : (ℕ × ℕ) × List (List ℤ) => - let dims := p.1 - negJet dims.1 dims.2 p.2) + (fun (((J, ℓ), a) : (ℕ × ℕ) × List (List ℤ)) => negJet J ℓ a) + (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) + (encList (encList encIntBin)) := + (by fun_prop : + ComputableInPolyTime (fun p : (ℕ × ℕ) × List (List ℤ) => negJet p.1.1 p.1.2 p.2) (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin)) := by - dsimp only; fun_prop + (encList (encList encIntBin))).of_enc_eq fun ⟨⟨_, _⟩, _⟩ => rfl /-- Direct polynomial-time certificate for `subJet`. -/ theorem subJet_polytime : ComputableInPolyTime - (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => - let da := p.1; let dims := da.1 - subJet dims.1 dims.2 da.2 p.2) + (fun ((((J, ℓ), a), b) : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ)) => subJet J ℓ a b) (encPair (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin))) (encList (encList encIntBin)) := by - dsimp only; fun_prop + (encList (encList encIntBin))) (encList (encList encIntBin)) := + (by fun_prop : + ComputableInPolyTime + (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => subJet p.1.1.1 p.1.1.2 p.1.2 p.2) + (encPair (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) + (encList (encList encIntBin))) (encList (encList encIntBin))).of_enc_eq + fun ⟨⟨⟨_, _⟩, _⟩, _⟩ => rfl /-- Direct polynomial-time certificate for `smulJet`. -/ theorem smulJet_polytime : ComputableInPolyTime - (fun p : ((ℕ × ℕ) × ℤ) × List (List ℤ) => - let dc := p.1; let dims := dc.1 - smulJet dims.1 dims.2 dc.2 p.2) + (fun ((((J, ℓ), c), a) : ((ℕ × ℕ) × ℤ) × List (List ℤ)) => smulJet J ℓ c a) (encPair (encPair (encPair encUnary encUnary) encIntBin) (encList (encList encIntBin))) - (encList (encList encIntBin)) := by - dsimp only; fun_prop + (encList (encList encIntBin)) := + (by fun_prop : + ComputableInPolyTime + (fun p : ((ℕ × ℕ) × ℤ) × List (List ℤ) => smulJet p.1.1.1 p.1.1.2 p.1.2 p.2) + (encPair (encPair (encPair encUnary encUnary) encIntBin) (encList (encList encIntBin))) + (encList (encList encIntBin))).of_enc_eq fun ⟨⟨⟨_, _⟩, _⟩, _⟩ => rfl /-- Direct polynomial-time certificate for `shiftZJet`. -/ theorem shiftZJet_polytime : ComputableInPolyTime - (fun p : (ℕ × ℕ) × List (List ℤ) => - let dims := p.1 - shiftZJet dims.1 dims.2 p.2) + (fun (((J, ℓ), a) : (ℕ × ℕ) × List (List ℤ)) => shiftZJet J ℓ a) + (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) + (encList (encList encIntBin)) := + (by fun_prop : + ComputableInPolyTime (fun p : (ℕ × ℕ) × List (List ℤ) => shiftZJet p.1.1 p.1.2 p.2) (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin)) := by - dsimp only; fun_prop + (encList (encList encIntBin))).of_enc_eq fun ⟨⟨_, _⟩, _⟩ => rfl /-- Direct polynomial-time certificate for `shiftVJet`. -/ theorem shiftVJet_polytime : ComputableInPolyTime - (fun p : (ℕ × ℕ) × List (List ℤ) => - let dims := p.1 - shiftVJet dims.1 dims.2 p.2) + (fun (((J, ℓ), a) : (ℕ × ℕ) × List (List ℤ)) => shiftVJet J ℓ a) + (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) + (encList (encList encIntBin)) := + (by fun_prop : + ComputableInPolyTime (fun p : (ℕ × ℕ) × List (List ℤ) => shiftVJet p.1.1 p.1.2 p.2) (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin)) := by - dsimp only; fun_prop + (encList (encList encIntBin))).of_enc_eq fun ⟨⟨_, _⟩, _⟩ => rfl /-- Direct polynomial-time certificate for `convJet`. -/ theorem convJet_polytime : ComputableInPolyTime - (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => - let da := p.1; let dims := da.1 - convJet dims.1 dims.2 da.2 p.2) + (fun ((((J, ℓ), a), b) : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ)) => convJet J ℓ a b) + (encPair (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) + (encList (encList encIntBin))) (encList (encList encIntBin)) := + (by fun_prop : + ComputableInPolyTime + (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => convJet p.1.1.1 p.1.1.2 p.1.2 p.2) (encPair (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin))) (encList (encList encIntBin)) := by - dsimp only; fun_prop + (encList (encList encIntBin))) (encList (encList encIntBin))).of_enc_eq + fun ⟨⟨⟨_, _⟩, _⟩, _⟩ => rfl end PolyTime diff --git a/Complexity/Computability/PolyTime/LinearAlgebra/BooleanMeasurements.lean b/Complexity/Computability/PolyTime/LinearAlgebra/BooleanMeasurements.lean index f96d6cfd86..cfd6309382 100644 --- a/Complexity/Computability/PolyTime/LinearAlgebra/BooleanMeasurements.lean +++ b/Complexity/Computability/PolyTime/LinearAlgebra/BooleanMeasurements.lean @@ -284,10 +284,9 @@ noncomputable def searchCertificate {encC : C ↪ List Bool} (ht : ComputableInPolyTime targetOf encC (encList encIntBin)) : NativeCertificate (search matOf targetOf) (encPair encC encUnary) (encOption encBits) := let h := exists_computableInO_search hM ht - let hspec := h.choose_spec.choose_spec.2 { time := fun p => (2 ^ p.2 + 1) * h.choose p space := h.choose_spec.choose - computes := hspec.2 } + computes := h.choose_spec.choose_spec.2.2 } /-- The exported certificate's actual charged workspace is polynomial in the full input. -/ theorem polyBounded_searchCertificate_space {encC : C ↪ List Bool} diff --git a/Complexity/Computability/PolyTime/LinearAlgebra/ReplacementDesignBuilder.lean b/Complexity/Computability/PolyTime/LinearAlgebra/ReplacementDesignBuilder.lean index 555ff294f6..f141d3b6c6 100644 --- a/Complexity/Computability/PolyTime/LinearAlgebra/ReplacementDesignBuilder.lean +++ b/Complexity/Computability/PolyTime/LinearAlgebra/ReplacementDesignBuilder.lean @@ -220,11 +220,10 @@ def finToScopeIncidence (n_free : ℕ) (scopes : List (List ℕ)) (i : Fin (scopeIncidencesList n_free scopes).length) : ScopeIncidence (listScopeFamily n_free scopes) := have hm := mem_scopeIncidencesList.mp (List.getElem_mem i.2) - have hmv := hm.2 ⟨⟨(scopeIncidencesList n_free scopes)[i.1].1, hm.1⟩, - ⟨⟨(scopeIncidencesList n_free scopes)[i.1].2, hmv.1⟩, by + ⟨⟨(scopeIncidencesList n_free scopes)[i.1].2, hm.2.1⟩, by rw [mem_listScopeFamily] - simpa only [Fin.getElem_fin, List.getD_eq_getElem _ _ hm.1] using hmv.2⟩⟩ + simpa only [Fin.getElem_fin, List.getD_eq_getElem _ _ hm.1] using hm.2.2⟩⟩ theorem bijective_finToScopeIncidence (n_free : ℕ) (scopes : List (List ℕ)) : Function.Bijective (finToScopeIncidence n_free scopes) := by @@ -524,13 +523,12 @@ def ReplacementDesignData.equivTuple : ReplacementDesignData ≃ ReplacementDesi toFun d := ((d.varGroups, d.factorGroups, d.incidences), (d.copyCount, d.placements, d.measurementMatrix), (d.groupMeasurementMatrices, d.denom, d.replacementRows)) - invFun t := - let g1 := t.1; let g12 := g1.2 - let g2 := t.2; let g21 := g2.1; let g212 := g21.2 - let g22 := g2.2; let g222 := g22.2 - { varGroups := g1.1, factorGroups := g12.1, incidences := g12.2, - copyCount := g21.1, placements := g212.1, measurementMatrix := g212.2, - groupMeasurementMatrices := g22.1, denom := g222.1, replacementRows := g222.2 } + invFun := fun ((varGroups, factorGroups, incidences), + (copyCount, placements, measurementMatrix), + (groupMeasurementMatrices, denom, replacementRows)) => + { varGroups, factorGroups, incidences, + copyCount, placements, measurementMatrix, + groupMeasurementMatrices, denom, replacementRows } left_inv d := by cases d; rfl right_inv _ := rfl diff --git a/Complexity/Computability/PolyTime/ParityFactorEval.lean b/Complexity/Computability/PolyTime/ParityFactorEval.lean index add42a785b..3935ba02c5 100644 --- a/Complexity/Computability/PolyTime/ParityFactorEval.lean +++ b/Complexity/Computability/PolyTime/ParityFactorEval.lean @@ -1345,12 +1345,14 @@ private theorem parityFactorCols_polytime {J ℓ : α → ℕ} {Δ : α → ℤ} and binary $(\Delta, \text{yJet})$. -/ theorem evalParityFactorJet_polytime : ComputableInPolyTime - (fun p : (ℕ × ℕ) × (ℤ × List ℤ) => - let dims := p.1; let dy := p.2 - evalParityFactorJet dims.1 dims.2 dy.1 dy.2) + (fun (((J, ℓ), (Δ, yJet)) : (ℕ × ℕ) × (ℤ × List ℤ)) => evalParityFactorJet J ℓ Δ yJet) (encPair (encPair encUnary encUnary) (encPair encIntBin (encList encIntBin))) - (encList (encList encIntBin)) := by - dsimp only; fun_prop + (encList (encList encIntBin)) := + (by fun_prop : + ComputableInPolyTime + (fun p : (ℕ × ℕ) × (ℤ × List ℤ) => evalParityFactorJet p.1.1 p.1.2 p.2.1 p.2.2) + (encPair (encPair encUnary encUnary) (encPair encIntBin (encList encIntBin))) + (encList (encList encIntBin))).of_enc_eq fun ⟨⟨_, _⟩, _, _⟩ => rfl end PolyTime From 716043b6e5d11a4b5a9c3412df92e2dba631dddf Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 31 Oct 2026 16:08:26 +0000 Subject: [PATCH 3/3] refactor(PolyTime/Int): address delta review on computableInPolyTime_foldl_mulZJet and TableIndex --- .../Computability/PolyTime/Int/Jet.lean | 8 +++---- .../Computability/PolyTime/Int/Table.lean | 9 +++---- .../Computability/PolyTime/JetArray.lean | 24 +++++++------------ .../PolyTime/ParityFactorEval.lean | 3 +-- 4 files changed, 17 insertions(+), 27 deletions(-) diff --git a/Complexity/Computability/PolyTime/Int/Jet.lean b/Complexity/Computability/PolyTime/Int/Jet.lean index d772169a39..8d2710a84d 100644 --- a/Complexity/Computability/PolyTime/Int/Jet.lean +++ b/Complexity/Computability/PolyTime/Int/Jet.lean @@ -323,10 +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 ℤ) × α => - let step := q.1 - let par := step.1 - factor par.1 par.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, @@ -340,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)) diff --git a/Complexity/Computability/PolyTime/Int/Table.lean b/Complexity/Computability/PolyTime/Int/Table.lean index 1a08504fbd..2366285cab 100644 --- a/Complexity/Computability/PolyTime/Int/Table.lean +++ b/Complexity/Computability/PolyTime/Int/Table.lean @@ -178,13 +178,14 @@ theorem computableInPolyTime_rowEntry {rows : α → List (List ℤ)} {i j : α 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 α) : α := - let xi := p.1; xi.1 +abbrev TableIndex.ctx (p : TableIndex α) : α := p.rowCtx.1 /-- Row index `i` of a `TableIndex`. -/ -abbrev TableIndex.row (p : TableIndex α) : ℕ := - let xi := p.1; xi.2 +abbrev TableIndex.row (p : TableIndex α) : ℕ := p.rowCtx.2 /-- Column index `j` of a `TableIndex`. -/ abbrev TableIndex.col (p : TableIndex α) : ℕ := p.2 diff --git a/Complexity/Computability/PolyTime/JetArray.lean b/Complexity/Computability/PolyTime/JetArray.lean index b07230990b..4cc7db998d 100644 --- a/Complexity/Computability/PolyTime/JetArray.lean +++ b/Complexity/Computability/PolyTime/JetArray.lean @@ -922,8 +922,7 @@ theorem constJet_polytime : (fun (((J, ℓ), c) : (ℕ × ℕ) × ℤ) => constJet J ℓ c) (encPair (encPair encUnary encUnary) encIntBin) (encList (encList encIntBin)) := (by fun_prop : - ComputableInPolyTime (fun p : (ℕ × ℕ) × ℤ => constJet p.1.1 p.1.2 p.2) - (encPair (encPair encUnary encUnary) encIntBin) (encList (encList encIntBin))).of_enc_eq + ComputableInPolyTime (fun p : (ℕ × ℕ) × ℤ => constJet p.1.1 p.1.2 p.2) _ _).of_enc_eq fun ⟨⟨_, _⟩, _⟩ => rfl /-- Direct polynomial-time certificate for `addJet`. -/ @@ -935,8 +934,7 @@ theorem addJet_polytime : (by fun_prop : ComputableInPolyTime (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => addJet p.1.1.1 p.1.1.2 p.1.2 p.2) - (encPair (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin))) (encList (encList encIntBin))).of_enc_eq + _ _).of_enc_eq fun ⟨⟨⟨_, _⟩, _⟩, _⟩ => rfl /-- Direct polynomial-time certificate for `negJet`. -/ @@ -947,8 +945,7 @@ theorem negJet_polytime : (encList (encList encIntBin)) := (by fun_prop : ComputableInPolyTime (fun p : (ℕ × ℕ) × List (List ℤ) => negJet p.1.1 p.1.2 p.2) - (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin))).of_enc_eq fun ⟨⟨_, _⟩, _⟩ => rfl + _ _).of_enc_eq fun ⟨⟨_, _⟩, _⟩ => rfl /-- Direct polynomial-time certificate for `subJet`. -/ theorem subJet_polytime : @@ -959,8 +956,7 @@ theorem subJet_polytime : (by fun_prop : ComputableInPolyTime (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => subJet p.1.1.1 p.1.1.2 p.1.2 p.2) - (encPair (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin))) (encList (encList encIntBin))).of_enc_eq + _ _).of_enc_eq fun ⟨⟨⟨_, _⟩, _⟩, _⟩ => rfl /-- Direct polynomial-time certificate for `smulJet`. -/ @@ -972,8 +968,7 @@ theorem smulJet_polytime : (by fun_prop : ComputableInPolyTime (fun p : ((ℕ × ℕ) × ℤ) × List (List ℤ) => smulJet p.1.1.1 p.1.1.2 p.1.2 p.2) - (encPair (encPair (encPair encUnary encUnary) encIntBin) (encList (encList encIntBin))) - (encList (encList encIntBin))).of_enc_eq fun ⟨⟨⟨_, _⟩, _⟩, _⟩ => rfl + _ _).of_enc_eq fun ⟨⟨⟨_, _⟩, _⟩, _⟩ => rfl /-- Direct polynomial-time certificate for `shiftZJet`. -/ theorem shiftZJet_polytime : @@ -983,8 +978,7 @@ theorem shiftZJet_polytime : (encList (encList encIntBin)) := (by fun_prop : ComputableInPolyTime (fun p : (ℕ × ℕ) × List (List ℤ) => shiftZJet p.1.1 p.1.2 p.2) - (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin))).of_enc_eq fun ⟨⟨_, _⟩, _⟩ => rfl + _ _).of_enc_eq fun ⟨⟨_, _⟩, _⟩ => rfl /-- Direct polynomial-time certificate for `shiftVJet`. -/ theorem shiftVJet_polytime : @@ -994,8 +988,7 @@ theorem shiftVJet_polytime : (encList (encList encIntBin)) := (by fun_prop : ComputableInPolyTime (fun p : (ℕ × ℕ) × List (List ℤ) => shiftVJet p.1.1 p.1.2 p.2) - (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin))).of_enc_eq fun ⟨⟨_, _⟩, _⟩ => rfl + _ _).of_enc_eq fun ⟨⟨_, _⟩, _⟩ => rfl /-- Direct polynomial-time certificate for `convJet`. -/ theorem convJet_polytime : @@ -1006,8 +999,7 @@ theorem convJet_polytime : (by fun_prop : ComputableInPolyTime (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => convJet p.1.1.1 p.1.1.2 p.1.2 p.2) - (encPair (encPair (encPair encUnary encUnary) (encList (encList encIntBin))) - (encList (encList encIntBin))) (encList (encList encIntBin))).of_enc_eq + _ _).of_enc_eq fun ⟨⟨⟨_, _⟩, _⟩, _⟩ => rfl end PolyTime diff --git a/Complexity/Computability/PolyTime/ParityFactorEval.lean b/Complexity/Computability/PolyTime/ParityFactorEval.lean index 3935ba02c5..2d33391169 100644 --- a/Complexity/Computability/PolyTime/ParityFactorEval.lean +++ b/Complexity/Computability/PolyTime/ParityFactorEval.lean @@ -1351,8 +1351,7 @@ theorem evalParityFactorJet_polytime : (by fun_prop : ComputableInPolyTime (fun p : (ℕ × ℕ) × (ℤ × List ℤ) => evalParityFactorJet p.1.1 p.1.2 p.2.1 p.2.2) - (encPair (encPair encUnary encUnary) (encPair encIntBin (encList encIntBin))) - (encList (encList encIntBin))).of_enc_eq fun ⟨⟨_, _⟩, _, _⟩ => rfl + _ _).of_enc_eq fun ⟨⟨_, _⟩, _, _⟩ => rfl end PolyTime