From 0a10ee524cac236a4879f76743247a0f9c9437be Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 24 Oct 2026 19:09:35 +0000 Subject: [PATCH 1/2] doc(Circuit/Boolean): document public declarations and align module docs in Boolean circuit subdirectories (#590) --- .../Circuit/Boolean/ACC0/Basic.lean | 4 ++ .../Boolean/AffineDisperser/Deletion.lean | 2 + .../Boolean/AffineDisperser/Elimination.lean | 4 ++ .../Boolean/AffineDisperser/MinimalAnd.lean | 8 ++- .../Boolean/AffineDisperser/Normal.lean | 3 + .../Boolean/AffineDisperser/Operations.lean | 38 ++++++++++++- .../Boolean/AffineDisperser/Reduction.lean | 12 ++++ .../AffineDisperser/Reparameterisation.lean | 14 ++++- .../Boolean/AffineDisperser/Rewiring.lean | 11 ++++ .../Boolean/AffineDisperser/State.lean | 46 +++++++++++++++- .../Circuit/Boolean/AltFormula/TopDown.lean | 9 +++ .../Boolean/CarryLookahead/PolyTime.lean | 11 +++- .../Circuit/Boolean/CarrySave/PolyTime.lean | 2 + .../Circuit/Boolean/CarrySave/Reduce.lean | 5 ++ .../Boolean/CarrySave/Reduce/PolyTime.lean | 5 ++ .../Circuit/Boolean/Encoding/Certificate.lean | 7 +++ .../Circuit/Boolean/FirstOrder/Parity.lean | 2 + .../Circuit/Boolean/Formula/Andreev.lean | 10 ++++ .../Circuit/Boolean/Formula/Restriction.lean | 32 ++++++++++- .../Boolean/Formula/Subbotovskaya.lean | 6 ++ .../Boolean/HardnessAmplification/Stages.lean | 3 +- .../Boolean/Iteration/AffineController.lean | 1 + .../Boolean/Iteration/CircuitCounting.lean | 2 + .../Boolean/Iteration/CounterBatch.lean | 10 ++++ .../Boolean/Iteration/CounterChart/Basic.lean | 5 ++ .../Iteration/CounterChart/Circuit.lean | 4 ++ .../Iteration/CounterChart/Decode.lean | 6 ++ .../Iteration/CounterChart/Encode.lean | 14 +++++ .../Boolean/Iteration/CounterChart/Time.lean | 2 + .../Circuit/Boolean/Iteration/Decoder.lean | 10 ++++ .../Iteration/ForestCircuitRecords.lean | 21 +++++-- .../Circuit/Boolean/Iteration/InPlace.lean | 10 ++++ .../Circuit/Boolean/Iteration/Label.lean | 19 ++++++- .../Boolean/Iteration/LabelCircuit.lean | 1 + .../Boolean/Iteration/ModulusCounter.lean | 4 ++ .../Iteration/ModulusCounter/Basic.lean | 18 ++++++ .../Iteration/ModulusCounter/Remainders.lean | 6 ++ .../Boolean/Iteration/NavigationWord.lean | 22 +++++++- .../Boolean/Iteration/Optimization.lean | 2 + .../Boolean/Iteration/PrimeCycles.lean | 48 ++++++++++++++-- .../Circuit/Boolean/Iteration/Record.lean | 30 ++++++++-- .../Boolean/Iteration/RecordCircuit.lean | 15 ++++- .../Circuit/Boolean/Iteration/Remainder.lean | 1 + .../Circuit/Boolean/Iteration/Residue.lean | 6 +- .../Circuit/Boolean/Iteration/ResidueAdd.lean | 7 ++- .../Circuit/Boolean/Iteration/Scan.lean | 2 + .../Boolean/Iteration/SharedDictionary.lean | 9 +++ .../Boolean/Iteration/SparseDisplacement.lean | 1 + .../Boolean/Iteration/SparseNavigation.lean | 5 ++ .../Circuit/Boolean/Iteration/SparseTime.lean | 3 + .../Boolean/Iteration/UniversalMap.lean | 5 ++ .../Iteration/VisitScheduleCircuits.lean | 1 + .../Circuit/Boolean/Layered/Compile.lean | 9 +++ .../Circuit/Boolean/Layered/Padding.lean | 9 +++ .../Circuit/Boolean/MassProduction/Basic.lean | 9 ++- .../MassProduction/FineParameters.lean | 4 ++ .../Boolean/MassProduction/FineStatement.lean | 1 + .../MassProduction/Pipeline/Circuit.lean | 10 ++++ .../MassProduction/Scheduler/Basic.lean | 4 ++ .../MassProduction/Scheduler/Phase.lean | 20 ++++++- .../MassProduction/Scheduler/State.lean | 14 ++++- .../Circuit/Boolean/MassProduction/Uhlig.lean | 1 + .../Boolean/MassProduction/Uhlig/Layer.lean | 14 ++++- .../Modular/InnerProduct/PolyTime.lean | 4 ++ .../Boolean/Modular/Multiply/PolyTime.lean | 4 ++ .../Modular/PartialProduct/PolyTime.lean | 5 ++ .../Circuit/Boolean/Modular/Subtract.lean | 3 + .../Boolean/Modular/Subtract/PolyTime.lean | 4 ++ .../Circuit/Boolean/SemiCircuit/Equation.lean | 19 ++++++- .../Circuit/Boolean/SemiCircuit/Gate.lean | 37 ++++++++++++- .../Boolean/SemiCircuit/OfCircuit.lean | 12 +++- .../SemiCircuit/Reparameterisation.lean | 4 +- .../Circuit/Boolean/SemiCircuit/Rewiring.lean | 7 ++- .../Boolean/SemiCircuit/Simplification.lean | 16 +++++- .../Boolean/ShallowSymmetric/ShiftTest.lean | 2 + .../Circuit/Boolean/Smolensky/Gates.lean | 6 ++ .../Circuit/Boolean/Tableau/Basic.lean | 10 +++- .../Circuit/Boolean/Tableau/Layout.lean | 55 ++++++++++++++++--- .../Circuit/Boolean/Tableau/Space.lean | 4 ++ .../Circuit/Boolean/Threshold/Parity.lean | 10 +++- .../Boolean/WeightedThreshold/Activation.lean | 8 ++- .../Boolean/WeightedThreshold/Activity.lean | 2 + .../Boolean/WeightedThreshold/Capacity.lean | 7 ++- .../WeightedThreshold/CapacityCircuit.lean | 7 ++- .../Boolean/WeightedThreshold/Components.lean | 9 +++ .../Boolean/WeightedThreshold/Cut.lean | 1 + .../Boolean/WeightedThreshold/Menus.lean | 14 +++++ .../Boolean/WeightedThreshold/Potential.lean | 14 ++++- .../WeightedThreshold/ScalarActivity.lean | 4 ++ .../WeightedThreshold/TranscriptTree.lean | 2 + 90 files changed, 822 insertions(+), 67 deletions(-) diff --git a/Complexity/Computability/Circuit/Boolean/ACC0/Basic.lean b/Complexity/Computability/Circuit/Boolean/ACC0/Basic.lean index abd4b0c0f..ff58ff1c9 100644 --- a/Complexity/Computability/Circuit/Boolean/ACC0/Basic.lean +++ b/Complexity/Computability/Circuit/Boolean/ACC0/Basic.lean @@ -88,6 +88,7 @@ def modZeroCircuit : (op : ExtOp) → Circuit Unbounded.signature (extSignature. | .ac op => Circuit.oneGate (σ := Unbounded.signature) op id | .gate m => Circuit.oneGate (σ := Unbounded.signature) (.or m) id +/-- `modZeroCircuit op` computes the `AC⁰[0]` operation `op` over the `AC⁰` basis. -/ theorem computes_modZeroCircuit (op : ExtOp) : (modZeroCircuit op).Computes Unbounded.interpretation (single (extInterpretation (modGate 0) op)) := by @@ -112,6 +113,7 @@ def modOneCircuit : (op : ExtOp) → Circuit Unbounded.signature (extSignature.A | .ac op => Circuit.oneGate (σ := Unbounded.signature) op id | .gate _ => constCircuit (Signature.Hom.id _) false +/-- `modOneCircuit op` computes the `AC⁰[1]` operation `op` over the `AC⁰` basis. -/ theorem computes_modOneCircuit (op : ExtOp) : (modOneCircuit op).Computes Unbounded.interpretation (single (extInterpretation (modGate 1) op)) := by @@ -155,6 +157,8 @@ def modMulCircuit (k : ℕ) : (op : ExtOp) → Circuit extSignature (extSignatur | .gate m => Circuit.oneGate (σ := extSignature) (.gate (m * k)) fun j => (finProdFinEquiv.symm j).1 +/-- `modMulCircuit k op` computes the `AC⁰[q]` operation `op` over the `AC⁰[q * k]` basis when +`0 < k`. -/ theorem computes_modMulCircuit (q : ℕ) {k : ℕ} (hk : 0 < k) (op : ExtOp) : (modMulCircuit k op).Computes (extInterpretation (modGate (q * k))) (single (extInterpretation (modGate q) op)) := by diff --git a/Complexity/Computability/Circuit/Boolean/AffineDisperser/Deletion.lean b/Complexity/Computability/Circuit/Boolean/AffineDisperser/Deletion.lean index a1bc43f3e..35495757c 100644 --- a/Complexity/Computability/Circuit/Boolean/AffineDisperser/Deletion.lean +++ b/Complexity/Computability/Circuit/Boolean/AffineDisperser/Deletion.lean @@ -51,6 +51,8 @@ namespace State variable {n : ℕ} {f : BooleanFunction n} +/-- A parameter `p` of degree `1` containing `H` among its children has `{H}` as its set of +children. -/ theorem children_eq_singleton {S : State n} {p : ℕ} {H : ℕ ⊕ ℕ} (h1 : S.deg p = 1) (hH : H ∈ S.children p) : S.children p = {H} := by obtain ⟨a, ha⟩ := Finset.card_eq_one.1 h1 diff --git a/Complexity/Computability/Circuit/Boolean/AffineDisperser/Elimination.lean b/Complexity/Computability/Circuit/Boolean/AffineDisperser/Elimination.lean index ade796a89..549777077 100644 --- a/Complexity/Computability/Circuit/Boolean/AffineDisperser/Elimination.lean +++ b/Complexity/Computability/Circuit/Boolean/AffineDisperser/Elimination.lean @@ -33,6 +33,9 @@ elimination (`State.Valid.step_of_minimalAnd`): * `Cslib.Circuits.Boolean.AffineDisperser.State.SharedSecondChild`, `Cslib.Circuits.Boolean.AffineDisperser.State.Bottleneck`: the configurations of Section 4.3. +* `Cslib.Circuits.Boolean.AffineDisperser.State.IsolatedBelow`, + `Cslib.Circuits.Boolean.AffineDisperser.State.fixInputDeleted`: unpaired isolated parameters + sharing a child with `G` and constraints deleted by fixing an input of `G`. ## Main results @@ -242,6 +245,7 @@ weight when `G` becomes constant. -/ def IsolatedBelow (S : State n) (G u : ℕ) : Prop := u ∈ S.unpaired ∧ S.deg u = 1 ∧ ∃ N ∈ S.children G, N ∈ S.children u +/-- Decidability of `State.IsolatedBelow`. -/ instance (S : State n) (G : ℕ) : DecidablePred (S.IsolatedBelow G) := fun _ => inferInstanceAs (Decidable (_ ∧ _ ∧ _)) diff --git a/Complexity/Computability/Circuit/Boolean/AffineDisperser/MinimalAnd.lean b/Complexity/Computability/Circuit/Boolean/AffineDisperser/MinimalAnd.lean index 8d57bfc13..b4000c0ae 100644 --- a/Complexity/Computability/Circuit/Boolean/AffineDisperser/MinimalAnd.lean +++ b/Complexity/Computability/Circuit/Boolean/AffineDisperser/MinimalAnd.lean @@ -30,7 +30,8 @@ child. ## Main definitions -* `Cslib.Circuits.Boolean.AffineDisperser.State.auxIn`, +* `Cslib.Circuits.Boolean.AffineDisperser.State.auxArgs`, + `Cslib.Circuits.Boolean.AffineDisperser.State.auxIn`, `Cslib.Circuits.Boolean.AffineDisperser.State.childIn`: the measures of the restructuring. * `Cslib.Circuits.Boolean.AffineDisperser.State.MinimalAnd`: the minimal AND. @@ -487,13 +488,17 @@ namespace MinimalAnd variable {S : State n} {G x y : ℕ} +/-- The first input `x` of a minimal AND is a parameter of `S`. -/ theorem mem_params_x (h : S.MinimalAnd G x y) : x ∈ S.params := (mem_unpaired.1 h.unpaired_x).1 +/-- The second input `y` of a minimal AND is a parameter of `S`. -/ theorem mem_params_y (h : S.MinimalAnd G x y) : y ∈ S.params := (mem_unpaired.1 h.unpaired_y).1 +/-- The minimal AND gate `G` is a child of its first input `x`. -/ theorem mem_children_x (h : S.MinimalAnd G x y) : Sum.inl G ∈ S.children x := (SemiCircuit.inl_mem_children _).2 ⟨h.mem, (Gate.reads_of_args h.args).1⟩ +/-- The minimal AND gate `G` is a child of its second input `y`. -/ theorem mem_children_y (h : S.MinimalAnd G x y) : Sum.inl G ∈ S.children y := (SemiCircuit.inl_mem_children _).2 ⟨h.mem, (Gate.reads_of_args h.args).2⟩ @@ -503,6 +508,7 @@ theorem exists_op (h : S.MinimalAnd G x y) : ∃ φ : Bool → Bool → Bool, ¬ obtain ⟨φ, hφ, hG⟩ := Gate.exists_op_of_args h.args exact ⟨φ, fun h' => h.and_op (hφ.1 h'), hG⟩ +/-- No parameter of a valid state is equal to its minimal AND gate `G`. -/ theorem ne_gate (hS : S.Valid f) (h : S.MinimalAnd G x y) {u : ℕ} (hu : u ∈ S.params) : u ≠ G := fun he => hS.wf.notMem_gates_of_mem_params hu (he ▸ h.mem) diff --git a/Complexity/Computability/Circuit/Boolean/AffineDisperser/Normal.lean b/Complexity/Computability/Circuit/Boolean/AffineDisperser/Normal.lean index 976d4eb77..cae54d6cd 100644 --- a/Complexity/Computability/Circuit/Boolean/AffineDisperser/Normal.lean +++ b/Complexity/Computability/Circuit/Boolean/AffineDisperser/Normal.lean @@ -45,6 +45,8 @@ AND-type gate. * `Cslib.Circuits.Boolean.AffineDisperser.State.AndOnIsolated`, `State.DegeneratePair`, `State.PartnersShareChild`, `State.PairInSystem`, `State.AndOnPair`: the configurations of Cases 2 to 6. +* `Cslib.Circuits.Boolean.AffineDisperser.State.Movable`, `State.freshEqn`: affine gates reading + no gates and a fresh equation name for moving them into the affine system. * `Cslib.Circuits.Boolean.AffineDisperser.State.Normal`: normal states. ## Main results @@ -150,6 +152,7 @@ def Movable (S : State n) (J : ℕ) : Prop := def freshEqn (S : State n) : ℕ := S.eqns.sup id + 1 +/-- `S.freshEqn` is not an equation name of `S`. -/ theorem freshEqn_notMem (S : State n) : S.freshEqn ∉ S.eqns := fun h => by have := Finset.le_sup (f := id) h simp only [id, freshEqn] at this diff --git a/Complexity/Computability/Circuit/Boolean/AffineDisperser/Operations.lean b/Complexity/Computability/Circuit/Boolean/AffineDisperser/Operations.lean index 642bcace9..f41ad5c8f 100644 --- a/Complexity/Computability/Circuit/Boolean/AffineDisperser/Operations.lean +++ b/Complexity/Computability/Circuit/Boolean/AffineDisperser/Operations.lean @@ -37,8 +37,9 @@ obligations `State.Transport` (`State.Valid.of_transport`). * `Cslib.Circuits.Boolean.AffineDisperser.State.Transport`: the obligations of transporting validity. -* `Cslib.Circuits.Boolean.AffineDisperser.State.restrict`, `State.deleteGate`, `State.deleteEqn`, - `State.dropEqn`, `State.dropTrivialEqn`: the operations. +* `Cslib.Circuits.Boolean.AffineDisperser.State.restrict`, `State.RestrictOK`, + `State.deleteGate`, `State.deleteEqn`, `State.dropEqn`, `State.dropTrivialEqn`: the operations + and the restriction hypotheses. ## Main results @@ -58,6 +59,8 @@ namespace Cslib.Circuits.Boolean.AffineDisperser open Finset Cslib.BitString SemiCircuit +/-- Evaluating a literal `ℓ` along an affine family of assignments `τ` defines an affine Boolean +function. -/ theorem isAffine_lit_eval {k : ℕ} {τ : BitString k → ℕ → Bool} (hτ : IsAffine τ) (ℓ : Lit) : IsAffine fun u => ℓ.eval (τ u) := by intro u v w @@ -162,21 +165,27 @@ structure RestrictOK (S : State n) (x : ℕ) (ℓ : Lit) (P : Finset (ℕ × ℕ avoid : ∀ pr ∈ P, pr.1 ≠ x ∧ pr.2 ≠ x drop : ∀ pr ∈ S.pairs, pr ∉ P → (pr.1 = x ∨ pr.2 = x) ∧ ∀ y, ℓ.Reads y → y = pr.1 ∨ y = pr.2 +/-- Restricting `x` removes `x` from the parameters of `S`. -/ @[simp] theorem restrict_params (S : State n) (x : ℕ) (ℓ : Lit) (P : Finset (ℕ × ℕ)) : (S.restrict x ℓ P).params = S.params.erase x := rfl +/-- The pairs of `S.restrict x ℓ P` are `P`. -/ @[simp] theorem restrict_pairs (S : State n) (x : ℕ) (ℓ : Lit) (P : Finset (ℕ × ℕ)) : (S.restrict x ℓ P).pairs = P := rfl +/-- The children of `z` in `S.restrict x ℓ P` are its children after substituting `x` with `ℓ`. -/ theorem restrict_children (S : State n) (x : ℕ) (ℓ : Lit) (P : Finset (ℕ × ℕ)) (z : ℕ) : (S.restrict x ℓ P).children z = (S.toSemiCircuit.subst x ℓ).children z := rfl +/-- Restricting a parameter preserves the size of the state. -/ theorem restrict_size (S : State n) (x : ℕ) (ℓ : Lit) (P : Finset (ℕ × ℕ)) : (S.restrict x ℓ P).size = S.size := rfl +/-- Restricting `x` to `ℓ` substitutes `x` with `ℓ` in every gate. -/ @[simp] theorem restrict_gate (S : State n) (x : ℕ) (ℓ : Lit) (P : Finset (ℕ × ℕ)) (J : ℕ) : (S.restrict x ℓ P).gate J = (S.gate J).subst x ℓ := rfl +/-- Restricting `x` to `ℓ` substitutes `x` with `ℓ` in every equation. -/ @[simp] theorem restrict_eqn (S : State n) (x : ℕ) (ℓ : Lit) (P : Finset (ℕ × ℕ)) (e : ℕ) : (S.restrict x ℓ P).eqn e = (S.eqn e).subst x ℓ := rfl @@ -254,24 +263,31 @@ theorem Valid.restrict {S : State n} (hS : S.Valid f) {x : ℕ} {ℓ : Lit} {P : def deleteGate (S : State n) (J : ℕ) (ℓ : Lit) : State n := { S with toSemiCircuit := S.toSemiCircuit.deleteGate J ℓ } +/-- Deleting a gate preserves the parameters of the state. -/ @[simp] theorem deleteGate_params (S : State n) (J : ℕ) (ℓ : Lit) : (S.deleteGate J ℓ).params = S.params := rfl +/-- Deleting a gate preserves the pairs of the state. -/ @[simp] theorem deleteGate_pairs (S : State n) (J : ℕ) (ℓ : Lit) : (S.deleteGate J ℓ).pairs = S.pairs := rfl +/-- Deleting a gate preserves the parameter map `phi`. -/ @[simp] theorem deleteGate_phi (S : State n) (J : ℕ) (ℓ : Lit) : (S.deleteGate J ℓ).phi = S.phi := rfl +/-- Deleting gate `J` with replacement `ℓ` substitutes `J` with `ℓ` in every gate. -/ @[simp] theorem deleteGate_gate (S : State n) (J : ℕ) (ℓ : Lit) (K : ℕ) : (S.deleteGate J ℓ).gate K = (S.gate K).subst J ℓ := rfl +/-- Deleting gate `J` with replacement `ℓ` substitutes `J` with `ℓ` in every equation. -/ @[simp] theorem deleteGate_eqn (S : State n) (J : ℕ) (ℓ : Lit) (e : ℕ) : (S.deleteGate J ℓ).eqn e = (S.eqn e).subst J ℓ := rfl +/-- Deleting gate `J` removes `J` from `S.gates`. -/ @[simp] theorem deleteGate_gates (S : State n) (J : ℕ) (ℓ : Lit) : (S.deleteGate J ℓ).gates = S.gates.erase J := rfl +/-- Deleting a gate decreases the size of the state by `1`. -/ theorem deleteGate_size {S : State n} {J : ℕ} {ℓ : Lit} (h : S.DeleteGateOK J ℓ) : (S.deleteGate J ℓ).size + 1 = S.size := by have := Finset.card_erase_add_one h.mem @@ -279,6 +295,8 @@ theorem deleteGate_size {S : State n} {J : ℕ} {ℓ : Lit} change (S.gates.erase J).card + S.eqns.card + 1 = _ omega +/-- After deleting gate `J` with replacement `ℓ`, the children of `z` are contained in the +children of `z` after substituting `J` with `ℓ` with `.inl J` removed. -/ theorem deleteGate_children_subset {S : State n} {J : ℕ} {ℓ : Lit} (z : ℕ) : (S.deleteGate J ℓ).children z ⊆ ((S.toSemiCircuit.subst J ℓ).children z).erase (.inl J) := by intro w hw @@ -311,15 +329,19 @@ to `ℓ`. -/ def deleteEqn (S : State n) (e v : ℕ) (ℓ : Lit) : State n := { S with toSemiCircuit := S.toSemiCircuit.deleteEqn e v ℓ } +/-- Deleting an equation preserves the parameters of the state. -/ @[simp] theorem deleteEqn_params (S : State n) (e v : ℕ) (ℓ : Lit) : (S.deleteEqn e v ℓ).params = S.params := rfl +/-- Deleting an equation preserves the pairs of the state. -/ @[simp] theorem deleteEqn_pairs (S : State n) (e v : ℕ) (ℓ : Lit) : (S.deleteEqn e v ℓ).pairs = S.pairs := rfl +/-- Deleting an equation preserves the parameter map `phi`. -/ @[simp] theorem deleteEqn_phi (S : State n) (e v : ℕ) (ℓ : Lit) : (S.deleteEqn e v ℓ).phi = S.phi := rfl +/-- Deleting an equation decreases the size of the state by `1`. -/ theorem deleteEqn_size {S : State n} {e v : ℕ} {ℓ : Lit} (h : S.DeleteEqnOK e v ℓ) : (S.deleteEqn e v ℓ).size + 1 = S.size := by have := Finset.card_erase_add_one h.mem @@ -327,6 +349,8 @@ theorem deleteEqn_size {S : State n} {e v : ℕ} {ℓ : Lit} (h : S.DeleteEqnOK change S.gates.card + (S.eqns.erase e).card + 1 = _ omega +/-- After deleting equation `e` and auxiliary variable `v` with replacement `ℓ`, the children of +`z` are contained in the children of `z` after substituting `v` with `ℓ` with `.inr e` removed. -/ theorem deleteEqn_children_subset {S : State n} {e v : ℕ} {ℓ : Lit} (z : ℕ) : (S.deleteEqn e v ℓ).children z ⊆ ((S.toSemiCircuit.subst v ℓ).children z).erase (.inr e) := by intro w hw @@ -338,6 +362,8 @@ theorem deleteEqn_children_subset {S : State n} {e v : ℕ} {ℓ : Lit} (z : ℕ · cases he; exact Finset.notMem_erase e _ hw.1 · exact (SemiCircuit.inr_mem_children _).2 ⟨Finset.mem_of_mem_erase hw.1, hw.2⟩ +/-- Deleting an equation removes it from the children of every parameter other than the target of +`ℓ`. -/ theorem deleteEqn_children_of_ne {S : State n} (hS : S.Valid f) {e v : ℕ} {ℓ : Lit} (h : S.DeleteEqnOK e v ℓ) {z : ℕ} (hz : z ∈ S.params) (hzℓ : ¬ ℓ.Reads z) : (S.deleteEqn e v ℓ).children z ⊆ (S.children z).erase (.inr e) := by @@ -356,10 +382,13 @@ theorem Valid.deleteEqn {S : State n} (hS : S.Valid f) {e v : ℕ} {ℓ : Lit} def dropEqn (S : State n) (e v : ℕ) : State n := { S with toSemiCircuit := S.toSemiCircuit.dropEqn e v } +/-- Dropping an equation preserves the parameters of the state. -/ @[simp] theorem dropEqn_params (S : State n) (e v : ℕ) : (S.dropEqn e v).params = S.params := rfl +/-- Dropping an equation preserves the pairs of the state. -/ @[simp] theorem dropEqn_pairs (S : State n) (e v : ℕ) : (S.dropEqn e v).pairs = S.pairs := rfl +/-- Dropping an equation decreases the size of the state by `1`. -/ theorem dropEqn_size {S : State n} {e v : ℕ} (h : S.DropEqnOK e v) : (S.dropEqn e v).size + 1 = S.size := by have := Finset.card_erase_add_one h.mem @@ -367,6 +396,7 @@ theorem dropEqn_size {S : State n} {e v : ℕ} (h : S.DropEqnOK e v) : change S.gates.card + (S.eqns.erase e).card + 1 = _ omega +/-- Dropping equation `e` removes `.inr e` from the children of `z`. -/ theorem dropEqn_children (S : State n) (e v z : ℕ) : (S.dropEqn e v).children z = (S.children z).erase (.inr e) := by ext (K | e') @@ -387,12 +417,15 @@ theorem Valid.dropEqn {S : State n} (hS : S.Valid f) {e v : ℕ} (h : S.DropEqnO def dropTrivialEqn (S : State n) (e : ℕ) : State n := { S with toSemiCircuit := S.toSemiCircuit.dropTrivialEqn e } +/-- Dropping a trivial equation preserves the parameters of the state. -/ @[simp] theorem dropTrivialEqn_params (S : State n) (e : ℕ) : (S.dropTrivialEqn e).params = S.params := rfl +/-- Dropping a trivial equation preserves the pairs of the state. -/ @[simp] theorem dropTrivialEqn_pairs (S : State n) (e : ℕ) : (S.dropTrivialEqn e).pairs = S.pairs := rfl +/-- Dropping a trivial equation decreases the size of the state by `1`. -/ theorem dropTrivialEqn_size {S : State n} {e : ℕ} (he : e ∈ S.eqns) : (S.dropTrivialEqn e).size + 1 = S.size := by have := Finset.card_erase_add_one he @@ -400,6 +433,7 @@ theorem dropTrivialEqn_size {S : State n} {e : ℕ} (he : e ∈ S.eqns) : change S.gates.card + (S.eqns.erase e).card + 1 = _ omega +/-- Dropping trivial equation `e` removes `.inr e` from the children of `z`. -/ theorem dropTrivialEqn_children (S : State n) (e z : ℕ) : (S.dropTrivialEqn e).children z = (S.children z).erase (.inr e) := by ext (K | e') diff --git a/Complexity/Computability/Circuit/Boolean/AffineDisperser/Reduction.lean b/Complexity/Computability/Circuit/Boolean/AffineDisperser/Reduction.lean index bc660eb07..c3185c2f7 100644 --- a/Complexity/Computability/Circuit/Boolean/AffineDisperser/Reduction.lean +++ b/Complexity/Computability/Circuit/Boolean/AffineDisperser/Reduction.lean @@ -159,6 +159,7 @@ namespace Reduction variable {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} +/-- The empty reduction from a valid state `S` to itself. -/ theorem refl (hS : S.Valid f) : Reduction f S S ∅ [] [] where valid := hS subset := Finset.empty_subset _ @@ -214,20 +215,25 @@ theorem mono (h : Reduction f S S' F D T) {T' : List (ℕ ⊕ ℕ)} (hT : ∀ N /-! ### Accounting -/ +/-- A reduction restricting `F` decreases the number of parameters `m` by `|F|`. -/ theorem m_add (h : Reduction f S S' F D T) : S'.m + F.card = S.m := by unfold m rw [h.params, Finset.card_sdiff_of_subset h.subset] have := Finset.card_le_card h.subset omega +/-- A reduction deleting `D` decreases the size `s` by `|D|`. -/ theorem s_add (h : Reduction f S S' F D T) : S'.s + D.length = S.s := h.size +/-- A reduction restricting `F` decreases the number of pairs `q` by the number of pairs meeting +`F`. -/ theorem q_add (h : Reduction f S S' F D T) : S'.q + (S.pairsMeeting F).card = S.q := by unfold q pairsMeeting rw [h.pairs, add_comm] exact Finset.card_filter_add_card_filter_not _ +/-- Under a reduction restricting `F`, `S'.a + |F| = S.a + (S.pairsMeeting F).card`. -/ theorem a_add (h : Reduction f S S' F D T) (hS : S.Valid f) : S'.a + F.card = S.a + (S.pairsMeeting F).card := by have hm := h.m_add @@ -465,21 +471,27 @@ private theorem restrictOK_fixConst {S : State n} {w : ℕ} (hw : w ∈ S.params push Not at h exact hP (Finset.mem_filter.2 ⟨hpr, h⟩) +/-- Fixing a parameter to a constant preserves validity. -/ theorem Valid.fixConst {S : State n} (hS : S.Valid f) {w : ℕ} (hw : w ∈ S.params) (b : Bool) : (S.fixConst w b).Valid f := hS.restrict (restrictOK_fixConst hw b) +/-- Fixing `w` to a constant removes `w` from `S.params`. -/ @[simp] theorem fixConst_params (S : State n) (w : ℕ) (b : Bool) : (S.fixConst w b).params = S.params.erase w := rfl +/-- Fixing `w` to a constant retains the pairs avoiding `w`. -/ @[simp] theorem fixConst_pairs (S : State n) (w : ℕ) (b : Bool) : (S.fixConst w b).pairs = S.pairsAvoid w := rfl +/-- Fixing a parameter to a constant preserves the size of the state. -/ theorem fixConst_size (S : State n) (w : ℕ) (b : Bool) : (S.fixConst w b).size = S.size := rfl +/-- Fixing `w` to `b` substitutes `w` with `Lit.const b` in every gate. -/ @[simp] theorem fixConst_gate (S : State n) (w : ℕ) (b : Bool) (J : ℕ) : (S.fixConst w b).gate J = (S.gate J).subst w (Lit.const b) := rfl +/-- Fixing `w` to a constant preserves the children of every `z ≠ w`. -/ theorem fixConst_children (S : State n) {w : ℕ} (b : Bool) {z : ℕ} (hz : z ≠ w) : (S.fixConst w b).children z = S.children z := SemiCircuit.children_subst hz (by simp [Lit.const]) diff --git a/Complexity/Computability/Circuit/Boolean/AffineDisperser/Reparameterisation.lean b/Complexity/Computability/Circuit/Boolean/AffineDisperser/Reparameterisation.lean index d1a74b3e8..248af2fab 100644 --- a/Complexity/Computability/Circuit/Boolean/AffineDisperser/Reparameterisation.lean +++ b/Complexity/Computability/Circuit/Boolean/AffineDisperser/Reparameterisation.lean @@ -28,7 +28,10 @@ parameter map is unchanged: ## Main definitions * `Cslib.Circuits.Boolean.AffineDisperser.State.swap`, - `Cslib.Circuits.Boolean.AffineDisperser.State.quad`: the reparameterisations. + `Cslib.Circuits.Boolean.AffineDisperser.State.SwapOK`, + `Cslib.Circuits.Boolean.AffineDisperser.State.quad`, + `Cslib.Circuits.Boolean.AffineDisperser.State.QuadOK`: the reparameterisations and their + hypotheses. ## Main results @@ -69,15 +72,19 @@ structure SwapOK (S : State n) (x Q : ℕ) (c : Bool) (T : Finset ℕ) : Prop wh affine : S.AffineIn Q c T mem_T : x ∈ T +/-- Exchanging `x` and `Q` replaces `x` with `Q` in `S.params`. -/ @[simp] theorem swap_params (S : State n) (x Q : ℕ) (c : Bool) (T : Finset ℕ) : (S.swap x Q c T).params = insert Q (S.params.erase x) := rfl +/-- Exchanging `x` and `Q` preserves the pairs of the state. -/ @[simp] theorem swap_pairs (S : State n) (x Q : ℕ) (c : Bool) (T : Finset ℕ) : (S.swap x Q c T).pairs = S.pairs := rfl +/-- Exchanging `x` and `Q` preserves the size of the state. -/ theorem swap_size (S : State n) (x Q : ℕ) (c : Bool) (T : Finset ℕ) : (S.swap x Q c T).size = S.size := rfl +/-- Exchanging `x` and `Q` preserves the children of every variable. -/ theorem swap_children (S : State n) (x Q : ℕ) (c : Bool) (T : Finset ℕ) (z : ℕ) : (S.swap x Q c T).children z = S.children z := rfl @@ -187,12 +194,15 @@ structure QuadOK (S : State n) (x y z G D : ℕ) (α β γ c : Bool) : Prop unpaired_y : ¬ S.Paired y unpaired_z : ¬ S.Paired z +/-- The quadratic reparameterisation replaces `z` with `D` in `S.params`. -/ @[simp] theorem quad_params (S : State n) (x y z G D : ℕ) (α β γ c : Bool) : (S.quad x y z G D α β γ c).params = insert D (S.params.erase z) := rfl +/-- The quadratic reparameterisation inserts `(x, y)` into `S.pairs`. -/ @[simp] theorem quad_pairs (S : State n) (x y z G D : ℕ) (α β γ c : Bool) : (S.quad x y z G D α β γ c).pairs = insert (x, y) S.pairs := rfl +/-- The quadratic reparameterisation decreases the size of the state by `2`. -/ theorem quad_size {S : State n} {x y z G D : ℕ} {α β γ c : Bool} (h : S.QuadOK x y z G D α β γ c) : (S.quad x y z G D α β γ c).size + 2 = S.size := by have h1 := Finset.card_erase_add_one h.mem_D @@ -201,6 +211,8 @@ theorem quad_size {S : State n} {x y z G D : ℕ} {α β γ c : Bool} change ((S.gates.erase D).erase G).card + S.eqns.card + 2 = _ omega +/-- After the quadratic reparameterisation, the children of `w` are contained in `S.children w` +with `.inl D` and `.inl G` removed. -/ theorem quad_children_subset (S : State n) (x y z G D : ℕ) (α β γ c : Bool) (w : ℕ) : (S.quad x y z G D α β γ c).children w ⊆ ((S.children w).erase (.inl D)).erase (.inl G) := by intro v hv diff --git a/Complexity/Computability/Circuit/Boolean/AffineDisperser/Rewiring.lean b/Complexity/Computability/Circuit/Boolean/AffineDisperser/Rewiring.lean index 3a9072f19..454ee0910 100644 --- a/Complexity/Computability/Circuit/Boolean/AffineDisperser/Rewiring.lean +++ b/Complexity/Computability/Circuit/Boolean/AffineDisperser/Rewiring.lean @@ -57,12 +57,15 @@ equation `e`. -/ def moveAffine (S : State n) (J e : ℕ) : State n := { S with toSemiCircuit := S.toSemiCircuit.moveAffine J e } +/-- Moving an affine gate into the affine system preserves the parameters of the state. -/ @[simp] theorem moveAffine_params (S : State n) (J e : ℕ) : (S.moveAffine J e).params = S.params := rfl +/-- Moving an affine gate into the affine system preserves the pairs of the state. -/ @[simp] theorem moveAffine_pairs (S : State n) (J e : ℕ) : (S.moveAffine J e).pairs = S.pairs := rfl +/-- Moving an affine gate into the affine system preserves the size of the state. -/ theorem moveAffine_size {S : State n} {J e : ℕ} (h : S.MoveOK J e) : (S.moveAffine J e).size = S.size := by have h1 := Finset.card_erase_add_one h.mem @@ -71,6 +74,7 @@ theorem moveAffine_size {S : State n} {J e : ℕ} (h : S.MoveOK J e) : change (S.gates.erase J).card + (insert e S.eqns).card = _ omega +/-- Moving an affine gate into the affine system decreases the number of gates by `1`. -/ theorem moveAffine_gates_card {S : State n} {J e : ℕ} (h : S.MoveOK J e) : (S.moveAffine J e).gates.card + 1 = S.gates.card := Finset.card_erase_add_one h.mem @@ -91,16 +95,22 @@ theorem Valid.moveAffine {S : State n} (hS : S.Valid f) {J e : ℕ} (h : S.MoveO def rewire (S : State n) (J : ℕ) (g : Gate) : State n := { S with toSemiCircuit := S.toSemiCircuit.rewire J g } +/-- Rewiring a gate preserves the parameters of the state. -/ @[simp] theorem rewire_params (S : State n) (J : ℕ) (g : Gate) : (S.rewire J g).params = S.params := rfl +/-- Rewiring a gate preserves the pairs of the state. -/ @[simp] theorem rewire_pairs (S : State n) (J : ℕ) (g : Gate) : (S.rewire J g).pairs = S.pairs := rfl +/-- Rewiring a gate preserves the size of the state. -/ theorem rewire_size (S : State n) (J : ℕ) (g : Gate) : (S.rewire J g).size = S.size := rfl +/-- Rewiring a gate preserves the set of gate names. -/ theorem rewire_gates (S : State n) (J : ℕ) (g : Gate) : (S.rewire J g).gates = S.gates := rfl +/-- A gate `K` is a child of `z` in `S.rewire J g` iff `K ∈ S.gates` and the gate at `K` (which +is `g` when `K = J`) reads `z`. -/ theorem inl_mem_children_rewire (S : State n) (J : ℕ) (g : Gate) (z K : ℕ) : Sum.inl K ∈ (S.rewire J g).children z ↔ K ∈ S.gates ∧ (if K = J then g.Reads z else (S.gate K).Reads z) := by @@ -110,6 +120,7 @@ theorem inl_mem_children_rewire (S : State n) (J : ℕ) (g : Gate) (z K : ℕ) : · subst hKJ; rw [Function.update_self, ite_eq_left rfl] · rw [Function.update_of_ne hKJ, ite_eq_right hKJ] +/-- Rewiring a gate preserves the equation children of every variable. -/ theorem inr_mem_children_rewire (S : State n) (J : ℕ) (g : Gate) (z e : ℕ) : Sum.inr e ∈ (S.rewire J g).children z ↔ Sum.inr e ∈ S.children z := by simp only [SemiCircuit.inr_mem_children] diff --git a/Complexity/Computability/Circuit/Boolean/AffineDisperser/State.lean b/Complexity/Computability/Circuit/Boolean/AffineDisperser/State.lean index 8d70086cd..edfbb59d2 100644 --- a/Complexity/Computability/Circuit/Boolean/AffineDisperser/State.lean +++ b/Complexity/Computability/Circuit/Boolean/AffineDisperser/State.lean @@ -50,14 +50,22 @@ elimination (`State.Step`) is a move to a valid state with smaller `m + s`, `Δa ## Main definitions * `Cslib.Circuits.Boolean.AffineDisperser.State`, - `Cslib.Circuits.Boolean.AffineDisperser.State.Valid`: states. + `Cslib.Circuits.Boolean.AffineDisperser.State.Valid`, + `Cslib.Circuits.Boolean.AffineDisperser.PairTame`: states and tame pairs. +* `Cslib.Circuits.Boolean.AffineDisperser.State.Paired`, + `Cslib.Circuits.Boolean.AffineDisperser.State.unpaired`, + `Cslib.Circuits.Boolean.AffineDisperser.State.wt`: paired and unpaired parameters and their + weights. * `Cslib.Circuits.Boolean.AffineDisperser.State.m`, `q`, `a`, `s`, `W`: the counted quantities and the potential, with `Cslib.Circuits.Boolean.AffineDisperser.weight`. +* `Cslib.Circuits.Boolean.AffineDisperser.State.spread`: spreading bits over a finite set of + names. * `Cslib.Circuits.Boolean.AffineDisperser.State.Step`, `Cslib.Circuits.Boolean.AffineDisperser.State.Preparation`: steps and preparatory operations. * `Cslib.Circuits.Boolean.AffineDisperser.State.IsPartner`, - `Cslib.Circuits.Boolean.AffineDisperser.State.pairsMeeting`: partners and the pairs meeting a - set of parameters. + `Cslib.Circuits.Boolean.AffineDisperser.State.pairsAvoid`, + `Cslib.Circuits.Boolean.AffineDisperser.State.pairsMeeting`: partners and the pairs avoiding a + parameter or meeting a set of parameters. ## Main results @@ -83,19 +91,25 @@ isolated and `7` otherwise (equation (4) of [Mishra and Santhanam][MishraSanthan def weight (k : ℕ) : ℕ := if k = 0 then 0 else if k = 1 then 6 else 7 +/-- The degree weight function `weight` is monotone. -/ theorem weight_mono {k l : ℕ} (h : k ≤ l) : weight k ≤ weight l := by unfold weight; split_ifs <;> omega +/-- Every degree weight `weight k` is at most `7`. -/ theorem weight_le_seven (k : ℕ) : weight k ≤ 7 := by unfold weight; split_ifs <;> omega +/-- An unused parameter (`k = 0`) has weight `0`. -/ @[simp] theorem weight_zero : weight 0 = 0 := rfl +/-- An isolated parameter (`k = 1`) has weight `6`. -/ @[simp] theorem weight_one : weight 1 = 6 := rfl +/-- A parameter of degree `k ≥ 2` has weight `7`. -/ theorem weight_of_two_le {k : ℕ} (hk : 2 ≤ k) : weight k = 7 := by unfold weight; split_ifs <;> omega +/-- A parameter of positive degree (`k ≥ 1`) has weight at least `6`. -/ theorem six_le_weight {k : ℕ} (hk : 1 ≤ k) : 6 ≤ weight k := by unfold weight; split_ifs <;> omega @@ -121,6 +135,7 @@ variable {n : ℕ} (S : State n) def Paired (x : ℕ) : Prop := ∃ pr ∈ S.pairs, pr.1 = x ∨ pr.2 = x +/-- Decidability of `State.Paired`. -/ instance : DecidablePred S.Paired := fun _ => inferInstanceAs (Decidable (∃ pr ∈ S.pairs, _)) @@ -177,20 +192,24 @@ structure Valid (f : BooleanFunction n) : Prop where def spread (F : Finset ℕ) {k : ℕ} (h : F.card = k) (u : BitString k) : ℕ → Bool := fun i => if hi : i ∈ F then u ((F.orderIsoOfFin h).symm ⟨i, hi⟩) else false +/-- Spreading a `k`-bit string over `F` defines an affine family of assignments. -/ theorem isAffine_spread (F : Finset ℕ) {k : ℕ} (h : F.card = k) : IsAffine (spread F h) := by intro u v w funext i simp only [spread, Pi.add_apply] split_ifs <;> rfl +/-- `spread F h u` assigns `false` to every index outside `F`. -/ theorem spread_of_notMem {F : Finset ℕ} {k : ℕ} (h : F.card = k) (u : BitString k) {i : ℕ} (hi : i ∉ F) : spread F h u i = false := by simp [spread, hi] +/-- At the `i`-th element of `F` in increasing order, `spread F h u` equals `u i`. -/ theorem spread_orderIsoOfFin {F : Finset ℕ} {k : ℕ} (h : F.card = k) (u : BitString k) (i : Fin k) : spread F h u (F.orderIsoOfFin h i) = u i := by simp only [spread, Finset.coe_mem, ↓reduceDIte, Subtype.coe_eta, OrderIso.symm_apply_apply] +/-- Two `k`-bit strings whose `spread` assignments agree on `F` are equal. -/ theorem eq_of_spread {F : Finset ℕ} {k : ℕ} (h : F.card = k) {u v : BitString k} (huv : ∀ i ∈ F, spread F h u i = spread F h v i) : u = v := by funext i @@ -377,32 +396,42 @@ otherwise. -/ def wt (S : State n) (x : ℕ) : ℕ := if x ∈ S.unpaired then weight (S.deg x) else 0 +/-- The weight `S.wt x` of any name `x` is at most `7`. -/ theorem wt_le_seven (S : State n) (x : ℕ) : S.wt x ≤ 7 := by unfold wt; split_ifs · exact weight_le_seven _ · omega +/-- A name `x` belongs to `S.unpaired` iff it is an unpaired parameter of `S`. -/ theorem mem_unpaired {S : State n} {x : ℕ} : x ∈ S.unpaired ↔ x ∈ S.params ∧ ¬ S.Paired x := by simp [unpaired] +/-- For an unpaired parameter `x`, `S.wt x` is `weight (S.deg x)`. -/ theorem wt_of_mem {S : State n} {x : ℕ} (hx : x ∈ S.unpaired) : S.wt x = weight (S.deg x) := by simp [wt, hx] +/-- For a name `x` outside `S.unpaired`, `S.wt x = 0`. -/ theorem wt_of_notMem {S : State n} {x : ℕ} (hx : x ∉ S.unpaired) : S.wt x = 0 := by simp [wt, hx] +/-- A paired parameter contributes weight `0`. -/ theorem wt_of_paired {S : State n} {x : ℕ} (hx : S.Paired x) : S.wt x = 0 := wt_of_notMem fun h => (mem_unpaired.1 h).2 hx +/-- A name outside `S.params` contributes weight `0`. -/ theorem wt_of_notMem_params {S : State n} {x : ℕ} (hx : x ∉ S.params) : S.wt x = 0 := wt_of_notMem fun h => hx (mem_unpaired.1 h).1 +/-- Summing `S.wt` over any superset `N` of `S.params` equals the sum of `weight (S.deg x)` over +`S.unpaired`. -/ theorem sum_wt (S : State n) {N : Finset ℕ} (hN : S.params ⊆ N) : ∑ x ∈ N, S.wt x = ∑ x ∈ S.unpaired, weight (S.deg x) := by have hU : S.unpaired ⊆ N := (Finset.filter_subset _ _).trans hN unfold wt rw [Finset.sum_ite_mem, Finset.inter_eq_right.2 hU] +/-- Expressing the potential `S.W` with the weight sum taken over any superset `N` of +`S.params`. -/ theorem W_eq_sum (S : State n) {N : Finset ℕ} (hN : S.params ⊆ N) : S.W = 2 * S.s + 3 * S.q + ∑ x ∈ N, S.wt x := by rw [sum_wt S hN]; rfl @@ -452,6 +481,7 @@ structure Preparation (f : BooleanFunction n) (S S' : State n) : Prop where /-- The potential does not increase. -/ W_le : S'.W ≤ S.W +/-- A preparatory operation preserves `a = m - q`. -/ theorem Preparation.a_eq {S S' : State n} (h : Preparation f S S') : S'.a = S.a := by simp only [a, h.m_eq, h.q_eq] @@ -471,6 +501,7 @@ theorem Step.of_preparation {S S₁ S' : State n} (hp : Preparation f S S₁) (h def IsPartner (S : State n) (w r : ℕ) : Prop := ∃ pr ∈ S.pairs, (pr.1 = w ∧ pr.2 = r) ∨ (pr.2 = w ∧ pr.1 = r) +/-- Decidability of `State.IsPartner`. -/ instance (S : State n) (w : ℕ) : DecidablePred (S.IsPartner w) := fun _ => inferInstanceAs (Decidable (∃ pr ∈ S.pairs, _)) @@ -482,15 +513,18 @@ def pairsAvoid (S : State n) (w : ℕ) : Finset (ℕ × ℕ) := def pairsMeeting (S : State n) (F : Finset ℕ) : Finset (ℕ × ℕ) := S.pairs.filter fun pr => pr.1 ∈ F ∨ pr.2 ∈ F +/-- Two states with the same pairs have the same paired names. -/ theorem paired_congr {S S' : State n} (h : S'.pairs = S.pairs) {x : ℕ} : S'.Paired x ↔ S.Paired x := by unfold Paired; rw [h] +/-- Two states with the same parameters and pairs have the same unpaired parameters. -/ theorem unpaired_congr {S S' : State n} (hp : S'.params = S.params) (h : S'.pairs = S.pairs) : S'.unpaired = S.unpaired := by ext x rw [mem_unpaired, mem_unpaired, hp, paired_congr h] +/-- Every paired name of a valid state is a parameter. -/ theorem Valid.mem_params_of_paired {S : State n} (hS : S.Valid f) {p : ℕ} (hp : S.Paired p) : p ∈ S.params := by obtain ⟨pr, hpr, h | h⟩ := hp @@ -505,26 +539,31 @@ theorem Valid.pair_unique {S : State n} (hS : S.Valid f) {w : ℕ} {pr pr' : ℕ have := hS.pairs_disjoint pr hpr pr' hpr' hne rcases h with rfl | rfl <;> rcases h' with h' | h' <;> tauto +/-- Every paired parameter has a partner. -/ theorem exists_partner {S : State n} {p : ℕ} (hp : S.Paired p) : ∃ r, S.IsPartner p r := by obtain ⟨pr, hpr, h | h⟩ := hp · exact ⟨pr.2, pr, hpr, Or.inl ⟨h, rfl⟩⟩ · exact ⟨pr.1, pr, hpr, Or.inr ⟨h, rfl⟩⟩ +/-- The partner relation `State.IsPartner` is symmetric. -/ theorem IsPartner.symm {S : State n} {p r : ℕ} (h : S.IsPartner p r) : S.IsPartner r p := by obtain ⟨pr, hpr, h⟩ := h exact ⟨pr, hpr, by tauto⟩ +/-- A parameter that has a partner is paired. -/ theorem IsPartner.paired {S : State n} {w r : ℕ} (h : S.IsPartner w r) : S.Paired w := by obtain ⟨pr, hpr, ⟨h1, -⟩ | ⟨h1, -⟩⟩ := h · exact ⟨pr, hpr, Or.inl h1⟩ · exact ⟨pr, hpr, Or.inr h1⟩ +/-- In a valid state, a parameter is distinct from its partner. -/ theorem Valid.partner_ne {S : State n} (hS : S.Valid f) {p r : ℕ} (h : S.IsPartner p r) : r ≠ p := by obtain ⟨pr, hpr, ⟨h1, h2⟩ | ⟨h1, h2⟩⟩ := h · rw [← h1, ← h2]; exact (hS.pair_mem pr hpr).2.2.symm · rw [← h1, ← h2]; exact (hS.pair_mem pr hpr).2.2 +/-- In a valid state, the partner of a parameter is a parameter. -/ theorem Valid.partner_mem {S : State n} (hS : S.Valid f) {p r : ℕ} (h : S.IsPartner p r) : r ∈ S.params := hS.mem_params_of_paired h.symm.paired @@ -606,6 +645,7 @@ theorem Valid.card_pairsMeeting_le {S : State n} (hS : S.Valid f) (F : Finset (by split_ifs <;> simp) ?_ rw [h]; split_ifs <;> simp +/-- The number of pairs meeting `{w}` is `1` if `w` is paired and `0` otherwise. -/ theorem Valid.card_pairsMeeting_singleton {S : State n} (hS : S.Valid f) (w : ℕ) : (S.pairsMeeting {w}).card = if S.Paired w then 1 else 0 := by split_ifs with hw diff --git a/Complexity/Computability/Circuit/Boolean/AltFormula/TopDown.lean b/Complexity/Computability/Circuit/Boolean/AltFormula/TopDown.lean index 885ee3dee..b30dd8b8d 100644 --- a/Complexity/Computability/Circuit/Boolean/AltFormula/TopDown.lean +++ b/Complexity/Computability/Circuit/Boolean/AltFormula/TopDown.lean @@ -27,6 +27,10 @@ for parity or majority have `S + 2 n + 1 > 2 ^ (ε n ^ (1 / (d - 1)))` for large ## Main definitions +* `Cslib.Circuits.Boolean.AltFormula.speaker`, `Cslib.Circuits.Boolean.AltFormula.witness`, + `Cslib.Circuits.Boolean.AltFormula.childIndex`, + `Cslib.Circuits.Boolean.AltFormula.childLiteral`: the speaker, witness bit, and selected child + or literal at a gate layer. * `Cslib.Circuits.Boolean.AltFormula.kwProtocol`: the Karchmer–Wigderson protocol of an alternating formula. @@ -92,6 +96,8 @@ def kwProtocol (S : ℕ) (i₀ : Fin n) : else .output i₀ | .inr _ => .output i₀ +/-- When some child of `fs` evaluates to `b` on `x`, `childIndex op fs b x` is the index of a +child evaluating to `b`. -/ theorem childIndex_spec {d : ℕ} {op : AltOp} {fs : List (AltFormula n d)} {b : Bool} {x : BitString n} (h : ∃ j : Fin fs.length, eval op (fs.get j) x = b) : ∃ j : Fin fs.length, childIndex op fs b x = j ∧ eval op (fs.get j) x = b := by @@ -102,6 +108,8 @@ theorem childIndex_spec {d : ℕ} {op : AltOp} {fs : List (AltFormula n d)} {b : exact absurd hj (by simpa using Fin.find?_eq_none_iff.1 hf j) | some j => exact ⟨j, rfl, by simpa using Fin.eq_true_of_find?_eq_some hf⟩ +/-- When some literal of `ls` evaluates to `b` on `x`, `childLiteral i₀ ls b x` is a literal in +`ls` evaluating to `b`. -/ theorem childLiteral_spec {i₀ : Fin n} {ls : List (Literal (Fin n))} {b : Bool} {x : BitString n} (h : ∃ l ∈ ls, Literal.eval x l = b) : childLiteral i₀ ls b x ∈ ls ∧ Literal.eval x (childLiteral i₀ ls b x) = b := by @@ -113,6 +121,7 @@ theorem childLiteral_spec {i₀ : Fin n} {ls : List (Literal (Fin n))} {b : Bool | some l => exact ⟨List.mem_of_find?_eq_some hf, by simpa using List.find?_some hf⟩ +/-- Every alternating formula of positive depth `d + 1` has at least `1` gate. -/ theorem one_le_size {d : ℕ} (f : AltFormula n (d + 1)) : 1 ≤ size f := by simp [size] diff --git a/Complexity/Computability/Circuit/Boolean/CarryLookahead/PolyTime.lean b/Complexity/Computability/Circuit/Boolean/CarryLookahead/PolyTime.lean index 0e2c66976..355b58465 100644 --- a/Complexity/Computability/Circuit/Boolean/CarryLookahead/PolyTime.lean +++ b/Complexity/Computability/Circuit/Boolean/CarryLookahead/PolyTime.lean @@ -26,7 +26,16 @@ justify the loop, including tags, delimiters and output references. ## Main definitions -* `Cslib.Circuits.Boolean.CarryLookahead.stepCode`: one round on raw parameters. +* `Cslib.Circuits.Boolean.CarryLookahead.neighbourIndex`, + `Cslib.Circuits.Boolean.CarryLookahead.generateCode`, + `Cslib.Circuits.Boolean.CarryLookahead.propagateCode`, + `Cslib.Circuits.Boolean.CarryLookahead.stepCode`: one round on raw parameters. +* `Cslib.Circuits.Boolean.CarryLookahead.initialGenerateCode`, + `Cslib.Circuits.Boolean.CarryLookahead.initialPropagateCode`, + `Cslib.Circuits.Boolean.CarryLookahead.initialCode`, + `Cslib.Circuits.Boolean.CarryLookahead.sumCode`, + `Cslib.Circuits.Boolean.CarryLookahead.finishCode`: initial generate/propagate, sum, and + finishing codes. ## Main results diff --git a/Complexity/Computability/Circuit/Boolean/CarrySave/PolyTime.lean b/Complexity/Computability/Circuit/Boolean/CarrySave/PolyTime.lean index 309bb78c8..5d0b13e40 100644 --- a/Complexity/Computability/Circuit/Boolean/CarrySave/PolyTime.lean +++ b/Complexity/Computability/Circuit/Boolean/CarrySave/PolyTime.lean @@ -26,6 +26,8 @@ charge the full code and hold uniformly at every width, including zero. ## Main definitions +* `Cslib.Circuits.Boolean.csaSumCode`, `Cslib.Circuits.Boolean.csaCarryCode`: raw code templates + for sum and carry bits. * `Cslib.Circuits.Boolean.csa3to2Code`: raw code generation for the three-to-two reducer. * `Cslib.Circuits.Boolean.csa4to2Code`: raw code generation for the four-to-two reducer. diff --git a/Complexity/Computability/Circuit/Boolean/CarrySave/Reduce.lean b/Complexity/Computability/Circuit/Boolean/CarrySave/Reduce.lean index 3b0a8224f..48555522b 100644 --- a/Complexity/Computability/Circuit/Boolean/CarrySave/Reduce.lean +++ b/Complexity/Computability/Circuit/Boolean/CarrySave/Reduce.lean @@ -18,6 +18,7 @@ These are the arithmetic reductions used by modular multiplication and GSW's sel ## Main definitions +* `Cslib.Circuits.Boolean.pairWithZero`: put an ordinary word into carry-save form. * `Cslib.Circuits.Boolean.reducePairs`: balanced four-to-two reduction on shared inputs. * `Cslib.Circuits.Boolean.sumPairs`: reduction followed by logarithmic-depth addition. @@ -46,21 +47,25 @@ def pairWithZero (C : Circuit signature n w) : Circuit signature n (w + w) := C.append ((Circuit.wiring signature (fun _ : Fin w => (0 : Fin 1))).comp (Circuit.oneGate (.const false) Fin.elim0)) +/-- Evaluating `pairWithZero C` appends `w` false bits to the output of `C`. -/ @[simp] theorem eval_pairWithZero (C : Circuit signature n w) (x : BitString n) : (pairWithZero C).eval interpretation x = Fin.append (C.eval interpretation x) (fun _ => false) := by simp only [pairWithZero, Circuit.eval_append, Circuit.eval_comp, Circuit.eval_wiring] rfl +/-- The carry-save value `pairVal` of `pairWithZero C` equals the unsigned value of `C`. -/ theorem pairVal_eval_pairWithZero (C : Circuit signature n w) (x : BitString n) : pairVal ((pairWithZero C).eval interpretation x) = (BitString.equivFin w (C.eval interpretation x) : ℕ) := by rw [eval_pairWithZero, pairVal_append, val_equivFin_false, Nat.add_zero] +/-- `pairWithZero C` adds one shared constant gate to `C`. -/ @[simp] theorem size_pairWithZero (C : Circuit signature n w) : (pairWithZero C).size = C.size + 1 := by simp [pairWithZero] +/-- The depth of `pairWithZero C` is at most `max C.depth 1`. -/ theorem depth_pairWithZero_le (C : Circuit signature n w) : (pairWithZero C).depth ≤ max C.depth 1 := by refine (Circuit.depth_append_le _ _).trans (max_le_max le_rfl ?_) diff --git a/Complexity/Computability/Circuit/Boolean/CarrySave/Reduce/PolyTime.lean b/Complexity/Computability/Circuit/Boolean/CarrySave/Reduce/PolyTime.lean index e90e472a7..cabc2edc1 100644 --- a/Complexity/Computability/Circuit/Boolean/CarrySave/Reduce/PolyTime.lean +++ b/Complexity/Computability/Circuit/Boolean/CarrySave/Reduce/PolyTime.lean @@ -24,6 +24,11 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Na The generator preserves the complete half-split reducer, its zero fallback and the final adder. Input counts and references are binary, word widths unary, and all supplied leaf code is charged. +## Main definitions + +* `Cslib.Circuits.Boolean.pairWithZeroCode`, `Cslib.Circuits.Boolean.sumPairsCode`: raw code + generators for `pairWithZero` and `sumPairs`. + ## Main results * `Cslib.Circuits.Boolean.sumPairsCode_eq_code`: exact reduction and final-adder code. diff --git a/Complexity/Computability/Circuit/Boolean/Encoding/Certificate.lean b/Complexity/Computability/Circuit/Boolean/Encoding/Certificate.lean index f2eaa629a..abdad5287 100644 --- a/Complexity/Computability/Circuit/Boolean/Encoding/Certificate.lean +++ b/Complexity/Computability/Circuit/Boolean/Encoding/Certificate.lean @@ -39,6 +39,8 @@ polynomial-time test `codeCheck` tells the codes of circuits apart (`codeCheck_e ## Main definitions +* `Cslib.Circuits.Boolean.Op.ofBits`, `Cslib.Circuits.Boolean.gateRow`, + `Cslib.Circuits.Boolean.readRow`: 3-bit operation decoding and gate row encoding/decoding. * `Cslib.Circuits.Boolean.certLength`: the length of certificates. * `Cslib.Circuits.Boolean.certificate`: the certificate of a circuit code. * `Cslib.Circuits.Boolean.readCertificate`: the gates and the output wire read from a certificate. @@ -72,10 +74,12 @@ open Turing.MultiTapeTM def unaryField (width a : ℕ) : List Bool := List.replicate a true ++ List.replicate (width - a) false +/-- A unary field of width `width` for `a ≤ width` has length `width`. -/ @[simp] theorem length_unaryField (width a : ℕ) (h : a ≤ width) : (unaryField width a).length = width := by simp [unaryField, h] +/-- A unary field of width `width` for `a` contains `a` ones. -/ @[simp] theorem count_unaryField (width a : ℕ) : (unaryField width a).count true = a := by simp [unaryField, List.count_replicate] @@ -87,6 +91,7 @@ def Op.bits : Op → List Bool | .and => [true, true, false] | .or => [false, false, true] +/-- The 3-bit encoding `op.bits` has length `3`. -/ @[simp] theorem Op.length_bits (op : Op) : op.bits.length = 3 := by cases op with | const b => cases b <;> rfl @@ -99,6 +104,7 @@ def Op.ofBits : Bool × Bool × Bool → Op | (true, true, false) => .and | (_, _, true) => .or +/-- Decoding the three bits of `op.bits` via `Op.ofBits` recovers `op`. -/ theorem Op.ofBits_bits (op : Op) : Op.ofBits (op.bits.getD 0 false, op.bits.getD 1 false, op.bits.getD 2 false) = op := by cases op with @@ -262,6 +268,7 @@ private theorem all_zipIdx_eq_true_iff {n : ℕ} (k : ℕ) (gates : List (Op × rw [List.zipIdx_cons, List.all_cons, Bool.and_eq_true, ih, Program.isCodeFrom_cons] simp +/-- `codeCheck n gates` returns `true` iff `gates` is a valid program code on `n` inputs. -/ theorem codeCheck_eq_true_iff {n : ℕ} {gates : List (Op × List ℕ)} : codeCheck n gates = true ↔ Program.IsCodeFrom signature n 0 gates := all_zipIdx_eq_true_iff 0 gates diff --git a/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean b/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean index c6c8e2eb1..aa59154d9 100644 --- a/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean +++ b/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean @@ -87,6 +87,8 @@ namespace Expansion variable {P : L.Relations 1} {N : L.Structure (Fin n)} {S : Finset (Fin n)} open Classical in +/-- The `L`-structure on `Expansion P N S` interpreting `P` as `S` and all other relations as in +`N`. -/ instance : L.Structure (Expansion P N S) where funMap f := isEmptyElim f RelMap {l} R t := diff --git a/Complexity/Computability/Circuit/Boolean/Formula/Andreev.lean b/Complexity/Computability/Circuit/Boolean/Formula/Andreev.lean index c389169cc..9dfa1f217 100644 --- a/Complexity/Computability/Circuit/Boolean/Formula/Andreev.lean +++ b/Complexity/Computability/Circuit/Boolean/Formula/Andreev.lean @@ -105,6 +105,7 @@ def andreev (b m : ℕ) : BooleanFunction (2 ^ b + b * m) := fun w => w (andreevTableIndex b m (BitString.equivFin b fun j => parity m fun t => w (andreevBlockVar b m j t))) +/-- Within each block `j`, the block variable map `andreevBlockVar b m j` is injective. -/ theorem andreevBlockVar_injective (b m : ℕ) (j : Fin b) : Function.Injective (andreevBlockVar b m j) := by intro t₁ t₂ h @@ -112,6 +113,7 @@ theorem andreevBlockVar_injective (b m : ℕ) (j : Fin b) : have h2 := finProdFinEquiv.injective h1 exact (Prod.ext_iff.1 h2).2 +/-- Each parity block `andreevBlock b m j` has cardinality `m`. -/ @[simp] theorem card_andreevBlock (b m : ℕ) (j : Fin b) : #(andreevBlock b m j) = m := by rw [andreevBlock, card_image_of_injective _ (andreevBlockVar_injective b m j), card_univ, @@ -123,16 +125,21 @@ def andreevFixTable (b m : ℕ) (h : BooleanFunction b) : PartialAssignment (Fin (2 ^ b + b * m)) := Fin.addCases (fun idx => some (h ((BitString.equivFin b).symm idx))) (fun _ => none) +/-- `andreevFixTable b m h` fixes the `idx`-th truth-table coordinate to the value of `h` at +`idx`. -/ @[simp] theorem andreevFixTable_tableIndex (b m : ℕ) (h : BooleanFunction b) (idx : Fin (2 ^ b)) : andreevFixTable b m h (andreevTableIndex b m idx) = some (h ((BitString.equivFin b).symm idx)) := by simp [andreevFixTable, andreevTableIndex] +/-- `andreevFixTable b m h` leaves every coordinate past the first `2 ^ b` truth-table bits +free. -/ @[simp] theorem andreevFixTable_natAdd (b m : ℕ) (h : BooleanFunction b) (u : Fin (b * m)) : andreevFixTable b m h (Fin.natAdd (2 ^ b) u) = none := by simp [andreevFixTable] +/-- `andreevFixTable b m h` leaves every block variable `andreevBlockVar b m j t` free. -/ @[simp] theorem andreevFixTable_blockVar (b m : ℕ) (h : BooleanFunction b) (j : Fin b) (t : Fin m) : andreevFixTable b m h (andreevBlockVar b m j t) = none := by @@ -148,11 +155,14 @@ private theorem free_andreevFixTable (b m : ℕ) (h : BooleanFunction b) : · rintro ⟨u, rfl⟩ exact andreevFixTable_natAdd b m h u +/-- `andreevFixTable b m h` has `b * m` free variables. -/ @[simp] theorem card_free_andreevFixTable (b m : ℕ) (h : BooleanFunction b) : #(andreevFixTable b m h).free = b * m := by rw [free_andreevFixTable, card_image_of_injective _ (Fin.natAdd_injective (b * m) (2 ^ b)), card_univ, Fintype.card_fin] +/-- Every parity block `andreevBlock b m j` is contained in the free variables of +`andreevFixTable b m h`. -/ theorem andreevBlock_subset_free_andreevFixTable (b m : ℕ) (h : BooleanFunction b) (j : Fin b) : andreevBlock b m j ⊆ (andreevFixTable b m h).free := by intro i hi diff --git a/Complexity/Computability/Circuit/Boolean/Formula/Restriction.lean b/Complexity/Computability/Circuit/Boolean/Formula/Restriction.lean index ae74be795..b49bbe7e6 100644 --- a/Complexity/Computability/Circuit/Boolean/Formula/Restriction.lean +++ b/Complexity/Computability/Circuit/Boolean/Formula/Restriction.lean @@ -33,8 +33,9 @@ with at most `3 L(f) - 2` operation nodes, or a constant (`Boolean.exists_comput ## Main definitions -* `Cslib.Circuits.Formula.mkNot`, `Cslib.Circuits.Formula.mkAnd`, `Cslib.Circuits.Formula.mkOr`: - negation, conjunction and disjunction, simplifying constants and double negations. +* `Cslib.Circuits.Formula.constValue?`, `Cslib.Circuits.Formula.mkNot`, + `Cslib.Circuits.Formula.mkAnd`, `Cslib.Circuits.Formula.mkOr`: constant inspection and negation, + conjunction and disjunction simplifying constants and double negations. * `Cslib.Circuits.Formula.restrict`: the restriction of a formula by a partial assignment. * `Cslib.Circuits.Formula.IsSimplified`: formulas without constants or double negations. * `Cslib.Circuits.Boolean.formulaSize`: the least leaf size of a De Morgan formula computing a @@ -77,6 +78,7 @@ def constValue? : Formula signature n → Option Bool | gate (.const b) _ => some b | _ => none +/-- `constValue?` of a constant formula `const b` is `some b`. -/ @[simp] theorem constValue?_const (b : Bool) : (const b : Formula signature n).constValue? = some b := rfl @@ -144,23 +146,29 @@ theorem gate_or_eq (args : Fin (signature.Arity Op.or) → Formula signature n) funext j fin_cases j <;> rfl +/-- `mkNot` of a constant `const b` is `const (!b)`. -/ @[simp] theorem mkNot_const (b : Bool) : mkNot (const b : Formula signature n) = const (!b) := rfl +/-- `mkNot` cancels a double negation. -/ @[simp] theorem mkNot_not (F : Formula signature n) : mkNot F.not = F := rfl +/-- `mkNot` of an input leaf is its negation. -/ @[simp] theorem mkNot_input (i : Fin n) : mkNot (input i : Formula signature n) = (input i).not := rfl +/-- `mkNot` of a conjunction is its negation. -/ @[simp] theorem mkNot_and (F G : Formula signature n) : mkNot (F.and G) = (F.and G).not := rfl +/-- `mkNot` of a disjunction is its negation. -/ @[simp] theorem mkNot_or (F G : Formula signature n) : mkNot (F.or G) = (F.or G).not := rfl variable (x : BitString n) +/-- `mkNot F` evaluates to the negation of `F`. -/ @[simp] theorem eval_mkNot (F : Formula signature n) : (mkNot F).eval interpretation x = !F.eval interpretation x := by cases F with @@ -173,6 +181,7 @@ variable (x : BitString n) | and => rw [gate_and_eq, mkNot_and, eval_not] | or => rw [gate_or_eq, mkNot_or, eval_not] +/-- `mkNot` preserves leaf size. -/ @[simp] theorem leafSize_mkNot (F : Formula signature n) : (mkNot F).leafSize = F.leafSize := by cases F with | input i => rfl @@ -183,55 +192,67 @@ variable (x : BitString n) | and => rw [gate_and_eq, mkNot_and, leafSize_not] | or => rw [gate_or_eq, mkNot_or, leafSize_not] +/-- `mkAnd F G` evaluates to the conjunction of `F` and `G`. -/ @[simp] theorem eval_mkAnd (F G : Formula signature n) : (mkAnd F G).eval interpretation x = (F.eval interpretation x && G.eval interpretation x) := by rcases eq_const_or_constValue?_eq_none F with ⟨_ | _, rfl⟩ | hF <;> rcases eq_const_or_constValue?_eq_none G with ⟨_ | _, rfl⟩ | hG <;> simp_all [mkAnd] +/-- `mkOr F G` evaluates to the disjunction of `F` and `G`. -/ @[simp] theorem eval_mkOr (F G : Formula signature n) : (mkOr F G).eval interpretation x = (F.eval interpretation x || G.eval interpretation x) := by rcases eq_const_or_constValue?_eq_none F with ⟨_ | _, rfl⟩ | hF <;> rcases eq_const_or_constValue?_eq_none G with ⟨_ | _, rfl⟩ | hG <;> simp_all [mkOr] +/-- The leaf size of `mkAnd F G` is at most `F.leafSize + G.leafSize`. -/ theorem leafSize_mkAnd_le (F G : Formula signature n) : (mkAnd F G).leafSize ≤ F.leafSize + G.leafSize := by rcases eq_const_or_constValue?_eq_none F with ⟨_ | _, rfl⟩ | hF <;> rcases eq_const_or_constValue?_eq_none G with ⟨_ | _, rfl⟩ | hG <;> simp_all [mkAnd] +/-- The leaf size of `mkOr F G` is at most `F.leafSize + G.leafSize`. -/ theorem leafSize_mkOr_le (F G : Formula signature n) : (mkOr F G).leafSize ≤ F.leafSize + G.leafSize := by rcases eq_const_or_constValue?_eq_none F with ⟨_ | _, rfl⟩ | hF <;> rcases eq_const_or_constValue?_eq_none G with ⟨_ | _, rfl⟩ | hG <;> simp_all [mkOr] +/-- `mkAnd` with `const false` on the left simplifies to `const false`. -/ @[simp] theorem mkAnd_const_false_left (G : Formula signature n) : mkAnd (const false) G = const false := rfl +/-- `mkAnd` with `const true` on the left simplifies to the right argument. -/ @[simp] theorem mkAnd_const_true_left (G : Formula signature n) : mkAnd (const true) G = G := rfl +/-- `mkAnd` with `const false` on the right simplifies to `const false`. -/ @[simp] theorem mkAnd_const_false_right (F : Formula signature n) : mkAnd F (const false) = const false := by rcases eq_const_or_constValue?_eq_none F with ⟨_ | _, rfl⟩ | hF <;> simp_all [mkAnd] +/-- `mkAnd` with `const true` on the right simplifies to the left argument. -/ @[simp] theorem mkAnd_const_true_right (F : Formula signature n) : mkAnd F (const true) = F := by rcases eq_const_or_constValue?_eq_none F with ⟨_ | _, rfl⟩ | hF <;> simp_all [mkAnd] +/-- `mkOr` with `const true` on the left simplifies to `const true`. -/ @[simp] theorem mkOr_const_true_left (G : Formula signature n) : mkOr (const true) G = const true := rfl +/-- `mkOr` with `const false` on the left simplifies to the right argument. -/ @[simp] theorem mkOr_const_false_left (G : Formula signature n) : mkOr (const false) G = G := rfl +/-- `mkOr` with `const true` on the right simplifies to `const true`. -/ @[simp] theorem mkOr_const_true_right (F : Formula signature n) : mkOr F (const true) = const true := by rcases eq_const_or_constValue?_eq_none F with ⟨_ | _, rfl⟩ | hF <;> simp_all [mkOr] +/-- `mkOr` with `const false` on the right simplifies to the left argument. -/ @[simp] theorem mkOr_const_false_right (F : Formula signature n) : mkOr F (const false) = F := by rcases eq_const_or_constValue?_eq_none F with ⟨_ | _, rfl⟩ | hF <;> simp_all [mkOr] @@ -248,21 +269,27 @@ def restrict (ρ : PartialAssignment (Fin n)) : Formula signature n → Formula variable (ρ : PartialAssignment (Fin n)) +/-- Restricting an input leaf `input i` by `ρ` yields `const b` if `ρ i = some b` and `input i` +otherwise. -/ @[simp] theorem restrict_input (i : Fin n) : (input i : Formula signature n).restrict ρ = (ρ i).elim (input i) const := rfl +/-- Restricting a constant formula `const b` leaves it unchanged. -/ @[simp] theorem restrict_const (b : Bool) : (const b : Formula signature n).restrict ρ = const b := rfl +/-- Restricting a negation applies `mkNot` to the restricted argument. -/ @[simp] theorem restrict_not (F : Formula signature n) : F.not.restrict ρ = mkNot (F.restrict ρ) := rfl +/-- Restricting a conjunction applies `mkAnd` to the restricted arguments. -/ @[simp] theorem restrict_and (F G : Formula signature n) : (F.and G).restrict ρ = mkAnd (F.restrict ρ) (G.restrict ρ) := rfl +/-- Restricting a disjunction applies `mkOr` to the restricted arguments. -/ @[simp] theorem restrict_or (F G : Formula signature n) : (F.or G).restrict ρ = mkOr (F.restrict ρ) (G.restrict ρ) := rfl @@ -347,6 +374,7 @@ inductive IsSimplified : Formula signature n → Prop | not_or {F G : Formula signature n} : F.IsSimplified → G.IsSimplified → (F.or G).not.IsSimplified +/-- A simplified formula is not a constant (`constValue? = none`). -/ theorem IsSimplified.constValue?_eq_none {F : Formula signature n} (hF : F.IsSimplified) : F.constValue? = none := by cases hF <;> rfl diff --git a/Complexity/Computability/Circuit/Boolean/Formula/Subbotovskaya.lean b/Complexity/Computability/Circuit/Boolean/Formula/Subbotovskaya.lean index 113b0dd70..4bcdd7931 100644 --- a/Complexity/Computability/Circuit/Boolean/Formula/Subbotovskaya.lean +++ b/Complexity/Computability/Circuit/Boolean/Formula/Subbotovskaya.lean @@ -82,6 +82,7 @@ namespace Formula def restrictAt (i : Fin n) (b : Bool) (F : Formula signature n) : Formula signature n := F.restrict (update PartialAssignment.empty i (some b)) +/-- Evaluating `F.restrictAt i b` at `x` equals evaluating `F` at `update x i b`. -/ @[simp] theorem eval_restrictAt (i : Fin n) (b : Bool) (F : Formula signature n) (x : BitString n) : (F.restrictAt i b).eval interpretation x = F.eval interpretation (update x i b) := by @@ -92,22 +93,27 @@ private theorem leafSize_restrictAt_add_leafSizeIn_le (F : Formula signature n) (F.restrictAt i b).leafSize + F.leafSizeIn {i} ≤ F.leafSize := leafSize_restrict_update_le F i b +/-- Restricting a constant formula `const c` at input `i` leaves it unchanged. -/ @[simp] theorem restrictAt_const (i : Fin n) (b c : Bool) : (const c : Formula signature n).restrictAt i b = const c := rfl +/-- Restricting a negation at input `i` applies `mkNot` to the restricted argument. -/ @[simp] theorem restrictAt_not (i : Fin n) (b : Bool) (F : Formula signature n) : F.not.restrictAt i b = mkNot (F.restrictAt i b) := rfl +/-- Restricting a conjunction at input `i` applies `mkAnd` to the restricted arguments. -/ @[simp] theorem restrictAt_and (i : Fin n) (b : Bool) (F G : Formula signature n) : (F.and G).restrictAt i b = mkAnd (F.restrictAt i b) (G.restrictAt i b) := rfl +/-- Restricting a disjunction at input `i` applies `mkOr` to the restricted arguments. -/ @[simp] theorem restrictAt_or (i : Fin n) (b : Bool) (F G : Formula signature n) : (F.or G).restrictAt i b = mkOr (F.restrictAt i b) (G.restrictAt i b) := rfl +/-- Restricting `input i` at input `i` to `b` yields `const b`. -/ theorem restrictAt_input_self (i : Fin n) (b : Bool) : (input i : Formula signature n).restrictAt i b = const b := by simp [restrictAt] diff --git a/Complexity/Computability/Circuit/Boolean/HardnessAmplification/Stages.lean b/Complexity/Computability/Circuit/Boolean/HardnessAmplification/Stages.lean index 67c7e314a..7f62f3979 100644 --- a/Complexity/Computability/Circuit/Boolean/HardnessAmplification/Stages.lean +++ b/Complexity/Computability/Circuit/Boolean/HardnessAmplification/Stages.lean @@ -44,7 +44,8 @@ operation. * `Cslib.Circuits.Boolean.pointOfBits`, `Cslib.Circuits.Boolean.bitsOfPoint`: points of `F ^ m` and their bits. * `Cslib.Circuits.Boolean.BitSynthesis`: bit-synthesizable functions. -* `Cslib.Circuits.Boolean.glPredictor`: the Goldreich–Levin decoder of the inner code. +* `Cslib.Circuits.Boolean.glPredictor`, `Cslib.Circuits.Boolean.glCost`: the Goldreich–Levin + decoder of the inner code and its gate budget. ## Main results diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/AffineController.lean b/Complexity/Computability/Circuit/Boolean/Iteration/AffineController.lean index f915fdb16..140240641 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/AffineController.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/AffineController.lean @@ -132,6 +132,7 @@ def controlledBits (g : BitString q → BitString q) Fin.append (g fun i => x (Fin.castAdd p i)) (a (fun i => x (Fin.castAdd p i)) (fun i => x (Fin.natAdd q i))) +/-- Applying `controlledBits g a` to `Fin.append u v` yields `Fin.append (g u) (a u v)`. -/ @[simp] theorem controlledBits_append (g : BitString q → BitString q) (a : BitString q → BitString p → BitString p) (u : BitString q) (v : BitString p) : controlledBits g a (Fin.append u v) = Fin.append (g u) (a u v) := by diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/CircuitCounting.lean b/Complexity/Computability/Circuit/Boolean/Iteration/CircuitCounting.lean index cda4a66fb..f92c372d0 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/CircuitCounting.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/CircuitCounting.lean @@ -101,6 +101,8 @@ noncomputable def Circuit.functionsAtMost (I : Interpretation σ U) (n m G : ℕ Finset.univ.image fun p : Program σ n g × (Fin m → Wire n g) => (⟨p.1, p.2⟩ : Circuit σ n m).eval I +/-- A function belongs to `Circuit.functionsAtMost I n m G` iff it is computed by a circuit of +size at most `G`. -/ theorem Circuit.mem_functionsAtMost_iff {I : Interpretation σ U} {n m G : ℕ} {target : (Fin n → U) → Fin m → U} : target ∈ Circuit.functionsAtMost I n m G ↔ diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/CounterBatch.lean b/Complexity/Computability/Circuit/Boolean/Iteration/CounterBatch.lean index 0774c3d78..c69a967ff 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/CounterBatch.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/CounterBatch.lean @@ -78,6 +78,8 @@ variable {k r : ℕ} abbrev counterRemainder (T : ℕ) (x : BitString k) : BitString k := ModulusCounter.remainder T x +/-- The `BitVec k` word of `counterRemainder T x` is `T % (word x).toNat` for nonzero `word x` +and `0` otherwise. -/ theorem word_counterRemainder (T : ℕ) (x : BitString k) : word (counterRemainder T x) = BitVec.ofNat k (if (word x).toNat = 0 then 0 else T % (word x).toNat) := @@ -110,10 +112,12 @@ theorem counterPower_of_remainder (T : ℕ) (c : Circuit signature k k) /-! ### Batched modular-counter states and dictionary -/ +/-- The quotient `divNat` of `finProdFinEquiv (a, b)` recovers the first coordinate `a`. -/ @[simp] theorem divNat_finProdFinEquiv {m n : ℕ} (a : Fin m) (b : Fin n) : (finProdFinEquiv (a, b)).divNat = a := congrArg Prod.fst (finProdFinEquiv.symm_apply_apply (a, b)) +/-- The remainder `modNat` of `finProdFinEquiv (a, b)` recovers the second coordinate `b`. -/ @[simp] theorem modNat_finProdFinEquiv {m n : ℕ} (a : Fin m) (b : Fin n) : (finProdFinEquiv (a, b)).modNat = b := congrArg Prod.snd (finProdFinEquiv.symm_apply_apply (a, b)) @@ -128,12 +132,16 @@ def counterBatchPower (T : ℕ) (x : BitString (r * (k + k))) : BitString (r * ( fun i => ModulusCounter.power T (counterBlock x (finProdFinEquiv.symm i).1) (finProdFinEquiv.symm i).2 +/-- At coordinate `finProdFinEquiv (member, bit)`, `counterBatchPower T x` evaluates bit `bit` of +`ModulusCounter.power T` on block `member`. -/ @[simp] theorem counterBatchPower_apply (T : ℕ) (x : BitString (r * (k + k))) (member : Fin r) (bit : Fin (k + k)) : counterBatchPower T x (finProdFinEquiv (member, bit)) = ModulusCounter.power T (counterBlock x member) bit := by simp [counterBatchPower] +/-- Extracting block `member` from `counterBatchPower T x` yields `ModulusCounter.power T` applied +to `counterBlock x member`. -/ @[simp] theorem counterBlock_counterBatchPower (T : ℕ) (x : BitString (r * (k + k))) (member : Fin r) : counterBlock (counterBatchPower T x) member = @@ -181,6 +189,8 @@ def residueKeys (k : ℕ) (j : Fin (2 ^ k - 1)) : BitString k := def residueValues (k T : ℕ) (j : Fin (2 ^ k - 1)) : BitString k := fun bit => (BitVec.ofNat k (T % (j.val + 1))).getLsbD bit.val +/-- The dictionary key map `residueKeys k` over the `2 ^ k - 1` positive `k`-bit moduli is +injective. -/ theorem residueKeys_injective (k : ℕ) : Function.Injective (residueKeys k) := by intro i j h have hw : BitVec.ofNat k (i.val + 1) = BitVec.ofNat k (j.val + 1) := diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Basic.lean b/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Basic.lean index 322cfbd95..52b833de5 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Basic.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Basic.lean @@ -23,6 +23,7 @@ semantic chart used by the sparse live-time circuit. ## Main definitions * `CounterIntervalChart`: intervals on which iteration is numerical translation. +* `nextBoundary`: the next interval start above `a`, or the upper endpoint `N`. ## Main results @@ -64,9 +65,12 @@ namespace CounterIntervalChart variable {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) +/-- Every interval start `chart.start j` is strictly below `2 ^ n`. -/ theorem start_lt (j : Fin R) : chart.start j < 2 ^ n := (chart.start_lt_stop j).trans_le (chart.stop_le j) +/-- A word `x` inside interval `j` is reached from `chart.start j` after `x.toNat - chart.start j` +steps of `f`. -/ theorem point_eq (j : Fin R) (x : BitVec n) (hlo : chart.start j ≤ x.toNat) (hhi : x.toNat < chart.stop j) : f^[x.toNat - chart.start j] (BitVec.ofNat n (chart.start j)) = x := by @@ -130,6 +134,7 @@ private theorem nextBoundary_gt (S : Finset ℕ) {N a : ℕ} (ha : a < N) : private theorem nextBoundary_le (S : Finset ℕ) (N a : ℕ) : nextBoundary S N a ≤ N := Finset.min'_le _ _ (by simp) +/-- Every element `b ∈ S` strictly above `a` is an upper bound on `nextBoundary S N a`. -/ theorem nextBoundary_le_of_mem (S : Finset ℕ) (N a b : ℕ) (hb : b ∈ S) (hab : a < b) : nextBoundary S N a ≤ b := Finset.min'_le _ _ (by simp [hb, hab]) diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Circuit.lean b/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Circuit.lean index fe210f643..8ccd7865d 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Circuit.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Circuit.lean @@ -44,6 +44,8 @@ open Cslib.FunctionalGraph variable {n R a : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) +/-- Synthesize the interval-chart encoding `chart.encode` using at most `R * (220 * (n + 3))` +gates. -/ theorem synthesis_encode (s : Set (BitString a → Bool)) (x : BitString a → BitVec n) (hx : wordWires x ⊆ s) (hc : ∀ b : Bool, (fun _ : BitString a => b) ∈ s) : Synthesis Boolean.interpretation s (wires fun z => chart.encode (x z)) @@ -80,6 +82,8 @@ theorem synthesis_encode (s : Set (BitString a → Bool)) (x : BitString a → B exact h.mono Set.Subset.rfl Set.Subset.rfl (Nat.mul_le_mul_left R (by dsimp [chartWidth]; lia)) +/-- Synthesize the interval-chart decoding `chart.decode` using at most `R * (150 * (n + 3))` +gates. -/ theorem synthesis_decode (s : Set (BitString a → Bool)) (rep : BitString a → BitVec n) (p : BitString a → BitVec (chartWidth n)) (hr : wordWires rep ⊆ s) (hp : wordWires p ⊆ s) diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Decode.lean b/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Decode.lean index bd499b142..c19d58201 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Decode.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Decode.lean @@ -12,6 +12,9 @@ public import Complexity.Computability.Circuit.Boolean.Iteration.CounterChart.En /-! # Decoding sparse interval coordinates, including intervals crossing phase zero ## Main definitions +* `CounterIntervalChart.negativePhase`, `CounterIntervalChart.phaseDistance`, + `CounterIntervalChart.decodedRow`, `CounterIntervalChart.decodeFlag`: per-interval phase + offset, decoded candidate word, and interval match test. * `CounterIntervalChart.decode`: recover a state from its representative and phase. ## Main results @@ -41,6 +44,8 @@ noncomputable def negativePhase (j : Fin R) : BitVec (chartWidth n) := BitVec.ofNat (chartWidth n) ((cycleLength f (chart.first j) - phase f (chart.first j)) % cycleLength f (chart.first j)) +/-- The natural-number value of `chart.negativePhase j` is the additive inverse of the initial +phase of interval `j` modulo its cycle length. -/ @[simp] theorem negativePhase_toNat (j : Fin R) : (chart.negativePhase j).toNat = (cycleLength f (chart.first j) - phase f (chart.first j)) % @@ -145,6 +150,7 @@ noncomputable def decode (rep : BitVec n) (p : BitVec (chartWidth n)) : BitStrin chooseRecord (fun j => chart.decodeFlag j rep p) (fun j i => (chart.decodedRow j p).getLsbD i.val) (fun _ => false) R +/-- Decoding the canonical cycle representative and phase of `y` recovers the bits of `y`. -/ theorem decode_spec (hf : Function.Injective f) (y : BitVec n) : chart.decode (canonicalCycle f y) (BitVec.ofNat (chartWidth n) (phase f y)) = fun i => y.getLsbD i.val := by diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Encode.lean b/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Encode.lean index e9387da9f..96675b56f 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Encode.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Encode.lean @@ -21,7 +21,13 @@ enumeration of payload states or an assumed constant-time table primitive. ## Main definitions +* `chartWidth`: widened bit-vector width `n + 2` for cycle lengths and phases. * `wordCycleLabel`: canonical word-cycle coordinates. +* `CounterIntervalChart.first`, `CounterIntervalChart.period`, + `CounterIntervalChart.initialPhase`, `CounterIntervalChart.length`, + `CounterIntervalChart.contains`, `CounterIntervalChart.offset`, + `CounterIntervalChart.encodedRow`: per-interval parameters, membership test, offset, and + predicted coordinates. * `CounterIntervalChart.encode`: select the coordinates of a containing interval. ## Main results @@ -51,6 +57,7 @@ variable {n R w : ℕ} /-- Two spare bits hold cycle lengths and sums even for a cycle of length `2^n`. -/ abbrev chartWidth (n : ℕ) := n + 2 +/-- Every cycle length of a map on `BitVec n` is at most `2 ^ n`. -/ theorem cycleLength_le_words (f : BitVec n → BitVec n) (x : BitVec n) : cycleLength f x ≤ 2 ^ n := by have h := transientDepth_add_cycleLength_le_card f x @@ -59,6 +66,7 @@ theorem cycleLength_le_words (f : BitVec n → BitVec n) (x : BitVec n) : rw [hc] at h lia +/-- Any natural number `a ≤ 2 ^ n` fits without wraparound in `BitVec (chartWidth n)`. -/ theorem chart_ofNat_toNat {a : ℕ} (ha : a ≤ 2 ^ n) : (BitVec.ofNat (chartWidth n) a).toNat = a := by apply Nat.mod_eq_of_lt @@ -96,14 +104,17 @@ noncomputable def initialPhase (j : Fin R) : BitVec (chartWidth n) := def length (j : Fin R) : BitVec (chartWidth n) := BitVec.ofNat (chartWidth n) (chart.stop j - chart.start j) +/-- The natural-number value of `chart.period j` is the cycle length of `chart.first j`. -/ @[simp] theorem period_toNat (j : Fin R) : (chart.period j).toNat = cycleLength f (chart.first j) := chart_ofNat_toNat (cycleLength_le_words f _) +/-- The natural-number value of `chart.initialPhase j` is the phase of `chart.first j`. -/ @[simp] theorem initialPhase_toNat (j : Fin R) : (chart.initialPhase j).toNat = phase f (chart.first j) := chart_ofNat_toNat ((phase_lt f _).le.trans (cycleLength_le_words f _)) +/-- The natural-number value of `chart.length j` is `chart.stop j - chart.start j`. -/ @[simp] theorem length_toNat (j : Fin R) : (chart.length j).toNat = chart.stop j - chart.start j := chart_ofNat_toNat ((Nat.sub_le _ _).trans (chart.stop_le j)) @@ -113,6 +124,7 @@ def contains (j : Fin R) (x : BitVec n) : Bool := !(x.setWidth (chartWidth n)).ult (BitVec.ofNat (chartWidth n) (chart.start j)) && (x.setWidth (chartWidth n)).ult (BitVec.ofNat (chartWidth n) (chart.stop j)) +/-- `chart.contains j x` is `true` iff `x.toNat` lies in `[chart.start j, chart.stop j)`. -/ @[simp] theorem contains_iff (j : Fin R) (x : BitVec n) : chart.contains j x = true ↔ chart.start j ≤ x.toNat ∧ x.toNat < chart.stop j := by have hx := chart_setWidth_toNat x @@ -169,6 +181,8 @@ private theorem encodedRow_spec (hf : Function.Injective f) (j : Fin R) (x : Bit noncomputable def encode (x : BitVec n) : BitString (n + (chartWidth n + chartWidth n)) := chooseRecord (fun j => chart.contains j x) (fun j => chart.encodedRow j x) (fun _ => false) R +/-- Encoding a word `x` under an injective map `f` produces its canonical cycle coordinates +`wordCycleLabel f x`. -/ theorem encode_spec (hf : Function.Injective f) (x : BitVec n) : chart.encode x = wordCycleLabel f x := by obtain ⟨j, hlo, hhi⟩ := chart.covers x diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Time.lean b/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Time.lean index b85a63390..59efc6101 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Time.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/CounterChart/Time.lean @@ -48,6 +48,8 @@ def advanceCycleLabel (r : BitString (n + (chartWidth n + chartWidth n))) (addResidue (labelLength r) (labelPhase r) (streamRemainder (labelLength r) bits)) +/-- Advancing the cycle label of `x` by `bits` yields the cycle label of +`f^[(word bits).toNat] x`. -/ theorem advanceCycleLabel_spec (f : BitVec n → BitVec n) (x : BitVec n) (bits : Fin m → Bool) : advanceCycleLabel (wordCycleLabel f x) bits = wordCycleLabel f (f^[(word bits).toNat] x) := by let ell := BitVec.ofNat (chartWidth n) (cycleLength f x) diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/Decoder.lean b/Complexity/Computability/Circuit/Boolean/Iteration/Decoder.lean index 1ef6e96c9..406c84252 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/Decoder.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/Decoder.lean @@ -24,7 +24,13 @@ pairs that a detector never produces. ## Main definitions +* `Cslib.Circuits.Boolean.Iteration.hitValue`: the state `K - index` steps after a checkpoint + payload. +* `Cslib.Circuits.Boolean.Iteration.repeatedValue`: the prefix state at the time in `[lo, hi)` + congruent to `T`. * `Cslib.Circuits.Boolean.Iteration.reconstruct`: the state determined by a pair of records. +* `Cslib.Circuits.Boolean.Iteration.prefixWires`: the wire functions of the prefix states up to + time `K`. ## Main results @@ -63,6 +69,7 @@ def reconstruct (f : BitString n → BitString n) (T K : ℕ) (x : BitString n) else if a.index.ult b.index then repeatedValue f T K x a.index b.index else repeatedValue f T K x b.index a.index +/-- Stepping `K - d` times from the checkpoint payload `f^[T - K] (f^[d] x)` recovers `f^[T] x`. -/ theorem hitValue_spec (f : BitString n → BitString n) (T K d : ℕ) (x : BitString n) (hd : d ≤ K) (hK : K < 2 ^ w) (hT : K ≤ T) : hitValue f K (BitVec.ofNat w d) (f^[T - K] (f^[d] x)) = f^[T] x := by @@ -114,6 +121,7 @@ theorem reconstruct_spec {M : ℕ} (f : BitString n → BitString n) (T K : ℕ) def prefixWires (f : BitString n → BitString n) (K : ℕ) : Set (BooleanFunction n) := Synthesis.stages (fun j => wires fun x => f^[j] x) K +/-- Every bit wire of `f^[j]` for `j ≤ K` belongs to `prefixWires f K`. -/ theorem prefix_mem (f : BitString n → BitString n) {K j : ℕ} (hj : j ≤ K) (bit : Fin n) : (fun x => f^[j] x bit) ∈ prefixWires f K := Synthesis.subset_stages _ hj ⟨bit, rfl⟩ @@ -135,6 +143,8 @@ private theorem synthesis_repeatedValue (s : Set (BooleanFunction n)) apply (hidx.trans hsel).mono Set.Subset.rfl Set.Subset.rfl nlinarith [Nat.zero_le (K * n ^ 2), Nat.zero_le (K * n * w), Nat.zero_le (K * w ^ 2)] +/-- Synthesizes `hitValue` by unfolding `K` steps of `c` from `payload` and selecting step +`K - index`. -/ theorem synthesis_hitValue {a : ℕ} (s : Set (BooleanFunction a)) (c : Circuit signature n n) (K : ℕ) (index : BitString a → BitVec w) (payload : BitString a → BitString n) diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/ForestCircuitRecords.lean b/Complexity/Computability/Circuit/Boolean/Iteration/ForestCircuitRecords.lean index 257b76a12..bb04dccee 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/ForestCircuitRecords.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/ForestCircuitRecords.lean @@ -23,10 +23,15 @@ circuit. ## Main definitions -* `Cslib.Circuits.Boolean.Iteration.forestLabelWord`: packs `(low x, high x)` as two `(n + 1)`-bit - words. -* `Cslib.Circuits.Boolean.Iteration.forestAnchorWord`: packs `(x, forestLabelWord low high x, - depthWord f x)`. +* `Cslib.Circuits.Boolean.Iteration.forestLabelWord`, + `Cslib.Circuits.Boolean.Iteration.forestLowWord`, + `Cslib.Circuits.Boolean.Iteration.forestHighWord`: pack and unpack `(low x, high x)` as two + `(n + 1)`-bit words. +* `Cslib.Circuits.Boolean.Iteration.forestAnchorWord`, + `Cslib.Circuits.Boolean.Iteration.forestAnchorState`, + `Cslib.Circuits.Boolean.Iteration.forestAnchorLabels`, + `Cslib.Circuits.Boolean.Iteration.forestAnchorDepth`: pack and unpack + `(x, forestLabelWord low high x, depthWord f x)`. * `Cslib.Circuits.Boolean.Iteration.dictionaryCost`: gate count of a shared fixed-dictionary lookup. * `Cslib.Circuits.Boolean.Iteration.ForestCircuitTables`: combined mark and compressed-edge tables for a functional graph on `BitString n`. @@ -70,11 +75,15 @@ def forestLowWord (r : BitString (n + 1 + (n + 1))) : BitVec (n + 1) := def forestHighWord (r : BitString (n + 1 + (n + 1))) : BitVec (n + 1) := word fun i : Fin (n + 1) => r (Fin.natAdd (n + 1) i) +/-- Unpacking the lower word from `forestLabelWord low high x` yields `low x` as an `(n + 1)`-bit +vector. -/ @[simp] theorem forestLowWord_bits (low high : BitString n → Fin (Nat.card (BitString n))) (x : BitString n) : forestLowWord (forestLabelWord low high x) = BitVec.ofNat (n + 1) (low x).val := by simp [forestLowWord, forestLabelWord, word_getLsbD] +/-- Unpacking the upper word from `forestLabelWord low high x` yields `high x` as an `(n + 1)`-bit +vector. -/ @[simp] theorem forestHighWord_bits (low high : BitString n → Fin (Nat.card (BitString n))) (x : BitString n) : forestHighWord (forestLabelWord low high x) = BitVec.ofNat (n + 1) (high x).val := by @@ -129,18 +138,22 @@ def forestAnchorLabels (r : BitString (n + (n + 1 + (n + 1)) + (n + 3))) : def forestAnchorDepth (r : BitString (n + (n + 1 + (n + 1)) + (n + 3))) : BitVec (n + 3) := word fun i : Fin (n + 3) => r (Fin.natAdd (n + (n + 1 + (n + 1))) i) +/-- Unpacking the state field of `forestAnchorWord f low high x` recovers `x`. -/ @[simp] theorem forestAnchorState_bits (f : BitString n → BitString n) (low high : BitString n → Fin (Nat.card (BitString n))) (x : BitString n) : forestAnchorState (forestAnchorWord f low high x) = x := by funext i simp [forestAnchorState, forestAnchorWord] +/-- Unpacking the interval-label field of `forestAnchorWord f low high x` recovers +`forestLabelWord low high x`. -/ @[simp] theorem forestAnchorLabels_bits (f : BitString n → BitString n) (low high : BitString n → Fin (Nat.card (BitString n))) (x : BitString n) : forestAnchorLabels (forestAnchorWord f low high x) = forestLabelWord low high x := by funext i simp [forestAnchorLabels, forestAnchorWord] +/-- Unpacking the depth field of `forestAnchorWord f low high x` recovers `depthWord f x`. -/ @[simp] theorem forestAnchorDepth_bits (f : BitString n → BitString n) (low high : BitString n → Fin (Nat.card (BitString n))) (x : BitString n) : forestAnchorDepth (forestAnchorWord f low high x) = depthWord f x := by diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/InPlace.lean b/Complexity/Computability/Circuit/Boolean/Iteration/InPlace.lean index 33c01d342..41b2f8b1c 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/InPlace.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/InPlace.lean @@ -54,6 +54,10 @@ projection `tape : Fin m → Fin w` satisfying `∀ x, e (M.init x) ∘ tape = x * `Cslib.Circuits.Boolean.Iteration.InPlace.Move`: clamped head moves (`left`, `stay`, `right`). * `Cslib.Circuits.Boolean.Iteration.InPlace.Machine`: an in-place multi-head machine. * `Cslib.Circuits.Boolean.Iteration.InPlace.Config`: machine configuration `(w, p, q)`. +* `Cslib.Circuits.Boolean.Iteration.InPlace.Machine.init`, + `Cslib.Circuits.Boolean.Iteration.InPlace.Machine.step`, + `Cslib.Circuits.Boolean.Iteration.InPlace.Machine.HaltingAbsorbing`: initial configuration, + one-step transition, and absorbing halting-state predicate. * `Cslib.Circuits.Boolean.Iteration.InPlace.reach`: configurations reachable from initial inputs. ## Main results @@ -160,6 +164,8 @@ def Machine.init [NeZero n] (M : Machine Q Γ h) (x : BitString n) : Config Q Γ def Machine.HaltingAbsorbing (M : Machine Q Γ h) : Prop := ∀ q, M.halting q → ∀ r a b, M.δ q r a b = (q, r, fun _ => Move.stay) +/-- Under `HaltingAbsorbing`, any configuration in a halting control state is a fixed point of +`Machine.step`. -/ theorem Machine.step_of_halting {M : Machine Q Γ h} (hM : M.HaltingAbsorbing) (z : Config Q Γ n h) (hz : M.halting z.2.2) : M.step z = z := by obtain ⟨w, p, q⟩ := z @@ -181,14 +187,18 @@ noncomputable def reach (M : Machine Q Γ h) (n : ℕ) [NeZero n] : Finset (Conf variable (M : Machine Q Γ h) +/-- A configuration belongs to `reach M n` iff it is reached in some number of steps from some +initial configuration `M.init x`. -/ theorem mem_reach {z : Config Q Γ n h} : z ∈ reach M n ↔ ∃ x t, M.step^[t] (M.init x) = z := by unfold reach simp only [Finset.mem_filter, Finset.mem_univ, true_and] +/-- Every initial configuration `M.init x` belongs to `reach M n`. -/ theorem init_mem_reach (x : BitString n) : M.init x ∈ reach M n := (mem_reach M).mpr ⟨x, 0, rfl⟩ +/-- Every iterate `M.step^[t] (M.init x)` from an initial configuration belongs to `reach M n`. -/ theorem iterate_mem_reach (x : BitString n) (t : ℕ) : M.step^[t] (M.init x) ∈ reach M n := (mem_reach M).mpr ⟨x, t, rfl⟩ diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/Label.lean b/Complexity/Computability/Circuit/Boolean/Iteration/Label.lean index 99b8b454e..73dd3d517 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/Label.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/Label.lean @@ -28,10 +28,19 @@ visit to the least state give its label directly (`shortLabel_eq_canonicalLabel` ## Main definitions +* `Cslib.Circuits.Boolean.Iteration.labelBits`, + `Cslib.Circuits.Boolean.Iteration.labelRepresentative`, + `Cslib.Circuits.Boolean.Iteration.labelLength`, + `Cslib.Circuits.Boolean.Iteration.labelPhase`, + `Cslib.Circuits.Boolean.Iteration.labelWidth`: bit-string packing and projections for cycle + labels. * `Cslib.Circuits.Boolean.Iteration.canonicalLabel`: representative, cycle length and phase. * `Cslib.Circuits.Boolean.Iteration.correctLabel`: shift a label back along the orbit. -* `Cslib.Circuits.Boolean.Iteration.shortLabel`: the label read from one traversal of a short - cycle. +* `Cslib.Circuits.Boolean.Iteration.shortRepresentative`, + `Cslib.Circuits.Boolean.Iteration.shortLength`, + `Cslib.Circuits.Boolean.Iteration.shortTime`, + `Cslib.Circuits.Boolean.Iteration.shortLabel`: the label components and label read from one + traversal of a short cycle. ## Main results @@ -75,15 +84,18 @@ def labelLength (r : BitString (n + (w + w))) : BitVec w := def labelPhase (r : BitString (n + (w + w))) : BitVec w := word fun i => r (Fin.natAdd n (Fin.natAdd w i)) +/-- Unpacking the representative from `labelBits c ell phi` recovers `c`. -/ @[simp] theorem labelRepresentative_labelBits (c : BitString n) (ell phi : BitVec w) : labelRepresentative (labelBits c ell phi) = c := by funext i simp only [labelRepresentative, labelBits, Fin.append_left] +/-- Unpacking the cycle-length word from `labelBits c ell phi` recovers `ell`. -/ @[simp] theorem labelLength_labelBits (c : BitString n) (ell phi : BitVec w) : labelLength (labelBits c ell phi) = ell := by simp only [labelLength, labelBits, Fin.append_left, Fin.append_right, word_getLsbD] +/-- Unpacking the phase word from `labelBits c ell phi` recovers `phi`. -/ @[simp] theorem labelPhase_labelBits (c : BitString n) (ell phi : BitVec w) : labelPhase (labelBits c ell phi) = phi := by simp only [labelPhase, labelBits, Fin.append_right, word_getLsbD] @@ -98,12 +110,14 @@ noncomputable def canonicalLabel (f : BitString n → BitString n) (x : BitStrin labelBits (canonicalCycle f x) (BitVec.ofNat (n + 3) (cycleLength f x)) (BitVec.ofNat (n + 3) (phase f x)) +/-- The cycle length of any `n`-bit state is at most `2 ^ n`. -/ theorem cycleLength_le_two_pow (f : BitString n → BitString n) (x : BitString n) : cycleLength f x ≤ 2 ^ n := by have h := transientDepth_add_cycleLength_le_card f x simp only [Fintype.card_fun, Fintype.card_fin, Fintype.card_bool] at h omega +/-- The `(n + 3)`-bit encoding of `cycleLength f x` evaluates to `cycleLength f x`. -/ theorem toNat_ofNat_cycleLength (f : BitString n → BitString n) (x : BitString n) : (BitVec.ofNat (n + 3) (cycleLength f x)).toNat = cycleLength f x := by have h := cycleLength_le_two_pow f x @@ -112,6 +126,7 @@ theorem toNat_ofNat_cycleLength (f : BitString n → BitString n) (x : BitString simp only [Nat.pow_succ] omega +/-- The `(n + 3)`-bit encoding of `phase f x` evaluates to `phase f x`. -/ theorem toNat_ofNat_phase (f : BitString n → BitString n) (x : BitString n) : (BitVec.ofNat (n + 3) (phase f x)).toNat = phase f x := by have h := (phase_lt f x).trans_le (cycleLength_le_two_pow f x) diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/LabelCircuit.lean b/Complexity/Computability/Circuit/Boolean/Iteration/LabelCircuit.lean index 828882afe..fd03f820a 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/LabelCircuit.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/LabelCircuit.lean @@ -230,6 +230,7 @@ private theorem canonicalLabel_iterate_factorial (f : BitString n → BitString simp only [canonicalLabel, canonicalCycle_iterate, cycleLength_iterate, phase_iterate, Nat.add_mod, Nat.mod_eq_zero_of_dvd hd, Nat.add_zero, Nat.mod_eq_of_lt (phase_lt f x)] +/-- Iterating `f` on `BitString n` for `(2 ^ n)!` steps lands on a periodic point. -/ theorem iterate_factorial_mem_periodicPts (f : BitString n → BitString n) (x : BitString n) : f^[(2 ^ n).factorial] x ∈ Function.periodicPts f := by apply (iterate_mem_periodicPts_iff f x _).mpr diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/ModulusCounter.lean b/Complexity/Computability/Circuit/Boolean/Iteration/ModulusCounter.lean index 2f54fe112..4e645d6fb 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/ModulusCounter.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/ModulusCounter.lean @@ -134,6 +134,8 @@ noncomputable def easyCounterPowers (k q : ℕ) : Finset (Fin (ModulusCounter.pe noncomputable def hardCounterPowers (k q : ℕ) : Finset (Fin (ModulusCounter.period k)) := Finset.univ \ easyCounterPowers k q +/-- An exponent `T < ModulusCounter.period k` belongs to `easyCounterPowers k q` iff +`ModulusCounter.power T.val` is computed by a circuit of size at most `q`. -/ theorem mem_easyCounterPowers (k q : ℕ) (T : Fin (ModulusCounter.period k)) : T ∈ easyCounterPowers k q ↔ ∃ c : Circuit signature (k + k) (k + k), @@ -156,6 +158,8 @@ private theorem easyCounterPowers_card_le (k q : ℕ) : _ ≤ _ := (Finset.card_le_card hsub).trans (Circuit.card_functionsAtMost_le interpretation) +/-- At least `ModulusCounter.period k - signature.orderedBudget (k + k) (k + k) q` exponents below +`ModulusCounter.period k` require more than `q` gates. -/ theorem hardCounterPowers_card_ge (k q : ℕ) : ModulusCounter.period k - signature.orderedBudget (k + k) (k + k) q ≤ (hardCounterPowers k q).card := by diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/ModulusCounter/Basic.lean b/Complexity/Computability/Circuit/Boolean/Iteration/ModulusCounter/Basic.lean index 28fd14125..73282245b 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/ModulusCounter/Basic.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/ModulusCounter/Basic.lean @@ -75,17 +75,20 @@ namespace ModulusCounter /-- Advance `b` by `T` modulo `a` when `0 < a` and `b < a`; inactive pairs are fixed. -/ def advance (a b T : ℕ) : ℕ := if 0 < a ∧ b < a then (b + T) % a else b +/-- Advancing by `0` steps leaves the state unchanged. -/ @[simp] theorem advance_zero (a b : ℕ) : advance a b 0 = b := by by_cases h : 0 < a ∧ b < a · simp [advance, h, Nat.mod_eq_of_lt h.2] · simp [advance, h] +/-- If both `a` and `b` are strictly below `U`, then `advance a b T` is strictly below `U`. -/ theorem advance_lt {a b U T : ℕ} (ha : a < U) (hb : b < U) : advance a b T < U := by unfold advance split_ifs with h · exact (Nat.mod_lt _ h.1).trans ha · exact hb +/-- Advancing by `S` steps and then by `T` steps is equivalent to advancing by `S + T` steps. -/ theorem advance_add (a b S T : ℕ) : advance a (advance a b S) T = advance a b (S + T) := by by_cases h : 0 < a ∧ b < a @@ -105,12 +108,15 @@ def rightWord (x : BitString (k + k)) : BitVec k := word fun i => x (Fin.natAdd def pack (a b : BitVec k) : BitString (k + k) := Fin.append (fun i : Fin k => a.getLsbD i.val) (fun i : Fin k => b.getLsbD i.val) +/-- Extracting the left word of `pack a b` recovers `a`. -/ @[simp] theorem leftWord_pack (a b : BitVec k) : leftWord (pack a b) = a := by simp only [leftWord, pack, Fin.append_left, word_getLsbD] +/-- Extracting the right word of `pack a b` recovers `b`. -/ @[simp] theorem rightWord_pack (a b : BitVec k) : rightWord (pack a b) = b := by simp only [rightWord, pack, Fin.append_right, word_getLsbD] +/-- Repacking the left and right words of `x` recovers `x`. -/ @[simp] theorem pack_words (x : BitString (k + k)) : pack (leftWord x) (rightWord x) = x := by funext bit induction bit using Fin.addCases with @@ -121,14 +127,17 @@ def pack (a b : BitVec k) : BitString (k + k) := def power (T : ℕ) (x : BitString (k + k)) : BitString (k + k) := pack (leftWord x) (BitVec.ofNat k (advance (leftWord x).toNat (rightWord x).toNat T)) +/-- The `0`-step counter map is the identity. -/ @[simp] theorem power_zero (x : BitString (k + k)) : power 0 x = x := by simp [power] +/-- Composing `power S` with `power T` yields `power (S + T)`. -/ theorem power_add (S T : ℕ) (x : BitString (k + k)) : power T (power S x) = power (S + T) x := by simp only [power, leftWord_pack, rightWord_pack, BitVec.toNat_ofNat] rw [Nat.mod_eq_of_lt (advance_lt (BitVec.isLt _) (BitVec.isLt _)), advance_add] +/-- Iterating the single-step counter map `power 1` for `T` steps yields `power T`. -/ theorem iterate_power (T : ℕ) : (power (k := k) 1)^[T] = power T := by funext x induction T with @@ -153,6 +162,7 @@ private theorem power_period (x : BitString (k + k)) : power (period k) x = x := simp · simp +/-- The single-step modular counter map `power 1` is a bijection on `BitString (k + k)`. -/ theorem power_bijective : Function.Bijective (power (k := k) 1) := by have hpos : 0 < period k := Nat.lcmUpto_pos _ constructor @@ -197,6 +207,7 @@ theorem powers_injective : def stepValue (a b : BitVec k) : BitVec k := if b.ult a then if b + 1 = a then 0 else b + 1 else b +/-- `stepValue a b` encodes `advance a.toNat b.toNat 1` as a `k`-bit vector. -/ theorem stepValue_spec (a b : BitVec k) : stepValue a b = BitVec.ofNat k (advance a.toNat b.toNat 1) := by by_cases h : b.toNat < a.toNat @@ -331,15 +342,18 @@ def counterNextBits (x : BitString (k + k)) : BitString k := (ModulusCounter.stepValue (ModulusCounter.leftWord x) (ModulusCounter.rightWord x)).getLsbD i.val +/-- `counterModulus` depends only on the first `k` coordinates of the `2 k`-bit state. -/ theorem counterModulus_eq_of_eq {x y : BitString (k + k)} (h : (fun i => x (Fin.castAdd k i)) = fun i => y (Fin.castAdd k i)) : counterModulus x = counterModulus y := congrArg (fun z => (word z).toNat) h +/-- `counterStep k` preserves the modulus stored in the first `k` coordinates. -/ theorem counterStep_preserve_modulus (x : BitString (k + k)) : counterModulus (counterStep k x) = counterModulus x := by simp [counterModulus, counterStep, ModulusCounter.power] +/-- Iterating `counterStepValue a` for `T` steps on `b` equals `ModulusCounter.advance a b T`. -/ theorem counterStepValue_iterate (a b T : ℕ) : (counterStepValue a)^[T] b = ModulusCounter.advance a b T := by induction T generalizing b with @@ -348,6 +362,8 @@ theorem counterStepValue_iterate (a b T : ℕ) : rw [Function.iterate_succ_apply, ih, counterStepValue, ModulusCounter.advance_add, Nat.add_comm 1 T] +/-- After `T` steps of `counterStep k`, the right word has natural value +`ModulusCounter.advance (leftWord x).toNat (rightWord x).toNat T`. -/ theorem counterStep_iterate_toNat (T : ℕ) (x : BitString (k + k)) : (ModulusCounter.rightWord ((counterStep k)^[T] x)).toNat = ModulusCounter.advance @@ -365,6 +381,8 @@ theorem counter_power_ne {S T : ℕ} (hS : S < ModulusCounter.period k) exact hne (Fin.val_eq_of_eq (ModulusCounter.powers_injective (a₁ := ⟨S, hS⟩) (a₂ := ⟨T, hT⟩) h)) +/-- There are `ModulusCounter.period k` distinct counter power functions for exponents below +`ModulusCounter.period k`. -/ theorem counter_family_card (k : ℕ) : (Finset.univ.image (fun T : Fin (ModulusCounter.period k) => ModulusCounter.power (k := k) T.val)).card = ModulusCounter.period k := by diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/ModulusCounter/Remainders.lean b/Complexity/Computability/Circuit/Boolean/Iteration/ModulusCounter/Remainders.lean index ae3c115de..fe53a0064 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/ModulusCounter/Remainders.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/ModulusCounter/Remainders.lean @@ -76,10 +76,14 @@ variable {k : ℕ} def remainder (T : ℕ) (x : BitString k) : BitString k := fun i => (BitVec.ofNat k (if (word x).toNat = 0 then 0 else T % (word x).toNat)).getLsbD i.val +/-- Packing `remainder T x` into a `BitVec k` gives `T % (word x).toNat` (or `0` when +`(word x).toNat = 0`). -/ theorem remainder_word (T : ℕ) (x : BitString k) : word (remainder T x) = BitVec.ofNat k (if (word x).toNat = 0 then 0 else T % (word x).toNat) := word_getLsbD _ +/-- When `r` encodes `T % a.toNat` for positive `a`, `addResidue a b r` encodes +`advance a.toNat b.toNat T`. -/ theorem addResidue_spec (a b r : BitVec k) (T : ℕ) (hr : 0 < a.toNat → r.toNat = T % a.toNat) : addResidue a b r = BitVec.ofNat k (advance a.toNat b.toNat T) := by @@ -289,10 +293,12 @@ def counterInput (x : BitString k) : BitString (k + k) := def counterOutput (y : BitString (k + k)) : BitString k := fun i => y (Fin.natAdd k i) +/-- The modulus word of `counterInput x` has natural value `(word x).toNat`. -/ @[simp] theorem counterInput_modulus_toNat (x : BitString k) : (ModulusCounter.leftWord (counterInput x)).toNat = (word x).toNat := by simp [counterInput] +/-- The initial counter state word of `counterInput x` has natural value `0`. -/ @[simp] theorem counterInput_state_toNat (x : BitString k) : (ModulusCounter.rightWord (counterInput x)).toNat = 0 := by simp [counterInput] diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/NavigationWord.lean b/Complexity/Computability/Circuit/Boolean/Iteration/NavigationWord.lean index 792f8fd5f..5d83d9290 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/NavigationWord.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/NavigationWord.lean @@ -28,8 +28,16 @@ These are word-level identities. The circuits that compute depths and labels are ## Main definitions -* `Cslib.Circuits.Boolean.Iteration.navigationFlag`, `navigationTime`: reachability and first - hitting time as word computations. +* `Cslib.Circuits.Boolean.Iteration.depthWord`, + `Cslib.Circuits.Boolean.Iteration.phaseWord`, + `Cslib.Circuits.Boolean.Iteration.lengthWord`: `(n + 3)`-bit words for transient depth, phase, + and cycle length. +* `Cslib.Circuits.Boolean.Iteration.navigationGap`, + `Cslib.Circuits.Boolean.Iteration.navigationDistance`: depth difference and cyclic phase + difference as `(n + 3)`-bit words. +* `Cslib.Circuits.Boolean.Iteration.navigationFlag`, + `Cslib.Circuits.Boolean.Iteration.navigationTime`: reachability and first hitting time as word + computations. * `Cslib.Circuits.Boolean.Iteration.navigationBits`: one flag bit and `n + 1` time bits. ## Main results @@ -68,18 +76,22 @@ noncomputable def phaseWord (x : BitString n) : BitVec (n + 3) := noncomputable def lengthWord (x : BitString n) : BitVec (n + 3) := BitVec.ofNat (n + 3) (cycleLength f x) +/-- The transient depth of any `n`-bit state is strictly less than `2 ^ n`. -/ theorem transientDepth_lt_two_pow (x : BitString n) : transientDepth f x < 2 ^ n := by simpa using transientDepth_lt_card f x +/-- `depthWord f x` has natural value `transientDepth f x`. -/ @[simp] theorem toNat_depthWord (x : BitString n) : (depthWord f x).toNat = transientDepth f x := by have h := transientDepth_lt_two_pow f x rw [depthWord, BitVec.toNat_ofNat, Nat.mod_eq_of_lt] simp only [Nat.pow_succ] omega +/-- `phaseWord f x` has natural value `phase f x`. -/ @[simp] theorem toNat_phaseWord (x : BitString n) : (phaseWord f x).toNat = phase f x := toNat_ofNat_phase f x +/-- `lengthWord f x` has natural value `cycleLength f x`. -/ @[simp] theorem toNat_lengthWord (x : BitString n) : (lengthWord f x).toNat = cycleLength f x := toNat_ofNat_cycleLength f x @@ -102,6 +114,8 @@ noncomputable def navigationFlag (x y : BitString n) : Bool := noncomputable def navigationTime (x y : BitString n) : BitVec (n + 3) := if depthWord f y = 0 then depthWord f x + navigationDistance f x y else navigationGap f x y +/-- When `transientDepth f y ≤ transientDepth f x`, `navigationGap f x y` has natural value +`transientDepth f x - transientDepth f y`. -/ theorem toNat_navigationGap (x y : BitString n) (hle : transientDepth f y ≤ transientDepth f x) : (navigationGap f x y).toNat = transientDepth f x - transientDepth f y := by @@ -121,10 +135,12 @@ private theorem toNat_navigationDistance (x y : BitString n) : toNat_phaseWord, toNat_phaseWord, toNat_depthWord, toNat_lengthWord, Nat.mod_eq_of_lt hsum] rfl +/-- `depthWord f x` is zero if and only if `transientDepth f x = 0`. -/ theorem depthWord_eq_zero_iff (x : BitString n) : depthWord f x = 0 ↔ transientDepth f x = 0 := by rw [← BitVec.toNat_inj, toNat_depthWord] rfl +/-- The word-level reachability flag `navigationFlag f x y` agrees with `reaches f x y`. -/ theorem navigationFlag_eq_reaches (x y : BitString n) : navigationFlag f x y = reaches f x y := by unfold navigationFlag reaches simp only [depthWord_eq_zero_iff] @@ -138,6 +154,7 @@ theorem navigationFlag_eq_reaches (x y : BitString n) : navigationFlag f x y = r · simp only [BitVec.ult, toNat_depthWord, show transientDepth f x < transientDepth f y by omega, decide_true, Bool.not_true, Bool.false_and, hle, decide_false] +/-- When `y` is reachable from `x`, `navigationTime f x y` has natural value `hittingTime f x y`. -/ theorem toNat_navigationTime (x y : BitString n) (h : reaches f x y = true) : (navigationTime f x y).toNat = hittingTime f x y := by unfold navigationTime hittingTime @@ -158,6 +175,7 @@ theorem toNat_navigationTime (x y : BitString n) (h : reaches f x y = true) : noncomputable def navigationBits (x y : BitString n) : BitString (1 + (n + 1)) := Fin.append (fun _ => navigationFlag f x y) fun i => (navigationTime f x y).getLsbD i.val +/-- Bit `0` of `navigationBits f x y` is `true` iff `y` is reachable from `x` under `f`. -/ theorem navigationBits_flag (x y : BitString n) : navigationBits f x y 0 = true ↔ ∃ t, f^[t] x = y := by change navigationFlag f x y = true ↔ _ diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/Optimization.lean b/Complexity/Computability/Circuit/Boolean/Iteration/Optimization.lean index 790985d53..602b54f37 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/Optimization.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/Optimization.lean @@ -107,6 +107,8 @@ theorem exists_le_three_mul_add_sqrt (a b M N : ℕ) (hb : 0 < b) (hba : b ≤ a change (a : ℝ) * L + b * ((M / L : ℕ) + 1) ≤ 3 * (a + z) nlinarith +/-- For any `M ≤ 2 ^ n`, there is a checkpoint parameter `0 < L ≤ 2 ^ n` with +`powerBudget n s M L ≤ 3 * optimizedBudget n s M`. -/ theorem exists_powerBudget_le_optimizedBudget (n s M : ℕ) (hM : M ≤ 2 ^ n) : ∃ L : ℕ, 0 < L ∧ L ≤ 2 ^ n ∧ (powerBudget n s M L : ℝ) ≤ 3 * optimizedBudget n s M := by obtain ⟨L, hL, hLN, h⟩ := exists_le_three_mul_add_sqrt (s + (n + 1) ^ 3) ((n + 1) ^ 3) diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/PrimeCycles.lean b/Complexity/Computability/Circuit/Boolean/Iteration/PrimeCycles.lean index 7cc777b78..5a7cb6988 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/PrimeCycles.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/PrimeCycles.lean @@ -48,16 +48,32 @@ advances `b` by `1` modulo `ℓ r` when `b < ℓ r` and fixes every other state. ## Main definitions +* `Cslib.Circuits.Boolean.Iteration.PrimeCycles.classWord`, + `Cslib.Circuits.Boolean.Iteration.PrimeCycles.posWord`, + `Cslib.Circuits.Boolean.Iteration.PrimeCycles.pack`: split and pack `m`-bit class and `K`-bit + position words. * `Cslib.Circuits.Boolean.Iteration.PrimeCycles.power`: `T`-step map advancing each class `r` modulo `ℓ r`. * `Cslib.Circuits.Boolean.Iteration.PrimeCycles.step`: single-step permutation `power ℓ 1`. -* `Cslib.Circuits.Boolean.Iteration.PrimeCycles.order`: common-period product of the nontrivial - cycle lengths (which equals the exact permutation order under `LengthsCoprime`). -* `Cslib.Circuits.Boolean.Iteration.PrimeCycles.classPrime`: least-index prime candidate in each - hash class, or `1` if none exists. +* `Cslib.Circuits.Boolean.Iteration.PrimeCycles.active`, + `Cslib.Circuits.Boolean.Iteration.PrimeCycles.order`, + `Cslib.Circuits.Boolean.Iteration.PrimeCycles.LengthsCoprime`: active classes, common-period + product of the nontrivial cycle lengths (which equals the exact permutation order under + `LengthsCoprime`), and pairwise coprimality predicate. +* `Cslib.Circuits.Boolean.Iteration.PrimeCycles.candidate`, + `Cslib.Circuits.Boolean.Iteration.PrimeCycles.classPrime`: prime candidates and least-index prime + candidate in each hash class, or `1` if none exists. * `Cslib.Circuits.Boolean.Iteration.lcmBelow`: least common multiple of `{1, …, n}`. -* `Cslib.Circuits.Boolean.Iteration.PrimeCycleData`: bundled cycle-length data with pairwise - coprime nontrivial lengths. +* `Cslib.Circuits.Boolean.Iteration.PrimeCycleData`, + `Cslib.Circuits.Boolean.Iteration.PrimeCycleData.activeLength`, + `Cslib.Circuits.Boolean.Iteration.PrimeCycleData.stepNat`, + `Cslib.Circuits.Boolean.Iteration.PrimeCycleData.step`, + `Cslib.Circuits.Boolean.Iteration.PrimeCycleData.perm`, + `Cslib.Circuits.Boolean.Iteration.PrimeCycleData.period`, + `Cslib.Circuits.Boolean.Iteration.PrimeCycleData.lengthBits`, + `Cslib.Circuits.Boolean.Iteration.PrimeCycleData.remainderBits`, + `Cslib.Circuits.Boolean.Iteration.PrimeCycleData.ofHash`: bundled cycle-length data with pairwise + coprime nontrivial lengths and associated step, period, bit-encoding, and hash constructors. ## Main results @@ -90,8 +106,10 @@ open scoped BigOperators /-- The least common multiple `lcm(1, …, n)`. -/ def lcmBelow (n : ℕ) : ℕ := Nat.lcmUpto n +/-- `lcmBelow n` is positive for every `n`. -/ theorem lcmBelow_pos (n : ℕ) : 0 < lcmBelow n := Nat.lcmUpto_pos n +/-- `lcmBelow n` equals the product of highest prime powers `p ^ p.log n` for primes `p ≤ n`. -/ theorem lcmBelow_eq_prod_prime_powers (n : ℕ) : lcmBelow n = ∏ p ∈ Nat.primesLE n, p ^ p.log n := Nat.lcmUpto_eq_prod_pow_log n @@ -217,12 +235,15 @@ def posWord (x : BitString (m + K)) : BitVec K := word fun i => x (Fin.natAdd m def pack (r : BitVec m) (b : BitVec K) : BitString (m + K) := Fin.append (fun i : Fin m => r.getLsbD i.val) (fun i : Fin K => b.getLsbD i.val) +/-- Extracting the class word from `pack r b` recovers `r`. -/ @[simp] theorem classWord_pack (r : BitVec m) (b : BitVec K) : classWord (pack r b) = r := by simp only [classWord, pack, Fin.append_left, word_getLsbD] +/-- Extracting the position word from `pack r b` recovers `b`. -/ @[simp] theorem posWord_pack (r : BitVec m) (b : BitVec K) : posWord (pack r b) = b := by simp only [posWord, pack, Fin.append_right, word_getLsbD] +/-- Repacking the class and position words of `x` recovers `x`. -/ @[simp] theorem pack_words (x : BitString (m + K)) : pack (classWord x) (posWord x) = x := by funext bit induction bit using Fin.addCases with @@ -239,6 +260,7 @@ def step (ℓ : BitVec m → ℕ) : BitString (m + K) → BitString (m + K) := p variable (ℓ : BitVec m → ℕ) +/-- The `0`-th power `power ℓ 0` is the identity map. -/ @[simp] theorem power_zero : power (K := K) ℓ 0 = id := by funext x simp [power] @@ -284,6 +306,7 @@ private theorem power_prod_eq_id : simp · simp +/-- When every cycle length is below `2 ^ K`, `step ℓ` is a bijection on `BitString (m + K)`. -/ theorem step_bijective (hℓ : ∀ r, ℓ r < 2 ^ K) : Function.Bijective (step (K := K) ℓ) := by set P := ∏ r ∈ Finset.univ.filter (fun r => 0 < ℓ r), ℓ r have hP : 0 < P := Finset.prod_pos fun r hr => (Finset.mem_filter.mp hr).2 @@ -323,6 +346,7 @@ def active : Finset (BitVec m) := Finset.univ.filter fun r => 1 < ℓ r order under `LengthsCoprime`). -/ def order : ℕ := ∏ r ∈ active ℓ, ℓ r +/-- The common-period product `order ℓ` of the nontrivial cycle lengths is positive. -/ theorem order_pos : 0 < order ℓ := Finset.prod_pos fun r hr => by have := (Finset.mem_filter.mp hr).2 @@ -337,6 +361,8 @@ def LengthsCoprime : Prop := ((active ℓ : Finset (BitVec m)) : Set (BitVec m)) variable {ℓ} +/-- Under `LengthsCoprime ℓ`, two exponents are congruent modulo `order ℓ` iff they are congruent +modulo every nontrivial cycle length `ℓ r`. -/ theorem modEq_order_iff (hc : LengthsCoprime ℓ) (S T : ℕ) : S ≡ T [MOD order ℓ] ↔ ∀ r, 1 < ℓ r → S ≡ T [MOD ℓ r] := by have hrel : ((active ℓ : Finset (BitVec m)) : Set (BitVec m)).Pairwise @@ -466,6 +492,8 @@ private theorem classPrime_spec {g : ℕ} (f : ℕ → ℕ) (r : BitVec m) : exact ⟨_, hs.1, rfl, hs.2⟩ · left; rfl +/-- Every `classPrime m g f r` is below `2 ^ (m + g + 1)`, and any nontrivial `classPrime m g f r` +is a prime at least `2 ^ (m + g)`. -/ theorem classPrime_bounds {g : ℕ} {f : ℕ → ℕ} (hf : ∀ z, f z < 2 ^ m) (r : BitVec m) : classPrime m g f r < 2 ^ (m + g + 1) ∧ (1 < classPrime m g f r → 2 ^ (m + g) ≤ classPrime m g f r ∧ (classPrime m g f r).Prime) := by @@ -546,6 +574,7 @@ def stepNat (r : BitVec m) (b : ℕ) : ℕ := def step : BitString (m + K) → BitString (m + K) := PrimeCycles.step D.length +/-- The single-step map `D.step` is a bijection on `BitString (m + K)`. -/ theorem step_bijective : Function.Bijective D.step := PrimeCycles.step_bijective D.length D.length_lt @@ -557,14 +586,18 @@ noncomputable def perm : Equiv.Perm (BitString (m + K)) := def period : ℕ := PrimeCycles.order D.length +/-- `D.step^[T]` is the identity iff `D.period` divides `T`. -/ theorem period_dvd_of_fixed (T : ℕ) : D.step^[T] = id ↔ D.period ∣ T := PrimeCycles.iterate_eq_id_iff D.length_lt D.lengths_coprime T +/-- Powers `D.step^[T]` for `T < D.period` are pairwise distinct. -/ theorem powers_injective : Function.Injective (fun T : Fin D.period => D.step^[T.val]) := PrimeCycles.iterate_injective D.length_lt D.lengths_coprime +/-- If the ordered-syntax budget for `q` gates is strictly below `D.period`, some power +`D.step^[T]` with `T < D.period` requires more than `q` gates. -/ theorem exists_hard_power (q : ℕ) (large : signature.orderedBudget (m + K) (m + K) q < D.period) : ∃ T < D.period, ∀ out : Circuit signature (m + K) (m + K), @@ -583,6 +616,7 @@ theorem step_diff_card_le : def lengthBits (r : BitString m) : BitString K := fun i : Fin K => (BitVec.ofNat K (D.length (word r))).getLsbD i.val +/-- Packing `D.lengthBits r` into a `BitVec K` gives `BitVec.ofNat K (D.length (word r))`. -/ @[simp] theorem word_lengthBits (r : BitString m) : word (D.lengthBits r) = BitVec.ofNat K (D.length (word r)) := word_getLsbD _ @@ -593,6 +627,8 @@ def remainderBits (T : ℕ) (r : BitString m) : BitString K := fun i : Fin K => (BitVec.ofNat K (if 0 < D.length (word r) then T % D.length (word r) else 0)).getLsbD i.val +/-- Packing `D.remainderBits T r` into a `BitVec K` gives `T % D.length (word r)` (or `0` when +`D.length (word r) = 0`). -/ @[simp] theorem word_remainderBits (T : ℕ) (r : BitString m) : word (D.remainderBits T r) = BitVec.ofNat K (if 0 < D.length (word r) then T % D.length (word r) else 0) := diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/Record.lean b/Complexity/Computability/Circuit/Boolean/Iteration/Record.lean index 2360b26b1..cefcaf0af 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/Record.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/Record.lean @@ -24,11 +24,26 @@ records repeat. Sorting uses the native Batcher circuit `bitonicSortCircuit`. ## Main definitions -* `Cslib.Circuits.Boolean.Iteration.Record`: a complete record and its bit encoding. -* `Cslib.Circuits.Boolean.Iteration.Record.initial`: checkpoints, then the orbit prefix, then - padding. +* `Cslib.Circuits.Boolean.Iteration.Record`, + `Cslib.Circuits.Boolean.Iteration.Record.width`, + `Cslib.Circuits.Boolean.Iteration.Record.key`, + `Cslib.Circuits.Boolean.Iteration.Record.keyBits`, + `Cslib.Circuits.Boolean.Iteration.Record.encode`, + `Cslib.Circuits.Boolean.Iteration.Record.decode`: a complete record, its sort key, and its bit + encoding. +* `Cslib.Circuits.Boolean.Iteration.Record.query`, + `Cslib.Circuits.Boolean.Iteration.Record.stored`, + `Cslib.Circuits.Boolean.Iteration.Record.pad`, + `Cslib.Circuits.Boolean.Iteration.Record.collision`, + `Cslib.Circuits.Boolean.Iteration.Record.initial`, + `Cslib.Circuits.Boolean.Iteration.Record.Valid`: query, checkpoint, and padding records, + collision test, initial array, and validity predicate. * `Cslib.Circuits.Boolean.Iteration.Record.Witness`: what a detected collision certifies. -* `Cslib.Circuits.Boolean.Iteration.Record.sorted`, `Record.detect`: sort and scan. +* `Cslib.Circuits.Boolean.Iteration.Record.pack`, + `Cslib.Circuits.Boolean.Iteration.Record.sorted`, + `Cslib.Circuits.Boolean.Iteration.Record.adjacentPair`, + `Cslib.Circuits.Boolean.Iteration.Record.detect`: array packing, sorting, and adjacent-collision + scan. ## Main results @@ -86,9 +101,11 @@ def decode (bits : BitString (width n w)) : Record n w where index := word fun i => bits (Fin.natAdd (n + 1) (Fin.castAdd n i).succ) payload i := bits (Fin.natAdd (n + 1) (Fin.natAdd w i).succ) +/-- Decoding the bit encoding of a record recovers the record. -/ @[simp] theorem decode_encode (r : Record n w) : decode (encode r) = r := by ext <;> simp [decode, encode, Fin.cons] +/-- Encoding the decoded record of a bit string recovers the bit string. -/ @[simp] theorem encode_decode (bits : BitString (width n w)) : encode (decode bits) = bits := by funext i induction i using Fin.addCases with @@ -104,6 +121,7 @@ def decode (bits : BitString (width n w)) : Record n w where | left i => simp [encode, decode] | right i => simp [encode, decode] +/-- Record bit encoding `encode` is injective. -/ theorem encode_injective : Function.Injective (encode : Record n w → BitString (width n w)) := Function.LeftInverse.injective decode_encode @@ -114,6 +132,7 @@ private theorem key_decode (bits : BitString (width n w)) : funext i induction i using Fin.cases <;> rfl +/-- Two records have equal sort keys iff they have the same padding flag and state. -/ theorem key_eq_iff (a b : Record n w) : a.key = b.key ↔ a.padding = b.padding ∧ a.state = b.state := by constructor @@ -137,6 +156,8 @@ def pad : Record n w := ⟨true, fun _ => false, false, 0, fun _ => false⟩ def collision (a b : Record n w) : Bool := !a.padding && !b.padding && decide (a.state = b.state) && decide (a ≠ b) +/-- `collision a b` holds iff neither record is padding, their states are equal, and the records +are distinct. -/ theorem collision_iff (a b : Record n w) : collision a b = true ↔ a.padding = false ∧ b.padding = false ∧ a.state = b.state ∧ a ≠ b := by @@ -219,6 +240,7 @@ private theorem collision_witness (f : BitString n → BitString n) (T K : ℕ) def pack (records : Fin R → Record n w) : BitString (R * width n w) := fun bit => encode (records (finProdFinEquiv.symm bit).1) (finProdFinEquiv.symm bit).2 +/-- Extracting the `j`-th block of `pack records` gives `encode (records j)`. -/ @[simp] theorem directProductInput_pack (records : Fin R → Record n w) (j : Fin R) : directProductInput (pack records) j = encode (records j) := by funext bit diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/RecordCircuit.lean b/Complexity/Computability/Circuit/Boolean/Iteration/RecordCircuit.lean index 2740f95c8..600618c6a 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/RecordCircuit.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/RecordCircuit.lean @@ -25,7 +25,11 @@ adjacent pair for a collision and selecting one costs linearly in the array ## Main definitions * `Cslib.Circuits.Boolean.Iteration.wires`: the coordinate functions of a family of bit strings. -* `Cslib.Circuits.Boolean.Iteration.Record.wireSet`, `Record.recordsWires`: available records. +* `Cslib.Circuits.Boolean.Iteration.Record.wireSet`, + `Cslib.Circuits.Boolean.Iteration.Record.pairEncode`, + `Cslib.Circuits.Boolean.Iteration.Record.pairWires`, + `Cslib.Circuits.Boolean.Iteration.Record.recordsWires`: available records, record pairs, and + record arrays. ## Main results @@ -69,6 +73,7 @@ theorem synthesis_bits_eq {m : ℕ} (s : Set (BooleanFunction n)) b x := funext fun i => by simp only [Function.comp_apply, Fin.append_right] simp only [Formula.eval_toCircuit, Formula.eval_equalBits_iff, decide_eq_true_eq, hl, hr] +/-- Multiplexing two `m`-bit strings by an available Boolean flag costs `4 * m` gates. -/ theorem synthesis_bits_mux {m : ℕ} (s : Set (BooleanFunction n)) (a b : BitString n → BitString m) (flag : BooleanFunction n) (ha : wires a ⊆ s) (hb : wires b ⊆ s) (hf : flag ∈ s) : @@ -95,22 +100,27 @@ namespace Record /-- The bits of an available family of records. -/ def wireSet (a : BitString n → Record n w) : Set (BooleanFunction n) := wires fun x => encode (a x) +/-- The padding bit of an available record belongs to `s`. -/ theorem padding_mem {s : Set (BooleanFunction n)} {a : BitString n → Record n w} (ha : wireSet a ⊆ s) : (fun x => (a x).padding) ∈ s := by simpa [encode] using ha ⟨Fin.castAdd (w + n + 1) 0, rfl⟩ +/-- Each state bit of an available record belongs to `s`. -/ theorem state_mem {s : Set (BooleanFunction n)} {a : BitString n → Record n w} (ha : wireSet a ⊆ s) (i : Fin n) : (fun x => (a x).state i) ∈ s := by simpa [encode] using ha ⟨Fin.castAdd (w + n + 1) i.succ, rfl⟩ +/-- The checkpoint bit of an available record belongs to `s`. -/ theorem checkpoint_mem {s : Set (BooleanFunction n)} {a : BitString n → Record n w} (ha : wireSet a ⊆ s) : (fun x => (a x).checkpoint) ∈ s := by simpa [encode] using ha ⟨Fin.natAdd (n + 1) 0, rfl⟩ +/-- Each index bit of an available record belongs to `s`. -/ theorem index_mem {s : Set (BooleanFunction n)} {a : BitString n → Record n w} (ha : wireSet a ⊆ s) (i : Fin w) : (fun x => (a x).index.getLsbD i.val) ∈ s := by simpa [encode] using ha ⟨Fin.natAdd (n + 1) (Fin.castAdd n i).succ, rfl⟩ +/-- Each payload bit of an available record belongs to `s`. -/ theorem payload_mem {s : Set (BooleanFunction n)} {a : BitString n → Record n w} (ha : wireSet a ⊆ s) (i : Fin n) : (fun x => (a x).payload i) ∈ s := by simpa [encode] using ha ⟨Fin.natAdd (n + 1) (Fin.natAdd w i).succ, rfl⟩ @@ -135,11 +145,13 @@ def pairEncode (pair : Record n w × Record n w) : BitString (width n w + width def pairWires (p : BitString n → Record n w × Record n w) : Set (BooleanFunction n) := wires fun x => pairEncode (p x) +/-- The wire set of the first record of a pair is contained in `pairWires p`. -/ theorem wireSet_fst_subset (p : BitString n → Record n w × Record n w) : wireSet (fun x => (p x).1) ⊆ pairWires p := by rintro _ ⟨i, rfl⟩ exact ⟨Fin.castAdd (width n w) i, by simp only [pairEncode, Fin.append_left]⟩ +/-- The wire set of the second record of a pair is contained in `pairWires p`. -/ theorem wireSet_snd_subset (p : BitString n → Record n w × Record n w) : wireSet (fun x => (p x).2) ⊆ pairWires p := by rintro _ ⟨i, rfl⟩ @@ -184,6 +196,7 @@ theorem synthesis_detect (s : Set (BooleanFunction n)) (records : BitString n def recordsWires (records : BitString n → Fin R → Record n w) : Set (BooleanFunction n) := ⋃ j, wireSet fun x => records x j +/-- The wire set of the `j`-th record in an array is contained in `recordsWires records`. -/ theorem wireSet_subset_recordsWires (records : BitString n → Fin R → Record n w) (j : Fin R) : wireSet (fun x => records x j) ⊆ recordsWires records := Set.subset_iUnion_of_subset j Set.Subset.rfl diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/Remainder.lean b/Complexity/Computability/Circuit/Boolean/Iteration/Remainder.lean index 6d5524d87..79e0344ff 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/Remainder.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/Remainder.lean @@ -34,6 +34,7 @@ are free. ## Main definitions +* `Cslib.Circuits.Boolean.Iteration.remainderStep`: one step of long division by a word. * `Cslib.Circuits.Boolean.Iteration.streamRemainder`: long division, most significant bit first. * `Cslib.Circuits.Boolean.Iteration.subMod`: modular difference of two words. diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/Residue.lean b/Complexity/Computability/Circuit/Boolean/Iteration/Residue.lean index 636ff33ff..34be83e60 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/Residue.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/Residue.lean @@ -25,7 +25,11 @@ fixed exponent `T` only through its residues, and then adds the period while the ## Main definitions -* `Cslib.Circuits.Boolean.Iteration.liftResidue`: one bounded correction of a residue. +* `Cslib.Circuits.Boolean.Iteration.liftResidue`, + `Cslib.Circuits.Boolean.Iteration.liftWord`: one bounded correction of a residue, on natural + numbers and on words. +* `Cslib.Circuits.Boolean.Iteration.residueWord`: table lookup of the residue of `T` modulo a + period word. * `Cslib.Circuits.Boolean.Iteration.repeatWordIndex`: the word computation of the time in the repeated interval. diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/ResidueAdd.lean b/Complexity/Computability/Circuit/Boolean/Iteration/ResidueAdd.lean index 5430ce387..5f6abff8e 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/ResidueAdd.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/ResidueAdd.lean @@ -20,9 +20,10 @@ division is needed: three subtractions, one comparison, and one word selection s ## Main definitions -* `addResidue a b r`: modulus `a`, initial residue `b`, and increment `r`; - return `b` unchanged when `b ≥ a`. -* `subtractResidues a b d`: modular difference `(a - b) mod d` of reduced residues `a, b < d`. +* `Cslib.Circuits.Boolean.Iteration.addResidue`: modular sum `(b + r) mod a` of reduced residues + `b, r < a`, returning `b` unchanged when `b ≥ a`. +* `Cslib.Circuits.Boolean.Iteration.subtractResidues`: modular difference `(a - b) mod d` of + reduced residues `a, b < d`. ## Main results diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/Scan.lean b/Complexity/Computability/Circuit/Boolean/Iteration/Scan.lean index 8f588ca83..fd9489492 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/Scan.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/Scan.lean @@ -179,6 +179,7 @@ reverse order. -/ def chooseFirst {α : Type*} (flags : Fin R → Bool) (records : Fin R → α) (fallback : α) : α := chooseRecord (fun j => flags j.rev) (fun j => records j.rev) fallback R +/-- If `j` is the first flagged position, `chooseFirst` returns `records j`. -/ theorem chooseFirst_spec {α : Type*} (flags : Fin R → Bool) (records : Fin R → α) (fallback : α) (j : Fin R) (hj : flags j = true) (hfirst : ∀ i : Fin R, i.val < j.val → flags i = false) : @@ -194,6 +195,7 @@ theorem chooseFirst_spec {α : Type*} (flags : Fin R → Bool) (records : Fin R def firstIndex (flags : Fin R → Bool) : BitVec w := word (chooseFirst flags (fun j bit => (BitVec.ofNat w j.val).getLsbD bit.val) fun _ => false) +/-- If `j` is the first flagged position, `firstIndex` returns `j.val` as a `w`-bit word. -/ theorem firstIndex_spec (flags : Fin R → Bool) (j : Fin R) (hj : flags j = true) (hfirst : ∀ i : Fin R, i.val < j.val → flags i = false) : firstIndex (w := w) flags = BitVec.ofNat w j.val := by diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/SharedDictionary.lean b/Complexity/Computability/Circuit/Boolean/Iteration/SharedDictionary.lean index 991797df5..e178b64fd 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/SharedDictionary.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/SharedDictionary.lean @@ -29,6 +29,10 @@ are free. ## Main definitions * `Cslib.Circuits.Boolean.Iteration.lookupOr`: the OR of the values stored under a key. +* `Cslib.Circuits.Boolean.Iteration.hitRecord`, + `Cslib.Circuits.Boolean.Iteration.hitIndex`, + `Cslib.Circuits.Boolean.Iteration.hitPayload`: a flagged checkpoint-hit record and its time and + payload projections. * `Cslib.Circuits.Boolean.Iteration.finishHit`: the state reached from the last flagged hit. ## Main results @@ -66,6 +70,7 @@ def lookupOr (keys : Fin M → BitString k) (values : Fin M → BitString v) (ke BitString v := fun bit => decide (∃ j, keys j = key ∧ values j bit = true) +/-- With injective keys, `lookupOr` returns the value at the matching entry. -/ theorem lookupOr_of_eq {keys : Fin M → BitString k} (values : Fin M → BitString v) (hkeys : Function.Injective keys) {j : Fin M} {key : BitString k} (h : keys j = key) : lookupOr keys values key = values j := by @@ -77,6 +82,7 @@ theorem lookupOr_of_eq {keys : Fin M → BitString k} (values : Fin M → BitStr rwa [hkeys (hi.trans h.symm)] at hv · exact fun hv => ⟨j, h, hv⟩ +/-- When `key` is absent from `keys`, `lookupOr` returns the all-false bit string. -/ theorem lookupOr_of_forall_ne {keys : Fin M → BitString k} (values : Fin M → BitString v) {key : BitString k} (h : ∀ j, keys j ≠ key) : lookupOr keys values key = fun _ => false := by funext bit @@ -129,14 +135,17 @@ def hitIndex (record : BitString (w + n + 1)) : BitVec w := def hitPayload (record : BitString (w + n + 1)) : BitString n := fun bit => record (Fin.natAdd w bit).succ +/-- Bit zero of `hitRecord` is the set hit flag `true`. -/ @[simp] theorem hitRecord_zero (index : ℕ) (payload : BitString n) : hitRecord (w := w) index payload 0 = true := rfl +/-- Reading `hitIndex` from `hitRecord index payload` recovers `BitVec.ofNat w index`. -/ @[simp] theorem hitIndex_hitRecord (index : ℕ) (payload : BitString n) : hitIndex (hitRecord (w := w) index payload) = BitVec.ofNat w index := by simpa only [hitIndex, hitRecord, Fin.cons_succ, Fin.append_left] using word_getLsbD (BitVec.ofNat w index) +/-- Reading `hitPayload` from `hitRecord index payload` recovers `payload`. -/ @[simp] theorem hitPayload_hitRecord (index : ℕ) (payload : BitString n) : hitPayload (hitRecord (w := w) index payload) = payload := by funext bit diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/SparseDisplacement.lean b/Complexity/Computability/Circuit/Boolean/Iteration/SparseDisplacement.lean index 89a5a6171..1619e308a 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/SparseDisplacement.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/SparseDisplacement.lean @@ -103,6 +103,7 @@ def displacementCuts (h : BitVec n → BitVec n) : Finset ℕ := (Finset.range (2 ^ n)).filter fun i => displacement h (BitVec.ofNat n (i + 1)) ≠ displacement h (BitVec.ofNat n i) +/-- The displacement of `h` changes across `x` and `x + 1` if and only if `h (x + 1) ≠ h x + 1`. -/ theorem displacement_change_iff (h : BitVec n → BitVec n) (x : BitVec n) : displacement h (x + 1) ≠ displacement h x ↔ h (x + 1) ≠ h x + 1 := by unfold displacement diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/SparseNavigation.lean b/Complexity/Computability/Circuit/Boolean/Iteration/SparseNavigation.lean index be7f2e1b2..94c33b9d8 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/SparseNavigation.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/SparseNavigation.lean @@ -125,6 +125,8 @@ private theorem cycleLabelVisits_period (f : BitVec n → BitVec n) (hf : Functi rw [chart_ofNat_toNat (cycleLength_le_words f y), Nat.mod_eq_of_lt hwide, cycleLength_eq_minimalPeriod_of_mem_periodicPts f (hf.mem_periodicPts y)] +/-- For an injective word map `f`, the visit schedule constructed from the cycle labels of `x` and +`y` contains time `t` if and only if `f^[t] x = y`. -/ theorem cycleLabelVisits_spec (f : BitVec n → BitVec n) (hf : Function.Injective f) (x y : BitVec n) (t : ℕ) : f^[t] x = y ↔ visitScheduleContains @@ -211,6 +213,9 @@ theorem cycle_label_visit_circuit (f : BitVec n → BitVec n) obtain ⟨out, ho, hs⟩ := ((hx.union hy).trans hnav).exists_circuit_outputs exact ⟨out, ho, by lia⟩ +/-- Every permutation `f` of `BitVec n` has a circuit of size at most `1200 * (n + 3) * (r + 1)` +computing the visit schedule between its two `n`-bit inputs from their cycle labels, where `r` is +the number of disagreements of `f` with the unit increment. -/ theorem sparse_counter_visit_circuit (f : Equiv.Perm (BitVec n)) : ∃ out : Circuit Boolean.signature (n + n) (visitScheduleWidth n), out.Computes Boolean.interpretation (fun z => diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/SparseTime.lean b/Complexity/Computability/Circuit/Boolean/Iteration/SparseTime.lean index d2fc280d6..2060bb39c 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/SparseTime.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/SparseTime.lean @@ -53,6 +53,9 @@ open Cslib.FunctionalGraph variable {n R : ℕ} +/-- Given a `CounterIntervalChart` with `R` runs for an injective map `f : BitVec n → BitVec n`, +iterating `f` by an `m`-bit input time on an `n`-bit input state has a Boolean circuit of size at +most `1000 * (n + 3) * (R + m)`. -/ theorem CounterIntervalChart.variable_time {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (hf : Function.Injective f) (m : ℕ) : ∃ out : Circuit Boolean.signature (n + m) n, diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/UniversalMap.lean b/Complexity/Computability/Circuit/Boolean/Iteration/UniversalMap.lean index 9cab08bde..7548f25dd 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/UniversalMap.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/UniversalMap.lean @@ -46,7 +46,12 @@ handled by the same hardwiring argument. * `Cslib.Circuits.Boolean.Iteration.Universal.Description`: straight-line program description held in the state of the universal step map. * `Cslib.Circuits.Boolean.Iteration.Universal.Config`: configuration of the universal step map. +* `Cslib.Circuits.Boolean.Iteration.Universal.read`: register lookup by natural-number index. * `Cslib.Circuits.Boolean.Iteration.Universal.step`: one step of the universal step map. +* `Cslib.Circuits.Boolean.Iteration.Universal.wireIndex`, + `Cslib.Circuits.Boolean.Iteration.Universal.describe`, + `Cslib.Circuits.Boolean.Iteration.Universal.start`: encoding a circuit into a program description + and initial universal configuration. ## Main results diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/VisitScheduleCircuits.lean b/Complexity/Computability/Circuit/Boolean/Iteration/VisitScheduleCircuits.lean index 8eb11d76f..79cecddbc 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/VisitScheduleCircuits.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/VisitScheduleCircuits.lean @@ -148,6 +148,7 @@ def visitScheduleCount (v : BitString (visitScheduleWidth n)) (T : ℕ) : ℕ := arithmeticProgressionCount (visitScheduleFirst v).toNat (visitSchedulePeriod v).toNat T else 0 +/-- `visitScheduleCount v T` counts the times `t ≤ T` satisfying `visitScheduleContains v t`. -/ theorem visitScheduleCount_spec (v : BitString (visitScheduleWidth n)) (T : ℕ) : Set.ncard {t : ℕ | t ≤ T ∧ visitScheduleContains v t} = visitScheduleCount v T := by unfold visitScheduleCount visitScheduleContains diff --git a/Complexity/Computability/Circuit/Boolean/Layered/Compile.lean b/Complexity/Computability/Circuit/Boolean/Layered/Compile.lean index 2a987a753..28a390a0d 100644 --- a/Complexity/Computability/Circuit/Boolean/Layered/Compile.lean +++ b/Complexity/Computability/Circuit/Boolean/Layered/Compile.lean @@ -24,6 +24,9 @@ Output selection is separate wiring, so an empty schedule preserves depth-zero c ## Main definitions +* `Cslib.Circuits.Boolean.Layered.carry`, `Cslib.Circuits.Boolean.Layered.prepareFirst`, + `Cslib.Circuits.Boolean.Layered.prepareSecond`, `Cslib.Circuits.Boolean.Layered.finish`: + per-node microlevel constructors for carrying wires and decomposing De Morgan gates into NANDs. * `Cslib.Circuits.Boolean.Layered.prepareLayer`: prepare one depth's NAND intermediates. * `Cslib.Circuits.Boolean.Layered.finishLayer`: finish gates at that depth and carry older wires. * `Cslib.Circuits.Boolean.Layered.schedule`: two consecutive layers per original depth. @@ -110,15 +113,18 @@ abbrev encCompiled : List (List Node) × List ℕ ↪ List Bool := Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList encNode)) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) +/-- `compile` preserves the designated output wire indices unchanged. -/ @[simp] theorem compile_outputs (inputCount : ℕ) (code : List (Op × List ℕ) × List ℕ) : (compile inputCount code).2 = code.2 := rfl +/-- Every preparation layer has width `inputCount + 3 * gates.length`. -/ @[simp] theorem length_prepareLayer (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (level : ℕ) : (prepareLayer inputCount gates depths level).length = inputCount + 3 * gates.length := by simp only [prepareLayer, List.length_append, List.length_map, List.length_range] omega +/-- Every finishing layer has width `inputCount + 3 * gates.length`. -/ @[simp] theorem length_finishLayer (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (level : ℕ) : (finishLayer inputCount gates depths level).length = inputCount + 3 * gates.length := by @@ -126,9 +132,12 @@ abbrev encCompiled : List (List Node) × List ℕ ↪ List Bool := List.length_replicate] omega +/-- At depth zero, the compiled schedule is empty. -/ @[simp] theorem schedule_zero (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) : schedule inputCount gates depths 0 = [] := rfl +/-- Scheduling `depth + 1` levels appends the preparation and finishing layers for level +`depth + 1`. -/ theorem schedule_succ (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (depth : ℕ) : schedule inputCount gates depths (depth + 1) = schedule inputCount gates depths depth ++ diff --git a/Complexity/Computability/Circuit/Boolean/Layered/Padding.lean b/Complexity/Computability/Circuit/Boolean/Layered/Padding.lean index eec7163b9..b53092210 100644 --- a/Complexity/Computability/Circuit/Boolean/Layered/Padding.lean +++ b/Complexity/Computability/Circuit/Boolean/Layered/Padding.lean @@ -41,6 +41,7 @@ namespace Cslib.Circuits.Boolean.Layered /-- Copy every wire in order, including the empty row when `width = 0`. -/ def identityLayer (width : ℕ) : List Node := (List.range width).map Node.copy +/-- An identity layer of width `width` has `width` nodes. -/ @[simp] theorem length_identityLayer (width : ℕ) : (identityLayer width).length = width := by simp [identityLayer] @@ -50,6 +51,7 @@ private theorem valid_identityLayer (width : ℕ) : obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hnode exact List.mem_range.mp hi +/-- Evaluating an identity layer of matching width returns the input row unchanged. -/ @[simp] theorem evalLayer_identityLayer (inputs : List Bool) : evalLayer inputs (identityLayer inputs.length) = inputs := by apply List.ext_getElem @@ -57,12 +59,14 @@ private theorem valid_identityLayer (width : ℕ) : · intro i hi hi' simp [evalLayer, identityLayer, Node.eval, hi'] +/-- Evaluating any number of replicated identity layers returns the input row unchanged. -/ @[simp] theorem eval_replicate_identityLayer (inputs : List Bool) (count : ℕ) : eval inputs (List.replicate count (identityLayer inputs.length)) = inputs := by induction count with | zero => rfl | succ count ih => simp only [List.replicate_succ, eval_cons, evalLayer_identityLayer, ih] +/-- Replicated identity layers of width `width` have output width `width`. -/ @[simp] theorem outputWidth_replicate_identityLayer (width count : ℕ) : outputWidth width (List.replicate count (identityLayer width)) = width := by induction count with @@ -82,15 +86,18 @@ private theorem wellFormed_replicate_identityLayer (width count : ℕ) : def padTo (inputCount target : ℕ) (layers : List (List Node)) : List (List Node) := layers ++ List.replicate (target - layers.length) (identityLayer (outputWidth inputCount layers)) +/-- Padding to `target` produces `max layers.length target` layers. -/ @[simp] theorem length_padTo (inputCount target : ℕ) (layers : List (List Node)) : (padTo inputCount target layers).length = max layers.length target := by simp only [padTo, List.length_append, List.length_replicate] omega +/-- When `layers.length ≤ target`, padding to `target` produces exactly `target` layers. -/ theorem length_padTo_of_le (inputCount target : ℕ) (layers : List (List Node)) (h : layers.length ≤ target) : (padTo inputCount target layers).length = target := by rw [length_padTo, max_eq_right h] +/-- When `target ≤ layers.length`, `padTo` leaves the schedule unchanged. -/ @[simp] theorem padTo_eq_self (inputCount target : ℕ) (layers : List (List Node)) (h : target ≤ layers.length) : padTo inputCount target layers = layers := by simp [padTo, Nat.sub_eq_zero_of_le h] @@ -100,10 +107,12 @@ theorem length_padTo_of_le (inputCount target : ℕ) (layers : List (List Node)) eval inputs (padTo inputs.length target layers) = eval inputs layers := by rw [padTo, eval_append, ← length_eval, eval_replicate_identityLayer] +/-- Padding preserves the output width of a layered schedule. -/ @[simp] theorem outputWidth_padTo (inputCount target : ℕ) (layers : List (List Node)) : outputWidth inputCount (padTo inputCount target layers) = outputWidth inputCount layers := by rw [padTo, outputWidth_append, outputWidth_replicate_identityLayer] +/-- Padding a well-formed layered schedule preserves `WellFormed`. -/ theorem WellFormed.padTo {inputCount : ℕ} {layers : List (List Node)} (h : WellFormed inputCount layers) (target : ℕ) : WellFormed inputCount (padTo inputCount target layers) := diff --git a/Complexity/Computability/Circuit/Boolean/MassProduction/Basic.lean b/Complexity/Computability/Circuit/Boolean/MassProduction/Basic.lean index 087c92834..e4b082697 100644 --- a/Complexity/Computability/Circuit/Boolean/MassProduction/Basic.lean +++ b/Complexity/Computability/Circuit/Boolean/MassProduction/Basic.lean @@ -26,8 +26,12 @@ versions; the exponential-range theorem requires further constructions. ## Main definitions * `Cslib.Circuits.Boolean.MassProduction.massComplexity`: minimum cost of independent copies. +* `Cslib.Circuits.Boolean.MassProduction.rationalCopyBudget`: discrete copy budget + `2 ^ (numerator * inputs / denominator)`. * `Cslib.Circuits.Boolean.MassProduction.MassProductionBound`: the bound at one input length. -* `Cslib.Circuits.Boolean.MassProduction.MassProducesAt`: the eventual rational-rate statement. +* `Cslib.Circuits.Boolean.MassProduction.MassProducesAt`, + `Cslib.Circuits.Boolean.MassProduction.MassProducesAtAllLengths`: the eventual and all-length + rational-rate statements. * `Cslib.Circuits.Boolean.MassProduction.ExponentialMassProduction`: the all-length statement for every fixed nonnegative rational exponent below one. @@ -78,6 +82,7 @@ theorem massComplexity_le_complexity : exists_computes_size_eq_complexity (I := interpretation) (f := directProduct f k) exact massComplexity_le_iff.mpr ⟨c, hc, (Program.cost_nonconstantCost_le _).trans hsize.le⟩ +/-- Evaluating zero copies of `f` has mass complexity zero. -/ @[simp] theorem massComplexity_zero : massComplexity f 0 = 0 := ecomplexityFrom_directProduct_zero @@ -100,11 +105,13 @@ theorem massComplexity_comp_wiring_le {p : ℕ} (select : Fin n → Fin p) (k : def rationalCopyBudget (numerator denominator inputs : ℕ) : ℕ := 2 ^ (numerator * inputs / denominator) +/-- `rationalCopyBudget` is monotone in the numerator. -/ theorem rationalCopyBudget_mono_numerator {small large denominator inputs : ℕ} (h : small ≤ large) : rationalCopyBudget small denominator inputs ≤ rationalCopyBudget large denominator inputs := Nat.pow_le_pow_right (by decide) (Nat.div_le_div_right (Nat.mul_le_mul_right inputs h)) +/-- `rationalCopyBudget` is monotone in the input length. -/ theorem rationalCopyBudget_mono_inputs {numerator denominator small large : ℕ} (h : small ≤ large) : rationalCopyBudget numerator denominator small ≤ diff --git a/Complexity/Computability/Circuit/Boolean/MassProduction/FineParameters.lean b/Complexity/Computability/Circuit/Boolean/MassProduction/FineParameters.lean index 842b72a43..9b9c08925 100644 --- a/Complexity/Computability/Circuit/Boolean/MassProduction/FineParameters.lean +++ b/Complexity/Computability/Circuit/Boolean/MassProduction/FineParameters.lean @@ -84,6 +84,7 @@ def depth (n : ℕ) : ℕ := variable {num den X} +/-- When `num ≤ den`, the prefix width is at most the input length `n`. -/ theorem prefixWidth_le (hnd : num ≤ den) (n : ℕ) : prefixWidth num den X n ≤ n := by rcases Nat.eq_zero_or_pos den with rfl | hden · simp [prefixWidth] @@ -93,6 +94,7 @@ theorem prefixWidth_le (hnd : num ≤ den) (n : ℕ) : prefixWidth num den X n nlinarith _ = (X + 1) * den * n := by ring +/-- When `num ≤ den`, the prefix width and suffix width sum to `n`. -/ theorem prefixWidth_add_suffixWidth (hnd : num ≤ den) (n : ℕ) : prefixWidth num den X n + suffixWidth num den X n = n := Nat.add_sub_of_le (prefixWidth_le hnd n) @@ -115,9 +117,11 @@ private theorem three_le_dimension : 3 ≤ dimension num den X := by unfold dimension omega +/-- The code dimension is at most `2 ^ blockWidth`. -/ theorem dimension_le_two_pow_blockWidth : dimension num den X ≤ 2 ^ blockWidth num den X := Nat.le_pow_clog (by norm_num) _ +/-- The block width is positive. -/ theorem blockWidth_pos : 0 < blockWidth num den X := by unfold blockWidth have h := three_le_dimension (num := num) (den := den) (X := X) diff --git a/Complexity/Computability/Circuit/Boolean/MassProduction/FineStatement.lean b/Complexity/Computability/Circuit/Boolean/MassProduction/FineStatement.lean index db8470c55..76682e108 100644 --- a/Complexity/Computability/Circuit/Boolean/MassProduction/FineStatement.lean +++ b/Complexity/Computability/Circuit/Boolean/MassProduction/FineStatement.lean @@ -96,6 +96,7 @@ theorem rationalCopyBudget_le_two_pow (n : ℕ) : rationalCopyBudget num den n ≤ 2 ^ (num * n / den + 1) := Nat.pow_le_pow_right (by norm_num) (Nat.le_succ _) +/-- The core fine bound implies the rational-rate statement over `rationalCopyBudget`. -/ theorem FineMassProducesThrough.fineMassProducesAt (h : FineMassProducesThrough num den) : FineMassProducesAt num den := by intro P _ diff --git a/Complexity/Computability/Circuit/Boolean/MassProduction/Pipeline/Circuit.lean b/Complexity/Computability/Circuit/Boolean/MassProduction/Pipeline/Circuit.lean index 96f27b060..c7bd1cdfc 100644 --- a/Complexity/Computability/Circuit/Boolean/MassProduction/Pipeline/Circuit.lean +++ b/Complexity/Computability/Circuit/Boolean/MassProduction/Pipeline/Circuit.lean @@ -41,6 +41,14 @@ running time of the circuit constructors. ## Main definitions +* `Cslib.Circuits.Boolean.MassProduction.Pipeline.slotEquiv`, + `Cslib.Circuits.Boolean.MassProduction.Pipeline.slotKey`: slot numbering and lookup keys. +* `Cslib.Circuits.Boolean.MassProduction.Pipeline.metaWidth`, + `Cslib.Circuits.Boolean.MassProduction.Pipeline.stateWidth`, + `Cslib.Circuits.Boolean.MassProduction.Pipeline.metadata`, + `Cslib.Circuits.Boolean.MassProduction.Pipeline.prefixWires`, + `Cslib.Circuits.Boolean.MassProduction.Pipeline.incidenceKey`: wire widths, prefix metadata, and + incidence lookup keys. * `Cslib.Circuits.Boolean.MassProduction.Pipeline.recoveryCircuit`: stages one to five. * `Cslib.Circuits.Boolean.MassProduction.Pipeline.lineSums`: stage six, as a function. * `Cslib.Circuits.Boolean.MassProduction.Pipeline.slotResource`: the resource of a slot. @@ -103,6 +111,7 @@ def slotEquiv : Fin copies × BitString (ℓ * b) ≃ Fin (copies * 2 ^ (ℓ * b def slotKey (q : Fin (copies * 2 ^ (ℓ * b))) : BitString (Nat.clog 2 copies + ℓ * b) := Fin.append (indexBits (slotEquiv.symm q).1) (slotEquiv.symm q).2 +/-- The key of `slotEquiv (c, y)` is the binary index of `c` followed by `y`. -/ theorem slotKey_slotEquiv (c : Fin copies) (y : BitString (ℓ * b)) : slotKey (slotEquiv (c, y)) = Fin.append (indexBits c) y := by simp only [slotKey, Equiv.symm_apply_apply] @@ -124,6 +133,7 @@ private theorem append_eq_append_iff {α : Type*} {m n : ℕ} {u u' : Fin m → · rintro ⟨rfl, rfl⟩ rfl +/-- Distinct slots have distinct lookup keys. -/ theorem slotKey_injective : Function.Injective (slotKey (copies := copies) (ℓ := ℓ) (b := b)) := by intro q q' h rw [slotKey, slotKey, append_eq_append_iff] at h diff --git a/Complexity/Computability/Circuit/Boolean/MassProduction/Scheduler/Basic.lean b/Complexity/Computability/Circuit/Boolean/MassProduction/Scheduler/Basic.lean index f0ade5afe..de999ddc8 100644 --- a/Complexity/Computability/Circuit/Boolean/MassProduction/Scheduler/Basic.lean +++ b/Complexity/Computability/Circuit/Boolean/MassProduction/Scheduler/Basic.lean @@ -31,6 +31,10 @@ the number of true flags (`eq_true_iff_lt_card_of_sorted`). Gate counts are synthesis budgets: they count every gate, including constants, and do not certify the running time of any construction. +## Main definitions + +* `Cslib.Circuits.Boolean.prefixOr`: the disjunction of the first `j + 1` of `r` functions. + ## Main results * `Cslib.Circuits.Synthesis.prefixOr`: all prefix disjunctions of `r` available functions. diff --git a/Complexity/Computability/Circuit/Boolean/MassProduction/Scheduler/Phase.lean b/Complexity/Computability/Circuit/Boolean/MassProduction/Scheduler/Phase.lean index 9fad80abf..27f2a3be9 100644 --- a/Complexity/Computability/Circuit/Boolean/MassProduction/Scheduler/Phase.lean +++ b/Complexity/Computability/Circuit/Boolean/MassProduction/Scheduler/Phase.lean @@ -29,10 +29,24 @@ state good (`good_next`). ## Main definitions +* `Cslib.Circuits.Boolean.MassProduction.Scheduler.pending`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.accepted`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.acceptedLines`: positions and lines of pending + and accepted requests. * `Cslib.Circuits.Boolean.MassProduction.Scheduler.candidate`: the bits of a candidate point. -* `Cslib.Circuits.Boolean.MassProduction.Scheduler.clean`: the clean flags. -* `Cslib.Circuits.Boolean.MassProduction.Scheduler.chosen`: the first successful entry. -* `Cslib.Circuits.Boolean.MassProduction.Scheduler.next`: the state after the phase. +* `Cslib.Circuits.Boolean.MassProduction.Scheduler.occupied`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.duplicate`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.clean`: conflict and cleanliness predicates. +* `Cslib.Circuits.Boolean.MassProduction.Scheduler.success`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.chosen`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.flag`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.newLine`: menu selection and selected candidate + flags and lines. +* `Cslib.Circuits.Boolean.MassProduction.Scheduler.enriched`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.flagKey`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.sortedPending`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.next`: sorting pending records by cleanliness + and forming the state after the phase. ## Main results diff --git a/Complexity/Computability/Circuit/Boolean/MassProduction/Scheduler/State.lean b/Complexity/Computability/Circuit/Boolean/MassProduction/Scheduler/State.lean index 547dcaaf1..fd4fadb44 100644 --- a/Complexity/Computability/Circuit/Boolean/MassProduction/Scheduler/State.lean +++ b/Complexity/Computability/Circuit/Boolean/MassProduction/Scheduler/State.lean @@ -33,10 +33,20 @@ records are accepted, sorting by label restores the original order: each label h ## Main definitions -* `Cslib.Circuits.Boolean.MassProduction.Scheduler.width`: the record width. +* `Cslib.Circuits.Boolean.MassProduction.Scheduler.width`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.labelBit`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.targetBit`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.lineBit`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.label`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.target`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.line`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.encode`: the record layout, field projections, + and request label encoding. * `Cslib.Circuits.Boolean.MassProduction.Scheduler.Good`: the scheduler invariant. * `Cslib.Circuits.Boolean.MassProduction.Scheduler.initialSubstitution`: the initial records. -* `Cslib.Circuits.Boolean.MassProduction.Scheduler.finalOutput`: lines in original order. +* `Cslib.Circuits.Boolean.MassProduction.Scheduler.sortedByLabel`, + `Cslib.Circuits.Boolean.MassProduction.Scheduler.finalOutput`: sorting records by label and + reading lines in original order. ## Main results diff --git a/Complexity/Computability/Circuit/Boolean/MassProduction/Uhlig.lean b/Complexity/Computability/Circuit/Boolean/MassProduction/Uhlig.lean index dba2c0d01..773b2b0f7 100644 --- a/Complexity/Computability/Circuit/Boolean/MassProduction/Uhlig.lean +++ b/Complexity/Computability/Circuit/Boolean/MassProduction/Uhlig.lean @@ -77,6 +77,7 @@ open Filter Uhlig /-! ### The finite recursion -/ +/-- `layerOverhead p w` is monotone in the suffix width `w`. -/ theorem layerOverhead_mono {p w w' : ℕ} (h : w ≤ w') : layerOverhead p w ≤ layerOverhead p w' := by unfold layerOverhead gcongr diff --git a/Complexity/Computability/Circuit/Boolean/MassProduction/Uhlig/Layer.lean b/Complexity/Computability/Circuit/Boolean/MassProduction/Uhlig/Layer.lean index aadbd45e1..277937f1f 100644 --- a/Complexity/Computability/Circuit/Boolean/MassProduction/Uhlig/Layer.lean +++ b/Complexity/Computability/Circuit/Boolean/MassProduction/Uhlig/Layer.lean @@ -35,7 +35,16 @@ does not certify the running time of any circuit constructor. * `Cslib.Circuits.Boolean.MassProduction.Uhlig.restriction`: the restrictions of `f` to prefixes, numbered by `BitString.equivFin`. * `Cslib.Circuits.Boolean.MassProduction.Uhlig.resource`: Uhlig's resource functions. -* `Cslib.Circuits.Boolean.MassProduction.Uhlig.layerOverhead`: the per-pair gate budget. +* `Cslib.Circuits.Boolean.MassProduction.Uhlig.rank`, + `Cslib.Circuits.Boolean.MassProduction.Uhlig.pairCopy`, + `Cslib.Circuits.Boolean.MassProduction.Uhlig.pairWires`, + `Cslib.Circuits.Boolean.MassProduction.Uhlig.pairSelect`, + `Cslib.Circuits.Boolean.MassProduction.Uhlig.routedBit`, + `Cslib.Circuits.Boolean.MassProduction.Uhlig.decoded`: prefix ranking, pair wiring, suffix + routing, and resource decoding. +* `Cslib.Circuits.Boolean.MassProduction.Uhlig.selectorCost`, + `Cslib.Circuits.Boolean.MassProduction.Uhlig.layerOverhead`: the DNF selector cost and per-pair + gate budget. ## Main results @@ -69,6 +78,7 @@ def restriction (f : BooleanFunction (p + w)) (z : BitString w) (a : ℕ) : Bool def resource (f : BooleanFunction (p + w)) (j : ℕ) : BooleanFunction w := fun z => code (restriction f z) j +/-- At index `2 ^ p`, out of range of `p`-bit prefixes, `restriction f z (2 ^ p)` is `false`. -/ @[simp] theorem restriction_two_pow (f : BooleanFunction (p + w)) (z : BitString w) : restriction f z (2 ^ p) = false := by simp [restriction] @@ -97,6 +107,8 @@ def pairSelect (s : Fin 2) (j : ℕ) (q : BitString (p + p)) : Bool := ![first, second] s (BitString.equivFin p (q ∘ Fin.castAdd p)) (BitString.equivFin p (q ∘ Fin.natAdd p)) j +/-- Composing `pairSelect` with `pairWires i` selects code positions from the prefix ranks of the +two copies in pair `i`. -/ theorem pairSelect_comp_pairWires (s : Fin 2) (j : ℕ) (i : Fin t) (x : BitString (2 * t * (p + w))) : pairSelect s j (x ∘ pairWires i) = diff --git a/Complexity/Computability/Circuit/Boolean/Modular/InnerProduct/PolyTime.lean b/Complexity/Computability/Circuit/Boolean/Modular/InnerProduct/PolyTime.lean index b49430fd1..6dd1c2078 100644 --- a/Complexity/Computability/Circuit/Boolean/Modular/InnerProduct/PolyTime.lean +++ b/Complexity/Computability/Circuit/Boolean/Modular/InnerProduct/PolyTime.lean @@ -22,6 +22,10 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Na Unary array count and word width generate all block selectors, complete product circuits and the balanced sum. Binary wire numbers and every generated code list are charged. +## Main definitions + +* `Cslib.Circuits.Boolean.Modular.innerProductCode`: raw circuit code for the modular inner product. + ## Main results * `Cslib.Circuits.Boolean.Modular.innerProductCode_eq_code`: exact raw and typed code agreement. diff --git a/Complexity/Computability/Circuit/Boolean/Modular/Multiply/PolyTime.lean b/Complexity/Computability/Circuit/Boolean/Modular/Multiply/PolyTime.lean index 314df0587..eaebe0826 100644 --- a/Complexity/Computability/Circuit/Boolean/Modular/Multiply/PolyTime.lean +++ b/Complexity/Computability/Circuit/Boolean/Modular/Multiply/PolyTime.lean @@ -23,6 +23,10 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Na All shifted partial products, balanced carry-save gates and the final adder are generated from unary width. The output is the full existing circuit code, including unused fallback gates. +## Main definitions + +* `Cslib.Circuits.Boolean.Modular.multiplyCode`: raw circuit code for the modular multiplier. + ## Main results * `Cslib.Circuits.Boolean.Modular.multiplyCode_eq_code`: exact code agreement. diff --git a/Complexity/Computability/Circuit/Boolean/Modular/PartialProduct/PolyTime.lean b/Complexity/Computability/Circuit/Boolean/Modular/PartialProduct/PolyTime.lean index aaf6ab129..a7bdab35a 100644 --- a/Complexity/Computability/Circuit/Boolean/Modular/PartialProduct/PolyTime.lean +++ b/Complexity/Computability/Circuit/Boolean/Modular/PartialProduct/PolyTime.lean @@ -23,6 +23,11 @@ The complete shifted word is generated from unary width and shift. Every emitted wire is charged. Out-of-range raw shifts have total behavior; the exact circuit theorem uses a valid shift. +## Main definitions + +* `Cslib.Circuits.Boolean.Modular.partialProductCode`: raw circuit code for a shifted partial + product. + ## Main results * `Cslib.Circuits.Boolean.Modular.partialProductCode_eq_code`: exact typed-circuit agreement. diff --git a/Complexity/Computability/Circuit/Boolean/Modular/Subtract.lean b/Complexity/Computability/Circuit/Boolean/Modular/Subtract.lean index 2eadad95a..970ff597a 100644 --- a/Complexity/Computability/Circuit/Boolean/Modular/Subtract.lean +++ b/Complexity/Computability/Circuit/Boolean/Modular/Subtract.lean @@ -23,6 +23,7 @@ discards the final carry, so underflow wraps modulo `2 ^ w` instead of truncated * `Cslib.Circuits.Boolean.Modular.val_eval_subtract`: exact modular subtraction on all words. * `Cslib.Circuits.Boolean.Modular.depth_subtract_le`: depth at most `8 + 2 * clog 2 (w + 1)`. +* `Cslib.Circuits.Boolean.Modular.size_subtract_le`: size at most `21 * (w + 1) ^ 2`. ## References @@ -101,6 +102,7 @@ theorem val_eval_subtract (a b : BitString w) : rw [hv] at hm exact (Nat.mod_eq_of_lt (BitString.equivFin w _).isLt).symm.trans hm +/-- The depth of `subtract w` is at most `8 + 2 * Nat.clog 2 (w + 1)`. -/ theorem depth_subtract_le (w : ℕ) : (subtract w).depth ≤ 8 + 2 * Nat.clog 2 (w + 1) := by have h := (Circuit.depth_comp_le (carryLookahead w) (subtractInputs w)).trans @@ -109,6 +111,7 @@ theorem depth_subtract_le (w : ℕ) : simp only [Circuit.depth_wiring, zero_add] omega +/-- The size of `subtract w` is at most `21 * (w + 1) ^ 2`. -/ theorem size_subtract_le (w : ℕ) : (subtract w).size ≤ 21 * (w + 1) ^ 2 := by have h := size_carryLookahead_le w simp only [subtract, Circuit.size_comp, Circuit.size_wiring, size_subtractInputs] diff --git a/Complexity/Computability/Circuit/Boolean/Modular/Subtract/PolyTime.lean b/Complexity/Computability/Circuit/Boolean/Modular/Subtract/PolyTime.lean index 737de25fb..7b5921b7f 100644 --- a/Complexity/Computability/Circuit/Boolean/Modular/Subtract/PolyTime.lean +++ b/Complexity/Computability/Circuit/Boolean/Modular/Subtract/PolyTime.lean @@ -22,6 +22,10 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Na The complete complement-plus-carry construction is generated from unary width. All circuit gates, wire references and output selectors are charged. +## Main definitions + +* `Cslib.Circuits.Boolean.Modular.subtractCode`: raw circuit code for modular subtraction. + ## Main results * `Cslib.Circuits.Boolean.Modular.subtractCode_eq_code`: exact generated code. diff --git a/Complexity/Computability/Circuit/Boolean/SemiCircuit/Equation.lean b/Complexity/Computability/Circuit/Boolean/SemiCircuit/Equation.lean index c8802c8ee..5fa25de33 100644 --- a/Complexity/Computability/Circuit/Boolean/SemiCircuit/Equation.lean +++ b/Complexity/Computability/Circuit/Boolean/SemiCircuit/Equation.lean @@ -26,7 +26,8 @@ terms (`affEqn`, `affEqn_holds`). * `Cslib.Circuits.Boolean.SemiCircuit.Equation`: equations, with `Equation.Holds` and `Equation.subst`. -* `Cslib.Circuits.Boolean.SemiCircuit.affEqn`: the equation of an affine gate. +* `Cslib.Circuits.Boolean.SemiCircuit.addArg`, + `Cslib.Circuits.Boolean.SemiCircuit.affEqn`: the equation of an affine gate. ## Main results @@ -75,6 +76,8 @@ private theorem sum_symmDiff_singleton (s : Finset ℕ) (t : ℕ) (val : ℕ → add_zero] · rw [Finset.sum_insert ht, add_comm] +/-- An element belongs to `s ∆ {t}` if and only if its membership in `s` differs from equality +with `t`. -/ theorem mem_symmDiff_singleton {s : Finset ℕ} {t z : ℕ} : z ∈ s ∆ {t} ↔ (z ∈ s ↔ z ≠ t) := by rw [symmDiff_singleton_eq] by_cases hz : z = t @@ -95,6 +98,7 @@ namespace Equation def Holds (E : Equation) (val : ℕ → Bool) : Prop := ∑ i ∈ E.terms, val i = E.rhs +/-- Decidability of whether an equation holds under a value assignment. -/ instance (E : Equation) (val : ℕ → Bool) : Decidable (E.Holds val) := inferInstanceAs (Decidable (_ = _)) @@ -129,6 +133,8 @@ theorem holds_subst {E : Equation} {v : ℕ} {ℓ : Lit} {val : ℕ → Bool} revert S r x c; decide · exact Iff.rfl +/-- Rerouting `v` to `ℓ` preserves membership in `E.terms` for any node distinct from `v` and not +read by `ℓ`. -/ theorem mem_subst_of_ne {E : Equation} {v : ℕ} {ℓ : Lit} {z : ℕ} (hzv : z ≠ v) (hzℓ : ℓ.arg ≠ .node z) : z ∈ (E.subst v ℓ).terms ↔ z ∈ E.terms := by unfold subst @@ -140,6 +146,8 @@ theorem mem_subst_of_ne {E : Equation} {v : ℕ} {ℓ : Lit} {z : ℕ} (hzv : z exact ⟨fun h => h.2 hzt, fun h => ⟨fun _ => hzt, fun _ => h⟩⟩ · exact Iff.rfl +/-- Every term of `E.subst v ℓ` either already belongs to `E.terms` or arises from `v ∈ E.terms` +with `ℓ` reading that node. -/ theorem mem_of_mem_subst {E : Equation} {v : ℕ} {ℓ : Lit} {z : ℕ} (h : z ∈ (E.subst v ℓ).terms) : z ∈ E.terms ∨ (v ∈ E.terms ∧ ℓ.arg = .node z) := by unfold subst at h @@ -151,6 +159,7 @@ theorem mem_of_mem_subst {E : Equation} {v : ℕ} {ℓ : Lit} {z : ℕ} · exact Or.inl (Finset.mem_of_mem_erase ((mem_symmDiff_singleton.1 h).2 hzt)) · exact Or.inl h +/-- Rerouting a variable in an equation does not increase the number of terms. -/ theorem card_subst_le {E : Equation} {v : ℕ} {ℓ : Lit} : (E.subst v ℓ).terms.card ≤ E.terms.card := by unfold subst @@ -164,6 +173,7 @@ theorem card_subst_le {E : Equation} {v : ℕ} {ℓ : Lit} : _ = E.terms.card := by omega · exact le_rfl +/-- Rerouting `v` to a literal not reading `v` eliminates `v` from the terms of the equation. -/ theorem notMem_subst {E : Equation} {v : ℕ} {ℓ : Lit} (hℓ : ℓ.arg ≠ .node v) : v ∉ (E.subst v ℓ).terms := by intro h @@ -175,10 +185,12 @@ theorem notMem_subst {E : Equation} {v : ℕ} {ℓ : Lit} (hℓ : ℓ.arg ≠ .n exact Finset.notMem_erase v _ ((mem_symmDiff_singleton.1 h).2 ht) · exact hv h +/-- Rerouting a variable that does not occur in `E.terms` leaves the equation unchanged. -/ theorem subst_of_notMem {E : Equation} {v : ℕ} {ℓ : Lit} (h : v ∉ E.terms) : E.subst v ℓ = E := by unfold subst rw [ite_eq_right h] +/-- Whether `E` holds depends only on the values assigned to `E.terms`. -/ theorem holds_congr {E : Equation} {val val' : ℕ → Bool} (h : ∀ i ∈ E.terms, val i = val' i) : E.Holds val ↔ E.Holds val' := by unfold Holds @@ -233,6 +245,7 @@ private theorem sum_addArg (p : Finset ℕ × Bool) (b : Bool) (a : Arg) (val : generalize ∑ i ∈ p.1, val i = s; generalize p.2 = r revert s v r; decide +/-- Any term in `(addArg p b a).1` either belongs to `p.1` or is the node read by `a`. -/ theorem mem_addArg {p : Finset ℕ × Bool} {b : Bool} {a : Arg} {z : ℕ} (h : z ∈ (addArg p b a).1) : z ∈ p.1 ∨ a = .node z := by unfold addArg at h @@ -262,6 +275,8 @@ def affEqn (g : Gate) (J : ℕ) : Equation := g.right ⟨p.1, p.2⟩ +/-- For an affine gate `g`, the equation `affEqn g J` holds under `val` if and only if +`val J = g.eval val`. -/ theorem affEqn_holds {g : Gate} (hg : IsAffineOp g.op) (J : ℕ) (val : ℕ → Bool) : (affEqn g J).Holds val ↔ val J = g.eval val := by unfold affEqn Equation.Holds @@ -289,6 +304,7 @@ theorem affEqn_holds {g : Gate} (hg : IsAffineOp g.op) (J : ℕ) (val : ℕ → generalize g.op true true = d revert s r j a b c d; decide +/-- Every term of `affEqn g J` is either the output wire `J` or a node read by `g`. -/ theorem mem_affEqn {g : Gate} {J z : ℕ} (h : z ∈ (affEqn g J).terms) : z = J ∨ g.Reads z := by unfold affEqn at h rcases mem_addArg h with h | h @@ -297,6 +313,7 @@ theorem mem_affEqn {g : Gate} {J z : ℕ} (h : z ∈ (affEqn g J).terms) : z = J · exact Or.inr (Or.inl h) · exact Or.inr (Or.inr h) +/-- The equation `affEqn g J` of a binary gate has at most three terms. -/ theorem card_affEqn_le (g : Gate) (J : ℕ) : (affEqn g J).terms.card ≤ 3 := by unfold affEqn have h1 := card_addArg_le ({J}, g.op false false) (g.op true false ^^ g.op false false) g.left diff --git a/Complexity/Computability/Circuit/Boolean/SemiCircuit/Gate.lean b/Complexity/Computability/Circuit/Boolean/SemiCircuit/Gate.lean index 8c2cb0c93..48ef9b298 100644 --- a/Complexity/Computability/Circuit/Boolean/SemiCircuit/Gate.lean +++ b/Complexity/Computability/Circuit/Boolean/SemiCircuit/Gate.lean @@ -31,10 +31,16 @@ An affine operation that is neither constant nor a projection is XOR-type (`exis ## Main definitions * `Cslib.Circuits.Boolean.SemiCircuit.Arg`, `Cslib.Circuits.Boolean.SemiCircuit.Lit`, - `Cslib.Circuits.Boolean.SemiCircuit.Gate`: arguments, literals and gates. -* `Cslib.Circuits.Boolean.SemiCircuit.Gate.subst`: rerouting an internal value to a literal. + `Cslib.Circuits.Boolean.SemiCircuit.Gate`: arguments, literals and gates, with evaluation + (`Arg.eval`, `Lit.eval`, `Gate.eval`), constructors (`Lit.const`, `Lit.node`) and dependency + predicates (`Lit.Reads`, `Gate.Reads`). +* `Cslib.Circuits.Boolean.SemiCircuit.Arg.substArg`, + `Cslib.Circuits.Boolean.SemiCircuit.Lit.subst`, + `Cslib.Circuits.Boolean.SemiCircuit.Gate.substNeg`, + `Cslib.Circuits.Boolean.SemiCircuit.Gate.subst`: rerouting an internal value to a literal. * `Cslib.Circuits.Boolean.SemiCircuit.Gate.Degenerate`, - `Cslib.Circuits.Boolean.SemiCircuit.Gate.lit`: degenerate gates and the literal they compute. + `Cslib.Circuits.Boolean.SemiCircuit.Gate.lit`, + `Cslib.Circuits.Boolean.SemiCircuit.unaryLit`: degenerate gates and the literal they compute. * `Cslib.Circuits.Boolean.SemiCircuit.IsAffineOp`, `Cslib.Circuits.Boolean.SemiCircuit.IsUnaryOp`: affine operations and projections. @@ -76,8 +82,10 @@ def eval (val : ℕ → Bool) : Arg → Bool | const b => b | node i => val i +/-- Evaluating a constant argument returns that constant. -/ @[simp] theorem eval_const (val : ℕ → Bool) (b : Bool) : (const b).eval val = b := rfl +/-- Evaluating a node argument looks up its index in the assignment. -/ @[simp] theorem eval_node (val : ℕ → Bool) (i : ℕ) : (node i).eval val = val i := rfl /-- The argument `node v` replaced by the argument of the literal `ℓ`. -/ @@ -113,9 +121,11 @@ def const (b : Bool) : Lit := ⟨.const b, false⟩ /-- The literal `t ⊕ c` of the internal value `t`. -/ def node (t : ℕ) (c : Bool) : Lit := ⟨.node t, c⟩ +/-- Evaluating a constant literal returns that constant. -/ @[simp] theorem eval_const (b : Bool) (val : ℕ → Bool) : (const b).eval val = b := by simp [const, eval] +/-- Evaluating `Lit.node t c` returns `val t ^^ c`. -/ @[simp] theorem eval_node (t : ℕ) (c : Bool) (val : ℕ → Bool) : (node t c).eval val = (val t ^^ c) := rfl @@ -123,6 +133,7 @@ def node (t : ℕ) (c : Bool) : Lit := ⟨.node t, c⟩ def subst (o : Lit) (v : ℕ) (ℓ : Lit) : Lit := if o.arg = .node v then ⟨ℓ.arg, o.neg ^^ ℓ.neg⟩ else o +/-- Rerouting `v` to `ℓ` in a literal preserves its value whenever `val v = ℓ.eval val`. -/ theorem eval_subst {o : Lit} {v : ℕ} {ℓ : Lit} {val : ℕ → Bool} (h : val v = ℓ.eval val) : (o.subst v ℓ).eval val = o.eval val := by unfold subst @@ -135,11 +146,14 @@ theorem eval_subst {o : Lit} {v : ℕ} {ℓ : Lit} {val : ℕ → Bool} (h : val def Reads (o : Lit) (t : ℕ) : Prop := o.arg = .node t +/-- A literal's value depends only on the internal values it reads. -/ theorem eval_congr {o : Lit} {val val' : ℕ → Bool} (h : ∀ i, o.Reads i → val i = val' i) : o.eval val = o.eval val' := by unfold eval rw [Arg.eval_congr h] +/-- Rerouting `v` to a literal `ℓ` that does not read `v` yields a literal that does not read +`v`. -/ theorem not_reads_subst {o : Lit} {v : ℕ} {ℓ : Lit} (hℓ : ¬ ℓ.Reads v) : ¬ (o.subst v ℓ).Reads v := by unfold subst Reads @@ -147,6 +161,7 @@ theorem not_reads_subst {o : Lit} {v : ℕ} {ℓ : Lit} (hℓ : ¬ ℓ.Reads v) · exact hℓ · exact ho +/-- If `o.subst v ℓ` reads `z`, then either `o` reads `z` or `o` reads `v` and `ℓ` reads `z`. -/ theorem reads_of_reads_subst {o : Lit} {v : ℕ} {ℓ : Lit} {z : ℕ} (h : (o.subst v ℓ).Reads z) : o.Reads z ∨ (o.Reads v ∧ ℓ.Reads z) := by unfold subst Reads at * @@ -154,6 +169,7 @@ theorem reads_of_reads_subst {o : Lit} {v : ℕ} {ℓ : Lit} {z : ℕ} (h : (o.s · exact Or.inr ⟨ho, h⟩ · exact Or.inl h +/-- Rerouting `v` in a literal that does not read `v` leaves the literal unchanged. -/ theorem subst_of_not_reads {o : Lit} {v : ℕ} {ℓ : Lit} (h : ¬ o.Reads v) : o.subst v ℓ = o := ite_eq_right (show ¬ o.arg = .node v from h) @@ -189,6 +205,7 @@ def eval (g : Gate) (val : ℕ → Bool) : Bool := def Reads (g : Gate) (t : ℕ) : Prop := g.left = .node t ∨ g.right = .node t +/-- Decidability of whether a gate reads a given internal value. -/ instance (g : Gate) : DecidablePred g.Reads := fun _ => inferInstanceAs (Decidable (_ ∨ _)) @@ -210,6 +227,8 @@ def subst (g : Gate) (v : ℕ) (ℓ : Lit) : Gate where left := g.left.substArg v ℓ.arg right := g.right.substArg v ℓ.arg +/-- Replacing `node v` by `ℓ.arg` and XORing with `substNeg a v ℓ` preserves the value of `a` +when `val v = ℓ.eval val`. -/ theorem eval_substArg {a : Arg} {v : ℕ} {ℓ : Lit} {val : ℕ → Bool} (h : val v = ℓ.eval val) : ((a.substArg v ℓ.arg).eval val ^^ substNeg a v ℓ) = a.eval val := by unfold Arg.substArg substNeg @@ -237,11 +256,13 @@ private theorem eq_node_of_substArg_eq_node {a : Arg} {v z : ℕ} {target : Arg} · rw [ite_eq_left ha] at h; exact Or.inr ⟨ha, h⟩ · rw [ite_eq_right ha] at h; exact Or.inl h +/-- Rerouting `v` to `ℓ` preserves whether `g` reads any node `z ≠ v` not read by `ℓ`. -/ theorem reads_subst_of_ne {g : Gate} {v : ℕ} {ℓ : Lit} {z : ℕ} (hzv : z ≠ v) (hzℓ : ℓ.arg ≠ .node z) : (g.subst v ℓ).Reads z ↔ g.Reads z := by unfold Reads subst simp only [substArg_eq_node_of_ne hzv hzℓ] +/-- If `g.subst v ℓ` reads `z`, then either `g` reads `z` or `g` reads `v` and `ℓ` reads `z`. -/ theorem reads_of_reads_subst {g : Gate} {v : ℕ} {ℓ : Lit} {z : ℕ} (h : (g.subst v ℓ).Reads z) : g.Reads z ∨ (g.Reads v ∧ ℓ.arg = .node z) := by unfold Reads subst at * @@ -251,12 +272,14 @@ theorem reads_of_reads_subst {g : Gate} {v : ℕ} {ℓ : Lit} {z : ℕ} (h : (g. · exact Or.inl (Or.inr h') · exact Or.inr ⟨Or.inr h', h''⟩ +/-- Rerouting `v` to a literal not reading `v` eliminates `v` from the nodes read by the gate. -/ theorem not_reads_subst {g : Gate} {v : ℕ} {ℓ : Lit} (hℓ : ℓ.arg ≠ .node v) : ¬ (g.subst v ℓ).Reads v := by intro h simp only [Reads, subst, Arg.substArg] at h rcases h with h | h <;> split_ifs at h with h' <;> first | exact hℓ h | exact h' h +/-- Rerouting a variable not read by `g` leaves the gate's evaluation unchanged. -/ theorem eval_subst_of_not_reads {g : Gate} {v : ℕ} {ℓ : Lit} (h : ¬ g.Reads v) (val : ℕ → Bool) : (g.subst v ℓ).eval val = g.eval val := by unfold Reads at h @@ -275,6 +298,8 @@ theorem eval_subst_update {g : Gate} {v : ℕ} {ℓ : Lit} (hℓ : ℓ.arg ≠ . exact eval_congr fun i hi => (Function.update_of_ne (by rintro rfl; exact not_reads_subst hℓ hi) _ _).symm +/-- Rerouting `v` to a constant literal `Lit.const b` evaluates the gate under the updated +assignment `Function.update val v b`. -/ @[simp] theorem eval_subst_const (g : Gate) (v : ℕ) (b : Bool) (val : ℕ → Bool) : (g.subst v (Lit.const b)).eval val = g.eval (Function.update val v b) := by rw [eval_subst_update (by simp [Lit.const]), Lit.eval_const] @@ -349,12 +374,14 @@ private theorem unary_cases (h : Bool → Bool) (x : Bool) : def unaryLit (h : Bool → Bool) (a : Arg) : Lit := if h false = h true then Lit.const (h false) else ⟨a, h false⟩ +/-- The literal `unaryLit h a` evaluates to `h (a.eval val)`. -/ theorem eval_unaryLit (h : Bool → Bool) (a : Arg) (val : ℕ → Bool) : h (a.eval val) = (unaryLit h a).eval val := by rw [unary_cases h (a.eval val)] unfold unaryLit split_ifs <;> simp [Lit.eval, Lit.const] +/-- If `unaryLit h a` reads `t`, then `a = .node t`. -/ theorem reads_of_unaryLit_reads {h : Bool → Bool} {a : Arg} {t : ℕ} (hr : (unaryLit h a).Reads t) : a = .node t := by unfold unaryLit at hr @@ -362,6 +389,7 @@ theorem reads_of_unaryLit_reads {h : Bool → Bool} {a : Arg} {t : ℕ} · simp [Lit.Reads, Lit.const] at hr · exact hr +/-- A degenerate gate evaluates to the same value as its simplified literal `g.lit`. -/ theorem Gate.eval_lit {g : Gate} (hg : g.Degenerate) (val : ℕ → Bool) : g.eval val = g.lit.eval val := by obtain ⟨op, l, r⟩ := g @@ -388,6 +416,7 @@ theorem Gate.eval_lit {g : Gate} (hg : g.Degenerate) (val : ℕ → Bool) : rw [unary_cases (fun x => op x x) (val t)] split_ifs <;> simp [Lit.eval, Lit.const] +/-- Any internal value read by `g.lit` is also read by `g`. -/ theorem Gate.reads_of_lit_reads {g : Gate} {t : ℕ} (h : g.lit.Reads t) : g.Reads t := by obtain ⟨op, l, r⟩ := g unfold Reads @@ -410,6 +439,7 @@ theorem Gate.reads_of_lit_reads {g : Gate} {t : ℕ} (h : g.lit.Reads t) : g.Rea · simp [Lit.Reads, Lit.const] at h · exact Or.inl h +/-- Rerouting a variable in a degenerate gate yields a degenerate gate. -/ theorem Gate.degenerate_subst {g : Gate} (hg : g.Degenerate) (v : ℕ) (ℓ : Lit) : (g.subst v ℓ).Degenerate := by unfold Gate.Degenerate at * @@ -426,6 +456,7 @@ theorem Gate.degenerate_subst {g : Gate} (hg : g.Degenerate) (v : ℕ) (ℓ : Li def IsAffineOp (op : Bool → Bool → Bool) : Prop := (op false false ^^ op true false ^^ op false true ^^ op true true) = false +/-- Decidability of whether a binary Boolean operation is affine. -/ instance (op : Bool → Bool → Bool) : Decidable (IsAffineOp op) := inferInstanceAs (Decidable (_ = _)) diff --git a/Complexity/Computability/Circuit/Boolean/SemiCircuit/OfCircuit.lean b/Complexity/Computability/Circuit/Boolean/SemiCircuit/OfCircuit.lean index f2ecae4e1..ed90a27d2 100644 --- a/Complexity/Computability/Circuit/Boolean/SemiCircuit/OfCircuit.lean +++ b/Complexity/Computability/Circuit/Boolean/SemiCircuit/OfCircuit.lean @@ -23,7 +23,9 @@ the circuit on the values of the parameters (`SemiCircuit.out_eval_ofCircuit`). ## Main definitions -* `Cslib.Circuits.Boolean.SemiCircuit.ofCircuit`: the semi-circuit of a circuit. +* `Cslib.Circuits.Boolean.SemiCircuit.wireName`, + `Cslib.Circuits.Boolean.SemiCircuit.lineGate`, + `Cslib.Circuits.Boolean.SemiCircuit.ofCircuit`: the semi-circuit of a circuit. ## Main results @@ -56,6 +58,8 @@ def lineGate {g : ℕ} : Line (fullSignature 2 Bool) n g → Gate .node (wireName (w ⟨1, by simp [fullSignature]⟩))⟩ | ⟨.con c, _⟩ => ⟨fun _ _ => c, .const false, .const false⟩ +/-- Evaluating `lineGate line` under `val` equals applying `fullInterpretation line.op` to the +values of `line`'s input wires. -/ theorem eval_lineGate {g : ℕ} (line : Line (fullSignature 2 Bool) n g) (val : ℕ → Bool) : (lineGate line).eval val = fullInterpretation line.op fun a => val (wireName (line.wires a)) := by @@ -89,15 +93,19 @@ def ofCircuit (C : Circuit (fullSignature 2 Bool) n 1) : SemiCircuit where eqn _ := ⟨∅, false⟩ out := ⟨.node (wireName (C.outputs 0)), false⟩ +/-- The parameters of `ofCircuit C` are `Finset.range n`. -/ @[simp] theorem ofCircuit_params (C : Circuit (fullSignature 2 Bool) n 1) : (ofCircuit C).params = Finset.range n := rfl +/-- The semi-circuit `ofCircuit C` has no auxiliary variables. -/ @[simp] theorem ofCircuit_aux (C : Circuit (fullSignature 2 Bool) n 1) : (ofCircuit C).aux = ∅ := rfl +/-- The gate indices of `ofCircuit C` are `Finset.Ico n (n + C.size)`. -/ @[simp] theorem ofCircuit_gates (C : Circuit (fullSignature 2 Bool) n 1) : (ofCircuit C).gates = Finset.Ico n (n + C.size) := rfl +/-- The semi-circuit `ofCircuit C` has no affine equations. -/ @[simp] theorem ofCircuit_eqns (C : Circuit (fullSignature 2 Bool) n 1) : (ofCircuit C).eqns = ∅ := rfl @@ -108,12 +116,14 @@ private theorem ofCircuit_gate (C : Circuit (fullSignature 2 Bool) n 1) (k : Fin congr 2 exact Fin.ext (by simp) +/-- The node index `wireName w` of any wire `w` of `C` is live in `ofCircuit C`. -/ theorem wireName_mem_live (C : Circuit (fullSignature 2 Bool) n 1) (w : Wire n C.size) : wireName w ∈ (ofCircuit C).live := by cases w with | input i => simp [live, ofCircuit, wireName] | gate j => simp [live, ofCircuit, wireName] +/-- Every gate index of `ofCircuit C` has the form `n + k` for some `k : Fin C.size`. -/ theorem exists_eq_add_of_mem_gates {C : Circuit (fullSignature 2 Bool) n 1} {J : ℕ} (hJ : J ∈ (ofCircuit C).gates) : ∃ k : Fin C.size, J = n + k := by simp only [ofCircuit, Finset.mem_Ico] at hJ diff --git a/Complexity/Computability/Circuit/Boolean/SemiCircuit/Reparameterisation.lean b/Complexity/Computability/Circuit/Boolean/SemiCircuit/Reparameterisation.lean index b666c3c1b..6eb80bc51 100644 --- a/Complexity/Computability/Circuit/Boolean/SemiCircuit/Reparameterisation.lean +++ b/Complexity/Computability/Circuit/Boolean/SemiCircuit/Reparameterisation.lean @@ -26,7 +26,8 @@ reparameterisations (AR) and (QR) of [Mishra and Santhanam, Section 3.2][MishraS ## Main definitions -* `Cslib.Circuits.Boolean.SemiCircuit.swap`, `Cslib.Circuits.Boolean.SemiCircuit.quad`. +* `Cslib.Circuits.Boolean.SemiCircuit.swap`, `Cslib.Circuits.Boolean.SemiCircuit.quad`, + `Cslib.Circuits.Boolean.SemiCircuit.QuadOK`, `Cslib.Circuits.Boolean.SemiCircuit.quadValue`. ## Main results @@ -148,6 +149,7 @@ theorem WellFormed.swap (hC : C.WellFormed) {x Q : ℕ} {c : Bool} {T : Finset def quad (C : SemiCircuit) (z G D : ℕ) : SemiCircuit := { C with params := insert D (C.params.erase z), gates := (C.gates.erase D).erase G } +/-- Any live node of `C` distinct from `z` and `G` remains live in `C.quad z G D`. -/ theorem mem_live_quad {z G D i : ℕ} (hi : i ∈ C.live) (hiz : i ≠ z) (hiG : i ≠ G) : i ∈ (C.quad z G D).live := by simp only [live, Finset.mem_union] at hi ⊢ diff --git a/Complexity/Computability/Circuit/Boolean/SemiCircuit/Rewiring.lean b/Complexity/Computability/Circuit/Boolean/SemiCircuit/Rewiring.lean index 714bc6993..e32e25f9b 100644 --- a/Complexity/Computability/Circuit/Boolean/SemiCircuit/Rewiring.lean +++ b/Complexity/Computability/Circuit/Boolean/SemiCircuit/Rewiring.lean @@ -26,7 +26,8 @@ the original semi-circuit (`SemiCircuit.MoveOK.liftsTo`, `SemiCircuit.RewireOK.l ## Main definitions -* `Cslib.Circuits.Boolean.SemiCircuit.moveAffine`, `Cslib.Circuits.Boolean.SemiCircuit.rewire`. +* `Cslib.Circuits.Boolean.SemiCircuit.moveAffine`, `Cslib.Circuits.Boolean.SemiCircuit.MoveOK`, + `Cslib.Circuits.Boolean.SemiCircuit.rewire`, `Cslib.Circuits.Boolean.SemiCircuit.RewireOK`. ## Main results @@ -71,6 +72,8 @@ namespace MoveOK variable {J e : ℕ} (h : C.MoveOK J e) include h +/-- Moving gate `J` with fresh equation index `e` leaves all existing equations of `C` +unchanged. -/ theorem eqn_of_mem {e' : ℕ} (he' : e' ∈ C.eqns) : (C.moveAffine J e).eqn e' = C.eqn e' := Function.update_of_ne (show e' ≠ e from fun he => h.fresh (he ▸ he')) _ _ @@ -102,6 +105,8 @@ private theorem live_eq : (C.moveAffine J e).live = C.live := by end MoveOK +/-- In a well-formed semi-circuit, any node read by a gate `J` satisfying `MoveOK J e` is a +parameter or auxiliary variable. -/ theorem MoveOK.mem_params_or_aux (hC : C.WellFormed) {J e : ℕ} (h : C.MoveOK J e) {i : ℕ} (hi : (C.gate J).Reads i) : i ∈ C.params ∪ C.aux := by have := hC.reads_live J h.mem i hi diff --git a/Complexity/Computability/Circuit/Boolean/SemiCircuit/Simplification.lean b/Complexity/Computability/Circuit/Boolean/SemiCircuit/Simplification.lean index bbd28c722..8e9995c93 100644 --- a/Complexity/Computability/Circuit/Boolean/SemiCircuit/Simplification.lean +++ b/Complexity/Computability/Circuit/Boolean/SemiCircuit/Simplification.lean @@ -33,8 +33,12 @@ consistent assignments of the deletions lift to the original semi-circuit ## Main definitions * `Cslib.Circuits.Boolean.SemiCircuit.restrict`, `Cslib.Circuits.Boolean.SemiCircuit.deleteGate`, - `Cslib.Circuits.Boolean.SemiCircuit.deleteEqn`, `Cslib.Circuits.Boolean.SemiCircuit.dropEqn`, - `Cslib.Circuits.Boolean.SemiCircuit.dropTrivialEqn`: the simplifications. + `Cslib.Circuits.Boolean.SemiCircuit.DeleteGateOK`, + `Cslib.Circuits.Boolean.SemiCircuit.deleteEqn`, + `Cslib.Circuits.Boolean.SemiCircuit.DeleteEqnOK`, + `Cslib.Circuits.Boolean.SemiCircuit.dropEqn`, + `Cslib.Circuits.Boolean.SemiCircuit.DropEqnOK`, + `Cslib.Circuits.Boolean.SemiCircuit.dropTrivialEqn`: the simplifications and their preconditions. ## Main results @@ -63,6 +67,7 @@ parameters. -/ def restrict (C : SemiCircuit) (x : ℕ) (ℓ : Lit) : SemiCircuit := { C.subst x ℓ with params := C.params.erase x } +/-- Any live node of `C` distinct from `x` remains live in `C.restrict x ℓ`. -/ theorem mem_live_restrict {x : ℕ} {ℓ : Lit} {i : ℕ} (hi : i ∈ C.live) (hix : i ≠ x) : i ∈ (C.restrict x ℓ).live := by simp only [live, Finset.mem_union] at hi ⊢ @@ -141,6 +146,8 @@ theorem consistent_restrict (hC : C.WellFormed) {x : ℕ} {ℓ : Lit} (hx : x C.Consistent (Function.update val x (ℓ.eval val)) := consistent_of_subst (hC.notMem_gates_of_mem_params hx) hℓ h +/-- Evaluating the output of `C.restrict x ℓ` under `val` equals evaluating the output of `C` +after updating `x` to `ℓ.eval val`. -/ theorem out_restrict {x : ℕ} {ℓ : Lit} (hℓ : ℓ.arg ≠ .node x) (val : ℕ → Bool) : (C.restrict x ℓ).out.eval val = C.out.eval (Function.update val x (ℓ.eval val)) := Lit.eval_subst_update hℓ val @@ -169,6 +176,7 @@ private theorem eqnsHold_deleteGate (hC : C.WellFormed) {J : ℕ} {ℓ : Lit} (h change ((C.eqn e).subst J ℓ).Holds val ↔ _ rw [Equation.subst_of_notMem (hC.notMem_terms_of_mem_gates hJ he)] +/-- Any live node of `C` distinct from `J` remains live in `C.deleteGate J ℓ`. -/ theorem mem_live_deleteGate {J : ℕ} {ℓ : Lit} {i : ℕ} (hi : i ∈ C.live) (hiJ : i ≠ J) : i ∈ (C.deleteGate J ℓ).live := by simp only [live, Finset.mem_union] at hi ⊢ @@ -268,6 +276,7 @@ structure DeleteEqnOK (C : SemiCircuit) (e v : ℕ) (ℓ : Lit) : Prop where holds : ∀ val, (C.eqn e).Holds val ↔ val v = ℓ.eval val reads : ∀ t, ℓ.Reads t → t ∈ (C.eqn e).terms ∧ t ≠ v +/-- Any live node of `C` distinct from `v` remains live in `C.deleteEqn e v ℓ`. -/ theorem mem_live_deleteEqn {e v : ℕ} {ℓ : Lit} {i : ℕ} (hi : i ∈ C.live) (hiv : i ≠ v) : i ∈ (C.deleteEqn e v ℓ).live := by simp only [live, Finset.mem_union] at hi ⊢ @@ -466,6 +475,7 @@ private theorem eqnsHold_dropTrivialEqn (hC : C.WellFormed) {e : ℕ} (he : e · subst hee; exact htriv · exact h e' (Finset.mem_erase.2 ⟨hee, he'⟩) +/-- Dropping an equation with no terms preserves well-formedness. -/ theorem WellFormed.dropTrivialEqn (hC : C.WellFormed) {e : ℕ} (he : e ∈ C.eqns) (hterms : (C.eqn e).terms = ∅) : (C.dropTrivialEqn e).WellFormed where disjoint_params_aux := hC.disjoint_params_aux @@ -483,6 +493,8 @@ theorem WellFormed.dropTrivialEqn (hC : C.WellFormed) {e : ℕ} (he : e ∈ C.eq hC.unique val val' hagree ((eqnsHold_dropTrivialEqn hC he hterms val).1 heq) ((eqnsHold_dropTrivialEqn hC he hterms val').1 heq') +/-- Every consistent assignment after dropping an equation with no terms is consistent for the +original semi-circuit. -/ theorem liftsTo_dropTrivialEqn (hC : C.WellFormed) {e : ℕ} (he : e ∈ C.eqns) (hterms : (C.eqn e).terms = ∅) : (C.dropTrivialEqn e).LiftsTo C := fun val hval => ⟨val, ⟨(eqnsHold_dropTrivialEqn hC he hterms val).1 hval.1, hval.2⟩, fun _ _ => rfl, rfl⟩ diff --git a/Complexity/Computability/Circuit/Boolean/ShallowSymmetric/ShiftTest.lean b/Complexity/Computability/Circuit/Boolean/ShallowSymmetric/ShiftTest.lean index 0a5173c45..4511bb9db 100644 --- a/Complexity/Computability/Circuit/Boolean/ShallowSymmetric/ShiftTest.lean +++ b/Complexity/Computability/Circuit/Boolean/ShallowSymmetric/ShiftTest.lean @@ -31,6 +31,8 @@ abelian group; the circuit construction uses `ZMod k`. ## Main definitions +* `Cslib.Circuits.Boolean.ShallowSymmetric.residueSum`: the sum of all elements in a finite + additive commutative group. * `Cslib.Circuits.Boolean.ShallowSymmetric.ShiftTest`: the shifted distinctness tests. ## Main results diff --git a/Complexity/Computability/Circuit/Boolean/Smolensky/Gates.lean b/Complexity/Computability/Circuit/Boolean/Smolensky/Gates.lean index 7ba63c432..28c3f040b 100644 --- a/Complexity/Computability/Circuit/Boolean/Smolensky/Gates.lean +++ b/Complexity/Computability/Circuit/Boolean/Smolensky/Gates.lean @@ -86,6 +86,8 @@ def andApprox (T : Fin ℓ → Finset (Fin m)) (u : Fin m → R) : R := def modApprox (u : Fin m → R) : R := (∑ i, u i) ^ (p - 1) +/-- Composing `orApprox p T` with degree-`D` polynomials yields a polynomial of degree at most +`ℓ * ((p - 1) * D)`. -/ theorem orApprox_comp_mem {D : ℕ} (T : Fin ℓ → Finset (Fin m)) {v : Fin m → BitString n → R} (hv : ∀ k, v k ∈ lowDegree R (Fin n) D) : (fun x => orApprox p T fun k => v k x) ∈ lowDegree R (Fin n) (ℓ * ((p - 1) * D)) := by @@ -101,6 +103,8 @@ theorem orApprox_comp_mem {D : ℕ} (T : Fin ℓ → Finset (Fin m)) {v : Fin m one_sub_mem_lowDegree (pow_mem_lowDegree (sum_mem_lowDegree _ fun i _ => hv i) (p - 1)) rwa [card_univ, Fintype.card_fin] at h +/-- Composing `andApprox p T` with degree-`D` polynomials yields a polynomial of degree at most +`ℓ * ((p - 1) * D)`. -/ theorem andApprox_comp_mem {D : ℕ} (T : Fin ℓ → Finset (Fin m)) {v : Fin m → BitString n → R} (hv : ∀ k, v k ∈ lowDegree R (Fin n) D) : (fun x => andApprox p T fun k => v k x) ∈ lowDegree R (Fin n) (ℓ * ((p - 1) * D)) := by @@ -113,6 +117,8 @@ theorem andApprox_comp_mem {D : ℕ} (T : Fin ℓ → Finset (Fin m)) {v : Fin m rw [hfun] exact one_sub_mem_lowDegree hmem +/-- Composing `modApprox p` with degree-`D` polynomials yields a polynomial of degree at most +`(p - 1) * D`. -/ theorem modApprox_comp_mem {D : ℕ} {v : Fin m → BitString n → R} (hv : ∀ k, v k ∈ lowDegree R (Fin n) D) : (fun x => modApprox p fun k => v k x) ∈ lowDegree R (Fin n) ((p - 1) * D) := by diff --git a/Complexity/Computability/Circuit/Boolean/Tableau/Basic.lean b/Complexity/Computability/Circuit/Boolean/Tableau/Basic.lean index fdb3e7432..16936e021 100644 --- a/Complexity/Computability/Circuit/Boolean/Tableau/Basic.lean +++ b/Complexity/Computability/Circuit/Boolean/Tableau/Basic.lean @@ -52,7 +52,11 @@ only inputs and earlier gates. Its correctness is proved in ## Main definitions -* `Cslib.Circuits.Boolean.Tableau.table`: the gate at each position of a block. +* `Cslib.Circuits.Boolean.Tableau.Attr.test`, `Cslib.Circuits.Boolean.Tableau.sitOf`, + `Cslib.Circuits.Boolean.Tableau.scanTerm`, `Cslib.Circuits.Boolean.Tableau.gfTerms`, + `Cslib.Circuits.Boolean.Tableau.colTerms`, `Cslib.Circuits.Boolean.Tableau.gfInit`, + `Cslib.Circuits.Boolean.Tableau.colInit`, `Cslib.Circuits.Boolean.Tableau.initBit`, + `Cslib.Circuits.Boolean.Tableau.table`: the gate and initial-configuration tables for a block. * `Cslib.Circuits.Boolean.Tableau.gateAt`, `Cslib.Circuits.Boolean.Tableau.gateCode`: the gate at a block position and the gate with a given number. * `Cslib.Circuits.Boolean.Tableau.gates`, `Cslib.Circuits.Boolean.Tableau.outWire`: the gate list @@ -553,6 +557,8 @@ theorem isCodeFrom_gates (n T : ℕ) : Program.IsCodeFrom signature n 0 (gates t omega omit [DecidableEq State] in +/-- The output wire index is strictly less than the total number of wires +`n + numGates k State T`. -/ theorem outWire_lt (n T : ℕ) : outWire k State n T < n + numGates k State T := by have := Loc.offset_lt (k := k) (State := State) (T := T) (l := .gf (.out (.one true)) true 7) (c := 0) rfl @@ -560,6 +566,8 @@ theorem outWire_lt (n T : ℕ) : outWire k State n T < n + numGates k State T := rw [Nat.succ_mul] omega +/-- The raw gate list `gates tm n T` and output wire `outWire k State n T` form a valid circuit +code. -/ theorem isSome_ofCode (n T : ℕ) : (Circuit.ofCode n 1 (gates tm n T, [outWire k State n T]) : Option (Circuit signature n 1)).isSome := by diff --git a/Complexity/Computability/Circuit/Boolean/Tableau/Layout.lean b/Complexity/Computability/Circuit/Boolean/Tableau/Layout.lean index 2c3b05123..a9bb85aeb 100644 --- a/Complexity/Computability/Circuit/Boolean/Tableau/Layout.lean +++ b/Complexity/Computability/Circuit/Boolean/Tableau/Layout.lean @@ -38,14 +38,26 @@ block position (`div_mod_wire`, `exists_wire_eq`). * `Cslib.Circuits.Boolean.Tableau.Attr`, `Cslib.Circuits.Boolean.Tableau.ColFeat`, `Cslib.Circuits.Boolean.Tableau.GFeat`, `Cslib.Circuits.Boolean.Tableau.ScanQ`, - `Cslib.Circuits.Boolean.Tableau.ScanLoc`, `Cslib.Circuits.Boolean.Tableau.GlobLoc`, - `Cslib.Circuits.Boolean.Tableau.Loc`: positions within a tableau block. -* `Cslib.Circuits.Boolean.Tableau.ColSel`, `Cslib.Circuits.Boolean.Tableau.Guard`, - `Cslib.Circuits.Boolean.Tableau.Ref`: symbolic wire references relative to a block and column. -* `Cslib.Circuits.Boolean.Tableau.blockSize`, `Cslib.Circuits.Boolean.Tableau.numGates`, - `Cslib.Circuits.Boolean.Tableau.Loc.offset`, `Cslib.Circuits.Boolean.Tableau.wire`, - `Cslib.Circuits.Boolean.Tableau.Ref.resolve`: numerical layout and wire resolution. -* `Cslib.Circuits.Boolean.Tableau.ScanLoc.ofIdx`, `Cslib.Circuits.Boolean.Tableau.GlobLoc.ofIdx`, + `Cslib.Circuits.Boolean.Tableau.ScanLoc`, `Cslib.Circuits.Boolean.Tableau.numSit`, + `Cslib.Circuits.Boolean.Tableau.GlobLoc`, `Cslib.Circuits.Boolean.Tableau.Loc`, + `Cslib.Circuits.Boolean.Tableau.Loc.ColOK`: positions within a tableau block. +* `Cslib.Circuits.Boolean.Tableau.ColSel`, `Cslib.Circuits.Boolean.Tableau.ColSel.apply`, + `Cslib.Circuits.Boolean.Tableau.Guard`, `Cslib.Circuits.Boolean.Tableau.Guard.test`, + `Cslib.Circuits.Boolean.Tableau.Ref`, `Cslib.Circuits.Boolean.Tableau.Ref.toData`, + `Cslib.Circuits.Boolean.Tableau.colF`, `Cslib.Circuits.Boolean.Tableau.gfF`, + `Cslib.Circuits.Boolean.Tableau.act`, `Cslib.Circuits.Boolean.Tableau.halted`, + `Cslib.Circuits.Boolean.Tableau.scanAt`: symbolic wire references relative to a block and column. +* `Cslib.Circuits.Boolean.Tableau.symIdx`, `Cslib.Circuits.Boolean.Tableau.attrIdx`, + `Cslib.Circuits.Boolean.Tableau.gadgetIdx`, `Cslib.Circuits.Boolean.Tableau.scanWidth`, + `Cslib.Circuits.Boolean.Tableau.globWidth`, `Cslib.Circuits.Boolean.Tableau.gfWidth`, + `Cslib.Circuits.Boolean.Tableau.colWidth`, `Cslib.Circuits.Boolean.Tableau.numCols`, + `Cslib.Circuits.Boolean.Tableau.globStart`, `Cslib.Circuits.Boolean.Tableau.gfStart`, + `Cslib.Circuits.Boolean.Tableau.colStart`, `Cslib.Circuits.Boolean.Tableau.blockSize`, + `Cslib.Circuits.Boolean.Tableau.numGates`, `Cslib.Circuits.Boolean.Tableau.Loc.offset`, + `Cslib.Circuits.Boolean.Tableau.wire`, `Cslib.Circuits.Boolean.Tableau.Ref.resolve`, + `Cslib.Circuits.Boolean.Tableau.argsOf`: numerical layout and wire resolution. +* `Cslib.Circuits.Boolean.Tableau.symOf`, `Cslib.Circuits.Boolean.Tableau.ScanQ.ofIdx`, + `Cslib.Circuits.Boolean.Tableau.ScanLoc.ofIdx`, `Cslib.Circuits.Boolean.Tableau.GlobLoc.ofIdx`, `Cslib.Circuits.Boolean.Tableau.GFeat.ofIdx`, `Cslib.Circuits.Boolean.Tableau.ColFeat.ofIdx`: arithmetic decoders for block offsets. @@ -168,6 +180,7 @@ inductive ColSel where | last deriving DecidableEq +/-- Finite enumeration of column selectors. -/ instance : Fintype ColSel where elems := {.same, .prev, .next, .last} complete x := by cases x <;> simp @@ -193,6 +206,7 @@ inductive Guard where | leEnd deriving DecidableEq +/-- Finite enumeration of column guards. -/ instance : Fintype Guard where elems := {.always, .pos, .ltLast, .inRange, .outRange, .isZero, .isEnd, .leEnd} complete x := by cases x <;> simp @@ -220,6 +234,7 @@ def Ref.toData : Ref k State → Option (Option (Option (Bool × Loc k State × | .inp => some (some none) | .node p l cs g => some (some (some (p, l, cs, g))) +/-- Finiteness of symbolic wire references. -/ instance : Finite (Ref k State) := Finite.of_injective Ref.toData fun a b h => by cases a <;> cases b <;> simp_all [Ref.toData] @@ -417,6 +432,7 @@ private theorem symOf_symIdx (s : Option Bool) : symOf (symIdx s) = s := by private theorem symIdx_lt (s : Option Bool) : symIdx s < 3 := by rcases s with _ | _ | _ <;> simp [symIdx] +/-- Decoding the index of a scanned quantity recovers the quantity. -/ theorem ScanQ.ofIdx_idx (q : ScanQ k) : ScanQ.ofIdx q.idx = q := by rcases q with s | ⟨i, s⟩ · simp [ScanQ.idx, ScanQ.ofIdx, symIdx_lt, symOf_symIdx] @@ -426,11 +442,13 @@ theorem ScanQ.ofIdx_idx (q : ScanQ k) : ScanQ.ofIdx q.idx = q := by simp only [ScanQ.idx, ScanQ.ofIdx, show ¬3 + 3 * (i : ℕ) + symIdx s < 3 by omega, ↓reduceIte, h₁, i.isLt, ↓reduceDIte, h₂, symOf_symIdx] +/-- The index of a scanned quantity is strictly less than `3 + 3 * k`. -/ theorem ScanQ.idx_lt (q : ScanQ k) : q.idx < 3 + 3 * k := by rcases q with s | ⟨i, s⟩ <;> simp only [ScanQ.idx] <;> have := symIdx_lt s · omega · have := i.isLt; omega +/-- Decoding the index of a scan position recovers the position. -/ theorem ScanLoc.ofIdx_idx (l : ScanLoc k) : ScanLoc.ofIdx l.idx = l := by rcases l with i | _ | q | q · simp [ScanLoc.idx, ScanLoc.ofIdx] @@ -445,6 +463,7 @@ theorem ScanLoc.ofIdx_idx (l : ScanLoc k) : ScanLoc.ofIdx l.idx = l := by show (k + 2 + 2 * q.idx - (k + 1)) / 2 = q.idx by omega, ScanQ.ofIdx_idx] rfl +/-- The index of a scan position is strictly less than `scanWidth k`. -/ theorem ScanLoc.idx_lt (l : ScanLoc k) : l.idx < scanWidth k := by rcases l with i | _ | q | q <;> simp only [ScanLoc.idx, scanWidth] · have := i.isLt; omega @@ -455,6 +474,7 @@ theorem ScanLoc.idx_lt (l : ScanLoc k) : l.idx < scanWidth k := by private theorem attrIdx_lt (v : Attr k State) : attrIdx v < Fintype.card (Attr k State) := (Fintype.equivFin (Attr k State) v).isLt +/-- The index of a global gate position is strictly less than `globWidth k State`. -/ theorem GlobLoc.idx_lt (l : GlobLoc k State) : l.idx < globWidth k State := by rcases l with ⟨j, i⟩ | ⟨v, j⟩ <;> simp only [GlobLoc.idx, globWidth] · have := j.isLt @@ -470,6 +490,7 @@ theorem GlobLoc.idx_lt (l : GlobLoc k State) : l.idx < globWidth k State := by Fintype.card (Attr k State) * (numSit k State + 1) := Nat.mul_le_mul_right _ h₂ omega +/-- Decoding the index of a global gate position recovers the position. -/ theorem GlobLoc.ofIdx_idx (l : GlobLoc k State) : GlobLoc.ofIdx l.idx = l := by rcases l with ⟨j, i⟩ | ⟨v, j⟩ · have hlt : (j : ℕ) * (k + 1) + i < numSit k State * (k + 1) := by @@ -498,6 +519,7 @@ theorem GlobLoc.ofIdx_idx (l : GlobLoc k State) : GlobLoc.ofIdx l.idx = l := by congr exact (Fintype.equivFin (Attr k State)).symm_apply_apply v +/-- The index of a global feature is strictly less than `Fintype.card (Option State) + 4`. -/ theorem GFeat.idx_lt (f : GFeat State) : f.idx < Fintype.card (Option State) + 4 := by rcases f with q | o · have := (Fintype.equivFin (Option State) q).isLt @@ -507,6 +529,7 @@ theorem GFeat.idx_lt (f : GFeat State) : f.idx < Fintype.card (Option State) + 4 simp only [GFeat.idx] omega +/-- Decoding the index of a global feature recovers the feature. -/ theorem GFeat.ofIdx_idx (f : GFeat State) : GFeat.ofIdx f.idx = f := by rcases f with q | o · simp only [GFeat.idx, GFeat.ofIdx, Fin.is_lt, ↓reduceDIte, Fin.eta, Equiv.symm_apply_apply] @@ -515,12 +538,14 @@ theorem GFeat.ofIdx_idx (f : GFeat State) : GFeat.ofIdx f.idx = f := by · exact absurd h (by simp only [GFeat.idx]; omega) · simp [GFeat.idx] +/-- The index of a column feature is strictly less than `1 + 4 * k`. -/ theorem ColFeat.idx_lt (f : ColFeat k) : f.idx < 1 + 4 * k := by rcases f with _ | i | ⟨i, s⟩ <;> simp only [ColFeat.idx] · omega · have := i.isLt; omega · have := i.isLt; have := symIdx_lt s; omega +/-- Decoding the index of a column feature recovers the feature. -/ theorem ColFeat.ofIdx_idx (f : ColFeat k) : ColFeat.ofIdx f.idx = f := by rcases f with _ | i | ⟨i, s⟩ · rfl @@ -532,6 +557,7 @@ theorem ColFeat.ofIdx_idx (f : ColFeat k) : ColFeat.ofIdx f.idx = f := by show ¬1 + k + 3 * (i : ℕ) + symIdx s - 1 < k by omega, ↓reduceIte, ↓reduceDIte, h₁, i.isLt, h₂, symOf_symIdx] +/-- The gadget index for feature `fi` is strictly less than `16 * (fi + 1)`. -/ theorem gadgetIdx_lt (fi : ℕ) (b : Bool) (j : Fin 8) : gadgetIdx fi b j < 16 * (fi + 1) := by have := j.isLt @@ -539,11 +565,13 @@ theorem gadgetIdx_lt (fi : ℕ) (b : Bool) (j : Fin 8) : simp only [gadgetIdx, Bool.toNat_false, Bool.toNat_true, mul_zero, mul_one, add_zero, gt_iff_lt] <;> omega +/-- Dividing `gadgetIdx fi b j` by `16` recovers the feature index `fi`. -/ theorem gadgetIdx_div (fi : ℕ) (b : Bool) (j : Fin 8) : gadgetIdx fi b j / 16 = fi := by have := j.isLt cases b <;> simp only [gadgetIdx, Bool.toNat_false, Bool.toNat_true, mul_zero, mul_one, add_zero] <;> omega +/-- Decoding the gate kind from `gadgetIdx fi b j` recovers `b`. -/ theorem gadgetB_gadgetIdx (fi : ℕ) (b : Bool) (j : Fin 8) : gadgetB (gadgetIdx fi b j) = b := by have := j.isLt @@ -552,6 +580,7 @@ theorem gadgetB_gadgetIdx (fi : ℕ) (b : Bool) (j : Fin 8) : Nat.mul_add_mod_self_left, decide_eq_false_iff_not, decide_eq_true_eq, not_le, ge_iff_le, gt_iff_lt] <;> omega +/-- Decoding the term index from `gadgetIdx fi b j` recovers `j`. -/ theorem gadgetJ_gadgetIdx (fi : ℕ) (b : Bool) (j : Fin 8) : gadgetJ (gadgetIdx fi b j) = j := by have := j.isLt @@ -576,10 +605,12 @@ private theorem mul_add_lt_mul {c w W i : ℕ} (hc : c < W) (hi : i < w) : c * w calc c * w + i < (c + 1) * w := by rw [Nat.succ_mul]; omega _ ≤ W * w := Nat.mul_le_mul_right _ hc +/-- Any scan gate offset in a valid column is strictly less than `globStart k T`. -/ theorem scan_offset_lt_globStart {c : ℕ} (hc : c < numCols T) (l : ScanLoc k) : c * scanWidth k + l.idx < globStart k T := mul_add_lt_mul hc l.idx_lt +/-- Any global-feature gadget offset is strictly less than `colStart k State T`. -/ theorem gfStart_add_gadgetIdx_lt (f : GFeat State) (b : Bool) (j : Fin 8) : gfStart k State T + gadgetIdx f.idx b j < colStart k State T := by have h₁ := gadgetIdx_lt f.idx b j @@ -624,6 +655,7 @@ theorem Loc.offset_lt_of_lt {l : Loc k State} {c : ℕ} (hc : c < numCols T) : · exact Loc.offset_lt (l := .gf f b j) (c := 0) rfl · exact Loc.offset_lt (l := .col f b j) hc +/-- Any admissible column `c` for a position `l` satisfies `c < numCols T`. -/ theorem Loc.ColOK.lt {l : Loc k State} {c : ℕ} (hl : l.ColOK T c) : c < numCols T := by rcases l with l | l | ⟨f, b, j⟩ | ⟨f, b, j⟩ <;> simp only [Loc.ColOK] at hl <;> first | exact hl | (subst hl; simp [numCols]) @@ -637,6 +669,8 @@ theorem wire_sub (n T t : ℕ) (l : Loc k State) (c : ℕ) : simp only [wire] omega +/-- Dividing and reducing `wire n T t l c - n - 2` modulo `blockSize` recovers the block `t` and +intra-block offset `l.offset T c`. -/ theorem div_mod_wire {n T t : ℕ} {l : Loc k State} {c : ℕ} (hl : l.ColOK T c) : (wire n T t l c - n - 2) / blockSize k State T = t ∧ (wire n T t l c - n - 2) % blockSize k State T = l.offset T c := by @@ -655,6 +689,7 @@ private theorem symIdx_symOf {m : ℕ} (hm : m < 3) : symIdx (symOf m) = m := by · rfl · omega +/-- Encoding `ScanQ.ofIdx m` for `m < 3 + 3 * k` recovers `m`. -/ theorem ScanQ.idx_ofIdx {m : ℕ} (hm : m < 3 + 3 * k) : (ScanQ.ofIdx m : ScanQ k).idx = m := by rw [ScanQ.ofIdx] @@ -665,6 +700,7 @@ theorem ScanQ.idx_ofIdx {m : ℕ} (hm : m < 3 + 3 * k) : omega · exact absurd (by omega) h₂ +/-- Encoding `ScanLoc.ofIdx m` for `m < scanWidth k` recovers `m`. -/ theorem ScanLoc.idx_ofIdx {m : ℕ} (hm : m < scanWidth k) : (ScanLoc.ofIdx m : ScanLoc k).idx = m := by simp only [scanWidth] at hm @@ -679,6 +715,7 @@ theorem ScanLoc.idx_ofIdx {m : ℕ} (hm : m < scanWidth k) : rw [ScanQ.idx_ofIdx (by omega)] omega +/-- Encoding `GlobLoc.ofIdx m` for `m < globWidth k State` recovers `m`. -/ theorem GlobLoc.idx_ofIdx {m : ℕ} (hm : m < globWidth k State) : (GlobLoc.ofIdx m : GlobLoc k State).idx = m := by simp only [globWidth] at hm @@ -693,6 +730,7 @@ theorem GlobLoc.idx_ofIdx {m : ℕ} (hm : m < globWidth k State) : Fintype.card (Attr k State) * (numSit k State + 1) := by omega exact absurd ((Nat.div_lt_iff_lt_mul (by omega)).2 this) h₂ +/-- Encoding `GFeat.ofIdx m` for `m < Fintype.card (Option State) + 4` recovers `m`. -/ theorem GFeat.idx_ofIdx {m : ℕ} (hm : m < Fintype.card (Option State) + 4) : (GFeat.ofIdx m : GFeat State).idx = m := by rw [GFeat.ofIdx] @@ -702,6 +740,7 @@ theorem GFeat.idx_ofIdx {m : ℕ} (hm : m < Fintype.card (Option State) + 4) : rw [OutView.index_ofIndex (by omega)] omega +/-- Encoding `ColFeat.ofIdx m` for `m < 1 + 4 * k` recovers `m`. -/ theorem ColFeat.idx_ofIdx {m : ℕ} (hm : m < 1 + 4 * k) : (ColFeat.ofIdx m : ColFeat k).idx = m := by rw [ColFeat.ofIdx] diff --git a/Complexity/Computability/Circuit/Boolean/Tableau/Space.lean b/Complexity/Computability/Circuit/Boolean/Tableau/Space.lean index 94ac68b07..9248ef194 100644 --- a/Complexity/Computability/Circuit/Boolean/Tableau/Space.lean +++ b/Complexity/Computability/Circuit/Boolean/Tableau/Space.lean @@ -191,6 +191,7 @@ private theorem globStart_inSpace : omit [DecidableEq State] in omit hT hin in +/-- Computing `gfStart k State (T x)` within space budget `Bs`. -/ theorem gfStart_inSpace (hT : ComputableInSpace T encIn encNat Bs) (hin : (fun x => (encIn x).length) ≼ Bs) : ComputableInSpace (fun x => gfStart k State (T x)) encIn encNat Bs := by @@ -206,6 +207,7 @@ private theorem colStart_inSpace : omit [DecidableEq State] in omit hT hin in +/-- Computing `blockSize k State (T x)` within space budget `Bs`. -/ theorem blockSize_inSpace (hT : ComputableInSpace T encIn encNat Bs) (hin : (fun x => (encIn x).length) ≼ Bs) : ComputableInSpace (fun x => blockSize k State (T x)) encIn encNat Bs := by @@ -214,9 +216,11 @@ theorem blockSize_inSpace (hT : ComputableInSpace T encIn encNat Bs) exact budget_natAdd (colStart_inSpace (k := k) (State := State) hT hin) (budget_natMul (numCols_inSpace hT hin) (budget_const _ hin)) +/-- Explicit finite enumeration of `ColSel`. -/ instance : FinEnum ColSel := FinEnum.ofList [.same, .prev, .next, .last] fun x => by cases x <;> decide +/-- Explicit finite enumeration of `Guard`. -/ instance : FinEnum Guard := FinEnum.ofList [.always, .pos, .ltLast, .inRange, .outRange, .isZero, .isEnd, .leEnd] fun x => by cases x <;> decide diff --git a/Complexity/Computability/Circuit/Boolean/Threshold/Parity.lean b/Complexity/Computability/Circuit/Boolean/Threshold/Parity.lean index 5bb00eab7..4a11be3b4 100644 --- a/Complexity/Computability/Circuit/Boolean/Threshold/Parity.lean +++ b/Complexity/Computability/Circuit/Boolean/Threshold/Parity.lean @@ -32,7 +32,9 @@ constant depth (`Threshold.parity_mem_constDepth`), and is in TC⁰ ## Main definitions -* `Cslib.Circuits.Boolean.Threshold.parityCircuit`: the depth-two threshold circuit for parity. +* `Cslib.Circuits.Boolean.Threshold.negIf`, + `Cslib.Circuits.Boolean.Threshold.signedLayerGate`, + `Cslib.Circuits.Boolean.Threshold.parityCircuit`: the depth-two threshold circuit for parity. ## Main results @@ -60,6 +62,7 @@ def negIf : Bool → Circuit signature 1 1 | true => Circuit.oneGate (σ := signature) .not id | false => Circuit.id signature 1 +/-- Evaluating `negIf b` XORs the input bit with `b`. -/ @[simp] theorem eval_negIf (b : Bool) (y : Fin 1 → Bool) (o : Fin 1) : (negIf b).eval interpretation y o = (b ^^ y 0) := by cases b @@ -69,12 +72,15 @@ def negIf : Bool → Circuit signature 1 1 private theorem cost_program_negIf (b : Bool) : (negIf b).program.cost thresholdCost = 0 := by cases b <;> rfl +/-- The gate count of `negIf b` is `b.toNat`. -/ @[simp] theorem size_negIf (b : Bool) : (negIf b).size = b.toNat := by cases b <;> rfl +/-- Under `thresholdCost`, `negIf b` has weighted depth `0`. -/ @[simp] theorem depthWith_negIf (b : Bool) : (negIf b).depthWith thresholdCost = 0 := by cases b <;> simp [negIf] +/-- The unweighted depth of `negIf b` is at most `1`. -/ theorem depth_negIf_le (b : Bool) : (negIf b).depth ≤ 1 := by cases b <;> simp [negIf] @@ -90,6 +96,8 @@ def parityCircuit (n : ℕ) : Circuit signature n 1 := (Circuit.oneGate (σ := signature) (.threshold n (n / 2 + 1)) id).comp (Circuit.pi (signedLayerGate n)) +/-- Evaluating `signedLayerGate n j` on `x` returns `threshold n (j + 1) x` negated when `j` is +odd. -/ theorem eval_signedLayerGate (j : Fin n) (x : BitString n) : (signedLayerGate n j).eval interpretation x 0 = (decide (j.val % 2 = 1) ^^ threshold n (j + 1) x) := by diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Activation.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Activation.lean index a2b9547d9..ec2d1aa33 100644 --- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Activation.lean +++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Activation.lean @@ -25,9 +25,11 @@ weights are constant in the input sum and have cost `1`. `Cslib.Circuits.Boolean.WeightedThreshold.activationSignature`, `Cslib.Circuits.Boolean.WeightedThreshold.activationInterpretation`: real-weight gates with arbitrary scalar activations `ℝ → Bool`. -* `Cslib.Circuits.Boolean.WeightedThreshold.ofWeightedThreshold`: embedding of the weighted +* `Cslib.Circuits.Boolean.WeightedThreshold.ofWeightedThresholdOp`, + `Cslib.Circuits.Boolean.WeightedThreshold.ofWeightedThreshold`: embedding of the weighted threshold signature into the activation signature. -* `Cslib.Circuits.Boolean.WeightedThreshold.activationInputWeight`, +* `Cslib.Circuits.Boolean.WeightedThreshold.activationLineWeight`, + `Cslib.Circuits.Boolean.WeightedThreshold.activationInputWeight`, `Cslib.Circuits.Boolean.WeightedThreshold.activationGateWeight`, `Cslib.Circuits.Boolean.WeightedThreshold.activationInputGates`: aggregated wire coefficients and input-reading gates. @@ -154,6 +156,8 @@ private theorem activationGateWeight_eq_zero_of_le (p : Program activationSignat noncomputable def activationInputGates (p : Program activationSignature n g) : Finset (Fin g) := univ.filter fun gate => ∃ i, activationInputWeight p gate i ≠ 0 +/-- A gate belongs to `activationInputGates p` if and only if it has a nonzero direct-input +weight. -/ @[simp] theorem mem_activationInputGates (p : Program activationSignature n g) (gate : Fin g) : gate ∈ activationInputGates p ↔ ∃ i, activationInputWeight p gate i ≠ 0 := by diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Activity.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Activity.lean index 5822f20b7..ff6370411 100644 --- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Activity.lean +++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Activity.lean @@ -79,6 +79,8 @@ noncomputable def inputActivityFrom (p : Program signature n g) noncomputable def gateActivityFrom (p : Program signature n g) (v : Fin g → Bool) : ℕ := univ.sup fun x => hammingDist (p.eval interpretation x) v +/-- A pattern belongs to `attainableTranscripts p` if and only if it is the restricted transcript +of some input `x`. -/ @[simp] theorem mem_attainableTranscripts (p : Program signature n g) (z : inputGates p → Bool) : z ∈ attainableTranscripts p ↔ ∃ x, transcript p x = z := by diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Capacity.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Capacity.lean index 0394f5611..83d575855 100644 --- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Capacity.lean +++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Capacity.lean @@ -37,8 +37,11 @@ of two on the second side. Integer division is retained at every step. ## Main definitions -* `Cslib.Circuits.Boolean.WeightedThreshold.BlockKind`: scalar and finite-summary blocks. -* `Cslib.Circuits.Boolean.WeightedThreshold.BlockDecomposition`: a semantic block decomposition. +* `Cslib.Circuits.Boolean.WeightedThreshold.weightedSum`: weighted sum of a Boolean input. +* `Cslib.Circuits.Boolean.WeightedThreshold.BlockKind`: scalar and finite-summary blocks, with + `BlockKind.cost` and `BlockKind.Step`. +* `Cslib.Circuits.Boolean.WeightedThreshold.BlockDecomposition`: a semantic block decomposition, + with `BlockDecomposition.cost`. ## Main results diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/CapacityCircuit.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/CapacityCircuit.lean index 71f6f971a..b0357f522 100644 --- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/CapacityCircuit.lean +++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/CapacityCircuit.lean @@ -42,7 +42,8 @@ wire is not part of this readout. * `Cslib.Circuits.Boolean.WeightedThreshold.evalFrom`: gate evaluation with fixed overrides and parametric input contributions. * `Cslib.Circuits.Boolean.WeightedThreshold.DirectionRuns`: a partition of the gates into - consecutive runs along single input directions, with `DirectionRuns.toBlockDecomposition`. + consecutive runs along single input directions, with `DirectionRuns.size`, `gateRuns`, + `singleRun`, and `DirectionRuns.toBlockDecomposition`. * `Cslib.Circuits.Boolean.WeightedThreshold.multilevelDecomposition`: a multilevel threshold representation `F (∑ i, w i * (x i).toNat)` as a single scalar block. @@ -480,6 +481,7 @@ noncomputable def DirectionRuns.size {p : Program signature n g} {B : ℕ} (R : DirectionRuns p B) (i : ℕ) : ℕ := ((inputGates p).filter fun gate => R.run gate = i).card +/-- The sizes `R.size i` of the runs partition the input-reading gates of `p`. -/ theorem DirectionRuns.sum_size {p : Program signature n g} {B : ℕ} (R : DirectionRuns p B) : ∑ i ∈ Finset.range B, R.size i = (inputGates p).card := by classical @@ -609,12 +611,15 @@ private theorem cost_oneDim_le_four_mul (r : ℕ) : simp only [BlockKind.cost] split_ifs <;> omega +/-- The capacity cost of `BlockKind.oneDim T` equals `max 1 (4 * T)`. -/ theorem cost_oneDim_eq_max (T : ℕ) : (BlockKind.oneDim T).cost = max 1 (4 * T) := by simp only [BlockKind.cost] split_ifs with hT · simp [hT] · omega +/-- The product of the one-dimensional block costs over all runs is at most +`4 ^ (inputGates p).card`. -/ theorem DirectionRuns.prod_cost_le_four_pow {p : Program signature n g} {B : ℕ} (R : DirectionRuns p B) : ∏ i ∈ Finset.range B, (BlockKind.oneDim (2 ^ R.size i - 1)).cost ≤ diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Components.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Components.lean index f79e6534c..db1ba13b2 100644 --- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Components.lean +++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Components.lean @@ -96,17 +96,23 @@ section Components variable (p : Program signature n g) +/-- An input `u` belongs to `componentInputs p c` if and only if its connected component in +`supportGraph p` is `c`. -/ @[simp] theorem mem_componentInputs {c : (supportGraph p).ConnectedComponent} {u : Fin n} : u ∈ componentInputs p c ↔ (supportGraph p).connectedComponentMk u = c := by classical simp [componentInputs] +/-- Coercing `componentInputs p c` to a set yields the support `c.supp` of the connected component +`c`. -/ theorem coe_componentInputs (c : (supportGraph p).ConnectedComponent) : (componentInputs p c : Set (Fin n)) = c.supp := by ext u simp [mem_componentInputs, SimpleGraph.ConnectedComponent.mem_supp_iff] +/-- A gate belongs to `componentGates p c` if and only if its input support is nonempty and +contained in `componentInputs p c`. -/ @[simp] theorem mem_componentGates {c : (supportGraph p).ConnectedComponent} {j : Fin g} : j ∈ componentGates p c ↔ inputSupport p j ≠ ∅ ∧ inputSupport p j ⊆ componentInputs p c := by @@ -408,12 +414,15 @@ noncomputable def residualGates (p : Program signature n g) (F b : Finset (Fin n Finset (Fin g) := univ.filter fun j => ¬ inputSupport p j ⊆ F ∧ inputSupport p j \ F ⊆ b +/-- A gate belongs to `residualGates p F b` if and only if its input support is not contained in +`F` and its residual support outside `F` is contained in `b`. -/ @[simp] theorem mem_residualGates (p : Program signature n g) (F b : Finset (Fin n)) (j : Fin g) : j ∈ residualGates p F b ↔ ¬ inputSupport p j ⊆ F ∧ inputSupport p j \ F ⊆ b := by classical simp [residualGates] +/-- Every gate in `residualGates p F b` belongs to `inputGates p`. -/ theorem residualGates_subset_inputGates (p : Program signature n g) (F b : Finset (Fin n)) : residualGates p F b ⊆ inputGates p := by intro j hj diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Cut.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Cut.lean index d1f65b4da..ed26af4f4 100644 --- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Cut.lean +++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Cut.lean @@ -73,6 +73,7 @@ variable {n g : ℕ} noncomputable def inputSupport (p : Program signature n g) (gate : Fin g) : Finset (Fin n) := univ.filter fun i => inputWeight p gate i ≠ 0 +/-- An input `i` belongs to `inputSupport p gate` if and only if `inputWeight p gate i ≠ 0`. -/ @[simp] theorem mem_inputSupport (p : Program signature n g) (gate : Fin g) (i : Fin n) : i ∈ inputSupport p gate ↔ inputWeight p gate i ≠ 0 := by diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean index 04fca4c7d..668ad74b9 100644 --- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean +++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean @@ -47,6 +47,10 @@ internal weights (`two_pow_lt_of_directionMenus_intWeight`, `two_pow_lt_of_direc direction `a : Fin d`. * `Cslib.Circuits.Boolean.WeightedThreshold.directionMenuSum`: sum of bias-menu cardinalities over `directionGates p dir a`. +* `Cslib.Circuits.Boolean.WeightedThreshold.MenuTable`, + `Cslib.Circuits.Boolean.WeightedThreshold.trueMenuTable`, + `Cslib.Circuits.Boolean.WeightedThreshold.menuHistory`: precomputed bias-menu threshold tables and + flattened block histories. * `Cslib.Circuits.Boolean.WeightedThreshold.menuBlockDecomposition`: the `(d + g)`-block decomposition precomputing menu tables for a chosen subset of directions. @@ -89,12 +93,14 @@ noncomputable def gateSupport (p : Program signature n g) (gate : Fin g) : Finse open scoped Classical in univ.filter fun prior => gateWeight p gate prior ≠ 0 +/-- A gate `prior` belongs to `gateSupport p gate` if and only if `gateWeight p gate prior ≠ 0`. -/ @[simp] theorem mem_gateSupport (p : Program signature n g) (gate prior : Fin g) : prior ∈ gateSupport p gate ↔ gateWeight p gate prior ≠ 0 := by classical simp [gateSupport] +/-- Every gate in `gateSupport p gate` precedes `gate` in the topological order. -/ theorem gateSupport_subset_Iio (p : Program signature n g) (gate : Fin g) : ∀ prior ∈ gateSupport p gate, prior < gate := by intro prior h @@ -107,11 +113,14 @@ noncomputable def biasMenu (p : Program signature n g) (gate : Fin g) : Finset open scoped Classical in univ.image fun u : Fin g → Bool => ∑ j, gateWeight p gate j * (u j).toNat +/-- The internal gate sum of `gate` under any Boolean valuation `u` belongs to +`biasMenu p gate`. -/ theorem gateBias_mem_biasMenu (p : Program signature n g) (gate : Fin g) (u : Fin g → Bool) : (∑ j, gateWeight p gate j * (u j).toNat) ∈ biasMenu p gate := by classical exact mem_image_of_mem _ (mem_univ u) +/-- The syntactic bias menu `biasMenu p gate` is nonempty. -/ theorem card_biasMenu_pos (p : Program signature n g) (gate : Fin g) : 0 < (biasMenu p gate).card := by classical @@ -208,6 +217,8 @@ noncomputable def directionGates (p : Program signature n g) (dir : Fin g → Fi (a : Fin d) : Finset (Fin g) := (inputGates p).filter fun gate => dir gate = a +/-- A gate belongs to `directionGates p dir a` if and only if it is an input-reading gate with +`dir gate = a`. -/ @[simp] theorem mem_directionGates (p : Program signature n g) (dir : Fin g → Fin d) (a : Fin d) (gate : Fin g) : @@ -219,12 +230,15 @@ noncomputable def directionMenuSum (p : Program signature n g) (dir : Fin g → (a : Fin d) : ℕ := ∑ gate ∈ directionGates p dir a, (biasMenu p gate).card +/-- The sets `directionGates p dir a` partition `inputGates p` across all directions `a`. -/ theorem sum_card_directionGates (p : Program signature n g) (dir : Fin g → Fin d) : ∑ a : Fin d, (directionGates p dir a).card = (inputGates p).card := by classical unfold directionGates exact (card_eq_sum_card_fiberwise fun gate _ => mem_univ (dir gate)).symm +/-- If direction `a` has at least one input-reading gate, then `directionMenuSum p dir a` is +positive. -/ theorem directionMenuSum_pos_of_nonempty (p : Program signature n g) (dir : Fin g → Fin d) {a : Fin d} (h : (directionGates p dir a).Nonempty) : 0 < directionMenuSum p dir a := by diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean index 4cc907c9c..603852f12 100644 --- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean +++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean @@ -48,8 +48,9 @@ its gate transcript (`StrictMarginProgram.eval`): * `Cslib.Circuits.Boolean.WeightedThreshold.boolSign`: `{false, true} → {-1, 1} ⊂ ℝ`. * `Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram`: straight-line threshold program with strictly lower-triangular gate weights and unit score margin `|Q_i(x, z)| ≥ 1`. -* `Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.score`, `.sweep`, `.faceEval`, - `.eval`: gate scores, topological coordinate sweep, face evaluation, and full evaluation. +* `Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.inputSum`, `.internalSum`, + `.score`, `.faceStep`, `.sweep`, `.faceEval`, `.eval`, `.ofProgram`: gate sums and scores, + topological coordinate sweep, face evaluation, full evaluation, and conversion from `Program`. * `Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.inTranscriptCell`, `.leftSupply`, `.rightDemand`, `.ilpValid`: transcript cell, split-dominance vectors, and ILP inequalities. * `Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.priority`, `.energy`, @@ -90,16 +91,20 @@ variable {n g : ℕ} def boolSign (b : Bool) : ℝ := if b then 1 else -1 +/-- The sign of `true` is `1`. -/ @[simp] theorem boolSign_true : boolSign true = 1 := rfl +/-- The sign of `false` is `-1`. -/ @[simp] theorem boolSign_false : boolSign false = -1 := rfl +/-- For any Boolean `b`, `boolSign b = 2 * b.toNat - 1`. -/ theorem boolSign_eq_two_mul_toNat_sub_one (b : Bool) : boolSign b = 2 * (b.toNat : ℝ) - 1 := by cases b <;> norm_num +/-- The absolute value of `boolSign b` is `1`. -/ @[simp] theorem abs_boolSign (b : Bool) : |boolSign b| = 1 := by cases b <;> norm_num @@ -213,6 +218,7 @@ noncomputable def sweep (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin if hk : k < g then P.faceStep fixed val x (sweep fixed val x z k) ⟨k, hk⟩ else sweep fixed val x z k +/-- Zero steps of `sweep` leave the initial assignment `z` unchanged. -/ @[simp] theorem sweep_zero (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin n → Bool) (z : Fin g → Bool) : @@ -267,12 +273,15 @@ noncomputable def faceEval (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : noncomputable def eval (x : Fin n → Bool) : Fin g → Bool := P.faceEval ∅ (fun _ => false) x +/-- At coordinate `i`, `faceEval` returns `val i` if `i ∈ fixed` and the threshold decision at +`faceEval` otherwise. -/ theorem faceEval_apply (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin n → Bool) (i : Fin g) : P.faceEval fixed val x i = if i ∈ fixed then val i else decide (0 < P.score x (P.faceEval fixed val x) i) := P.sweep_apply fixed val x val i +/-- On a fixed coordinate `i ∈ fixed`, `faceEval` evaluates to `val i`. -/ @[simp] theorem faceEval_of_mem {fixed : Finset (Fin g)} {val : Fin g → Bool} {x : Fin n → Bool} {i : Fin g} (hi : i ∈ fixed) : @@ -281,6 +290,7 @@ theorem faceEval_of_mem {fixed : Finset (Fin g)} {val : Fin g → Bool} {x : Fin split_ifs rfl +/-- On a free coordinate `i ∉ fixed`, `faceEval` satisfies gate `i`'s local threshold equation. -/ @[simp] theorem faceEval_of_notMem {fixed : Finset (Fin g)} {val : Fin g → Bool} {x : Fin n → Bool} {i : Fin g} (hi : i ∉ fixed) : diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean index a2d646918..5e2faf859 100644 --- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean +++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean @@ -38,6 +38,9 @@ enumerative coding for weight-bounded words (Theorem 4.3) is in * `Cslib.Circuits.Boolean.WeightedThreshold.scalarScore`: directional projection `∑ i, w i * (x i).toNat`. +* `Cslib.Circuits.Boolean.WeightedThreshold.leInputs`, + `Cslib.Circuits.Boolean.WeightedThreshold.scalarRep`: inputs with scalar score at most `t` and a + canonical representative input for `t`. * `Cslib.Circuits.Boolean.WeightedThreshold.scalarEval`, `Cslib.Circuits.Boolean.WeightedThreshold.scalarTranscript`, `Cslib.Circuits.Boolean.WeightedThreshold.scalarReadout`: extension of gate evaluation, @@ -182,6 +185,7 @@ theorem attainableTranscripts_nonempty (p : Program signature n g) : classical exact ⟨transcript p (fun _ => false), mem_image_of_mem _ (mem_univ _)⟩ +/-- The number of attainable transcripts of `p` is positive. -/ theorem card_attainableTranscripts_pos (p : Program signature n g) : 0 < (attainableTranscripts p).card := (attainableTranscripts_nonempty p).card_pos diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/TranscriptTree.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/TranscriptTree.lean index 4b7837e01..6f4c5230d 100644 --- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/TranscriptTree.lean +++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/TranscriptTree.lean @@ -34,6 +34,8 @@ This construction is semantic and noncomputable; no efficient compiler is assert * `Cslib.Circuits.Boolean.WeightedThreshold.inputOfSplit`: assemble the two sides of an input. * `Cslib.Circuits.Boolean.WeightedThreshold.lineComparison`: express an input-only threshold line as a separable comparison across a coordinate split. +* `Cslib.Circuits.Boolean.WeightedThreshold.gateComparison`: express a gate query with fixed earlier + gate values as a separable comparison across a coordinate split. ## Main results From 9e3699a33239e69bf490df52323e07a4db0941dc Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 24 Oct 2026 20:13:08 +0000 Subject: [PATCH 2/2] doc(Circuit/Boolean): specify fixed-width word subtraction in hitValue and menuHistory (#590) --- .../Computability/Circuit/Boolean/Iteration/Decoder.lean | 8 ++++---- .../Circuit/Boolean/WeightedThreshold/Menus.lean | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Complexity/Computability/Circuit/Boolean/Iteration/Decoder.lean b/Complexity/Computability/Circuit/Boolean/Iteration/Decoder.lean index 406c84252..f558ec837 100644 --- a/Complexity/Computability/Circuit/Boolean/Iteration/Decoder.lean +++ b/Complexity/Computability/Circuit/Boolean/Iteration/Decoder.lean @@ -24,8 +24,8 @@ pairs that a detector never produces. ## Main definitions -* `Cslib.Circuits.Boolean.Iteration.hitValue`: the state `K - index` steps after a checkpoint - payload. +* `Cslib.Circuits.Boolean.Iteration.hitValue`: the state after `(BitVec.ofNat w K - index).toNat` + steps from a checkpoint payload (using the selector's out-of-range fallback above `K`). * `Cslib.Circuits.Boolean.Iteration.repeatedValue`: the prefix state at the time in `[lo, hi)` congruent to `T`. * `Cslib.Circuits.Boolean.Iteration.reconstruct`: the state determined by a pair of records. @@ -143,8 +143,8 @@ private theorem synthesis_repeatedValue (s : Set (BooleanFunction n)) apply (hidx.trans hsel).mono Set.Subset.rfl Set.Subset.rfl nlinarith [Nat.zero_le (K * n ^ 2), Nat.zero_le (K * n * w), Nat.zero_le (K * w ^ 2)] -/-- Synthesizes `hitValue` by unfolding `K` steps of `c` from `payload` and selecting step -`K - index`. -/ +/-- Synthesizes `hitValue` by unfolding `K` steps of `c` from `payload` and selecting the step at +the unsigned value of `BitVec.ofNat w K - index x` (with the selector's out-of-range fallback). -/ theorem synthesis_hitValue {a : ℕ} (s : Set (BooleanFunction a)) (c : Circuit signature n n) (K : ℕ) (index : BitString a → BitVec w) (payload : BitString a → BitString n) diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean index 668ad74b9..0593aacdc 100644 --- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean +++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean @@ -50,7 +50,7 @@ internal weights (`two_pow_lt_of_directionMenus_intWeight`, `two_pow_lt_of_direc * `Cslib.Circuits.Boolean.WeightedThreshold.MenuTable`, `Cslib.Circuits.Boolean.WeightedThreshold.trueMenuTable`, `Cslib.Circuits.Boolean.WeightedThreshold.menuHistory`: precomputed bias-menu threshold tables and - flattened block histories. + intermediate block histories. * `Cslib.Circuits.Boolean.WeightedThreshold.menuBlockDecomposition`: the `(d + g)`-block decomposition precomputing menu tables for a chosen subset of directions.