no sw
The theorem ledger
Every theorem the Lean kernel accepted in the Qpu modules, read from the environment by scripts/theorems.lean on 2026-10-25: 993 constants, of which 491 hand-written and 502 equation and match lemmas the compiler generated beside them; 0 depend on sorryAx; axioms used: Classical.choice, Quot.sound, propext. The ledger is also served as /theorems.ndjson, one JSON line per theorem, the form offered to the unit's deposit door.
| Module | Hand-written theorems |
|---|---|
| Qpu.Annealing | 1 |
| Qpu.Anyon | 1 |
| Qpu.Cern | 1 |
| Qpu.Circuit | 22 |
| Qpu.Clay | 55 |
| Qpu.Clifford | 1 |
| Qpu.Coil | 9 |
| Qpu.Combinatorics | 13 |
| Qpu.Cross | 16 |
| Qpu.Fuse | 1 |
| Qpu.Fusion | 4 |
| Qpu.Galois | 1 |
| Qpu.Grover | 1 |
| Qpu.Hybrid | 3 |
| Qpu.Lattice | 38 |
| Qpu.Leads.CausalInference | 39 |
| Qpu.Leads.ExplainableAI | 47 |
| Qpu.Leads.FederatedLearning | 60 |
| Qpu.Leads.HarmonicClosure | 6 |
| Qpu.Leads.ProgramSynthesis | 57 |
| Qpu.Leads.ZeroShotLearning | 52 |
| Qpu.Magic | 1 |
| Qpu.Mint | 4 |
| Qpu.Physics | 4 |
| Qpu.Pi | 8 |
| Qpu.Primes | 13 |
| Qpu.Qaoa | 1 |
| Qpu.Qft | 1 |
| Qpu.Shor | 2 |
| Qpu.Sigma | 17 |
| Qpu.Stabilizer | 1 |
| Qpu.Surfacecode | 1 |
| Qpu.Textbook | 10 |
| Key | Statement | Axioms |
|---|---|---|
Qpu.CausalInference.ate_bounded | ∀ (s : Qpu.CausalInference.Study), s.bounded → s.sumY s.treated * s.control.length ≤ s.sumY s.control * s.treated.length + s.ymax * s.treated.length * s.control.length ∧ s.sumY s.control * s.treated.length ≤ s.sumY s.treated * s.control.length + s.ymax * s.treated.length * s.control.length | propext, Quot.sound |
Qpu.CausalInference.children_gt | ∀ {g : Qpu.CausalInference.Dag}, g.ordered = true → ∀ {c v : Nat}, c ∈ g.children v → v < c | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.common_support | ∀ (s : Qpu.CausalInference.Study), s.overlap → s.units ≠ [] → s.treated ≠ [] ∧ s.control ≠ [] | propext, Quot.sound |
Qpu.CausalInference.do_consistent | ∀ {m : Qpu.CausalInference.Scm}, m.ordered = true → ∀ (u : Nat → Nat) (x v : Nat), (m.doOp x (m.value u x)).value u v = m.value u v | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.do_ordered | ∀ {m : Qpu.CausalInference.Scm}, m.ordered = true → ∀ (x c : Nat), (m.doOp x c).vars = m.vars ∧ (m.doOp x c).ordered = true | propext, Quot.sound |
Qpu.CausalInference.do_parents_ne | ∀ (m : Qpu.CausalInference.Scm) {x v : Nat}, v ≠ x → ∀ (c : Nat), (m.doOp x c).parents v = m.parents v | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.do_parents_self | ∀ (m : Qpu.CausalInference.Scm) (x c : Nat), (m.doOp x c).parents x = [] | propext |
Qpu.CausalInference.do_pre_treatment | ∀ {m : Qpu.CausalInference.Scm}, m.ordered = true → ∀ (u : Nat → Nat) {x v : Nat}, v < x → ∀ (c : Nat), (m.doOp x c).value u v = m.value u v | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.do_valueF_consistent | ∀ {m : Qpu.CausalInference.Scm}, m.ordered = true → ∀ (u : Nat → Nat) (x f v : Nat), v < f → (m.doOp x (m.value u x)).valueF u f v = m.valueF u f v | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.do_valueF_exogenous | ∀ (m : Qpu.CausalInference.Scm) (u : Nat → Nat) {x : Nat}, m.exogenous x → ∀ (c f v : Nat), (m.doOp x c).valueF u f v = m.valueF (fun w => if w = x then c else u w) f v | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.do_valueF_pre | ∀ {m : Qpu.CausalInference.Scm}, m.ordered = true → ∀ (u : Nat → Nat) (x c f v : Nat), v < x → (m.doOp x c).valueF u f v = m.valueF u f v | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.do_value_self | ∀ (m : Qpu.CausalInference.Scm) (u : Nat → Nat) (x c : Nat), (m.doOp x c).value u x = c | propext |
Qpu.CausalInference.exogenous_do_eq_see | ∀ (m : Qpu.CausalInference.Scm) (u : Nat → Nat) {x : Nat}, m.exogenous x → ∀ (c v : Nat), (m.doOp x c).value u v = m.value (fun w => if w = x then c else u w) v | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.filter_filter_ne | ∀ {x v : Nat}, v ≠ x → ∀ (l : List (Nat × Nat)), List.filter (fun e => e.snd == v) (List.filter (fun e => !e.snd == x) l) = List.filter (fun e => e.snd == v) l | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.filter_filter_not | ∀ {α : Type} (p : α → Bool) (l : List α), List.filter p (List.filter (fun a => !p a) l) = [] | propext |
Qpu.CausalInference.hte_bounded_average | ∀ (y₁ y₀ : Nat → Nat) (d : Nat) (l : List Nat), (∀ (u : Nat), u ∈ l → y₁ u ≤ y₀ u + d) → (List.map y₁ l).sum ≤ (List.map y₀ l).sum + d * l.length | propext, Quot.sound |
Qpu.CausalInference.length_filter_partition | ∀ {α : Type} (p : α → Bool) (l : List α), (List.filter p l).length + (List.filter (fun a => !p a) l).length = l.length | propext, Quot.sound |
Qpu.CausalInference.mediation_decomposition | ∀ {m : Qpu.CausalInference.Scm}, m.ordered = true → ∀ (u : Nat → Nat) (x med y : Nat), m.totalEffect u x y = m.directEffect u x med y + m.indirectEffect u x med y | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.mem_children | ∀ {g : Qpu.CausalInference.Dag} {c v : Nat}, c ∈ g.children v ↔ (v, c) ∈ g.edges | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.mem_parents | ∀ {g : Qpu.CausalInference.Dag} {p v : Nat}, p ∈ g.parents v ↔ (p, v) ∈ g.edges | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.mem_stratum | ∀ {s : Qpu.CausalInference.Study} {u k : Nat}, u ∈ s.stratum k ↔ u ∈ s.units ∧ s.cov u = k | propext, Quot.sound |
Qpu.CausalInference.no_cycle | ∀ {g : Qpu.CausalInference.Dag}, g.ordered = true → ∀ (a : Nat) (l : List Nat), g.path (a :: (l ++ [a])) = false | propext, Quot.sound |
Qpu.CausalInference.ordered_edge | ∀ {g : Qpu.CausalInference.Dag}, g.ordered = true → ∀ {e : Nat × Nat}, e ∈ g.edges → e.fst < e.snd ∧ e.snd < g.vars | propext, Quot.sound |
Qpu.CausalInference.overlap_match | ∀ (s : Qpu.CausalInference.Study), s.overlap → ∀ {t : Nat}, t ∈ s.treated → ∃ c, c ∈ s.control ∧ s.cov c = s.cov t | propext, Quot.sound |
Qpu.CausalInference.parent_not_descendant | ∀ {g : Qpu.CausalInference.Dag}, g.ordered = true → ∀ {p v : Nat}, p ∈ g.parents v → ∀ (l : List Nat), g.path (v :: (l ++ [p])) = false | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.parents_backdoor | ∀ {g : Qpu.CausalInference.Dag}, g.ordered = true → ∀ (x : Nat), (∀ (p : List Nat), g.backdoorPath x p → Qpu.CausalInference.blocks (g.parents x) p) ∧ ∀ (w : Nat), w ∈ g.parents x → ∀ (l : List Nat), g.path (x :: (l ++ [w])) = false | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.parents_lt | ∀ {g : Qpu.CausalInference.Dag}, g.ordered = true → ∀ {p v : Nat}, p ∈ g.parents v → p < v | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.parents_lt_vars | ∀ {g : Qpu.CausalInference.Dag}, g.ordered = true → ∀ {p v : Nat}, p ∈ g.parents v → p < g.vars | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.path_lt | ∀ {g : Qpu.CausalInference.Dag}, g.ordered = true → ∀ (a : Nat) (l : List Nat), g.path (a :: l) = true → ∀ (b : Nat), b ∈ l → a < b | propext, Quot.sound |
Qpu.CausalInference.positivity | ∀ (s : Qpu.CausalInference.Study), s.overlap → ∀ {u : Nat}, u ∈ s.units → 0 < (s.treatedIn (s.cov u)).length ∧ (s.treatedIn (s.cov u)).length < (s.stratum (s.cov u)).length | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.rd_no_overlap | ∀ (s : Qpu.CausalInference.Study) {c : Nat}, s.sharpRd c → ∀ (k : Nat), ¬(s.treatedIn k ≠ [] ∧ s.controlIn k ≠ []) | propext, Quot.sound |
Qpu.CausalInference.rd_not_overlap | ∀ (s : Qpu.CausalInference.Study) {c : Nat}, s.sharpRd c → s.units ≠ [] → ¬s.overlap | propext, Quot.sound |
Qpu.CausalInference.sum_le_mul_length | ∀ (f : Nat → Nat) (b : Nat) (l : List Nat), (∀ (a : Nat), a ∈ l → f a ≤ b) → (List.map f l).sum ≤ b * l.length | propext, Quot.sound |
Qpu.CausalInference.treated_control_partition | ∀ (s : Qpu.CausalInference.Study), s.treated.length + s.control.length = s.units.length | propext, Quot.sound |
Qpu.CausalInference.triangle_confounded | ∀ (u : Nat → Nat), Qpu.CausalInference.triangle.value (fun x => 1) 2 = 2 ∧ Qpu.CausalInference.triangle.value (fun x => 0) 2 = 0 ∧ (Qpu.CausalInference.triangle.doOp 1 1).value u 2 = (Qpu.CausalInference.triangle.doOp 1 0).value u 2 + 1 | — |
Qpu.CausalInference.triangle_shape | Qpu.CausalInference.triangle.ordered = true ∧ Qpu.CausalInference.triangle.parents 1 = [0] ∧ Qpu.CausalInference.triangle.exogenous 0 | — |
Qpu.CausalInference.valueF_stable | ∀ {m : Qpu.CausalInference.Scm}, m.ordered = true → ∀ (u : Nat → Nat) (f₁ v : Nat), v < f₁ → ∀ (f₂ : Nat), v < f₂ → m.valueF u f₁ v = m.valueF u f₂ v | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.value_eq_valueF | ∀ {m : Qpu.CausalInference.Scm}, m.ordered = true → ∀ (u : Nat → Nat) {f v : Nat}, v < f → m.value u v = m.valueF u f v | propext, Classical.choice, Quot.sound |
Qpu.CausalInference.vars_pos_of_edge | ∀ {g : Qpu.CausalInference.Dag}, g.ordered = true → ∀ {e : Nat × Nat}, e ∈ g.edges → 0 < g.vars | propext, Quot.sound |
Qpu.Federated.avgV_bounded | ∀ {d : Nat} (lo hi : Int) (us : List (Qpu.Federated.Vec d)), 0 < us.length → ∀ (i : Fin d), (∀ (u : Qpu.Federated.Vec d), u ∈ us → lo ≤ u i ∧ u i ≤ hi) → lo ≤ Qpu.Federated.avgV us i ∧ Qpu.Federated.avgV us i ≤ hi | propext, Classical.choice, Quot.sound |
Qpu.Federated.avgV_replicate | ∀ {d : Nat} (k : Nat), 0 < k → ∀ (u : Qpu.Federated.Vec d), Qpu.Federated.avgV (List.replicate k u) = u | propext, Quot.sound |
Qpu.Federated.avgZ_bounded | ∀ (lo hi : Int) (l : List Int), 0 < l.length → (∀ (x : Int), x ∈ l → lo ≤ x ∧ x ≤ hi) → lo ≤ Qpu.Federated.avgZ l ∧ Qpu.Federated.avgZ l ≤ hi | propext, Classical.choice, Quot.sound |
Qpu.Federated.avgZ_replicate | ∀ (k : Nat), 0 < k → ∀ (x : Int), Qpu.Federated.avgZ (List.replicate k x) = x | propext, Quot.sound |
Qpu.Federated.byzantine_lattice | ∀ (l : List Int) (lo hi : Int), l.length = faces → List.countP (Qpu.Federated.outside lo hi) l ≤ hexbit → lo ≤ Qpu.Federated.median l ∧ Qpu.Federated.median l ≤ hi | propext, Quot.sound |
Qpu.Federated.byzantine_median | ∀ (l : List Int) (lo hi : Int) (malicious : Nat), 0 < l.length → List.countP (Qpu.Federated.outside lo hi) l ≤ malicious → 3 * malicious < l.length → lo ≤ Qpu.Federated.median l ∧ Qpu.Federated.median l ≤ hi | propext, Quot.sound |
Qpu.Federated.byzantine_medianV | ∀ {d : Nat} (us : List (Qpu.Federated.Vec d)) (lo hi : Qpu.Federated.Vec d) (malicious : Nat), 0 < us.length → List.countP (fun u => !Qpu.Federated.inBox lo hi u) us ≤ malicious → 3 * malicious < us.length → ∀ (i : Fin d), lo i ≤ Qpu.Federated.medianV us i ∧ Qpu.Federated.medianV us i ≤ hi i | propext, Quot.sound |
Qpu.Federated.byzantine_trimmedMean | ∀ (l : List Int) (lo hi : Int) (malicious : Nat), List.countP (Qpu.Federated.outside lo hi) l ≤ malicious → 3 * malicious < l.length → lo ≤ Qpu.Federated.trimmedMean malicious l ∧ Qpu.Federated.trimmedMean malicious l ≤ hi | propext, Classical.choice, Quot.sound |
Qpu.Federated.clipV_bounded | ∀ {d : Nat} (c : Nat) (u : Qpu.Federated.Vec d) (i : Fin d), -↑c ≤ Qpu.Federated.clipV c u i ∧ Qpu.Federated.clipV c u i ≤ ↑c | propext, Classical.choice, Quot.sound |
Qpu.Federated.clipV_idem | ∀ {d : Nat} (c : Nat) (u : Qpu.Federated.Vec d), Qpu.Federated.clipV c (Qpu.Federated.clipV c u) = Qpu.Federated.clipV c u | propext, Classical.choice, Quot.sound |
Qpu.Federated.clipZ_bounded | ∀ (c : Nat) (x : Int), -↑c ≤ Qpu.Federated.clipZ c x ∧ Qpu.Federated.clipZ c x ≤ ↑c | propext, Classical.choice, Quot.sound |
Qpu.Federated.clipZ_idem | ∀ (c : Nat) (x : Int), Qpu.Federated.clipZ c (Qpu.Federated.clipZ c x) = Qpu.Federated.clipZ c x | propext, Classical.choice, Quot.sound |
Qpu.Federated.clipZ_ne_iff | ∀ (c : Nat) (x : Int), Qpu.Federated.clipZ c x ≠ x ↔ x < -↑c ∨ ↑c < x | propext, Classical.choice, Quot.sound |
Qpu.Federated.clipZ_of_bounded | ∀ (c : Nat) (x : Int), -↑c ≤ x ∧ x ≤ ↑c → Qpu.Federated.clipZ c x = x | propext, Quot.sound |
Qpu.Federated.clipped_avg_bounded | ∀ {d : Nat} (c : Nat) (us : List (Qpu.Federated.Vec d)), 0 < us.length → ∀ (i : Fin d), -↑c ≤ Qpu.Federated.avgV (List.map (Qpu.Federated.clipV c) us) i ∧ Qpu.Federated.avgV (List.map (Qpu.Federated.clipV c) us) i ≤ ↑c | propext, Classical.choice, Quot.sound |
Qpu.Federated.clipped_sum_bounded | ∀ {d : Nat} (c : Nat) (us : List (Qpu.Federated.Vec d)) (i : Fin d), -(↑c * ↑us.length) ≤ Qpu.Federated.sumV (List.map (Qpu.Federated.clipV c) us) i ∧ Qpu.Federated.sumV (List.map (Qpu.Federated.clipV c) us) i ≤ ↑c * ↑us.length | propext, Classical.choice, Quot.sound |
Qpu.Federated.communication_lower_bound | ∀ (rounds clients k : Nat), 0 < k → rounds * clients ≤ Qpu.Federated.totalMessages rounds clients k | propext |
Qpu.Federated.countP_gt_le_outside | ∀ (l : List Int) (lo hi : Int), List.countP (fun x => decide (hi < x)) l ≤ List.countP (Qpu.Federated.outside lo hi) l | propext |
Qpu.Federated.countP_lt_le_outside | ∀ (l : List Int) (lo hi : Int), List.countP (fun x => decide (x < lo)) l ≤ List.countP (Qpu.Federated.outside lo hi) l | propext |
Qpu.Federated.dropout_sum_bounded | ∀ {d : Nat} (c : Nat) (us active : List (Qpu.Federated.Vec d)), active.Sublist us → ∀ (i : Fin d), -(↑c * ↑us.length) ≤ Qpu.Federated.sumV (List.map (Qpu.Federated.clipV c) active) i ∧ Qpu.Federated.sumV (List.map (Qpu.Federated.clipV c) active) i ≤ ↑c * ↑us.length | propext, Classical.choice, Quot.sound |
Qpu.Federated.halve_le | ∀ (r L : Nat), Qpu.Federated.halve r L ≤ L | propext |
Qpu.Federated.halving_converges | ∀ (r L : Nat), L < mintOf r → Qpu.Federated.halve r L = 0 | propext, Quot.sound |
Qpu.Federated.heterogeneity_bounded | ∀ {d : Nat} (c : Nat) (us : List (Qpu.Federated.Vec d)), 0 < us.length → ∀ (u : Qpu.Federated.Vec d) (i : Fin d), -(2 * ↑c) ≤ Qpu.Federated.clipV c u i - Qpu.Federated.avgV (List.map (Qpu.Federated.clipV c) us) i ∧ Qpu.Federated.clipV c u i - Qpu.Federated.avgV (List.map (Qpu.Federated.clipV c) us) i ≤ 2 * ↑c | propext, Classical.choice, Quot.sound |
Qpu.Federated.lattice_instance | 3 * hexbit < faces | — |
Qpu.Federated.lt_mintOf_self | ∀ (L : Nat), L < mintOf L | propext, Quot.sound |
Qpu.Federated.median_bounded | ∀ (l : List Int) (lo hi : Int) (f : Nat), 0 < l.length → List.countP (fun x => decide (x < lo)) l ≤ f → List.countP (fun x => decide (hi < x)) l ≤ f → 2 * f < l.length → lo ≤ Qpu.Federated.median l ∧ Qpu.Federated.median l ≤ hi | propext, Quot.sound |
Qpu.Federated.median_eq_getElem | ∀ (l : List Int) (hpos : 0 < l.length), Qpu.Federated.median l = (Qpu.Federated.sortZ l)[l.length / 2] | propext, Quot.sound |
Qpu.Federated.mem_map_clipV_bounded | ∀ {d : Nat} (c : Nat) (us : List (Qpu.Federated.Vec d)) (i : Fin d) (x : Int), x ∈ Qpu.Federated.coord i (List.map (Qpu.Federated.clipV c) us) → -↑c ≤ x ∧ x ≤ ↑c | propext, Classical.choice, Quot.sound |
Qpu.Federated.noised_clipped_bounded | ∀ {d : Nat} (c b : Nat) (us : List (Qpu.Federated.Vec d)) (i : Fin d) (e : Int), -↑b ≤ e ∧ e ≤ ↑b → -(↑c * ↑us.length + ↑b) ≤ Qpu.Federated.sumV (List.map (Qpu.Federated.clipV c) us) i + e ∧ Qpu.Federated.sumV (List.map (Qpu.Federated.clipV c) us) i + e ≤ ↑c * ↑us.length + ↑b | propext, Classical.choice, Quot.sound |
Qpu.Federated.noised_privacy | ∀ (a a' : Int) (b : Nat), -↑b ≤ a - a' ∧ a - a' ≤ ↑b → ∃ e e', (-↑b ≤ e ∧ e ≤ ↑b) ∧ (-↑b ≤ e' ∧ e' ≤ ↑b) ∧ a + e = a' + e' | propext, Classical.choice, Quot.sound |
Qpu.Federated.noised_utility | ∀ (a e : Int) (b : Nat), -↑b ≤ e ∧ e ≤ ↑b → -↑b ≤ a + e - a ∧ a + e - a ≤ ↑b | propext, Classical.choice, Quot.sound |
Qpu.Federated.pairwise_mask_cancels | ∀ {d : Nat} (u v m : Qpu.Federated.Vec d), Qpu.Federated.addV (Qpu.Federated.addV u m) (Qpu.Federated.subV v m) = Qpu.Federated.addV u v | propext, Quot.sound |
Qpu.Federated.privacy_utility_tradeoff | ∀ (a a' e e' : Int) (b : Nat), -↑b ≤ e ∧ e ≤ ↑b → -↑b ≤ e' ∧ e' ≤ ↑b → a + e = a' + e' → -(2 * ↑b) ≤ a - a' ∧ a - a' ≤ 2 * ↑b | propext, Classical.choice, Quot.sound |
Qpu.Federated.quantization_error | ∀ (q : Nat), 0 < q → ∀ (x : Int), 0 ≤ x - Qpu.Federated.dequantize q (Qpu.Federated.quantize q x) ∧ x - Qpu.Federated.dequantize q (Qpu.Federated.quantize q x) < ↑q | propext, Classical.choice, Quot.sound |
Qpu.Federated.quantize_clipped_bounded | ∀ (q c : Nat), 0 < q → ∀ (x : Int), -↑c / ↑q ≤ Qpu.Federated.quantize q (Qpu.Federated.clipZ c x) ∧ Qpu.Federated.quantize q (Qpu.Federated.clipZ c x) ≤ ↑c / ↑q | propext, Classical.choice, Quot.sound |
Qpu.Federated.rounds_suffice | ∀ (L : Nat), Qpu.Federated.halve L L = 0 | propext, Quot.sound |
Qpu.Federated.secureAggregate_eq | ∀ {d : Nat} (cs : List (Qpu.Federated.Vec d × List (Qpu.Federated.Vec d))), Qpu.Federated.secureAggregate cs = Qpu.Federated.sumV (List.map Prod.fst cs) | propext, Quot.sound |
Qpu.Federated.shares_consistent | ∀ {d : Nat} (s s' m : Qpu.Federated.Vec d) (ms : List (Qpu.Federated.Vec d)), ∃ m', (Qpu.Federated.shares s' (m' :: ms)).head? = (Qpu.Federated.shares s (m :: ms)).head? ∧ (Qpu.Federated.shares s' (m' :: ms)).tail.tail = (Qpu.Federated.shares s (m :: ms)).tail.tail | propext, Quot.sound |
Qpu.Federated.shares_length | ∀ {d : Nat} (s : Qpu.Federated.Vec d) (ms : List (Qpu.Federated.Vec d)), (Qpu.Federated.shares s ms).length = ms.length + 1 | — |
Qpu.Federated.shares_tail_independent | ∀ {d : Nat} (s s' : Qpu.Federated.Vec d) (ms : List (Qpu.Federated.Vec d)), (Qpu.Federated.shares s ms).tail = (Qpu.Federated.shares s' ms).tail | — |
Qpu.Federated.shares_traffic | ∀ {d : Nat} (k : Nat) (cs : List (Qpu.Federated.Vec d × List (Qpu.Federated.Vec d))), (∀ (c : Qpu.Federated.Vec d × List (Qpu.Federated.Vec d)), c ∈ cs → c.snd.length + 1 = k) → (List.flatMap (fun c => Qpu.Federated.shares c.fst c.snd) cs).length = cs.length * k | propext, Quot.sound |
Qpu.Federated.sortZ_length | ∀ (l : List Int), (Qpu.Federated.sortZ l).length = l.length | propext, Quot.sound |
Qpu.Federated.sortZ_perm | ∀ (l : List Int), (Qpu.Federated.sortZ l).Perm l | propext, Quot.sound |
Qpu.Federated.sortZ_sorted | ∀ (l : List Int), List.Pairwise (fun x1 x2 => x1 ≤ x2) (Qpu.Federated.sortZ l) | propext, Quot.sound |
Qpu.Federated.sorted_lower | ∀ {s : List Int}, List.Pairwise (fun x1 x2 => x1 ≤ x2) s → ∀ (lo : Int) {k : Nat} (hk : k < s.length), List.countP (fun x => decide (x < lo)) s ≤ k → lo ≤ s[k] | propext, Quot.sound |
Qpu.Federated.sorted_upper | ∀ {s : List Int}, List.Pairwise (fun x1 x2 => x1 ≤ x2) s → ∀ (hi : Int) {k : Nat} (hk : k < s.length), List.countP (fun x => decide (hi < x)) s ≤ s.length - 1 - k → s[k] ≤ hi | propext, Quot.sound |
Qpu.Federated.sumV_append | ∀ {d : Nat} (us vs : List (Qpu.Federated.Vec d)), Qpu.Federated.sumV (us ++ vs) = Qpu.Federated.addV (Qpu.Federated.sumV us) (Qpu.Federated.sumV vs) | propext, Quot.sound |
Qpu.Federated.sumV_cons | ∀ {d : Nat} (u : Qpu.Federated.Vec d) (us : List (Qpu.Federated.Vec d)), Qpu.Federated.sumV (u :: us) = Qpu.Federated.addV u (Qpu.Federated.sumV us) | — |
Qpu.Federated.sumV_nil | ∀ {d : Nat}, Qpu.Federated.sumV [] = Qpu.Federated.zeroV | — |
Qpu.Federated.sumV_perm | ∀ {d : Nat} {us vs : List (Qpu.Federated.Vec d)}, us.Perm vs → Qpu.Federated.sumV us = Qpu.Federated.sumV vs | propext, Quot.sound |
Qpu.Federated.sumV_shares | ∀ {d : Nat} (s : Qpu.Federated.Vec d) (ms : List (Qpu.Federated.Vec d)), Qpu.Federated.sumV (Qpu.Federated.shares s ms) = s | propext, Quot.sound |
Qpu.Federated.sumZ_append | ∀ (a b : List Int), Qpu.Federated.sumZ (a ++ b) = Qpu.Federated.sumZ a + Qpu.Federated.sumZ b | propext |
Qpu.Federated.sumZ_bounded | ∀ (lo hi : Int) (l : List Int), (∀ (x : Int), x ∈ l → lo ≤ x ∧ x ≤ hi) → lo * ↑l.length ≤ Qpu.Federated.sumZ l ∧ Qpu.Federated.sumZ l ≤ hi * ↑l.length | propext, Classical.choice, Quot.sound |
Qpu.Federated.sumZ_cons | ∀ (x : Int) (xs : List Int), Qpu.Federated.sumZ (x :: xs) = x + Qpu.Federated.sumZ xs | — |
Qpu.Federated.sumZ_nil | Qpu.Federated.sumZ [] = 0 | — |
Qpu.Federated.sumZ_perm | ∀ {a b : List Int}, a.Perm b → Qpu.Federated.sumZ a = Qpu.Federated.sumZ b | propext, Quot.sound |
Qpu.Federated.sumZ_replicate | ∀ (k : Nat) (x : Int), Qpu.Federated.sumZ (List.replicate k x) = x * ↑k | propext, Quot.sound |
Qpu.Federated.trimmedMean_bounded | ∀ (l : List Int) (lo hi : Int) (f : Nat), List.countP (fun x => decide (x < lo)) l ≤ f → List.countP (fun x => decide (hi < x)) l ≤ f → 2 * f < l.length → lo ≤ Qpu.Federated.trimmedMean f l ∧ Qpu.Federated.trimmedMean f l ≤ hi | propext, Classical.choice, Quot.sound |
Qpu.Federated.trimmed_length | ∀ (f : Nat) (l : List Int), 2 * f ≤ l.length → (Qpu.Federated.trimmed f l).length = l.length - 2 * f | propext, Quot.sound |
Qpu.Federated.trimmed_mem_bounded | ∀ (l : List Int) (lo hi : Int) (f : Nat), List.countP (fun x => decide (x < lo)) l ≤ f → List.countP (fun x => decide (hi < x)) l ≤ f → 2 * f < l.length → ∀ (x : Int), x ∈ Qpu.Federated.trimmed f l → lo ≤ x ∧ x ≤ hi | propext, Quot.sound |
Qpu.Harmonic.L1_range | ∀ (t : Nat), 1 ≤ Qpu.Harmonic.L1 t ∧ Qpu.Harmonic.L1 t ≤ 60 | propext, Classical.choice, Quot.sound |
Qpu.Harmonic.L2_range | ∀ (t : Nat), 1 ≤ Qpu.Harmonic.L2 t ∧ Qpu.Harmonic.L2 t ≤ 30 | propext, Classical.choice, Quot.sound |
Qpu.Harmonic.closing_count | (List.filter (fun t => Qpu.Harmonic.Involute t == 100) (List.range 107)).length = 18 | — |
Qpu.Harmonic.closing_set | List.filter (fun t => Qpu.Harmonic.Involute t == 100) (List.range 107) = [23, 24, 25, 26, 27, 28, 53, 54, 55, 56, 57, 58, 83, 84, 85, 86, 87, 88] | — |
Qpu.Harmonic.involute_eq_100_iff | ∀ (t : Nat), Qpu.Harmonic.Involute t = 100 ↔ 23 ≤ t % 60 ∧ t % 60 ≤ 28 ∨ 53 ≤ t % 60 ∧ t % 60 ≤ 58 | propext, Classical.choice, Quot.sound |
Qpu.Harmonic.involute_values | ∀ (t : Nat), Qpu.Harmonic.Involute t = 100 ∨ Qpu.Harmonic.Involute t = 0 | propext, Quot.sound |
Qpu.ProgramSynthesis.cegis_eliminates | ∀ {e : Qpu.ProgramSynthesis.Expr} {ex : Qpu.ProgramSynthesis.Example} {c : List Qpu.ProgramSynthesis.Expr}, Qpu.ProgramSynthesis.eval e ex.fst ≠ ex.snd → ¬e ∈ Qpu.ProgramSynthesis.prune ex c | propext, Quot.sound |
Qpu.ProgramSynthesis.checkLower_complete | ∀ {e : Qpu.ProgramSynthesis.Expr} {bound : Nat}, (∀ (x : Nat), bound ≤ Qpu.ProgramSynthesis.eval e x) → Qpu.ProgramSynthesis.checkLower e bound = true | propext |
Qpu.ProgramSynthesis.checkLower_sound | ∀ {e : Qpu.ProgramSynthesis.Expr} {bound : Nat}, Qpu.ProgramSynthesis.checkLower e bound = true → ∀ (x : Nat), bound ≤ Qpu.ProgramSynthesis.eval e x | propext |
Qpu.ProgramSynthesis.complete_complete | ∀ {k : Nat} {sk : Qpu.ProgramSynthesis.Sketch} {s : Qpu.ProgramSynthesis.Spec} {w : Qpu.ProgramSynthesis.Expr}, Qpu.ProgramSynthesis.satisfies (Qpu.ProgramSynthesis.fill sk w) s → Qpu.ProgramSynthesis.size w ≤ k → ∃ e, Qpu.ProgramSynthesis.complete k sk s = some e | propext, Quot.sound |
Qpu.ProgramSynthesis.complete_hole | ∀ (k : Nat) (s : Qpu.ProgramSynthesis.Spec), Qpu.ProgramSynthesis.complete k Qpu.ProgramSynthesis.Sketch.hole s = Qpu.ProgramSynthesis.synth k s | — |
Qpu.ProgramSynthesis.complete_sound | ∀ {k : Nat} {sk : Qpu.ProgramSynthesis.Sketch} {s : Qpu.ProgramSynthesis.Spec} {e : Qpu.ProgramSynthesis.Expr}, Qpu.ProgramSynthesis.complete k sk s = some e → Qpu.ProgramSynthesis.satisfies (Qpu.ProgramSynthesis.fill sk e) s | propext, Quot.sound |
Qpu.ProgramSynthesis.counterexample_of_not_satisfies | ∀ {e : Qpu.ProgramSynthesis.Expr} {s : Qpu.ProgramSynthesis.Spec}, ¬Qpu.ProgramSynthesis.satisfies e s → ∃ ex, ex ∈ s ∧ Qpu.ProgramSynthesis.eval e ex.fst ≠ ex.snd | propext, Classical.choice, Quot.sound |
Qpu.ProgramSynthesis.double_equiv | Qpu.ProgramSynthesis.Equiv (Qpu.ProgramSynthesis.Expr.var.add Qpu.ProgramSynthesis.Expr.var) ((Qpu.ProgramSynthesis.Expr.lit 2).mul Qpu.ProgramSynthesis.Expr.var) | propext, Quot.sound |
Qpu.ProgramSynthesis.double_propagate | Qpu.ProgramSynthesis.propagate Qpu.ProgramSynthesis.doubleSpec (Qpu.ProgramSynthesis.upTo 3) = [Qpu.ProgramSynthesis.Expr.var.add Qpu.ProgramSynthesis.Expr.var] | — |
Qpu.ProgramSynthesis.double_synth | Qpu.ProgramSynthesis.synth 3 Qpu.ProgramSynthesis.doubleSpec = some (Qpu.ProgramSynthesis.Expr.var.add Qpu.ProgramSynthesis.Expr.var) ∧ Qpu.ProgramSynthesis.size (Qpu.ProgramSynthesis.Expr.var.add Qpu.ProgramSynthesis.Expr.var) ≤ Qpu.ProgramSynthesis.size ((Qpu.ProgramSynthesis.Expr.lit 2).mul Qpu.ProgramSynthesis.Expr.var) | propext, Quot.sound |
Qpu.ProgramSynthesis.equiv_satisfies_traceOf | ∀ {e₁ e₂ : Qpu.ProgramSynthesis.Expr}, Qpu.ProgramSynthesis.Equiv e₁ e₂ → ∀ (inputs : List Nat), Qpu.ProgramSynthesis.satisfies e₂ (Qpu.ProgramSynthesis.traceOf e₁ inputs) | propext, Quot.sound |
Qpu.ProgramSynthesis.eval_affine | ∀ (a b x : Nat), Qpu.ProgramSynthesis.eval (Qpu.ProgramSynthesis.affine a b) x = a * x + b | — |
Qpu.ProgramSynthesis.eval_mono | ∀ (e : Qpu.ProgramSynthesis.Expr) {x y : Nat}, x ≤ y → Qpu.ProgramSynthesis.eval e x ≤ Qpu.ProgramSynthesis.eval e y | — |
Qpu.ProgramSynthesis.eval_replace | ∀ (e : Qpu.ProgramSynthesis.Expr) (p : Qpu.ProgramSynthesis.Pos) {old new : Qpu.ProgramSynthesis.Expr}, Qpu.ProgramSynthesis.get? e p = some old → ∀ {x : Nat}, Qpu.ProgramSynthesis.eval new x = Qpu.ProgramSynthesis.eval old x → Qpu.ProgramSynthesis.eval (Qpu.ProgramSynthesis.replace e p new) x = Qpu.ProgramSynthesis.eval e x | propext |
Qpu.ProgramSynthesis.eval_zero | ∀ (e : Qpu.ProgramSynthesis.Expr), Qpu.ProgramSynthesis.eval e 0 = Qpu.ProgramSynthesis.lower e | propext |
Qpu.ProgramSynthesis.fill_of_holes_zero | ∀ (sk : Qpu.ProgramSynthesis.Sketch), Qpu.ProgramSynthesis.holes sk = 0 → ∀ (e e' : Qpu.ProgramSynthesis.Expr), Qpu.ProgramSynthesis.fill sk e = Qpu.ProgramSynthesis.fill sk e' | propext, Quot.sound |
Qpu.ProgramSynthesis.holds_iff | ∀ (e : Qpu.ProgramSynthesis.Expr) (ex : Qpu.ProgramSynthesis.Example), Qpu.ProgramSynthesis.holds e ex = true ↔ Qpu.ProgramSynthesis.eval e ex.fst = ex.snd | propext, Quot.sound |
Qpu.ProgramSynthesis.inconsistent_spec | ∀ (e : Qpu.ProgramSynthesis.Expr), ¬Qpu.ProgramSynthesis.satisfies e [(0, 0), (0, 1)] | propext |
Qpu.ProgramSynthesis.lower_le_eval | ∀ (e : Qpu.ProgramSynthesis.Expr) (x : Nat), Qpu.ProgramSynthesis.lower e ≤ Qpu.ProgramSynthesis.eval e x | propext |
Qpu.ProgramSynthesis.mem_propagate | ∀ {s : Qpu.ProgramSynthesis.Spec} {c : List Qpu.ProgramSynthesis.Expr} {e : Qpu.ProgramSynthesis.Expr}, e ∈ Qpu.ProgramSynthesis.propagate s c ↔ e ∈ c ∧ Qpu.ProgramSynthesis.satisfies e s | propext, Quot.sound |
Qpu.ProgramSynthesis.mem_prune | ∀ {ex : Qpu.ProgramSynthesis.Example} {c : List Qpu.ProgramSynthesis.Expr} {e : Qpu.ProgramSynthesis.Expr}, e ∈ Qpu.ProgramSynthesis.prune ex c ↔ e ∈ c ∧ Qpu.ProgramSynthesis.eval e ex.fst = ex.snd | propext, Quot.sound |
Qpu.ProgramSynthesis.mem_upTo_of_size_le | ∀ {k : Nat} (e : Qpu.ProgramSynthesis.Expr), Qpu.ProgramSynthesis.size e ≤ k → e ∈ Qpu.ProgramSynthesis.upTo k | propext, Quot.sound |
Qpu.ProgramSynthesis.programs_unbounded | ∀ (k : Nat), ∃ e, k < Qpu.ProgramSynthesis.size e | — |
Qpu.ProgramSynthesis.propagate_append_subset | ∀ {s t : Qpu.ProgramSynthesis.Spec} {c : List Qpu.ProgramSynthesis.Expr} {e : Qpu.ProgramSynthesis.Expr}, e ∈ Qpu.ProgramSynthesis.propagate (s ++ t) c → e ∈ Qpu.ProgramSynthesis.propagate s c | propext, Quot.sound |
Qpu.ProgramSynthesis.propagate_length_le | ∀ (s : Qpu.ProgramSynthesis.Spec) (c : List Qpu.ProgramSynthesis.Expr), (Qpu.ProgramSynthesis.propagate s c).length ≤ c.length | propext |
Qpu.ProgramSynthesis.propagate_nil_iff | ∀ (k : Nat) (s : Qpu.ProgramSynthesis.Spec), Qpu.ProgramSynthesis.propagate s (Qpu.ProgramSynthesis.upTo k) = [] ↔ Qpu.ProgramSynthesis.synth k s = none | propext, Classical.choice, Quot.sound |
Qpu.ProgramSynthesis.prune_keeps | ∀ {ex : Qpu.ProgramSynthesis.Example} {s : Qpu.ProgramSynthesis.Spec} {c : List Qpu.ProgramSynthesis.Expr} {e : Qpu.ProgramSynthesis.Expr}, Qpu.ProgramSynthesis.satisfies e s → ex ∈ s → e ∈ c → e ∈ Qpu.ProgramSynthesis.prune ex c | propext, Quot.sound |
Qpu.ProgramSynthesis.prune_length_le | ∀ (ex : Qpu.ProgramSynthesis.Example) (c : List Qpu.ProgramSynthesis.Expr), (Qpu.ProgramSynthesis.prune ex c).length ≤ c.length | propext |
Qpu.ProgramSynthesis.repair_preserves | ∀ {e : Qpu.ProgramSynthesis.Expr} {p : Qpu.ProgramSynthesis.Pos} {old new : Qpu.ProgramSynthesis.Expr}, Qpu.ProgramSynthesis.get? e p = some old → ∀ {ex : Qpu.ProgramSynthesis.Example}, Qpu.ProgramSynthesis.eval e ex.fst = ex.snd → Qpu.ProgramSynthesis.eval new ex.fst = Qpu.ProgramSynthesis.eval old ex.fst → Qpu.ProgramSynthesis.eval (Qpu.ProgramSynthesis.replace e p new) ex.fst = ex.snd | propext |
Qpu.ProgramSynthesis.repair_preserves_spec | ∀ {e : Qpu.ProgramSynthesis.Expr} {p : Qpu.ProgramSynthesis.Pos} {old new : Qpu.ProgramSynthesis.Expr} {s : Qpu.ProgramSynthesis.Spec}, Qpu.ProgramSynthesis.get? e p = some old → Qpu.ProgramSynthesis.satisfies e s → (∀ (ex : Qpu.ProgramSynthesis.Example), ex ∈ s → Qpu.ProgramSynthesis.eval new ex.fst = Qpu.ProgramSynthesis.eval old ex.fst) → Qpu.ProgramSynthesis.satisfies (Qpu.ProgramSynthesis.replace e p new) s | propext |
Qpu.ProgramSynthesis.repair_root | ∀ (e : Qpu.ProgramSynthesis.Expr) (ex : Qpu.ProgramSynthesis.Example), Qpu.ProgramSynthesis.eval (Qpu.ProgramSynthesis.replace e Qpu.ProgramSynthesis.Pos.here (Qpu.ProgramSynthesis.Expr.lit ex.snd)) ex.fst = ex.snd | propext |
Qpu.ProgramSynthesis.satisfiable_iff | ∀ (k : Nat) (s : Qpu.ProgramSynthesis.Spec), Qpu.ProgramSynthesis.satisfiable k s = true ↔ ∃ e, Qpu.ProgramSynthesis.size e ≤ k ∧ Qpu.ProgramSynthesis.satisfies e s | propext, Quot.sound |
Qpu.ProgramSynthesis.satisfiable_monotone | ∀ {e : Qpu.ProgramSynthesis.Expr} {s : Qpu.ProgramSynthesis.Spec}, Qpu.ProgramSynthesis.satisfies e s → ∀ {x y x' y' : Nat}, (x, y) ∈ s → (x', y') ∈ s → x ≤ x' → y ≤ y' | — |
Qpu.ProgramSynthesis.satisfiesB_iff | ∀ (e : Qpu.ProgramSynthesis.Expr) (s : Qpu.ProgramSynthesis.Spec), Qpu.ProgramSynthesis.satisfiesB e s = true ↔ Qpu.ProgramSynthesis.satisfies e s | propext, Quot.sound |
Qpu.ProgramSynthesis.satisfies_append | ∀ {e : Qpu.ProgramSynthesis.Expr} (s t : Qpu.ProgramSynthesis.Spec), Qpu.ProgramSynthesis.satisfies e (s ++ t) ↔ Qpu.ProgramSynthesis.satisfies e s ∧ Qpu.ProgramSynthesis.satisfies e t | propext, Quot.sound |
Qpu.ProgramSynthesis.satisfies_of_equiv | ∀ {e₁ e₂ : Qpu.ProgramSynthesis.Expr} {s : Qpu.ProgramSynthesis.Spec}, Qpu.ProgramSynthesis.Equiv e₁ e₂ → (Qpu.ProgramSynthesis.satisfies e₁ s ↔ Qpu.ProgramSynthesis.satisfies e₂ s) | — |
Qpu.ProgramSynthesis.satisfies_traceOf | ∀ (e : Qpu.ProgramSynthesis.Expr) (inputs : List Nat), Qpu.ProgramSynthesis.satisfies e (Qpu.ProgramSynthesis.traceOf e inputs) | propext, Quot.sound |
Qpu.ProgramSynthesis.singleton_satisfiable | ∀ (ex : Qpu.ProgramSynthesis.Example), Qpu.ProgramSynthesis.satisfies (Qpu.ProgramSynthesis.Expr.lit ex.snd) [ex] | propext |
Qpu.ProgramSynthesis.size_affine | ∀ (a b : Nat), Qpu.ProgramSynthesis.size (Qpu.ProgramSynthesis.affine a b) = a + b + 5 | propext, Quot.sound |
Qpu.ProgramSynthesis.size_compose | ∀ (a b : Qpu.ProgramSynthesis.Expr), Qpu.ProgramSynthesis.size (a.add b) = Qpu.ProgramSynthesis.size a + Qpu.ProgramSynthesis.size b + 1 ∧ Qpu.ProgramSynthesis.size (a.mul b) = Qpu.ProgramSynthesis.size a + Qpu.ProgramSynthesis.size b + 1 | — |
Qpu.ProgramSynthesis.size_fill | ∀ (sk : Qpu.ProgramSynthesis.Sketch) (e : Qpu.ProgramSynthesis.Expr), Qpu.ProgramSynthesis.size (Qpu.ProgramSynthesis.fill sk e) = Qpu.ProgramSynthesis.skeleton sk + Qpu.ProgramSynthesis.holes sk * Qpu.ProgramSynthesis.size e | propext, Quot.sound |
Qpu.ProgramSynthesis.size_le_of_mem_upTo | ∀ {k : Nat} {e : Qpu.ProgramSynthesis.Expr}, e ∈ Qpu.ProgramSynthesis.upTo k → Qpu.ProgramSynthesis.size e ≤ k | propext, Quot.sound |
Qpu.ProgramSynthesis.size_of_mem_layer | ∀ {k : Nat} {prev : List Qpu.ProgramSynthesis.Expr} {e : Qpu.ProgramSynthesis.Expr}, e ∈ Qpu.ProgramSynthesis.layer k prev → Qpu.ProgramSynthesis.size e = k + 1 | propext, Quot.sound |
Qpu.ProgramSynthesis.size_pos | ∀ (e : Qpu.ProgramSynthesis.Expr), 0 < Qpu.ProgramSynthesis.size e | propext |
Qpu.ProgramSynthesis.size_replace | ∀ (e : Qpu.ProgramSynthesis.Expr) (p : Qpu.ProgramSynthesis.Pos) {old new : Qpu.ProgramSynthesis.Expr}, Qpu.ProgramSynthesis.get? e p = some old → Qpu.ProgramSynthesis.size (Qpu.ProgramSynthesis.replace e p new) + Qpu.ProgramSynthesis.size old = Qpu.ProgramSynthesis.size e + Qpu.ProgramSynthesis.size new | propext, Quot.sound |
Qpu.ProgramSynthesis.sketch_completion_size | ∀ (sk : Qpu.ProgramSynthesis.Sketch), Qpu.ProgramSynthesis.size (Qpu.ProgramSynthesis.fill sk Qpu.ProgramSynthesis.Expr.var) = Qpu.ProgramSynthesis.skeleton sk + Qpu.ProgramSynthesis.holes sk | propext, Quot.sound |
Qpu.ProgramSynthesis.succ_synth | Qpu.ProgramSynthesis.synth 4 Qpu.ProgramSynthesis.succSpec = some (Qpu.ProgramSynthesis.Expr.var.add (Qpu.ProgramSynthesis.Expr.lit 1)) ∧ Qpu.ProgramSynthesis.synth 3 Qpu.ProgramSynthesis.succSpec = none | — |
Qpu.ProgramSynthesis.synth_complete | ∀ {k : Nat} {s : Qpu.ProgramSynthesis.Spec} {w : Qpu.ProgramSynthesis.Expr}, Qpu.ProgramSynthesis.satisfies w s → Qpu.ProgramSynthesis.size w ≤ k → ∃ e, Qpu.ProgramSynthesis.synth k s = some e | propext, Quot.sound |
Qpu.ProgramSynthesis.synth_mem_propagate | ∀ {k : Nat} {s : Qpu.ProgramSynthesis.Spec} {e : Qpu.ProgramSynthesis.Expr}, Qpu.ProgramSynthesis.synth k s = some e → e ∈ Qpu.ProgramSynthesis.propagate s (Qpu.ProgramSynthesis.upTo k) | propext, Quot.sound |
Qpu.ProgramSynthesis.synth_minimal | ∀ {s : Qpu.ProgramSynthesis.Spec} {k : Nat} {e : Qpu.ProgramSynthesis.Expr}, Qpu.ProgramSynthesis.synth k s = some e → ∀ (w : Qpu.ProgramSynthesis.Expr), Qpu.ProgramSynthesis.satisfies w s → Qpu.ProgramSynthesis.size e ≤ Qpu.ProgramSynthesis.size w | propext, Quot.sound |
Qpu.ProgramSynthesis.synth_size | ∀ {k : Nat} {s : Qpu.ProgramSynthesis.Spec} {e : Qpu.ProgramSynthesis.Expr}, Qpu.ProgramSynthesis.synth k s = some e → Qpu.ProgramSynthesis.size e ≤ k | propext, Quot.sound |
Qpu.ProgramSynthesis.synth_sound | ∀ {k : Nat} {s : Qpu.ProgramSynthesis.Spec} {e : Qpu.ProgramSynthesis.Expr}, Qpu.ProgramSynthesis.synth k s = some e → Qpu.ProgramSynthesis.satisfies e s | propext, Quot.sound |
Qpu.ProgramSynthesis.synth_traceOf | ∀ (e : Qpu.ProgramSynthesis.Expr) (inputs : List Nat), ∃ e', Qpu.ProgramSynthesis.synth (Qpu.ProgramSynthesis.size e) (Qpu.ProgramSynthesis.traceOf e inputs) = some e' ∧ Qpu.ProgramSynthesis.size e' ≤ Qpu.ProgramSynthesis.size e | propext, Quot.sound |
Qpu.ProgramSynthesis.synth_typed | ∀ {k : Nat} {s : Qpu.ProgramSynthesis.Spec} {e : Qpu.ProgramSynthesis.Expr}, Qpu.ProgramSynthesis.synth k s = some e → Qpu.ProgramSynthesis.satisfies e s ∧ Qpu.ProgramSynthesis.size e ≤ k ∧ ∀ (x y : Nat), x ≤ y → Qpu.ProgramSynthesis.eval e x ≤ Qpu.ProgramSynthesis.eval e y | propext, Quot.sound |
Qpu.ProgramSynthesis.testing_incomplete | Qpu.ProgramSynthesis.satisfies (Qpu.ProgramSynthesis.Expr.var.mul Qpu.ProgramSynthesis.Expr.var) [(0, 0), (2, 4)] ∧ Qpu.ProgramSynthesis.satisfies (Qpu.ProgramSynthesis.Expr.var.add Qpu.ProgramSynthesis.Expr.var) [(0, 0), (2, 4)] ∧ ¬Qpu.ProgramSynthesis.Equiv (Qpu.ProgramSynthesis.Expr.var.mul Qpu.ProgramSynthesis.Expr.var) (Qpu.ProgramSynthesis.Expr.var.add Qpu.ProgramSynthesis.Expr.var) | propext, Quot.sound |
Qpu.ProgramSynthesis.unsatisfiable_spec | ∀ (e : Qpu.ProgramSynthesis.Expr), ¬Qpu.ProgramSynthesis.satisfies e [(0, 1), (1, 0)] | propext |
Qpu.ProgramSynthesis.upTo_counts | (Qpu.ProgramSynthesis.upTo 1).length = 2 ∧ (Qpu.ProgramSynthesis.upTo 2).length = 3 ∧ (Qpu.ProgramSynthesis.upTo 3).length = 12 ∧ (Qpu.ProgramSynthesis.upTo 4).length = 21 | — |
Qpu.Xai.Attention.sums | ∀ {total : Nat} (self : Qpu.Xai.Attention total), self.weights.sum = total | — |
Qpu.Xai.ablation_complete | ∀ (f : List Int → Int) (x b : List Int), x.length = b.length → (Qpu.Xai.ablation f x b).sum = f x - f b | propext, Quot.sound |
Qpu.Xai.attention_rollout_normalised | ∀ {T : Nat} (A : Qpu.Xai.Attention T) (B : List (Qpu.Xai.Attention T)), A.weights.length ≤ B.length → (Qpu.Xai.rollout A.weights (List.map Qpu.Xai.Attention.weights B)).sum = T * T | propext, Quot.sound |
Qpu.Xai.attention_weight_le_total | ∀ {T : Nat} (A : Qpu.Xai.Attention T) (w : Nat), w ∈ A.weights → w ≤ T | propext, Quot.sound |
Qpu.Xai.attr_complete | ∀ (m : Qpu.Xai.Linear) (x b : List Int), x.length = b.length → (Qpu.Xai.attr m.weights x b).sum = m.eval x - m.eval b | propext, Classical.choice, Quot.sound |
Qpu.Xai.attr_sum | ∀ (w x b : List Int), x.length = b.length → (Qpu.Xai.attr w x b).sum = Qpu.Xai.dot w x - Qpu.Xai.dot w b | propext, Classical.choice, Quot.sound |
Qpu.Xai.cam_total | ∀ (w : List Nat) (maps : List (List Nat)) (T : Nat), (∀ (f : List Nat), f ∈ maps → f.sum = T) → w.length ≤ maps.length → (Qpu.Xai.rollout w maps).sum = w.sum * T | propext, Quot.sound |
Qpu.Xai.counterfactual_exists | ∀ (m : Qpu.Xai.Linear) (x : List Int) (i : Nat), i < x.length → m.weights.getD i 0 ≠ 0 → ∃ y, Qpu.Xai.hamming x y ≤ 1 ∧ m.eval y ≠ m.eval x | propext, Quot.sound |
Qpu.Xai.dot_mono | ∀ (w x y : List Int), (∀ (a : Int), a ∈ w → 0 ≤ a) → Qpu.Xai.Le x y → Qpu.Xai.dot w x ≤ Qpu.Xai.dot w y | propext |
Qpu.Xai.dot_set_sub_set | ∀ (w l : List Int) (i : Nat) (u v : Int), i < l.length → Qpu.Xai.dot w (l.set i v) - Qpu.Xai.dot w (l.set i u) = w.getD i 0 * (v - u) | propext, Quot.sound |
Qpu.Xai.dot_sub_set | ∀ (w l : List Int) (i : Nat) (v : Int), i < l.length → Qpu.Xai.dot w l - Qpu.Xai.dot w (l.set i v) = w.getD i 0 * (l.getD i 0 - v) | propext, Quot.sound |
Qpu.Xai.eval_mono | ∀ (m : Qpu.Xai.Linear) (x y : List Int), (∀ (a : Int), a ∈ m.weights → 0 ≤ a) → Qpu.Xai.Le x y → m.eval x ≤ m.eval y | propext |
Qpu.Xai.eval_set_sub_set | ∀ (m : Qpu.Xai.Linear) (l : List Int) (i : Nat) (u v : Int), i < l.length → m.eval (l.set i v) - m.eval (l.set i u) = m.weights.getD i 0 * (v - u) | propext, Quot.sound |
Qpu.Xai.eval_sub_set | ∀ (m : Qpu.Xai.Linear) (l : List Int) (i : Nat) (v : Int), i < l.length → m.eval l - m.eval (l.set i v) = m.weights.getD i 0 * (l.getD i 0 - v) | propext, Quot.sound |
Qpu.Xai.fidelity_le | ∀ (f g : List Int → Int) (data : List (List Int)), Qpu.Xai.fidelity f g data ≤ data.length | propext |
Qpu.Xai.fidelity_self | ∀ (f : List Int → Int) (data : List (List Int)), Qpu.Xai.fidelity f f data = data.length | propext, Quot.sound |
Qpu.Xai.getD_map_natAbs | ∀ (l : List Int) (i : Nat), (List.map Int.natAbs l).getD i 0 = (l.getD i 0).natAbs | propext |
Qpu.Xai.getD_set_ne | ∀ {α : Type} (l : List α) (i j : Nat) (v d : α), i ≠ j → (l.set i v).getD j d = l.getD j d | propext |
Qpu.Xai.hamming_le_length | ∀ (x y : List Int), Qpu.Xai.hamming x y ≤ x.length | propext, Quot.sound |
Qpu.Xai.hamming_self | ∀ (x : List Int), Qpu.Xai.hamming x x = 0 | propext |
Qpu.Xai.hamming_set_le_one | ∀ (x : List Int) (i : Nat) (v : Int), Qpu.Xai.hamming x (x.set i v) ≤ 1 | propext, Quot.sound |
Qpu.Xai.importance_le_total | ∀ (a : List Int) (k : Nat), k ∈ Qpu.Xai.importance a → k ≤ (Qpu.Xai.importance a).sum | propext, Quot.sound |
Qpu.Xai.influence_loo | ∀ (m : Qpu.Xai.Linear) (y : List Int) (j : Nat), j < y.length → m.eval y - m.eval (y.set j 0) = Qpu.Xai.influence m y j | propext, Quot.sound |
Qpu.Xai.influence_stability | ∀ (m : Qpu.Xai.Linear) (y : List Int) (j k : Nat) (v : Int), k ≠ j → Qpu.Xai.influence m (y.set k v) j = Qpu.Xai.influence m y j | propext |
Qpu.Xai.integrated_gradients_linear | ∀ (steps : Nat), 0 < steps → ∀ (a : Int), (Qpu.Xai.igRiemann steps a).sum / ↑steps = a | propext, Quot.sound |
Qpu.Xai.interaction_zero | ∀ (m : Qpu.Xai.Linear) (x : List Int) (i j : Nat) (a b : Int), j < x.length → i ≠ j → m.eval ((x.set i a).set j b) - m.eval (x.set i a) - (m.eval (x.set j b) - m.eval x) = 0 | propext, Quot.sound |
Qpu.Xai.lattice_attention_bounded | ∀ (w : Nat), w ∈ (Qpu.Xai.uniform n hexbit).weights → w ≤ n * hexbit | propext, Quot.sound |
Qpu.Xai.lrp_conservation | ∀ (R : List Nat) (Ss : List (List (List Nat))), Qpu.Xai.Chain R Ss → (Qpu.Xai.propagateAll R Ss).sum = R.sum | propext, Quot.sound |
Qpu.Xai.mem_le_sum | ∀ (l : List Nat) (a : Nat), a ∈ l → a ≤ l.sum | propext, Quot.sound |
Qpu.Xai.natAbs_sum_le | ∀ (l : List Int), l.sum.natAbs ≤ (List.map Int.natAbs l).sum | propext, Quot.sound |
Qpu.Xai.output_change_le_total_importance | ∀ (f : List Int → Int) (x b : List Int), x.length = b.length → (f x - f b).natAbs ≤ (Qpu.Xai.importance (Qpu.Xai.ablation f x b)).sum | propext, Quot.sound |
Qpu.Xai.pd_slope | ∀ (m : Qpu.Xai.Linear) (x : List Int) (i : Nat) (v : Int), i < x.length → Qpu.Xai.pd m x i (v + 1) - Qpu.Xai.pd m x i v = m.weights.getD i 0 | propext, Quot.sound |
Qpu.Xai.propagate_sum | ∀ (splits : List (List Nat)), (Qpu.Xai.propagate splits).sum = (List.map List.sum splits).sum | propext, Quot.sound |
Qpu.Xai.saliency_zero_iff | ∀ (m : Qpu.Xai.Linear) (i : Nat), (Qpu.Xai.saliency m).getD i 0 = 0 ↔ m.weights.getD i 0 = 0 | propext |
Qpu.Xai.saliency_zero_insensitive | ∀ (m : Qpu.Xai.Linear) (x : List Int) (i : Nat) (v : Int), i < x.length → (Qpu.Xai.saliency m).getD i 0 = 0 → m.eval (x.set i v) = m.eval x | propext, Quot.sound |
Qpu.Xai.sensitivity_eq_weight | ∀ (m : Qpu.Xai.Linear) (x : List Int) (i : Nat) (δ : Int), i < x.length → m.eval (x.set i (x.getD i 0 + δ)) - m.eval x = m.weights.getD i 0 * δ | propext, Quot.sound |
Qpu.Xai.sensitivity_noise_invariant | ∀ (m : Qpu.Xai.Linear) (x x' : List Int) (i : Nat) (δ : Int), i < x.length → i < x'.length → m.eval (x'.set i (x'.getD i 0 + δ)) - m.eval x' = m.eval (x.set i (x.getD i 0 + δ)) - m.eval x | propext, Quot.sound |
Qpu.Xai.sensitivity_ratio | ∀ (m : Qpu.Xai.Linear) (x : List Int) (i : Nat) (δ : Int), i < x.length → δ ≠ 0 → (m.eval (x.set i (x.getD i 0 + δ)) - m.eval x) / δ = m.weights.getD i 0 | propext, Quot.sound |
Qpu.Xai.shap_marginal_constant | ∀ (w : List Int) (S : List Bool) (x b : List Int) (i : Nat), i < S.length → S.length = x.length → x.length = b.length → Qpu.Xai.dot w (Qpu.Xai.mask (S.set i true) x b) - Qpu.Xai.dot w (Qpu.Xai.mask (S.set i false) x b) = w.getD i 0 * (x.getD i 0 - b.getD i 0) | propext, Quot.sound |
Qpu.Xai.sum_foldl_vadd | ∀ (L : List (List Nat)) (acc : List Nat), (List.foldl Qpu.Xai.vadd acc L).sum = acc.sum + (List.map List.sum L).sum | propext, Quot.sound |
Qpu.Xai.sum_replicate_int | ∀ (n : Nat) (a : Int), (List.replicate n a).sum = ↑n * a | propext, Quot.sound |
Qpu.Xai.sum_replicate_nat | ∀ (n k : Nat), (List.replicate n k).sum = n * k | propext, Quot.sound |
Qpu.Xai.sum_rollout | ∀ (a : List Nat) (B : List (List Nat)) (T : Nat), (∀ (r : List Nat), r ∈ B → r.sum = T) → a.length ≤ B.length → (Qpu.Xai.rollout a B).sum = a.sum * T | propext, Quot.sound |
Qpu.Xai.sum_smul | ∀ (k : Nat) (r : List Nat), (Qpu.Xai.smul k r).sum = k * r.sum | propext |
Qpu.Xai.sum_vadd | ∀ (u v : List Nat), (Qpu.Xai.vadd u v).sum = u.sum + v.sum | propext, Quot.sound |
Qpu.Xai.support_sufficient | ∀ (w x b : List Int), x.length = b.length → Qpu.Xai.dot w (Qpu.Xai.maskSupport w x b) = Qpu.Xai.dot w x | propext, Classical.choice, Quot.sound |
Qpu.Xai.telescope | ∀ (g : Nat → Int) (n : Nat), (List.map (fun k => g k - g (k + 1)) (List.range n)).sum = g 0 - g n | propext, Quot.sound |
Qpu.ZeroShot.agree_comm | ∀ (a b : Qpu.ZeroShot.Attr), Qpu.ZeroShot.agree a b = Qpu.ZeroShot.agree b a | propext |
Qpu.ZeroShot.agree_eq_length_iff | ∀ (a b : Qpu.ZeroShot.Attr), List.length a = List.length b → (Qpu.ZeroShot.agree a b = List.length a ↔ a = b) | propext, Classical.choice, Quot.sound |
Qpu.ZeroShot.agree_le_length_left | ∀ (a b : Qpu.ZeroShot.Attr), Qpu.ZeroShot.agree a b ≤ List.length a | propext, Quot.sound |
Qpu.ZeroShot.agree_le_length_right | ∀ (a b : Qpu.ZeroShot.Attr), Qpu.ZeroShot.agree a b ≤ List.length b | propext, Quot.sound |
Qpu.ZeroShot.agree_lt_of_ne | ∀ (a b : Qpu.ZeroShot.Attr), List.length a = List.length b → a ≠ b → Qpu.ZeroShot.agree a b < List.length a | propext, Classical.choice, Quot.sound |
Qpu.ZeroShot.agree_nil_right | ∀ (a : Qpu.ZeroShot.Attr), Qpu.ZeroShot.agree a [] = 0 | — |
Qpu.ZeroShot.agree_self | ∀ (a : Qpu.ZeroShot.Attr), Qpu.ZeroShot.agree a a = List.length a | propext |
Qpu.ZeroShot.agree_triangle | ∀ (a b c : Qpu.ZeroShot.Attr), List.length a = List.length b → List.length b = List.length c → Qpu.ZeroShot.agree a b + Qpu.ZeroShot.agree b c ≤ List.length a + Qpu.ZeroShot.agree a c | propext, Classical.choice, Quot.sound |
Qpu.ZeroShot.allClasses_distinct | ∀ (d : Nat), Qpu.ZeroShot.Distinct (Qpu.ZeroShot.allClasses d) | propext, Quot.sound |
Qpu.ZeroShot.allClasses_length | ∀ (d : Nat), (Qpu.ZeroShot.allClasses d).length = mintOf d | propext |
Qpu.ZeroShot.allClasses_uniform | ∀ (d : Nat), Qpu.ZeroShot.Uniform d (Qpu.ZeroShot.allClasses d) | propext, Quot.sound |
Qpu.ZeroShot.allVecs_complete | ∀ (v : Qpu.ZeroShot.Attr), v ∈ Qpu.ZeroShot.allVecs (List.length v) | propext, Quot.sound |
Qpu.ZeroShot.allVecs_length | ∀ (d : Nat), (Qpu.ZeroShot.allVecs d).length = mintOf d | propext |
Qpu.ZeroShot.allVecs_nodup | ∀ (d : Nat), (Qpu.ZeroShot.allVecs d).Nodup | propext, Quot.sound |
Qpu.ZeroShot.allVecs_uniform | ∀ (d : Nat) (v : Qpu.ZeroShot.Attr), v ∈ Qpu.ZeroShot.allVecs d → List.length v = d | propext, Quot.sound |
Qpu.ZeroShot.best_attained | ∀ (q : Qpu.ZeroShot.Attr) {cs : List Qpu.ZeroShot.Class}, cs ≠ [] → ∃ c, c ∈ cs ∧ Qpu.ZeroShot.score q c = Qpu.ZeroShot.best q cs | propext, Quot.sound |
Qpu.ZeroShot.best_cons_ge | ∀ (q : Qpu.ZeroShot.Attr) (c : Qpu.ZeroShot.Class) (cs : List Qpu.ZeroShot.Class), Qpu.ZeroShot.best q cs ≤ Qpu.ZeroShot.best q (c :: cs) | propext |
Qpu.ZeroShot.best_ge_score | ∀ (q : Qpu.ZeroShot.Attr) {c : Qpu.ZeroShot.Class} {cs : List Qpu.ZeroShot.Class}, c ∈ cs → Qpu.ZeroShot.score q c ≤ Qpu.ZeroShot.best q cs | propext |
Qpu.ZeroShot.best_le_length | ∀ (q : Qpu.ZeroShot.Attr) (cs : List Qpu.ZeroShot.Class), Qpu.ZeroShot.best q cs ≤ List.length q | propext, Quot.sound |
Qpu.ZeroShot.code_inj | ∀ (a b : Qpu.ZeroShot.Attr), List.length a = List.length b → Qpu.ZeroShot.code a = Qpu.ZeroShot.code b → a = b | propext, Classical.choice, Quot.sound |
Qpu.ZeroShot.code_lt | ∀ (a : Qpu.ZeroShot.Attr), Qpu.ZeroShot.code a < mintOf (List.length a) | propext, Quot.sound |
Qpu.ZeroShot.dim_insufficient | ∀ {dim : Nat} {cs : List Qpu.ZeroShot.Class}, Qpu.ZeroShot.Uniform dim cs → mintOf dim < cs.length → ¬Qpu.ZeroShot.Distinct cs | propext, Classical.choice, Quot.sound |
Qpu.ZeroShot.distinct_attr_inj | ∀ {cs : List Qpu.ZeroShot.Class}, Qpu.ZeroShot.Distinct cs → ∀ {c d : Qpu.ZeroShot.Class}, c ∈ cs → d ∈ cs → c.attr = d.attr → c = d | propext |
Qpu.ZeroShot.distinct_le_mintOf | ∀ {dim : Nat} {cs : List Qpu.ZeroShot.Class}, Qpu.ZeroShot.Uniform dim cs → Qpu.ZeroShot.Distinct cs → cs.length ≤ mintOf dim | propext, Classical.choice, Quot.sound |
Qpu.ZeroShot.dot_comm | ∀ (a b : List Nat), Qpu.ZeroShot.dot a b = Qpu.ZeroShot.dot b a | propext |
Qpu.ZeroShot.dot_indicator_le_agree | ∀ (a b : Qpu.ZeroShot.Attr), Qpu.ZeroShot.dot (Qpu.ZeroShot.indicator a) (Qpu.ZeroShot.indicator b) ≤ Qpu.ZeroShot.agree a b | propext, Quot.sound |
Qpu.ZeroShot.exact_match_best | ∀ (q : Qpu.ZeroShot.Attr) {c : Qpu.ZeroShot.Class} {cs : List Qpu.ZeroShot.Class}, c ∈ cs → c.attr = q → Qpu.ZeroShot.best q cs = List.length q | propext, Quot.sound |
Qpu.ZeroShot.exact_match_predicted | ∀ (q : Qpu.ZeroShot.Attr) {c : Qpu.ZeroShot.Class} {cs : List Qpu.ZeroShot.Class}, Qpu.ZeroShot.Uniform (List.length q) cs → Qpu.ZeroShot.Distinct cs → c ∈ cs → c.attr = q → Qpu.ZeroShot.predict q cs = some c | propext, Classical.choice, Quot.sound |
Qpu.ZeroShot.exact_match_predicted_attr | ∀ (q : Qpu.ZeroShot.Attr) {c d : Qpu.ZeroShot.Class} {cs : List Qpu.ZeroShot.Class}, Qpu.ZeroShot.Uniform (List.length q) cs → c ∈ cs → c.attr = q → Qpu.ZeroShot.predict q cs = some d → d.attr = q | propext, Classical.choice, Quot.sound |
Qpu.ZeroShot.exact_match_predicted_score | ∀ (q : Qpu.ZeroShot.Attr) {c d : Qpu.ZeroShot.Class} {cs : List Qpu.ZeroShot.Class}, c ∈ cs → c.attr = q → Qpu.ZeroShot.predict q cs = some d → Qpu.ZeroShot.score q d = List.length q | propext, Quot.sound |
Qpu.ZeroShot.indistinguishable | ∀ {c d : Qpu.ZeroShot.Class}, c.attr = d.attr → ∀ (q : Qpu.ZeroShot.Attr), Qpu.ZeroShot.score q c = Qpu.ZeroShot.score q d | propext |
Qpu.ZeroShot.mem_unseen | ∀ (isSeen : Qpu.ZeroShot.Class → Bool) (cs : List Qpu.ZeroShot.Class) (c : Qpu.ZeroShot.Class), c ∈ (Qpu.ZeroShot.split isSeen cs).snd ↔ c ∈ cs ∧ isSeen c = false | propext |
Qpu.ZeroShot.nodup_lt_length_le | ∀ (m : Nat) (l : List Nat), l.Nodup → (∀ (x : Nat), x ∈ l → x < m) → l.length ≤ m | propext, Classical.choice, Quot.sound |
Qpu.ZeroShot.predict_cons_of_ge | ∀ (q : Qpu.ZeroShot.Attr) {c : Qpu.ZeroShot.Class} {cs : List Qpu.ZeroShot.Class}, (∀ (d : Qpu.ZeroShot.Class), d ∈ cs → Qpu.ZeroShot.score q d ≤ Qpu.ZeroShot.score q c) → Qpu.ZeroShot.predict q (c :: cs) = some c | propext |
Qpu.ZeroShot.predict_cons_of_gt | ∀ (q : Qpu.ZeroShot.Attr) {c : Qpu.ZeroShot.Class} {cs : List Qpu.ZeroShot.Class}, Qpu.ZeroShot.best q cs < Qpu.ZeroShot.score q c → Qpu.ZeroShot.predict q (c :: cs) = some c | propext |
Qpu.ZeroShot.predict_exists | ∀ (q : Qpu.ZeroShot.Attr) {cs : List Qpu.ZeroShot.Class}, cs ≠ [] → ∃ c, Qpu.ZeroShot.predict q cs = some c | propext |
Qpu.ZeroShot.predict_is_argmax | ∀ (q : Qpu.ZeroShot.Attr) {cs : List Qpu.ZeroShot.Class} {c : Qpu.ZeroShot.Class}, Qpu.ZeroShot.predict q cs = some c → ∀ (d : Qpu.ZeroShot.Class), d ∈ cs → Qpu.ZeroShot.score q d ≤ Qpu.ZeroShot.score q c | propext, Quot.sound |
Qpu.ZeroShot.predict_mem | ∀ (q : Qpu.ZeroShot.Attr) {cs : List Qpu.ZeroShot.Class} {c : Qpu.ZeroShot.Class}, Qpu.ZeroShot.predict q cs = some c → c ∈ cs | propext |
Qpu.ZeroShot.predict_none_iff | ∀ (q : Qpu.ZeroShot.Attr) (cs : List Qpu.ZeroShot.Class), Qpu.ZeroShot.predict q cs = none ↔ cs = [] | propext |
Qpu.ZeroShot.predict_score | ∀ (q : Qpu.ZeroShot.Attr) {cs : List Qpu.ZeroShot.Class} {c : Qpu.ZeroShot.Class}, Qpu.ZeroShot.predict q cs = some c → Qpu.ZeroShot.score q c = Qpu.ZeroShot.best q cs | propext, Quot.sound |
Qpu.ZeroShot.predict_unseen_cons_seen | ∀ (isSeen : Qpu.ZeroShot.Class → Bool) (q : Qpu.ZeroShot.Attr) (cs : List Qpu.ZeroShot.Class) {s : Qpu.ZeroShot.Class}, isSeen s = true → Qpu.ZeroShot.predict q (Qpu.ZeroShot.split isSeen (s :: cs)).snd = Qpu.ZeroShot.predict q (Qpu.ZeroShot.split isSeen cs).snd | propext |
Qpu.ZeroShot.predict_unseen_cons_unseen | ∀ (isSeen : Qpu.ZeroShot.Class → Bool) (q : Qpu.ZeroShot.Attr) (cs : List Qpu.ZeroShot.Class) {u : Qpu.ZeroShot.Class}, isSeen u = false → Qpu.ZeroShot.best q (Qpu.ZeroShot.split isSeen cs).snd < Qpu.ZeroShot.score q u → Qpu.ZeroShot.predict q (Qpu.ZeroShot.split isSeen (u :: cs)).snd = some u | propext |
Qpu.ZeroShot.score_exact | ∀ (q : Qpu.ZeroShot.Attr) {c : Qpu.ZeroShot.Class}, c.attr = q → Qpu.ZeroShot.score q c = List.length q | propext |
Qpu.ZeroShot.score_le_length | ∀ (q : Qpu.ZeroShot.Attr) (c : Qpu.ZeroShot.Class), Qpu.ZeroShot.score q c ≤ List.length q | propext, Quot.sound |
Qpu.ZeroShot.score_of_attr_eq | ∀ (q : Qpu.ZeroShot.Attr) {c d : Qpu.ZeroShot.Class}, c.attr = d.attr → Qpu.ZeroShot.score q c = Qpu.ZeroShot.score q d | propext |
Qpu.ZeroShot.semantic_transitivity | ∀ (a b c : Qpu.ZeroShot.Attr) (k : Nat), List.length a = List.length b → List.length b = List.length c → List.length a ≤ Qpu.ZeroShot.agree a b + k → List.length a ≤ Qpu.ZeroShot.agree b c + k → List.length a ≤ Qpu.ZeroShot.agree a c + 2 * k | propext, Classical.choice, Quot.sound |
Qpu.ZeroShot.separable | ∀ {c d : Qpu.ZeroShot.Class}, List.length c.attr = List.length d.attr → c.attr ≠ d.attr → Qpu.ZeroShot.score c.attr d < Qpu.ZeroShot.score c.attr c | propext, Classical.choice, Quot.sound |
Qpu.ZeroShot.split_cover | ∀ (isSeen : Qpu.ZeroShot.Class → Bool) {cs : List Qpu.ZeroShot.Class} {c : Qpu.ZeroShot.Class}, c ∈ cs → c ∈ (Qpu.ZeroShot.split isSeen cs).fst ∨ c ∈ (Qpu.ZeroShot.split isSeen cs).snd | propext |
Qpu.ZeroShot.split_disjoint | ∀ (isSeen : Qpu.ZeroShot.Class → Bool) (cs : List Qpu.ZeroShot.Class) {c : Qpu.ZeroShot.Class}, c ∈ (Qpu.ZeroShot.split isSeen cs).fst → ¬c ∈ (Qpu.ZeroShot.split isSeen cs).snd | propext |
Qpu.ZeroShot.split_length | ∀ (isSeen : Qpu.ZeroShot.Class → Bool) (cs : List Qpu.ZeroShot.Class), (Qpu.ZeroShot.split isSeen cs).fst.length + (Qpu.ZeroShot.split isSeen cs).snd.length = cs.length | propext, Quot.sound |
Qpu.ZeroShot.split_unseen_cons_seen | ∀ (isSeen : Qpu.ZeroShot.Class → Bool) (cs : List Qpu.ZeroShot.Class) {s : Qpu.ZeroShot.Class}, isSeen s = true → (Qpu.ZeroShot.split isSeen (s :: cs)).snd = (Qpu.ZeroShot.split isSeen cs).snd | propext |
Qpu.ZeroShot.vertices_bound | ∀ {cs : List Qpu.ZeroShot.Class}, Qpu.ZeroShot.Uniform n cs → Qpu.ZeroShot.Distinct cs → cs.length ≤ vertices | propext, Classical.choice, Quot.sound |
all_complete | faces = coins * rays ∧ faces = rays + rays ∧ coil = faces ∧ amplitudes = mintOf bits ∧ fused = faces * mintOf (bits + seed) | — |
all_entangle | 1 * 1 ≠ 0 * 0 | propext |
all_noclone | coins ≠ mintOf coins | — |
all_product | faces = coins * rays | — |
all_shor | periodOf shorBase shorModulus % coins = 0 | — |
all_sum | faces = rays + rays | — |
amplitudes_as_sum | mintOf (bits + seed) = amplitudes + amplitudes | — |
amplitudes_from_sum | 2 * amplitudes = mintOf (bits + seed) | — |
annealing_all | chimera 16 = 2048 ∧ pegasus 16 = 5760 | — |
anyon_all | fibFusion 5 = 5 ∧ fibFusion 10 = 55 ∧ isingFusion 3 = 4 | — |
around | faces = coins * rays | — |
bits_both_forms | bits = vertices * hexbit ∧ bits = mintOf (n + coins) | — |
bits_exponential | bits = mintOf (n + coins) | — |
bits_multiplicative | bits = vertices * hexbit | — |
breakthrough | faces = rays + rays ∧ coins * rays = faces ∧ bits = vertices * hexbit ∧ fused = faces * mintOf (bits + seed) ∧ mintOf hexbit > seed ∧ mintOf (bits + seed) = amplitudes + amplitudes ∧ coins = seed + seed ∧ hexbit = n + seed | — |
cern | 116 * 17922 + 54 = 2079006 ∧ 184 * 12509 + 12 = 2301668 ∧ 72 * 26572 + 6 = 1913190 ∧ 130 * 21121 + 21 = 2745751 ∧ 8 - 7 = 1 ∧ 8000 - 7000 = 1000 ∧ 7000 / 2 = 3500 ∧ 8000 / 2 = 4000 ∧ 4000 - 3500 = 500 ∧ 2019 - 2011 = 8 ∧ 2019 - 2012 = 7 ∧ 2017 - 2011 = 6 ∧ 2301668 + 2745751 = 5047419 ∧ 2079006 + 1913190 + 2301668 + 2745751 = 9039615 | — |
choose_five_two | choose 5 2 = 10 | — |
choose_pascal | ∀ (n k : Nat), choose (n + 1) (k + 1) = choose n (k + 1) + choose n k | — |
choose_symm_small | choose 5 2 = choose 5 3 | — |
choose_zero | ∀ (n : Nat), choose n 0 = 1 | — |
choose_zero_succ | ∀ (k : Nat), choose 0 (k + 1) = 0 | — |
circuit | 0 ^^^ 1 ^^^ 2 = 3 ∧ 3 ^^^ 1 ^^^ 1 = 3 ∧ mintOf n = vertices | propext |
clay | coins * rays = (seed + (mintOf n - coins)) * coins ∧ (seed + (mintOf n - coins)) * coins = coil | — |
clay_sigma | 2 - (2 - 1) = 1 ∧ 1 - (1 - 0) = 0 ∧ 1 - (1 - 1) = 1 ∧ 2 * 2 = 4 ∧ 1 + 1 = 2 | — |
clay_wings | (vertices = hybridSpeed ∧ vertices = mintOf n) ∧ (magicBlock = glProd hexbit seed ∧ magicBlock = qftDepth vertices) ∧ (mintOf hexbit = powMod coins rays plane ∧ mintOf hexbit = powMod coins hexbit bits) ∧ (bits = chimera coins ∧ bits = qaoaZz vertices hexbit) ∧ (mintOf rays = chimera hexbit ∧ mintOf rays = isingFusion vertices) ∧ (plane = chooseOf vertices coins ∧ plane = choose vertices coins) ∧ (mintOf vertices = groverSize hexbit ∧ mintOf vertices = qaoaZz vertices bits) ∧ triangular hexbit = qftGates hexbit ∧ (faces = coil ∧ faces = qaoaParams rays) ∧ (chooseOf rays coins = fibFusion vertices ∧ chooseOf rays coins = powMod rays coins plane) ∧ (powMod n hexbit plane = powMod n faces bits ∧ powMod n hexbit plane = powMod n plane plane) ∧ (isingFusion rays = groverSize n ∧ isingFusion rays = qaoaParams bits) ∧ (mintOf faces = groverSize rays ∧ mintOf faces = qftStates faces) ∧ (fibFusion rays = powMod n n faces ∧ fibFusion rays = half n faces) ∧ (powMod faces n bits = cliffordOrder seed ∧ powMod faces n bits = factorial hexbit) ∧ (magicCubic = chooseOf rays n ∧ magicCubic = chooseOf rays hexbit) ∧ triangular faces = qftGates faces ∧ (mintOf plane = groverSize faces ∧ mintOf plane = qftStates plane) ∧ (amplitudes = mintOf bits ∧ amplitudes = qftStates bits) ∧ (powMod n coins bits = powMod n coins faces ∧ powMod n coins bits = powMod n coins plane) ∧ (groverIters hexbit = qaoaZz n hexbit ∧ groverIters hexbit = qaoaZz hexbit n) ∧ (powMod n hexbit bits = powMod n plane bits ∧ powMod n hexbit bits = powMod rays coins bits) ∧ (chooseOf vertices n = choose vertices n ∧ chooseOf vertices n = qaoaParams plane) ∧ chooseOf vertices hexbit = choose vertices hexbit ∧ (qaoaZz bits bits = qaoaX bits bits ∧ qaoaZz bits bits = paulis hexbit) ∧ (powMod n n bits = powMod n n plane ∧ powMod n n bits = half n plane) ∧ triangular vertices = qftGates vertices ∧ (glProd n coins = qaoaZz n faces ∧ glProd n coins = qaoaZz faces n) ∧ qaoaZz rays rays = qaoaX rays rays ∧ chooseOf faces coins = choose faces coins ∧ (qaoaZz n bits = qaoaZz bits n ∧ qaoaZz n bits = qaoaX n bits) ∧ (qaoaZz rays plane = qaoaZz faces faces ∧ qaoaZz rays plane = qaoaZz plane rays) ∧ (qaoaZz rays bits = qaoaZz vertices plane ∧ qaoaZz rays bits = qaoaZz bits rays) ∧ chooseOf faces n = choose faces n ∧ chooseOf plane coins = choose plane coins ∧ (chimera rays = qaoaZz faces plane ∧ chimera rays = qaoaZz plane faces) ∧ triangular plane = qftGates plane ∧ chooseOf bits coins = choose bits coins ∧ triangular bits = qftGates bits ∧ chooseOf faces hexbit = choose faces hexbit ∧ chooseOf faces vertices = choose faces vertices ∧ chooseOf plane n = choose plane n ∧ chooseOf faces rays = choose faces rays ∧ chooseOf bits n = choose bits n ∧ chimera bits = isingFusion faces ∧ chooseOf plane hexbit = choose plane hexbit ∧ (chooseOf bits hexbit = chooseOf bits plane ∧ chooseOf bits hexbit = choose bits hexbit) ∧ groverSize vertices = paulis rays ∧ chooseOf plane rays = choose plane rays ∧ chooseOf plane vertices = choose plane vertices ∧ chooseOf bits rays = choose bits rays ∧ chooseOf bits vertices = choose bits vertices ∧ chooseOf plane faces = choose plane faces ∧ chooseOf bits faces = choose bits faces | — |
clifford_all | symplectic 1 = 6 ∧ symplectic 2 = 720 ∧ symplectic 3 = 1451520 ∧ cliffordOrder 2 = 11520 | — |
cluster | faces = rays + rays ∧ coins * rays = faces | — |
coil_efficiency | coil = faces ∧ faces = rays + rays ∧ coins * rays = faces | — |
coins_bridges_forms | coins = 2 ∧ ∀ (x : Nat), coins * x = x + x | — |
coins_two | coins = 2 | — |
computer | 1 ^^^ 3 = 2 ∧ 6 ^^^ 1 = 7 ∧ mintOf 0 = 1 | propext |
cooling_stays_positive | ∀ (t a n : Nat), 0 < t → 0 < a → 0 < t * a ^ n | — |
cooling_strictly_decreases | ∀ (t a b n : Nat), 0 < t → 0 < a → a < b → t * a ^ n * a < t * a ^ n * b | — |
crypto | fused = faces * mintOf (vertices * hexbit + seed) | — |
cube | bits = vertices * hexbit | — |
dense | coins * coins = mintOf coins | — |
design | 0 ^^^ 4 ^^^ 4 = 0 ∧ 3 ^^^ 4 ^^^ 4 = 3 | propext |
deutsch | 1 - 1 = 0 ∧ seed ≠ coins | — |
distribute | fused = faces * mintOf (bits + seed) ∧ faces = coins * rays | — |
double_is_sum | ∀ (x : Nat), x + x = 2 * x | — |
drift | coins = 2 ∧ mintOf n = vertices ∧ 0 ^^^ 1 ^^^ 2 = 3 ∧ 3 ^^^ 1 ^^^ 1 = 3 | propext |
electronics | coil = faces | — |
energy | mintOf hexbit = mintOf (n + seed) | — |
entangle | 1 * 1 ≠ 0 * 0 | propext |
faces_additive | faces = rays + rays | — |
faces_both_forms | faces = coins * rays ∧ faces = rays + rays | — |
faces_multiplicative | faces = coins * rays | — |
factorial_succ | ∀ (n : Nat), factorial (n + 1) = (n + 1) * factorial n | — |
factorial_three | factorial 3 = 6 | — |
factorial_zero | factorial 0 = 1 | — |
fill | mintOf n * faces = vertices * (coins * rays) | — |
follow_the_coins | ∀ (app : Nat), app + coins = app + theory + practice | — |
fuse | 2247 + 282 = 2529 ∧ 94598 + 343701 = 438299 ∧ 406 + 1565 + 3389 + 6011 + 12801 + 414127 = 438299 ∧ 448 ≤ 1264 ∧ 362 ≤ 955 ∧ 301 ≤ 340 ∧ 252 ≤ 284 ∧ 144 ≤ 166 ∧ 2529 + 438299 = 440828 | — |
fused_additive_form | fused + fused = faces * mintOf (bits + coins) | — |
fused_both_directions | fused = faces * mintOf (bits + seed) ∧ fused + fused = faces * mintOf (bits + coins) | — |
fused_multiplicative_form | fused = faces * mintOf (bits + seed) | — |
fusion | fused = faces * mintOf (bits + seed) ∧ faces = rays + rays | — |
fusion_baseline | fusionBaselineQ * fusionBaselineC = 2076880 | — |
fusion_max_x | fusionMaxX = 3133452 | — |
fusion_register | fusionRegister = 22 | — |
fusion_tolerance | fusionTolSquared = 2 ^ 128 / 2 ^ 48 | — |
galois_all | gl2 2 = 6 ∧ gl2 3 = 168 ∧ gl2 4 = 20160 | — |
gates | 0 ^^^ 1 ^^^ 2 = 3 | propext |
ghz | mintOf n - seed = 7 ∧ 1 * 1 ≠ 0 * 0 | propext |
grover_all | groverIters 2 = 3 ∧ groverIters 5 = 25 ∧ groverSize 5 = 1024 | — |
handle | amplitudes = mintOf bits ∧ mintOf (bits + seed) = amplitudes + amplitudes | — |
harmonic | faces = rays + rays | — |
health | mintOf hexbit > seed ∧ fused = faces * mintOf (bits + seed) ∧ faces = rays + rays | — |
hexbit_eq | hexbit = n + seed | — |
hexbit_pos | 0 < hexbit | — |
hybrid | coins + seed = n ∧ rays + seed = mintOf n ∧ coins = seed + seed | — |
hybrid_cost | coins + seed = n | — |
hybrid_speed | rays + seed = mintOf n | — |
infinite | ∀ (k : Nat), mintOf (k + seed) = mintOf k + mintOf k | — |
integrity | fused = faces * mintOf (bits + seed) ∧ bits = vertices * hexbit ∧ faces = coins * rays | — |
interfere | 1 + 1 = 2 ∧ 1 - 1 = 0 | — |
involution | ∀ (face : Nat), (face + rays + rays) % faces = face % faces | propext |
key_trinity | 4 + 3 + 2 = 9 ∧ 432 % 9 = 0 ∧ 10 - 9 = 1 | — |
kickback | 1 - 1 = 0 ∧ 0 ^^^ 1 ^^^ 2 = 3 | propext |
kv | fused = faces * mintOf (bits + seed) ∧ mintOf (bits + seed) = amplitudes + amplitudes | — |
light | seed = mintOf 0 | — |
magic_all | magicBlock = 15 ∧ magicLogical = 1 ∧ magicDistance = 3 ∧ magicCubic = 35 | — |
measurement | mintOf n = 8 | — |
mersenne_127 | mintOf rays - seed = 127 | — |
mersenne_3 | mintOf coins - seed = 3 | — |
mersenne_31 | bits - seed = 31 | — |
mersenne_7 | mintOf n - seed = 7 | — |
mint | mintOf (n + seed) = mintOf n + mintOf n | — |
mintOf_add | ∀ (a b : Nat), mintOf (a + b) = mintOf a * mintOf b | — |
mintOf_ge_seed | ∀ (k : Nat), seed ≤ mintOf k | — |
mintOf_lt | ∀ {a b : Nat}, a < b → mintOf a < mintOf b | — |
mintOf_lt_succ | ∀ (k : Nat), mintOf k < mintOf (k + 1) | — |
mintOf_pos | ∀ (k : Nat), 0 < mintOf k | — |
mintOf_succ | ∀ (k : Nat), mintOf (k + 1) = mintOf k + mintOf k | — |
mintOf_zero | mintOf 0 = 1 | — |
monogamy | 1 * 1 ≠ 0 * 0 ∧ 1 * 0 = 0 * 0 | propext |
multiply | ∀ (a b : Nat), mintOf (a + b) = mintOf a * mintOf b | — |
n_eq | n = 3 | — |
neuro | faces = coins * rays ∧ mintOf n = 8 ∧ 0 ^^^ 4 ^^^ 4 = 0 | propext |
next | mintOf (bits + seed) = amplitudes + amplitudes | — |
next_coil | coil * mintOf (bits + coins) = fused + fused | — |
next_cover | mintOf (bits + seed) = amplitudes + amplitudes ∧ faces * mintOf (bits + coins) = fused + fused | — |
next_fused | faces * mintOf (bits + coins) = fused + fused | — |
noclone | coins ≠ mintOf coins | — |
noise | 3 ^^^ 1 ^^^ 1 = 3 | propext |
one_plus_six | seed + (mintOf n - coins) = rays | — |
only | 1 * 1 ≠ 0 * 0 ∧ 1 + 1 = 2 ∧ 1 - 1 = 0 ∧ coins ≠ mintOf coins ∧ mintOf n - seed = 7 ∧ 2 * 2 * 2 * 2 = 16 ∧ 16 = 16 ∧ 0 ^^^ 1 ^^^ 2 = 3 ∧ seed ≠ coins ∧ coins * coins = mintOf coins ∧ 1 * 0 = 0 * 0 | propext |
physical | n = 3 ∧ mintOf n = vertices ∧ 0 ^^^ 1 ^^^ 2 = 3 ∧ 3 ^^^ 1 ^^^ 1 = 3 | propext |
pi_all | mintOf coins - seed = 3 ∧ faces + vertices = 22 ∧ rays = 7 ∧ plane * (faces - seed) - n * n = 355 ∧ plane * hexbit + seed = 113 ∧ (faces - coins) * (plane + coins) = 360 ∧ (faces - coins) * (faces + seed) = 180 | — |
pi_archimedes_den | rays = 7 | — |
pi_archimedes_num | faces + vertices = 22 | — |
pi_floor | mintOf coins - seed = 3 | — |
pi_half_turn | (faces - coins) * (faces + seed) = 180 | — |
pi_turn_degrees | (faces - coins) * (plane + coins) = 360 | — |
pi_zu_den | plane * hexbit + seed = 113 | — |
pi_zu_num | plane * (faces - seed) - n * n = 355 | — |
planes | plane < mintOf (rays + seed) ∧ coins * rays = faces | — |
prime_three | n = 3 | — |
prime_two | coins = 2 | — |
primes_all | coins = 2 ∧ n = 3 ∧ mintOf coins - seed = 3 ∧ mintOf n - seed = 7 ∧ bits - seed = 31 ∧ mintOf rays - seed = 127 ∧ rays * (faces - seed) = 91 ∧ rays * (faces - seed) = chooseOf faces coins ∧ faces - n = 11 ∧ faces - seed = 13 ∧ faces - seed - (faces - n) = coins ∧ coins * n * (n + coins) * rays = 210 | — |
primorial_210 | coins * n * (n + coins) * rays = 210 | — |
propulsion | mintOf hexbit > seed | — |
qaoa_all | qaoaParams 3 = 6 ∧ qaoaZz 2 5 = 10 ∧ qaoaX 3 4 = 12 | — |
qft_all | qftGates 3 = 6 ∧ qftGates 4 = 10 ∧ qftSwaps 4 = 2 ∧ qftDepth 4 = 7 ∧ qftStates 4 = 16 | — |
quantum | fused = faces * mintOf (bits + seed) | — |
qubits | n = 3 ∧ mintOf n = vertices | — |
raid | faces = coins * rays ∧ faces = rays + rays | — |
ramsey22_eq | ∀ (n : Nat), ramsey22 n = n | — |
ramsey_three_three | triangular 3 = 6 | — |
relation_10 | triangular hexbit = qftGates hexbit | — |
relation_1001 | chooseOf faces hexbit = choose faces hexbit | — |
relation_1024 | qaoaZz bits bits = qaoaX bits bits ∧ qaoaZz bits bits = paulis hexbit | — |
relation_105 | triangular faces = qftGates faces | — |
relation_10518300 | chooseOf bits vertices = choose bits vertices | — |
relation_1184040 | chooseOf plane rays = choose plane rays | — |
relation_12 | groverIters hexbit = qaoaZz n hexbit ∧ groverIters hexbit = qaoaZz hexbit n | — |
relation_128 | mintOf rays = chimera hexbit ∧ mintOf rays = isingFusion vertices | — |
relation_13 | fibFusion rays = powMod n n faces ∧ fibFusion rays = half n faces | — |
relation_14 | faces = coil ∧ faces = qaoaParams rays | — |
relation_15 | magicBlock = glProd hexbit seed ∧ magicBlock = qftDepth vertices | — |
relation_16 | mintOf hexbit = powMod coins rays plane ∧ mintOf hexbit = powMod coins hexbit bits | — |
relation_16384 | mintOf faces = groverSize rays ∧ mintOf faces = qftStates faces | — |
relation_17 | powMod n hexbit bits = powMod n plane bits ∧ powMod n hexbit bits = powMod rays coins bits | — |
relation_196 | qaoaZz rays plane = qaoaZz faces faces ∧ qaoaZz rays plane = qaoaZz plane rays | — |
relation_20475 | chooseOf plane hexbit = choose plane hexbit | — |
relation_21 | chooseOf rays coins = fibFusion vertices ∧ chooseOf rays coins = powMod rays coins plane | — |
relation_224 | qaoaZz rays bits = qaoaZz vertices plane ∧ qaoaZz rays bits = qaoaZz bits rays | — |
relation_24 | powMod faces n bits = cliffordOrder seed ∧ powMod faces n bits = factorial hexbit | — |
relation_25 | powMod n hexbit plane = powMod n faces bits ∧ powMod n hexbit plane = powMod n plane plane | — |
relation_256 | mintOf vertices = groverSize hexbit ∧ mintOf vertices = qaoaZz vertices bits | — |
relation_268435456 | mintOf plane = groverSize faces ∧ mintOf plane = qftStates plane | — |
relation_27 | powMod n n bits = powMod n n plane ∧ powMod n n bits = half n plane | — |
relation_28 | plane = chooseOf vertices coins ∧ plane = choose vertices coins | — |
relation_3003 | chooseOf faces vertices = choose faces vertices | — |
relation_3108105 | chooseOf plane vertices = choose plane vertices | — |
relation_32 | bits = chimera coins ∧ bits = qaoaZz vertices hexbit | — |
relation_3276 | chooseOf plane n = choose plane n | — |
relation_3365856 | chooseOf bits rays = choose bits rays | — |
relation_3432 | chooseOf faces rays = choose faces rays | — |
relation_35 | magicCubic = chooseOf rays n ∧ magicCubic = chooseOf rays hexbit | — |
relation_35960 | chooseOf bits hexbit = chooseOf bits plane ∧ chooseOf bits hexbit = choose bits hexbit | — |
relation_36 | triangular vertices = qftGates vertices | — |
relation_364 | chooseOf faces n = choose faces n | — |
relation_378 | chooseOf plane coins = choose plane coins | — |
relation_392 | chimera rays = qaoaZz faces plane ∧ chimera rays = qaoaZz plane faces | — |
relation_40116600 | chooseOf plane faces = choose plane faces | — |
relation_406 | triangular plane = qftGates plane | — |
relation_42 | glProd n coins = qaoaZz n faces ∧ glProd n coins = qaoaZz faces n | — |
relation_4294967296 | amplitudes = mintOf bits ∧ amplitudes = qftStates bits | — |
relation_471435600 | chooseOf bits faces = choose bits faces | — |
relation_49 | qaoaZz rays rays = qaoaX rays rays | — |
relation_496 | chooseOf bits coins = choose bits coins | — |
relation_4960 | chooseOf bits n = choose bits n | — |
relation_528 | triangular bits = qftGates bits | — |
relation_56 | chooseOf vertices n = choose vertices n ∧ chooseOf vertices n = qaoaParams plane | — |
relation_64 | isingFusion rays = groverSize n ∧ isingFusion rays = qaoaParams bits | — |
relation_65536 | groverSize vertices = paulis rays | — |
relation_70 | chooseOf vertices hexbit = choose vertices hexbit | — |
relation_8 | vertices = hybridSpeed ∧ vertices = mintOf n | — |
relation_8192 | chimera bits = isingFusion faces | — |
relation_9 | powMod n coins bits = powMod n coins faces ∧ powMod n coins bits = powMod n coins plane | — |
relation_91 | chooseOf faces coins = choose faces coins | — |
relation_96 | qaoaZz n bits = qaoaZz bits n ∧ qaoaZz n bits = qaoaX n bits | — |
sciences | coins = 2 ∧ n = 3 ∧ mintOf n = vertices ∧ faces = coins * rays ∧ bits = vertices * hexbit ∧ fused = faces * mintOf (bits + seed) ∧ 0 ^^^ 1 ^^^ 2 = 3 | propext |
seed_eq | seed = 1 | — |
server | faces = coins * rays ∧ mintOf n = 8 | — |
shor | periodOf shorBase shorModulus % coins = 0 ∧ half shorBase shorModulus < shorModulus - seed ∧ seed < gcdOf (half shorBase shorModulus - seed) shorModulus ∧ gcdOf (half shorBase shorModulus - seed) shorModulus < shorModulus ∧ gcdOf (half shorBase shorModulus - seed) shorModulus * gcdOf (half shorBase shorModulus + seed) shorModulus = shorModulus | — |
shor_factored | rays * (faces - seed) = 91 | — |
shor_modulus_binomial | rays * (faces - seed) = chooseOf faces coins | — |
shor_sigma | periodOf shorBase shorModulus = mintOf coins ∧ periodOf shorBase shorModulus - periodOf shorBase shorModulus / coins = periodOf shorBase shorModulus / coins ∧ gcdOf (half shorBase shorModulus - seed) shorModulus = rays ∧ gcdOf (half shorBase shorModulus + seed) shorModulus = faces - seed ∧ gcdOf (half shorBase shorModulus - seed) shorModulus * gcdOf (half shorBase shorModulus + seed) shorModulus = shorModulus | propext, Quot.sound |
sigma_choose | choose rays coins = choose rays (rays - coins) ∧ rays - (rays - coins) = coins | propext, Quot.sound |
sigma_grover | 2 * groverSize seed - groverSize seed = groverSize seed | propext, Quot.sound |
sigma_hodge | ∀ (g : Nat), 2 * g = g + g | propext, Quot.sound |
sigma_lattice | 2 * faces - faces = faces ∧ faces - (faces - vertices) = vertices | propext, Quot.sound |
sigma_midpoint | ∀ (d x : Nat), 2 * x = d → d - x = x | propext, Quot.sound |
sigma_pauli | 1 - (1 - seed) = seed ∧ 1 - (1 - (n - n)) = n - n | propext, Quot.sound |
sigma_planck | planck - (planck - boltzmann) = boltzmann ∧ 2 * planck - planck = planck ∧ 2 * photon - photon = photon ∧ 2 * (planck * planck) - planck * planck = planck * planck | propext, Quot.sound |
sigma_pvsnp | ∀ (m : Nat), m ≤ 1 → 1 - (1 - m) = m | propext, Quot.sound |
sigma_qft | 2 * qftStates n - qftStates n = qftStates n ∧ qftStates n - (qftStates n - seed) = seed | propext, Quot.sound |
sigma_reflect | ∀ (d x : Nat), x ≤ d → d - (d - x) = x | propext, Quot.sound |
sigma_ten_involution | ∀ (x : Nat), x ≤ 10 → 10 - (10 - x) = x | propext, Quot.sound |
singularity | periodOf 8 91 - periodOf 8 91 / 2 = periodOf 8 91 / 2 ∧ 2 * planck - planck = planck ∧ choose rays coins = choose rays (rays - coins) ∧ 2 * qftStates n - qftStates n = qftStates n ∧ 2 * groverSize seed - groverSize seed = groverSize seed ∧ 2 * faces - faces = faces | propext, Quot.sound |
split_coin | ∀ (k : Nat), mintOf (k + seed) = mintOf k + mintOf k | — |
stabilizer_all | stabStates 1 = 6 ∧ stabStates 2 = 60 ∧ stabStates 3 = 1080 ∧ paulis 1 = 16 | — |
superconductivity | aluminium > 10 ∧ niobium > aluminium ∧ bcs / 100 = 3 ∧ gap aluminium = 88 ∧ gap aluminium > transmon ∧ gap niobium = 679 | — |
surfacecode_all | surfacePhysical 3 = 13 ∧ surfaceCorrectable 5 = 2 ∧ surfaceLogical = 2 | — |
teleport | 2 * 2 * 2 * 2 = 16 ∧ 16 = 16 | — |
temperature | photon / thermal 10 = 23 ∧ photon / thermal 100 = 2 ∧ photon / thermal 4000 = 0 ∧ 4000 / 100 = 40 ∧ 100 / 10 = 10 ∧ 10 < 35 | — |
tetra | coins + coins = mintOf coins | — |
textbook_configurations_closed | ∀ (k : Nat), k ≤ 8 → k = 8 → 8 - k = 0 | propext, Quot.sound |
textbook_fold_mirror | ∀ (n i : Nat), i ≤ n → i + (n - i) = n | propext, Quot.sound |
textbook_integrations_are_ten | 8 + 1 + 1 = 10 | — |
textbook_plugin_combinations | 2 ^ 8 = 256 | — |
textbook_prices_are_variants_times_currencies | 7 * 2 = 14 | — |
textbook_providers_are_tenants_plus_operator | 2 + 1 = 3 | — |
textbook_reflection_sums_to_ten | ∀ (s : Nat), s ≤ 10 → s + (10 - s) = 10 | propext, Quot.sound |
textbook_skills_documents | 2 + 12 = 14 | — |
textbook_uuid_is_36 | 32 + 4 = 36 | — |
textbook_website_plugins_partition | 4 + 3 + 1 = 8 | — |
triad_reflect | (10 - 3 = 7 ∧ 10 - 6 = 4 ∧ 10 - 9 = 1) ∧ (10 - 7 = 3 ∧ 10 - 4 = 6 ∧ 10 - 1 = 9) ∧ 10 - 2 = 8 ∧ 10 - 5 = 5 ∧ 10 - 8 = 2 | — |
triad_sum | 3 + 7 = 10 ∧ 6 + 4 = 10 ∧ 9 + 1 = 10 ∧ 2 + 8 = 10 ∧ 5 + 5 = 10 | — |
triangular_four | triangular 4 = 10 | — |
triangular_succ | ∀ (n : Nat), triangular (n + 1) = n + 1 + triangular n | — |
triangular_zero | triangular 0 = 0 | — |
twin_gap | faces - seed - (faces - n) = coins | — |
twin_lower | faces - n = 11 | — |
twin_upper | faces - seed = 13 | — |
two_coins_make_a_coil | coil = faces | — |
two_x_seven_coins | coins * rays = (seed + (mintOf n - coins)) * coins | — |
waves | mintOf hexbit > seed | — |