From ac97d72e79c0167df57024614e222b66b610cc8e Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 02:31:45 -0400 Subject: [PATCH] refactor(classes): expose shared plain certificate for splitAlternatingBlocks --- .../Classes/BooleanHierarchy/Kadin.lean | 20 +--------- .../Complexity/Classes/PH/Closure.lean | 39 ++++++++++++------- 2 files changed, 26 insertions(+), 33 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean b/Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean index 0166a77dbf..2cfd20baea 100644 --- a/Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean +++ b/Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean @@ -121,23 +121,6 @@ private theorem computableTidilyInPolyTime_shiftVerifier (p : Polynomial ℕ) (bitsAppend (fst _ _).snd' (bitsTakeWithInput (snd _ _) hn))).prod (bitsDropWithInput (snd _ _) hn)) -private theorem computableTidilyInPolyTime_splitAlternatingBlocks' {γ : Type} - {encIn : γ ↪ List Bool} (ps : List (Polynomial ℕ × Polynomial ℕ)) {N : γ → ℕ} - (hN : ComputableTidilyInPolyTime N encIn encUnary) {W : γ → List Bool} - (hW : ComputableTidilyInPolyTime W encIn encBits) : - ComputableTidilyInPolyTime - (fun x => splitAlternatingBlocks (ps.map fun pq => (pq.1.eval (N x), pq.2.eval (N x))) - (W x)) encIn (encPair encBits encBits) := by - induction ps generalizing W with - | nil => exact .const ([], []) - | cons pq ps ih => - have hp := (ComputableTidilyInPolyTime.unary_eval pq.1).comp hN - have hq := (ComputableTidilyInPolyTime.unary_eval pq.2).comp hN - have ht := ih (hW.bitsDropWithInput (ComputableTidilyInPolyTime.unary_add.comp - (hp.prod hq))) - exact ((hW.bitsTakeWithInput hp).bitsAppend ht.fst').prod - (((hW.bitsDropWithInput hp).bitsTakeWithInput hq).bitsAppend ht.snd') - /-- `R : α → List Bool → Prop` is verified at `(b, k)` on prefixes `s` of length `q |enc a|` by a polynomial-time alternating verifier whose certificate block lengths are polynomials in `|enc a|`. -/ @@ -211,7 +194,8 @@ private theorem and (h₁ : OnSliceAlt enc b k q R₁) (h₂ : OnSliceAlt enc b (fun x : (α × List Bool) × List Bool => (enc x.1.1).length) (encPair (encPair enc encBits) encBits) encUnary := (encoding_length enc).comp (fst _ _).fst' - have hs := computableTidilyInPolyTime_splitAlternatingBlocks' pqs hn (snd _ _) + have hs := (computableInPolyTime_splitAlternatingBlocks pqs + hn.computableInPolyTime (snd _ _).computableInPolyTime).tidy exact .of_tidy <| (hV.tidy.comp ((fst _ _).prod hs.fst')).bool_and' (hW.tidy.comp ((fst _ _).prod hs.snd')) diff --git a/Complexity/Computability/Complexity/Classes/PH/Closure.lean b/Complexity/Computability/Complexity/Classes/PH/Closure.lean index ced794ad0c..9f01e162dd 100644 --- a/Complexity/Computability/Complexity/Classes/PH/Closure.lean +++ b/Complexity/Computability/Complexity/Classes/PH/Closure.lean @@ -25,6 +25,8 @@ The construction uses exact certificate lengths and polynomial-time bit-string s ## Main results +* `computableInPolyTime_splitAlternatingBlocks`: polynomial-time certificate for splitting paired + certificate blocks. * `inter_mem_SigmaP`, `union_mem_SigmaP`: closure of each existential level. * `inter_mem_PiP`, `union_mem_PiP`: closure of each universal level. * `compl_mem_PH`, `inter_mem_PH`, `union_mem_PH`, `diff_mem_PH`: Boolean closure of the hierarchy. @@ -104,22 +106,29 @@ theorem alternation_splitAlternatingBlocks (ns : List (ℕ × ℕ)) (q : Bool) /-- Splitting paired blocks is polynomial-time when their lengths are fixed polynomials of a computed unary size. -/ -private theorem computableTidilyInPolyTime_splitAlternatingBlocks {γ : Type} +theorem computableInPolyTime_splitAlternatingBlocks {γ : Type} {encIn : γ ↪ List Bool} (ps : List (Polynomial ℕ × Polynomial ℕ)) {N : γ → ℕ} - (hN : ComputableTidilyInPolyTime N encIn encUnary) {W : γ → List Bool} - (hW : ComputableTidilyInPolyTime W encIn encBits) : - ComputableTidilyInPolyTime + (hN : ComputableInPolyTime N encIn encUnary) {W : γ → List Bool} + (hW : ComputableInPolyTime W encIn encBits) : + ComputableInPolyTime (fun x => splitAlternatingBlocks (ps.map fun pq => (pq.1.eval (N x), pq.2.eval (N x))) (W x)) encIn (encPair encBits encBits) := by - induction ps generalizing W with - | nil => exact .const ([], []) - | cons pq ps ih => - have hp := (ComputableTidilyInPolyTime.unary_eval pq.1).comp hN - have hq := (ComputableTidilyInPolyTime.unary_eval pq.2).comp hN - have ht := ih (hW.bitsDropWithInput (ComputableTidilyInPolyTime.unary_add.comp - (hp.prod hq))) - exact ((hW.bitsTakeWithInput hp).bitsAppend ht.fst').prod - (((hW.bitsDropWithInput hp).bitsTakeWithInput hq).bitsAppend ht.snd') + have key : ∀ {W : γ → List Bool}, + ComputableTidilyInPolyTime W encIn encBits → + ComputableTidilyInPolyTime + (fun x => splitAlternatingBlocks (ps.map fun pq => (pq.1.eval (N x), pq.2.eval (N x))) + (W x)) encIn (encPair encBits encBits) := by + induction ps with + | nil => intro _ _; exact .const ([], []) + | cons pq ps ih => + intro W hW + have hp := (ComputableTidilyInPolyTime.unary_eval pq.1).comp hN.tidy + have hq := (ComputableTidilyInPolyTime.unary_eval pq.2).comp hN.tidy + have ht := ih (hW.bitsDropWithInput (ComputableTidilyInPolyTime.unary_add.comp + (hp.prod hq))) + exact ((hW.bitsTakeWithInput hp).bitsAppend ht.fst').prod + (((hW.bitsDropWithInput hp).bitsTakeWithInput hq).bitsAppend ht.snd') + exact .of_tidy (key hW.tidy) variable {α : Type} {enc : α ↪ List Bool} @@ -161,8 +170,8 @@ private theorem exists_inter_verifier {q : Bool} {k : ℕ} {A B : Set α} · simp [hp, hq] · have hn : ComputableTidilyInPolyTime (fun x : α × List Bool => (enc x.1).length) (encPair enc encBits) encUnary := by fun_prop - have hs := computableTidilyInPolyTime_splitAlternatingBlocks (ps.zip qs) hn - (ComputableTidilyInPolyTime.snd enc encBits) + have hs := (computableInPolyTime_splitAlternatingBlocks (ps.zip qs) hn.computableInPolyTime + (ComputableTidilyInPolyTime.snd enc encBits).computableInPolyTime).tidy exact .of_tidy <| (hV.tidy.comp ((ComputableTidilyInPolyTime.fst enc encBits).prod hs.fst')).bool_and' (hW.tidy.comp ((ComputableTidilyInPolyTime.fst enc encBits).prod hs.snd'))