From c53df333aab97767fac377373e1c58f66ae48053 Mon Sep 17 00:00:00 2001 From: chris-ai1 Date: Fri, 30 Oct 2026 22:36:25 +0000 Subject: [PATCH] refactor(Universal): use plain description decoder certificates --- .../Complexity/Classes/Hierarchy.lean | 7 +++---- .../Complexity/Classes/Hierarchy/Space.lean | 4 ++-- .../Complexity/Classes/Hierarchy/Time.lean | 4 ++-- .../Machines/Turing/MultiTape/Halting/Rice.lean | 4 ++-- .../Turing/MultiTape/Universal/Decode.lean | 14 ++++++-------- .../Turing/MultiTape/Universal/PolyTime.lean | 14 +++----------- ComplexityTests/TimeHierarchy.lean | 7 ++++++- scripts/tidy_surface_baseline.json | 3 +-- 8 files changed, 25 insertions(+), 32 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy.lean b/Complexity/Computability/Complexity/Classes/Hierarchy.lean index 56e883d9a6..e8f23856f5 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy.lean +++ b/Complexity/Computability/Complexity/Classes/Hierarchy.lean @@ -269,10 +269,9 @@ theorem computableInO_diagonal : fun x => 2 ^ (2 * x.length) := by have this : ComputableTidilyInO diagonal encBits encBool (fun x => 2 ^ (4 * x.length)) fun x => 2 ^ (2 * x.length) := by - obtain ⟨dd, ed, hdec⟩ := exists_computableTidilyInDegree_decodeDesc - have hu : ComputableTidilyInDegree unframe encBits encBits 1 1 := - .of_linear (.of_unframe fun _ => rfl) - have hdesc := (hdec.comp hu).inO + obtain ⟨dd, ed, hdec⟩ := exists_computableInDegree_decodeDesc + have hu := Internal.DecoderWords.unframe_degree + have hdesc := (hdec.comp hu).inO.tidy have hsym := Universal.computableTidilyInDegree_map_eBit.inO_one have hclock := (ComputableTidilyInDegree.two_pow_length encBits).inO_one have hpre := hdesc.prod (hsym.prod hclock) diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/Space.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/Space.lean index 0ee88de7c3..5d11917ff2 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy/Space.lean +++ b/Complexity/Computability/Complexity/Classes/Hierarchy/Space.lean @@ -120,10 +120,10 @@ space linear in the description, the budget and the lengths of the clock and of theorem computableInO_spaceDiagonal {G : ℕ → ℕ} (hG : SpaceConstructible G) : ∃ T, ComputableInO (spaceDiagonal G) encBits encBool T fun x => x.length + G x.length := by - obtain ⟨dd, ed, hdec⟩ := exists_computableTidilyInDegree_decodeDesc + obtain ⟨dd, ed, hdec⟩ := exists_computableInDegree_decodeDesc have hu : ComputableInO unframe encBits encBits (fun x => x.length) fun x => x.length := ComputableInO.of_linear (.of_unframe fun _ => rfl) - have hdesc := hdec.inO.computableInO.comp hu + have hdesc := hdec.inO.comp hu have hsym := Universal.computableTidilyInDegree_map_eBit.inO_one.computableInO obtain ⟨TG, hGb⟩ := hG.computableInO have hGu := ComputableInO.natToUnary.comp hGb diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean index f23f9d159c..48b8e810dc 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean +++ b/Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean @@ -251,10 +251,10 @@ theorem computableInO_timeDiagonal {J : ℕ → ℕ} (hJ : TimeConstructible J) have this : ComputableTidilyInO (timeDiagonal J) encBits encBool (fun x => (x.length + 1) ^ 5 * (J x.length + 1) ^ 3) fun x => (x.length + 1) ^ 5 * (J x.length + 1) ^ 3 := by - obtain ⟨dd, ed, hdec⟩ := exists_computableTidilyInDegree_decodeDesc + obtain ⟨dd, ed, hdec⟩ := exists_computableInDegree_decodeDesc have hu : ComputableTidilyInO unframe encBits encBits (fun x => x.length) fun x => x.length := ComputableTidilyInO.of_linear (.of_unframe fun _ => rfl) - have hdesc := hdec.inO.comp hu + have hdesc := hdec.inO.tidy.comp hu have hsym := Universal.computableTidilyInDegree_map_eBit.inO_one have hclock := hJ.computableInO.tidy have hU := computableTidilyInO_universal.comp (hdesc.prod (hsym.prod hclock)) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Halting/Rice.lean b/Complexity/Computability/Machines/Turing/MultiTape/Halting/Rice.lean index 35f4425d60..33c47fecc2 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Halting/Rice.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Halting/Rice.lean @@ -576,8 +576,8 @@ polynomial time. -/ theorem computableInPolyTime_selfHardwire : ComputableInPolyTime (fun y : List Bool => eDesc (hardwire (decodeDesc y) (frame y))) encBits encBits := by - obtain ⟨_, _, hdec⟩ := exists_computableTidilyInDegree_decodeDesc - have hpair := hdec.computableTidilyInPolyTime.computableInPolyTime.prod + obtain ⟨_, _, hdec⟩ := exists_computableInDegree_decodeDesc + have hpair := hdec.computableInPolyTime.prod (ComputableInPolyTime.bitsFrame encBits) exact (ComputableInPolyTime.of_eq (f := fun d : Desc => eDesc d) (encIn := eDesc) (encOut := encBits) fun _ => rfl).comp (computableInPolyTime_hardwire.comp hpair) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Decode.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Decode.lean index 0f456970e2..b2f56affa5 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Decode.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Decode.lean @@ -15,7 +15,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Decod Every word decodes to a description of a machine (`Turing.MultiTapeTM.Universal.descDecoder`): the decoder inverts the encoding `Turing.MultiTapeTM.Universal.eDesc` of descriptions, returns a -description of polynomial encoded length on every other word, and is tidily computable within +description of polynomial encoded length on every other word, and is computable within bounds of fixed degrees. It is assembled from the generic decoders of `Complexity.Computability.Machines.Turing.MultiTape.Encodings.Decoder` along the fields of a description, its transitions, their keys and their actions. @@ -32,7 +32,7 @@ to any length. * `Turing.MultiTapeTM.Universal.decodeDesc_eDesc`: decoding inverts the encoding. * `Turing.MultiTapeTM.Universal.decodeDesc_unframe_frame_append`: padded descriptions. -* `Turing.MultiTapeTM.Universal.exists_computableTidilyInDegree_decodeDesc`: decoding is tidily +* `Turing.MultiTapeTM.Universal.exists_computableInDegree_decodeDesc`: decoding is computable within bounds of fixed degrees. -/ @@ -91,13 +91,11 @@ theorem decodeDesc_unframe_frame_append (d : Desc) (pad : List Bool) : decodeDesc (unframe (frame (eDesc d) ++ pad)) = d := by rw [unframe_frame_append, decodeDesc_eDesc] -/-- **Decoding is efficient.** It is tidily computable, and the decoded descriptions have +/-- **Decoding is efficient.** It is computable, and the decoded descriptions have encoded length polynomial in the length of the word, within bounds of fixed degrees. -/ -theorem exists_computableTidilyInDegree_decodeDesc : - ∃ d e, ComputableTidilyInDegree decodeDesc encBits eDesc d e := by - obtain ⟨d, e, h⟩ := descDecoder.computable - obtain ⟨t, s, ht, hs, k, Q, hfin, tm, htm⟩ := Internal.NormalForm.degree h - exact ⟨d, e, ⟨t, s, ht, hs, k, Q, hfin, tm, htm⟩, h.2⟩ +theorem exists_computableInDegree_decodeDesc : + ∃ d e, ComputableInDegree decodeDesc encBits eDesc d e := + descDecoder.computable end Universal diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/PolyTime.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/PolyTime.lean index 11dc9b7d91..ace32c2ca1 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/PolyTime.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/PolyTime.lean @@ -40,8 +40,7 @@ single bit, independently of hierarchy theorems and Ladner's language. * `Turing.MultiTapeTM.Universal.computableTidilyInDegree_map_eBit`: input symbols in linear time and output size. -* `Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_decodeDesc`, - `Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_map_eBit`, +* `Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_map_eBit`, `Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_eBit`, `Turing.MultiTapeTM.Universal.computableInPolyTime_decodeDesc`, `Turing.MultiTapeTM.Universal.computableInPolyTime_map_eBit`, @@ -132,14 +131,6 @@ theorem computableTidilyInDegree_map_eBit : (ComputableTidilyInDegree.of_linear (encIn := encBits) (encMid := encTrueDoubled) (f := id) (trueDoubleT.computableTidilyInLinearTimeAndSpace fun x => (trueDoubleT_run x).symm)) - -/-- Decoding a machine description is polynomial-time in the input word. -/ -@[fun_prop] -theorem computableTidilyInPolyTime_decodeDesc : - ComputableTidilyInPolyTime decodeDesc encBits eDesc := - let ⟨_, _, h⟩ := exists_computableTidilyInDegree_decodeDesc - h.computableTidilyInPolyTime - /-- The input of a machine as symbols is linear. -/ @[fun_prop] theorem computableTidilyInPolyTime_map_eBit : @@ -232,7 +223,8 @@ theorem computableTidilyInPolyTime_universal : @[fun_prop] theorem computableInPolyTime_decodeDesc : ComputableInPolyTime decodeDesc encBits eDesc := - .of_tidy computableTidilyInPolyTime_decodeDesc + let ⟨_, _, h⟩ := exists_computableInDegree_decodeDesc + h.computableInPolyTime /-- Plain polynomial-time certificate for coding a bit string as unary symbol numbers. -/ @[fun_prop] diff --git a/ComplexityTests/TimeHierarchy.lean b/ComplexityTests/TimeHierarchy.lean index 6a74959b47..2ae023a25c 100644 --- a/ComplexityTests/TimeHierarchy.lean +++ b/ComplexityTests/TimeHierarchy.lean @@ -41,10 +41,15 @@ example : /-- Every word decodes to a description of polynomial encoded length. -/ example : ∃ e c : ℕ, ∀ w : List Bool, (eDesc (decodeDesc w)).length ≤ c * (w.length + 1) ^ e := by - obtain ⟨_d, e, h⟩ := exists_computableTidilyInDegree_decodeDesc + obtain ⟨_d, e, h⟩ := exists_computableInDegree_decodeDesc obtain ⟨c, hc⟩ := h.2 exact ⟨e, c, fun w => hc w⟩ +/-- Plain automation composes description decoding with framing of its input. -/ +example : ComputableInPolyTime (fun w : List Bool => (decodeDesc w, frame w)) encBits + (encPair eDesc encBits) := by + fun_prop + /-! ### The clock -/ example : diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json index e20fbe018c..cd26f703ac 100644 --- a/scripts/tidy_surface_baseline.json +++ b/scripts/tidy_surface_baseline.json @@ -53,10 +53,9 @@ "Complexity/Computability/Machines/Turing/MultiTape/Halting/Rice.lean": 2, "Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/QueryTake.lean": 2, "Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean": 7, - "Complexity/Computability/Machines/Turing/MultiTape/Universal/Decode.lean": 1, "Complexity/Computability/Machines/Turing/MultiTape/Universal/InPlace.lean": 9, "Complexity/Computability/Machines/Turing/MultiTape/Universal/Machine.lean": 2, - "Complexity/Computability/Machines/Turing/MultiTape/Universal/PolyTime.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Universal/PolyTime.lean": 4, "Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean": 2, "Complexity/Computability/Probabilistic/Adaptive.lean": 5, "Complexity/Computability/Probabilistic/CoinTape.lean": 5,