diff --git a/Complexity/Algorithms/Lean/Karger/Contraction.lean b/Complexity/Algorithms/Lean/Karger/Contraction.lean index 4a198db794..adce16a1fd 100644 --- a/Complexity/Algorithms/Lean/Karger/Contraction.lean +++ b/Complexity/Algorithms/Lean/Karger/Contraction.lean @@ -9,6 +9,7 @@ module public import Complexity.Algorithms.WordRAM.Karger.Graph public import Complexity.DataStructure.StateTransition.Randomized +public import Complexity.Languages.Probabilistic.Iteration /-! # Karger's contraction algorithm as a randomized client @@ -34,25 +35,35 @@ and answers half their total weight, the weight of the cut between them. All probability is proved here, on the specification. Contracting from `t + s` down to `t` supervertices preserves a fixed minimum cut with probability at least `t (t - 1) / ((t + s) (t + s - 1))` (`survives_contractTimes`), so `karger` answers the minimum cut -weight with probability at least `2 / (n (n - 1))` (`two_div_le_toOuterMeasure_karger`), and never -less than it (`minCut_le_of_mem_support_karger`). Every call it makes is admissible +weight with probability at least `2 / (n (n - 1))` (`two_div_le_toOuterMeasure_karger`), and every +answer is the weight of a non-trivial cut (`exists_cut_of_mem_support_answerLaw`), never less than +the minimum (`minCut_le_of_mem_support_karger`). Every call it makes is admissible (`demonicValid_karger`). The combinatorics and the one-step bound are `Karger.Graph`'s (`isContractionOf_contract`, `pullbackCut_contractCut`, `step_survival_prob_ge`, `telescope_survival_step`), used unchanged, and the composition of the stages is `Probability.PMF.toOuterMeasure_bind_ge_mul_ennreal`. +Amplification is a client of a trial oracle whose one call answers one run of `karger`: +`minRuns R` makes `R` calls and keeps the least answer, one `minStep` per call after the first. +Answered by independent runs, `OracleComp.evalWith (fun _ => answerLaw G)`, it misses the minimum +cut weight with probability at most `(1 - 2 / (n (n - 1))) ^ R` (`minRuns_ne_minCut_le`), since +the least answer misses it only when every run does (`minRuns_ne_le`, for any trial). + No register, address or instruction count appears here. The word-RAM loop `Cslib.Algorithms.WordRAM.Karger.contractDownTo` simulates `contractTimes`: the graph it holds has the law of the client's final state (`Cslib.Algorithms.WordRAM.Karger.contractDownTo_law`), so its -survival bound is `survives_contractTimes`. An implementation of `spec` over the memory oracle is a -separate, deterministic hop, and `Refinement.toRandomized` with `RandomizedRefinement.withCoins` -carries the law of the client through it. +survival bound is `survives_contractTimes`. The programs of `Cslib.Algorithms.WordRAM.KargerMinCut` +simulate `karger` and `minRuns` in the same way. An implementation of `spec` over the memory +oracle is a separate, deterministic hop, and `Refinement.toRandomized` with +`RandomizedRefinement.withCoins` carries the law of the client through it. ## Main definitions * `Graph`, `Op`, `step`, `valid`, `spec`: the contraction structure. * `sampledPair`, `contractGraph`: the pair sampled at an offset, and contraction. * `contractStep`, `contractTimes`, `karger`: the algorithm as a client with coins. +* `answerLaw`: the law of the answer of one run of `karger`. +* `minStep`, `minRuns`: amplification, as a client of a trial oracle. * `Survives`: a cut of the input survives in a contracted graph. ## Main results @@ -61,8 +72,15 @@ carries the law of the client through it. step that an implementation simulates. * `survives_contractTimes`: the survival bound. * `two_div_le_toOuterMeasure_karger`: Karger's success probability. -* `isContractionOf_of_mem_support_contractTimes`, `minCut_le_of_mem_support_karger`: every - outcome is a contraction, so the answer is never below the minimum cut weight. +* `isContractionOf_of_mem_support_contractTimes`, `exists_cut_of_mem_support_answerLaw`, + `minCut_le_of_mem_support_karger`: every outcome is a contraction, so the answer is the weight + of a non-trivial cut, never below the minimum. +* `answerLaw_eq`: the answer is half the total weight of the graph left by `n - 2` contractions. +* `minRuns_ne_minCut_le`: amplified Karger, `R` independent runs miss with probability at most + `(1 - 2 / (n (n - 1))) ^ R`. +* `mem_support_iterate_minStep`, `mem_support_minRuns`: every amplified answer is the answer of + one of the runs. +* `minRuns_ne_le`: amplification of any trial whose answers are at least `m`. * `isCostBounded_contractStep`, `isCostBounded_contractTimes`: each contraction makes one coin call and at most four calls of the structure. * `demonicValid_contractTimes`, `demonicValid_karger`: every call is admissible. @@ -305,15 +323,15 @@ theorem isContractionOf_of_mem_support_contractTimes {n t : ℕ} (ht : 1 ≤ t) rw [sampledPair_eq hsamp, contractGraph_fin] at hx exact ih (isContractionOf_contract hC (isSampledPair_ne hC.multigraph hsamp)) hx -/-- Running `karger` from `n = 2 + s` supervertices contracts `s` times, then answers half the -total weight. -/ -private theorem run_karger {s : ℕ} (W : Fin (2 + s) → Fin (2 + s) → ℕ) : - spec.toRandomized.withCoins.run karger ⟨2 + s, W⟩ = - (spec.toRandomized.withCoins.run (contractTimes s) ⟨2 + s, W⟩).bind fun x => +/-- Running `karger` from `n` supervertices contracts `n - 2` times, then answers half the total +weight. -/ +private theorem run_karger {n : ℕ} (W : Fin n → Fin n → ℕ) : + spec.toRandomized.withCoins.run karger ⟨n, W⟩ = + (spec.toRandomized.withCoins.run (contractTimes (n - 2)) ⟨n, W⟩).bind fun x => PMF.pure (totalDoubledWeight x.2.weight / 2, x.2) := by rw [karger, StateTransitionSpec.run_withCoins_query_bind] dsimp only [StateTransitionSpec.stepFn, step] - rw [Nat.add_sub_cancel_left, RandomizedSpec.run_bind] + rw [RandomizedSpec.run_bind] exact congrArg _ (funext fun ⟨_, G⟩ => StateTransitionSpec.run_withCoins_query_bind (D := spec) Op.total (fun S => pure (S / 2)) G) @@ -331,7 +349,7 @@ theorem two_div_le_toOuterMeasure_karger {n : ℕ} (hn : 2 ≤ n) {W₀ : Fin n have hsurv := survives_contractTimes le_rfl hmin s (isContractionOf_id hW₀) hC (by rw [hid, hCmin]) rw [hid] at hsurv - rw [run_karger, show (2 : ℝ≥0∞) / ((2 + s) * (2 + s - 1) : ℕ) = + rw [run_karger, Nat.add_sub_cancel_left, show (2 : ℝ≥0∞) / ((2 + s) * (2 + s - 1) : ℕ) = ((2 * (2 - 1) : ℕ) : ℝ≥0∞) / ((2 + s) * (2 + s - 1) : ℕ) * 1 by norm_num] refine Probability.PMF.toOuterMeasure_bind_ge_mul_ennreal _ _ _ _ hsurv fun x _ ⟨W', part', B', hx, hC', hpb⟩ => ?_ @@ -343,24 +361,146 @@ theorem two_div_le_toOuterMeasure_karger {n : ℕ} (hn : 2 ≤ n) {W₀ : Fin n rw [totalDoubledWeight_fin_two hC'.multigraph, ← hcut] omega +/-- The law of the answer of one run of `karger` on `G`. -/ +noncomputable def answerLaw (G : Graph) : PMF ℕ := + (spec.toRandomized.withCoins.run karger G).map Prod.fst + +/-- The answer of `karger` is half the total weight of the graph that `n - 2` contractions leave. -/ +theorem answerLaw_eq {n : ℕ} (W : Fin n → Fin n → ℕ) : + answerLaw ⟨n, W⟩ = ((spec.toRandomized.withCoins.run (contractTimes (n - 2)) ⟨n, W⟩).map + Prod.snd).map fun G => totalDoubledWeight G.weight / 2 := by + rw [answerLaw, run_karger, PMF.map_comp, PMF.map_bind] + simp only [PMF.pure_map] + exact PMF.bind_pure_comp _ _ + +/-- Every answer of `karger` on a multigraph with `n ≥ 2` vertices is the weight of a non-trivial +cut. -/ +theorem exists_cut_of_mem_support_answerLaw {n : ℕ} (hn : 2 ≤ n) {W₀ : Fin n → Fin n → ℕ} + (hW₀ : IsMultigraph W₀) {v : ℕ} (hv : v ∈ (answerLaw ⟨n, W₀⟩).support) : + ∃ C : Finset (Fin n), IsNonTrivialCut C ∧ v = cutWeight W₀ C := by + obtain ⟨s, rfl⟩ : ∃ s, n = 2 + s := ⟨n - 2, by omega⟩ + rw [answerLaw_eq, PMF.map_comp, PMF.mem_support_map_iff, Nat.add_sub_cancel_left] at hv + obtain ⟨x, hx, rfl⟩ := hv + obtain ⟨W', part', hx', hC'⟩ := + isContractionOf_of_mem_support_contractTimes (t := 2) (by norm_num) s + (isContractionOf_id hW₀) hx + obtain ⟨hnt, hcw, -⟩ := two_vertex_contraction_output hC' + refine ⟨_, hnt, ?_⟩ + change totalDoubledWeight x.2.weight / 2 = _ + rw [hx'] + change totalDoubledWeight W' / 2 = _ + rw [totalDoubledWeight_fin_two hC'.multigraph, ← hcw] + omega + /-- **One-sided error.** Every answer of `karger` on a multigraph with `n ≥ 2` vertices is the weight of a non-trivial cut, so it is never below the minimum cut weight. -/ theorem minCut_le_of_mem_support_karger {n : ℕ} (hn : 2 ≤ n) {W₀ : Fin n → Fin n → ℕ} (hW₀ : IsMultigraph W₀) {x : ℕ × Graph} (hx : x ∈ (spec.toRandomized.withCoins.run karger ⟨n, W₀⟩).support) : minCut W₀ ≤ x.1 := by - obtain ⟨s, rfl⟩ : ∃ s, n = 2 + s := ⟨n - 2, by omega⟩ - rw [run_karger, PMF.mem_support_bind_iff] at hx - obtain ⟨y, hy, hx⟩ := hx - obtain ⟨W', part', hy', hC'⟩ := - isContractionOf_of_mem_support_contractTimes (t := 2) (by norm_num) s - (isContractionOf_id hW₀) hy - obtain rfl := (PMF.mem_support_pure_iff _ _).mp hx - obtain ⟨-, hcw, hle⟩ := two_vertex_contraction_output hC' - change minCut W₀ ≤ totalDoubledWeight y.2.weight / 2 - rw [hy'] - change minCut W₀ ≤ totalDoubledWeight W' / 2 - rw [totalDoubledWeight_fin_two hC'.multigraph] - omega + obtain ⟨C, hC, hx⟩ := exists_cut_of_mem_support_answerLaw hn hW₀ + ((PMF.mem_support_map_iff _ _ _).mpr ⟨x, hx, rfl⟩) + exact hx ▸ minCut_le_cutWeight W₀ hC + +/-! ## Amplification -/ + +/-- One more run of a trial, keeping the least answer `b` so far. The trial is an oracle whose one +call `()` answers one run of `karger`. -/ +def minStep (b : ℕ) : OracleComp (fun _ : Unit => ℕ) ℕ := do + let v ← OracleComp.query () + pure (min v b) + +/-- **Amplification** [Karger1993]: make `R` runs of a trial and answer the least answer, or `0` +when `R = 0`. Answering each call by an independent run of `karger` on `G`, with +`OracleComp.evalWith (fun _ => answerLaw G)`, gives the law of `R` independent runs. -/ +def minRuns : ℕ → OracleComp (fun _ : Unit => ℕ) ℕ + | 0 => pure 0 + | R + 1 => do + let v ← OracleComp.query () + OracleComp.iterate R minStep v + +/-- After the least answer `b` of earlier runs, `R` more runs answer at most `b`: either `b` or the +answer of one of them. -/ +theorem mem_support_iterate_minStep {μ : PMF ℕ} {R b v : ℕ} + (hv : v ∈ (OracleComp.evalWith (fun _ => μ) (OracleComp.iterate R minStep b)).support) : + v ≤ b ∧ (v = b ∨ v ∈ μ.support) := by + rw [OracleComp.support_evalWith] at hv + refine OracleComp.iterate_invariant (fun _ v => v ≤ b ∧ (v = b ∨ v ∈ μ.support)) + ⟨le_rfl, .inl rfl⟩ (fun _ c _ ⟨hcb, hc⟩ next hnext => ?_) v hv + obtain ⟨u, hu, hnext⟩ := OracleComp.mem_supportWith_bind_iff.mp hnext + obtain rfl := OracleComp.eq_of_mem_supportWith_pure hnext + rw [OracleComp.supportWith_query] at hu + refine ⟨(min_le_right u c).trans hcb, ?_⟩ + rcases min_choice u c with h | h <;> rw [h] + · exact .inr hu + · exact hc + +/-- With `R ≥ 1` runs, every answer of `minRuns R` is the answer of one of the runs. -/ +theorem mem_support_minRuns {μ : PMF ℕ} {R v : ℕ} (hR : R ≠ 0) + (hv : v ∈ (OracleComp.evalWith (fun _ => μ) (minRuns R)).support) : v ∈ μ.support := by + obtain ⟨R, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hR + rw [minRuns, OracleComp.evalWith_bind, OracleComp.evalWith_query, PMF.mem_support_bind_iff] at hv + obtain ⟨u, hu, hv⟩ := hv + obtain ⟨-, rfl | hv⟩ := mem_support_iterate_minStep hv + exacts [hu, hv] + +/-- **Amplification.** If every answer of a run is at least `m` and a run misses `m` with +probability at most `q`, then `R` independent runs all miss it, so `minRuns R` misses it, with +probability at most `q ^ R`. -/ +theorem minRuns_ne_le {μ : PMF ℕ} {m : ℕ} {q : ℝ≥0∞} (hge : ∀ v ∈ μ.support, m ≤ v) + (hmiss : μ.toOuterMeasure {v | v ≠ m} ≤ q) (R : ℕ) : + (OracleComp.evalWith (fun _ => μ) (minRuns R)).toOuterMeasure {v | v ≠ m} ≤ q ^ R := by + have hstep (b : ℕ) : + OracleComp.evalWith (fun _ => μ) (minStep b) = μ.map fun v => min v b := by + simp only [minStep, OracleComp.evalWith_bind, OracleComp.evalWith_query, + OracleComp.evalWith_pure] + exact PMF.bind_pure_comp _ _ + -- Once a run hits `m`, the least answer stays there. + have hstay (R : ℕ) : + (OracleComp.evalWith (fun _ => μ) (OracleComp.iterate R minStep m)).toOuterMeasure + {v | v ≠ m} = 0 := by + refine (PMF.toOuterMeasure_apply_eq_zero_iff _ _).mpr + (Set.disjoint_left.mpr fun v hv hne => hne ?_) + obtain ⟨hle, rfl | hv⟩ := mem_support_iterate_minStep hv + · rfl + · exact le_antisymm hle (hge v hv) + -- After a least answer of at least `m`, each further run misses independently. + have hfrom (R : ℕ) : ∀ b, m ≤ b → + (OracleComp.evalWith (fun _ => μ) (OracleComp.iterate R minStep b)).toOuterMeasure + {v | v ≠ m} ≤ q ^ R := by + induction R with + | zero => exact fun _ _ => (Probability.PMF.toOuterMeasure_le_one _ _).trans (by rw [pow_zero]) + | succ R ih => + intro b hb + rw [OracleComp.iterate_succ_bind, OracleComp.evalWith_bind, pow_succ'] + refine Probability.PMF.toOuterMeasure_bind_le_mul_ennreal _ _ {c | c ≠ m} _ ?_ + (fun c hc _ => ih c ?_) fun c _ hc => by rw [not_not.mp hc]; exact hstay R + · rw [hstep, PMF.toOuterMeasure_map_apply] + refine (PMF.toOuterMeasure_mono _ ?_).trans hmiss + rintro v ⟨hv, -⟩ rfl + exact hv (min_eq_left hb) + · rw [hstep, PMF.mem_support_map_iff] at hc + obtain ⟨v, hv, rfl⟩ := hc + exact le_min (hge v hv) hb + cases R with + | zero => exact (Probability.PMF.toOuterMeasure_le_one _ _).trans (by rw [pow_zero]) + | succ R => + rw [minRuns, OracleComp.evalWith_bind, OracleComp.evalWith_query, pow_succ'] + exact Probability.PMF.toOuterMeasure_bind_le_mul_ennreal _ _ {v | v ≠ m} _ hmiss + (fun v hv _ => hfrom R v (hge v hv)) fun v _ hv => by rw [not_not.mp hv]; exact hstay R + +/-- **Amplification of Karger's algorithm** [Karger1993]. On a connected multigraph with `n ≥ 2` +vertices, `R` independent runs of `karger` all miss the minimum cut weight, so `minRuns R` misses +it, with probability at most `(1 - 2 / (n (n - 1))) ^ R`. -/ +theorem minRuns_ne_minCut_le {n : ℕ} (hn : 2 ≤ n) {W₀ : Fin n → Fin n → ℕ} + (hW₀ : IsMultigraph W₀) (hmin : 0 < minCut W₀) (R : ℕ) : + (OracleComp.evalWith (fun _ => answerLaw ⟨n, W₀⟩) (minRuns R)).toOuterMeasure + {v | v ≠ minCut W₀} ≤ (1 - 2 / ((n * (n - 1) : ℕ) : ℝ≥0∞)) ^ R := by + refine minRuns_ne_le (fun v hv => ?_) (Probability.PMF.toOuterMeasure_compl_le_one_sub _ + {v | v = minCut W₀} ?_) R + · obtain ⟨C, hC, rfl⟩ := exists_cut_of_mem_support_answerLaw hn hW₀ hv + exact minCut_le_cutWeight W₀ hC + · rw [answerLaw, PMF.toOuterMeasure_map_apply] + exact two_div_le_toOuterMeasure_karger hn hW₀ hmin /-! ## Calls -/ diff --git a/Complexity/Algorithms/WordRAM/Karger/Contract.lean b/Complexity/Algorithms/WordRAM/Karger/Contract.lean index 7f52b17c88..7fb8044ed5 100644 --- a/Complexity/Algorithms/WordRAM/Karger/Contract.lean +++ b/Complexity/Algorithms/WordRAM/Karger/Contract.lean @@ -95,6 +95,10 @@ law. * `Cslib.Algorithms.WordRAM.Karger.contractDownTo_law`: `contractDownTo` simulates `k - t` contractions of the specification: `ExecRandLaw` with `IsQueryBounded (k - t)`, worst-case step bound `36 * (k ^ 2 - t ^ 2) + 4`, `Modifies` frame, and the law of `heldGraph`. +* `Cslib.Algorithms.WordRAM.Karger.contractDownToAt_law`: the same on any `r ≥ 16` registers, + preserving the caller's registers. +* `Cslib.Algorithms.WordRAM.Karger.ContractState.mem_add_one`: on two supervertices, the weight + between them is half the total weight of the held graph. * `Cslib.Algorithms.WordRAM.Karger.contractDownTo_spec`: joint certificate of `ExecRand`, `IsQueryBounded (k - t)`, worst-case step bound `36 * (k ^ 2 - t ^ 2) + 4`, `Modifies` frame, contraction invariant `IsContractionOf`, and cut-survival probability lower bound @@ -198,6 +202,16 @@ theorem ContractState.heldGraph_eq {w wb db str k t : ℕ} {W : Fin k → Fin k rw [hst.regs_activeK] exact congrArg _ (funext₂ hst.workspace.1) +/-- On two supervertices, the weight between them, at `wb + 1`, is half the total weight of the +held graph. -/ +theorem ContractState.mem_add_one {w wb db str t : ℕ} {W : Fin 2 → Fin 2 → ℕ} {x : Data 16} + (hst : ContractState w wb db str 2 t W x) (hW : IsMultigraph W) : + x.mem (wb + 1) = totalDoubledWeight (heldGraph wb str x).weight / 2 := by + rw [hst.heldGraph_eq] + change _ = totalDoubledWeight W / 2 + rw [totalDoubledWeight_fin_two hW, show x.mem (wb + 1) = W 0 1 by simpa using hst.workspace.1 0 1] + omega + /-- The weight matrix of a state is the weight of the graph it holds. -/ private theorem ContractState.eq_of_heldGraph_eq {w wb db str k t : ℕ} {W W' : Fin k → Fin k → ℕ} {x : Data 16} (hst : ContractState w wb db str k t W x) (h : heldGraph wb str x = ⟨k, W'⟩) : @@ -2855,6 +2869,24 @@ theorem computeDegreesAndTotalAt_exec {r w wb db str k : ℕ} (hr : 16 ≤ r) · rw [extend_castLE_regs_lt, hy₀_t]; rfl · rw [extend_castLE_regs_lt, hy₀_tot] +/-- `contractDownToAt hr` simulates `k - t` contractions of `Lean.Karger.spec` on any `r`-register +file (`16 ≤ r`), as `contractDownTo_law` does, and preserves all caller registers with index +`≥ 16`. -/ +theorem contractDownToAt_law {r w wb db str k t : ℕ} (hr : 16 ≤ r) {W : Fin k → Fin k → ℕ} + {x : Data r} (ht : 2 ≤ t) (htk : t ≤ k) (hW : IsMultigraph W) + (hst : ContractState w wb db str k t W (x.comap (Fin.castLE hr))) : + ExecRandLaw w (contractDownToAt hr) x + (fun y => Modifies (workspaceFootprint wb db str k) x.mem y.mem ∧ + (∀ j : Fin r, 16 ≤ j.val → y.regs j = x.regs j) ∧ + ∃ W' : Fin t → Fin t → ℕ, IsMultigraph W' ∧ + ContractState w wb db str t t W' (y.comap (Fin.castLE hr))) + (36 * (k ^ 2 - t ^ 2) + 4) (k - t) (fun y => heldGraph wb str (y.comap (Fin.castLE hr))) + ((Lean.Karger.spec.toRandomized.withCoins.run (Lean.Karger.contractTimes (k - t)) + ⟨k, W⟩).map Prod.snd) := + (ExecRandLaw.rename (Fin.castLE_injective hr) (contractDownTo_law ht htk hW hst)).mono + (fun _ ⟨y, ⟨hmod, hy⟩, he⟩ => he ▸ ⟨hmod, fun j hj => extend_castLE_regs_ge hr y x j hj, + by rwa [Data.comap_extend (Fin.castLE_injective hr)]⟩) le_rfl le_rfl + /-- Specification of `contractDownToAt hr` on any `r`-register file (`16 ≤ r`), preserving all caller registers with index `≥ 16`. -/ theorem contractDownToAt_spec {r n w wb db str k t : ℕ} (hr : 16 ≤ r) diff --git a/Complexity/Algorithms/WordRAM/KargerMinCut.lean b/Complexity/Algorithms/WordRAM/KargerMinCut.lean index 4152ddf546..cf1de33e8b 100644 --- a/Complexity/Algorithms/WordRAM/KargerMinCut.lean +++ b/Complexity/Algorithms/WordRAM/KargerMinCut.lean @@ -39,6 +39,19 @@ three complete machine-level endpoints built on the workspace-relocatable subrou misses `minCut W` with probability at most `1 / (2 * n)` (hence at most `1 / n`) whenever `0 < minCut W`, via an elementary Bernoulli power bound without `Real.exp`. +No probability is proved on machine states. Each program simulates a client of +`Cslib.Algorithms.Lean.Karger`: the word it outputs has the law of the answer of +`Cslib.Algorithms.Lean.Karger.karger` (`singleCode_law`), or of the amplification client +`Cslib.Algorithms.Lean.Karger.minRuns` run against independent runs of `karger` +(`amplifiedCode_law`, `highProbCode_law`). Each trial contracts as the client does +(`contractDownTo_law`) and reads half the total weight of the two supervertices left +(`ContractState.mem_add_one`), and the loop of trials keeps the least answer as `minRuns` does +(`ampTrialBody_law`, `ampLoop_law`). The success and failure bounds and the cut realization are the +specification's (`Cslib.Algorithms.Lean.Karger.two_div_le_toOuterMeasure_karger`, +`Cslib.Algorithms.Lean.Karger.minRuns_ne_minCut_le`, +`Cslib.Algorithms.Lean.Karger.exists_cut_of_mem_support_answerLaw`, +`Cslib.Algorithms.Lean.Karger.mem_support_minRuns`), carried through those laws. + ## Source statements and notation mapping * **Source locators (paraphrase):** @@ -88,6 +101,13 @@ three complete machine-level endpoints built on the workspace-relocatable subrou ## Main results +* `Cslib.Algorithms.WordRAM.Karger.singleCode_law`, + `Cslib.Algorithms.WordRAM.Karger.amplifiedCode_law`, + `Cslib.Algorithms.WordRAM.Karger.highProbCode_law`: each program's output has the law of the + output of `karger` or of amplified `karger`, within its instruction and `rand`-call bounds. +* `Cslib.Algorithms.WordRAM.Karger.ampTrialBody_law`, `Cslib.Algorithms.WordRAM.Karger.ampLoop_law`, + `Cslib.Algorithms.WordRAM.Karger.ampCore_law`: one trial, the loop of trials and the + amplification core. * `Cslib.Algorithms.WordRAM.Karger.singleProgram_spec`: worst-case `O(n ^ 2)` step bound, `n - 2` `rand`-call bound, pathwise non-trivial cut realization, `Modifies` frame, and `2 / (n * (n - 1))` success probability lower bound for `singleProgram`. @@ -202,6 +222,53 @@ theorem holdsMatrix_init_amplified {r R n : ℕ} (W : Fin n → Fin n → ℕ) : HoldsMatrix (Data.init (r := r) (R :: n :: flattenMatrix W)).mem 3 n W := holdsMatrix_init_append [R, n] W +/-! ### Compiled programs from the law of their output -/ + +/-- A compiled program whose output word has the law `μ`, supported on the weights of non-trivial +cuts of `W`, halts on every path with such a weight, and outputs `minCut W` with the probability +that `μ` gives it. -/ +private theorem program_of_law {r R T T' n w : ℕ} {c : Code .standard r} {out : Fin r} + {input : List ℕ} {F : Finset ℕ} {W : Fin n → Fin n → ℕ} {μ : PMF ℕ} + (h : ExecRandLaw w c (.init input) (fun y => Modifies F (Data.init (r := r) input).mem y.mem) + T R (fun y => y.regs out) μ) (hT : T + 1 ≤ T') (hfit : InputFits w input) + (hμ : ∀ v ∈ μ.support, ∃ C : Finset (Fin n), IsNonTrivialCut C ∧ v = cutWeight W C) : + RandHaltsWithin w (c.program out) (.init input) T' ∧ + RandCallsBounded w (c.program out) (.init input) T' R ∧ + (∀ cfg ∈ (runRand w (c.program out) T' (.running (.init input))).support, + ∃ (y : Data r) (C : Finset (Fin n)), + cfg = .halted (cutWeight W C) y ∧ y.Bounded w ∧ IsNonTrivialCut C ∧ + minCut W ≤ cutWeight W C ∧ Modifies F (Data.init (r := r) input).mem y.mem) ∧ + μ.toOuterMeasure {v | v = minCut W} ≤ + (evalRand w (c.program out) T' (.init input)).toOuterMeasure + {cfg | ∃ y, cfg = .halted (minCut W) y} ∧ + (evalRand w (c.program out) T' (.init input)).toOuterMeasure + {cfg | ∀ y, cfg ≠ .halted (minCut W) y} ≤ μ.toOuterMeasure {v | v ≠ minCut W} := by + let output : RandCfg r → ℕ := fun | .halted v _ => v | _ => 0 + obtain ⟨hhalt, hcalls, hpost, hlaw⟩ := h.program out hT output fun _ _ => rfl + have hhalted : ∀ cfg ∈ (evalRand w (c.program out) T' (.init input)).support, + ∃ y : Data r, cfg = .halted (y.regs out) y := fun cfg hcfg => by + obtain ⟨y, rfl, -⟩ := hpost cfg (by rwa [support_evalRand] at hcfg) + exact ⟨y, rfl⟩ + refine ⟨hhalt, hcalls, fun cfg hcfg => ?_, ?_, ?_⟩ + · obtain ⟨y, rfl, hmod⟩ := hpost cfg hcfg + obtain ⟨C, hC, hv⟩ := hμ (y.regs out) (by + rw [← hlaw, PMF.mem_support_map_iff] + exact ⟨_, by rwa [support_evalRand], rfl⟩) + exact ⟨y, C, by rw [hv], (runRand_bounded_init hfit hcfg).2, hC, minCut_le_cutWeight W hC, + hmod⟩ + · rw [← hlaw, PMF.toOuterMeasure_map_apply] + refine PMF.toOuterMeasure_mono _ ?_ + rintro cfg ⟨hv, hcfg⟩ + obtain ⟨y, rfl⟩ := hhalted cfg hcfg + change y.regs out = minCut W at hv + exact ⟨y, by rw [hv]⟩ + · rw [← hlaw, PMF.toOuterMeasure_map_apply] + refine PMF.toOuterMeasure_mono _ ?_ + rintro cfg ⟨hne, hcfg⟩ hv + obtain ⟨y, rfl⟩ := hhalted cfg hcfg + change y.regs out = minCut W at hv + exact hne y (by rw [hv]) + /-! ### Endpoint 1: Single-trial Basic Karger (`r = 16`) -/ section SingleTrial @@ -314,21 +381,20 @@ theorem singlePost_exec {w wb : ℕ} {x : Data 16} (hwBase : x.regs wBase = wb) Exec.load (B := .standard) (w := w) (d := val1) (a := addr1) (x := s₂) exact ⟨s₃, e1.seq (e2.seq e3), rfl, by simp [s₃]⟩ -/-- Structured `ProbComp` specification of `singleCode`. -/ -theorem singleCode_spec {n w : ℕ} {W : Fin n → Fin n → ℕ} +/-- **A single trial runs `karger`.** At word size `w ≥ logWidth 3 n` with +`totalDoubledWeight W < 2 ^ w`, `singleCode` on `n :: flattenMatrix W` runs within +`singleTime n - 1` instructions and `n - 2` `rand` calls and writes only `[2, 2 + n * n + n)`. The +weight it leaves in `val1` has the law of the answer of `Lean.Karger.karger` on `⟨n, W⟩`: +`contractDownTo` contracts as the client does (`contractDownTo_law`), and `singlePost` reads the +weight between the last two supervertices, half their total weight. -/ +theorem singleCode_law {n w : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hW : IsMultigraph W) (hw : logWidth 3 n ≤ w) (htot : Fits w (totalDoubledWeight W)) : - ∃ m : ProbComp (Data 16 × ℕ), - ExecRand w singleCode (Data.init (n :: flattenMatrix W)) m ∧ - m.IsQueryBounded (n - 2) ∧ - (∀ z ∈ m.support, - z.2 + 1 ≤ singleTime n ∧ - Modifies (Finset.Ico 2 (2 + n * n + n)) - (Data.init (r := 16) (n :: flattenMatrix W)).mem z.1.mem ∧ - ∃ C : Finset (Fin n), IsNonTrivialCut C ∧ z.1.regs val1 = cutWeight W C) ∧ - (0 < minCut W → - (2 : ℝ≥0∞) / ((n * (n - 1) : ℕ) : ℝ≥0∞) ≤ - m.eval.toOuterMeasure {z | z.1.regs val1 = minCut W}) := by + ExecRandLaw w singleCode (Data.init (n :: flattenMatrix W)) + (fun y => Modifies (Finset.Ico 2 (2 + n * n + n)) + (Data.init (r := 16) (n :: flattenMatrix W)).mem y.mem) + (42 * n ^ 2 + 12 * n + 20) (n - 2) (fun y => y.regs val1) + (Lean.Karger.answerLaw ⟨n, W⟩) := by have hws_fit := fits_workspace_of_logWidth_three hn hw have h1 : Fits w 1 := hws_fit.of_le (by omega) have hwEnd : Fits w (2 + n * n) := hws_fit.of_le (by omega) @@ -336,8 +402,7 @@ theorem singleCode_spec {n w : ℕ} {W : Fin n → Fin n → ℕ} have hwb1 : Fits w (2 + 1) := hws_fit.of_le (by omega) obtain ⟨y_setup, e_setup, hmem_setup, hwb_s, hdb_s, hstr_s, hk_s, ht_s⟩ := singleSetup_exec (W := W) hn hw - obtain ⟨y_deg, ⟨n_deg, hn_deg, e_deg⟩, hws_deg, hmod_deg, _, _, - hwb_d, hdb_d, hstr_d, hk_d, ht_d, htot_d⟩ := + obtain ⟨y_deg, e_deg, hws_deg, hmod_deg, _, _, hwb_d, hdb_d, hstr_d, hk_d, ht_d, htot_d⟩ := computeDegreesAndTotal_exec (w := w) (W := W) (x := y_setup) hwb_s hdb_s hstr_s hk_s (le_refl n) (Or.inl (le_refl _)) h1 hwEnd hdEnd htot (hmem_setup ▸ holdsMatrix_init_single W) @@ -345,106 +410,27 @@ theorem singleCode_spec {n w : ℕ} {W : Fin n → Fin n → ℕ} have hst_deg : ContractState w 2 (2 + n * n) n n 2 W y_deg := ⟨hwb_d, hdb_d, hstr_d, hk_d, ht_d, htot_d, le_refl n, Or.inl (le_refl _), hwEnd, hdEnd, htot, hws_deg⟩ - obtain ⟨m_c, hm_c, hq_c, hsup_c, hsurv_c⟩ := - contractDownTo_spec (le_refl 2) hn (isContractionOf_id hW) hst_deg - have hpost_all : ∀ z ∈ m_c.support, - ∃ y_p : Data 16, Exec w singlePost z.1 y_p 3 ∧ - y_p.mem = z.1.mem ∧ y_p.regs val1 = z.1.mem 3 := by - intro z hz - rcases hsup_c z hz with ⟨_, _, W', part', _, hst'⟩ - exact singlePost_exec hst'.regs_wBase h1 hwb1 - obtain ⟨m_post, hm_post_def⟩ : - ∃ m_post : Data 16 → ProbComp (Data 16 × ℕ), - ∀ d, m_post d = codeComp w singlePost d := ⟨_, fun _ => rfl⟩ - have hm_post : ∀ z ∈ m_c.support, ExecRand w singlePost z.1 (m_post z.1) := by - intro z hz - obtain ⟨y_p, e_p, _, _⟩ := hpost_all z hz - have hr := e_p.execRand - rw [hm_post_def] - simpa only [hr.codeComp_eq] using hr - have hm_c_post : ExecRand w (ram[⟪contractDownTo⟫; ⟪singlePost⟫]) y_deg - (do let z₁ ← m_c; let z₂ ← m_post z₁.1; pure (z₂.1, z₁.2 + z₂.2)) := - ExecRand.seq hm_c hm_post - have hm_deg_rest := e_deg.seqRand hm_c_post - have hm_full := e_setup.seqRand hm_deg_rest - let m_total := (fun z => (z.1, 7 + z.2)) <$> - ((fun z => (z.1, n_deg + z.2)) <$> - (do let z₁ ← m_c; let z₂ ← m_post z₁.1; pure (z₂.1, z₁.2 + z₂.2))) + have hsub : workspaceFootprint 2 (2 + n * n) n n ⊆ Finset.Ico 2 (2 + n * n + n) := by + intro a ha + simp only [workspaceFootprint, Finset.mem_union, Finset.mem_Ico] at ha ⊢ + omega + have hrun := ExecRandLaw.seq (contractDownTo_law (le_refl 2) hn hW hst_deg) + (κ := fun G => PMF.pure (totalDoubledWeight G.weight / 2)) fun y ⟨hmod_c, W', hW', hst'⟩ => by + obtain ⟨y_p, e_p, hmem_p, hv_p⟩ := singlePost_exec hst'.regs_wBase h1 hwb1 + have hmod : Modifies (Finset.Ico 2 (2 + n * n + n)) + (Data.init (r := 16) (n :: flattenMatrix W)).mem y_p.mem := by + rw [hmem_p] + exact modifies_trans_subset (hmem_setup ▸ hmod_deg) hmod_c + (Finset.Ico_subset_Ico (by omega) le_rfl) hsub + exact (ExecRandLaw.of_execWithin (f := fun y => y.regs val1) e_p.within hmod).congr_law + (by rw [hv_p, hst'.mem_add_one hW']) have hcode_eq : singleCode = .seq singleSetup (.seq computeDegreesAndTotal (.seq contractDownTo singlePost)) := rfl rw [hcode_eq] - refine ⟨m_total, hm_full, ?_, ?_, ?_⟩ - · simp only [m_total, OracleComp.IsQueryBounded, OracleComp.isCostBounded_map_iff] - have hq_post : ∀ z₁ ∈ m_c.support, - (m_post z₁.1 >>= fun z₂ => pure (z₂.1, z₁.2 + z₂.2)).IsQueryBounded 0 := by - intro z₁ hz₁ - obtain ⟨y_p, e_p, _, _⟩ := hpost_all z₁ hz₁ - rw [hm_post_def, e_p.execRand.codeComp_eq, pure_bind] - exact .pure _ 0 - simpa only [Nat.add_zero] using OracleComp.IsCostBounded.bind_on_support hq_c hq_post - · intro z hz - simp only [m_total, Functor.map_map] at hz - obtain ⟨z₀, hz₀, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hz - obtain ⟨z₁, hz₁, hrest⟩ := OracleComp.mem_supportWith_bind_iff.mp hz₀ - obtain ⟨y_p, e_p, hmem_p, hv1_p⟩ := hpost_all z₁ hz₁ - rw [hm_post_def, e_p.execRand.codeComp_eq] at hrest - obtain ⟨z₂, hz₂, hpure⟩ := OracleComp.mem_supportWith_bind_iff.mp hrest - cases OracleComp.eq_of_mem_supportWith_pure hz₂ - cases OracleComp.eq_of_mem_supportWith_pure hpure - rcases hsup_c z₁ hz₁ with ⟨ht_c, hmod_c, W', part', hC', hst'⟩ - refine ⟨?_, ?_, ?_⟩ - · simp only [singleTime] - omega - · rw [hmem_p] - have hsub1 : Finset.Ico (2 + n * n) (2 + n * n + n) ⊆ Finset.Ico 2 (2 + n * n + n) := - Finset.Ico_subset_Ico (by omega) (le_refl _) - have hsub2 : workspaceFootprint 2 (2 + n * n) n n ⊆ Finset.Ico 2 (2 + n * n + n) := by - intro a ha - simp only [workspaceFootprint, Finset.mem_union, Finset.mem_Ico] at ha ⊢ - omega - exact modifies_trans_subset (hmem_setup ▸ hmod_deg) hmod_c hsub1 hsub2 - · refine ⟨pullbackCut part' {0}, - isNonTrivialCut_pullbackCut hC'.surj (isNonTrivialCut_singleton (by simp) 0), ?_⟩ - rw [hv1_p, cutWeight_pullbackCut hC', cutWeight_two_singleton_zero hC'.multigraph] - simpa using hst'.workspace.1 0 1 - · intro hmin_pos - obtain ⟨C_star, hC_nt, hC_min⟩ := exists_minCut_achiever (by rwa [Fintype.card_fin]) W - have hpb_id : pullbackCut (id : Fin n → Fin n) C_star = C_star := by - ext u - simp [pullbackCut] - have hsurv := hsurv_c C_star hmin_pos hC_nt (by rw [hpb_id, hC_min]) - rw [hpb_id] at hsurv - have h2 : (((2 * (2 - 1) : ℕ) : ℝ≥0∞) / ((n * (n - 1) : ℕ) : ℝ≥0∞)) = - (2 : ℝ≥0∞) / ((n * (n - 1) : ℕ) : ℝ≥0∞) := by norm_num - rw [h2] at hsurv - refine hsurv.trans ?_ - have hm_eval : m_total.eval = - m_c.eval.bind fun z₁ => - ((m_post z₁.1).eval.map fun z₂ => (z₂.1, 7 + (n_deg + (z₁.2 + z₂.2)))) := by - have hm_eq : m_total = (do - let z₁ ← m_c - let z₂ ← m_post z₁.1 - pure (z₂.1, 7 + (n_deg + (z₁.2 + z₂.2)))) := by - simp only [m_total, ← bind_pure_comp, bind_assoc, pure_bind] - rw [hm_eq, ProbComp.eval_bind] - refine congrArg (m_c.eval.bind ·) (funext fun z₁ => ?_) - rw [bind_pure_comp, ProbComp.eval_map] - rw [hm_eval] - have hstep := toOuterMeasure_bind_ge_mul_ennreal m_c.eval - (fun z₁ => (m_post z₁.1).eval.map fun z₂ => (z₂.1, 7 + (n_deg + (z₁.2 + z₂.2)))) - {z | SurvivalPost W 2 (2 + n * n) n 2 C_star z.1} - {z | z.1.regs val1 = minCut W} - (s₁ := m_c.eval.toOuterMeasure {z | SurvivalPost W 2 (2 + n * n) n 2 C_star z.1}) - (s₂ := 1) le_rfl ?_ - · simpa using hstep - · intro z₁ hz₁_eval hsurv₁ - have hz₁ : z₁ ∈ m_c.support := (ProbComp.support_eval m_c) ▸ hz₁_eval - obtain ⟨y_p, e_p, _, hv1_p⟩ := hpost_all z₁ hz₁ - rw [hm_post_def, e_p.execRand.codeComp_eq, ProbComp.eval_pure, - PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_pure_apply] - have hmem3 : z₁.1.mem 3 = minCut W := survivalPost_two_mem_eq hC_nt hC_min hsurv₁ - have hhit : y_p.regs val1 = minCut W := hv1_p.trans hmem3 - simp [hhit] + refine ((ExecRandLaw.seq_det e_setup.within (ExecRandLaw.seq_det e_deg hrun)).congr_law ?_).mono + (fun _ h => h) (by omega) (by omega) + rw [Lean.Karger.answerLaw_eq] + exact PMF.bind_pure_comp _ _ /-- **Single-trial Basic Karger specification (`singleProgram`).** At word size `w ≥ logWidth 3 n` when `totalDoubledWeight W < 2 ^ w`: @@ -473,29 +459,12 @@ theorem singleProgram_spec {n w : ℕ} {W : Fin n → Fin n → ℕ} (evalRand w singleProgram (singleTime n) (.init input)).toOuterMeasure {cfg | ∃ y, cfg = .halted (minCut W) y}) := by intro input - have hfit_in : InputFits w input := inputFits_single hn hw htot - obtain ⟨m, hm, hq, hsup, hsurv⟩ := singleCode_spec hn hW hw htot - have hrun : runRand w singleProgram (singleTime n) (.running (.init input)) = - (fun z : Data 16 × ℕ => RandCfg.halted (z.1.regs val1) z.1) <$> m := - hm.runRand_program val1 fun z hz => (hsup z hz).1 - refine ⟨?_, ?_, ?_, ?_⟩ - · intro cfg hcfg - rw [hrun] at hcfg - obtain ⟨z, -, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hcfg - exact ⟨z.1.regs val1, z.1, rfl⟩ - · rw [RandCallsBounded, hrun] - exact (OracleComp.isCostBounded_map_iff _ _ _).mpr hq - · intro cfg hcfg - have hbnd := (runRand_bounded_init hfit_in hcfg) - rw [hrun] at hcfg - obtain ⟨z, hz, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hcfg - rcases hsup z hz with ⟨_, hmod, C, hC_nt, hv1⟩ - exact ⟨z.1, C, by rw [hv1], hbnd.2, hC_nt, minCut_le_cutWeight W hC_nt, hmod⟩ - · intro hmin_pos - rw [evalRand, hrun, ProbComp.eval_map, PMF.toOuterMeasure_map_apply] - refine (hsurv hmin_pos).trans (PMF.toOuterMeasure_mono _ ?_) - intro z hz - exact ⟨z.1, congrArg (fun v => RandCfg.halted v z.1) hz.1⟩ + obtain ⟨hhalt, hcalls, hpost, hhit, -⟩ := program_of_law (T' := singleTime n) + (singleCode_law hn hW hw htot) (by unfold singleTime; omega) (inputFits_single hn hw htot) + fun _ hv => Lean.Karger.exists_cut_of_mem_support_answerLaw hn hW hv + refine ⟨hhalt, hcalls, hpost, fun hmin => le_trans ?_ hhit⟩ + rw [Lean.Karger.answerLaw, PMF.toOuterMeasure_map_apply] + exact Lean.Karger.two_div_le_toOuterMeasure_karger hn hW hmin end SingleTrial @@ -692,7 +661,6 @@ structure AmpInv (w sb n R i : ℕ) (W : Fin n → Fin n → ℕ) (mem₀ : ℕ regs_trialIdx : x.regs trialIdx = i src_matrix : HoldsMatrix x.mem sb n W modifies_ws : Modifies (Finset.Ico (sb + n * n) (sb + 2 * (n * n) + n)) mem₀ x.mem - best_cut : 0 < i → ∃ C : Finset (Fin n), IsNonTrivialCut C ∧ x.regs bestVal = cutWeight W C theorem ampTrialPost_exec {w wb i R : ℕ} {x : Data 22} (hwb : x.regs wBase = wb) (hti : x.regs trialIdx = i) (hiR : i < R) @@ -821,37 +789,27 @@ theorem ampTrialPost_exec {w wb i R : ℕ} {x : Data 22} exact ((e1.within).seq ((e2.within).seq ((e3.within).seq ((e4.within).seq (e_br.seq e_inc))))).mono (by omega) -private theorem ampTrial_step_bound {n n_cp n_deg t_c n_p : ℕ} - (hcp : n_cp ≤ 7 * (n * n) + 4) - (hdeg : n_deg ≤ 6 * n ^ 2 + 12 * n + 6) - (hc : t_c ≤ 36 * (n ^ 2 - 2 ^ 2) + 4) - (hp : n_p ≤ 10) : - (n_cp + (3 + n_deg)) + (t_c + n_p) ≤ 49 * n ^ 2 + 12 * n + 27 := by - have hnn : n * n = n ^ 2 := (sq n).symm - omega - -/-- Specification of a single trial `ampTrialBody` from `AmpInv`. -/ -theorem ampTrialBody_spec {w sb n R i : ℕ} {W : Fin n → Fin n → ℕ} {mem₀ : ℕ → ℕ} {x : Data 22} +/-- **One trial runs `karger`.** From `AmpInv` at trial `i < R`, `ampTrialBody` runs within +`49 n² + 12 n + 27` instructions and `n - 2` `rand` calls and keeps the invariant at trial `i + 1`. +Its new `bestVal` has the law of the answer `v` of `Lean.Karger.karger` on `⟨n, W⟩`, taken as is on +the first trial and as `min v bestVal` after: `contractDownToAt` contracts the fresh copy of `W` as +the client does (`contractDownToAt_law`), and `ampTrialPost` reads the weight between the last two +supervertices, half their total weight. -/ +theorem ampTrialBody_law {w sb n R i : ℕ} {W : Fin n → Fin n → ℕ} {mem₀ : ℕ → ℕ} {x : Data 22} (hn : 2 ≤ n) (hW : IsMultigraph W) (hiR : i < R) (h1 : Fits w 1) (hdEnd : Fits w (sb + 2 * (n * n) + n)) (hR_fit : Fits w R) (htot : Fits w (totalDoubledWeight W)) (hinv : AmpInv w sb n R i W mem₀ x) : - ∃ m : ProbComp (Data 22 × ℕ), - ExecRand w ampTrialBody x m ∧ - m.IsQueryBounded (n - 2) ∧ - (∀ z ∈ m.support, - z.2 ≤ 49 * n ^ 2 + 12 * n + 27 ∧ - AmpInv w sb n R (i + 1) W mem₀ z.1 ∧ - (0 < i → x.regs bestVal = minCut W → z.1.regs bestVal = minCut W)) ∧ - (0 < minCut W → - m.eval.toOuterMeasure {z | z.1.regs bestVal ≠ minCut W} ≤ - (1 : ℝ≥0∞) - (2 : ℝ≥0∞) / ((n * (n - 1) : ℕ) : ℝ≥0∞)) := by + ExecRandLaw w ampTrialBody x (AmpInv w sb n R (i + 1) W mem₀) (49 * n ^ 2 + 12 * n + 27) + (n - 2) (fun y => y.regs bestVal) + ((Lean.Karger.answerLaw ⟨n, W⟩).map fun v => + if i = 0 then v else min v (x.regs bestVal)) := by let wb := sb + n * n let db := sb + 2 * (n * n) have hwEnd : Fits w (wb + n * n) := hdEnd.of_le (by omega) have h2_fit : Fits w 2 := hdEnd.of_le (by omega) have hwb1_fit : Fits w (wb + 1) := hdEnd.of_le (by omega) - obtain ⟨y_cp, ⟨n_cp, hn_cp, e_cp⟩, hmat_cp, hmod_cp, + obtain ⟨y_cp, e_cp, hmat_cp, hmod_cp, hwb_cp, hdb_cp, hsb_cp, hn_cp_reg, hml_cp, hnt_cp, hti_cp, hbv_cp⟩ := copyMatrixCode_exec hinv.regs_srcBase hinv.regs_wBase hinv.regs_matLen (le_refl _) h1 hwEnd hinv.src_matrix @@ -872,7 +830,7 @@ theorem ampTrialBody_spec {w sb n R i : ℕ} {W : Fin n → Fin n → ℕ} {mem have ec3 : Exec (B := .standard) w ram[targetT ← #2] ((y_cp.set activeK n).set stride n) y_cfg 1 := Exec.const h2_fit - obtain ⟨y_deg, ⟨n_deg, hn_deg, e_deg⟩, hws_deg, hmod_deg, + obtain ⟨y_deg, e_deg, hws_deg, hmod_deg, hwb_d, hdb_d, hstr_d, hk_d, ht_d, htot_d, hhi_d⟩ := computeDegreesAndTotalAt_exec (w := w) (W := W) (x := y_cfg) hr22 (by change y_cfg.regs wBase = wb; simpa +decide [y_cfg, Function.update_apply] using hwb_cp) @@ -887,8 +845,6 @@ theorem ampTrialBody_spec {w sb n R i : ℕ} {W : Fin n → Fin n → ℕ} {mem have hst_deg : ContractState w wb db n n 2 W (y_deg.comap (Fin.castLE hr22)) := ⟨hwb_d, hdb_d, hstr_d, hk_d, ht_d', htot_d, le_refl n, Or.inl (by omega), hwEnd, hdEnd, htot, hws_deg⟩ - obtain ⟨m_c, hm_c, hq_c, hsup_c, hsurv_c⟩ := - contractDownToAt_spec hr22 (le_refl 2) hn (isContractionOf_id hW) hst_deg have hy_deg_hi : y_deg.regs srcBase = sb ∧ y_deg.regs nOrig = n ∧ y_deg.regs matLen = n * n ∧ y_deg.regs numTrials = R ∧ y_deg.regs trialIdx = i ∧ y_deg.regs bestVal = x.regs bestVal := by @@ -899,321 +855,106 @@ theorem ampTrialBody_spec {w sb n R i : ℕ} {W : Fin n → Fin n → ℕ} {mem · rw [hhi_d numTrials (by decide)]; simpa +decide [y_cfg, Function.update_apply] using hnt_cp · rw [hhi_d trialIdx (by decide)]; simpa +decide [y_cfg, Function.update_apply] using hti_cp · rw [hhi_d bestVal (by decide)]; simpa +decide [y_cfg, Function.update_apply] using hbv_cp - have hpost_all : ∀ z ∈ m_c.support, - ∃ (y_p : Data 22) (n_p : ℕ), n_p ≤ 10 ∧ Exec w ampTrialPost z.1 y_p n_p ∧ - y_p.mem = z.1.mem ∧ - y_p.regs srcBase = sb ∧ y_p.regs wBase = wb ∧ y_p.regs dBase = db ∧ - y_p.regs nOrig = n ∧ y_p.regs matLen = n * n ∧ y_p.regs numTrials = R ∧ - y_p.regs trialIdx = i + 1 ∧ - y_p.regs bestVal = - (if i = 0 then z.1.mem (wb + 1) else min (z.1.mem (wb + 1)) (x.regs bestVal)) := by - intro z hz - rcases hsup_c z hz with ⟨_, _, hz_hi, W', part', _, hst'⟩ - have hz_wb : z.1.regs wBase = wb := hst'.regs_wBase - have hz_db : z.1.regs dBase = db := hst'.regs_dBase - have hz_sb : z.1.regs srcBase = sb := (hz_hi srcBase (by decide)).trans hy_deg_hi.1 - have hz_n : z.1.regs nOrig = n := (hz_hi nOrig (by decide)).trans hy_deg_hi.2.1 - have hz_ml : z.1.regs matLen = n * n := (hz_hi matLen (by decide)).trans hy_deg_hi.2.2.1 - have hz_nt : z.1.regs numTrials = R := (hz_hi numTrials (by decide)).trans hy_deg_hi.2.2.2.1 - have hz_ti : z.1.regs trialIdx = i := (hz_hi trialIdx (by decide)).trans hy_deg_hi.2.2.2.2.1 - have hz_bv : z.1.regs bestVal = x.regs bestVal := - (hz_hi bestVal (by decide)).trans hy_deg_hi.2.2.2.2.2 - obtain ⟨y_p, ⟨n_p, hn_p, e_p⟩, hm_p, hsb_p, hwb_p, hdb_p, hn_p_r, hml_p, hnt_p, hti_p, hbv_p⟩ := - ampTrialPost_exec hz_wb hz_ti hiR h1 hwb1_fit hR_fit - exact ⟨y_p, n_p, hn_p, e_p, hm_p, hsb_p.trans hz_sb, hwb_p, hdb_p.trans hz_db, - hn_p_r.trans hz_n, hml_p.trans hz_ml, hnt_p.trans hz_nt, hti_p, - by simpa only [hz_bv] using hbv_p⟩ - obtain ⟨m_post, hm_post_def⟩ : - ∃ m_post : Data 22 → ProbComp (Data 22 × ℕ), - ∀ d, m_post d = codeComp w ampTrialPost d := ⟨_, fun _ => rfl⟩ - have hm_post : ∀ z ∈ m_c.support, ExecRand w ampTrialPost z.1 (m_post z.1) := by - intro z hz - obtain ⟨y_p, n_p, _, e_p, _⟩ := hpost_all z hz - have hr := e_p.execRand - rw [hm_post_def] - simpa only [hr.codeComp_eq] using hr - have hm_c_post := ExecRand.seq hm_c hm_post - have hm_body : ExecRand w ampTrialBody x - ((fun z => (z.1, (n_cp + (3 + n_deg)) + z.2)) <$> - (do let z₁ ← m_c; let z₂ ← m_post z₁.1; pure (z₂.1, z₁.2 + z₂.2))) := by - have hbody_eq : ampTrialBody = .seq copyMatrixCode - (.seq ram[activeK ← nOrig] (.seq ram[stride ← nOrig] - (.seq ram[targetT ← #2] (.seq (computeDegreesAndTotalAt hr22) - (.seq (contractDownToAt hr22) ampTrialPost))))) := rfl - rw [hbody_eq] - have r4 := e_deg.seqRand hm_c_post - have r3 := ec3.seqRand r4 - have r2 := ec2.seqRand r3 - have r1 := ec1.seqRand r2 - have r0 := e_cp.seqRand r1 - have h111 : ∀ k, 1 + (1 + (1 + k)) = 3 + k := fun _ => by omega - simpa only [Functor.map_map, Nat.add_assoc, h111] using r0 - let m_total := (fun z => (z.1, (n_cp + (3 + n_deg)) + z.2)) <$> - (do let z₁ ← m_c; let z₂ ← m_post z₁.1; pure (z₂.1, z₁.2 + z₂.2)) - refine ⟨m_total, hm_body, ?_, ?_, ?_⟩ - · simp only [m_total, OracleComp.IsQueryBounded, OracleComp.isCostBounded_map_iff] - have hq_post : ∀ z₁ ∈ m_c.support, - (m_post z₁.1 >>= fun z₂ => pure (z₂.1, z₁.2 + z₂.2)).IsQueryBounded 0 := by - intro z₁ hz₁ - obtain ⟨y_p, n_p, _, e_p, _⟩ := hpost_all z₁ hz₁ - rw [hm_post_def, e_p.execRand.codeComp_eq, pure_bind] - exact .pure _ 0 - simpa only [Nat.add_zero] using OracleComp.IsCostBounded.bind_on_support hq_c hq_post - · intro z hz - obtain ⟨z₀, hz₀, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hz - obtain ⟨z₁, hz₁, hrest⟩ := OracleComp.mem_supportWith_bind_iff.mp hz₀ - obtain ⟨y_p, n_p, hn_p, e_p, hm_p, hsb_p, hwb_p, hdb_p, hn_p_r, hml_p, hnt_p, hti_p, hbv_p⟩ := - hpost_all z₁ hz₁ - rw [hm_post_def, e_p.execRand.codeComp_eq] at hrest - obtain ⟨z₂, hz₂, hpure⟩ := OracleComp.mem_supportWith_bind_iff.mp hrest - cases OracleComp.eq_of_mem_supportWith_pure hz₂ - cases OracleComp.eq_of_mem_supportWith_pure hpure - rcases hsup_c z₁ hz₁ with ⟨ht_c, hmod_c, _, W', part', hC', hst'⟩ - have hmod_ws_all : Modifies (Finset.Ico wb (db + n)) x.mem y_p.mem := by - rw [hm_p] - have hs_cp : Finset.Ico wb (wb + n * n) ⊆ Finset.Ico wb (db + n) := - Finset.Ico_subset_Ico (le_refl _) (by omega) - have hs_deg : Finset.Ico db (db + n) ⊆ Finset.Ico wb (db + n) := - Finset.Ico_subset_Ico (by omega) (le_refl _) - have hs_c : workspaceFootprint wb db n n ⊆ Finset.Ico wb (db + n) := by - intro a ha - simp only [workspaceFootprint, Finset.mem_union, Finset.mem_Ico] at ha ⊢ - omega - have hm12 := modifies_trans_subset hmod_cp hmod_deg hs_cp hs_deg - exact modifies_trans_subset hm12 hmod_c Finset.Subset.rfl hs_c - have hsrc_preserved : HoldsMatrix y_p.mem sb n W := by - intro a b - have hlt : sb + a.val * n + b.val < wb := by - have := matAddr_lt_end (wb := sb) (le_refl n) a b - omega - rw [hmod_ws_all _ (by rw [Finset.mem_Ico]; omega)] - exact hinv.src_matrix a b - have hnew_cut : z₁.1.mem (wb + 1) = cutWeight W (pullbackCut part' {0}) := by - rw [cutWeight_pullbackCut hC', cutWeight_two_singleton_zero hC'.multigraph] - simpa using hst'.workspace.1 0 1 - have hnew_nt : IsNonTrivialCut (pullbackCut part' {0}) := - isNonTrivialCut_pullbackCut hC'.surj (isNonTrivialCut_singleton (by simp) 0) - refine ⟨ampTrial_step_bound hn_cp hn_deg ht_c hn_p, ?_, ?_⟩ - · refine ⟨hsb_p, hwb_p, hdb_p, hn_p_r, hml_p, hnt_p, hti_p, hsrc_preserved, - modifies_trans_subset hinv.modifies_ws hmod_ws_all Finset.Subset.rfl Finset.Subset.rfl, - fun _ => ?_⟩ - by_cases hi0 : i = 0 - · exact ⟨pullbackCut part' {0}, hnew_nt, by simp [hbv_p, hi0, hnew_cut]⟩ - · obtain ⟨C_old, hC_old_nt, hbv_old⟩ := hinv.best_cut (Nat.pos_of_ne_zero hi0) - simp only [hbv_p, hi0, ↓reduceIte] - by_cases hle : z₁.1.mem (wb + 1) ≤ x.regs bestVal - · exact ⟨pullbackCut part' {0}, hnew_nt, by rw [Nat.min_eq_left hle, hnew_cut]⟩ - · exact ⟨C_old, hC_old_nt, by rw [Nat.min_eq_right (Nat.le_of_not_le hle), hbv_old]⟩ - · intro hi_pos hbv_min - have hi0 : i ≠ 0 := Nat.ne_of_gt hi_pos - have hge : minCut W ≤ z₁.1.mem (wb + 1) := by - rw [hnew_cut] - exact minCut_le_cutWeight W hnew_nt - simp only [hbv_p, hi0, ↓reduceIte, hbv_min] - exact Nat.min_eq_right hge - · intro hmin_pos - obtain ⟨C_star, hC_nt, hC_min⟩ := exists_minCut_achiever (by rwa [Fintype.card_fin]) W - have hpb_id : pullbackCut (id : Fin n → Fin n) C_star = C_star := by - ext u - simp [pullbackCut] - have hsurv := hsurv_c C_star hmin_pos hC_nt (by rw [hpb_id, hC_min]) - rw [hpb_id] at hsurv - have h2 : (((2 * (2 - 1) : ℕ) : ℝ≥0∞) / ((n * (n - 1) : ℕ) : ℝ≥0∞)) = - (2 : ℝ≥0∞) / ((n * (n - 1) : ℕ) : ℝ≥0∞) := by norm_num - rw [h2] at hsurv - have hhit_ge : (2 : ℝ≥0∞) / ((n * (n - 1) : ℕ) : ℝ≥0∞) ≤ - m_total.eval.toOuterMeasure {z | z.1.regs bestVal = minCut W} := by - refine hsurv.trans ?_ - have hm_eval : m_total.eval = - m_c.eval.bind fun z₁ => - ((m_post z₁.1).eval.map fun z₂ => - (z₂.1, (n_cp + (3 + n_deg)) + (z₁.2 + z₂.2))) := by - have hm_eq : m_total = (do - let z₁ ← m_c - let z₂ ← m_post z₁.1 - pure (z₂.1, (n_cp + (3 + n_deg)) + (z₁.2 + z₂.2))) := by - simp only [m_total, ← bind_pure_comp, bind_assoc, pure_bind] - rw [hm_eq, ProbComp.eval_bind] - refine congrArg (m_c.eval.bind ·) (funext fun z₁ => ?_) - rw [bind_pure_comp, ProbComp.eval_map] - rw [hm_eval] - have hstep := toOuterMeasure_bind_ge_mul_ennreal m_c.eval - (fun z₁ => (m_post z₁.1).eval.map fun z₂ => - (z₂.1, (n_cp + (3 + n_deg)) + (z₁.2 + z₂.2))) - {z | SurvivalPost W wb db n 2 C_star (z.1.comap (Fin.castLE hr22))} - {z | z.1.regs bestVal = minCut W} - (s₁ := m_c.eval.toOuterMeasure - {z | SurvivalPost W wb db n 2 C_star (z.1.comap (Fin.castLE hr22))}) - (s₂ := 1) le_rfl ?_ - · simpa using hstep - · intro z₁ hz₁_eval hsurv₁ - have hz₁ : z₁ ∈ m_c.support := (ProbComp.support_eval m_c) ▸ hz₁_eval - obtain ⟨y_p, n_p, _, e_p, _, _, _, _, _, _, _, _, hbv_p⟩ := hpost_all z₁ hz₁ - rw [hm_post_def, e_p.execRand.codeComp_eq, ProbComp.eval_pure, - PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_pure_apply] - have hmem_wb1 : z₁.1.mem (wb + 1) = minCut W := - survivalPost_two_mem_eq hC_nt hC_min hsurv₁ - have hbv_hit : y_p.regs bestVal = minCut W := by - rw [hbv_p, hmem_wb1] - by_cases hi0 : i = 0 - · simp [hi0] - · obtain ⟨C_old, hC_old_nt, hbv_old⟩ := hinv.best_cut (Nat.pos_of_ne_zero hi0) - simp only [hi0, ↓reduceIte, hbv_old] - exact Nat.min_eq_left (minCut_le_cutWeight W hC_old_nt) - simp [hbv_hit] - have hcompl : {z : Data 22 × ℕ | z.1.regs bestVal ≠ minCut W} = - {z : Data 22 × ℕ | z.1.regs bestVal = minCut W}ᶜ := by - ext z - simp - rw [hcompl] - exact toOuterMeasure_compl_le_one_sub m_total.eval _ hhit_ge - -/-- Specification of `ampLoop` over `rem = R - i` remaining trials. -/ -theorem ampLoop_spec {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {mem₀ : ℕ → ℕ} - (hn : 2 ≤ n) (hW : IsMultigraph W) + have hmod_deg' : Modifies (Finset.Ico wb (db + n)) x.mem y_deg.mem := + modifies_trans_subset hmod_cp hmod_deg (Finset.Ico_subset_Ico (le_refl _) (by omega)) + (Finset.Ico_subset_Ico (by omega) (le_refl _)) + have hs_c : workspaceFootprint wb db n n ⊆ Finset.Ico wb (db + n) := by + intro a ha + simp only [workspaceFootprint, Finset.mem_union, Finset.mem_Ico] at ha ⊢ + omega + -- The contraction runs `karger` on the copy, then `ampTrialPost` updates `bestVal`. + have hrun := ExecRandLaw.seq (contractDownToAt_law hr22 (le_refl 2) hn hW hst_deg) + (κ := fun G => PMF.pure (if i = 0 then totalDoubledWeight G.weight / 2 + else min (totalDoubledWeight G.weight / 2) (x.regs bestVal))) + fun y ⟨hmod_c, hy_hi, W', hW', hst'⟩ => by + have hz_db : y.regs dBase = db := hst'.regs_dBase + have hz_ti : y.regs trialIdx = i := (hy_hi trialIdx (by decide)).trans hy_deg_hi.2.2.2.2.1 + have hv : y.mem (wb + 1) = _ := hst'.mem_add_one hW' + obtain ⟨y_p, e_p, hm_p, hsb_p, hwb_p, hdb_p, hn_p, hml_p, hnt_p, hti_p, hbv_p⟩ := + ampTrialPost_exec hst'.regs_wBase hz_ti hiR h1 hwb1_fit hR_fit + have hmod : Modifies (Finset.Ico wb (db + n)) x.mem y_p.mem := by + rw [hm_p] + exact modifies_trans_subset hmod_deg' hmod_c Finset.Subset.rfl hs_c + refine (ExecRandLaw.of_execWithin (P := AmpInv w sb n R (i + 1) W mem₀) + (f := fun y => y.regs bestVal) e_p ⟨?_, hwb_p, hdb_p.trans hz_db, ?_, ?_, ?_, hti_p, + fun a b => ?_, modifies_trans_subset hinv.modifies_ws hmod Finset.Subset.rfl + Finset.Subset.rfl⟩).congr_law ?_ + · exact hsb_p.trans ((hy_hi srcBase (by decide)).trans hy_deg_hi.1) + · exact hn_p.trans ((hy_hi nOrig (by decide)).trans hy_deg_hi.2.1) + · exact hml_p.trans ((hy_hi matLen (by decide)).trans hy_deg_hi.2.2.1) + · exact hnt_p.trans ((hy_hi numTrials (by decide)).trans hy_deg_hi.2.2.2.1) + · have hlt := matAddr_lt_end (wb := sb) (le_refl n) a b + rw [hmod _ (by rw [Finset.mem_Ico]; omega)] + exact hinv.src_matrix a b + · rw [hbv_p, (hy_hi bestVal (by decide)).trans hy_deg_hi.2.2.2.2.2, hv] + have hbody_eq : ampTrialBody = .seq copyMatrixCode + (.seq ram[activeK ← nOrig] (.seq ram[stride ← nOrig] + (.seq ram[targetT ← #2] (.seq (computeDegreesAndTotalAt hr22) + (.seq (contractDownToAt hr22) ampTrialPost))))) := rfl + rw [hbody_eq] + refine ((ExecRandLaw.seq_det e_cp (ExecRandLaw.seq_det ec1.within + (ExecRandLaw.seq_det ec2.within (ExecRandLaw.seq_det ec3.within + (ExecRandLaw.seq_det e_deg hrun))))).congr_law ?_).mono (fun _ h => h) ?_ (by omega) + · rw [Lean.Karger.answerLaw_eq, PMF.map_comp] + exact PMF.bind_pure_comp _ _ + · have hnn : n * n = n ^ 2 := (sq n).symm + omega + +/-- **The loop of trials runs amplified Karger.** From `AmpInv` at trial `i`, with `rem = R - i` +trials left, `ampLoop` runs within `rem (50 n² + 12 n + 30) + 2` instructions and `rem (n - 2)` +`rand` calls and ends at trial `R`. Its `bestVal` has the law of the amplification client run +against independent runs of `Lean.Karger.karger` on `⟨n, W⟩`: of `Lean.Karger.minRuns rem` on the +first trial, and of `rem` more `Lean.Karger.minStep`s from `bestVal` after. -/ +theorem ampLoop_law {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {mem₀ : ℕ → ℕ} + (hR : 1 ≤ R) (hn : 2 ≤ n) (hW : IsMultigraph W) (h1 : Fits w 1) (hdEnd : Fits w (sb + 2 * (n * n) + n)) (hR_fit : Fits w R) (htot : Fits w (totalDoubledWeight W)) : - ∀ (rem i : ℕ) (x : Data 22), - i + rem = R → - AmpInv w sb n R i W mem₀ x → - ∃ m : ProbComp (Data 22 × ℕ), - ExecRand w ampLoop x m ∧ - m.IsQueryBounded (rem * (n - 2)) ∧ - (∀ z ∈ m.support, - z.2 ≤ rem * (50 * n ^ 2 + 12 * n + 30) + 2 ∧ - AmpInv w sb n R R W mem₀ z.1 ∧ - (0 < i → x.regs bestVal = minCut W → z.1.regs bestVal = minCut W)) ∧ - (0 < minCut W → - m.eval.toOuterMeasure {z | z.1.regs bestVal ≠ minCut W} ≤ - ((1 : ℝ≥0∞) - (2 : ℝ≥0∞) / ((n * (n - 1) : ℕ) : ℝ≥0∞)) ^ rem) := by + ∀ (rem i : ℕ) (x : Data 22), i + rem = R → AmpInv w sb n R i W mem₀ x → + ExecRandLaw w ampLoop x (AmpInv w sb n R R W mem₀) + (rem * (50 * n ^ 2 + 12 * n + 30) + 2) (rem * (n - 2)) (fun y => y.regs bestVal) + (OracleComp.evalWith (fun _ => Lean.Karger.answerLaw ⟨n, W⟩) + (if i = 0 then Lean.Karger.minRuns rem + else OracleComp.iterate rem Lean.Karger.minStep (x.regs bestVal))) := by intro rem induction rem with | zero => intro i x hiR hinv - have hi_eq : i = R := by omega - subst hi_eq + obtain rfl : i = R := by omega have hc : ¬(Cond.lt trialIdx numTrials).Holds x := by simp [Cond.holds_lt, hinv.regs_trialIdx, hinv.regs_numTrials] - refine ⟨pure (x, 2), .loop_exit hc, .pure _ _, ?_, ?_⟩ - · intro z hz - cases OracleComp.eq_of_mem_supportWith_pure hz - exact ⟨by simp, hinv, fun _ hbv => hbv⟩ - · intro _ - simp only [pow_zero] - exact Cslib.Probability.PMF.toOuterMeasure_le_one _ _ + rw [ite_eq_right (by omega)] + exact (ExecRandLaw.loop_exit hc hinv).mono (fun _ h => h) (by omega) (Nat.zero_le _) | succ rem ih => intro i x hiR hinv - have hi_lt : i < R := by omega have hc : (Cond.lt trialIdx numTrials).Holds x := by - simp [Cond.holds_lt, hinv.regs_trialIdx, hinv.regs_numTrials, hi_lt] - obtain ⟨m_b, hm_b, hq_b, hsup_b, hfail_b⟩ := - ampTrialBody_spec hn hW hi_lt h1 hdEnd hR_fit htot hinv - have hnext : ∀ z₁ ∈ m_b.support, - ∃ m_r : ProbComp (Data 22 × ℕ), - ExecRand w ampLoop z₁.1 m_r ∧ - m_r.IsQueryBounded (rem * (n - 2)) ∧ - (∀ z₂ ∈ m_r.support, - z₂.2 ≤ rem * (50 * n ^ 2 + 12 * n + 30) + 2 ∧ - AmpInv w sb n R R W mem₀ z₂.1 ∧ - (0 < i + 1 → z₁.1.regs bestVal = minCut W → z₂.1.regs bestVal = minCut W)) ∧ - (0 < minCut W → - m_r.eval.toOuterMeasure {z | z.1.regs bestVal ≠ minCut W} ≤ - ((1 : ℝ≥0∞) - (2 : ℝ≥0∞) / ((n * (n - 1) : ℕ) : ℝ≥0∞)) ^ rem) := by - intro z₁ hz₁ - exact ih (i + 1) z₁.1 (by omega) (hsup_b z₁ hz₁).2.1 - obtain ⟨ml, hml_def⟩ : - ∃ ml : Data 22 → ProbComp (Data 22 × ℕ), - ∀ d, ml d = codeComp w ampLoop d := ⟨_, fun _ => rfl⟩ - have hml_exec : ∀ z₁ ∈ m_b.support, ExecRand w ampLoop z₁.1 (ml z₁.1) := by - intro z₁ hz₁ - obtain ⟨m_r, hm_r, _⟩ := hnext z₁ hz₁ - rw [hml_def] - simpa only [hm_r.codeComp_eq] using hm_r - have hm_iter : ExecRand w ampLoop x - (do let z₁ ← m_b; let z₂ ← ml z₁.1; pure (z₂.1, z₁.2 + z₂.2 + 2)) := - ExecRand.loop_iter hc hm_b hml_exec - let m_total := (do let z₁ ← m_b; let z₂ ← ml z₁.1; pure (z₂.1, z₁.2 + z₂.2 + 2)) - refine ⟨m_total, hm_iter, ?_, ?_, ?_⟩ - · have hq_each : ∀ z₁ ∈ m_b.support, - (ml z₁.1 >>= fun z₂ => pure (z₂.1, z₁.2 + z₂.2 + 2)).IsQueryBounded - (rem * (n - 2)) := by - intro z₁ hz₁ - obtain ⟨m_r, hm_r, hq_r, _⟩ := hnext z₁ hz₁ - rw [hml_def, hm_r.codeComp_eq] - simpa only [Nat.add_zero] using hq_r.bind fun _ => .pure _ 0 - have hq_tot := OracleComp.IsCostBounded.bind_on_support hq_b hq_each - exact hq_tot.mono (by rw [Nat.succ_mul, Nat.add_comm]) - · intro z hz - obtain ⟨z₁, hz₁, hrest⟩ := OracleComp.mem_supportWith_bind_iff.mp hz - obtain ⟨m_r, hm_r, _, hsup_r, _⟩ := hnext z₁ hz₁ - rw [hml_def, hm_r.codeComp_eq] at hrest - obtain ⟨z₂, hz₂, hpure⟩ := OracleComp.mem_supportWith_bind_iff.mp hrest - cases OracleComp.eq_of_mem_supportWith_pure hpure - rcases hsup_b z₁ hz₁ with ⟨ht₁, _, hstick₁⟩ - rcases hsup_r z₂ hz₂ with ⟨ht₂, hinv₂, hstick₂⟩ - refine ⟨?_, hinv₂, ?_⟩ - · rw [Nat.succ_mul] - omega - · intro hi_pos hbv_x - exact hstick₂ (Nat.succ_pos i) (hstick₁ hi_pos hbv_x) - · intro hmin_pos - have hm_eval : m_total.eval = - m_b.eval.bind fun z₁ => - ((ml z₁.1).eval.map fun z₂ => (z₂.1, z₁.2 + z₂.2 + 2)) := by - dsimp only [m_total] - rw [ProbComp.eval_bind] - refine congrArg (m_b.eval.bind ·) (funext fun z₁ => ?_) - rw [bind_pure_comp, ProbComp.eval_map] - rw [hm_eval, pow_succ'] - refine toOuterMeasure_bind_le_mul_ennreal m_b.eval - (fun z₁ => (ml z₁.1).eval.map fun z₂ => (z₂.1, z₁.2 + z₂.2 + 2)) - {z₁ | z₁.1.regs bestVal ≠ minCut W} - {z | z.1.regs bestVal ≠ minCut W} - (q₁ := (1 : ℝ≥0∞) - (2 : ℝ≥0∞) / ((n * (n - 1) : ℕ) : ℝ≥0∞)) - (q₂ := ((1 : ℝ≥0∞) - (2 : ℝ≥0∞) / ((n * (n - 1) : ℕ) : ℝ≥0∞)) ^ rem) - (hfail_b hmin_pos) ?_ ?_ - · intro z₁ hz₁_eval _ - have hz₁ : z₁ ∈ m_b.support := (ProbComp.support_eval m_b) ▸ hz₁_eval - obtain ⟨m_r, hm_r, _, _, hfail_r⟩ := hnext z₁ hz₁ - rw [hml_def, hm_r.codeComp_eq, PMF.toOuterMeasure_map_apply] - exact hfail_r hmin_pos - · intro z₁ hz₁_eval hhit - have hz₁ : z₁ ∈ m_b.support := (ProbComp.support_eval m_b) ▸ hz₁_eval - have hbv₁ : z₁.1.regs bestVal = minCut W := not_not.mp hhit - obtain ⟨m_r, hm_r, _, hsup_r, _⟩ := hnext z₁ hz₁ - rw [hml_def, hm_r.codeComp_eq, PMF.toOuterMeasure_map_apply, - PMF.toOuterMeasure_apply] - refine tsum_eq_zero_iff.mpr ?_ - intro z₂ - by_cases hz₂_eval : z₂ ∈ m_r.eval.support - · have hz₂ : z₂ ∈ m_r.support := (ProbComp.support_eval m_r) ▸ hz₂_eval - have hbv₂ : z₂.1.regs bestVal = minCut W := - (hsup_r z₂ hz₂).2.2 (Nat.succ_pos i) hbv₁ - have hnot : z₂ ∉ ((fun z : Data 22 × ℕ => (z.1, z₁.2 + z.2 + 2)) ⁻¹' - {z : Data 22 × ℕ | z.1.regs bestVal ≠ minCut W}) := by - simp [hbv₂] - exact Set.indicator_of_notMem hnot _ - · have hp0 : m_r.eval z₂ = 0 := by simpa only [PMF.mem_support_iff, not_not] using hz₂_eval - simp [hp0] - -/-- Specification of `ampCore` for `1 ≤ R` trials from any state with `srcBase = sb`, -`nOrig = n`, `numTrials = R`, and `HoldsMatrix x.mem sb n W`. -/ -theorem ampCore_spec {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {x : Data 22} + simp [Cond.holds_lt, hinv.regs_trialIdx, hinv.regs_numTrials] + omega + refine ((ExecRandLaw.loop_iter hc (ampTrialBody_law hn hW (by omega) h1 hdEnd hR_fit htot hinv) + (κ := fun b => OracleComp.evalWith (fun _ => Lean.Karger.answerLaw ⟨n, W⟩) + (OracleComp.iterate rem Lean.Karger.minStep b)) fun y hy => by + have h := ih (i + 1) y (by omega) hy + rw [ite_eq_right (Nat.succ_ne_zero i)] at h + exact h).congr_law ?_).mono (fun _ h => h) (by rw [add_one_mul]; omega) + (by rw [add_one_mul]; omega) + by_cases hi : i = 0 + · simp [hi, Lean.Karger.minRuns, Function.comp_def] + · simp [hi, OracleComp.iterate_succ_bind, Lean.Karger.minStep, Function.comp_def] + +/-- **The amplification core runs amplified Karger.** For `1 ≤ R` trials, from a state with +`srcBase = sb`, `nOrig = n`, `numTrials = R` and `HoldsMatrix x.mem sb n W`, `ampCore` runs within +`R (50 n² + 12 n + 30) + 8` instructions and `R (n - 2)` `rand` calls and writes only the +workspace. Its `bestVal` has the law of `Lean.Karger.minRuns R` against independent runs of +`Lean.Karger.karger` on `⟨n, W⟩`. -/ +theorem ampCore_law {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {x : Data 22} (hR : 1 ≤ R) (hn : 2 ≤ n) (hW : IsMultigraph W) (hsb : x.regs srcBase = sb) (hnOrig : x.regs nOrig = n) (hnumT : x.regs numTrials = R) (h1 : Fits w 1) (hdEnd : Fits w (sb + 2 * (n * n) + n)) (hR_fit : Fits w R) (htot : Fits w (totalDoubledWeight W)) (hsrc_mat : HoldsMatrix x.mem sb n W) : - ∃ m : ProbComp (Data 22 × ℕ), - ExecRand w ampCore x m ∧ - m.IsQueryBounded (R * (n - 2)) ∧ - (∀ z ∈ m.support, - z.2 ≤ R * (50 * n ^ 2 + 12 * n + 30) + 8 ∧ - Modifies (Finset.Ico (sb + n * n) (sb + 2 * (n * n) + n)) x.mem z.1.mem ∧ - ∃ C : Finset (Fin n), IsNonTrivialCut C ∧ z.1.regs bestVal = cutWeight W C) ∧ - (0 < minCut W → - m.eval.toOuterMeasure {z | z.1.regs bestVal ≠ minCut W} ≤ - ((1 : ℝ≥0∞) - (2 : ℝ≥0∞) / ((n * (n - 1) : ℕ) : ℝ≥0∞)) ^ R) := by + ExecRandLaw w ampCore x + (fun y => Modifies (Finset.Ico (sb + n * n) (sb + 2 * (n * n) + n)) x.mem y.mem) + (R * (50 * n ^ 2 + 12 * n + 30) + 8) (R * (n - 2)) (fun y => y.regs bestVal) + (OracleComp.evalWith (fun _ => Lean.Karger.answerLaw ⟨n, W⟩) (Lean.Karger.minRuns R)) := by have hnn_fit : Fits w (n * n) := hdEnd.of_le (by omega) have hwb_fit : Fits w (sb + n * n) := hdEnd.of_le (by omega) have hdb_fit : Fits w (sb + 2 * (n * n)) := hdEnd.of_le (by omega) @@ -1246,7 +987,7 @@ theorem ampCore_spec {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {x : Data 22 have e5 : Exec (B := .standard) w ram[trialIdx ← #0] s₄ s₅ 1 := Exec.const (fits_zero w) have e6 : Exec (B := .standard) w ram[bestVal ← #0] s₅ s₆ 1 := Exec.const (fits_zero w) have hinv₀ : AmpInv w sb n R 0 W x.mem s₆ := by - refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, hsrc_mat, Modifies.refl _ _, fun h0 => absurd h0 (by omega)⟩ + refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, hsrc_mat, Modifies.refl _ _⟩ · simpa +decide [s₆, s₅, s₄, s₃, s₂, s₁, Function.update_apply] using hsb · simp +decide [s₆, s₅, s₄, s₃] · simp +decide [s₆, s₅, s₄] @@ -1254,25 +995,17 @@ theorem ampCore_spec {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {x : Data 22 · simp +decide [s₆, s₅, s₄, s₃, s₂] · simpa +decide [s₆, s₅, s₄, s₃, s₂, s₁, Function.update_apply] using hnumT · simp +decide [s₆, s₅] - obtain ⟨m_l, hm_l, hq_l, hsup_l, hfail_l⟩ := - ampLoop_spec (mem₀ := x.mem) hn hW h1 hdEnd hR_fit htot R 0 s₆ (Nat.zero_add R) hinv₀ + have hloop := ampLoop_law (mem₀ := x.mem) hR hn hW h1 hdEnd hR_fit htot R 0 s₆ + (Nat.zero_add R) hinv₀ + rw [ite_eq_left rfl] at hloop have hcore_eq : ampCore = .seq ram[val1 ← nOrig * nOrig] (.seq ram[matLen ← val1] (.seq ram[wBase ← srcBase + matLen] (.seq ram[dBase ← wBase + matLen] (.seq ram[trialIdx ← #0] (.seq ram[bestVal ← #0] ampLoop))))) := rfl rw [hcore_eq] - have hm_full := e1.seqRand (e2.seqRand (e3.seqRand (e4.seqRand (e5.seqRand (e6.seqRand hm_l))))) - refine ⟨_, hm_full, ?_, ?_, ?_⟩ - · simp only [Functor.map_map, OracleComp.IsQueryBounded, OracleComp.isCostBounded_map_iff] - exact hq_l - · intro z hz - simp only [Functor.map_map] at hz - obtain ⟨z₀, hz₀, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hz - rcases hsup_l z₀ hz₀ with ⟨ht₀, hinv_f, _⟩ - exact ⟨by omega, hinv_f.modifies_ws, hinv_f.best_cut hR⟩ - · intro hmin_pos - simp only [Functor.map_map, ProbComp.eval_map, PMF.toOuterMeasure_map_apply] - exact hfail_l hmin_pos + exact (ExecRandLaw.seq_det e1.within (ExecRandLaw.seq_det e2.within + (ExecRandLaw.seq_det e3.within (ExecRandLaw.seq_det e4.within (ExecRandLaw.seq_det e5.within + (ExecRandLaw.seq_det e6.within hloop)))))).mono (fun _ h => h.modifies_ws) (by omega) le_rfl end AmplificationEngine @@ -1337,37 +1070,24 @@ theorem amplifiedSetup_exec {w R n : ℕ} {W : Fin n → Fin n → ℕ} exact ⟨s₅, e1.seq (e2.seq (e3.seq (e4.seq e5))), rfl, by simp [s₅], by simp +decide [s₅, s₄], by simp +decide [s₅, s₄, s₃, s₂]⟩ -/-- Structured `ProbComp` specification of `amplifiedCode`. -/ -theorem amplifiedCode_spec {R n w : ℕ} {W : Fin n → Fin n → ℕ} +/-- **`amplifiedCode` runs amplified Karger.** At word size `w ≥ logWidth 3 n` with `1 ≤ R`, +`R < 2 ^ w` and `totalDoubledWeight W < 2 ^ w`, `amplifiedCode` on `R :: n :: flattenMatrix W` runs +within `amplifiedTime R n - 1` instructions and `R (n - 2)` `rand` calls and writes only +`[3 + n * n, 3 + 2 * (n * n) + n)`. Its `bestVal` has the law of `Lean.Karger.minRuns R` against +independent runs of `Lean.Karger.karger` on `⟨n, W⟩`. -/ +theorem amplifiedCode_law {R n w : ℕ} {W : Fin n → Fin n → ℕ} (hR : 1 ≤ R) (hn : 2 ≤ n) (hW : IsMultigraph W) (hw : logWidth 3 n ≤ w) (hR_fit : Fits w R) (htot : Fits w (totalDoubledWeight W)) : - ∃ m : ProbComp (Data 22 × ℕ), - ExecRand w amplifiedCode (Data.init (R :: n :: flattenMatrix W)) m ∧ - m.IsQueryBounded (R * (n - 2)) ∧ - (∀ z ∈ m.support, - z.2 + 1 ≤ amplifiedTime R n ∧ - Modifies (Finset.Ico (3 + n * n) (3 + 2 * (n * n) + n)) - (Data.init (r := 22) (R :: n :: flattenMatrix W)).mem z.1.mem ∧ - ∃ C : Finset (Fin n), IsNonTrivialCut C ∧ z.1.regs bestVal = cutWeight W C) ∧ - (0 < minCut W → - m.eval.toOuterMeasure {z | z.1.regs bestVal ≠ minCut W} ≤ - ((1 : ℝ≥0∞) - (2 : ℝ≥0∞) / ((n * (n - 1) : ℕ) : ℝ≥0∞)) ^ R) := by + ExecRandLaw w amplifiedCode (Data.init (R :: n :: flattenMatrix W)) + (fun y => Modifies (Finset.Ico (3 + n * n) (3 + 2 * (n * n) + n)) + (Data.init (r := 22) (R :: n :: flattenMatrix W)).mem y.mem) + (R * (50 * n ^ 2 + 12 * n + 30) + 15) (R * (n - 2)) (fun y => y.regs bestVal) + (OracleComp.evalWith (fun _ => Lean.Karger.answerLaw ⟨n, W⟩) (Lean.Karger.minRuns R)) := by have hws := fits_workspace_of_logWidth_three hn hw - have h1 : Fits w 1 := hws.of_le (by omega) obtain ⟨y_s, e_s, hm_s, hsb_s, hn_s, hnt_s⟩ := amplifiedSetup_exec (R := R) (W := W) hn hw - obtain ⟨m_c, hm_c, hq_c, hsup_c, hfail_c⟩ := - ampCore_spec hR hn hW hsb_s hn_s hnt_s h1 hws hR_fit htot - (hm_s ▸ holdsMatrix_init_amplified W) - refine ⟨_, e_s.seqRand hm_c, ?_, ?_, ?_⟩ - · simp only [OracleComp.IsQueryBounded, OracleComp.isCostBounded_map_iff] - exact hq_c - · intro z hz - obtain ⟨z₀, hz₀, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hz - rcases hsup_c z₀ hz₀ with ⟨ht₀, hmod₀, hcut₀⟩ - exact ⟨by simp only [amplifiedTime]; omega, hm_s ▸ hmod₀, hcut₀⟩ - · intro hmin_pos - rw [ProbComp.eval_map, PMF.toOuterMeasure_map_apply] - exact hfail_c hmin_pos + exact (ExecRandLaw.seq_det e_s.within (ampCore_law hR hn hW hsb_s hn_s hnt_s + (hws.of_le (by omega)) hws hR_fit htot (hm_s ▸ holdsMatrix_init_amplified W))).mono + (fun _ h => hm_s ▸ h) (by omega) le_rfl /-- **`R`-trial amplified Karger specification (`amplifiedProgram`).** At word size `w ≥ logWidth 3 n` when `1 ≤ R`, `R < 2 ^ w`, and `totalDoubledWeight W < 2 ^ w`: @@ -1397,29 +1117,14 @@ theorem amplifiedProgram_spec {R n w : ℕ} {W : Fin n → Fin n → ℕ} {cfg | ∀ y, cfg ≠ .halted (minCut W) y} ≤ ((1 : ℝ≥0∞) - (2 : ℝ≥0∞) / ((n * (n - 1) : ℕ) : ℝ≥0∞)) ^ R) := by intro input - have hfit_in : InputFits w input := inputFits_amplified hn hw hR_fit htot - obtain ⟨m, hm, hq, hsup, hfail⟩ := amplifiedCode_spec hR hn hW hw hR_fit htot - have hrun : runRand w amplifiedProgram (amplifiedTime R n) (.running (.init input)) = - (fun z : Data 22 × ℕ => RandCfg.halted (z.1.regs bestVal) z.1) <$> m := - hm.runRand_program bestVal fun z hz => (hsup z hz).1 - refine ⟨?_, ?_, ?_, ?_⟩ - · intro cfg hcfg - rw [hrun] at hcfg - obtain ⟨z, -, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hcfg - exact ⟨z.1.regs bestVal, z.1, rfl⟩ - · rw [RandCallsBounded, hrun] - exact (OracleComp.isCostBounded_map_iff _ _ _).mpr hq - · intro cfg hcfg - have hbnd := runRand_bounded_init hfit_in hcfg - rw [hrun] at hcfg - obtain ⟨z, hz, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hcfg - rcases hsup z hz with ⟨_, hmod, C, hC_nt, hbv⟩ - exact ⟨z.1, C, by rw [hbv], hbnd.2, hC_nt, minCut_le_cutWeight W hC_nt, hmod⟩ - · intro hmin_pos - rw [evalRand, hrun, ProbComp.eval_map, PMF.toOuterMeasure_map_apply] - refine (PMF.toOuterMeasure_mono _ ?_).trans (hfail hmin_pos) - intro z hz heq - exact hz.1 z.1 (congrArg (fun v => RandCfg.halted v z.1) heq) + obtain ⟨hhalt, hcalls, hpost, -, hmiss⟩ := + program_of_law (T' := amplifiedTime R n) (amplifiedCode_law hR hn hW hw hR_fit htot) + (by unfold amplifiedTime; omega) + (inputFits_amplified hn hw hR_fit htot) + fun _ hv => Lean.Karger.exists_cut_of_mem_support_answerLaw hn hW + (Lean.Karger.mem_support_minRuns (by omega) hv) + exact ⟨hhalt, hcalls, hpost, fun hmin => + hmiss.trans (Lean.Karger.minRuns_ne_minCut_le hn hW hmin R)⟩ end Amplified @@ -1624,9 +1329,10 @@ theorem highProbSetup_exec {w n : ℕ} {W : Fin n → Fin n → ℕ} (e_loop.seq ((p1.within).seq ((p2.within).seq ((p3.within).seq ((p4.within).seq ((p5.within).seq ((p6.within).seq p7.within))))))))))).mono (by omega) -private theorem highProbTime_bound {n : ℕ} (hn : 2 ≤ n) : - (4 * Nat.log 2 n + 13) + (highProbTrials n * (50 * n ^ 2 + 12 * n + 30) + 8) + 1 ≤ - highProbTime n := by +/-- The setup's `4 log₂ n + 13` instructions, the `highProbTrials n` trials' +`highProbTrials n (50 n² + 12 n + 30) + 8` and the final halt fit in `highProbTime n`. -/ +theorem highProbTime_bound {n : ℕ} (hn : 2 ≤ n) : + 4 * Nat.log 2 n + highProbTrials n * (50 * n ^ 2 + 12 * n + 30) + 22 ≤ highProbTime n := by unfold highProbTime highProbTrials obtain ⟨d, rfl⟩ : ∃ d, n = d + 2 := ⟨n - 2, by omega⟩ have h1 : 50 * (d + 2) ^ 2 + 12 * (d + 2) + 30 ≤ 64 * (d + 2) ^ 2 := by nlinarith @@ -1650,9 +1356,9 @@ private theorem highProbTime_bound {n : ℕ} (hn : 2 ≤ n) : have hpow4 : 16 ≤ (d + 2) ^ 4 := by nlinarith nlinarith calc - (4 * Nat.log 2 (d + 2) + 13) + - (((d + 2) * (d + 2 - 1) / 2 * (Nat.log 2 (d + 2) + 2)) * - (50 * (d + 2) ^ 2 + 12 * (d + 2) + 30) + 8) + 1 + 4 * Nat.log 2 (d + 2) + + ((d + 2) * (d + 2 - 1) / 2 * (Nat.log 2 (d + 2) + 2)) * + (50 * (d + 2) ^ 2 + 12 * (d + 2) + 30) + 22 = (4 * Nat.log 2 (d + 2) + 22) + (((d + 2) * (d + 2 - 1) / 2 * (Nat.log 2 (d + 2) + 2)) * (50 * (d + 2) ^ 2 + 12 * (d + 2) + 30)) := by ring @@ -1660,41 +1366,27 @@ private theorem highProbTime_bound {n : ℕ} (hn : 2 ≤ n) : 32 * (d + 2) ^ 4 * (Nat.log 2 (d + 2) + 2) := Nat.add_le_add hoverhead htrial _ = 33 * (d + 2) ^ 4 * (Nat.log 2 (d + 2) + 2) := by ring -/-- Structured `ProbComp` specification of `highProbCode`. -/ -theorem highProbCode_spec {n w : ℕ} {W : Fin n → Fin n → ℕ} +/-- **`highProbCode` runs amplified Karger.** At word size `w ≥ logWidth 3 n` with +`totalDoubledWeight W < 2 ^ w`, `highProbCode` on `n :: flattenMatrix W` runs within +`4 log₂ n + highProbTrials n (50 n² + 12 n + 30) + 21` instructions and +`highProbTrials n (n - 2)` `rand` calls and writes only `[2 + n * n, 2 + 2 * (n * n) + n)`. Its +`bestVal` has the law of `Lean.Karger.minRuns (highProbTrials n)` against independent runs of +`Lean.Karger.karger` on `⟨n, W⟩`. -/ +theorem highProbCode_law {n w : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hW : IsMultigraph W) (hw : logWidth 3 n ≤ w) (htot : Fits w (totalDoubledWeight W)) : - ∃ m : ProbComp (Data 22 × ℕ), - ExecRand w highProbCode (Data.init (n :: flattenMatrix W)) m ∧ - m.IsQueryBounded (highProbTrials n * (n - 2)) ∧ - (∀ z ∈ m.support, - z.2 + 1 ≤ highProbTime n ∧ - Modifies (Finset.Ico (2 + n * n) (2 + 2 * (n * n) + n)) - (Data.init (r := 22) (n :: flattenMatrix W)).mem z.1.mem ∧ - ∃ C : Finset (Fin n), IsNonTrivialCut C ∧ z.1.regs bestVal = cutWeight W C) ∧ - (0 < minCut W → - m.eval.toOuterMeasure {z | z.1.regs bestVal ≠ minCut W} ≤ - (1 : ℝ≥0∞) / ((2 * n : ℕ) : ℝ≥0∞)) := by + ExecRandLaw w highProbCode (Data.init (n :: flattenMatrix W)) + (fun y => Modifies (Finset.Ico (2 + n * n) (2 + 2 * (n * n) + n)) + (Data.init (r := 22) (n :: flattenMatrix W)).mem y.mem) + (4 * Nat.log 2 n + highProbTrials n * (50 * n ^ 2 + 12 * n + 30) + 21) + (highProbTrials n * (n - 2)) (fun y => y.regs bestVal) + (OracleComp.evalWith (fun _ => Lean.Karger.answerLaw ⟨n, W⟩) + (Lean.Karger.minRuns (highProbTrials n))) := by have hws := fits_workspace_of_logWidth_three hn hw - have h1 : Fits w 1 := hws.of_le (by omega) - have hdEnd : Fits w (2 + 2 * (n * n) + n) := hws.of_le (by omega) - have hhp_fit := fits_highProbTrials_of_logWidth_three hn hw - obtain ⟨y_s, ⟨n_s, hn_s, e_s⟩, hm_s, hsb_s, hn_s_r, hnt_s⟩ := - highProbSetup_exec (W := W) hn hw - obtain ⟨m_c, hm_c, hq_c, hsup_c, hfail_c⟩ := - ampCore_spec (highProbTrials_pos hn) hn hW hsb_s hn_s_r hnt_s h1 hdEnd hhp_fit htot - (hm_s ▸ holdsMatrix_init_single W) - have hbound := highProbTime_bound hn - refine ⟨_, e_s.seqRand hm_c, ?_, ?_, ?_⟩ - · simp only [OracleComp.IsQueryBounded, OracleComp.isCostBounded_map_iff] - exact hq_c - · intro z hz - obtain ⟨z₀, hz₀, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hz - rcases hsup_c z₀ hz₀ with ⟨ht₀, hmod₀, hcut₀⟩ - exact ⟨by omega, hm_s ▸ hmod₀, hcut₀⟩ - · intro hmin_pos - rw [ProbComp.eval_map, PMF.toOuterMeasure_map_apply] - exact (hfail_c hmin_pos).trans (highProb_failure_le hn) + obtain ⟨y_s, e_s, hm_s, hsb_s, hn_s, hnt_s⟩ := highProbSetup_exec (W := W) hn hw + exact (ExecRandLaw.seq_det e_s (ampCore_law (highProbTrials_pos hn) hn hW hsb_s hn_s hnt_s + (hws.of_le (by omega)) (hws.of_le (by omega)) (fits_highProbTrials_of_logWidth_three hn hw) + htot (hm_s ▸ holdsMatrix_init_single W))).mono (fun _ h => hm_s ▸ h) (by omega) le_rfl /-- **Explicit `O(n ^ 4 log n)` high-probability global minimum cut (`highProbProgram`).** At word size `w ≥ logWidth 3 n` when `2 ≤ n` and `totalDoubledWeight W < 2 ^ w`: @@ -1724,29 +1416,13 @@ theorem highProbProgram_spec {n w : ℕ} {W : Fin n → Fin n → ℕ} {cfg | ∀ y, cfg ≠ .halted (minCut W) y} ≤ (1 : ℝ≥0∞) / ((2 * n : ℕ) : ℝ≥0∞)) := by intro input - have hfit_in : InputFits w input := inputFits_single hn hw htot - obtain ⟨m, hm, hq, hsup, hfail⟩ := highProbCode_spec hn hW hw htot - have hrun : runRand w highProbProgram (highProbTime n) (.running (.init input)) = - (fun z : Data 22 × ℕ => RandCfg.halted (z.1.regs bestVal) z.1) <$> m := - hm.runRand_program bestVal fun z hz => (hsup z hz).1 - refine ⟨?_, ?_, ?_, ?_⟩ - · intro cfg hcfg - rw [hrun] at hcfg - obtain ⟨z, -, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hcfg - exact ⟨z.1.regs bestVal, z.1, rfl⟩ - · rw [RandCallsBounded, hrun] - exact (OracleComp.isCostBounded_map_iff _ _ _).mpr hq - · intro cfg hcfg - have hbnd := runRand_bounded_init hfit_in hcfg - rw [hrun] at hcfg - obtain ⟨z, hz, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hcfg - rcases hsup z hz with ⟨_, hmod, C, hC_nt, hbv⟩ - exact ⟨z.1, C, by rw [hbv], hbnd.2, hC_nt, minCut_le_cutWeight W hC_nt, hmod⟩ - · intro hmin_pos - rw [evalRand, hrun, ProbComp.eval_map, PMF.toOuterMeasure_map_apply] - refine (PMF.toOuterMeasure_mono _ ?_).trans (hfail hmin_pos) - intro z hz heq - exact hz.1 z.1 (congrArg (fun v => RandCfg.halted v z.1) heq) + obtain ⟨hhalt, hcalls, hpost, -, hmiss⟩ := + program_of_law (highProbCode_law hn hW hw htot) (highProbTime_bound hn) + (inputFits_single hn hw htot) fun _ hv => + Lean.Karger.exists_cut_of_mem_support_answerLaw hn hW + (Lean.Karger.mem_support_minRuns (Nat.one_le_iff_ne_zero.mp (highProbTrials_pos hn)) hv) + exact ⟨hhalt, hcalls, hpost, fun hmin => + (hmiss.trans (Lean.Karger.minRuns_ne_minCut_le hn hW hmin _)).trans (highProb_failure_le hn)⟩ /-- Corollary of `highProbProgram_spec`: when `0 < minCut W`, `highProbProgram` misses `minCut W` with probability at most `1 / n`. -/ diff --git a/Complexity/Computability/WordRAM/Randomized/Law.lean b/Complexity/Computability/WordRAM/Randomized/Law.lean index da5b674dff..140259bc45 100644 --- a/Complexity/Computability/WordRAM/Randomized/Law.lean +++ b/Complexity/Computability/WordRAM/Randomized/Law.lean @@ -42,6 +42,7 @@ with `f` (`Cslib.WordRAM.ExecRandLaw.program`). * `Cslib.WordRAM.ExecRandLaw.seq`, `Cslib.WordRAM.ExecRandLaw.branch_pos`, `Cslib.WordRAM.ExecRandLaw.branch_neg`, `Cslib.WordRAM.ExecRandLaw.loop_exit`, `Cslib.WordRAM.ExecRandLaw.loop_iter`: composition rules. +* `Cslib.WordRAM.ExecRandLaw.rename`: renaming registers. * `Cslib.WordRAM.ExecRandLaw.execRandWithin`: forgetting the law. * `Cslib.WordRAM.ExecRandLaw.program`: the compiled program halts within the bound, respects the call budget and the postcondition, and has the law `μ`. @@ -88,6 +89,18 @@ theorem withPreserves {i : Fin r} (h : ExecRandLaw w c x P T R f μ) (hi : c.Pre obtain ⟨m, hm, hq, hsup, hlaw⟩ := h exact ⟨m, hm, hq, fun z hz => ⟨⟨(hsup z hz).1, hm.regs_eq hi hz⟩, (hsup z hz).2⟩, hlaw⟩ +/-- Renaming along an injective register map `ρ`: the renamed code observes the registers that `ρ` +chooses and keeps the others. -/ +theorem rename {r' : ℕ} {ρ : Fin r → Fin r'} (hρ : ρ.Injective) {x' : Data r'} + (h : ExecRandLaw w c (x'.comap ρ) P T R f μ) : + ExecRandLaw w (c.rename ρ) x' (fun y' => ∃ y, P y ∧ y' = y.extend ρ x') T R + (fun y' => f (y'.comap ρ)) μ := by + obtain ⟨m, hm, hq, hsup, hlaw⟩ := h + refine ⟨_, hm.rename hρ, (OracleComp.isCostBounded_map_iff _ _ _).mpr hq, fun z hz => ?_, ?_⟩ + · obtain ⟨z₀, hz₀, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hz + exact ⟨⟨z₀.1, (hsup z₀ hz₀).1, rfl⟩, (hsup z₀ hz₀).2⟩ + · simpa only [Functor.map_map, Data.comap_extend hρ] using hlaw + /-- Deterministic code reaching `y` has the point law at the observation of `y`. -/ theorem of_execWithin {y : Data r} (h : ExecWithin w c x y T) (hy : P y) : ExecRandLaw w c x P T 0 f (PMF.pure (f y)) := by diff --git a/abstracts/ComplexityAbstracts/KargerMinCutBridge.lean b/abstracts/ComplexityAbstracts/KargerMinCutBridge.lean index 68a967dcf9..1c9e8d3c8e 100644 --- a/abstracts/ComplexityAbstracts/KargerMinCutBridge.lean +++ b/abstracts/ComplexityAbstracts/KargerMinCutBridge.lean @@ -929,20 +929,20 @@ private theorem ampLoop_exact {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {me have hc : (Cond.lt trialIdx numTrials).Holds x := by simp [Cond.holds_lt, hinv.regs_trialIdx, hinv.regs_numTrials, hiR] obtain ⟨m_b, hm_b, _, hsup_b, _⟩ := - ampTrialBody_spec hn hW hiR h1 hdEnd hR_fit htot hinv + ampTrialBody_law hn hW hiR h1 hdEnd hR_fit htot hinv have hm_b_ex := ampTrialBody_toExact hn hW hiR h1 hdEnd hR_fit htot hinv hm_b let ml (d : Data 22) := codeComp (B := .standard) w ampLoop d refine ⟨_, ExecRand.loop_iter hc hm_b (ml := ml) ?_, ExecRand.loop_iter hc hm_b_ex (ml := ml) ?_⟩ · intro z hz obtain ⟨m_r, hm_r⟩ := ampLoop_exact hn hW h1 hdEnd hR_fit htot r (i + 1) z.1 - (by omega) (hsup_b z hz).2.1 + (by omega) (hsup_b z hz).1 dsimp only [ml] rw [hm_r.1.codeComp_eq] exact hm_r.1 · intro z hz obtain ⟨m_r, hm_r⟩ := ampLoop_exact hn hW h1 hdEnd hR_fit htot r (i + 1) z.1 - (by omega) (hsup_b z hz).2.1 + (by omega) (hsup_b z hz).1 dsimp only [ml] rw [hm_r.1.codeComp_eq] exact hm_r.2 @@ -987,7 +987,7 @@ private theorem ampCore_exact {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {x have e5 : Exec (B := .standard) w ram[trialIdx ← #0] s₄ s₅ 1 := Exec.const (fits_zero w) have e6 : Exec (B := .standard) w ram[bestVal ← #0] s₅ s₆ 1 := Exec.const (fits_zero w) have hinv₀ : AmpInv w sb n R 0 W x.mem s₆ := by - refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, hsrc_mat, Modifies.refl _ _, fun h0 => absurd h0 (by omega)⟩ + refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, hsrc_mat, Modifies.refl _ _⟩ · exact (set_regs_ne _ _ _ _ (by decide)).trans ((set_regs_ne _ _ _ _ (by decide)).trans ((set_regs_ne _ _ _ _ (by decide)).trans ((set_regs_ne _ _ _ _ (by decide)).trans ((set_regs_ne _ _ _ _ (by decide)).trans ((set_regs_ne _ _ _ _ (by decide)).trans hsb))))) @@ -2257,10 +2257,11 @@ private theorem singleExactProgram_runRand_eq {n w : ℕ} {W : Fin n → Fin n (.running (.init (n :: flattenMatrix W))) = Cslib.WordRAM.runRand w singleProgram (singleTime n) (.running (.init (n :: flattenMatrix W))) := by - obtain ⟨m, hm_std, _, hsup, _⟩ := singleCode_spec hn hW hw htot + obtain ⟨m, hm_std, _, hsup, _⟩ := singleCode_law hn hW hw htot have hm_ex := singleCode_toExact hn hW hw htot hm_std - exact (hm_ex.runRand_program Reg.val1 fun z hz => (hsup z hz).1).trans - (hm_std.runRand_program Reg.val1 fun z hz => (hsup z hz).1).symm + have hT : ∀ z ∈ m.support, z.2 + 1 ≤ singleTime n := fun z hz => + Nat.add_le_add_right (hsup z hz).2 1 + exact (hm_ex.runRand_program Reg.val1 hT).trans (hm_std.runRand_program Reg.val1 hT).symm private theorem amplifiedExactProgram_runRand_eq {R n w : ℕ} {W : Fin n → Fin n → ℕ} (hR : 1 ≤ R) (hn : 2 ≤ n) (hW : IsMultigraph W) (hw : logWidth 3 n ≤ w) @@ -2269,10 +2270,12 @@ private theorem amplifiedExactProgram_runRand_eq {R n w : ℕ} {W : Fin n → Fi (.running (.init (R :: n :: flattenMatrix W))) = Cslib.WordRAM.runRand w amplifiedProgram (amplifiedTime R n) (.running (.init (R :: n :: flattenMatrix W))) := by - obtain ⟨m, hm_std, _, hsup, _⟩ := amplifiedCode_spec hR hn hW hw hR_fit htot + obtain ⟨m, hm_std, _, hsup, _⟩ := amplifiedCode_law hR hn hW hw hR_fit htot have hm_ex := amplifiedCode_toExact hn hW hw hR_fit htot hm_std - exact (hm_ex.runRand_program AmpReg.bestVal fun z hz => (hsup z hz).1).trans - (hm_std.runRand_program AmpReg.bestVal fun z hz => (hsup z hz).1).symm + have hT : ∀ z ∈ m.support, z.2 + 1 ≤ amplifiedTime R n := fun z hz => + Nat.add_le_add_right (hsup z hz).2 1 + exact (hm_ex.runRand_program AmpReg.bestVal hT).trans + (hm_std.runRand_program AmpReg.bestVal hT).symm private theorem highProbExactProgram_runRand_eq {n w : ℕ} {W : Fin n → Fin n → ℕ} (hn : 2 ≤ n) (hW : IsMultigraph W) (hw : logWidth 3 n ≤ w) @@ -2281,10 +2284,12 @@ private theorem highProbExactProgram_runRand_eq {n w : ℕ} {W : Fin n → Fin n (.running (.init (n :: flattenMatrix W))) = Cslib.WordRAM.runRand w highProbProgram (highProbTime n) (.running (.init (n :: flattenMatrix W))) := by - obtain ⟨m, hm_std, _, hsup, _⟩ := highProbCode_spec hn hW hw htot + obtain ⟨m, hm_std, _, hsup, _⟩ := highProbCode_law hn hW hw htot have hm_ex := highProbCode_toExact hn hW hw htot hm_std - exact (hm_ex.runRand_program AmpReg.bestVal fun z hz => (hsup z hz).1).trans - (hm_std.runRand_program AmpReg.bestVal fun z hz => (hsup z hz).1).symm + have hT : ∀ z ∈ m.support, z.2 + 1 ≤ highProbTime n := fun z hz => + (Nat.add_le_add_right (hsup z hz).2 1).trans (highProbTime_bound hn) + exact (hm_ex.runRand_program AmpReg.bestVal hT).trans + (hm_std.runRand_program AmpReg.bestVal hT).symm private theorem init_mem_eq {r : ℕ} (input : List ℕ) : (Data.init (r := r) input).mem = Presentation.initMem input := by