From 8d91656675cfea95ceab36626db5f6b2bd892338 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 1 Nov 2026 14:28:06 -0500 Subject: [PATCH 1/2] refactor(CountingSimulation): share the clocked-run budget between the fast machines fastCertificate_le (explicit networks) and exists_fastCore_le (entry procedures) repeated the same 150-line arithmetic: lifting the bounds of Scheme.certificate_le, the resource analysis, the clock and the output step into one K B ^ K 2 ^ (K s / S) budget. It is now exists_clockedRun_le in FastAlgorithm.lean, used by both. The output-step bound is proved once for time and space together, and the private time/space assembly lemmas are gone. DescribedContraction.contractionCertificate_le proves the leaf bounds for time and space in one case analysis, and their arithmetic through one local lemma. Public statements are unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../TensorNetwork/DescribedContraction.lean | 101 ++--- .../CountingSimulation/EntryAnalysis.lean | 260 ++----------- .../CountingSimulation/FastAlgorithm.lean | 365 +++++++----------- 3 files changed, 227 insertions(+), 499 deletions(-) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedContraction.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedContraction.lean index 8168cafce7..4f37457f9c 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedContraction.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedContraction.lean @@ -806,70 +806,46 @@ theorem contractionCertificate_le [Inhabited Y] (hops : ops.PolyTime encQ encY) omega have hnode (x : Node Q T) (hx : (sumInvariant ops eval (P, d)).node x) : (encNode encQ encT x).length ≤ 5 * z + 7 := (length_encNode_le hx).trans (by omega) - have hleafT (x : Node Q T) (hx : (sumInvariant ops eval (P, d)).node x) : + -- The leaf step: the vertex lookup, and the zero or the query and the evaluator. + have hleaf (x : Node Q T) (hx : (sumInvariant ops eval (P, d)).node x) : (leafCertificate eval hops ev).time x ≤ 2 * cv * (5 * z + 8) ^ dv + (5 * z + 7) + - cz * (5 * z + 8) ^ dz + cq * (11 * z + 16) ^ dq + E := by - have h1 := hnode x hx - rw [leafCertificate_time] - have h2 : (vertexCertificate (encQ := encQ) (encT := encT)).time x ≤ - cv * (5 * z + 8) ^ dv := - (hvt x).trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _)) - have h2' : 2 * (vertexCertificate (encQ := encQ) (encT := encT)).time x ≤ - 2 * cv * (5 * z + 8) ^ dv := by - rw [Nat.mul_assoc]; exact Nat.mul_le_mul_left 2 h2 - cases hvx : x.2.1.2.vertices[x.2.2.2]? with - | none => - simp only [Option.elim] - have h3 : (zeroCertificate (encT := encT) hops).time x ≤ cz * (5 * z + 8) ^ dz := - (hzt x).trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _)) - omega - | some v => - simp only [Option.elim] - have hmem : v ∈ x.2.1.2.vertices := List.mem_of_getElem? hvx - obtain ⟨hq, -, -, -⟩ := hx - rw [hq] at hmem - have h3 := hvlen v hmem - have h4 : (queryCertificate (encQ := encQ) (encT := encT)).time (x, v) ≤ - cq * (11 * z + 16) ^ dq := by - refine (hqt (x, v)).trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left ?_ _)) - have := length_encPair (enc₁ := encNode encQ encT) - (enc₂ := encPair (encList encNat) encT) (x, v) - dsimp only at this - omega - have h5 := (hE v hmem (wordBits x.2.2.1 v.1) (by simp [wordBits])).1 - omega - have hleafS (x : Node Q T) (hx : (sumInvariant ops eval (P, d)).node x) : + cz * (5 * z + 8) ^ dz + cq * (11 * z + 16) ^ dq + E ∧ (leafCertificate eval hops ev).space x ≤ 2 * cv' * (5 * z + 8) ^ dv' + (5 * z + 7) + cz' * (5 * z + 8) ^ dz' + cq' * (11 * z + 16) ^ dq' + ES := by have h1 := hnode x hx - rw [leafCertificate_space] - have h2 : (vertexCertificate (encQ := encQ) (encT := encT)).space x ≤ - cv' * (5 * z + 8) ^ dv' := - (hvs x).trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _)) + have hx8 {c e : ℕ} : c * ((encNode encQ encT x).length + 1) ^ e ≤ c * (5 * z + 8) ^ e := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _) + have h2 : 2 * (vertexCertificate (encQ := encQ) (encT := encT)).time x ≤ + 2 * cv * (5 * z + 8) ^ dv := by + rw [Nat.mul_assoc]; exact Nat.mul_le_mul_left 2 ((hvt x).trans hx8) have h2' : 2 * (vertexCertificate (encQ := encQ) (encT := encT)).space x ≤ 2 * cv' * (5 * z + 8) ^ dv' := by - rw [Nat.mul_assoc]; exact Nat.mul_le_mul_left 2 h2 + rw [Nat.mul_assoc]; exact Nat.mul_le_mul_left 2 ((hvs x).trans hx8) + rw [leafCertificate_time, leafCertificate_space] cases hvx : x.2.1.2.vertices[x.2.2.2]? with | none => + have h3 := (hzt x).trans hx8 + have h3' := (hzs x).trans hx8 simp only [Option.elim] - have h3 : (zeroCertificate (encT := encT) hops).space x ≤ cz' * (5 * z + 8) ^ dz' := - (hzs x).trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _)) - omega + constructor <;> omega | some v => - simp only [Option.elim] have hmem : v ∈ x.2.1.2.vertices := List.mem_of_getElem? hvx obtain ⟨hq, -, -, -⟩ := hx rw [hq] at hmem have h3 := hvlen v hmem - have h4 : (queryCertificate (encQ := encQ) (encT := encT)).space (x, v) ≤ - cq' * (11 * z + 16) ^ dq' := by - refine (hqs (x, v)).trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left ?_ _)) + have hxv {c e : ℕ} : + c * ((encPair (encNode encQ encT) (encPair (encList encNat) encT) (x, v)).length + 1) ^ e ≤ + c * (11 * z + 16) ^ e := by + refine Nat.mul_le_mul_left _ (Nat.pow_le_pow_left ?_ _) have := length_encPair (enc₁ := encNode encQ encT) (enc₂ := encPair (encList encNat) encT) (x, v) dsimp only at this omega - have h5 := (hE v hmem (wordBits x.2.2.1 v.1) (by simp [wordBits])).2.1 - omega + have h4 := (hqt (x, v)).trans hxv + have h4' := (hqs (x, v)).trans hxv + obtain ⟨h5, h5', -⟩ := hE v hmem (wordBits x.2.2.1 v.1) (by simp [wordBits]) + simp only [Option.elim] + constructor <;> omega obtain ⟨h, hh, he⟩ := eval_sumRoot (ops := ops) (eval := eval) P d have hres := hK₀ (NativeCertificate.ofPolyTime fuel_polyTime) (NativeCertificate.ofPolyTime sumRoot_polyTime) (sumInvariant ops eval (P, d)) (13 * z + 18) @@ -877,7 +853,7 @@ theorem contractionCertificate_le [Inhabited Y] (hops : ops.PolyTime encQ encY) cq * (11 * z + 16) ^ dq + E) (2 * cv' * (5 * z + 8) ^ dv' + (5 * z + 7) + cz' * (5 * z + 8) ^ dz' + cq' * (11 * z + 16) ^ dq' + ES) - (fun x hx => ⟨(hnode x hx).trans (by omega), fun _ => ⟨hleafT x hx, hleafS x hx⟩⟩) + (fun x hx => ⟨(hnode x hx).trans (by omega), fun _ => hleaf x hx⟩) (fun x a ha => by obtain ⟨hx, ha1, ha2⟩ := ha have h1 := hnode x hx @@ -932,26 +908,21 @@ theorem contractionCertificate_le [Inhabited Y] (hops : ops.PolyTime encQ encY) have h3 : (h + 1) * (13 * z + 18 + 1) ≤ 39 * z + 57 := by have := Nat.mul_le_mul_right (13 * z + 18 + 1) (show h + 1 ≤ 3 by omega); omega exact (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left h3 _)).trans (hterm (by omega)) - have hTL : 2 * cv * (5 * z + 8) ^ dv + (5 * z + 7) + cz * (5 * z + 8) ^ dz + - cq * (11 * z + 16) ^ dq ≤ (2 * cv * 13 ^ dv + 12 + cz * 13 ^ dz + cq * 27 ^ dq) * W := by - have a1 := hterm (c := 2 * cv) (a := 5) (b := 8) (show dv ≤ D by omega) - have a2 := hterm (c := cz) (a := 5) (b := 8) (show dz ≤ D by omega) - have a3 := hterm (c := cq) (a := 11) (b := 16) (show dq ≤ D by omega) - have e : (2 * cv * 13 ^ dv + 12 + cz * 13 ^ dz + cq * 27 ^ dq) * W = - 2 * cv * (5 + 8) ^ dv * W + 12 * W + cz * (5 + 8) ^ dz * W + cq * (11 + 16) ^ dq * W := by - ring - omega - have hSL : 2 * cv' * (5 * z + 8) ^ dv' + (5 * z + 7) + cz' * (5 * z + 8) ^ dz' + - cq' * (11 * z + 16) ^ dq' ≤ - (2 * cv' * 13 ^ dv' + 12 + cz' * 13 ^ dz' + cq' * 27 ^ dq') * W := by - have a1 := hterm (c := 2 * cv') (a := 5) (b := 8) (show dv' ≤ D by omega) - have a2 := hterm (c := cz') (a := 5) (b := 8) (show dz' ≤ D by omega) - have a3 := hterm (c := cq') (a := 11) (b := 16) (show dq' ≤ D by omega) - have e : (2 * cv' * 13 ^ dv' + 12 + cz' * 13 ^ dz' + cq' * 27 ^ dq') * W = - 2 * cv' * (5 + 8) ^ dv' * W + 12 * W + cz' * (5 + 8) ^ dz' * W + - cq' * (11 + 16) ^ dq' * W := by + -- The leaf bound, for time and for space. + have hleafW {a b c e f g : ℕ} (hb : b ≤ D) (he : e ≤ D) (hg : g ≤ D) : + 2 * a * (5 * z + 8) ^ b + (5 * z + 7) + c * (5 * z + 8) ^ e + f * (11 * z + 16) ^ g ≤ + (2 * a * 13 ^ b + 12 + c * 13 ^ e + f * 27 ^ g) * W := by + have a1 := hterm (c := 2 * a) (a := 5) (b := 8) hb + have a2 := hterm (c := c) (a := 5) (b := 8) he + have a3 := hterm (c := f) (a := 11) (b := 16) hg + have e : (2 * a * 13 ^ b + 12 + c * 13 ^ e + f * 27 ^ g) * W = + 2 * a * (5 + 8) ^ b * W + 12 * W + c * (5 + 8) ^ e * W + f * (11 + 16) ^ g * W := by ring omega + have hTL := hleafW (a := cv) (c := cz) (f := cq) (show dv ≤ D by omega) (show dz ≤ D by omega) + (show dq ≤ D by omega) + have hSL := hleafW (a := cv') (c := cz') (f := cq') (show dv' ≤ D by omega) + (show dz' ≤ D by omega) (show dq' ≤ D by omega) have hclock : ((encNat (fuel (P, d))).length + 1) ^ 2 ≤ 16 * W := by have h3 : (encNat (fuel (P, d))).length + 1 ≤ 4 * (z + 1) := by omega calc ((encNat (fuel (P, d))).length + 1) ^ 2 ≤ (4 * (z + 1)) ^ 2 := Nat.pow_le_pow_left h3 2 diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/EntryAnalysis.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/EntryAnalysis.lean index 44f0e9c8a2..436cee0775 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/EntryAnalysis.lean +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/EntryAnalysis.lean @@ -468,30 +468,6 @@ theorem exists_entryAnalysis /-! ### The resources of the machine -/ -private theorem mul_succ_le_sq (H F : ℕ) : (H + 1) * (F + 1) ≤ (H + F + 1) ^ 2 := by nlinarith - -private theorem mul_add_one_le {c x : ℕ} (hx : 1 ≤ x) : c * x + 1 ≤ (c + 1) * x := by nlinarith - -/-- The arithmetic of the time bound. -/ -private theorem time_assemble {gT runT cT rT fuel Z TL Wb n rest Q W c₁ k₁ c₃ ka R : ℕ} - (hrun : runT ≤ cT + rT + 2 * n + (fuel + 1) * (Z + TL + Wb)) - (hq : gT + cT + rT ≤ Q) (hQ : Q ≤ c₁ * W) - (hP1 : (fuel + 1) * Z ≤ 2 * k₁ * W) (hP2 : (fuel + 1) * TL ≤ 2 * ka * W) - (hP3 : (fuel + 1) * Wb ≤ 2 * c₃ * W) (hn : n + 1 ≤ W) (hR : rest ≤ R * W) : - gT + (2 * runT + n + rest) ≤ (2 * c₁ + 5 + 4 * k₁ + 4 * c₃ + 4 * ka + R) * W := by - have e : (fuel + 1) * (Z + TL + Wb) = (fuel + 1) * Z + (fuel + 1) * TL + (fuel + 1) * Wb := by - ring - rw [e] at hrun - nlinarith - -/-- The arithmetic of the space bound. -/ -private theorem space_assemble {gS runS cS rS fb Z SL n rest Q W c₁ k₁ ka R : ℕ} - (hrun : runS ≤ cS + rS + 2 * n + Z + SL + fb) - (hq : gS + cS + rS + fb ≤ Q) (hQ : Q ≤ c₁ * W) (hZ : Z ≤ k₁ * W) (hSL : SL ≤ ka * W) - (hn : n + 1 ≤ W) (hR : rest ≤ R * W) : - gS + (2 * runS + n + rest) ≤ (2 * c₁ + 5 + 2 * k₁ + 2 * ka + R) * W := by - nlinarith - /-- **The machine within the interface's bounds.** For a native certificate `ce` of the entry procedure and all constants `C` and `D` there is `K` such that on every input at the modulus admissible at size `s ≥ 2` with constant `C` and with precision `1 ≤ P ≤ D s`, the machine @@ -516,76 +492,31 @@ theorem exists_fastCore_le have hcnP := NativeCertificate.ofPolyTime_isPolynomial (clock_polyTime (encT := encT)) have hcrP := NativeCertificate.ofPolyTime_isPolynomial (rootCall_polyTime (encT := encT)) have hfuelL := (clock_polyTime (encT := encT)).polyBounded_length - obtain ⟨c₁, d₁, h₁⟩ := ((((((hgP.1.add hgP.2).add hcnP.1).add hcnP.2).add hcrP.1).add - hcrP.2).add hfuelL).exists_le + obtain ⟨c₁, d₁, h₁⟩ := (((((((hgP.1.add hgP.2).add hcnP.1).add hcnP.2).add hcrP.1).add + hcrP.2).add hfuelL).add .self).exists_le have htP := NativeCertificate.ofPolyTime_isPolynomial (valueTag_polyTime (encT := encT)) have hoP := NativeCertificate.ofPolyTime_isPolynomial (valueList_polyTime (encT := encT)) have hfP := NativeCertificate.ofPolyTime_isPolynomial (ComputableInPolyTime.fst (encInput encT) encValue) obtain ⟨c₂, d₂, h₂⟩ := (((((htP.1.add htP.2).add hoP.1).add hoP.2).add hfP.1).add hfP.2).exists_le - -- The constants. - set E := 2 * d₁ + 2 * Ka * K₁ + (Ka + 1) * d₂ + K₂ + Ka + 1 with hE - set Kc := 2 * c₁ + 5 + 4 * (K₁ * (Ka + 1) ^ (2 * K₁)) + 4 * (c₁ + 1) ^ 2 + 4 * Ka + - (c₂ * (Ka + 2) ^ d₂ + K₂ * 2 ^ (K₂ * s₀)) with hKc - refine ⟨Kc + E + fuelConst * (C + D) + Ka, fun s P r G hs hP hPD hA => ?_⟩ + obtain ⟨K, hK⟩ := exists_clockedRun_le K₁ Ka (4 * c₁) d₁ (2 * (c₂ * (Ka + 2) ^ d₂)) + ((Ka + 1) * d₂) (2 * (K₂ * 2 ^ (K₂ * s₀))) K₂ (fuelConst * (C + D)) + refine ⟨K, fun s P r G hs hP hPD hA => ?_⟩ obtain ⟨N, H, F, TL, SL, he, hN, hnode, hframe, hvalue, hHFS, hTL⟩ := hKa s P r G hs hP hPD hA have hg : EntryContraction.guard (P, modulus G.numEdges, r, G) = true := guard_of_entryAdmissible hA obtain ⟨hdT, hdS⟩ := hK₂ s P r G hA - have hsm : s ≤ G.numEdges := hA.2.1 - have hmC : G.numEdges ≤ C * s := hA.2.2.1 - set x := (P, modulus G.numEdges, r, G) with hx - set n := (encInput encT x).length with hn - set B := n + 1 with hB - have hB1 : 1 ≤ B := by omega - set S := Nat.sqrt (Nat.log 2 s) - set Xf := 2 ^ (fuelConst * (C + D) * s / S) - set Xa := 2 ^ (Ka * s / S) - set X := 2 ^ ((fuelConst * (C + D) + Ka) * s / S) - have hXfX : Xf ≤ X := Nat.pow_le_pow_right (by norm_num) - (Nat.div_le_div_right (Nat.mul_le_mul_right _ (by omega))) - have hXfXa : Xf * Xa ≤ X := by - rw [← pow_add] - refine Nat.pow_le_pow_right (by norm_num) (Nat.div_add_div_le_add_div.trans ?_) - rw [add_mul] - have hX1 : 1 ≤ X := Nat.one_le_two_pow - -- The run. + set x := (P, modulus G.numEdges, r, G) + have hq1 := h₁ x + set B := (encInput encT x).length + 1 with hB obtain ⟨hrT, hrS⟩ := hK₁ (NativeCertificate.ofPolyTime clock_polyTime) (NativeCertificate.ofPolyTime rootCall_polyTime) _ F TL SL hnode hframe hvalue x _ N H he - have hclock : clock x ≤ Xf := clock_le hs hsm hmC hPD - have hq1 := h₁ x have hrT' : (runCore ce).time x ≤ _ := hrT have hrS' : (runCore ce).space x ≤ _ := hrS - -- Polynomial pieces. - set Q₁ := c₁ * B ^ d₁ with hQ₁ - have hBK (k : ℕ) : 1 ≤ B ^ k := Nat.one_le_pow _ _ (by omega) - have hHF : (H + 1) * (F + 1) ≤ ((Ka + 1) * B ^ Ka) ^ 2 := by - have h1 : H + F ≤ Ka * B ^ Ka := by have := hHFS; omega - have h2 := hBK Ka - calc (H + 1) * (F + 1) ≤ (H + F + 1) ^ 2 := mul_succ_le_sq H F - _ ≤ (Ka * B ^ Ka + B ^ Ka) ^ 2 := Nat.pow_le_pow_left (by omega) 2 - _ = ((Ka + 1) * B ^ Ka) ^ 2 := by ring - have hZ : K₁ * ((H + 1) * (F + 1)) ^ K₁ ≤ K₁ * (Ka + 1) ^ (2 * K₁) * B ^ (2 * Ka * K₁) := by - calc K₁ * ((H + 1) * (F + 1)) ^ K₁ ≤ K₁ * (((Ka + 1) * B ^ Ka) ^ 2) ^ K₁ := - Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hHF _) - _ = K₁ * (Ka + 1) ^ (2 * K₁) * B ^ (2 * Ka * K₁) := by - rw [mul_pow, ← pow_mul, mul_pow, ← pow_mul, ← pow_mul, - show Ka * 2 * K₁ = 2 * Ka * K₁ by ring] - ring - have hW : ((encNat (clock x)).length + 1) ^ 2 ≤ (c₁ + 1) ^ 2 * B ^ (2 * d₁) := by - have h1 : (encNat (clock x)).length ≤ Q₁ := by omega - have h2 := hBK d₁ - calc _ ≤ (Q₁ + 1) ^ 2 := Nat.pow_le_pow_left (by omega) 2 - _ ≤ ((c₁ + 1) * B ^ d₁) ^ 2 := Nat.pow_le_pow_left (mul_add_one_le h2) 2 - _ = (c₁ + 1) ^ 2 * B ^ (2 * d₁) := by ring - have hTL' : TL ≤ Ka * B ^ Ka * Xa := hTL - have hSL : SL ≤ Ka * B ^ Ka := by have := hHFS; omega - -- The output and direct summation. - set R₁ := c₂ * (Ka + 2) ^ d₂ * B ^ ((Ka + 1) * d₂) with hR₁ - set R₂ := K₂ * 2 ^ (K₂ * s₀) * B ^ K₂ with hR₂ - have hdec : ∀ v : ℕ × List ℕ, (reachInv entry nativeMk (rootCall x)).value v → + -- The output of the run, and direct summation below `s₀`. + have hdec (v : ℕ × List ℕ) (hv : (reachInv entry nativeMk (rootCall x)).value v) : (NativeCertificate.ofPolyTime (valueTag_polyTime (encT := encT))).time (x, v) + (NativeCertificate.ofPolyTime (valueTag_polyTime (encT := encT))).space (x, v) + (NativeCertificate.ofPolyTime (valueList_polyTime (encT := encT))).time (x, v) + @@ -593,148 +524,41 @@ theorem exists_fastCore_le (NativeCertificate.ofPolyTime (ComputableInPolyTime.fst (encInput encT) encValue)).time (x, v) + (NativeCertificate.ofPolyTime - (ComputableInPolyTime.fst (encInput encT) encValue)).space (x, v) ≤ R₁ := by - intro v hv - have h := h₂ (x, v) - have hv' := hvalue v hv - have hF : F ≤ Ka * B ^ Ka := by have := hHFS; omega - have hk1 : B ≤ B ^ (Ka + 1) := by - calc B = B ^ 1 := (pow_one B).symm - _ ≤ B ^ (Ka + 1) := Nat.pow_le_pow_right hB1 (by omega) - have hk2 : B ^ Ka ≤ B ^ (Ka + 1) := Nat.pow_le_pow_right hB1 (by omega) - have hlen : (encPair (encInput encT) encValue (x, v)).length + 1 ≤ - (Ka + 2) * B ^ (Ka + 1) := by - have hl := length_encPair (enc₁ := encInput encT) (enc₂ := encValue) (x, v) - simp only at hl - rw [hl] - have : Ka * B ^ Ka ≤ Ka * B ^ (Ka + 1) := Nat.mul_le_mul_left _ hk2 - have e : (Ka + 2) * B ^ (Ka + 1) = Ka * B ^ (Ka + 1) + 2 * B ^ (Ka + 1) := by ring - omega - calc _ ≤ c₂ * ((encPair (encInput encT) encValue (x, v)).length + 1) ^ d₂ := h - _ ≤ c₂ * ((Ka + 2) * B ^ (Ka + 1)) ^ d₂ := - Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hlen _) - _ = R₁ := by rw [hR₁, mul_pow, ← pow_mul, Nat.mul_assoc] - have hdir (hs₀ : s < s₀) : (directCore entry ce).time x ≤ R₂ := by - refine hdT.trans ?_ - have h2 : 2 ^ (K₂ * s) ≤ 2 ^ (K₂ * s₀) := - Nat.pow_le_pow_right (by norm_num) (Nat.mul_le_mul_left _ hs₀.le) - calc K₂ * B ^ K₂ * 2 ^ (K₂ * s) ≤ K₂ * B ^ K₂ * 2 ^ (K₂ * s₀) := Nat.mul_le_mul_left _ h2 - _ = R₂ := by rw [hR₂]; ring - have hdirS : (directCore entry ce).space x ≤ R₂ := - hdS.trans (by - rw [hR₂] - calc K₂ * B ^ K₂ ≤ K₂ * B ^ K₂ * 2 ^ (K₂ * s₀) := - Nat.le_mul_of_pos_right _ Nat.one_le_two_pow - _ = K₂ * 2 ^ (K₂ * s₀) * B ^ K₂ := by ring) + (ComputableInPolyTime.fst (encInput encT) encValue)).space (x, v) ≤ + c₂ * (Ka + 2) ^ d₂ * B ^ ((Ka + 1) * d₂) := by + refine (h₂ (x, v)).trans ?_ + rw [Nat.mul_assoc, pow_mul, ← mul_pow] + refine Nat.mul_le_mul_left _ (Nat.pow_le_pow_left ?_ _) + have := hvalue v hv + have hB1 : B ≤ B ^ (Ka + 1) := Nat.le_self_pow (by omega) _ + have hBK := Nat.mul_le_mul_left Ka + (Nat.pow_le_pow_right (by omega : 1 ≤ B) (by omega : Ka ≤ Ka + 1)) + simp only [length_encPair (enc₁ := encInput encT) (enc₂ := encValue), add_mul] + omega + have hdir (hs₀ : s < s₀) : (directCore entry ce).time x ≤ K₂ * 2 ^ (K₂ * s₀) * B ^ K₂ := + hdT.trans (le_of_le_of_eq (Nat.mul_le_mul_left _ + (Nat.pow_le_pow_right (by norm_num) (Nat.mul_le_mul_left _ hs₀.le))) (by ring)) + have hdirS : (directCore entry ce).space x ≤ K₂ * 2 ^ (K₂ * s₀) * B ^ K₂ := + hdS.trans (le_of_le_of_eq (Nat.le_mul_of_pos_right _ (Nat.two_pow_pos (K₂ * s₀))) (by ring)) have hbig : s₀ ≤ s → (scheme entry nativeMk).run clock rootCall x = some (0, value entry nativeMk (rootCall x)) := fun h => Scheme.run_eq_some he (hN h) - clear hKa hK₁ hK₂ h₁ h₂ - -- Everything against `W = B ^ E X`. - set W := B ^ E * X with hWdef - have lift {c d : ℕ} (hd : d ≤ E) : c * B ^ d ≤ c * W := by - rw [hWdef, ← Nat.mul_assoc] - exact (Nat.mul_le_mul_left c (Nat.pow_le_pow_right hB1 hd)).trans - (Nat.le_mul_of_pos_right _ hX1) - have lift' {c d : ℕ} (hd : d ≤ E) : c * B ^ d ≤ c * B ^ E := - Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hB1 hd) - have hQW : Q₁ ≤ c₁ * W := lift (by omega) - have hR₁W : R₁ ≤ c₂ * (Ka + 2) ^ d₂ * W := lift (by omega) - have hR₂W : R₂ ≤ K₂ * 2 ^ (K₂ * s₀) * W := lift (by omega) - have hnW : n + 1 ≤ W := by - have := lift (c := 1) (d := 1) (by omega); rw [pow_one] at this; omega - have hfuel1 : clock x + 1 ≤ 2 * Xf := by - have : 1 ≤ Xf := Nat.one_le_two_pow - omega - have hP1 : (clock x + 1) * (K₁ * ((H + 1) * (F + 1)) ^ K₁) ≤ - 2 * (K₁ * (Ka + 1) ^ (2 * K₁)) * W := by - calc _ ≤ (2 * Xf) * (K₁ * (Ka + 1) ^ (2 * K₁) * B ^ (2 * Ka * K₁)) := - Nat.mul_le_mul hfuel1 hZ - _ = 2 * (K₁ * (Ka + 1) ^ (2 * K₁)) * (B ^ (2 * Ka * K₁) * Xf) := by ring - _ ≤ 2 * (K₁ * (Ka + 1) ^ (2 * K₁)) * W := Nat.mul_le_mul_left _ - (Nat.mul_le_mul (Nat.pow_le_pow_right hB1 (by omega)) hXfX) - have hP2 : (clock x + 1) * TL ≤ 2 * Ka * W := by - calc _ ≤ (2 * Xf) * (Ka * B ^ Ka * Xa) := Nat.mul_le_mul hfuel1 hTL' - _ = 2 * Ka * (B ^ Ka * (Xf * Xa)) := by ring - _ ≤ 2 * Ka * W := Nat.mul_le_mul_left _ - (Nat.mul_le_mul (Nat.pow_le_pow_right hB1 (by omega)) hXfXa) - have hP3 : (clock x + 1) * ((encNat (clock x)).length + 1) ^ 2 ≤ 2 * (c₁ + 1) ^ 2 * W := by - calc _ ≤ (2 * Xf) * ((c₁ + 1) ^ 2 * B ^ (2 * d₁)) := Nat.mul_le_mul hfuel1 hW - _ = 2 * (c₁ + 1) ^ 2 * (B ^ (2 * d₁) * Xf) := by ring - _ ≤ 2 * (c₁ + 1) ^ 2 * W := Nat.mul_le_mul_left _ - (Nat.mul_le_mul (Nat.pow_le_pow_right hB1 (by omega)) hXfX) - have hZE : K₁ * ((H + 1) * (F + 1)) ^ K₁ ≤ K₁ * (Ka + 1) ^ (2 * K₁) * B ^ E := - hZ.trans (lift' (by omega)) - have hQE : Q₁ ≤ c₁ * B ^ E := lift' (by omega) - have hR₁E : R₁ ≤ c₂ * (Ka + 2) ^ d₂ * B ^ E := lift' (by omega) - have hR₂E : R₂ ≤ K₂ * 2 ^ (K₂ * s₀) * B ^ E := lift' (by omega) - have hSLE : SL ≤ Ka * B ^ E := hSL.trans (lift' (by omega)) - have hnE : n + 1 ≤ B ^ E := by - have := lift' (c := 1) (d := 1) (by omega); rw [pow_one] at this; omega - have hKK : Kc ≤ Kc + E + fuelConst * (C + D) + Ka := by omega - have hBE : B ^ E ≤ B ^ (Kc + E + fuelConst * (C + D) + Ka) := - Nat.pow_le_pow_right hB1 (by omega) - have hXK : X ≤ 2 ^ ((Kc + E + fuelConst * (C + D) + Ka) * s / S) := - Nat.pow_le_pow_right (by norm_num) (Nat.div_le_div_right (Nat.mul_le_mul_right _ (by omega))) - have hR : R₁ + R₂ ≤ (c₂ * (Ka + 2) ^ d₂ + K₂ * 2 ^ (K₂ * s₀)) * W := by - rw [Nat.add_mul]; exact Nat.add_le_add hR₁W hR₂W - have hRE : R₁ + R₂ ≤ (c₂ * (Ka + 2) ^ d₂ + K₂ * 2 ^ (K₂ * s₀)) * B ^ E := by - rw [Nat.add_mul]; exact Nat.add_le_add hR₁E hR₂E - refine ⟨?_, ?_⟩ - · rw [fastCore_time] - simp only [hg, ↓reduceIte] - have hrest : ((scheme entry nativeMk).run clock rootCall x).elim - ((directCore entry ce).time x) (fun (tag, coeffs) => - (NativeCertificate.ofPolyTime (valueTag_polyTime (encT := encT))).time - (x, (tag, coeffs)) + - if decide (tag = 0) = true then - (NativeCertificate.ofPolyTime (valueList_polyTime (encT := encT))).time - (x, (tag, coeffs)) - else (NativeCertificate.ofPolyTime - (ComputableInPolyTime.fst (encInput encT) encValue)).time (x, (tag, coeffs)) + - (directCore entry ce).time x) ≤ R₁ + R₂ := by - rcases hr : (scheme entry nativeMk).run clock rootCall x with _ | ⟨tag, coeffs⟩ - · by_cases hs₀ : s₀ ≤ s - · rw [hbig hs₀] at hr; cases hr - · simp only [Option.elim_none]; have := hdir (by omega); omega - · have hd := hdec (tag, coeffs) (Scheme.value_of_run_eq_some he hr) - simp only [Option.elim_some] - split_ifs with h0 - · omega - · by_cases hs₀ : s₀ ≤ s - · rw [hbig hs₀] at hr; cases hr; simp at h0 - · have := hdir (by omega); omega - have htot := time_assemble (gT := (NativeCertificate.ofPolyTime - (guard_polyTime (encT := encT))).time x) hrT' (by omega) hQW hP1 hP2 hP3 hnW - (hrest.trans hR) - calc _ ≤ Kc * W := by rw [hKc]; exact htot - _ ≤ _ := by - rw [hWdef, ← Nat.mul_assoc] - exact Nat.mul_le_mul (Nat.mul_le_mul hKK hBE) hXK - · rw [fastCore_space] - simp only [hg, ↓reduceIte] - have hrest : ((scheme entry nativeMk).run clock rootCall x).elim - ((directCore entry ce).space x) (fun (tag, coeffs) => - (NativeCertificate.ofPolyTime (valueTag_polyTime (encT := encT))).space - (x, (tag, coeffs)) + - if decide (tag = 0) = true then - (NativeCertificate.ofPolyTime (valueList_polyTime (encT := encT))).space - (x, (tag, coeffs)) - else (NativeCertificate.ofPolyTime - (ComputableInPolyTime.fst (encInput encT) encValue)).space (x, (tag, coeffs)) + - (directCore entry ce).space x) ≤ R₁ + R₂ := by - rcases hr : (scheme entry nativeMk).run clock rootCall x with _ | ⟨tag, coeffs⟩ - · simp only [Option.elim_none]; omega - · have hd := hdec (tag, coeffs) (Scheme.value_of_run_eq_some he hr) - simp only [Option.elim_some] - split_ifs <;> omega - have htot := space_assemble (gS := (NativeCertificate.ofPolyTime - (guard_polyTime (encT := encT))).space x) hrS' (by omega) hQE hZE hSLE hnE - (hrest.trans hRE) - calc _ ≤ (2 * c₁ + 5 + 2 * (K₁ * (Ka + 1) ^ (2 * K₁)) + 2 * Ka + - (c₂ * (Ka + 2) ^ d₂ + K₂ * 2 ^ (K₂ * s₀))) * B ^ E := htot - _ ≤ Kc * B ^ E := Nat.mul_le_mul_right _ (by rw [hKc]; omega) - _ ≤ _ := Nat.mul_le_mul hKK hBE + rw [fastCore_time, fastCore_space, ite_eq_left hg, ite_eq_left hg] + -- The output step: decoding a value, or direct summation below `s₀`. + refine hK (by omega) hrT' hrS' (by rw [Nat.mul_assoc]; omega) ?_ (clock_le hs hA.2.1 hA.2.2.1 hPD) + hHFS hTL + rw [Nat.mul_assoc 2, Nat.mul_assoc 2] + rcases hr : (scheme entry nativeMk).run clock rootCall x with _ | ⟨tag, coeffs⟩ + · have hs₀ : s < s₀ := Nat.lt_of_not_le fun h => by rw [hbig h] at hr; cases hr + have := hdir hs₀ + simp only [Option.elim_none]; omega + · have hd := hdec (tag, coeffs) (Scheme.value_of_run_eq_some he hr) + simp only [Option.elim_some] + split_ifs with h0 + · omega + · have hs₀ : s < s₀ := Nat.lt_of_not_le fun h => by + rw [hbig h] at hr; cases hr; simp at h0 + have := hdir hs₀; omega /-! ### The contraction algorithm -/ diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAlgorithm.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAlgorithm.lean index 229fd0594c..3cf7ee3a0a 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAlgorithm.lean +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAlgorithm.lean @@ -80,6 +80,8 @@ components of the scheme in polynomial time, the correctness of one active call * `Cslib.Complexity.CountingSimulation.fastGuard_polyTime`: the guard is polynomial-time. * `Cslib.Complexity.CountingSimulation.wf_root`: guarded inputs have well-formed roots. * `Cslib.Complexity.CountingSimulation.fuel_le`: the clock on admissible inputs. +* `Cslib.Complexity.CountingSimulation.exists_clockedRun_le`: the budget of a clocked run, the + arithmetic shared with the machine for entry procedures (`CountingSimulation.exists_fastCore_le`). * `Cslib.Complexity.CountingSimulation.fastCertificate_le`: the fast machine within the interface's bounds. @@ -252,38 +254,101 @@ whose leaves take time at most `TL` and space at most `SL`, with `H` open calls, TL ≤ K * ((FastContraction.encInput (P, G)).length + 1) ^ K * 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) -/-- `c B ^ d ≤ c B ^ E X` for `1 ≤ B`, `d ≤ E` and `1 ≤ X`. -/ -private theorem lift_le {c B d E X : ℕ} (hB : 1 ≤ B) (hd : d ≤ E) (hX : 1 ≤ X) : - c * B ^ d ≤ c * B ^ E * X := - (Nat.mul_le_mul_left c (Nat.pow_le_pow_right hB hd)).trans (Nat.le_mul_of_pos_right _ hX) - -private theorem mul_succ_le_sq (H F : ℕ) : (H + 1) * (F + 1) ≤ (H + F + 1) ^ 2 := by nlinarith - -private theorem mul_add_one_le {c x : ℕ} (hx : 1 ≤ x) : c * x + 1 ≤ (c + 1) * x := by nlinarith - -/-- The arithmetic of the time bound. -/ -private theorem time_assemble - {capT runT cnT crT capL fuel Z TL Wb n R₁ R₂ Q W c₁ k₁ c₃ ka c₂ k₂ : ℕ} - (hrun : runT ≤ cnT + crT + 2 * capL + (fuel + 1) * (Z + TL + Wb)) - (hq : capT + cnT + crT + capL ≤ Q) (hQ : Q ≤ c₁ * W) - (hP1 : (fuel + 1) * Z ≤ 2 * k₁ * W) (hP2 : (fuel + 1) * TL ≤ 2 * ka * W) - (hP3 : (fuel + 1) * Wb ≤ 2 * c₃ * W) (hn : n + 1 ≤ 1 * W) (hR₁ : R₁ ≤ c₂ * W) - (hR₂ : R₂ ≤ k₂ * W) : - 2 * (capT + runT) + n + (R₁ + R₂) ≤ (6 * c₁ + 1 + 4 * k₁ + 4 * c₃ + 4 * ka + c₂ + k₂) * W := by - have e : (fuel + 1) * (Z + TL + Wb) = (fuel + 1) * Z + (fuel + 1) * TL + (fuel + 1) * Wb := by - ring - rw [e] at hrun - nlinarith - -/-- The arithmetic of the space bound. -/ -private theorem space_assemble - {capS runS cnS crS capL fb Z SL n R₁ R₂ Q W c₁ k₁ c₃ ka c₂ k₂ : ℕ} - (hrun : runS ≤ cnS + crS + 2 * capL + Z + SL + fb) - (hq : capS + cnS + crS + capL + fb ≤ Q) (hQ : Q ≤ c₁ * W) - (hZ : Z ≤ k₁ * W) (hSL : SL ≤ ka * W) (hn : n + 1 ≤ 1 * W) (hR₁ : R₁ ≤ c₂ * W) - (hR₂ : R₂ ≤ k₂ * W) : - 2 * (capS + runS) + n + (R₁ + R₂) ≤ (6 * c₁ + 1 + 4 * k₁ + 4 * c₃ + 4 * ka + c₂ + k₂) * W := by - nlinarith +/-- **The budget of a clocked run**, the arithmetic shared by the fast machines +(`CountingSimulation.fastCertificate_le`, `CountingSimulation.exists_fastCore_le`). Take a run +bounded as in `Cslib.GenericRAM.StackRecursion.Scheme.certificate_le` with constant `K₁`, whose +derivation has open calls, node sizes and leaf space at most `Ka B ^ Ka`, leaf time at most +`Ka B ^ Ka 2 ^ (Ka s / S)` and clock at most `2 ^ (kf s / S)`, for `B` above the input length +`n`; let the steps `pre` before it and the fuel and root machines cost at most `c B ^ d`, and the +output step `rest` at most `r₁ B ^ e₁ + r₂ B ^ e₂`. Then the steps, twice the run, the input +and the output step are at most `K B ^ K 2 ^ (K s / S)` in time and `K B ^ K` in space, for one +`K` depending only on the constants. -/ +theorem exists_clockedRun_le (K₁ Ka c d r₁ e₁ r₂ e₂ kf : ℕ) : + ∃ K : ℕ, ∀ {s S n B fuel H F TL SL A AS runT runS pre preS rest restS : ℕ}, n < B → + runT ≤ A + (fuel + 1) * (K₁ * ((H + 1) * (F + 1)) ^ K₁ + TL + + ((encNat fuel).length + 1) ^ 2) → + runS ≤ AS + K₁ * ((H + 1) * (F + 1)) ^ K₁ + SL + (encNat fuel).length → + pre + preS + A + AS + (encNat fuel).length ≤ c * B ^ d → + rest + restS ≤ r₁ * B ^ e₁ + r₂ * B ^ e₂ → fuel ≤ 2 ^ (kf * s / S) → + H + F + SL ≤ Ka * B ^ Ka → TL ≤ Ka * B ^ Ka * 2 ^ (Ka * s / S) → + pre + (2 * runT + n + rest) ≤ K * B ^ K * 2 ^ (K * s / S) ∧ + preS + (2 * runS + n + restS) ≤ K * B ^ K := by + set E := 2 * d + 2 * Ka * K₁ + Ka + e₁ + e₂ + 1 + set Z₀ := K₁ * (Ka + 1) ^ (2 * K₁) + set M := 4 * c + 4 * Z₀ + 4 * (c + 1) ^ 2 + 4 * Ka + r₁ + r₂ + 1 with hM + refine ⟨M + E + kf + Ka, fun {s S n B fuel H F TL SL A AS runT runS pre preS rest restS} + hn hrT hrS hpoly hrest hfuel hHFS hTL => ?_⟩ + have hBE {k : ℕ} (hk : k ≤ E) : B ^ k ≤ B ^ E := Nat.pow_le_pow_right (by omega) hk + have hB1 (k : ℕ) : 1 ≤ B ^ k := Nat.one_le_pow _ _ (by omega) + -- The pieces against `B ^ E`. + have hc : c * B ^ d ≤ c * B ^ E := Nat.mul_le_mul_left _ (hBE (by omega)) + have hr : r₁ * B ^ e₁ + r₂ * B ^ e₂ ≤ (r₁ + r₂) * B ^ E := by + rw [Nat.add_mul] + exact Nat.add_le_add (Nat.mul_le_mul_left _ (hBE (by omega))) + (Nat.mul_le_mul_left _ (hBE (by omega))) + have hB : B ≤ B ^ E := by simpa using hBE (k := 1) (by omega) + have hZ : K₁ * ((H + 1) * (F + 1)) ^ K₁ ≤ Z₀ * B ^ E := by + have h1 : H + F + 1 ≤ (Ka + 1) * B ^ Ka := by have := hB1 Ka; rw [add_one_mul]; omega + have h2 : (H + 1) * (F + 1) ≤ ((Ka + 1) * B ^ Ka) ^ 2 := + (Nat.mul_le_mul (by omega : H + 1 ≤ H + F + 1) (by omega : F + 1 ≤ H + F + 1)).trans + ((sq _).symm.le.trans (Nat.pow_le_pow_left h1 2)) + calc K₁ * ((H + 1) * (F + 1)) ^ K₁ ≤ K₁ * (((Ka + 1) * B ^ Ka) ^ 2) ^ K₁ := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left h2 _) + _ = Z₀ * B ^ (2 * Ka * K₁) := by + rw [mul_pow, ← pow_mul, mul_pow, ← pow_mul, ← pow_mul]; ring + _ ≤ Z₀ * B ^ E := Nat.mul_le_mul_left _ (hBE (by omega)) + have hL : ((encNat fuel).length + 1) ^ 2 ≤ (c + 1) ^ 2 * B ^ E := by + calc ((encNat fuel).length + 1) ^ 2 ≤ ((c + 1) * B ^ d) ^ 2 := + Nat.pow_le_pow_left (by have := hB1 d; rw [add_one_mul]; omega) 2 + _ = (c + 1) ^ 2 * B ^ (2 * d) := by ring + _ ≤ (c + 1) ^ 2 * B ^ E := Nat.mul_le_mul_left _ (hBE (by omega)) + have hKa : Ka * B ^ Ka ≤ Ka * B ^ E := Nat.mul_le_mul_left _ (hBE (by omega)) + -- The space. + have hspace : preS + (2 * runS + n + restS) ≤ M * B ^ E := by + have e : M * B ^ E = 4 * (c * B ^ E) + 4 * (Z₀ * B ^ E) + 4 * ((c + 1) ^ 2 * B ^ E) + + 4 * (Ka * B ^ E) + (r₁ + r₂) * B ^ E + B ^ E := by rw [hM]; ring + omega + -- The time, against `W = B ^ E X` with `X ≥ 2 ^ (kf s / S) 2 ^ (Ka s / S)`. + set Xf := 2 ^ (kf * s / S) + set Xa := 2 ^ (Ka * s / S) + set X := 2 ^ ((kf + Ka) * s / S) + have hXf : 1 ≤ Xf := Nat.one_le_two_pow + have hXa : 1 ≤ Xa := Nat.one_le_two_pow + have hX : Xf * Xa ≤ X := by + rw [← pow_add] + exact Nat.pow_le_pow_right (by norm_num) (Nat.div_add_div_le_add_div.trans (by rw [add_mul])) + have hXfX : Xf ≤ X := (Nat.le_mul_of_pos_right _ hXa).trans hX + set W := B ^ E * X + have hEW (a : ℕ) : a * B ^ E ≤ a * W := + Nat.mul_le_mul_left _ (Nat.le_mul_of_pos_right _ (hXf.trans hXfX)) + have hfuel1 : fuel + 1 ≤ 2 * Xf := by omega + have hP1 : (fuel + 1) * (K₁ * ((H + 1) * (F + 1)) ^ K₁) ≤ 2 * (Z₀ * W) := + calc _ ≤ 2 * Xf * (Z₀ * B ^ E) := Nat.mul_le_mul hfuel1 hZ + _ = 2 * (Z₀ * (B ^ E * Xf)) := by ring + _ ≤ 2 * (Z₀ * W) := + Nat.mul_le_mul_left _ (Nat.mul_le_mul_left _ (Nat.mul_le_mul_left _ hXfX)) + have hP2 : (fuel + 1) * TL ≤ 2 * (Ka * W) := + calc _ ≤ 2 * Xf * (Ka * B ^ E * Xa) := + Nat.mul_le_mul hfuel1 (hTL.trans (Nat.mul_le_mul_right _ hKa)) + _ = 2 * (Ka * (B ^ E * (Xf * Xa))) := by ring + _ ≤ 2 * (Ka * W) := Nat.mul_le_mul_left _ (Nat.mul_le_mul_left _ (Nat.mul_le_mul_left _ hX)) + have hP3 : (fuel + 1) * ((encNat fuel).length + 1) ^ 2 ≤ 2 * ((c + 1) ^ 2 * W) := + calc _ ≤ 2 * Xf * ((c + 1) ^ 2 * B ^ E) := Nat.mul_le_mul hfuel1 hL + _ = 2 * ((c + 1) ^ 2 * (B ^ E * Xf)) := by ring + _ ≤ 2 * ((c + 1) ^ 2 * W) := + Nat.mul_le_mul_left _ (Nat.mul_le_mul_left _ (Nat.mul_le_mul_left _ hXfX)) + have htime : pre + (2 * runT + n + rest) ≤ M * W := by + have e : M * W = 4 * (c * W) + 4 * (Z₀ * W) + 4 * ((c + 1) ^ 2 * W) + 4 * (Ka * W) + + (r₁ + r₂) * W + 1 * W := by rw [hM]; ring + rw [Nat.mul_add, Nat.mul_add] at hrT + have := hEW c; have := hEW (r₁ + r₂); have := hEW 1 + omega + have hMK : M ≤ M + E + kf + Ka := by omega + have hEK : B ^ E ≤ B ^ (M + E + kf + Ka) := Nat.pow_le_pow_right (by omega) (by omega) + refine ⟨htime.trans ?_, hspace.trans (Nat.mul_le_mul hMK hEK)⟩ + rw [← Nat.mul_assoc] + exact Nat.mul_le_mul (Nat.mul_le_mul hMK hEK) + (Nat.pow_le_pow_right (by norm_num) (Nat.div_le_div_right (Nat.mul_le_mul_right _ (by omega)))) variable {mk} @@ -320,70 +385,22 @@ theorem fastCertificate_le (ComputableInPolyTime.fst FastContraction.encInput encValue) obtain ⟨c₂, d₂, h₂⟩ := (((((htP.1.add htP.2).add hdP.1).add hdP.2).add hfP.1).add hfP.2).exists_le - -- The constants. - set E := 2 * d₁ + 2 * Ka * K₁ + (Ka + 1) * d₂ + K₂ + Ka + 1 with hE - set Kc := 6 * c₁ + 1 + 4 * K₁ * (Ka + 1) ^ (2 * K₁) + 4 * (c₁ + 1) ^ 2 + 4 * Ka + - c₂ * (Ka + 2) ^ d₂ + K₂ * 2 ^ (C * s₀) with hKc - refine ⟨Kc + E + FastContraction.fuelConst * (C + D) + Ka, fun s P G hs hP hPD hA hg => ?_⟩ + obtain ⟨K, hK⟩ := exists_clockedRun_le K₁ Ka (4 * c₁) d₁ (2 * (c₂ * (Ka + 2) ^ d₂)) + ((Ka + 1) * d₂) (2 * (K₂ * 2 ^ (C * s₀))) K₂ (FastContraction.fuelConst * (C + D)) + refine ⟨K, fun s P G hs hP hPD hA hg => ?_⟩ obtain ⟨I, N, H, F, TL, SL, he, hN, hnode, hframe, hvalue, hHFS, hTL⟩ := hKa s P G hs hP hPD hA hg - set q : ℕ × ℕ × ExplicitTensorNetwork ℕ := (P, G) with hq - set n := (FastContraction.encInput q).length with hn - set B := n + 1 with hB - have hB1 : 1 ≤ B := by omega - set S := Nat.sqrt (Nat.log 2 s) - set Xf := 2 ^ (FastContraction.fuelConst * (C + D) * s / S) - set Xa := 2 ^ (Ka * s / S) - set X := 2 ^ ((FastContraction.fuelConst * (C + D) + Ka) * s / S) - have hXf : 1 ≤ Xf := Nat.one_le_two_pow - have hXa : 1 ≤ Xa := Nat.one_le_two_pow - have hXfX : Xf ≤ X := Nat.pow_le_pow_right (by norm_num) - (Nat.div_le_div_right (Nat.mul_le_mul_right _ (by omega))) - have hXfXa : Xf * Xa ≤ X := by - rw [← pow_add] - refine Nat.pow_le_pow_right (by norm_num) (Nat.div_add_div_le_add_div.trans ?_) - rw [add_mul] - have hX1 : 1 ≤ X := Nat.one_le_two_pow - -- The run. + set q : ℕ × ℕ × ExplicitTensorNetwork ℕ := (P, G) + have hq1 := h₁ q + obtain ⟨hdT, hdS⟩ := hK₂ q + set B := (FastContraction.encInput q).length + 1 with hB obtain ⟨hrT, hrS⟩ := hK₁ (NativeCertificate.ofPolyTime fuel_polyTime) (NativeCertificate.ofPolyTime root_polyTime) I F TL SL hnode hframe hvalue (ExplicitTensorNetwork.capPrecision q) _ N H he - have hfuel : FastContraction.fuel (ExplicitTensorNetwork.capPrecision q) ≤ Xf := - fuel_le hA hs hPD - have hq1 := h₁ q have hrT' : (runCertificate hpoly).time (ExplicitTensorNetwork.capPrecision q) ≤ _ := hrT have hrS' : (runCertificate hpoly).space (ExplicitTensorNetwork.capPrecision q) ≤ _ := hrS - -- Polynomial pieces. - set Q₁ := c₁ * B ^ d₁ with hQ₁ - have hBK (k : ℕ) : 1 ≤ B ^ k := Nat.one_le_pow _ _ (by omega) - have hHF : (H + 1) * (F + 1) ≤ ((Ka + 1) * B ^ Ka) ^ 2 := by - have h1 : H + F ≤ Ka * B ^ Ka := by have := hHFS; omega - have h2 := hBK Ka - calc (H + 1) * (F + 1) ≤ (H + F + 1) ^ 2 := mul_succ_le_sq H F - _ ≤ (Ka * B ^ Ka + B ^ Ka) ^ 2 := Nat.pow_le_pow_left (by omega) 2 - _ = ((Ka + 1) * B ^ Ka) ^ 2 := by ring - have hZ : K₁ * ((H + 1) * (F + 1)) ^ K₁ ≤ K₁ * (Ka + 1) ^ (2 * K₁) * B ^ (2 * Ka * K₁) := by - calc K₁ * ((H + 1) * (F + 1)) ^ K₁ ≤ K₁ * (((Ka + 1) * B ^ Ka) ^ 2) ^ K₁ := - Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hHF _) - _ = K₁ * (Ka + 1) ^ (2 * K₁) * B ^ (2 * Ka * K₁) := by - rw [mul_pow, ← pow_mul, mul_pow, ← pow_mul, ← pow_mul, - show Ka * 2 * K₁ = 2 * Ka * K₁ by ring] - ring - have hW : ((encNat (FastContraction.fuel (ExplicitTensorNetwork.capPrecision q))).length + 1) ^ 2 - ≤ (c₁ + 1) ^ 2 * B ^ (2 * d₁) := by - have h1 : (encNat (FastContraction.fuel (ExplicitTensorNetwork.capPrecision q))).length ≤ Q₁ := - by omega - have h2 := hBK d₁ - calc _ ≤ (Q₁ + 1) ^ 2 := Nat.pow_le_pow_left (by omega) 2 - _ ≤ ((c₁ + 1) * B ^ d₁) ^ 2 := Nat.pow_le_pow_left (mul_add_one_le h2) 2 - _ = (c₁ + 1) ^ 2 * B ^ (2 * d₁) := by ring - have hTL' : TL ≤ Ka * B ^ Ka * Xa := hTL - have hF : F ≤ Ka * B ^ Ka := by have := hHFS; omega - have hSL : SL ≤ Ka * B ^ Ka := by have := hHFS; omega - -- Decoding and direct summation. - set R₁ := c₂ * (Ka + 2) ^ d₂ * B ^ ((Ka + 1) * d₂) with hR₁ - set R₂ := K₂ * 2 ^ (C * s₀) * B ^ K₂ with hR₂ - have hdec : ∀ v : ℕ × List ℕ, I.value v → + -- Decoding a value of the run, and direct summation below `s₀`. + have hdec (v : ℕ × List ℕ) (hv : I.value v) : (NativeCertificate.ofPolyTime tag_polyTime).time (q, v) + (NativeCertificate.ofPolyTime tag_polyTime).space (q, v) + (NativeCertificate.ofPolyTime decode_polyTime).time (q, v) + @@ -391,149 +408,65 @@ theorem fastCertificate_le (NativeCertificate.ofPolyTime (ComputableInPolyTime.fst FastContraction.encInput encValue)).time (q, v) + (NativeCertificate.ofPolyTime - (ComputableInPolyTime.fst FastContraction.encInput encValue)).space (q, v) ≤ R₁ := by - intro v hv - have h := h₂ (q, v) - have hv' := hvalue v hv - have hk1 : B ≤ B ^ (Ka + 1) := by - calc B = B ^ 1 := (pow_one B).symm - _ ≤ B ^ (Ka + 1) := Nat.pow_le_pow_right hB1 (by omega) - have hk2 : B ^ Ka ≤ B ^ (Ka + 1) := Nat.pow_le_pow_right hB1 (by omega) - have hlen : (encPair FastContraction.encInput encValue (q, v)).length + 1 ≤ - (Ka + 2) * B ^ (Ka + 1) := by - have hl := length_encPair (enc₁ := FastContraction.encInput) (enc₂ := encValue) (q, v) - simp only at hl - rw [hl] - have : Ka * B ^ Ka ≤ Ka * B ^ (Ka + 1) := Nat.mul_le_mul_left _ hk2 - have e : (Ka + 2) * B ^ (Ka + 1) = Ka * B ^ (Ka + 1) + 2 * B ^ (Ka + 1) := by ring - omega - calc _ ≤ c₂ * ((encPair FastContraction.encInput encValue (q, v)).length + 1) ^ d₂ := h - _ ≤ c₂ * ((Ka + 2) * B ^ (Ka + 1)) ^ d₂ := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hlen _) - _ = R₁ := by rw [hR₁, mul_pow, ← pow_mul, Nat.mul_assoc] - obtain ⟨hdT, hdS⟩ := hK₂ q - have hm : q.2.2.numEdges ≤ C * s := hA.2.1 + (ComputableInPolyTime.fst FastContraction.encInput encValue)).space (q, v) ≤ + c₂ * (Ka + 2) ^ d₂ * B ^ ((Ka + 1) * d₂) := by + refine (h₂ (q, v)).trans ?_ + rw [Nat.mul_assoc, pow_mul, ← mul_pow] + refine Nat.mul_le_mul_left _ (Nat.pow_le_pow_left ?_ _) + have := hvalue v hv + have hB1 : B ≤ B ^ (Ka + 1) := Nat.le_self_pow (by omega) _ + have hBK := Nat.mul_le_mul_left Ka + (Nat.pow_le_pow_right (by omega : 1 ≤ B) (by omega : Ka ≤ Ka + 1)) + simp only [length_encPair (enc₁ := FastContraction.encInput) (enc₂ := encValue), add_mul] + omega + have h2 : 1 ≤ 2 ^ (C * s₀) := Nat.one_le_two_pow have hdir (hs₀ : s < s₀) : - ExplicitTensorNetwork.directContractionBinaryCertificate.time q ≤ R₂ := by - refine hdT.trans ?_ - have h2 : 2 ^ q.2.2.numEdges ≤ 2 ^ (C * s₀) := - Nat.pow_le_pow_right (by norm_num) (hm.trans (Nat.mul_le_mul_left _ hs₀.le)) - calc K₂ * ((encInput q).length + 1) ^ K₂ * 2 ^ q.2.2.numEdges - ≤ K₂ * B ^ K₂ * 2 ^ (C * s₀) := Nat.mul_le_mul_left _ h2 - _ = R₂ := by rw [hR₂]; ring - have hdirS : ExplicitTensorNetwork.directContractionBinaryCertificate.space q ≤ R₂ := - hdS.trans (by - rw [hR₂] - calc K₂ * ((encInput q).length + 1) ^ K₂ ≤ - K₂ * ((encInput q).length + 1) ^ K₂ * 2 ^ (C * s₀) := - Nat.le_mul_of_pos_right _ Nat.one_le_two_pow - _ = K₂ * 2 ^ (C * s₀) * B ^ K₂ := by ring) + ExplicitTensorNetwork.directContractionBinaryCertificate.time q ≤ + K₂ * 2 ^ (C * s₀) * B ^ K₂ := by + refine hdT.trans (le_of_le_of_eq (Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by norm_num) + (hA.2.1.trans (Nat.mul_le_mul_left _ hs₀.le)))) (by ring)) + have hdirS : ExplicitTensorNetwork.directContractionBinaryCertificate.space q ≤ + K₂ * 2 ^ (C * s₀) * B ^ K₂ := + hdS.trans (le_of_le_of_eq (Nat.le_mul_of_pos_right _ h2) (by ring)) have hbig : s₀ ≤ s → (scheme tableEntry mk).run fuel root (ExplicitTensorNetwork.capPrecision q) = some (0, value tableEntry mk (root (ExplicitTensorNetwork.capPrecision q))) := fun h => Scheme.run_eq_some he (hN h) - clear hKa hK₁ hK₂ h₁ h₂ - -- Everything against `W = B ^ E X`. - set W := B ^ E * X with hWdef - have lift {c d : ℕ} (hd : d ≤ E) : c * B ^ d ≤ c * W := by - rw [hWdef, ← Nat.mul_assoc]; exact lift_le hB1 hd hX1 - have lift' {c d : ℕ} (hd : d ≤ E) : c * B ^ d ≤ c * B ^ E := - Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hB1 hd) - have hQW : Q₁ ≤ c₁ * W := lift (by omega) - have hR₁W : R₁ ≤ c₂ * (Ka + 2) ^ d₂ * W := lift (by omega) - have hR₂W : R₂ ≤ K₂ * 2 ^ (C * s₀) * W := lift (by omega) - have hnW : n + 1 ≤ 1 * W := by - have := lift (c := 1) (d := 1) (by omega); rw [pow_one] at this; omega - have hfuel1 : FastContraction.fuel (ExplicitTensorNetwork.capPrecision q) + 1 ≤ 2 * Xf := by - omega - have hP1 : (FastContraction.fuel (ExplicitTensorNetwork.capPrecision q) + 1) * - (K₁ * ((H + 1) * (F + 1)) ^ K₁) ≤ 2 * (K₁ * (Ka + 1) ^ (2 * K₁)) * W := by - calc _ ≤ (2 * Xf) * (K₁ * (Ka + 1) ^ (2 * K₁) * B ^ (2 * Ka * K₁)) := - Nat.mul_le_mul hfuel1 hZ - _ = 2 * (K₁ * (Ka + 1) ^ (2 * K₁)) * (B ^ (2 * Ka * K₁) * Xf) := by ring - _ ≤ 2 * (K₁ * (Ka + 1) ^ (2 * K₁)) * W := Nat.mul_le_mul_left _ - (Nat.mul_le_mul (Nat.pow_le_pow_right hB1 (by omega)) hXfX) - have hP2 : (FastContraction.fuel (ExplicitTensorNetwork.capPrecision q) + 1) * TL ≤ - 2 * Ka * W := by - calc _ ≤ (2 * Xf) * (Ka * B ^ Ka * Xa) := Nat.mul_le_mul hfuel1 hTL' - _ = 2 * Ka * (B ^ Ka * (Xf * Xa)) := by ring - _ ≤ 2 * Ka * W := Nat.mul_le_mul_left _ - (Nat.mul_le_mul (Nat.pow_le_pow_right hB1 (by omega)) hXfXa) - have hP3 : (FastContraction.fuel (ExplicitTensorNetwork.capPrecision q) + 1) * - ((encNat (FastContraction.fuel (ExplicitTensorNetwork.capPrecision q))).length + 1) ^ 2 ≤ - 2 * (c₁ + 1) ^ 2 * W := by - calc _ ≤ (2 * Xf) * ((c₁ + 1) ^ 2 * B ^ (2 * d₁)) := Nat.mul_le_mul hfuel1 hW - _ = 2 * (c₁ + 1) ^ 2 * (B ^ (2 * d₁) * Xf) := by ring - _ ≤ 2 * (c₁ + 1) ^ 2 * W := Nat.mul_le_mul_left _ - (Nat.mul_le_mul (Nat.pow_le_pow_right hB1 (by omega)) hXfX) - have hZE : K₁ * ((H + 1) * (F + 1)) ^ K₁ ≤ K₁ * (Ka + 1) ^ (2 * K₁) * B ^ E := - hZ.trans (lift' (by omega)) - have hQE : Q₁ ≤ c₁ * B ^ E := lift' (by omega) - have hR₁E : R₁ ≤ c₂ * (Ka + 2) ^ d₂ * B ^ E := lift' (by omega) - have hR₂E : R₂ ≤ K₂ * 2 ^ (C * s₀) * B ^ E := lift' (by omega) - have hSLE : SL ≤ Ka * B ^ E := hSL.trans (lift' (by omega)) - have hnE : n + 1 ≤ 1 * B ^ E := by - have := lift' (c := 1) (d := 1) (by omega); rw [pow_one] at this; omega - have hKK : Kc ≤ Kc + E + FastContraction.fuelConst * (C + D) + Ka := by omega - have hBE : B ^ E ≤ B ^ (Kc + E + FastContraction.fuelConst * (C + D) + Ka) := - Nat.pow_le_pow_right hB1 (by omega) - have hXK : X ≤ 2 ^ ((Kc + E + FastContraction.fuelConst * (C + D) + Ka) * s / S) := - Nat.pow_le_pow_right (by norm_num) (Nat.div_le_div_right (Nat.mul_le_mul_right _ (by omega))) - refine ⟨?_, ?_⟩ - · rw [fastCertificate_time] - have hrest : ((scheme tableEntry mk).run fuel root (ExplicitTensorNetwork.capPrecision q)).elim + have hrest : ((scheme tableEntry mk).run fuel root (ExplicitTensorNetwork.capPrecision q)).elim (ExplicitTensorNetwork.directContractionBinaryCertificate.time q) (fun v => (NativeCertificate.ofPolyTime tag_polyTime).time (q, v) + if decide (v.1 = 0) = true then (NativeCertificate.ofPolyTime decode_polyTime).time (q, v) else (NativeCertificate.ofPolyTime (ComputableInPolyTime.fst FastContraction.encInput encValue)).time (q, v) + - ExplicitTensorNetwork.directContractionBinaryCertificate.time q) ≤ R₁ + R₂ := by - rcases hr : (scheme tableEntry mk).run fuel root - (ExplicitTensorNetwork.capPrecision q) with _ | v - · by_cases hs₀ : s₀ ≤ s - · rw [hbig hs₀] at hr; cases hr - · simp only [Option.elim_none]; have := hdir (by omega); omega - · have hd := hdec v (Scheme.value_of_run_eq_some he hr) - simp only [Option.elim_some] - split_ifs with h0 - · omega - · by_cases hs₀ : s₀ ≤ s - · rw [hbig hs₀] at hr; cases hr; simp at h0 - · have := hdir (by omega); omega - have htot := time_assemble (capT := (NativeCertificate.ofPolyTime - ExplicitTensorNetwork.capPrecision_polyTime).time q) hrT' (by omega) hQW hP1 hP2 - hP3 hnW hR₁W hR₂W - have hKc' : Kc = 6 * c₁ + 1 + 4 * (K₁ * (Ka + 1) ^ (2 * K₁)) + 4 * (c₁ + 1) ^ 2 + 4 * Ka + - c₂ * (Ka + 2) ^ d₂ + K₂ * 2 ^ (C * s₀) := by rw [hKc]; ring - rw [← hKc'] at htot - calc _ ≤ _ := Nat.add_le_add_left hrest _ - _ ≤ Kc * W := htot - _ ≤ _ := by - rw [hWdef, ← Nat.mul_assoc] - exact Nat.mul_le_mul (Nat.mul_le_mul hKK hBE) hXK - · rw [fastCertificate_space] - have hrest : ((scheme tableEntry mk).run fuel root (ExplicitTensorNetwork.capPrecision q)).elim + ExplicitTensorNetwork.directContractionBinaryCertificate.time q) + + ((scheme tableEntry mk).run fuel root (ExplicitTensorNetwork.capPrecision q)).elim (ExplicitTensorNetwork.directContractionBinaryCertificate.space q) (fun v => (NativeCertificate.ofPolyTime tag_polyTime).space (q, v) + if decide (v.1 = 0) = true then (NativeCertificate.ofPolyTime decode_polyTime).space (q, v) else (NativeCertificate.ofPolyTime (ComputableInPolyTime.fst FastContraction.encInput encValue)).space (q, v) + - ExplicitTensorNetwork.directContractionBinaryCertificate.space q) ≤ R₁ + R₂ := by - rcases hr : (scheme tableEntry mk).run fuel root - (ExplicitTensorNetwork.capPrecision q) with _ | v - · simp only [Option.elim_none]; omega - · have hd := hdec v (Scheme.value_of_run_eq_some he hr) - simp only [Option.elim_some] - split_ifs <;> omega - have htot := space_assemble (capS := (NativeCertificate.ofPolyTime - ExplicitTensorNetwork.capPrecision_polyTime).space q) (c₃ := (c₁ + 1) ^ 2) hrS' - (by omega) hQE hZE hSLE hnE hR₁E hR₂E - have hKc' : Kc = 6 * c₁ + 1 + 4 * (K₁ * (Ka + 1) ^ (2 * K₁)) + 4 * (c₁ + 1) ^ 2 + 4 * Ka + - c₂ * (Ka + 2) ^ d₂ + K₂ * 2 ^ (C * s₀) := by rw [hKc]; ring - rw [← hKc'] at htot - calc _ ≤ _ := Nat.add_le_add_left hrest _ - _ ≤ Kc * B ^ E := htot - _ ≤ _ := Nat.mul_le_mul hKK hBE + ExplicitTensorNetwork.directContractionBinaryCertificate.space q) ≤ + 2 * (c₂ * (Ka + 2) ^ d₂) * B ^ ((Ka + 1) * d₂) + 2 * (K₂ * 2 ^ (C * s₀)) * B ^ K₂ := by + rw [Nat.mul_assoc 2, Nat.mul_assoc 2] + rcases hr : (scheme tableEntry mk).run fuel root (ExplicitTensorNetwork.capPrecision q) + with _ | v + · have hs₀ : s < s₀ := Nat.lt_of_not_le fun h => by rw [hbig h] at hr; cases hr + have := hdir hs₀ + simp only [Option.elim_none]; omega + · have hd := hdec v (Scheme.value_of_run_eq_some he hr) + simp only [Option.elim_some] + split_ifs with h0 + · omega + · have hs₀ : s < s₀ := Nat.lt_of_not_le fun h => by + rw [hbig h] at hr; cases hr; simp at h0 + have := hdir hs₀; omega + rw [fastCertificate_time, fastCertificate_space] + exact (hK (n := (FastContraction.encInput q).length) + (pre := 2 * (NativeCertificate.ofPolyTime ExplicitTensorNetwork.capPrecision_polyTime).time q) + (preS := 2 * (NativeCertificate.ofPolyTime ExplicitTensorNetwork.capPrecision_polyTime).space q) + (by omega) hrT' hrS' (by rw [Nat.mul_assoc]; omega) hrest (fuel_le hA hs hPD) hHFS hTL).imp + (fun h => by omega) fun h => by omega /-- **The contraction algorithm from the fast machine**, given its remaining obligations: polynomial-time components of the scheme, the correctness of one active From 1e047d6c155e588656b890f0c99bb257461be918 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 1 Nov 2026 14:30:13 -0500 Subject: [PATCH 2/2] style: wrap a long line Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Circuit/Frontier/TensorNetwork/DescribedContraction.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedContraction.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedContraction.lean index 4f37457f9c..f3911873cb 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedContraction.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedContraction.lean @@ -833,9 +833,8 @@ theorem contractionCertificate_le [Inhabited Y] (hops : ops.PolyTime encQ encY) obtain ⟨hq, -, -, -⟩ := hx rw [hq] at hmem have h3 := hvlen v hmem - have hxv {c e : ℕ} : - c * ((encPair (encNode encQ encT) (encPair (encList encNat) encT) (x, v)).length + 1) ^ e ≤ - c * (11 * z + 16) ^ e := by + have hxv {c e : ℕ} : c * ((encPair (encNode encQ encT) (encPair (encList encNat) encT) + (x, v)).length + 1) ^ e ≤ c * (11 * z + 16) ^ e := by refine Nat.mul_le_mul_left _ (Nat.pow_le_pow_left ?_ _) have := length_encPair (enc₁ := encNode encQ encT) (enc₂ := encPair (encList encNat) encT) (x, v)