From c33195005eae3e6da0e33ad648b13d3cefaf9b42 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 17:41:28 -0400 Subject: [PATCH 1/9] feat(circuit/frontier): Boolean tensor networks and their contraction Tensor networks over a commutative semiring as the weighted form of the frontier constraint networks (shared Multigraph and locality), with the contraction Z, subdivision by equality tensors (preserves Z, bipartite, keeps degree bounds), explicit tables with ordered ports and size measures, the write-out theorem, and the 0-1 bridge from constraint networks. Tracking: #1833 (T1), #1538. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 3 + .../Circuit/Frontier/TensorNetwork.lean | 251 ++++++++++++++++++ .../Frontier/TensorNetwork/Constraint.lean | 81 ++++++ .../Frontier/TensorNetwork/Explicit.lean | 210 +++++++++++++++ .../Circuit/Frontier/TensorNetwork.lean | 116 ++++++++ 5 files changed, 661 insertions(+) create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork.lean create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork/Constraint.lean create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean create mode 100644 ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean diff --git a/Complexity.lean b/Complexity.lean index 3942e2e28b..3e53d5172a 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -857,6 +857,9 @@ public import Complexity.Computability.Circuit.Frontier.Projection public import Complexity.Computability.Circuit.Frontier.Rectangle public import Complexity.Computability.Circuit.Frontier.Reduction public import Complexity.Computability.Circuit.Frontier.Sweep +public import Complexity.Computability.Circuit.Frontier.TensorNetwork +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Constraint +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit public import Complexity.Computability.Circuit.Frontier.TwoSidedWitness public import Complexity.Computability.Circuit.Frontier.Unconditional public import Complexity.Computability.Circuit.Frontier.Witness diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork.lean new file mode 100644 index 0000000000..cf45df7f82 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork.lean @@ -0,0 +1,251 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Frontier.Multigraph +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Combinatorics.SimpleGraph.Bipartite +public import Mathlib.Basic.Finite.Sum +public import Mathlib.Data.Fintype.Pi +import Mathlib.Algebra.BigOperators.GroupWithZero.Finset +import Mathlib.Algebra.BigOperators.Ring.Finset + +/-! +# Tensor networks and their contraction + +A *tensor network* over a commutative semiring `R` and an alphabet `U` is a multigraph whose +edges carry values in `U`, with a *tensor* at each vertex `v`: a value `N.tensor v x ∈ R` for each +assignment `x : E → U` of values to the edges, which depends only on the values on the edges at +`v`. Its *contraction* sums, over all assignments, the product of the tensors: + + `Z(N) = ∑ x : E → U, ∏ v, N.tensor v x`. + +A *Boolean* tensor network has `U = Bool`, one bit per edge. The usual presentation gives the +tensor at `v` as a function `F_v` of the bits on the ordered list `δ(v)` of edges at `v`, with +`Z = ∑ x ∏ v F_v (x|δ(v))`. Here the tensor is a function of the whole assignment, constrained to +read only the edges at `v` (`TensorNetwork.tensor_congr`); the ordered presentation, with +explicit tables, is `Cslib.Circuits.Frontier.ExplicitTensorNetwork`, and +`Cslib.Circuits.Frontier.TensorNetwork.contraction_toExplicit` shows that the two contractions +agree. Parallel edges are distinct elements of `E` and so give distinct ports. + +A tensor network is the weighted form of a constraint network +(`Cslib.Circuits.Frontier.Network`) on a fixed input: the two share the multigraph and the +locality condition, and a constraint becomes its `0`–`1` indicator tensor, whose contraction +counts the satisfying assignments +(`Cslib.Circuits.Frontier.Network.contraction_toTensorNetwork`). + +**Subdivision** (`TensorNetwork.subdivide`). Splitting every edge `e` into two edges joined at a +new vertex that carries the *equality tensor* `[y₁ = y₂]` preserves the contraction +(`TensorNetwork.contraction_subdivide`): each assignment of the old network extends in exactly one +way to an assignment of the new one with nonzero weight. The subdivided network is bipartite +(`TensorNetwork.isBipartite_subdivide`), with the old vertices on one side and the new ones on the +other, and it keeps the degree bound of a loopless network (`TensorNetwork.maxDegreeLE_subdivide`). +It has twice as many edges and one new vertex per old edge. + +## Main definitions + +* `Cslib.Circuits.Frontier.Multigraph.IsBipartite`: the vertices split into two sides and every + edge joins the two sides. +* `Cslib.Circuits.Frontier.TensorNetwork`: a tensor network. +* `Cslib.Circuits.Frontier.TensorNetwork.contraction`: its contraction `Z`. +* `Cslib.Circuits.Frontier.TensorNetwork.subdivide`: subdivision of every edge by an equality + tensor. + +## Main results + +* `Cslib.Circuits.Frontier.Multigraph.isBipartite_iff`: a multigraph is bipartite iff it has no + loops and its underlying simple graph is bipartite (`SimpleGraph.IsBipartite`). +* `Cslib.Circuits.Frontier.TensorNetwork.contraction_subdivide`: subdivision preserves the + contraction. +* `Cslib.Circuits.Frontier.TensorNetwork.isBipartite_subdivide`: a subdivided network is + bipartite. +* `Cslib.Circuits.Frontier.TensorNetwork.maxDegreeLE_subdivide`: subdividing a loopless network of + maximum degree at most `d ≥ 2` gives maximum degree at most `d`. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.1 (p. 53) and + the subdivision step of Appendix D.2 (p. 54). +-/ + +@[expose] public section + +namespace Cslib.Circuits.Frontier + +open Set + +/-! ### Bipartite multigraphs -/ + +namespace Multigraph + +variable {V E : Type*} (G : Multigraph V E) + +/-- A multigraph is *bipartite* when its vertices split into two sides, `side v = true` and +`side v = false`, and every edge joins the two sides. A bipartite multigraph has no loops +(`Multigraph.IsBipartite.loopless`). -/ +def IsBipartite : Prop := + ∃ side : V → Bool, ∀ e, side (G.src e) ≠ side (G.tgt e) + +variable {G} + +/-- A bipartite multigraph has no loops. -/ +theorem IsBipartite.loopless (h : G.IsBipartite) : G.Loopless := by + obtain ⟨side, hside⟩ := h + exact fun e he => hside e (congrArg side he) + +/-- A multigraph is bipartite exactly when it has no loops and its underlying simple graph is +bipartite in the sense of Mathlib (`SimpleGraph.IsBipartite`, a `2`-colouring). -/ +theorem isBipartite_iff : G.IsBipartite ↔ G.Loopless ∧ G.toSimpleGraph.IsBipartite := by + constructor + · intro h + refine ⟨h.loopless, ?_⟩ + obtain ⟨side, hside⟩ := h + have hcol : G.toSimpleGraph.Coloring Bool := SimpleGraph.Coloring.mk side fun {u v} huv => by + obtain ⟨-, e, he⟩ := toSimpleGraph_adj.mp huv + rcases Sym2.eq_iff.mp he with ⟨hu, hv⟩ | ⟨hu, hv⟩ + · exact hu ▸ hv ▸ hside e + · exact hu ▸ hv ▸ (hside e).symm + simpa using hcol.colorable + · rintro ⟨hloop, ⟨c⟩⟩ + refine ⟨fun v => decide (c v = 0), fun e he => ?_⟩ + have hadj : G.toSimpleGraph.Adj (G.src e) (G.tgt e) := toSimpleGraph_adj.mpr ⟨hloop e, e, rfl⟩ + have key : ∀ a b : Fin 2, a ≠ b → decide (a = 0) ≠ decide (b = 0) := by decide + exact key _ _ (c.valid hadj) he + +end Multigraph + +/-! ### Tensor networks -/ + +/-- A *tensor network* over the commutative semiring `R` with alphabet `U`: a multigraph on the +vertices `V` and edges `E`, whose edges carry values in `U`, and at each vertex a *tensor*, a value +in `R` for each assignment of values to the edges, that sees only the values on the edges at that +vertex. A *Boolean* tensor network has `U = Bool`. -/ +structure TensorNetwork (R U V E : Type*) extends Multigraph V E where + /-- The tensor at a vertex: its value on an assignment of values to the edges. -/ + tensor : V → (E → U) → R + /-- Tensors are local: the tensor at `v` sees only the values on the edges incident to `v`. -/ + tensor_congr : ∀ v x y, (∀ e, src e = v ∨ tgt e = v → x e = y e) → tensor v x = tensor v y + +namespace TensorNetwork + +variable {R U V E : Type*} + +section Contraction + +variable [CommSemiring R] [Fintype U] [Fintype V] [Fintype E] [DecidableEq E] + +/-- The *contraction* of a tensor network: the sum over all assignments of values to the edges of +the product of the tensors at all vertices. -/ +def contraction (N : TensorNetwork R U V E) : R := + ∑ x : E → U, ∏ v, N.tensor v x + +end Contraction + +/-! ### Subdivision by equality tensors -/ + +section Subdivide + +variable [DecidableEq U] [DecidableEq V] [Zero R] [One R] (N : TensorNetwork R U V E) + +/-- The *subdivision* of a tensor network by equality tensors. Each edge `e` becomes a new vertex +`Sum.inr e` and two edges: `Sum.inl e`, from the source of `e`, and `Sum.inr e`, from its target, +both ending at `Sum.inr e`. The new vertex carries the *equality tensor*, one when its two edges +carry the same value and zero otherwise. An old vertex reads the value of `e` on the half of `e` +at its end. -/ +def subdivide : TensorNetwork R U (V ⊕ E) (E ⊕ E) where + src := Sum.elim (fun e => .inl (N.src e)) (fun e => .inl (N.tgt e)) + tgt := Sum.elim .inr .inr + tensor + | .inl v, y => N.tensor v fun e => if N.src e = v then y (.inl e) else y (.inr e) + | .inr e, y => if y (.inl e) = y (.inr e) then 1 else 0 + tensor_congr := by + rintro (v | e) y y' h + · refine N.tensor_congr v _ _ fun e he => ?_ + by_cases hs : N.src e = v + · simp only [hs, ite_true] + exact h (.inl e) (Or.inl (by simp [hs])) + · simp only [hs, ite_false] + exact h (.inr e) (Or.inl (by simp [he.resolve_left hs])) + · simp only + rw [h (.inl e) (Or.inr rfl), h (.inr e) (Or.inr rfl)] + +@[simp] theorem subdivide_src_inl (e : E) : N.subdivide.src (.inl e) = .inl (N.src e) := rfl + +@[simp] theorem subdivide_src_inr (e : E) : N.subdivide.src (.inr e) = .inl (N.tgt e) := rfl + +@[simp] theorem subdivide_tgt_inl (e : E) : N.subdivide.tgt (.inl e) = .inr e := rfl + +@[simp] theorem subdivide_tgt_inr (e : E) : N.subdivide.tgt (.inr e) = .inr e := rfl + +/-- The tensor at an old vertex of the subdivision. -/ +theorem subdivide_tensor_inl (v : V) (y : E ⊕ E → U) : + N.subdivide.tensor (.inl v) y = + N.tensor v fun e => if N.src e = v then y (.inl e) else y (.inr e) := rfl + +/-- The equality tensor at a new vertex of the subdivision. -/ +theorem subdivide_tensor_inr (e : E) (y : E ⊕ E → U) : + N.subdivide.tensor (.inr e) y = if y (.inl e) = y (.inr e) then 1 else 0 := rfl + +/-- **Subdivision is bipartite.** Every edge of the subdivision joins an old vertex to a new one. -/ +theorem isBipartite_subdivide : N.subdivide.IsBipartite := + ⟨Sum.isLeft, fun e => by cases e <;> simp⟩ + +/-- **Subdivision preserves the contraction.** An assignment of the subdivision has nonzero +weight only when the two halves of every edge carry the same value, and such assignments are +exactly the assignments of the original network. -/ +theorem contraction_subdivide {R : Type*} [CommSemiring R] [Fintype U] [Fintype V] [Fintype E] + [DecidableEq E] (N : TensorNetwork R U V E) : N.subdivide.contraction = N.contraction := by + classical + -- Split an assignment of the subdivision into its values `a` on the source halves and `b` on + -- the target halves. + rw [contraction, contraction, ← (Equiv.sumArrowEquivProdArrow E E U).symm.sum_comp, + Fintype.sum_prod_type] + refine Finset.sum_congr rfl fun a _ => ?_ + simp only [Fintype.prod_sum_type, subdivide_tensor_inl, subdivide_tensor_inr, + Equiv.sumArrowEquivProdArrow_symm_apply_inl, Equiv.sumArrowEquivProdArrow_symm_apply_inr] + rw [Finset.sum_eq_single a] + · -- Equal halves: every equality tensor is one, and the old vertices read `a`. + simp only [ite_self, ite_true, Finset.prod_const_one, mul_one] + · -- Unequal halves on some edge `e`: the equality tensor at `e` vanishes. + intro b _ hb + obtain ⟨e, he⟩ := Function.ne_iff.mp hb + exact mul_eq_zero_of_right _ + (Finset.prod_eq_zero (Finset.mem_univ e) (ite_eq_right fun h => he h.symm)) + · exact fun h => absurd (Finset.mem_univ a) h + +/-- The edges at an old vertex of the subdivision are the halves of its old edges at it. -/ +theorem incidenceSet_subdivide_inl (v : V) : + N.subdivide.incidenceSet (.inl v) = + Sum.inl '' {e | N.src e = v} ∪ Sum.inr '' {e | N.tgt e = v} := by + ext (e | e) <;> simp [Multigraph.mem_incidenceSet] + +/-- The edges at a new vertex of the subdivision are the two halves of its edge. -/ +theorem incidenceSet_subdivide_inr (e : E) : + N.subdivide.incidenceSet (.inr e) = {.inl e, .inr e} := by + ext (e' | e') <;> simp [Multigraph.mem_incidenceSet, eq_comm] + +/-- **Subdivision keeps the degree bound.** In a loopless network, the edges at a vertex are those +with it as source and those with it as target, and they are the halves at its old vertex in the +subdivision; a new vertex has degree two. -/ +theorem maxDegreeLE_subdivide [Finite E] {d : ℕ} (hloop : N.Loopless) + (hd : N.MaxDegreeLE d) (h2 : 2 ≤ d) : N.subdivide.MaxDegreeLE d := by + rintro (v | e) + · rw [incidenceSet_subdivide_inl, ncard_union_eq _ (toFinite _) (toFinite _), + ncard_image_of_injective _ Sum.inl_injective, ncard_image_of_injective _ Sum.inr_injective, + ← ncard_union_eq _ (toFinite _) (toFinite _)] + · exact hd v + · exact disjoint_left.mpr fun e hs ht => hloop e (hs.trans ht.symm) + · exact disjoint_left.mpr fun _ ⟨_, _, h⟩ ⟨_, _, h'⟩ => Sum.inl_ne_inr (h.trans h'.symm) + · rw [incidenceSet_subdivide_inr, ncard_pair Sum.inl_ne_inr] + exact h2 + +end Subdivide + +end TensorNetwork + +end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Constraint.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Constraint.lean new file mode 100644 index 0000000000..08c80a6649 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Constraint.lean @@ -0,0 +1,81 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Frontier.Network +public import Complexity.Computability.Circuit.Frontier.TensorNetwork +import Mathlib.Algebra.BigOperators.GroupWithZero.Finset +import Mathlib.Algebra.BigOperators.Ring.Finset + +/-! +# Constraint networks as `0`–`1` tensor networks + +A constraint network (`Cslib.Circuits.Frontier.Network`) on a fixed input is a tensor network +whose tensors take only the values zero and one: the tensor at `v` is the indicator of the +constraint at `v` (`Network.toTensorNetwork`). The two share the multigraph, and the locality of +the constraints is the locality of the tensors. The contraction of this tensor network is the +number of satisfying assignments (`Network.contraction_toTensorNetwork`), so over `ℕ` it is +nonzero exactly at the accepted inputs (`Network.mem_accepted_iff_contraction_ne_zero`). + +A general tensor network is thus the weighted form of a constraint network, and the frontier +constraint networks of circuits (`Cslib.Circuits.Frontier.Compiler.network`) are special cases. + +## Main definitions + +* `Cslib.Circuits.Frontier.Network.toTensorNetwork`: the indicator tensor network of a constraint + network on an input. + +## Main results + +* `Cslib.Circuits.Frontier.Network.contraction_toTensorNetwork`: its contraction counts the + satisfying assignments. +* `Cslib.Circuits.Frontier.Network.mem_accepted_iff_contraction_ne_zero`: an input is accepted iff + the contraction over `ℕ` is nonzero. +-/ + +@[expose] public section + +namespace Cslib.Circuits.Frontier.Network + +variable {U ι V E : Type*} (R : Type*) (N : Network U ι V E) + +open Classical in +/-- The `0`–`1` tensor network of a constraint network on the input `x`: the same multigraph, with +the tensor at `v` equal to one where the constraint at `v` holds and to zero elsewhere. -/ +noncomputable def toTensorNetwork [Zero R] [One R] (x : ι → U) : TensorNetwork R U V E where + toMultigraph := N.toMultigraph + tensor v α := if N.Constraint v x α then 1 else 0 + tensor_congr v α β h := by + have hiff : N.Constraint v x α ↔ N.Constraint v x β := + ⟨N.constraint_congr v x x α β (fun _ _ => rfl) h, + N.constraint_congr v x x β α (fun _ _ => rfl) fun e he => (h e he).symm⟩ + simp only [hiff] + +/-- The tensor network of a constraint network has the same multigraph. -/ +@[simp] theorem toMultigraph_toTensorNetwork [Zero R] [One R] (x : ι → U) : + (N.toTensorNetwork R x).toMultigraph = N.toMultigraph := + rfl + +/-- **The contraction counts satisfying assignments.** The contraction of the `0`–`1` tensor +network of a constraint network on the input `x` is the number of assignments of values to the +edges that satisfy every constraint on `x`. -/ +theorem contraction_toTensorNetwork [CommSemiring R] [Fintype U] [Fintype V] [Fintype E] + [DecidableEq E] (x : ι → U) : + (N.toTensorNetwork R x).contraction = ({α | N.Satisfies x α} : Set (E → U)).ncard := by + classical + simp only [TensorNetwork.contraction, toTensorNetwork, Fintype.prod_boole, Finset.sum_boole, + Set.ncard_eq_toFinset_card', Set.toFinset_ofPred, Satisfies] + +/-- Over `ℕ`, the contraction is nonzero exactly at the accepted inputs. -/ +theorem mem_accepted_iff_contraction_ne_zero [Fintype U] [Fintype V] [Fintype E] [DecidableEq E] + (x : ι → U) : x ∈ N.accepted ↔ (N.toTensorNetwork ℕ x).contraction ≠ 0 := by + rw [contraction_toTensorNetwork, Nat.cast_id, Ne, Set.ncard_eq_zero (Set.toFinite _), + ← Ne, ← Set.nonempty_iff_ne_empty] + rfl + +end Cslib.Circuits.Frontier.Network diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean new file mode 100644 index 0000000000..28f5dd3f54 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean @@ -0,0 +1,210 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork +import Mathlib.Algebra.BigOperators.Fin +import Mathlib.Data.List.GetD + +/-! +# Explicit Boolean tensor networks + +An *explicit* Boolean tensor network (`ExplicitTensorNetwork R`) is the data an algorithm reads: +the number of edges, numbered `0, 1, …`, and a list of vertices, each given by + +* its ordered list of *ports*, the numbers of the edges at the vertex, and +* its *table*: the value of its tensor when port `i` carries the bit `bs[i]` is the entry at + position `tableIndex bs`, the number whose binary digit `i` is `bs[i]`. + +So a vertex with `k` ports has a table of `2 ^ k` entries. The contraction of an explicit network +(`ExplicitTensorNetwork.contraction`) sums, over all assignments of bits to the edges, the product +of the table entries at the bits on the ports. It needs no well-formedness: a port naming no edge +reads `false`, and a position past the end of a table has entry zero. + +Its size measures are the number of edges, the number of vertices, the maximum number of ports of +a vertex (`ExplicitTensorNetwork.maxDegree`) and the total length of the tables +(`ExplicitTensorNetwork.tableLength`). + +**Writing a network out** (`TensorNetwork.toExplicit`). Given numberings of the vertices and the +edges of a Boolean tensor network on finite types, list the edges at each vertex in increasing +order and tabulate its tensor on them. The contraction is unchanged +(`TensorNetwork.contraction_toExplicit`). + +## Main definitions + +* `Cslib.Circuits.Frontier.tableIndex`: the position of a list of bits in a table. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork`: an explicit Boolean tensor network. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.entry`, + `Cslib.Circuits.Frontier.ExplicitTensorNetwork.portBits`: table lookup and the bits on a list + of ports. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.contraction`: the contraction. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.maxDegree`, + `Cslib.Circuits.Frontier.ExplicitTensorNetwork.tableLength`: size measures. +* `Cslib.Circuits.Frontier.TensorNetwork.explicitPorts`, + `Cslib.Circuits.Frontier.TensorNetwork.explicitTable`, + `Cslib.Circuits.Frontier.TensorNetwork.toExplicit`: writing a Boolean tensor network out. + +## Main results + +* `Cslib.Circuits.Frontier.testBit_tableIndex`, `Cslib.Circuits.Frontier.tableIndex_lt`: the + digits and range of a table position. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.maxDegree_le_iff`: the degree bound. +* `Cslib.Circuits.Frontier.TensorNetwork.entry_explicitTable`: a written-out table evaluates the + tensor. +* `Cslib.Circuits.Frontier.TensorNetwork.contraction_toExplicit`: writing a network out preserves + its contraction. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.1 (p. 53). +-/ + +@[expose] public section + +namespace Cslib.Circuits.Frontier + +/-- The position of a list of bits in a table: the number whose binary digit `i` is `bs[i]`, so +that the bits are read little-endian. -/ +def tableIndex (bs : List Bool) : ℕ := + (BitVec.ofBoolListLE bs).toNat + +/-- Binary digit `i` of the position of `bs` is `bs[i]`, or `false` past the end of `bs`. -/ +@[simp] theorem testBit_tableIndex (bs : List Bool) (i : ℕ) : + (tableIndex bs).testBit i = bs.getD i false := by + rw [tableIndex, BitVec.testBit_toNat, BitVec.getLsbD_ofBoolListLE] + +/-- A list of `k` bits has a position below `2 ^ k`. -/ +theorem tableIndex_lt (bs : List Bool) : tableIndex bs < 2 ^ bs.length := + BitVec.isLt _ + +/-- An *explicit Boolean tensor network* over `R`: the number of edges, numbered from zero, and a +list of vertices. A vertex is given by its ordered list of *ports*, the numbers of its edges, and +its *table*, whose entry at position `tableIndex bs` is the value of its tensor when port `i` +carries the bit `bs[i]`. -/ +structure ExplicitTensorNetwork (R : Type*) where + /-- The number of edges; the edges are numbered `0, …, numEdges - 1`. -/ + numEdges : ℕ + /-- The vertices, each given by its ports and its table. -/ + vertices : List (List ℕ × List R) + +namespace ExplicitTensorNetwork + +variable {R : Type*} (d : ExplicitTensorNetwork R) + +/-- The entry of a table at a list of bits. A position past the end of the table has entry +zero. -/ +def entry [Zero R] (table : List R) (bs : List Bool) : R := + table.getD (tableIndex bs) 0 + +/-- The bits on a list of ports under an assignment of bits to the edges. A port naming no edge +reads `false`. -/ +def portBits (x : Fin d.numEdges → Bool) (ports : List ℕ) : List Bool := + ports.map fun i => if h : i < d.numEdges then x ⟨i, h⟩ else false + +/-- The *contraction* of an explicit network: the sum over all assignments of bits to the edges of +the product, over the vertices, of the table entries at the bits on their ports. -/ +def contraction [CommSemiring R] : R := + ∑ x : Fin d.numEdges → Bool, (d.vertices.map fun v => entry v.2 (d.portBits x v.1)).prod + +/-- The *maximum degree*: the largest number of ports of a vertex, or zero without vertices. -/ +def maxDegree : ℕ := + (d.vertices.map fun v => v.1.length).foldr max 0 + +/-- The total length of the tables. -/ +def tableLength : ℕ := + (d.vertices.map fun v => v.2.length).sum + +private theorem foldr_max_le_iff (l : List ℕ) (k : ℕ) : l.foldr max 0 ≤ k ↔ ∀ n ∈ l, n ≤ k := by + induction l with + | nil => simp + | cons a l ih => simp [ih] + +/-- The maximum degree is at most `k` exactly when every vertex has at most `k` ports. -/ +theorem maxDegree_le_iff {k : ℕ} : d.maxDegree ≤ k ↔ ∀ v ∈ d.vertices, v.1.length ≤ k := by + rw [maxDegree, foldr_max_le_iff] + constructor + · exact fun h v hv => h _ (List.mem_map_of_mem hv) + · rintro h _ hn + obtain ⟨v, hv, rfl⟩ := List.mem_map.mp hn + exact h v hv + +/-- Every vertex has at most `maxDegree` ports. -/ +theorem length_le_maxDegree {v : List ℕ × List R} (hv : v ∈ d.vertices) : + v.1.length ≤ d.maxDegree := + d.maxDegree_le_iff.mp le_rfl v hv + +end ExplicitTensorNetwork + +/-! ### Writing a tensor network out -/ + +namespace TensorNetwork + +variable {R V E : Type*} [DecidableEq V] {n m : ℕ} (N : TensorNetwork R Bool V E) (ev : V ≃ Fin n) + (ee : E ≃ Fin m) + +/-- The ports of a vertex when the edges are numbered by `ee`: the numbers of the edges at the +vertex, in increasing order. -/ +def explicitPorts (v : V) : List (Fin m) := + (List.finRange m).filter fun j => N.src (ee.symm j) = v ∨ N.tgt (ee.symm j) = v + +/-- An edge is a port of `v` exactly when it is incident to `v`. -/ +@[simp] theorem mem_explicitPorts {v : V} {j : Fin m} : + j ∈ N.explicitPorts ee v ↔ N.src (ee.symm j) = v ∨ N.tgt (ee.symm j) = v := by + simp [explicitPorts] + +/-- The table of a vertex: its tensor at each list of bits on its ports, by position. -/ +def explicitTable (v : V) : List R := + (List.range (2 ^ (N.explicitPorts ee v).length)).map fun j => + N.tensor v fun e => j.testBit ((N.explicitPorts ee v).idxOf (ee e)) + +/-- **A written-out table evaluates the tensor.** At the bits that an assignment puts on the ports +of `v`, the table of `v` has the value of the tensor at that assignment. -/ +theorem entry_explicitTable [Zero R] (v : V) (x : Fin m → Bool) : + ExplicitTensorNetwork.entry (N.explicitTable ee v) ((N.explicitPorts ee v).map x) = + N.tensor v (x ∘ ee) := by + set ps := N.explicitPorts ee v + have hlt : tableIndex (ps.map x) < (N.explicitTable ee v).length := by + simpa [explicitTable, ps] using tableIndex_lt (ps.map x) + rw [ExplicitTensorNetwork.entry, List.getD_eq_getElem _ _ hlt] + simp only [explicitTable, List.getElem_map, List.getElem_range] + refine N.tensor_congr v _ _ fun e he => ?_ + have hmem : ee e ∈ ps := (N.mem_explicitPorts ee).mpr (by simpa using he) + have hidx := List.idxOf_lt_length_of_mem hmem + rw [testBit_tableIndex, List.getD_eq_getElem _ _ (by simpa using hidx), List.getElem_map, + List.getElem_idxOf hidx, Function.comp_apply] + +/-- A Boolean tensor network on finite types written out as an explicit network, numbering the +vertices by `ev` and the edges by `ee`: vertex `i` is `ev.symm i`, with its ports in increasing +order and its table. -/ +def toExplicit : ExplicitTensorNetwork R where + numEdges := m + vertices := List.ofFn fun i => + ((N.explicitPorts ee (ev.symm i)).map Fin.val, N.explicitTable ee (ev.symm i)) + +/-- **Writing a network out preserves its contraction.** -/ +theorem contraction_toExplicit [CommSemiring R] [Fintype V] [Fintype E] [DecidableEq E] : + (N.toExplicit ev ee).contraction = N.contraction := by + rw [ExplicitTensorNetwork.contraction, contraction] + refine Fintype.sum_equiv (ee.symm.arrowCongr (Equiv.refl Bool)) _ _ fun x => ?_ + have hv : (N.toExplicit ev ee).vertices = List.ofFn fun i => + ((N.explicitPorts ee (ev.symm i)).map Fin.val, N.explicitTable ee (ev.symm i)) := rfl + rw [hv, List.map_ofFn, List.prod_ofFn, ← ev.symm.prod_comp] + refine Finset.prod_congr rfl fun i _ => ?_ + -- Every port names an edge, so the bits on the ports are those of the assignment. + have hbits : (N.toExplicit ev ee).portBits x ((N.explicitPorts ee (ev.symm i)).map Fin.val) = + (N.explicitPorts ee (ev.symm i)).map x := by + unfold ExplicitTensorNetwork.portBits + rw [List.map_map] + exact List.map_congr_left fun j _ => dite_eq_left j.isLt + simp only [Function.comp_apply] + rw [hbits, entry_explicitTable] + rfl + +end TensorNetwork + +end Cslib.Circuits.Frontier diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean new file mode 100644 index 0000000000..5be31a11e9 --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean @@ -0,0 +1,116 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: local-only (test driver) + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Constraint +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit +public import Mathlib.Data.ZMod.Defs + +/-! +# Tests for tensor networks + +Hand-checked contractions of small explicit Boolean tensor networks (two parallel edges, and +four-cycles of equality and negation tensors over `ZMod 8`), a tensor network on finite types +written out and subdivided, and a constraint network counted by its indicator tensor network. +-/ + +@[expose] public section + +namespace ComplexityTests.Computability.Circuit.Frontier.TensorNetwork + +open Cslib.Circuits.Frontier + +/-! ### Explicit networks -/ + +/-- Two vertices joined by two parallel edges `0` and `1`, with the tables `A = (1, 2, 3, 4)` and +`B = (5, 6, 7, 8)`, read at positions `x₀ + 2 x₁`. -/ +def parallel : ExplicitTensorNetwork ℤ := + ⟨2, [([0, 1], [1, 2, 3, 4]), ([0, 1], [5, 6, 7, 8])]⟩ + +/-- By hand: `Z = ∑ᵢ Aᵢ Bᵢ = 1·5 + 2·6 + 3·7 + 4·8 = 70`. -/ +example : parallel.contraction = 70 := by decide + +example : parallel.maxDegree = 2 ∧ parallel.tableLength = 8 := by decide + +/-- The equality tensor on two ports. -/ +def eqTable : List (ZMod 8) := [1, 0, 0, 1] + +/-- The negation tensor on two ports: its two bits differ. -/ +def neTable : List (ZMod 8) := [0, 1, 1, 0] + +/-- A bipartite four-cycle `r₀ - c₀ - r₁ - c₁ - r₀` on the edges `0, 1, 2, 3`, with the table `t` +at `c₁` and equality tensors elsewhere. -/ +def cycle (t : List (ZMod 8)) : ExplicitTensorNetwork (ZMod 8) := + ⟨4, [([3, 0], eqTable), ([0, 1], eqTable), ([1, 2], eqTable), ([2, 3], t)]⟩ + +/-- With equality tensors all around, an assignment contributes exactly when all four bits are +equal: `Z = 2`. -/ +example : (cycle eqTable).contraction = 2 := by decide + +/-- One negation on a cycle forces an odd number of bit changes around it, which is impossible: +`Z = 0`. -/ +example : (cycle neTable).contraction = 0 := by decide + +/-! ### A network on finite types, written out and subdivided -/ + +/-- The table `A` or `B` of `parallel` as a tensor on assignments to `Fin 2`. -/ +def table (v : Fin 2) (x : Fin 2 → Bool) : ℤ := + [[1, 2, 3, 4], [5, 6, 7, 8]][v]!.getD (tableIndex [x 0, x 1]) 0 + +/-- The network `parallel` on `Fin 2` vertices and `Fin 2` edges, both edges from `0` to `1`. +Every edge is at both vertices, so the tensors are trivially local. -/ +def parallelNetwork : TensorNetwork ℤ Bool (Fin 2) (Fin 2) where + src _ := 0 + tgt _ := 1 + tensor := table + tensor_congr v x y h := by + have hxy : x = y := funext fun e => h e (by fin_cases v <;> simp) + rw [hxy] + +/-- Writing the network out gives `parallel` up to the order of its data, and the same +contraction. -/ +example : parallelNetwork.contraction = 70 := by + rw [← parallelNetwork.contraction_toExplicit (Equiv.refl _) (Equiv.refl _)] + decide + +/-- Subdividing both edges by equality tensors gives a bipartite network with the same +contraction and degree bound. -/ +example : parallelNetwork.subdivide.contraction = 70 ∧ parallelNetwork.subdivide.IsBipartite ∧ + parallelNetwork.subdivide.MaxDegreeLE 2 := by + refine ⟨?_, parallelNetwork.isBipartite_subdivide, + parallelNetwork.maxDegreeLE_subdivide (fun e => by simp [parallelNetwork]) (fun v => ?_) + le_rfl⟩ + · rw [TensorNetwork.contraction_subdivide, + ← parallelNetwork.contraction_toExplicit (Equiv.refl _) (Equiv.refl _)] + decide + · exact (Set.ncard_le_card _).trans (by simp) + +/-! ### Constraint networks -/ + +/-- Two vertices joined by two parallel edges, each requiring its two edges to agree. -/ +def agree : Network Bool Empty (Fin 2) (Fin 2) where + src _ := 0 + tgt _ := 1 + site := Empty.elim + Constraint _ _ α := α 0 = α 1 + constraint_congr v _ _ α β _ h hα := by + have h' : ∀ e, α e = β e := fun e => h e (by fin_cases v <;> simp) + rw [← h' 0, ← h' 1] + exact hα + +/-- The indicator tensor network of `agree` counts its two satisfying assignments. -/ +example : (agree.toTensorNetwork ℕ Empty.elim).contraction = 2 := by + rw [Network.contraction_toTensorNetwork, Nat.cast_id] + have hsat : {α | agree.Satisfies Empty.elim α} = {fun _ => false, fun _ => true} := by + ext α + simp only [Network.Satisfies, agree, Set.mem_ofPred_eq, forall_const, Set.mem_insert_iff, + Set.mem_singleton_iff, funext_iff, Fin.forall_fin_two] + cases α 0 <;> cases α 1 <;> simp + rw [hsat, Set.ncard_pair (fun h => Bool.false_ne_true (congrFun h 0))] + +end ComplexityTests.Computability.Circuit.Frontier.TensorNetwork From da93e6d6579ef4ba3ffca28fed5d8a91fff0018e Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 17:41:53 -0400 Subject: [PATCH 2/9] feat(time): accepting choice-string counts for NTIME and BPTIME (#1833 H1) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Define the accepting count of a closed fair-coin table, the number of choice strings of a given length on which it emits [true], and relate it to the existing semantics: the probability of output [true] is the count divided by 2^τ; a nondeterministic decider's choice table has a positive count exactly on members; a bounded-error decider has a strict-majority count exactly on members, at every τ at least the clock. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + .../Complexity/Classes/Time/AcceptCount.lean | 137 +++++++++++++++ .../MultiTape/Probabilistic/AcceptCount.lean | 103 +++++++++++ ComplexityTests/HPVChoiceCount.lean | 161 ++++++++++++++++++ 4 files changed, 403 insertions(+) create mode 100644 Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean create mode 100644 ComplexityTests/HPVChoiceCount.lean diff --git a/Complexity.lean b/Complexity.lean index 3942e2e28b..ce92f5d3ef 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1177,6 +1177,7 @@ public import Complexity.Computability.Complexity.Classes.TFNP.Subclasses public import Complexity.Computability.Complexity.Classes.TFNP.Subclasses.Completeness public import Complexity.Computability.Complexity.Classes.TFNP.Subclasses.Principles public import Complexity.Computability.Complexity.Classes.Time +public import Complexity.Computability.Complexity.Classes.Time.AcceptCount public import Complexity.Computability.Complexity.Classes.Time.Polynomial public import Complexity.Computability.Complexity.Classes.Toda public import Complexity.Computability.Complexity.Classes.Toda.Counting @@ -1795,6 +1796,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.WhileC public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.WhileInput public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.AcceptCount public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Clock public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Closed public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.CoinTape diff --git a/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean b/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean new file mode 100644 index 0000000000..47496225e5 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean @@ -0,0 +1,137 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.Time +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.AcceptCount + +/-! +# Time classes through accepting choice strings + +Problems in `NTIME` and `BPTIME` are decided by comparing the accepting count of a fixed +binary-choice machine (`Turing.MultiTapePTM.acceptCount`) with a threshold, at every number `τ` +of choice bits at least a linear function of the time bound. This is the normal form used by +counting simulations of nondeterministic and probabilistic time, which compute the accepting +count exactly. + +* A nondeterministic decider is replayed by its choice table `Turing.MultiTapeNTM.choiceTable`, + which encodes each choice in binary and rejects at a stuck configuration: an instance is a + member exactly when the accepting count is positive + (`Turing.MultiTapeNTM.DecidesInTime.mem_iff_acceptCount_choiceTable_pos`). +* A bounded-error fair-coin decider accepts a member with probability at least `2 / 3` and a + nonmember with probability at most `1 / 3`, so an instance is a member exactly when more than + half of the choice strings accept + (`Turing.MultiTapePTM.DecidesWithBoundedErrorInTime.mem_iff_two_pow_lt_two_mul_acceptCount`). + +Both hold for every `τ` at least the clock: a halted table ignores further bits. + +## Main results + +* `Turing.MultiTapeNTM.DecidesInTime.mem_iff_acceptCount_choiceTable_pos`: nondeterministic + acceptance is a positive accepting count. +* `Turing.MultiTapePTM.DecidesWithBoundedErrorInTime.mem_iff_two_pow_lt_two_mul_acceptCount`: + bounded-error acceptance is a strict-majority accepting count. +* `Cslib.Complexity.exists_acceptCount_of_mem_NTIME`, + `Cslib.Complexity.exists_acceptCount_of_mem_BPTIME`: the class-level normal forms. +-/ + +public section + +namespace Turing.MultiTapeNTM + +variable {k : ℕ} {State : Type} [Finite State] {α : Type} {enc : α ↪ List Bool} + +/-- **Nondeterministic acceptance is a positive accepting count.** If `ntm` decides `A` within +`t`, then `a ∈ A` exactly when some choice string of length `τ` makes the choice table accept, +for every `τ` of at least `M * t a`, where `M` is the number of actions. -/ +theorem DecidesInTime.mem_iff_acceptCount_choiceTable_pos {ntm : MultiTapeNTM k Bool State} + {A : Set α} {t : α → ℕ} (h : ntm.DecidesInTime enc A t) {a : α} {τ : ℕ} + (hτ : Nat.card (Turing.Action k Bool State) * t a ≤ τ) : + a ∈ A ↔ 0 < ntm.choiceTable.acceptCount (enc a) τ := by + rw [h.mem_iff_exists_checkChoices hτ, MultiTapePTM.acceptCount_pos_iff] + simp only [checkChoices, decide_eq_true_eq] + +end Turing.MultiTapeNTM + +namespace Turing.MultiTapePTM + +open Cslib +open scoped ENNReal + +variable {k : ℕ} {State : Type} {α : Type} {enc : α ↪ List Bool} + +/-- A probability of at least `2 / 3` is more than one half. -/ +private theorem inv_two_lt_of_two_div_three_le {p : ℝ≥0∞} (h : 2 / 3 ≤ p) : 2⁻¹ < p := by + refine lt_of_lt_of_le ?_ h + rw [ENNReal.lt_div_iff_mul_lt (by simp) (by simp), ← ENNReal.div_eq_inv_mul, + ENNReal.div_lt_iff (by simp) (by simp)] + norm_num + +/-- Two distinct outcomes have total probability at most one. -/ +private theorem apply_add_apply_le_one {β : Type} (P : PMF β) {b b' : β} (hb : b ≠ b') : + P b + P b' ≤ 1 := by + classical + rw [← Finset.sum_pair hb, ← P.tsum_coe] + exact sum_le_tsum _ + +/-- **Bounded-error acceptance is a strict-majority accepting count.** If `machine` decides `A` +with bounded error within `t`, then `a ∈ A` exactly when more than half of the choice strings of +length `τ` accept, for every `τ` of at least `t a`. -/ +theorem DecidesWithBoundedErrorInTime.mem_iff_two_pow_lt_two_mul_acceptCount + {machine : MultiTapePTM k Bool State} {A : Set α} {t : α → ℕ} + (h : machine.DecidesWithBoundedErrorInTime enc A t) {a : α} {τ : ℕ} (hτ : t a ≤ τ) : + a ∈ A ↔ 2 ^ τ < 2 * machine.acceptCount (enc a) τ := by + obtain ⟨hhalt, hprob⟩ := h a + rw [← machine.eval_runClosed_eq_of_halted (enc a) hτ hhalt] at hprob + rw [← half_lt_eval_runClosed_apply_iff] + by_cases ha : a ∈ A + · simp only [MultiTapeTM.indicator, ha] at hprob + exact iff_of_true ha (inv_two_lt_of_two_div_three_le hprob) + · simp only [MultiTapeTM.indicator, ha] at hprob + refine iff_of_false ha fun htrue => ?_ + have hsum := apply_add_apply_le_one (ProbComp.eval (machine.runClosed τ (enc a))) + (b := [true]) (b' := [false]) (by simp) + exact absurd ((ENNReal.inv_two_add_inv_two.symm.trans_lt + (ENNReal.add_lt_add htrue (inv_two_lt_of_two_div_three_le hprob))).trans_le hsum) + (lt_irrefl 1) + +end Turing.MultiTapePTM + +namespace Cslib.Complexity + +open _root_.Turing + +variable {α : Type} {enc : α ↪ List Bool} {A : Set α} {t : ℕ → ℕ} + +/-- **Nondeterministic time as accepting counts.** A problem in `NTIME enc t` is decided by a +fixed binary-choice machine with a binary alphabet and finitely many states: for constants `c₁` +and `c₂`, an instance is a member exactly when its accepting count on `τ` choice bits is +positive, for every `τ ≥ c₁ * t n + c₂` on instances of encoded length `n`. -/ +theorem exists_acceptCount_of_mem_NTIME (h : A ∈ NTIME enc t) : + ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapePTM k Bool State) (c₁ c₂ : ℕ), + ∀ a τ, c₁ * t (enc a).length + c₂ ≤ τ → (a ∈ A ↔ 0 < machine.acceptCount (enc a) τ) := by + obtain ⟨c₁, c₂, k, State, hfinite, ntm, hntm⟩ := h + set M := Nat.card (Turing.Action k Bool State) + refine ⟨k, _, inferInstance, ntm.choiceTable, M * c₁, M * c₂, fun a τ hτ => + hntm.mem_iff_acceptCount_choiceTable_pos ?_⟩ + rw [Nat.mul_add, ← Nat.mul_assoc] + exact hτ + +/-- **Bounded-error probabilistic time as accepting counts.** A problem in `BPTIME enc t` is +decided by a fixed fair-coin machine with a binary alphabet and finitely many states: for +constants `c₁` and `c₂`, an instance is a member exactly when more than half of its choice +strings of length `τ` accept, for every `τ ≥ c₁ * t n + c₂` on instances of encoded length `n`. -/ +theorem exists_acceptCount_of_mem_BPTIME (h : A ∈ BPTIME enc t) : + ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapePTM k Bool State) (c₁ c₂ : ℕ), + ∀ a τ, c₁ * t (enc a).length + c₂ ≤ τ → + (a ∈ A ↔ 2 ^ τ < 2 * machine.acceptCount (enc a) τ) := by + obtain ⟨c₁, c₂, k, State, hfinite, machine, hmachine⟩ := h + exact ⟨k, State, hfinite, machine, c₁, c₂, fun a τ hτ => + hmachine.mem_iff_two_pow_lt_two_mul_acceptCount hτ⟩ + +end Cslib.Complexity diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean new file mode 100644 index 0000000000..1f0692c761 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean @@ -0,0 +1,103 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Machines.Turing.MultiTape.Machine.Nondeterministic +import Mathlib.Data.Fintype.Pi + +/-! +# Accepting choice strings of a fair-coin table + +A closed fair-coin table `Turing.MultiTapePTM k Bool State` is the binary-choice normal form of a +machine: a run is a deterministic replay of a list of choice bits, one bit per live step. When +both branches of an instruction agree, its bit is ignored, and a halted configuration ignores all +further bits (`Turing.MultiTapePTM.stepCoins`). So every run on `τ` bits is padded to exactly `τ` +steps. A nondeterministic machine with finitely many states and a binary alphabet is put in this +form by its choice table `Turing.MultiTapeNTM.choiceTable`, which encodes each choice in binary and +rejects at a stuck configuration. + +The *accepting count* `Turing.MultiTapePTM.acceptCount machine input τ` is the number of bit +strings `y ∈ {0,1}^τ` on which the table emits `[true]` on `input`: the count `A_M(x)` of the +counting simulations of nondeterministic and probabilistic time. Its fraction of all `2 ^ τ` +strings is exactly the probability that the closed fair-coin run outputs `[true]` +(`Turing.MultiTapePTM.eval_runClosed_apply_eq_acceptCount`). The membership characterizations +for nondeterministic and bounded-error deciders are in +`Complexity.Computability.Complexity.Classes.Time.AcceptCount`. + +## Main definitions + +* `Turing.MultiTapePTM.acceptCount`: the number of accepting choice strings of a given length. + +## Main results + +* `Turing.MultiTapePTM.eval_runClosed_apply_eq_acceptCount`: the probability of output `[true]` + is the accepting count divided by `2 ^ τ`. +* `Turing.MultiTapePTM.half_lt_eval_runClosed_apply_iff`: strict majority acceptance, as an + integer comparison `2 ^ τ < 2 * acceptCount`. +* `Turing.MultiTapePTM.acceptCount_pos_iff`: some choice string accepts. +* `Turing.MultiTapePTM.acceptCount_le_two_pow`: at most all `2 ^ τ` strings accept. +* `Turing.MultiTapePTM.runClosedCoins_eq_output_stepCoins`: the replay on upstream + configurations. +-/ + +public section + +namespace Turing.MultiTapePTM + +open Cslib Cslib.Probability +open scoped ENNReal + +variable {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) (input : List Bool) + (τ : ℕ) + +/-- **The accepting count** `A_M(x)`: the number of choice strings `y ∈ {0,1}^τ` replaying +which the closed fair-coin table emits `[true]` on `input`. -/ +def acceptCount : ℕ := + (Finset.univ.filter fun y : Fin τ → Bool => + machine.runClosedCoins (List.ofFn y) input = [true]).card + +/-- At most all `2 ^ τ` choice strings accept. -/ +theorem acceptCount_le_two_pow : machine.acceptCount input τ ≤ 2 ^ τ := + (Finset.card_filter_le _ _).trans (by simp) + +/-- The accepting count is positive exactly when some choice string of length `τ` accepts. -/ +theorem acceptCount_pos_iff : + 0 < machine.acceptCount input τ ↔ + ∃ coins : List Bool, coins.length = τ ∧ machine.runClosedCoins coins input = [true] := by + rw [acceptCount, Finset.card_pos, Finset.filter_nonempty_iff] + constructor + · rintro ⟨y, -, hy⟩ + exact ⟨List.ofFn y, List.length_ofFn, hy⟩ + · rintro ⟨coins, rfl, hcoins⟩ + exact ⟨fun i => coins[i.val], Finset.mem_univ _, by rwa [List.ofFn_getElem]⟩ + +/-- **Acceptance probability is the accepting fraction.** The closed fair-coin run with clock +`τ` outputs `[true]` with probability `acceptCount / 2 ^ τ`. -/ +theorem eval_runClosed_apply_eq_acceptCount : + ProbComp.eval (machine.runClosed τ input) [true] = + (machine.acceptCount input τ : ℝ≥0∞) / 2 ^ τ := by + rw [eval_runClosed_eq_map_coins, BitString.uniformList_map_apply] + rfl + +/-- **Strict majority acceptance** is the integer comparison `2 ^ τ < 2 * acceptCount`. -/ +theorem half_lt_eval_runClosed_apply_iff : + 2⁻¹ < ProbComp.eval (machine.runClosed τ input) [true] ↔ + 2 ^ τ < 2 * machine.acceptCount input τ := by + rw [eval_runClosed_apply_eq_acceptCount, ENNReal.lt_div_iff_mul_lt (by simp) (by simp), + ← ENNReal.div_eq_inv_mul, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] + exact_mod_cast Iff.rfl + +/-- The replay on the configurations of the shared interpreter is the replay on upstream +configurations, by deterministic steps under each coin. -/ +theorem runClosedCoins_eq_output_stepCoins (coins : List Bool) : + machine.runClosedCoins coins input = + (machine.stepCoins coins (Cfg.init machine.initial input)).output := by + rw [runClosedCoins, tapes_runClosedConfigFromCoins] + rfl + +end Turing.MultiTapePTM diff --git a/ComplexityTests/HPVChoiceCount.lean b/ComplexityTests/HPVChoiceCount.lean new file mode 100644 index 0000000000..d76ffc8f3b --- /dev/null +++ b/ComplexityTests/HPVChoiceCount.lean @@ -0,0 +1,161 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Complexity.Classes.Time.AcceptCount + +/-! Accepting choice strings of concrete fair-coin and nondeterministic machines. -/ + +namespace ComplexityTests.HPVChoiceCount + +open Cslib Turing +open scoped ENNReal + +/-- Emit the first coin and halt. -/ +private def emitCoin : MultiTapePTM 0 Bool Unit where + initial := () + tr _ _ _ _ bit := .step + { inputTape := 0, workTapes := Fin.elim0, output := some bit, state := none } + Empty.elim Empty.elim + +-- No step is taken without a choice bit: nothing is accepted. +example : emitCoin.acceptCount [] 0 = 0 := by decide + +-- After the first step the machine has halted, and the remaining bits are ignored. +example : emitCoin.acceptCount [] 1 = 1 := by decide +example : emitCoin.acceptCount [true, false] 3 = 4 := by decide + +-- The accepted fraction is the probability of output `[true]`. +example : ProbComp.eval (emitCoin.runClosed 3 [true, false]) [true] = 4 / 8 := by + rw [MultiTapePTM.eval_runClosed_apply_eq_acceptCount, + show emitCoin.acceptCount [true, false] 3 = 4 by decide] + norm_num + +-- Exactly half accept: this is not a strict majority. +example : ¬ 2⁻¹ < ProbComp.eval (emitCoin.runClosed 3 []) [true] := by + rw [MultiTapePTM.half_lt_eval_runClosed_apply_iff, + show emitCoin.acceptCount [] 3 = 4 by decide] + decide + +/-- Run two steps, each ignoring its coin, then emit `true` exactly when the input is +nonempty. -/ +private def readInput : MultiTapePTM 0 Bool (Fin 2) where + initial := 0 + tr state symbol _ _ _ := .step + (if state = 0 then { inputTape := 0, workTapes := Fin.elim0, output := none, state := some 1 } + else { inputTape := 0, workTapes := Fin.elim0, output := some symbol.isSome, state := none }) + Empty.elim Empty.elim + +-- Ignored bits still count: every string accepts, or none does. +example : readInput.acceptCount [false] 3 = 8 := by decide +example : readInput.acceptCount [] 3 = 0 := by decide +-- Before the decision step, no string accepts. +example : readInput.acceptCount [false] 1 = 0 := by decide + +/-! ### A bounded-error decider and the strict-majority criterion -/ + +/-- Emit `true` exactly when the first input symbol is `true`, ignoring the coin. -/ +private def echo : MultiTapePTM 0 Bool Unit where + initial := () + tr _ symbol _ _ _ := .step + { inputTape := 0, workTapes := Fin.elim0, output := some (symbol == some true), state := none } + Empty.elim Empty.elim + +/-- `echo` decides `{true}` (encoded as one-symbol words) with no error within one step. -/ +private theorem echo_decides : + echo.DecidesWithBoundedErrorInTime MultiTapeTM.encBool {b | b = true} fun _ => 1 := by + intro a + refine ⟨fun final hfinal => ?_, ?_⟩ + · rw [MultiTapePTM.eval_runClosedConfigFrom_eq_map_coins, PMF.mem_support_map_iff] at hfinal + obtain ⟨coins, hcoins, rfl⟩ := hfinal + obtain ⟨c, rfl⟩ := List.length_eq_one_iff.mp + (BitString.mem_support_uniformList_iff.mp hcoins) + cases a <;> cases c <;> rfl + · rw [MultiTapePTM.eval_runClosed_eq_map_coins, BitString.uniformList_map_apply] + cases a + · rw [show MultiTapeTM.indicator {b : Bool | b = true} false = false by + simp [MultiTapeTM.indicator]] + rw [show (Finset.univ.filter fun r : Fin 1 → Bool => + echo.runClosedCoins (List.ofFn r) (MultiTapeTM.encBool false) = [false]).card = 2 by + decide] + norm_num [ENNReal.div_self] + exact ENNReal.div_le_of_le_mul (by norm_num) + · rw [show MultiTapeTM.indicator {b : Bool | b = true} true = true by + simp [MultiTapeTM.indicator]] + rw [show (Finset.univ.filter fun r : Fin 1 → Bool => + echo.runClosedCoins (List.ofFn r) (MultiTapeTM.encBool true) = [true]).card = 2 by + decide] + norm_num [ENNReal.div_self] + exact ENNReal.div_le_of_le_mul (by norm_num) + +-- With more bits than the clock, a member is accepted by all `2 ^ 4` strings. +example : true ∈ {b : Bool | b = true} ↔ 2 ^ 4 < 2 * echo.acceptCount [true] 4 := + echo_decides.mem_iff_two_pow_lt_two_mul_acceptCount (a := true) (by norm_num) +example : echo.acceptCount [true] 4 = 16 ∧ echo.acceptCount [false] 4 = 0 := by decide + +/-! ### Nondeterministic deciders through their choice tables -/ + +/-- Halt with output `[b]`. -/ +private def emit (b : Bool) : Action 0 Bool Bool := + { inputTape := 0, workTapes := Fin.elim0, output := some b, state := none } + +/-- From its only running state, either accept or reject. -/ +private def guess : MultiTapeNTM 0 Bool Bool where + q₀ := false + Tr q _ _ action := q = false ∧ (action = emit true ∨ action = emit false) + +private theorem guess_decides : + guess.DecidesInTime (Function.Embedding.refl (List Bool)) Set.univ fun _ => 1 := by + intro a + refine ⟨MultiTapeNTM.runsInTime_one_of_forall_step_initCfg fun c hc => ?_, ?_⟩ + · simp only [MultiTapeNTM.Step, MultiTapeNTM.initCfg, Cfg.init] at hc + obtain ⟨action, ⟨-, rfl | rfl⟩, rfl⟩ := hc <;> rfl + · have hstep : guess.Step (guess.initCfg a) ((emit true).apply (guess.initCfg a)) := + ⟨emit true, ⟨rfl, .inl rfl⟩, rfl⟩ + exact iff_of_true trivial + ⟨⟨(RelSeries.singleton _ _).cons (guess.initCfg a) hstep, rfl⟩, rfl, rfl⟩ + +-- The accepting branch is encoded by some padded choice string, of every sufficient length. +example (x : List Bool) (τ : ℕ) (hτ : Nat.card (Action 0 Bool Bool) ≤ τ) : + 0 < guess.choiceTable.acceptCount x τ := + (guess_decides.mem_iff_acceptCount_choiceTable_pos (a := x) (by simpa using hτ)).mp trivial + +/-- A machine permitting no action: its initial configuration is stuck. -/ +private def stuck : MultiTapeNTM 0 Bool Bool where + q₀ := false + Tr _ _ _ _ := False + +private theorem stuck_decides : + stuck.DecidesInTime (Function.Embedding.refl (List Bool)) ∅ fun _ => 1 := by + intro a + have hrun : stuck.RunsInTime a 1 := + MultiTapeNTM.runsInTime_one_of_forall_step_initCfg fun _ hc => by + simp [MultiTapeNTM.Step, MultiTapeNTM.initCfg, Cfg.init, stuck] at hc + refine ⟨hrun, iff_of_false id fun hacc => ?_⟩ + obtain ⟨p, hp, -⟩ := (MultiTapeNTM.accepts_iff_exists_time_eq hrun).mp hacc + have h0 := p.toRunPath.step ⟨0, by + unfold MultiTapeNTM.ComputationPath.time MultiTapeNTM.RunPath.time at hp; omega⟩ + change stuck.Step (p.toRunPath 0) _ at h0 + rw [show p.toRunPath 0 = stuck.initCfg a from p.head_eq] at h0 + simp [MultiTapeNTM.Step, MultiTapeNTM.initCfg, Cfg.init, stuck] at h0 + +-- The choice table rejects at the stuck configuration: no choice string accepts. +example (x : List Bool) (τ : ℕ) (hτ : Nat.card (Action 0 Bool Bool) ≤ τ) : + stuck.choiceTable.acceptCount x τ = 0 := + Nat.eq_zero_of_not_pos fun h => + (stuck_decides.mem_iff_acceptCount_choiceTable_pos (a := x) (by simpa using hτ)).mpr h + +/-! ### Class-level normal forms -/ + +example : {b : Bool | b = true} ∈ Complexity.BPTIME MultiTapeTM.encBool fun _ => 1 := + ⟨1, 0, 0, Unit, inferInstance, echo, by simpa using echo_decides⟩ + +example (h : {b : Bool | b = true} ∈ Complexity.BPTIME MultiTapeTM.encBool fun _ => 1) : + ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapePTM k Bool State) + (c₁ c₂ : ℕ), ∀ a τ, c₁ * 1 + c₂ ≤ τ → + (a ∈ {b : Bool | b = true} ↔ 2 ^ τ < 2 * machine.acceptCount (MultiTapeTM.encBool a) τ) := + Complexity.exists_acceptCount_of_mem_BPTIME h + +end ComplexityTests.HPVChoiceCount From 686b2301fd9328db5085827bbe5967e8764001c3 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:05:44 -0400 Subject: [PATCH 3/9] feat(machines): HPV time intervals, tape blocks and schedules of coin runs (#1833 H2) Run-level facts of the HPV block decomposition for choice-string runs: every head (input head included) moves at most one cell per bit, so within b bits it stays in the three blocks around its starting block; movement schedules in {-1,0,1}, their count 3^((k+1)q), and recovery of block indices from a schedule; locality: configurations agreeing on the three-block windows evolve identically there and emit the same output; and cells outside the windows of a range of intervals are untouched. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + .../Machines/Turing/MultiTape/Locality.lean | 184 ++++++++++ .../MultiTape/Probabilistic/Blocks.lean | 330 ++++++++++++++++++ ComplexityTests/HPVBlocks.lean | 113 ++++++ references.bib | 11 + 5 files changed, 640 insertions(+) create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Locality.lean create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Blocks.lean create mode 100644 ComplexityTests/HPVBlocks.lean diff --git a/Complexity.lean b/Complexity.lean index bd5e471f87..823e67fda0 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1749,6 +1749,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Internal.Resour public import Complexity.Computability.Machines.Turing.MultiTape.Internal.StepMachineCompiler public import Complexity.Computability.Machines.Turing.MultiTape.Internal.UnaryMachines public import Complexity.Computability.Machines.Turing.MultiTape.Internal.WordPredicates +public import Complexity.Computability.Machines.Turing.MultiTape.Locality public import Complexity.Computability.Machines.Turing.MultiTape.Machine public import Complexity.Computability.Machines.Turing.MultiTape.Machine.ChoiceTable public import Complexity.Computability.Machines.Turing.MultiTape.Machine.Clock @@ -1796,6 +1797,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.WhileC public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.WhileInput public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Blocks public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Clock public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Closed public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.CoinTape diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Locality.lean b/Complexity/Computability/Machines/Turing/MultiTape/Locality.lean new file mode 100644 index 0000000000..3cb609e61e --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Locality.lean @@ -0,0 +1,184 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic +public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas + +/-! +# Locality of a step + +A step of a multi-tape machine reads the cells under its heads, writes at most the cells under +its work heads, and moves every head by at most one cell. This file records these facts in the +form used to cut a computation into local pieces. + +The heads are indexed by `Option (Fin k)`: `none` is the read-only input head and `some i` the +head of work tape `i`. `Turing.Cfg.headPos` places them in coordinates where every head starts at +zero; the input head's stored position `inputPos` is shifted by one, so its coordinate ranges over +`[-1, n]` on an input of length `n`. The write-only output tape is never read and has no head +here. + +Two configurations *agree on* a family `W` of work-tape cells (`Turing.Cfg.AgreeOn`) when they have +the same control state and head positions and the same work-tape contents on `W`. If the work +heads lie in `W`, a step reads the same symbols in both, takes the same action, and preserves +agreement on `W`; both append the same symbol, if any, to their outputs +(`Turing.MultiTapeTM.agreeOn_step`). Contents outside `W` and earlier outputs may differ. + +## Main definitions + +* `Turing.Cfg.headPos`: head positions, starting at zero. +* `Turing.Cfg.AgreeOn`: same control and heads, and same work-tape contents on given cells. + +## Main results + +* `Turing.MultiTapeNTM.Step.abs_headPos_sub_le`: a step moves every head by at most one cell. +* `Turing.MultiTapeTM.agreeOn_step`: agreement on cells containing the work heads is preserved + by a step, which emits the same output in both configurations. +-/ + +public section + +namespace Turing + +variable {k : ℕ} {Symbol State : Type*} {input : List Symbol} + +/-- The position of a head, in coordinates where every head starts at zero: the input head +(`none`) at its stored position shifted by one, and the head of work tape `i` (`some i`). -/ +@[expose] def Cfg.headPos (cfg : Cfg k Symbol State input) : Option (Fin k) → ℤ + | none => (cfg.inputPos.val : ℤ) - 1 + | some i => cfg.workTapePos i + +@[simp] theorem Cfg.headPos_none (cfg : Cfg k Symbol State input) : + cfg.headPos none = (cfg.inputPos.val : ℤ) - 1 := rfl + +@[simp] theorem Cfg.headPos_some (cfg : Cfg k Symbol State input) (i : Fin k) : + cfg.headPos (some i) = cfg.workTapePos i := rfl + +/-- Every head starts at zero. -/ +theorem Cfg.headPos_init (q₀ : State) (head : Option (Fin k)) : + (Cfg.init q₀ input : Cfg k Symbol State input).headPos head = 0 := by + cases head with + | none => simp [Cfg.headPos] + | some i => rfl + +/-- The input head is at a coordinate in `[-1, n]` on an input of length `n`. -/ +theorem Cfg.headPos_none_mem_Icc (cfg : Cfg k Symbol State input) : + cfg.headPos none ∈ Set.Icc (-1) (input.length : ℤ) := by + have := cfg.inputPos.isLt + simp only [headPos_none, Set.mem_Icc] + omega + +/-- An action moves every head by at most one cell. -/ +theorem Action.abs_headPos_apply_sub_le (action : Action k Symbol State) + (cfg : Cfg k Symbol State input) (head : Option (Fin k)) : + |(action.apply cfg).headPos head - cfg.headPos head| ≤ 1 := by + cases head with + | none => + have hmove := val_moveInputPos_eq cfg.inputPos action.inputTape + have hlt := cfg.inputPos.isLt + have hcast : (action.inputTape.cast : ℤ) = -1 ∨ (action.inputTape.cast : ℤ) = 0 ∨ + (action.inputTape.cast : ℤ) = 1 := by + rcases action.inputTape with _ | _ | _ <;> simp [SignType.cast] + simp only [Cfg.headPos_none, Action.apply_inputPos, abs_le] + omega + | some i => exact workTapePos_apply_le action cfg i + +/-- **A step moves every head by at most one cell.** -/ +theorem MultiTapeNTM.Step.abs_headPos_sub_le {ntm : MultiTapeNTM k Symbol State} + {c c' : Cfg k Symbol State input} (h : ntm.Step c c') (head : Option (Fin k)) : + |c'.headPos head - c.headPos head| ≤ 1 := by + unfold MultiTapeNTM.Step at h + split at h + · simp [h] + · obtain ⟨action, -, rfl⟩ := h + exact action.abs_headPos_apply_sub_le c head + +/-- Two configurations agree on the work-tape cells `W`: they have the same control state, the +same input and work head positions, and the same work-tape contents on `W`. Their outputs and +their contents outside `W` are unconstrained. -/ +structure Cfg.AgreeOn (W : Fin k → Set ℤ) (c c' : Cfg k Symbol State input) : Prop where + /-- The same control state. -/ + state_eq : c.state = c'.state + /-- The same input head position. -/ + inputPos_eq : c.inputPos = c'.inputPos + /-- The same work head positions. -/ + workTapePos_eq : c.workTapePos = c'.workTapePos + /-- The same work-tape contents on `W`. -/ + workTapes_eq : ∀ i, ∀ z ∈ W i, c.workTapes i z = c'.workTapes i z + +/-- A configuration agrees with itself on every family of cells. -/ +theorem Cfg.AgreeOn.refl (W : Fin k → Set ℤ) (c : Cfg k Symbol State input) : c.AgreeOn W c := + ⟨rfl, rfl, rfl, fun _ _ _ => rfl⟩ + +theorem Cfg.AgreeOn.symm {W : Fin k → Set ℤ} {c c' : Cfg k Symbol State input} + (h : c.AgreeOn W c') : c'.AgreeOn W c := + ⟨h.state_eq.symm, h.inputPos_eq.symm, h.workTapePos_eq.symm, + fun i z hz => (h.workTapes_eq i z hz).symm⟩ + +theorem Cfg.AgreeOn.trans {W : Fin k → Set ℤ} {c c' c'' : Cfg k Symbol State input} + (h : c.AgreeOn W c') (h' : c'.AgreeOn W c'') : c.AgreeOn W c'' := + ⟨h.state_eq.trans h'.state_eq, h.inputPos_eq.trans h'.inputPos_eq, + h.workTapePos_eq.trans h'.workTapePos_eq, + fun i z hz => (h.workTapes_eq i z hz).trans (h'.workTapes_eq i z hz)⟩ + +/-- Agreement on more cells is agreement on fewer. -/ +theorem Cfg.AgreeOn.mono {W W' : Fin k → Set ℤ} {c c' : Cfg k Symbol State input} + (h : c.AgreeOn W c') (hW : ∀ i, W' i ⊆ W i) : c.AgreeOn W' c' := + ⟨h.state_eq, h.inputPos_eq, h.workTapePos_eq, fun i z hz => h.workTapes_eq i z (hW i hz)⟩ + +/-- Agreeing configurations are at the same head positions. -/ +theorem Cfg.AgreeOn.headPos_eq {W : Fin k → Set ℤ} {c c' : Cfg k Symbol State input} + (h : c.AgreeOn W c') : c.headPos = c'.headPos := by + funext head + cases head with + | none => simp [h.inputPos_eq] + | some i => simp [h.workTapePos_eq] + +/-- Agreement on cells containing the work heads gives the same read symbols. -/ +theorem Cfg.AgreeOn.workTapeSymbols_eq {W : Fin k → Set ℤ} {c c' : Cfg k Symbol State input} + (h : c.AgreeOn W c') (hpos : ∀ i, c.workTapePos i ∈ W i) : + c.workTapeSymbols = c'.workTapeSymbols := by + funext i + simp only [Cfg.workTapeSymbols, ← h.workTapePos_eq] + exact h.workTapes_eq i _ (hpos i) + +/-- One action applied to agreeing configurations keeps them agreeing on `W`: it writes the same +symbols under the same heads. -/ +theorem Cfg.AgreeOn.apply {W : Fin k → Set ℤ} {c c' : Cfg k Symbol State input} + (h : c.AgreeOn W c') (action : Action k Symbol State) : + (action.apply c).AgreeOn W (action.apply c') := by + refine ⟨rfl, by simp [h.inputPos_eq], by funext i; simp [h.workTapePos_eq], fun i z hz => ?_⟩ + simp only [Action.apply_workTapes, ← h.workTapePos_eq] + cases (action.workTapes i).1 with + | none => exact h.workTapes_eq i z hz + | some s => + by_cases hz' : z = c.workTapePos i + · simp [hz'] + · simp only [Function.update_of_ne hz'] + exact h.workTapes_eq i z hz + +/-- **Locality of a step.** If two configurations agree on cells `W` containing their work +heads, one step keeps them agreeing on `W`, and both append the same word to their outputs. -/ +theorem MultiTapeTM.agreeOn_step (tm : MultiTapeTM k Symbol State) {W : Fin k → Set ℤ} + {c c' : Cfg k Symbol State input} (h : c.AgreeOn W c') (hpos : ∀ i, c.workTapePos i ∈ W i) : + (tm.step c).AgreeOn W (tm.step c') ∧ + ∃ e, (tm.step c).output = c.output ++ e ∧ (tm.step c').output = c'.output ++ e := by + cases hs : c.state with + | none => + have hs' : c'.state = none := h.state_eq ▸ hs + rw [MultiTapeTM.step_of_halt hs, MultiTapeTM.step_of_halt hs'] + exact ⟨h, [], by simp, by simp⟩ + | some q => + have hs' : c'.state = some q := h.state_eq ▸ hs + have hread : c.inputSymbol = c'.inputSymbol := by + simp only [Cfg.inputSymbol, h.inputPos_eq] + rw [MultiTapeTM.step_of_state hs, MultiTapeTM.step_of_state hs', hread, + h.workTapeSymbols_eq hpos] + exact ⟨h.apply _, _, Action.apply_output _ _, Action.apply_output _ _⟩ + +end Turing diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Blocks.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Blocks.lean new file mode 100644 index 0000000000..5a41b6e994 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Blocks.lean @@ -0,0 +1,330 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Machines.Turing.MultiTape.Locality +public import Complexity.Computability.Machines.Turing.MultiTape.Machine.Nondeterministic +public import Mathlib.Data.Fintype.Option +public import Mathlib.Data.Fintype.Pi +public import Mathlib.Basic.Sign.Defs +import Mathlib.Algebra.Order.BigOperators.Group.Finset +import Mathlib.Basic.Sign.Basic +import Mathlib.Tactic.Linarith + +/-! +# Time intervals and tape blocks of a choice-string run + +The blocking idea of Hopcroft, Paul and Valiant [HopcroftPaulValiant1977], in the form of +Lemma 2.1 of the note *Deterministic simulations of nondeterministic and randomized time* +(30 October 2026) formalized in issue #1833. It uses three neighbouring tape blocks instead of +making the machine block-respecting (compare [Williams2025], Lemma 2.1 and §3.2). The +statements here are the run-level facts of that lemma, for the replay +`Turing.MultiTapePTM.stepCoins` of a fair-coin table on a list of choice bits. + +Time is cut into intervals of `b` steps: interval `i` starts at +`Turing.MultiTapePTM.intervalStart b coins c i`, after the first `i * b` bits. Each tape is cut +into blocks `B_j = [b j, b (j + 1))`, so a head at coordinate `p` (`Turing.Cfg.headPos`) is in +block `p / b` at offset `p % b`. The blocked heads are the input head and the `k` work heads; +the write-only output tape is never read and is not blocked. + +* **Three blocks.** Within `b` steps a head moves at most `b` cells, so it stays in the blocks + `B_{j-1}, B_j, B_{j+1}` around its starting block `B_j` + (`Turing.MultiTapePTM.headPos_stepCoins_mem_Ico`), and its block index changes by at most one + (`Turing.MultiTapePTM.abs_blockIndex_stepCoins_sub_le`). +* **Schedules.** The *movement schedule* of a run (`Turing.MultiTapePTM.schedule`) records this + change in `{-1, 0, 1}` for every interval and head. There are `3 ^ ((k + 1) * q)` schedules of + `q` intervals (`Turing.MultiTapePTM.card_schedule`), every run has exactly one, and it + determines all block indices from the starting ones + (`Turing.MultiTapePTM.blockIndex_intervalStart`). +* **Locality.** An interval only reads and writes the window `Turing.Cfg.blockWindow` of three + blocks around each work head. Two configurations agreeing on their control, heads and window + contents still agree after `b` steps on the same bits, and emit the same output + (`Turing.MultiTapePTM.agreeOn_blockWindow_stepCoins`). So the interval is determined by its + bits, its entering state and head positions and the contents of its windows. Cells outside the + window are unchanged (`Turing.MultiTapePTM.workTapes_stepCoins_eq_of_notMem_blockWindow`), and + a cell lying outside the windows of a range of intervals is untouched throughout that range + (`Turing.MultiTapePTM.workTapes_intervalStart_eq_of_notMem_blockWindow`). + +All statements hold for every block length `b > 0` and number `q` of intervals; the choice +`q = ⌈t / b⌉` and the bound `2 ≤ b ≤ t` of the note only matter for counting. + +## Main definitions + +* `Turing.Cfg.blockWindow`: the three blocks around each work head. +* `Turing.MultiTapePTM.intervalStart`: the configuration at the start of a time interval. +* `Turing.MultiTapePTM.Schedule`, `Turing.MultiTapePTM.schedule`: movement schedules. + +## Main results + +* `Turing.MultiTapePTM.abs_headPos_stepCoins_sub_le`: a head moves at most one cell per bit. +* `Turing.MultiTapePTM.headPos_stepCoins_mem_Ico`: within `b` steps, three blocks. +* `Turing.MultiTapePTM.abs_blockIndex_stepCoins_sub_le`: block indices change by at most one. +* `Turing.MultiTapePTM.card_schedule`: there are `3 ^ ((k + 1) * q)` schedules. +* `Turing.MultiTapePTM.coe_schedule`: a schedule entry is the change of block index. +* `Turing.MultiTapePTM.blockIndex_intervalStart`: schedules determine block indices. +* `Turing.MultiTapePTM.agreeOn_stepCoins`: locality of a run on cells containing its heads. +* `Turing.MultiTapePTM.agreeOn_blockWindow_stepCoins`: an interval is determined by its window. +* `Turing.MultiTapePTM.workTapes_stepCoins_eq_of_notMem_blockWindow`: cells outside the window + are unchanged. +* `Turing.MultiTapePTM.workTapes_intervalStart_eq_of_notMem_blockWindow`: blocks outside the + windows of a range of intervals are untouched. + +## References + +* [J. Hopcroft, W. Paul, L. Valiant, *On Time Versus Space*][HopcroftPaulValiant1977] +* [R. Williams, *Simulating Time With Square-Root Space*][Williams2025] +-/ + +public section + +namespace Turing + +variable {k : ℕ} {Symbol State : Type} {input : List Symbol} + +/-! ### Block arithmetic -/ + +/-- Within distance `b` of a point of block `p / b`, the three blocks around it. -/ +private theorem mem_Ico_of_abs_sub_le {b p p' : ℤ} (hb : 0 < b) (h : |p' - p| ≤ b) : + b * (p / b - 1) ≤ p' ∧ p' < b * (p / b + 2) := by + have hdiv := Int.mul_ediv_add_emod p b + have hlo := Int.emod_nonneg p hb.ne' + have hhi := Int.emod_lt_of_pos p hb + have := abs_le.mp h + constructor <;> nlinarith + +/-- Within distance `b`, block indices differ by at most one. -/ +private theorem abs_ediv_sub_ediv_le_one {b p p' : ℤ} (hb : 0 < b) (h : |p' - p| ≤ b) : + |p' / b - p / b| ≤ 1 := by + obtain ⟨hlo, hhi⟩ := mem_Ico_of_abs_sub_le hb h + have hdiv := Int.mul_ediv_add_emod p' b + have hlo' := Int.emod_nonneg p' hb.ne' + have hhi' := Int.emod_lt_of_pos p' hb + have h₁ : p' / b < p / b + 2 := lt_of_mul_lt_mul_left (by linarith) hb.le + have h₂ : p / b - 1 < p' / b + 1 := lt_of_mul_lt_mul_left (by linarith) hb.le + rw [abs_le] + constructor <;> omega + +/-- The three blocks of length `b` around the block of each work head: the cells a work head can +visit within `b` steps. -/ +@[expose] def Cfg.blockWindow (b : ℕ) (c : Cfg k Symbol State input) (i : Fin k) : Set ℤ := + Set.Ico (b * (c.workTapePos i / b - 1)) (b * (c.workTapePos i / b + 2)) + +namespace MultiTapePTM + +variable (machine : MultiTapePTM k Symbol State) + +/-! ### Head movement -/ + +/-- A replayed bit is a step of the table with that coin fixed. -/ +private theorem step_withCoin (bit : Bool) (c : Cfg k Symbol State input) : + (machine.withCoin bit).toTM.Step c ((machine.withCoin bit).toTM.step c) := + MultiTapeTM.step_iff.mpr rfl + +/-- A head moves at most one cell per replayed bit. -/ +theorem abs_headPos_stepCoins_sub_le (coins : List Bool) (c : Cfg k Symbol State input) + (head : Option (Fin k)) : + |(machine.stepCoins coins c).headPos head - c.headPos head| ≤ coins.length := by + induction coins generalizing c with + | nil => simp + | cons bit coins ih => + rw [stepCoins_cons] + have h₁ := abs_le.mp (ih ((machine.withCoin bit).toTM.step c)) + have h₂ := abs_le.mp ((machine.step_withCoin bit c).abs_headPos_sub_le head) + rw [abs_le, List.length_cons] + push_cast + constructor <;> linarith + +/-- **Three blocks.** Within `b` replayed bits, a head stays in the three blocks of length `b` +around its starting block. -/ +theorem headPos_stepCoins_mem_Ico {b : ℕ} (hb : 0 < b) {coins : List Bool} + (hlen : coins.length ≤ b) (c : Cfg k Symbol State input) (head : Option (Fin k)) : + (machine.stepCoins coins c).headPos head ∈ + Set.Ico ((b : ℤ) * (c.headPos head / b - 1)) (b * (c.headPos head / b + 2)) := + mem_Ico_of_abs_sub_le (by exact_mod_cast hb) + ((machine.abs_headPos_stepCoins_sub_le coins c head).trans (by exact_mod_cast hlen)) + +/-- Within `b` replayed bits, the block index of a head changes by at most one. -/ +theorem abs_blockIndex_stepCoins_sub_le {b : ℕ} (hb : 0 < b) {coins : List Bool} + (hlen : coins.length ≤ b) (c : Cfg k Symbol State input) (head : Option (Fin k)) : + |(machine.stepCoins coins c).headPos head / b - c.headPos head / b| ≤ 1 := + abs_ediv_sub_ediv_le_one (by exact_mod_cast hb) + ((machine.abs_headPos_stepCoins_sub_le coins c head).trans (by exact_mod_cast hlen)) + +/-- A work-tape cell farther from the head than the number of replayed bits is unchanged. -/ +theorem workTapes_stepCoins_eq_of_lt_abs (coins : List Bool) (c : Cfg k Symbol State input) + {i : Fin k} {z : ℤ} (hz : (coins.length : ℤ) < |z - c.workTapePos i|) : + (machine.stepCoins coins c).workTapes i z = c.workTapes i z := by + induction coins generalizing c with + | nil => rfl + | cons bit coins ih => + have hstep := machine.step_withCoin bit c + have hmove := abs_le.mp (hstep.abs_headPos_sub_le (some i)) + simp only [Cfg.headPos_some] at hmove + simp only [List.length_cons, Nat.cast_add, Nat.cast_one] at hz + rw [stepCoins_cons, ih _ ?_] + · refine hstep.workTapes_eq_of_ne fun hzpos => ?_ + rw [hzpos, sub_self, abs_zero] at hz + omega + · rw [lt_abs] at hz ⊢ + omega + +/-- **Locality of a run.** If two configurations agree on cells `W`, and the work heads of the +first stay in `W` before each replayed bit, then after replaying the same bits they still agree +on `W` and have appended the same word to their outputs. -/ +theorem agreeOn_stepCoins {W : Fin k → Set ℤ} {c c' : Cfg k Symbol State input} + (h : c.AgreeOn W c') (coins : List Bool) + (hpos : ∀ j < coins.length, ∀ i, (machine.stepCoins (coins.take j) c).workTapePos i ∈ W i) : + (machine.stepCoins coins c).AgreeOn W (machine.stepCoins coins c') ∧ + ∃ e, (machine.stepCoins coins c).output = c.output ++ e ∧ + (machine.stepCoins coins c').output = c'.output ++ e := by + induction coins generalizing c c' with + | nil => exact ⟨h, [], by simp, by simp⟩ + | cons bit coins ih => + obtain ⟨hstep, e, he, he'⟩ := + MultiTapeTM.agreeOn_step (machine.withCoin bit).toTM h (hpos 0 (by simp)) + obtain ⟨hrest, e', hrest₁, hrest₂⟩ := ih hstep fun j hj => by + simpa only [List.take_succ_cons, stepCoins_cons] using + hpos (j + 1) (by simpa only [List.length_cons, Nat.add_lt_add_iff_right] using hj) + refine ⟨hrest, e ++ e', ?_, ?_⟩ + · rw [stepCoins_cons, hrest₁, he, List.append_assoc] + · rw [stepCoins_cons, hrest₂, he', List.append_assoc] + +/-- **An interval is determined by its window.** Two configurations agreeing on the three blocks +around each work head of the first still agree there after at most `b` replayed bits, and have +appended the same word to their outputs. -/ +theorem agreeOn_blockWindow_stepCoins {b : ℕ} (hb : 0 < b) {coins : List Bool} + (hlen : coins.length ≤ b) {c c' : Cfg k Symbol State input} + (h : c.AgreeOn (c.blockWindow b) c') : + (machine.stepCoins coins c).AgreeOn (c.blockWindow b) (machine.stepCoins coins c') ∧ + ∃ e, (machine.stepCoins coins c).output = c.output ++ e ∧ + (machine.stepCoins coins c').output = c'.output ++ e := + machine.agreeOn_stepCoins h coins fun j _ i => + machine.headPos_stepCoins_mem_Ico hb (coins := coins.take j) + ((List.length_take_le' j coins).trans hlen) c (some i) + +/-- Within `b` replayed bits, a work-tape cell outside the three blocks around its head is +unchanged. -/ +theorem workTapes_stepCoins_eq_of_notMem_blockWindow {b : ℕ} (hb : 0 < b) {coins : List Bool} + (hlen : coins.length ≤ b) (c : Cfg k Symbol State input) {i : Fin k} {z : ℤ} + (hz : z ∉ c.blockWindow b i) : + (machine.stepCoins coins c).workTapes i z = c.workTapes i z := by + refine machine.workTapes_stepCoins_eq_of_lt_abs coins c ?_ + have hb' : (0 : ℤ) < b := by exact_mod_cast hb + have hdiv := Int.mul_ediv_add_emod (c.workTapePos i) b + have hlo := Int.emod_nonneg (c.workTapePos i) hb'.ne' + have hhi := Int.emod_lt_of_pos (c.workTapePos i) hb' + have hlen' : (coins.length : ℤ) ≤ b := by exact_mod_cast hlen + simp only [Cfg.blockWindow, Set.mem_Ico, not_and_or, not_le, not_lt] at hz + rw [lt_abs] + rcases hz with hz | hz + · right + nlinarith + · left + nlinarith + +/-! ### Time intervals and schedules -/ + +/-- The configuration at the start of time interval `i`, of `b` steps each: replay the first +`i * b` bits. -/ +@[expose] noncomputable def intervalStart (b : ℕ) (coins : List Bool) (c : Cfg k Symbol State input) + (i : ℕ) : Cfg k Symbol State input := + machine.stepCoins (coins.take (i * b)) c + +@[simp] theorem intervalStart_zero (b : ℕ) (coins : List Bool) (c : Cfg k Symbol State input) : + machine.intervalStart b coins c 0 = c := by + simp [intervalStart] + +/-- Interval `i + 1` starts after replaying the `b` bits of interval `i`. -/ +theorem intervalStart_succ (b : ℕ) (coins : List Bool) (c : Cfg k Symbol State input) (i : ℕ) : + machine.intervalStart b coins c (i + 1) = + machine.stepCoins ((coins.drop (i * b)).take b) (machine.intervalStart b coins c i) := by + rw [intervalStart, intervalStart, ← stepCoins_append, Nat.succ_mul, List.take_add] + +/-- The bits of an interval number at most `b`. -/ +theorem length_intervalCoins_le (b : ℕ) (coins : List Bool) (i : ℕ) : + ((coins.drop (i * b)).take b).length ≤ b := + List.length_take_le _ _ + +/-- A movement schedule of `q` intervals: the change, in `{-1, 0, 1}`, of the block index of +the input head (`none`) and of each work head (`some i`) across each interval. -/ +abbrev Schedule (k q : ℕ) := Fin q → Option (Fin k) → SignType + +/-- There are `3 ^ ((k + 1) * q)` movement schedules of `q` intervals. -/ +theorem card_schedule (k q : ℕ) : Fintype.card (Schedule k q) = 3 ^ ((k + 1) * q) := by + simp only [Fintype.card_fun, Fintype.card_option, Fintype.card_fin] + rw [show Fintype.card SignType = 3 from rfl, ← pow_mul, mul_comm] + +/-- The movement schedule of the run replaying `coins` from `c`, in `q` intervals of `b` bits: +the change of the block index of every head across every interval. -/ +noncomputable def schedule (b q : ℕ) (coins : List Bool) (c : Cfg k Symbol State input) : + Schedule k q := fun i head => + SignType.sign ((machine.intervalStart b coins c (i + 1)).headPos head / b - + (machine.intervalStart b coins c i).headPos head / b) + +/-- An integer of absolute value at most one is its own sign. -/ +private theorem coe_sign_eq_self {d : ℤ} (hd : |d| ≤ 1) : + ((SignType.sign d : SignType) : ℤ) = d := by + have : d = -1 ∨ d = 0 ∨ d = 1 := by rw [abs_le] at hd; omega + rcases this with rfl | rfl | rfl <;> rfl + +/-- A schedule entry is the change of block index across the interval. -/ +theorem coe_schedule {b : ℕ} (hb : 0 < b) (q : ℕ) (coins : List Bool) + (c : Cfg k Symbol State input) (i : Fin q) (head : Option (Fin k)) : + (machine.schedule b q coins c i head : ℤ) = + (machine.intervalStart b coins c (i + 1)).headPos head / b - + (machine.intervalStart b coins c i).headPos head / b := by + refine coe_sign_eq_self ?_ + rw [intervalStart_succ] + exact machine.abs_blockIndex_stepCoins_sub_le hb (length_intervalCoins_le _ _ _) _ head + +/-- **Schedules determine block indices.** At the start of interval `i ≤ q`, the block index of a +head is its starting block index plus the schedule entries of the earlier intervals. -/ +theorem blockIndex_intervalStart {b : ℕ} (hb : 0 < b) {q : ℕ} (coins : List Bool) + (c : Cfg k Symbol State input) (head : Option (Fin k)) {i : ℕ} (hi : i ≤ q) : + (machine.intervalStart b coins c i).headPos head / b = + c.headPos head / b + + ∑ j : Fin i, (machine.schedule b q coins c (Fin.castLE hi j) head : ℤ) := by + induction i with + | zero => simp + | succ i ih => + have hsum : ∑ j : Fin i, (machine.schedule b q coins c (Fin.castLE hi j.castSucc) head : ℤ) = + ∑ j : Fin i, (machine.schedule b q coins c (Fin.castLE (by omega) j) head : ℤ) := rfl + rw [Fin.sum_univ_castSucc, hsum, ← add_assoc, ← ih (by omega)] + have := machine.coe_schedule hb q coins c ⟨i, by omega⟩ head + simp only at this + change _ = _ + (machine.schedule b q coins c ⟨i, by omega⟩ head : ℤ) + rw [this] + ring + +/-- Across interval `i`, a work-tape cell outside the window of interval `i` is unchanged. -/ +theorem workTapes_intervalStart_succ_eq {b : ℕ} (hb : 0 < b) (coins : List Bool) + (c : Cfg k Symbol State input) (i : ℕ) {h : Fin k} {z : ℤ} + (hz : z ∉ (machine.intervalStart b coins c i).blockWindow b h) : + (machine.intervalStart b coins c (i + 1)).workTapes h z = + (machine.intervalStart b coins c i).workTapes h z := by + rw [intervalStart_succ] + exact machine.workTapes_stepCoins_eq_of_notMem_blockWindow hb + (length_intervalCoins_le _ _ _) _ hz + +/-- **Untouched blocks.** A work-tape cell outside the windows of intervals `i₁, …, i₂ - 1` has +the same contents at the start of interval `i₂` as at the start of interval `i₁`. -/ +theorem workTapes_intervalStart_eq_of_notMem_blockWindow {b : ℕ} (hb : 0 < b) + (coins : List Bool) (c : Cfg k Symbol State input) {h : Fin k} {z : ℤ} {i₁ i₂ : ℕ} + (hle : i₁ ≤ i₂) + (hz : ∀ i, i₁ ≤ i → i < i₂ → z ∉ (machine.intervalStart b coins c i).blockWindow b h) : + (machine.intervalStart b coins c i₂).workTapes h z = + (machine.intervalStart b coins c i₁).workTapes h z := by + induction i₂, hle using Nat.le_induction with + | base => rfl + | succ i₂ hle ih => + rw [machine.workTapes_intervalStart_succ_eq hb coins c i₂ (hz i₂ hle (by omega)), + ih fun i hi hi₂ => hz i hi (by omega)] + +end MultiTapePTM + +end Turing diff --git a/ComplexityTests/HPVBlocks.lean b/ComplexityTests/HPVBlocks.lean new file mode 100644 index 0000000000..8b8e0aa4a7 --- /dev/null +++ b/ComplexityTests/HPVBlocks.lean @@ -0,0 +1,113 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Blocks + +/-! Time intervals, tape blocks and schedules of a concrete choice-string run. -/ + +namespace ComplexityTests.HPVBlocks + +open Turing MultiTapeMachine + +/-- On one work tape, write the coin and move right on `true`, left on `false`. The input head +moves right on `true` too. -/ +private def zigzag : MultiTapePTM 1 Bool Unit where + initial := () + tr _ _ _ _ bit := .step + { inputTape := if bit then 1 else 0, + workTapes := fun _ => (some (some bit), if bit then 1 else -1), + output := none, state := some () } + Empty.elim Empty.elim + +/-- Replays on upstream configurations, evaluated through the computable interpreter. -/ +private theorem stepCoins_eq (coins : List Bool) (cfg : Cfg 1 Bool Unit [true, false]) : + zigzag.stepCoins coins cfg = + (zigzag.runClosedConfigFromCoins coins { tapes := cfg }).tapes := + (MultiTapePTM.tapes_runClosedConfigFromCoins zigzag coins { tapes := cfg }).symm + +private def start : Cfg 1 Bool Unit [true, false] := Cfg.init () [true, false] + +private def coins : List Bool := [true, true, true, false, true, true] + +-- The work head visits 0, 1, 2, 3, 2, 3, 4; the input head is clamped at the right boundary. +example : ((zigzag.stepCoins coins start).headPos (some 0), + (zigzag.stepCoins coins start).headPos none) = (4, 2) := by + rw [stepCoins_eq] + rfl + +-- With blocks of length 2, the work head starts intervals 0, 1, 2, 3 in blocks 0, 1, 1, 2. +example : (List.range 4).map + (fun i => (zigzag.intervalStart 2 coins start i).headPos (some 0) / 2) = [0, 1, 1, 2] := by + simp only [List.range_succ, List.range_zero, List.nil_append, MultiTapePTM.intervalStart, + stepCoins_eq] + rfl + +-- So the schedule of the work head is `(1, 0, 1)`; the input head moves right then stays. +example : (List.ofFn fun i : Fin 3 => (zigzag.schedule 2 3 coins start i (some 0) : ℤ)) = + [1, 0, 1] ∧ + (List.ofFn fun i : Fin 3 => (zigzag.schedule 2 3 coins start i none : ℤ)) = [1, 0, 0] := by + simp only [List.ofFn_succ, List.ofFn_zero, MultiTapePTM.coe_schedule zigzag two_pos, + MultiTapePTM.intervalStart, stepCoins_eq] + constructor <;> rfl + +-- The block index at the end is recovered from the schedule. +example : (zigzag.intervalStart 2 coins start 3).headPos (some 0) / (2 : ℕ) = 2 := by + rw [zigzag.blockIndex_intervalStart two_pos coins start (some 0) le_rfl, Fin.sum_univ_three] + simp only [MultiTapePTM.coe_schedule zigzag two_pos, MultiTapePTM.intervalStart, stepCoins_eq] + rfl + +-- There are `3 ^ 6` schedules of three intervals for the input head and one work head. +example : Fintype.card (MultiTapePTM.Schedule 1 3) = 729 := by + rw [MultiTapePTM.card_schedule] + norm_num + +/-! ### Three blocks -/ + +/-- After one bit the work head is at offset `1` of block `0`, with blocks of length `2`. -/ +private theorem headPos_one : (zigzag.stepCoins [true] start).headPos (some 0) = 1 := by + rw [stepCoins_eq] + rfl + +-- Within two more bits it stays in blocks `-1, 0, 1`: here it reaches block `1`. +example : (zigzag.stepCoins [true, true] (zigzag.stepCoins [true] start)).headPos (some 0) = 3 ∧ + (3 : ℤ) ∈ Set.Ico (2 * (1 / 2 - 1)) (2 * (1 / 2 + 2)) := by + refine ⟨?_, by decide⟩ + rw [← MultiTapePTM.stepCoins_append, stepCoins_eq] + rfl + +-- The bound needs at most `b` bits: three bits leave the three blocks. +example : (zigzag.stepCoins [true, true, true] (zigzag.stepCoins [true] start)).headPos (some 0) ∉ + Set.Ico (2 * ((zigzag.stepCoins [true] start).headPos (some 0) / 2 - 1)) + (2 * ((zigzag.stepCoins [true] start).headPos (some 0) / 2 + 2)) := by + rw [headPos_one, ← MultiTapePTM.stepCoins_append, stepCoins_eq] + decide + +/-! ### Locality -/ + +/-- The start configuration with a written cell outside its window `[-2, 4)`. -/ +private def marked : Cfg 1 Bool Unit [true, false] := + { start with workTapes := fun _ z => if z = 5 then some false else none } + +private theorem agreeOn_marked : start.AgreeOn (start.blockWindow 2) marked := + ⟨rfl, rfl, rfl, fun _ z hz => by + simp only [Cfg.blockWindow, start, Cfg.init, Set.mem_Ico] at hz + simp [marked, start, show z ≠ 5 by omega]⟩ + +-- A window cell written by the run from `start` is written the same way from `marked`. +example : (zigzag.stepCoins [true, false] marked).workTapes 0 1 = some false := by + have hstart : (zigzag.stepCoins [true, false] start).workTapes 0 1 = some false := by + rw [stepCoins_eq] + rfl + rw [← hstart] + exact ((zigzag.agreeOn_blockWindow_stepCoins two_pos (by simp) agreeOn_marked).1.workTapes_eq + 0 1 (by simp [Cfg.blockWindow, start])).symm + +-- The cell outside the window keeps its mark. +example : (zigzag.stepCoins [true, false] marked).workTapes 0 5 = some false := + zigzag.workTapes_stepCoins_eq_of_notMem_blockWindow two_pos (by simp) marked + (by simp [Cfg.blockWindow, marked, start]) + +end ComplexityTests.HPVBlocks diff --git a/references.bib b/references.bib index e41912a56b..8d4525226f 100644 --- a/references.bib +++ b/references.bib @@ -2288,6 +2288,17 @@ @book{ Hopcroft2006 address = {USA} } +@article{HopcroftPaulValiant1977, + author = {Hopcroft, John and Paul, Wolfgang and Valiant, Leslie}, + title = {On Time Versus Space}, + journal = {Journal of the ACM}, + volume = {24}, + number = {2}, + pages = {332--337}, + year = {1977}, + doi = {10.1145/322003.322015} +} + @techreport{Hoza2022, author = {Hoza, William M.}, title = {Recent Progress on Derandomizing Space-Bounded Computation}, From b7576bcda7f3f2574939699dbf8735d15944e60f Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:11:24 -0400 Subject: [PATCH 4/9] refactor(complexity): share the generic accepted-string count with machines Move `Cslib.Complexity.acceptCount` and its elementary lemmas unchanged from `Classes/SharpP.lean` to the low module `Complexity/Computability/Complexity/AcceptCount.lean`, which SharpP re-exports. Define `Turing.MultiTapePTM.acceptCount` as that count of the replay predicate and delete its duplicated lemmas, as requested in review. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Computability/Complexity/AcceptCount.lean | 119 ++++++++++++++++++ .../Complexity/Classes/SharpP.lean | 84 +------------ .../Complexity/Classes/Time/AcceptCount.lean | 4 +- .../MultiTape/Probabilistic/AcceptCount.lean | 32 ++--- 5 files changed, 134 insertions(+), 106 deletions(-) create mode 100644 Complexity/Computability/Complexity/AcceptCount.lean diff --git a/Complexity.lean b/Complexity.lean index ce92f5d3ef..f6e56784bc 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -984,6 +984,7 @@ public import Complexity.Computability.Communication.TopDown.Adversary public import Complexity.Computability.Communication.TopDown.Majority public import Complexity.Computability.Communication.TopDown.Parity public import Complexity.Computability.Communication.TopDown.Rectangle +public import Complexity.Computability.Complexity.AcceptCount public import Complexity.Computability.Complexity.AffineDisperser public import Complexity.Computability.Complexity.AffineDisperser.BinaryPolynomial public import Complexity.Computability.Complexity.AffineDisperser.Coordinates diff --git a/Complexity/Computability/Complexity/AcceptCount.lean b/Complexity/Computability/Complexity/AcceptCount.lean new file mode 100644 index 0000000000..c14ce50bbb --- /dev/null +++ b/Complexity/Computability/Complexity/AcceptCount.lean @@ -0,0 +1,119 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Data.Fintype.Pi +import Complexity.Foundations.Data.BitString.WordCount + +/-! +# Counting accepted strings + +`Cslib.Complexity.acceptCount V a n` is the number of strings `w` of length `n` with +`V (a, w) = true`, for any Boolean predicate `V : α × List Bool → Bool`. No efficiency of `V` is +assumed. It counts the certificates of a verifier in the counting classes +(`Cslib.Complexity.SharpP`), the random strings accepted by a bounded-error or majority verifier, +and the choice strings accepted by a fair-coin machine (`Turing.MultiTapePTM.acceptCount`). + +## Main definitions + +* `Cslib.Complexity.acceptCount`: the number of accepted strings of a given length. + +## Main results + +* `Cslib.Complexity.acceptCount_le_two_pow`, `Cslib.Complexity.acceptCount_pos_iff`: the range + and support of the count. +* `Cslib.Complexity.acceptCount_add`: counting accepted strings by their prefixes. +* `Cslib.Complexity.acceptCount_zero`, `Cslib.Complexity.acceptCount_add_acceptCount_not`, + `Cslib.Complexity.acceptCount_not`: counts of trivial and negated verifiers. +-/ + +@[expose] public section + +namespace Cslib.Complexity + +variable {α : Type} + +/-- The number of strings `w` of length `n` with `V (a, w) = true`. -/ +def acceptCount (V : α × List Bool → Bool) (a : α) (n : ℕ) : ℕ := + (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = true).card + +section acceptCount + +variable {V : α × List Bool → Bool} {a : α} {n : ℕ} + +/-- At most all `2 ^ n` strings are accepted. -/ +theorem acceptCount_le_two_pow : acceptCount V a n ≤ 2 ^ n := + (Finset.card_filter_le _ _).trans (by simp) + +/-- Some string of length `n` is accepted exactly when the count is positive. -/ +theorem acceptCount_pos_iff : + 0 < acceptCount V a n ↔ ∃ w : List Bool, w.length = n ∧ V (a, w) = true := by + rw [acceptCount, Finset.card_pos, Finset.filter_nonempty_iff] + constructor + · rintro ⟨w, -, hw⟩ + exact ⟨List.ofFn w, List.length_ofFn, hw⟩ + · rintro ⟨w, rfl, hw⟩ + exact ⟨fun i => w[i.val], Finset.mem_univ _, by rwa [List.ofFn_getElem]⟩ + +/-- The strings that `V` accepts together with `a` and those it rejects are all the strings. -/ +theorem acceptCount_add_card_filter_eq_false : + acceptCount V a n + + (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = false).card = 2 ^ n := by + have := Finset.card_filter_add_card_filter_not (s := Finset.univ) + fun w : Fin n → Bool => V (a, List.ofFn w) = true + simpa only [acceptCount, Bool.not_eq_true, Finset.card_univ, Fintype.card_fun, Fintype.card_bool, + Fintype.card_fin] using this + +/-- **Counting strings by their prefixes**: the strings of length `m + n` accepted by `V` are the +strings `u ++ w`, with `u` of length `m` and `w` of length `n` accepted with the prefix `u`. -/ +theorem acceptCount_add (V : α × List Bool → Bool) (a : α) (m n : ℕ) : + acceptCount V a (m + n) = + ∑ u : Fin m → Bool, acceptCount (fun x => V (x.1, List.ofFn u ++ x.2)) a n := by + have h := BitString.card_filter_ofFn_add m n fun u w => V (a, u ++ w) = true + simp only [List.take_append_drop] at h + exact h + +/-- Verifiers that agree on an instance accept the same strings with it. -/ +theorem acceptCount_congr {W : α × List Bool → Bool} (h : ∀ w, V (a, w) = W (a, w)) (n : ℕ) : + acceptCount V a n = acceptCount W a n := by + simp only [acceptCount, h] + +/-- With no bits there is one string, the empty one. -/ +theorem acceptCount_zero (V : α × List Bool → Bool) (a : α) : + acceptCount V a 0 = if V (a, []) = true then 1 else 0 := by + unfold acceptCount + rw [Finset.univ_unique, Finset.filter_singleton] + split_ifs with h₁ h₂ h₂ <;> simp_all + +/-- The verifier accepting everything accepts all `2 ^ n` strings of length `n`. -/ +@[simp] +theorem acceptCount_true (a : α) (n : ℕ) : acceptCount (fun _ => true) a n = 2 ^ n := by + simp [acceptCount] + +/-- The verifier rejecting everything accepts no string. -/ +@[simp] +theorem acceptCount_false (a : α) (n : ℕ) : acceptCount (fun _ => false) a n = 0 := by + simp [acceptCount] + +/-- A verifier and its negation together accept every string once. -/ +theorem acceptCount_add_acceptCount_not (V : α × List Bool → Bool) (a : α) (n : ℕ) : + acceptCount V a n + acceptCount (fun x => !V x) a n = 2 ^ n := by + simpa only [acceptCount, Bool.not_eq_true'] using + acceptCount_add_card_filter_eq_false (V := V) (a := a) (n := n) + +/-- The negation of a verifier accepts the strings that it rejects. -/ +theorem acceptCount_not (V : α × List Bool → Bool) (a : α) (n : ℕ) : + acceptCount (fun x => !V x) a n = 2 ^ n - acceptCount V a n := by + have := acceptCount_add_acceptCount_not V a n + omega + +end acceptCount + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/SharpP.lean b/Complexity/Computability/Complexity/Classes/SharpP.lean index c61dce990f..a8141bc0e6 100644 --- a/Complexity/Computability/Complexity/Classes/SharpP.lean +++ b/Complexity/Computability/Complexity/Classes/SharpP.lean @@ -7,12 +7,12 @@ Authors: Samuel Schlesinger module -- upstream: candidate +public import Complexity.Computability.Complexity.AcceptCount public import Complexity.Computability.Complexity.Classes.NP public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain public import Mathlib.Algebra.BigOperators.Group.Finset.Basic public import Mathlib.Algebra.Order.Group.Int public import Mathlib.Data.Fintype.Pi -import Complexity.Foundations.Data.BitString.WordCount /-! # The counting classes #P and GapP @@ -21,7 +21,8 @@ import Complexity.Foundations.Data.BitString.WordCount [Valiant][Valiant1979], [Arora and Barak, Chapter 17][AroraBarak09]: `f ∈ SharpP enc` when there are a polynomial `p` and a function `V : α × List Bool → Bool`, computable in polynomial time on inputs `encPair enc encBits (a, w) = frame (enc a) ++ w`, such that `f a` is the number of strings -`w` of length `p (enc a).length` with `V (a, w) = true`. The problems in `NP` are exactly the sets +`w` of length `p (enc a).length` with `V (a, w) = true`, the count `Cslib.Complexity.acceptCount` +of `Complexity.Computability.Complexity.AcceptCount`. The problems in `NP` are exactly the sets where functions in `#P` are nonzero (`mem_NP_iff_exists_SharpP`). `GapP` consists of the differences of two functions in `#P`. Fenner, Fortnow and Kurtz define it @@ -36,16 +37,11 @@ signed routing and the corresponding bidirectional `GapP` characterization. ## Main definitions -* `Cslib.Complexity.acceptCount`: the number of strings of a given length that a verifier accepts - together with an instance. * `Cslib.Complexity.SharpP`, `Cslib.Complexity.GapP`. ## Main results * `Cslib.Complexity.mem_NP_iff_exists_SharpP`: `NP` consists of the supports of functions in `#P`. -* `Cslib.Complexity.acceptCount_add`: counting accepted strings by their prefixes. -* `Cslib.Complexity.acceptCount_zero`, `Cslib.Complexity.acceptCount_add_acceptCount_not`, - `Cslib.Complexity.acceptCount_not`: counts of trivial and negated verifiers. * `Cslib.Complexity.SharpP.exists_le_two_pow`: functions in `#P` are at most exponential. * `Cslib.Complexity.GapP.exists_abs_le_two_pow`: every `GapP` function is bounded in absolute value by `2 ^ p(|x|)` for a polynomial `p`. @@ -66,80 +62,6 @@ open Turing.MultiTapeTM variable {α : Type} -/-- The number of strings `w` of length `n` with `V (a, w) = true`. -/ -def acceptCount (V : α × List Bool → Bool) (a : α) (n : ℕ) : ℕ := - (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = true).card - -section acceptCount - -variable {V : α × List Bool → Bool} {a : α} {n : ℕ} - -theorem acceptCount_le_two_pow : acceptCount V a n ≤ 2 ^ n := - (Finset.card_filter_le _ _).trans (by simp) - -theorem acceptCount_pos_iff : - 0 < acceptCount V a n ↔ ∃ w : List Bool, w.length = n ∧ V (a, w) = true := by - rw [acceptCount, Finset.card_pos, Finset.filter_nonempty_iff] - constructor - · rintro ⟨w, -, hw⟩ - exact ⟨List.ofFn w, List.length_ofFn, hw⟩ - · rintro ⟨w, rfl, hw⟩ - exact ⟨fun i => w[i.val], Finset.mem_univ _, by rwa [List.ofFn_getElem]⟩ - -/-- The strings that `V` accepts together with `a` and those it rejects are all the strings. -/ -theorem acceptCount_add_card_filter_eq_false : - acceptCount V a n + - (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = false).card = 2 ^ n := by - have := Finset.card_filter_add_card_filter_not (s := Finset.univ) - fun w : Fin n → Bool => V (a, List.ofFn w) = true - simpa only [acceptCount, Bool.not_eq_true, Finset.card_univ, Fintype.card_fun, Fintype.card_bool, - Fintype.card_fin] using this - -/-- **Counting strings by their prefixes**: the strings of length `m + n` accepted by `V` are the -strings `u ++ w`, with `u` of length `m` and `w` of length `n` accepted with the prefix `u`. -/ -theorem acceptCount_add (V : α × List Bool → Bool) (a : α) (m n : ℕ) : - acceptCount V a (m + n) = - ∑ u : Fin m → Bool, acceptCount (fun x => V (x.1, List.ofFn u ++ x.2)) a n := by - have h := BitString.card_filter_ofFn_add m n fun u w => V (a, u ++ w) = true - simp only [List.take_append_drop] at h - exact h - -/-- Verifiers that agree on an instance accept the same strings with it. -/ -theorem acceptCount_congr {W : α × List Bool → Bool} (h : ∀ w, V (a, w) = W (a, w)) (n : ℕ) : - acceptCount V a n = acceptCount W a n := by - simp only [acceptCount, h] - -/-- With no bits there is one string, the empty one. -/ -theorem acceptCount_zero (V : α × List Bool → Bool) (a : α) : - acceptCount V a 0 = if V (a, []) = true then 1 else 0 := by - unfold acceptCount - rw [Finset.univ_unique, Finset.filter_singleton] - split_ifs with h₁ h₂ h₂ <;> simp_all - -/-- The verifier accepting everything accepts all `2 ^ n` strings of length `n`. -/ -@[simp] -theorem acceptCount_true (a : α) (n : ℕ) : acceptCount (fun _ => true) a n = 2 ^ n := by - simp [acceptCount] - -/-- The verifier rejecting everything accepts no string. -/ -@[simp] -theorem acceptCount_false (a : α) (n : ℕ) : acceptCount (fun _ => false) a n = 0 := by - simp [acceptCount] - -/-- A verifier and its negation together accept every string once. -/ -theorem acceptCount_add_acceptCount_not (V : α × List Bool → Bool) (a : α) (n : ℕ) : - acceptCount V a n + acceptCount (fun x => !V x) a n = 2 ^ n := by - simpa only [acceptCount, Bool.not_eq_true'] using - acceptCount_add_card_filter_eq_false (V := V) (a := a) (n := n) - -/-- The negation of a verifier accepts the strings that it rejects. -/ -theorem acceptCount_not (V : α × List Bool → Bool) (a : α) (n : ℕ) : - acceptCount (fun x => !V x) a n = 2 ^ n - acceptCount V a n := by - have := acceptCount_add_acceptCount_not V a n - omega - -end acceptCount - /-- The functions counting the certificates that a polynomial-time verifier accepts, with certificates of polynomial length, with respect to the encoding `enc` of instances. -/ def SharpP (enc : α ↪ List Bool) : Set (α → ℕ) := diff --git a/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean b/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean index 47496225e5..714b56d7b4 100644 --- a/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean +++ b/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean @@ -53,8 +53,8 @@ theorem DecidesInTime.mem_iff_acceptCount_choiceTable_pos {ntm : MultiTapeNTM k {A : Set α} {t : α → ℕ} (h : ntm.DecidesInTime enc A t) {a : α} {τ : ℕ} (hτ : Nat.card (Turing.Action k Bool State) * t a ≤ τ) : a ∈ A ↔ 0 < ntm.choiceTable.acceptCount (enc a) τ := by - rw [h.mem_iff_exists_checkChoices hτ, MultiTapePTM.acceptCount_pos_iff] - simp only [checkChoices, decide_eq_true_eq] + rw [h.mem_iff_exists_checkChoices hτ, Cslib.Complexity.acceptCount_pos_iff] + rfl end Turing.MultiTapeNTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean index 1f0692c761..a81d09a827 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean @@ -7,8 +7,8 @@ Authors: Samuel Schlesinger module -- upstream: candidate +public import Complexity.Computability.Complexity.AcceptCount public import Complexity.Computability.Machines.Turing.MultiTape.Machine.Nondeterministic -import Mathlib.Data.Fintype.Pi /-! # Accepting choice strings of a fair-coin table @@ -23,7 +23,10 @@ rejects at a stuck configuration. The *accepting count* `Turing.MultiTapePTM.acceptCount machine input τ` is the number of bit strings `y ∈ {0,1}^τ` on which the table emits `[true]` on `input`: the count `A_M(x)` of the -counting simulations of nondeterministic and probabilistic time. Its fraction of all `2 ^ τ` +counting simulations of nondeterministic and probabilistic time. It is the generic count +`Cslib.Complexity.acceptCount` of the replay predicate, so the elementary lemmas about that count +(`Cslib.Complexity.acceptCount_le_two_pow`, `Cslib.Complexity.acceptCount_pos_iff`, …) apply +to it directly. Its fraction of all `2 ^ τ` strings is exactly the probability that the closed fair-coin run outputs `[true]` (`Turing.MultiTapePTM.eval_runClosed_apply_eq_acceptCount`). The membership characterizations for nondeterministic and bounded-error deciders are in @@ -39,8 +42,6 @@ for nondeterministic and bounded-error deciders are in is the accepting count divided by `2 ^ τ`. * `Turing.MultiTapePTM.half_lt_eval_runClosed_apply_iff`: strict majority acceptance, as an integer comparison `2 ^ τ < 2 * acceptCount`. -* `Turing.MultiTapePTM.acceptCount_pos_iff`: some choice string accepts. -* `Turing.MultiTapePTM.acceptCount_le_two_pow`: at most all `2 ^ τ` strings accept. * `Turing.MultiTapePTM.runClosedCoins_eq_output_stepCoins`: the replay on upstream configurations. -/ @@ -57,24 +58,9 @@ variable {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) (input : /-- **The accepting count** `A_M(x)`: the number of choice strings `y ∈ {0,1}^τ` replaying which the closed fair-coin table emits `[true]` on `input`. -/ -def acceptCount : ℕ := - (Finset.univ.filter fun y : Fin τ → Bool => - machine.runClosedCoins (List.ofFn y) input = [true]).card - -/-- At most all `2 ^ τ` choice strings accept. -/ -theorem acceptCount_le_two_pow : machine.acceptCount input τ ≤ 2 ^ τ := - (Finset.card_filter_le _ _).trans (by simp) - -/-- The accepting count is positive exactly when some choice string of length `τ` accepts. -/ -theorem acceptCount_pos_iff : - 0 < machine.acceptCount input τ ↔ - ∃ coins : List Bool, coins.length = τ ∧ machine.runClosedCoins coins input = [true] := by - rw [acceptCount, Finset.card_pos, Finset.filter_nonempty_iff] - constructor - · rintro ⟨y, -, hy⟩ - exact ⟨List.ofFn y, List.length_ofFn, hy⟩ - · rintro ⟨coins, rfl, hcoins⟩ - exact ⟨fun i => coins[i.val], Finset.mem_univ _, by rwa [List.ofFn_getElem]⟩ +abbrev acceptCount : ℕ := + Complexity.acceptCount + (fun p : List Bool × List Bool => decide (machine.runClosedCoins p.2 p.1 = [true])) input τ /-- **Acceptance probability is the accepting fraction.** The closed fair-coin run with clock `τ` outputs `[true]` with probability `acceptCount / 2 ^ τ`. -/ @@ -82,7 +68,7 @@ theorem eval_runClosed_apply_eq_acceptCount : ProbComp.eval (machine.runClosed τ input) [true] = (machine.acceptCount input τ : ℝ≥0∞) / 2 ^ τ := by rw [eval_runClosed_eq_map_coins, BitString.uniformList_map_apply] - rfl + simp only [Complexity.acceptCount, decide_eq_true_eq] /-- **Strict majority acceptance** is the integer comparison `2 ^ τ < 2 * acceptCount`. -/ theorem half_lt_eval_runClosed_apply_iff : From b06c2112f2badd9381e157200e2880137e5a13db Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:19:33 -0400 Subject: [PATCH 5/9] refactor(circuit/frontier): index explicit tables by BitString.lsbValue Address the #1844 review: replace the duplicate public `tableIndex` encoding and its lemmas by the existing `Cslib.BitString.lsbValue` and `lsbValue_lt`. Add the missing digit lemma `BitString.testBit_lsbValue` next to `lsbValue` in `BitString/Counter.lean`, and update the table lookup, its proof and the tests. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Frontier/TensorNetwork/Explicit.lean | 37 ++++++------------- .../Foundations/Data/BitString/Counter.lean | 11 ++++++ .../Circuit/Frontier/TensorNetwork.lean | 2 +- 3 files changed, 23 insertions(+), 27 deletions(-) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean index 28f5dd3f54..051a95b90a 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Computability.Circuit.Frontier.TensorNetwork +public import Complexity.Foundations.Data.BitString.Counter import Mathlib.Algebra.BigOperators.Fin import Mathlib.Data.List.GetD @@ -19,7 +20,8 @@ the number of edges, numbered `0, 1, …`, and a list of vertices, each given by * its ordered list of *ports*, the numbers of the edges at the vertex, and * its *table*: the value of its tensor when port `i` carries the bit `bs[i]` is the entry at - position `tableIndex bs`, the number whose binary digit `i` is `bs[i]`. + position `BitString.lsbValue bs`, the number whose binary digit `i` is `bs[i]` + (`BitString.testBit_lsbValue`). So a vertex with `k` ports has a table of `2 ^ k` entries. The contraction of an explicit network (`ExplicitTensorNetwork.contraction`) sums, over all assignments of bits to the edges, the product @@ -37,7 +39,6 @@ order and tabulate its tensor on them. The contraction is unchanged ## Main definitions -* `Cslib.Circuits.Frontier.tableIndex`: the position of a list of bits in a table. * `Cslib.Circuits.Frontier.ExplicitTensorNetwork`: an explicit Boolean tensor network. * `Cslib.Circuits.Frontier.ExplicitTensorNetwork.entry`, `Cslib.Circuits.Frontier.ExplicitTensorNetwork.portBits`: table lookup and the bits on a list @@ -51,8 +52,6 @@ order and tabulate its tensor on them. The contraction is unchanged ## Main results -* `Cslib.Circuits.Frontier.testBit_tableIndex`, `Cslib.Circuits.Frontier.tableIndex_lt`: the - digits and range of a table position. * `Cslib.Circuits.Frontier.ExplicitTensorNetwork.maxDegree_le_iff`: the degree bound. * `Cslib.Circuits.Frontier.TensorNetwork.entry_explicitTable`: a written-out table evaluates the tensor. @@ -68,24 +67,10 @@ order and tabulate its tensor on them. The contraction is unchanged namespace Cslib.Circuits.Frontier -/-- The position of a list of bits in a table: the number whose binary digit `i` is `bs[i]`, so -that the bits are read little-endian. -/ -def tableIndex (bs : List Bool) : ℕ := - (BitVec.ofBoolListLE bs).toNat - -/-- Binary digit `i` of the position of `bs` is `bs[i]`, or `false` past the end of `bs`. -/ -@[simp] theorem testBit_tableIndex (bs : List Bool) (i : ℕ) : - (tableIndex bs).testBit i = bs.getD i false := by - rw [tableIndex, BitVec.testBit_toNat, BitVec.getLsbD_ofBoolListLE] - -/-- A list of `k` bits has a position below `2 ^ k`. -/ -theorem tableIndex_lt (bs : List Bool) : tableIndex bs < 2 ^ bs.length := - BitVec.isLt _ - /-- An *explicit Boolean tensor network* over `R`: the number of edges, numbered from zero, and a list of vertices. A vertex is given by its ordered list of *ports*, the numbers of its edges, and -its *table*, whose entry at position `tableIndex bs` is the value of its tensor when port `i` -carries the bit `bs[i]`. -/ +its *table*, whose entry at position `BitString.lsbValue bs` is the value of its tensor when +port `i` carries the bit `bs[i]`. -/ structure ExplicitTensorNetwork (R : Type*) where /-- The number of edges; the edges are numbered `0, …, numEdges - 1`. -/ numEdges : ℕ @@ -96,10 +81,10 @@ namespace ExplicitTensorNetwork variable {R : Type*} (d : ExplicitTensorNetwork R) -/-- The entry of a table at a list of bits. A position past the end of the table has entry -zero. -/ +/-- The entry of a table at a list of bits, read little-endian (`BitString.lsbValue`). A position +past the end of the table has entry zero. -/ def entry [Zero R] (table : List R) (bs : List Bool) : R := - table.getD (tableIndex bs) 0 + table.getD (BitString.lsbValue bs) 0 /-- The bits on a list of ports under an assignment of bits to the edges. A port naming no edge reads `false`. -/ @@ -168,14 +153,14 @@ theorem entry_explicitTable [Zero R] (v : V) (x : Fin m → Bool) : ExplicitTensorNetwork.entry (N.explicitTable ee v) ((N.explicitPorts ee v).map x) = N.tensor v (x ∘ ee) := by set ps := N.explicitPorts ee v - have hlt : tableIndex (ps.map x) < (N.explicitTable ee v).length := by - simpa [explicitTable, ps] using tableIndex_lt (ps.map x) + have hlt : BitString.lsbValue (ps.map x) < (N.explicitTable ee v).length := by + simpa [explicitTable, ps] using BitString.lsbValue_lt (ps.map x) rw [ExplicitTensorNetwork.entry, List.getD_eq_getElem _ _ hlt] simp only [explicitTable, List.getElem_map, List.getElem_range] refine N.tensor_congr v _ _ fun e he => ?_ have hmem : ee e ∈ ps := (N.mem_explicitPorts ee).mpr (by simpa using he) have hidx := List.idxOf_lt_length_of_mem hmem - rw [testBit_tableIndex, List.getD_eq_getElem _ _ (by simpa using hidx), List.getElem_map, + rw [BitString.testBit_lsbValue, List.getD_eq_getElem _ _ (by simpa using hidx), List.getElem_map, List.getElem_idxOf hidx, Function.comp_apply] /-- A Boolean tensor network on finite types written out as an explicit network, numbering the diff --git a/Complexity/Foundations/Data/BitString/Counter.lean b/Complexity/Foundations/Data/BitString/Counter.lean index d13e8137f0..40319f05b8 100644 --- a/Complexity/Foundations/Data/BitString/Counter.lean +++ b/Complexity/Foundations/Data/BitString/Counter.lean @@ -35,6 +35,7 @@ their candidates in this way, storing only the current one. * `Cslib.BitString.iterate_increment`, `Cslib.BitString.iterate_increment_lsbValue`: counting from zero enumerates the words of a length. * `Cslib.BitString.lsbValue_eq_foldr_bit`: `lsbValue` is a right fold of `Nat.bit`. +* `Cslib.BitString.testBit_lsbValue`: binary digit `i` of `lsbValue w` is the bit `w[i]`. -/ @[expose] public section @@ -154,4 +155,14 @@ theorem lsbValue_eq_foldr_bit (w : List Bool) : lsbValue w = w.foldr Nat.bit 0 : | nil => rfl | cons b w ih => rw [lsbValue, List.foldr_cons, ← ih, Nat.bit_val, Nat.add_comm] +/-- Binary digit `i` of the value of a word is its bit `i`, or `false` past its end. -/ +@[simp] theorem testBit_lsbValue : ∀ (w : List Bool) (i : ℕ), + (lsbValue w).testBit i = w.getD i false + | [], _ => by simp [lsbValue] + | b :: w, i => by + rw [lsbValue_eq_foldr_bit, List.foldr_cons, ← lsbValue_eq_foldr_bit] + cases i with + | zero => simp + | succ i => simp [Nat.testBit_bit_succ, testBit_lsbValue w i] + end Cslib.BitString diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean index 5be31a11e9..27d867afd5 100644 --- a/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean @@ -60,7 +60,7 @@ example : (cycle neTable).contraction = 0 := by decide /-- The table `A` or `B` of `parallel` as a tensor on assignments to `Fin 2`. -/ def table (v : Fin 2) (x : Fin 2 → Bool) : ℤ := - [[1, 2, 3, 4], [5, 6, 7, 8]][v]!.getD (tableIndex [x 0, x 1]) 0 + [[1, 2, 3, 4], [5, 6, 7, 8]][v]!.getD (Cslib.BitString.lsbValue [x 0, x 1]) 0 /-- The network `parallel` on `Fin 2` vertices and `Fin 2` edges, both edges from `0` to `1`. Every edge is at both vertices, so the tensors are trivially local. -/ From 13a6daeafef1e752435505e47f5329da96b392e6 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:24:25 -0400 Subject: [PATCH 6/9] feat(circuit/frontier): binarize a tensor network by an injective code MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit An injective code `U → (Fin m → Bool)` turns a tensor network over a finite alphabet into a Boolean one on `m` parallel copies of every edge. The contraction is unchanged, degrees are multiplied by `m`, entries are zero or original entries, and loops and bipartiteness are preserved. Used by the HPV block-counting networks of #1833 (H3). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Frontier/TensorNetwork/Binarize.lean | 165 ++++++++++++++++++ .../Frontier/TensorNetworkBinarize.lean | 78 +++++++++ 3 files changed, 244 insertions(+) create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork/Binarize.lean create mode 100644 ComplexityTests/Computability/Circuit/Frontier/TensorNetworkBinarize.lean diff --git a/Complexity.lean b/Complexity.lean index 3e53d5172a..d6cce81ba8 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -858,6 +858,7 @@ public import Complexity.Computability.Circuit.Frontier.Rectangle public import Complexity.Computability.Circuit.Frontier.Reduction public import Complexity.Computability.Circuit.Frontier.Sweep public import Complexity.Computability.Circuit.Frontier.TensorNetwork +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Binarize public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Constraint public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit public import Complexity.Computability.Circuit.Frontier.TwoSidedWitness diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Binarize.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Binarize.lean new file mode 100644 index 0000000000..caaca2155c --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Binarize.lean @@ -0,0 +1,165 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork +public import Mathlib.Logic.Function.Basic +import Mathlib.Data.Set.Card + +/-! +# Binarizing a tensor network + +A tensor network whose edges carry letters of a finite alphabet `U` becomes a Boolean tensor +network once every letter is written in `m` bits. Fix an injective *code* +`code : U → (Fin m → Bool)`. The *binarization* `TensorNetwork.binarize` replaces every edge `e` +by the `m` parallel Boolean edges `(e, 0), …, (e, m - 1)` between the same two vertices. A vertex +decodes the `m` bits on each of its edges and evaluates its old tensor on the decoded letters; if +the bits on one of its edges are not the code of any letter, its tensor is zero. + +The contraction is unchanged (`TensorNetwork.contraction_binarize`): assignments of bits in which +every edge carries a code word correspond exactly to assignments of letters, and every other +assignment of bits has an edge with an invalid code word, whose source tensor vanishes. Every edge +becomes `m` edges, so vertex degrees are multiplied by `m` +(`TensorNetwork.maxDegreeLE_binarize`). Every tensor entry of the binarization is zero or an entry +of the original network (`TensorNetwork.tensor_binarize_eq_zero_or`). Loops and bipartiteness are +preserved. + +This lets a construction use a structured alphabet, such as words over a machine's tape alphabet, +and then pass to the Boolean networks of [OpenAI2026ETH], Appendix D. + +## Main definitions + +* `Cslib.Circuits.Frontier.TensorNetwork.binarize`: the binarization by a code. +* `Cslib.Circuits.Frontier.TensorNetwork.bitsOn`: the bits on the copies of an edge. + +## Main results + +* `Cslib.Circuits.Frontier.TensorNetwork.contraction_binarize`: binarization by an injective code + preserves the contraction. +* `Cslib.Circuits.Frontier.TensorNetwork.maxDegreeLE_binarize`: degrees are multiplied by the + code length. +* `Cslib.Circuits.Frontier.TensorNetwork.loopless_binarize`, + `Cslib.Circuits.Frontier.TensorNetwork.isBipartite_binarize`: loops and bipartiteness are + preserved. +* `Cslib.Circuits.Frontier.TensorNetwork.tensor_binarize_eq_zero_or`: binarized entries are zero + or original entries. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.1 (p. 53). +-/ + +public section + +namespace Cslib.Circuits.Frontier.TensorNetwork + +open Function + +variable {R U V E : Type*} {m : ℕ} + +/-- The bits on the `m` copies of the edge `e`. -/ +@[expose] def bitsOn (y : E × Fin m → Bool) (e : E) : Fin m → Bool := + fun j => y (e, j) + +@[simp] theorem bitsOn_apply (y : E × Fin m → Bool) (e : E) (j : Fin m) : + bitsOn y e j = y (e, j) := rfl + +variable [Zero R] [Nonempty U] (N : TensorNetwork R U V E) (code : U → Fin m → Bool) + +open Classical in +/-- The *binarization* of a tensor network by a code `code : U → (Fin m → Bool)`. Every edge `e` +becomes the `m` Boolean edges `(e, j)` between the same two vertices. A vertex whose edges all +carry code words evaluates its old tensor on the decoded letters (`Function.invFun code`); a +vertex with an edge carrying a word that is not a code word has tensor zero. -/ +@[expose] noncomputable def binarize : TensorNetwork R Bool V (E × Fin m) where + src p := N.src p.1 + tgt p := N.tgt p.1 + tensor v y := + if ∀ e, N.src e = v ∨ N.tgt e = v → bitsOn y e ∈ Set.range code then + N.tensor v fun e => invFun code (bitsOn y e) + else 0 + tensor_congr v y y' h := by + have hrow : ∀ e, N.src e = v ∨ N.tgt e = v → bitsOn y e = bitsOn y' e := + fun e he => funext fun j => h (e, j) he + have hcond : (∀ e, N.src e = v ∨ N.tgt e = v → bitsOn y e ∈ Set.range code) ↔ + ∀ e, N.src e = v ∨ N.tgt e = v → bitsOn y' e ∈ Set.range code := + forall_congr' fun e => imp_congr_right fun he => by rw [hrow e he] + simp only [hcond] + split_ifs + · exact N.tensor_congr v _ _ fun e he => by rw [hrow e he] + · rfl + +@[simp] theorem binarize_src (p : E × Fin m) : (N.binarize code).src p = N.src p.1 := rfl + +@[simp] theorem binarize_tgt (p : E × Fin m) : (N.binarize code).tgt p = N.tgt p.1 := rfl + +/-- Every tensor entry of the binarization is zero or an entry of the original network at some +assignment of letters. -/ +theorem tensor_binarize_eq_zero_or (v : V) (y : E × Fin m → Bool) : + (N.binarize code).tensor v y = 0 ∨ ∃ x, (N.binarize code).tensor v y = N.tensor v x := by + classical + simp only [binarize] + split_ifs + · exact Or.inr ⟨_, rfl⟩ + · exact Or.inl rfl + +/-- Binarization keeps a network without loops loopless. -/ +theorem loopless_binarize (h : N.Loopless) : (N.binarize code).Loopless := + fun p => h p.1 + +/-- Binarization keeps a network bipartite, with the same sides. -/ +theorem isBipartite_binarize (h : N.IsBipartite) : (N.binarize code).IsBipartite := by + obtain ⟨side, hside⟩ := h + exact ⟨side, fun p => hside p.1⟩ + +/-- The edges at a vertex of the binarization are the copies of its old edges. -/ +theorem incidenceSet_binarize (v : V) : + (N.binarize code).incidenceSet v = N.incidenceSet v ×ˢ Set.univ := by + ext p + simp [Multigraph.mem_incidenceSet] + +/-- **Binarization multiplies degrees by the code length.** -/ +theorem maxDegreeLE_binarize [Finite E] {d : ℕ} (hd : N.MaxDegreeLE d) : + (N.binarize code).MaxDegreeLE (d * m) := by + intro v + rw [incidenceSet_binarize, Set.ncard_prod, Set.ncard_univ, Nat.card_eq_fintype_card, + Fintype.card_fin] + exact Nat.mul_le_mul_right m (hd v) + +/-- **Binarization preserves the contraction.** Assignments of bits in which every edge carries a +code word are the codes of the assignments of letters, and every other assignment of bits has an +edge with an invalid word, at whose source the tensor vanishes. -/ +theorem contraction_binarize {R : Type*} [CommSemiring R] [Fintype U] [Fintype V] [Fintype E] + [DecidableEq E] (N : TensorNetwork R U V E) {code : U → Fin m → Bool} + (hcode : Injective code) : (N.binarize code).contraction = N.contraction := by + classical + symm + refine Fintype.sum_of_injective (fun x p => code (x p.1) p.2) ?_ _ _ ?_ fun x => ?_ + · -- Distinct assignments of letters differ at some edge, so their codes differ there. + intro x x' hxx' + funext e + exact hcode (funext fun j => congrFun hxx' (e, j)) + · -- A word on some edge is not a code word, so the tensor at its source vanishes. + intro y hy + have : ∃ e, bitsOn y e ∉ Set.range code := by + by_contra! hall + exact hy ⟨fun e => invFun code (bitsOn y e), funext fun p => + congrFun (invFun_eq (hall p.1)) p.2⟩ + obtain ⟨e, he⟩ := this + refine Finset.prod_eq_zero (Finset.mem_univ (N.src e)) ?_ + simp only [binarize] + rw [ite_eq_right fun hall => he (hall e (Or.inl rfl))] + · -- On a code word everywhere, every vertex decodes the original assignment. + refine Finset.prod_congr rfl fun v _ => ?_ + simp only [binarize] + rw [ite_eq_left fun e _ => ⟨x e, rfl⟩] + congr 1 + funext e + exact (leftInverse_invFun hcode (x e)).symm + +end Cslib.Circuits.Frontier.TensorNetwork diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkBinarize.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkBinarize.lean new file mode 100644 index 0000000000..72f6e28aaf --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkBinarize.lean @@ -0,0 +1,78 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: local-only (test driver) + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Binarize +public import Mathlib.Data.Fin.VecNotation + +/-! +# Tests for binarized tensor networks + +A network with one edge over the alphabet `Fin 3`, binarized with the two-bit code of each +letter: its contraction is unchanged, the unused word `(true, true)` gets weight zero, a valid +word reads the original tensor, and the degree doubles. +-/ + +@[expose] public section + +namespace ComplexityTests.Computability.Circuit.Frontier.TensorNetworkBinarize + +open Cslib.Circuits.Frontier + +/-- Two vertices joined by one edge carrying a letter of `Fin 3`, with the tensors +`A = (1, 2, 3)` at vertex `0` and `B = (4, 5, 6)` at vertex `1`. -/ +def ternary : TensorNetwork ℕ (Fin 3) (Fin 2) Unit where + src _ := 0 + tgt _ := 1 + tensor v x := ![![1, 2, 3], ![4, 5, 6]] v (x ()) + tensor_congr v x y h := by + rw [h () (by fin_cases v <;> simp)] + +/-- By hand: `Z = 1·4 + 2·5 + 3·6 = 32`. -/ +theorem contraction_ternary : ternary.contraction = 32 := by decide + +/-- The two binary digits of a letter, least significant first. -/ +def code (u : Fin 3) : Fin 2 → Bool := + ![u.val.testBit 0, u.val.testBit 1] + +theorem code_injective : Function.Injective code := by decide + +/-- Binarization keeps the contraction `32`. -/ +example : (ternary.binarize code).contraction = 32 := by + rw [TensorNetwork.contraction_binarize _ code_injective, contraction_ternary] + +/-- The word `(true, true)` codes no letter, so a vertex reading it has weight zero. -/ +example : (ternary.binarize code).tensor 0 (fun _ => true) = 0 := by + have : TensorNetwork.bitsOn (fun _ : Unit × Fin 2 => true) () ∉ Set.range code := by + rintro ⟨u, hu⟩ + have h0 := congrFun hu 0 + have h1 := congrFun hu 1 + revert h0 h1 + fin_cases u <;> decide + simp only [TensorNetwork.binarize] + exact ite_eq_right fun h => this (h () (Or.inl rfl)) + +/-- The word `(false, true)` codes the letter `2`, so vertex `1` reads its entry `6`. -/ +example : (ternary.binarize code).tensor 1 (fun p => p.2 = 1) = 6 := by + have hword : TensorNetwork.bitsOn (fun p : Unit × Fin 2 => decide (p.2 = 1)) () = code 2 := by + funext j + fin_cases j <;> rfl + have hdec : Function.invFun code (code 2) = 2 := + Function.leftInverse_invFun code_injective 2 + simp only [TensorNetwork.binarize] + rw [ite_eq_left fun e _ => ⟨2, by cases e; exact hword.symm⟩] + simp only [ternary, hword, hdec] + rfl + +/-- Each vertex has one edge; after binarization it has two, and the network stays bipartite. -/ +example : (ternary.binarize code).MaxDegreeLE 2 ∧ (ternary.binarize code).IsBipartite := by + refine ⟨ternary.maxDegreeLE_binarize code (d := 1) fun v => ?_, + ternary.isBipartite_binarize code ⟨fun v => v = 0, fun _ => by simp [ternary]⟩⟩ + exact (Set.ncard_le_card _).trans (by simp) + +end ComplexityTests.Computability.Circuit.Frontier.TensorNetworkBinarize From 822658ff3d92494f44dbe97d1bae3ef090f55b0c Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:39:42 -0400 Subject: [PATCH 7/9] feat(machines): interval tensors of HPV-blocked coin runs (#1833 H3) Views of a configuration with blocks of length `b` (block indices, control record, window contents), the configuration embedded from a view, interval steps and the interval tensor `F_i` of Lemma 2.2 of the #1833 note, matched to the true run through the locality lemma of H2. Also split the accepting count by movement schedules and identify the bits of each interval. `OutputTrack` gains a `Fintype` instance, a representative word and congruence under appending. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 3 +- .../Turing/MultiTape/Machine/ChoiceTable.lean | 24 +- .../Probabilistic/IntervalTensor.lean | 351 ++++++++++++++++++ ComplexityTests/HPVIntervalTensors.lean | 106 ++++++ 4 files changed, 479 insertions(+), 5 deletions(-) create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalTensor.lean create mode 100644 ComplexityTests/HPVIntervalTensors.lean diff --git a/Complexity.lean b/Complexity.lean index 0323fa5922..e16898c89c 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1799,8 +1799,8 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.WhileC public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.WhileInput public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic -public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Blocks public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.AcceptCount +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Blocks public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Clock public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Closed public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.CoinTape @@ -1808,6 +1808,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.C public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Deterministic public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExtendTapes public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.InputFromTape +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalTensor public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IterateWhile public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Loop public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.OrElse diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Machine/ChoiceTable.lean b/Complexity/Computability/Machines/Turing/MultiTape/Machine/ChoiceTable.lean index 6394b54282..487783761f 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Machine/ChoiceTable.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Machine/ChoiceTable.lean @@ -87,10 +87,8 @@ inductive OutputTrack namespace OutputTrack -instance : Finite OutputTrack := - Finite.of_surjective (fun i : Fin 3 => [empty, accept, other][i]) fun t => by - cases t - exacts [⟨0, rfl⟩, ⟨1, rfl⟩, ⟨2, rfl⟩] +instance : Fintype OutputTrack := + ⟨{empty, accept, other}, fun t => by cases t <;> simp⟩ /-- The track of a word. -/ def ofWord (word : List Bool) : OutputTrack := @@ -120,6 +118,24 @@ theorem ofWord_eq_accept_iff (word : List Bool) : ofWord word = accept ↔ word unfold ofWord split_ifs with h₁ h₂ <;> simp_all +/-- Emitting the same word after words with the same track gives words with the same track. -/ +theorem ofWord_append_eq_of_eq {word word' : List Bool} (h : ofWord word = ofWord word') + (more : List Bool) : ofWord (word ++ more) = ofWord (word' ++ more) := by + induction more using List.reverseRecOn with + | nil => simpa using h + | append_singleton more symbol ih => + have hsym : [symbol] = (some symbol).toList := rfl + rw [← List.append_assoc, ← List.append_assoc, hsym, ofWord_append, ofWord_append, ih] + +/-- A word with a given track: `[]`, `[true]` or `[false]`. -/ +def toWord : OutputTrack → List Bool + | empty => [] + | accept => [true] + | other => [false] + +@[simp] theorem ofWord_toWord (track : OutputTrack) : ofWord track.toWord = track := by + cases track <;> rfl + end OutputTrack /-- The states of the choice table: the simulated state, the index of the candidate action, and diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalTensor.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalTensor.lean new file mode 100644 index 0000000000..18eaa4a012 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalTensor.lean @@ -0,0 +1,351 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.AcceptCount +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Blocks +public import Complexity.Computability.Machines.Turing.MultiTape.Machine.ChoiceTable +public import Mathlib.Data.ZMod.Defs +import Mathlib.Data.ZMod.Basic +import Mathlib.Logic.Equiv.Fin.Basic +import Mathlib.Tactic.Linarith + +/-! +# Interval tensors of a choice-string run + +The local pieces of the block-counting identity, Lemma 2.2 of the note *Deterministic +simulations of nondeterministic and randomized time* (30 October 2026) formalized in issue #1833, +which builds on the blocking of Hopcroft, Paul and Valiant [HopcroftPaulValiant1977] in the +three-block form of `Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Blocks` +(compare [Williams2025], Lemma 2.1 and §3.2). The proof idea is original to that note. + +Fix a block length `b > 0`. A configuration of a fair-coin table over `Bool` is seen through + +* its *block indices* `Turing.Cfg.blockIndex`: the block `p / b` of every head; +* its *control record* `Turing.Cfg.blockControl`: its state, the offset `p mod b` of every head + in its block, and the track (`Turing.MultiTapeNTM.ChoiceTable.OutputTrack`) of its output; +* its *window contents* `Turing.Cfg.windowContents`: the contents of the three blocks + `J - 1, J, J + 1` around given block indices `J` on every work tape. + +Conversely, `Turing.embedCfg` builds a configuration from block indices, a control record and +window contents, with blank cells outside the windows and an output of the right track. The +*interval step* `Turing.MultiTapePTM.IntervalStep` replays the bits of a time interval from such +an embedded configuration and compares the record, window contents and block indices it leaves +with prescribed ones. The *interval tensor* `Turing.MultiTapePTM.intervalCount` counts the bit +strings `u ∈ {0,1}^b` doing so: the entry `F_i` of the note's equation (3). + +**Matching the true run** (`Turing.MultiTapePTM.intervalStep_view_iff`). Embedding the view of a +configuration `c` gives a configuration that agrees with `c` on its state, its heads and its +windows, and whose output has the same track. By the locality of runs +(`Turing.MultiTapePTM.agreeOn_blockWindow_stepCoins`), an interval step from the view of `c` +holds exactly when the true replay from `c` leaves the prescribed record, contents and block +indices. The input tape is not blocked as a word: it is fixed by `input`, which the embedded +configuration shares. + +**Splitting the count by schedules** (`Turing.MultiTapePTM.acceptCount_eq_sum_card_schedule`). +The accepting count `A_M(x)` on `q * b` bits is the sum, over the movement schedules `σ` of `q` +intervals, of the number of accepting choice strings with schedule `σ`. The bits of interval `i` +of a choice string `y : Fin (q * b) → Bool` are `y (finProdFinEquiv (i, r))` for `r < b` +(`Turing.MultiTapePTM.intervalStart_succ_ofFn`). + +## Main definitions + +* `Turing.Cfg.blockIndex`, `Turing.Cfg.blockContents`, `Turing.Cfg.windowContents`: block + indices and block contents. +* `Turing.BlockControl`, `Turing.Cfg.blockControl`: control records. +* `Turing.embedCfg`: the configuration with given block indices, record and window contents. +* `Turing.MultiTapePTM.IntervalStep`, `Turing.MultiTapePTM.intervalCount`: interval steps and + interval tensors. + +## Main results + +* `Turing.MultiTapePTM.acceptCount_eq_sum_card_schedule`: the accepting count split by schedules. +* `Turing.MultiTapePTM.intervalStart_succ_ofFn`: the bits of each interval. +* `Turing.agreeOn_embedCfg_view`: an embedded view agrees with the configuration on its windows. +* `Turing.MultiTapePTM.intervalStep_view_iff`: interval steps from a view are the true replay. +* `Turing.MultiTapePTM.intervalCount_le`: interval tensor entries are at most `2 ^ b`. + +## References + +* [J. Hopcroft, W. Paul, L. Valiant, *On Time Versus Space*][HopcroftPaulValiant1977] +* [R. Williams, *Simulating Time With Square-Root Space*][Williams2025] +-/ + +public section + +namespace Turing + +open MultiTapeNTM.ChoiceTable + +variable {k : ℕ} {Symbol State : Type} + +/-! ### Views of a configuration -/ + +section View + +variable (b : ℕ) [NeZero b] {input : List Symbol} + +/-- The block index of every head, with blocks of length `b`: a head at coordinate `p` is in +block `p / b`. -/ +@[expose] def Cfg.blockIndex (c : Cfg k Symbol State input) (head : Option (Fin k)) : ℤ := + c.headPos head / b + +/-- The contents of block `j` of work tape `h`, with blocks of length `b`: the cells +`b * j + r` for `r < b`. -/ +@[expose] def Cfg.blockContents (c : Cfg k Symbol State input) (h : Fin k) (j : ℤ) : + ZMod b → Option Symbol := + fun r => c.workTapes h (b * j + r.val) + +/-- The contents of the three blocks `J h - 1, J h, J h + 1` around block indices `J` on every +work tape `h`; entry `d : Fin 3` is block `J h + d - 1`. -/ +@[expose] def Cfg.windowContents (J : Option (Fin k) → ℤ) (c : Cfg k Symbol State input) : + Fin k → Fin 3 → ZMod b → Option Symbol := + fun h d => c.blockContents b h (J (some h) + d - 1) + +end View + +section Embed + +variable (b : ℕ) [NeZero b] {input : List Bool} + +/-- A *control record* with blocks of length `b`: a state, the offset of every head in its block, +and the track of the output. -/ +abbrev BlockControl (k : ℕ) (State : Type) (b : ℕ) := + Option State × (Option (Fin k) → ZMod b) × OutputTrack + +/-- The control record of a configuration: its state, the offset `p mod b` of every head, and the +track of its output. -/ +@[expose] def Cfg.blockControl (c : Cfg k Bool State input) : + BlockControl k State b := + (c.state, fun head => (c.headPos head : ZMod b), OutputTrack.ofWord c.output) + +/-- The input head position with coordinate `p`, that is, stored position `p + 1`, or the +left end when `p + 1` is out of range. -/ +@[expose] def inputPosOfCoord (input : List Bool) (p : ℤ) : Fin (input.length + 2) := + if h : 0 ≤ p + 1 ∧ p + 1 < input.length + 2 then ⟨(p + 1).toNat, by omega⟩ else 0 + +/-- Cell `z` of work tape `h` of the configuration with window contents `w` at block indices `J`: +the entry of `w` if `z` lies in one of the three blocks around `J h`, and blank otherwise. -/ +@[expose] def windowCell (J : Option (Fin k) → ℤ) (w : Fin k → Fin 3 → ZMod b → Option Bool) + (h : Fin k) (z : ℤ) : Option Bool := + if hz : 0 ≤ z / b - J (some h) + 1 ∧ z / b - J (some h) + 1 < 3 then + w h ⟨(z / b - J (some h) + 1).toNat, by omega⟩ z + else none + +/-- The configuration with block indices `J`, control record `c` and window contents `w`: every +head at `b * J + offset`, the work tapes holding `w` on the windows and blank elsewhere, and an +output with the track of `c`. -/ +@[expose] def embedCfg (J : Option (Fin k) → ℤ) (c : BlockControl k State b) + (w : Fin k → Fin 3 → ZMod b → Option Bool) : Cfg k Bool State input where + state := c.1 + inputPos := inputPosOfCoord input (b * J none + (c.2.1 none).val) + workTapes := windowCell b J w + workTapePos h := b * J (some h) + (c.2.1 (some h)).val + output := c.2.2.toWord + +variable {b} + +/-- A coordinate is its block start plus its offset. -/ +private theorem mul_ediv_add_val_intCast (p : ℤ) : + (b : ℤ) * (p / b) + ((p : ZMod b).val : ℤ) = p := by + rw [ZMod.val_intCast] + exact Int.mul_ediv_add_emod p b + +omit [NeZero b] in +/-- The embedded configuration has the output track of its record. -/ +@[simp] theorem ofWord_output_embedCfg (J : Option (Fin k) → ℤ) (c : BlockControl k State b) + (w : Fin k → Fin 3 → ZMod b → Option Bool) : + OutputTrack.ofWord (embedCfg (input := input) b J c w).output = c.2.2 := + OutputTrack.ofWord_toWord _ + +/-- The cells of the window entries lie in the three blocks around the block index. -/ +private theorem mem_blockWindow_of_window {c : Cfg k Bool State input} (h : Fin k) (d : Fin 3) + (r : ZMod b) : + b * (c.blockIndex b (some h) + d - 1) + (r.val : ℤ) ∈ c.blockWindow b h := by + have hb : (0 : ℤ) < b := by exact_mod_cast Nat.pos_of_neZero b + have hr : (r.val : ℤ) < b := by exact_mod_cast ZMod.val_lt r + have hd : ((d : ℕ) : ℤ) < 3 := by exact_mod_cast d.isLt + simp only [Cfg.blockWindow, Cfg.blockIndex, Cfg.headPos_some, Set.mem_Ico] + constructor <;> nlinarith + +/-- **An embedded view agrees with the configuration.** Embedding the block indices, control +record and window contents of `c` gives a configuration with the state, heads and window contents +of `c`. -/ +theorem agreeOn_embedCfg_view (c : Cfg k Bool State input) : + (embedCfg b (c.blockIndex b) (c.blockControl b) + (c.windowContents b (c.blockIndex b))).AgreeOn (c.blockWindow b) c := by + have hb : (0 : ℤ) < b := by exact_mod_cast Nat.pos_of_neZero b + refine ⟨rfl, ?_, ?_, fun h z hz => ?_⟩ + · -- The input head is at its coordinate plus one, which is in range. + have hpos := mul_ediv_add_val_intCast (b := b) (c.headPos none) + have hlt := c.inputPos.isLt + change inputPosOfCoord input + (b * (c.headPos none / b) + ((c.headPos none : ZMod b)).val) = c.inputPos + rw [hpos, Cfg.headPos_none] + unfold inputPosOfCoord + split_ifs with hcond + · ext + simp only + omega + · exact absurd ⟨by omega, by omega⟩ hcond + · funext h + exact mul_ediv_add_val_intCast (c.headPos (some h)) + · -- A window cell `z` is entry `z / b - J + 1` of the window, at offset `z mod b`. + simp only [Cfg.blockWindow, Set.mem_Ico] at hz + have hlo := Int.emod_nonneg z hb.ne' + have hhi := Int.emod_lt_of_pos z hb + have hval := mul_ediv_add_val_intCast (b := b) z + have hdiv := Int.mul_ediv_add_emod z b + have hJ : c.blockIndex b (some h) = c.workTapePos h / b := rfl + have h₁ : c.workTapePos h / b - 1 ≤ z / b := by + by_contra hcon + have : b * (z / b) ≤ b * (c.workTapePos h / b - 2) := + mul_le_mul_of_nonneg_left (by omega) hb.le + nlinarith + have h₂ : z / b < c.workTapePos h / b + 2 := by + by_contra hcon + have : b * (c.workTapePos h / b + 2) ≤ b * (z / b) := + mul_le_mul_of_nonneg_left (by omega) hb.le + nlinarith + have hcond : 0 ≤ z / b - c.blockIndex b (some h) + 1 ∧ + z / b - c.blockIndex b (some h) + 1 < 3 := by + rw [hJ] + omega + change windowCell b (c.blockIndex b) (c.windowContents b (c.blockIndex b)) h z = _ + rw [windowCell, dite_eq_left hcond] + simp only [Cfg.windowContents, Cfg.blockContents] + rw [Int.toNat_of_nonneg hcond.1, + show c.blockIndex b (some h) + (z / b - c.blockIndex b (some h) + 1) - 1 = z / b by ring, + hval] + +end Embed + +namespace MultiTapePTM + +variable (machine : MultiTapePTM k Bool State) {input : List Bool} + +/-! ### Interval steps and interval tensors -/ + +section Interval + +variable (b : ℕ) [NeZero b] + +/-- **An interval step.** Replaying `coins` from the configuration embedded at block indices `J` +with entering control record `cIn` and window contents `wIn` leaves the control record `cOut`, +the contents `wOut` of the same windows, and moves the block of every head `h` by `δ h`. -/ +def IntervalStep (input : List Bool) (J : Option (Fin k) → ℤ) (δ : Option (Fin k) → SignType) + (cIn : BlockControl k State b) (wIn : Fin k → Fin 3 → ZMod b → Option Bool) + (coins : List Bool) (cOut : BlockControl k State b) + (wOut : Fin k → Fin 3 → ZMod b → Option Bool) : Prop := + (machine.stepCoins coins (embedCfg (input := input) b J cIn wIn)).blockControl b = cOut ∧ + (machine.stepCoins coins (embedCfg (input := input) b J cIn wIn)).windowContents b J = wOut ∧ + ∀ head, (machine.stepCoins coins (embedCfg (input := input) b J cIn wIn)).blockIndex b head = + J head + δ head + +open scoped Classical in +/-- **The interval tensor**: the number of bit strings `u ∈ {0,1}^b` whose replay is an interval +step from the entering record `cIn` and contents `wIn` at block indices `J` to the leaving record +`cOut` and contents `wOut`, moving the blocks by `δ`. This is the entry `F_i` of the note's +equation (3). -/ +noncomputable def intervalCount (input : List Bool) (J : Option (Fin k) → ℤ) + (δ : Option (Fin k) → SignType) (cIn : BlockControl k State b) + (wIn : Fin k → Fin 3 → ZMod b → Option Bool) + (cOut : BlockControl k State b) (wOut : Fin k → Fin 3 → ZMod b → Option Bool) : ℕ := + (Finset.univ.filter fun u : Fin b → Bool => + machine.IntervalStep b input J δ cIn wIn (List.ofFn u) cOut wOut).card + +omit [NeZero b] in +/-- An interval tensor entry is at most the number `2 ^ b` of bit strings. -/ +theorem intervalCount_le (input : List Bool) (J : Option (Fin k) → ℤ) + (δ : Option (Fin k) → SignType) (cIn : BlockControl k State b) + (wIn : Fin k → Fin 3 → ZMod b → Option Bool) + (cOut : BlockControl k State b) (wOut : Fin k → Fin 3 → ZMod b → Option Bool) : + machine.intervalCount b input J δ cIn wIn cOut wOut ≤ 2 ^ b := by + classical + unfold intervalCount + exact (Finset.card_filter_le _ _).trans (by simp) + +/-- **Interval steps from a view are the true replay.** For at most `b` bits, an interval step +from the view of `c` (its block indices, control record and window contents) holds exactly when +replaying the bits from `c` itself leaves the prescribed record and window contents and moves the +blocks by `δ`. -/ +theorem intervalStep_view_iff (c : Cfg k Bool State input) {coins : List Bool} + (hlen : coins.length ≤ b) (δ : Option (Fin k) → SignType) (cOut : BlockControl k State b) + (wOut : Fin k → Fin 3 → ZMod b → Option Bool) : + machine.IntervalStep b input (c.blockIndex b) δ (c.blockControl b) + (c.windowContents b (c.blockIndex b)) coins cOut wOut ↔ + (machine.stepCoins coins c).blockControl b = cOut ∧ + (machine.stepCoins coins c).windowContents b (c.blockIndex b) = wOut ∧ + ∀ head, (machine.stepCoins coins c).blockIndex b head = c.blockIndex b head + δ head := by + set e := embedCfg (input := input) b (c.blockIndex b) (c.blockControl b) + (c.windowContents b (c.blockIndex b)) + obtain ⟨hagree, word, hword, hword'⟩ := + machine.agreeOn_blockWindow_stepCoins (Nat.pos_of_neZero b) hlen + (agreeOn_embedCfg_view c).symm (coins := coins) + replace hagree := hagree.symm + -- The two replays have the same state, heads, output track and window contents. + have htrack : OutputTrack.ofWord (machine.stepCoins coins e).output = + OutputTrack.ofWord (machine.stepCoins coins c).output := by + rw [hword, hword'] + refine OutputTrack.ofWord_append_eq_of_eq ?_ word + rw [ofWord_output_embedCfg] + rfl + have hcontrol : (machine.stepCoins coins e).blockControl b = + (machine.stepCoins coins c).blockControl b := by + rw [Cfg.blockControl, Cfg.blockControl, hagree.state_eq, hagree.headPos_eq, htrack] + have hwindow : (machine.stepCoins coins e).windowContents b (c.blockIndex b) = + (machine.stepCoins coins c).windowContents b (c.blockIndex b) := by + funext h d r + exact hagree.workTapes_eq h _ (mem_blockWindow_of_window h d r) + have hindex : (machine.stepCoins coins e).blockIndex b = + (machine.stepCoins coins c).blockIndex b := by + funext head + rw [Cfg.blockIndex, Cfg.blockIndex, hagree.headPos_eq] + rw [IntervalStep, hcontrol, hwindow, hindex] + +end Interval + +/-! ### Splitting the accepting count -/ + +/-- **The accepting count split by schedules.** The accepting choice strings of `q` intervals of +`b` bits are counted schedule by schedule. -/ +theorem acceptCount_eq_sum_card_schedule (input : List Bool) (b q : ℕ) : + machine.acceptCount input (q * b) = ∑ σ : Schedule k q, + (Finset.univ.filter fun y : Fin (q * b) → Bool => + machine.runClosedCoins (List.ofFn y) input = [true] ∧ + machine.schedule b q (List.ofFn y) (Cfg.init machine.initial input) = σ).card := by + classical + rw [acceptCount, Cslib.Complexity.acceptCount, Finset.card_eq_sum_card_fiberwise + (f := fun y : Fin (q * b) → Bool => + machine.schedule b q (List.ofFn y) (Cfg.init machine.initial input)) + (t := Finset.univ) fun _ _ => Finset.mem_coe.mpr (Finset.mem_univ _)] + refine Finset.sum_congr rfl fun σ _ => ?_ + rw [Finset.filter_filter] + simp only [decide_eq_true_eq] + +/-- **The bits of an interval.** For a choice string `y` of `q` intervals of `b` bits, interval +`i` replays the bits `y (finProdFinEquiv (i, r))`, `r < b`. -/ +theorem intervalStart_succ_ofFn {q b : ℕ} (y : Fin (q * b) → Bool) (c : Cfg k Bool State input) + (i : Fin q) : + machine.intervalStart b (List.ofFn y) c (i + 1) = + machine.stepCoins (List.ofFn fun r : Fin b => y (finProdFinEquiv (i, r))) + (machine.intervalStart b (List.ofFn y) c i) := by + rw [intervalStart_succ] + congr 1 + have hi := i.isLt + have hle : i * b + b ≤ q * b := by nlinarith + refine List.ext_getElem (by simp; omega) fun r h₁ h₂ => ?_ + simp only [List.getElem_take, List.getElem_drop, List.getElem_ofFn] + congr 1 + ext + change i * b + r = r + b * i + ring + +end MultiTapePTM + +end Turing diff --git a/ComplexityTests/HPVIntervalTensors.lean b/ComplexityTests/HPVIntervalTensors.lean new file mode 100644 index 0000000000..aceca68168 --- /dev/null +++ b/ComplexityTests/HPVIntervalTensors.lean @@ -0,0 +1,106 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalTensor + +/-! Views, embeddings and interval steps of a concrete choice-string run, with blocks of +length `2`. -/ + +namespace ComplexityTests.HPVIntervalTensors + +open Turing MultiTapeMachine + +/-- On one work tape, write the coin and move right on `true`, left on `false`. The input head +moves right on `true` too. -/ +private def zigzag : MultiTapePTM 1 Bool Unit where + initial := () + tr _ _ _ _ bit := .step + { inputTape := if bit then 1 else 0, + workTapes := fun _ => (some (some bit), if bit then 1 else -1), + output := none, state := some () } + Empty.elim Empty.elim + +/-- Replays on upstream configurations, evaluated through the computable interpreter. -/ +private theorem stepCoins_eq (coins : List Bool) (cfg : Cfg 1 Bool Unit [true, false]) : + zigzag.stepCoins coins cfg = + (zigzag.runClosedConfigFromCoins coins { tapes := cfg }).tapes := + (MultiTapePTM.tapes_runClosedConfigFromCoins zigzag coins { tapes := cfg }).symm + +private def start : Cfg 1 Bool Unit [true, false] := Cfg.init () [true, false] + +/-! ### Embedding a view keeps the window and forgets the rest -/ + +/-- The start configuration with marks in its window `[-2, 4)` (cell `3`) and outside it +(cell `5`). -/ +private def marked : Cfg 1 Bool Unit [true, false] := + { start with workTapes := fun _ z => if z = 3 ∨ z = 5 then some false else none } + +/-- The configuration embedded from the view of `marked`. -/ +private noncomputable def markedView : Cfg 1 Bool Unit [true, false] := + embedCfg 2 (marked.blockIndex 2) (marked.blockControl 2) + (marked.windowContents 2 (marked.blockIndex 2)) + +-- The mark in the window is kept. +example : markedView.workTapes 0 3 = some false := + (agreeOn_embedCfg_view marked).workTapes_eq 0 3 (by simp [Cfg.blockWindow, marked, start]) + +-- The mark outside the window is forgotten: block `2` is not part of the view. +example : markedView.workTapes 0 5 = none := by + simp only [markedView, embedCfg, windowCell] + rw [dite_eq_right (by decide)] + +/-! ### Interval steps -/ + +/-- After `true, true` both heads have moved two cells to the right. -/ +private noncomputable def after : Cfg 1 Bool Unit [true, false] := + zigzag.stepCoins [true, true] start + +private theorem headPos_after : after.headPos = fun _ => 2 := by + funext head + cases head <;> (rw [after, stepCoins_eq]; rfl) + +-- The interval wrote `true` into cells `0` and `1`: offsets `0` and `1` of the middle block. +example : after.windowContents 2 (start.blockIndex 2) 0 1 = fun _ => some true := by + funext r + fin_cases r <;> (rw [after, stepCoins_eq]; rfl) + +/-- Both heads move one block to the right. -/ +private theorem blockIndex_after (head : Option (Fin 1)) : + after.blockIndex 2 head = start.blockIndex 2 head + ((1 : SignType) : ℤ) := by + simp only [Cfg.blockIndex, headPos_after, Cfg.headPos_init, start] + rfl + +-- From the view of `start`, the interval step on `true, true` leaves the record and window of +-- the true replay and moves both blocks by `+1`. +example : zigzag.IntervalStep 2 [true, false] (start.blockIndex 2) (fun _ => 1) + (start.blockControl 2) (start.windowContents 2 (start.blockIndex 2)) [true, true] + (after.blockControl 2) (after.windowContents 2 (start.blockIndex 2)) := + (zigzag.intervalStep_view_iff 2 start (by decide) _ _ _).mpr ⟨rfl, rfl, blockIndex_after⟩ + +-- The schedule entry is checked: the step does not keep the work head in its block. +example : ¬ zigzag.IntervalStep 2 [true, false] (start.blockIndex 2) (fun _ => 0) + (start.blockControl 2) (start.windowContents 2 (start.blockIndex 2)) [true, true] + (after.blockControl 2) (after.windowContents 2 (start.blockIndex 2)) := by + rw [zigzag.intervalStep_view_iff 2 start (by decide)] + rintro ⟨-, -, h⟩ + have := (h (some 0)).symm.trans (blockIndex_after (some 0)) + simp at this + +/-- An entry of the interval tensor counts at most the `4` bit strings of the interval. -/ +example : zigzag.intervalCount 2 [true, false] (start.blockIndex 2) (fun _ => 1) + (start.blockControl 2) (start.windowContents 2 (start.blockIndex 2)) + (after.blockControl 2) (after.windowContents 2 (start.blockIndex 2)) ≤ 4 := + zigzag.intervalCount_le 2 _ _ _ _ _ _ _ + +/-! ### Bits of an interval -/ + +-- With two intervals of two bits, interval `1` replays bits `2` and `3`. +example (y : Fin (2 * 2) → Bool) : + zigzag.intervalStart 2 (List.ofFn y) start 2 = + zigzag.stepCoins [y 2, y 3] (zigzag.intervalStart 2 (List.ofFn y) start 1) := by + exact zigzag.intervalStart_succ_ofFn y start 1 + +end ComplexityTests.HPVIntervalTensors From e84e948852ef1c9e8d94e9b3d5f5f0f12df35f72 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:53:02 -0400 Subject: [PATCH 8/9] feat(machines): block-counting tensor networks (#1833 H3, Lemma 2.2) The tensor network of a movement schedule: one vertex per interval and a sink per edge, control-record and block-content edges from each interval to the next interval whose window holds that block, and the interval tensors of the previous commit. Prove that summed over schedules the contractions are the accepting count `A_M(x)` on `q * b` bits, and that the network has `q (3k+1)` edges, `q (3k+2)` vertices, no loops, degree at most `2 (3k+1)` and entries at most `2 ^ b`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../MultiTape/Probabilistic/BlockNetwork.lean | 844 ++++++++++++++++++ ComplexityTests/HPVBlockNetwork.lean | 55 ++ 3 files changed, 900 insertions(+) create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/BlockNetwork.lean create mode 100644 ComplexityTests/HPVBlockNetwork.lean diff --git a/Complexity.lean b/Complexity.lean index 6d065c46bf..edb6e44788 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1804,6 +1804,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.WhileI public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.AcceptCount +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.BlockNetwork public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Blocks public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Clock public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Closed diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/BlockNetwork.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/BlockNetwork.lean new file mode 100644 index 0000000000..32b9261096 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/BlockNetwork.lean @@ -0,0 +1,844 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalTensor +public import Complexity.Computability.Circuit.Frontier.TensorNetwork +import Mathlib.Algebra.BigOperators.GroupWithZero.Finset +import Mathlib.Algebra.BigOperators.Ring.Finset +import Mathlib.Data.Fintype.Sum + +/-! +# Block-counting tensor networks + +The block-counting identity, Lemma 2.2 of the note *Deterministic simulations of +nondeterministic and randomized time* (30 October 2026) formalized in issue #1833. Fix a closed +fair-coin table `machine` over `Bool`, an input, a block length `b > 0` and a movement schedule +`σ` of `q > 0` intervals (`Turing.MultiTapePTM.Schedule`). The tensor network +`Turing.MultiTapePTM.blockNetwork` counts the accepting choice strings of `q * b` bits whose run +has schedule `σ` (`Turing.MultiTapePTM.contraction_blockNetwork`), so summing over the schedules +gives the accepting count `A_M(x)` (`Turing.MultiTapePTM.sum_contraction_blockNetwork`). The proof +idea is original to that note, building on the blocking of Hopcroft, Paul and Valiant +[HopcroftPaulValiant1977] (compare [Williams2025], Lemma 2.1 and §3.2). + +**The network.** The schedule fixes the block index of every head at the start of every interval +(`Turing.MultiTapePTM.scheduleBlock`), and hence the window of three blocks around each work head. + +* There is one vertex for each interval `i`, and one *sink* vertex for each edge. +* Every edge leaves an interval (`Turing.MultiTapePTM.BlockEdge`): the edge `.inl i` carries the + control record leaving interval `i`, and the edge `.inr (i, h, d)` the contents of block + `scheduleBlock σ i h + d - 1` of work tape `h` leaving interval `i`. Its target is the next + interval whose window contains that block, or the next interval for a control record; when + there is none, it ends at its sink. +* The tensor of interval `i` is the interval tensor of + `Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalTensor`: the number of + bit strings `u ∈ {0,1}^b` taking the entering record and window to the leaving ones and moving + every block as `σ i` prescribes. The entering record comes from the control edge of interval + `i - 1`, or is the initial record for `i = 0`. The entering contents of a block come from the + previous interval whose window contains it, or are blank when there is none. +* The sink of the last control edge accepts exactly the records whose output track is `accept`; + every other sink is the constant `1`. + +Edges carry letters of `Turing.MultiTapePTM.BlockLetter`, a control record or the contents of a +block. A letter of the wrong kind on an edge gives weight zero, because the interval leaving +it requires the right kind. + +**The identity.** Expanding every interval tensor as a sum over its bit strings writes the +contraction as a sum over `q` strings of `b` bits, that is over choice strings of `q * b` bits. +For a fixed choice string, induction over the intervals shows that an assignment of letters with +nonzero weight is forced to be the true run's: the control records and the window contents of +the true run at the end of each interval, and the run is forced to follow `σ`. Between two +appearances of a block in windows, the block is untouched +(`Turing.MultiTapePTM.workTapes_intervalStart_eq_of_notMem_blockWindow`), and within an interval +the embedded window is matched to the true run (`Turing.MultiTapePTM.intervalStep_view_iff`). +Conversely the true run's letters have weight one exactly when the run has schedule `σ` and +accepts. + +**Size.** The network has `q * (3 k + 1)` edges and `q * (3 k + 2)` vertices, no loops, maximum +degree at most `2 * (3 k + 1)`, and entries at most `2 ^ b`. Its letters have `O(b)` bits, so +binarizing (`Cslib.Circuits.Frontier.TensorNetwork.binarize`) and subdividing it gives a +bipartite Boolean network with `O(q b)` edges and degree `O(b)`, as in the note. + +## Main definitions + +* `Turing.MultiTapePTM.scheduleBlock`: block indices prescribed by a schedule. +* `Turing.MultiTapePTM.InWindow`, `Turing.MultiTapePTM.portBlock`, `Turing.MultiTapePTM.portOf`: + windows and window entries under a schedule. +* `Turing.MultiTapePTM.BlockEdge`, `Turing.MultiTapePTM.BlockLetter`: edges and letters. +* `Turing.MultiTapePTM.inControl`, `Turing.MultiTapePTM.inWindow`, + `Turing.MultiTapePTM.IntervalHolds`, `Turing.MultiTapePTM.edgeTarget`: the entering record and + window of an interval, its condition, and the targets of edges. +* `Turing.MultiTapePTM.blockNetwork`: the block-counting network of a schedule. + +## Main results + +* `Turing.MultiTapePTM.blockIndex_intervalStart_eq_scheduleBlock`: a run following `σ` has the + block indices of `σ`. +* `Turing.MultiTapePTM.contraction_blockNetwork`: the network of `σ` counts the accepting choice + strings with schedule `σ`. +* `Turing.MultiTapePTM.sum_contraction_blockNetwork`: summed over the `3 ^ ((k + 1) * q)` + schedules, the contractions give the accepting count. +* `Turing.MultiTapePTM.card_blockEdge`, `Turing.MultiTapePTM.card_blockVertex`, + `Turing.MultiTapePTM.loopless_blockNetwork`, `Turing.MultiTapePTM.maxDegreeLE_blockNetwork`, + `Turing.MultiTapePTM.tensor_blockNetwork_le`: size, degree and entry bounds. + +## References + +* [J. Hopcroft, W. Paul, L. Valiant, *On Time Versus Space*][HopcroftPaulValiant1977] +* [R. Williams, *Simulating Time With Square-Root Space*][Williams2025] +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.1 (p. 53) +-/ + +public section + +namespace Turing.MultiTapePTM + +open Cslib.Circuits.Frontier MultiTapeNTM.ChoiceTable + +variable {k q : ℕ} {State : Type} + +/-! ### Block indices prescribed by a schedule -/ + +/-- The block index of every head at the start of interval `i` under the schedule `σ`, when every +head starts in block `0`: the sum of the entries of `σ` for the intervals before `i`. -/ +@[expose] def scheduleBlock (σ : Schedule k q) : ℕ → Option (Fin k) → ℤ + | 0 => fun _ => 0 + | i + 1 => fun head => scheduleBlock σ i head + if hi : i < q then (σ ⟨i, hi⟩ head : ℤ) else 0 + +@[simp] theorem scheduleBlock_zero (σ : Schedule k q) : scheduleBlock σ 0 = fun _ => 0 := rfl + +theorem scheduleBlock_succ (σ : Schedule k q) {i : ℕ} (hi : i < q) (head : Option (Fin k)) : + scheduleBlock σ (i + 1) head = scheduleBlock σ i head + (σ ⟨i, hi⟩ head : ℤ) := by + simp only [scheduleBlock, dite_eq_left hi] + +/-- **A run following `σ` has the block indices of `σ`.** If the run replaying `coins` from the +start has schedule entries `σ j` for the intervals `j < i`, it starts interval `i` with the block +indices `scheduleBlock σ i`. -/ +theorem blockIndex_intervalStart_eq_scheduleBlock (machine : MultiTapePTM k Bool State) + {input : List Bool} (b : ℕ) [NeZero b] (coins : List Bool) (σ : Schedule k q) {i : ℕ} + (hi : i ≤ q) + (hσ : ∀ j : Fin q, j.val < i → + machine.schedule b q coins (Cfg.init machine.initial input) j = σ j) : + (machine.intervalStart b coins (Cfg.init machine.initial input) i).blockIndex b = + scheduleBlock σ i := by + induction i with + | zero => + funext head + rw [intervalStart_zero, Cfg.blockIndex, Cfg.headPos_init, Int.zero_ediv] + rfl + | succ i ih => + funext head + have hiq : i < q := by omega + have hstep := machine.coe_schedule (Nat.pos_of_neZero b) q coins + (Cfg.init machine.initial input) ⟨i, hiq⟩ head + rw [hσ ⟨i, hiq⟩ (by simp)] at hstep + have hprev := congrFun (ih (by omega) fun j hj => hσ j (by omega)) head + simp only [Cfg.blockIndex] at hprev ⊢ + rw [scheduleBlock_succ σ hiq] + simp only at hstep + omega + +/-! ### Appearances of a block in windows -/ + +/-- The first index after `i` satisfying `p`, if any. -/ +private def firstAfter (p : Fin q → Prop) [DecidablePred p] (i : Fin q) : Option (Fin q) := + if h : (Finset.univ.filter fun i' => i < i' ∧ p i').Nonempty then + some ((Finset.univ.filter fun i' => i < i' ∧ p i').min' h) + else none + +/-- The last index before `i` satisfying `p`, if any. -/ +private def lastBefore (p : Fin q → Prop) [DecidablePred p] (i : Fin q) : Option (Fin q) := + if h : (Finset.univ.filter fun i' => i' < i ∧ p i').Nonempty then + some ((Finset.univ.filter fun i' => i' < i ∧ p i').max' h) + else none + +private theorem firstAfter_eq_some_iff {p : Fin q → Prop} [DecidablePred p] {i i' : Fin q} : + firstAfter p i = some i' ↔ i < i' ∧ p i' ∧ ∀ j, i < j → j < i' → ¬ p j := by + unfold firstAfter + split_ifs with h + · rw [Option.some_inj] + constructor + · rintro rfl + have hmem := Finset.mem_filter.mp (Finset.min'_mem _ h) + refine ⟨hmem.2.1, hmem.2.2, fun j hj hjlt hpj => ?_⟩ + exact absurd (Finset.min'_le _ j (by simp [hj, hpj])) (not_le.mpr hjlt) + · rintro ⟨hlt, hp, hmin⟩ + refine le_antisymm (Finset.min'_le _ _ (by simp [hlt, hp])) ?_ + have hmem := Finset.mem_filter.mp (Finset.min'_mem _ h) + by_contra hcon + exact hmin _ hmem.2.1 (not_le.mp hcon) hmem.2.2 + · simp only [false_iff] + rintro ⟨hlt, hp, -⟩ + exact h ⟨i', by simp [hlt, hp]⟩ + +private theorem lastBefore_eq_some_iff {p : Fin q → Prop} [DecidablePred p] {i i' : Fin q} : + lastBefore p i = some i' ↔ i' < i ∧ p i' ∧ ∀ j, i' < j → j < i → ¬ p j := by + unfold lastBefore + split_ifs with h + · rw [Option.some_inj] + constructor + · rintro rfl + have hmem := Finset.mem_filter.mp (Finset.max'_mem _ h) + refine ⟨hmem.2.1, hmem.2.2, fun j hj hjlt hpj => ?_⟩ + exact absurd (Finset.le_max' _ j (by simp [hjlt, hpj])) (not_le.mpr hj) + · rintro ⟨hlt, hp, hmax⟩ + refine le_antisymm ?_ (Finset.le_max' _ _ (by simp [hlt, hp])) + have hmem := Finset.mem_filter.mp (Finset.max'_mem _ h) + by_contra hcon + exact hmax _ (not_le.mp hcon) hmem.2.1 hmem.2.2 + · simp only [false_iff] + rintro ⟨hlt, hp, -⟩ + exact h ⟨i', by simp [hlt, hp]⟩ + +private theorem lastBefore_eq_none_iff {p : Fin q → Prop} [DecidablePred p] {i : Fin q} : + lastBefore p i = none ↔ ∀ j, j < i → ¬ p j := by + unfold lastBefore + split_ifs with h + · simp only [false_iff, not_forall, not_not] + obtain ⟨j, hj⟩ := h + exact ⟨j, (Finset.mem_filter.mp hj).2.1, (Finset.mem_filter.mp hj).2.2⟩ + · simp only [true_iff] + intro j hj hp + exact h ⟨j, by simp [hj, hp]⟩ + +/-- Consecutive appearances: the last appearance before `i` has `i` as its next appearance. -/ +private theorem firstAfter_of_lastBefore {p : Fin q → Prop} [DecidablePred p] {i i' : Fin q} + (hi : p i) (h : lastBefore p i = some i') : firstAfter p i' = some i := by + obtain ⟨hlt, -, hbetween⟩ := lastBefore_eq_some_iff.mp h + exact firstAfter_eq_some_iff.mpr ⟨hlt, hi, hbetween⟩ + +private theorem lastBefore_of_firstAfter {p : Fin q → Prop} [DecidablePred p] {i i' : Fin q} + (hi' : p i') (h : firstAfter p i' = some i) : lastBefore p i = some i' := by + obtain ⟨hlt, -, hbetween⟩ := firstAfter_eq_some_iff.mp h + exact lastBefore_eq_some_iff.mpr ⟨hlt, hi', hbetween⟩ + +/-- Block `j` of work tape `h` lies in the window of interval `i` under `σ`. -/ +abbrev InWindow (σ : Schedule k q) (h : Fin k) (j : ℤ) (i : Fin q) : Prop := + |scheduleBlock σ i (some h) - j| ≤ 1 + +/-- The block of the window entry `d` of work tape `h` in interval `i`. -/ +@[expose] def portBlock (σ : Schedule k q) (i : Fin q) (h : Fin k) (d : Fin 3) : ℤ := + scheduleBlock σ i (some h) + d - 1 + +/-- The window entry of block `j` of work tape `h` in interval `i`. -/ +@[expose] def portOf (σ : Schedule k q) (i : Fin q) (h : Fin k) (j : ℤ) : Fin 3 := + ⟨(j - scheduleBlock σ i (some h) + 1).toNat % 3, Nat.mod_lt _ (by norm_num)⟩ + +theorem portBlock_portOf {σ : Schedule k q} {i : Fin q} {h : Fin k} {j : ℤ} + (hj : InWindow σ h j i) : portBlock σ i h (portOf σ i h j) = j := by + simp only [InWindow, abs_le] at hj + simp only [portBlock, portOf] + omega + +theorem inWindow_portBlock (σ : Schedule k q) (i : Fin q) (h : Fin k) (d : Fin 3) : + InWindow σ h (portBlock σ i h d) i := by + have := d.isLt + simp only [InWindow, portBlock, abs_le] + omega + +/-! ### The network -/ + +/-- The edges of a block-counting network of `q` intervals: `.inl i` carries the control record +leaving interval `i`, and `.inr (i, h, d)` the contents of window entry `d` of work tape `h` +leaving interval `i`. -/ +abbrev BlockEdge (k q : ℕ) := Fin q ⊕ (Fin q × Fin k × Fin 3) + +/-- The letters on the edges: a control record or the contents of a block. -/ +abbrev BlockLetter (k : ℕ) (State : Type) (b : ℕ) := + BlockControl k State b ⊕ (ZMod b → Option Bool) + +variable {b : ℕ} + +/-- The control record of a letter, or a default for block contents. -/ +@[expose] def BlockLetter.control : BlockLetter k State b → BlockControl k State b + | .inl c => c + | .inr _ => (none, 0, .empty) + +/-- The block contents of a letter, or blank for a control record. -/ +@[expose] def BlockLetter.contents : BlockLetter k State b → ZMod b → Option Bool + | .inl _ => fun _ => none + | .inr w => w + +/-- The weight of the last control record: one when its output track is `accept`. -/ +@[expose] def acceptWeight : BlockLetter k State b → ℕ + | .inl c => if c.2.2 = .accept then 1 else 0 + | .inr _ => 0 + +variable (machine : MultiTapePTM k Bool State) (input : List Bool) (b : ℕ) [NeZero b] + (σ : Schedule k q) + +/-- The control record entering interval `i`: the initial record for `i = 0`, and otherwise the +letter on the control edge leaving interval `i - 1`. -/ +@[expose] def inControl (i : Fin q) (x : BlockEdge k q → BlockLetter k State b) : + BlockControl k State b := + if hi : i.val = 0 then (some machine.initial, 0, .empty) + else (x (.inl ⟨i - 1, by omega⟩)).control + +variable {b} in +/-- The window contents entering interval `i`: each block is read from the edge leaving the +previous interval whose window contains it, and is blank if there is none. -/ +def inWindow (i : Fin q) (x : BlockEdge k q → BlockLetter k State b) : + Fin k → Fin 3 → ZMod b → Option Bool := fun h d => + (lastBefore (InWindow σ h (portBlock σ i h d)) i).elim (fun _ => none) fun i' => + (x (.inr (i', h, portOf σ i' h (portBlock σ i h d)))).contents + +/-- The edge condition at interval `i` for the bits `u`: an interval step from the entering +record and window to the letters on the edges leaving `i`, which must be of the right kinds, +moving the blocks as `σ i` prescribes. -/ +def IntervalHolds (i : Fin q) (x : BlockEdge k q → BlockLetter k State b) (u : Fin b → Bool) : + Prop := + ∃ cOut wOut, machine.IntervalStep b input (scheduleBlock σ i) (σ i) + (machine.inControl b i x) (inWindow σ i x) (List.ofFn u) cOut wOut ∧ + x (.inl i) = .inl cOut ∧ ∀ h d, x (.inr (i, h, d)) = .inr (wOut h d) + +/-- The target of an edge: the interval reading it next, or its sink. -/ +def edgeTarget : BlockEdge k q → Fin q ⊕ BlockEdge k q + | .inl i => if hi : i.val + 1 < q then .inl ⟨i + 1, hi⟩ else .inr (.inl i) + | .inr (i, h, d) => + (firstAfter (InWindow σ h (portBlock σ i h d)) i).elim (.inr (.inr (i, h, d))) .inl + +/-- The interval `i ≠ 0` reads the control edge of interval `i - 1`. -/ +private theorem edgeTarget_inl_pred {i : Fin q} (hi : i.val ≠ 0) : + edgeTarget σ (.inl ⟨i - 1, by omega⟩) = .inl i := by + simp only [edgeTarget] + rw [dite_eq_left (by omega)] + congr 1 + ext + simp only + omega + +/-- Interval `i` reads the block edges of the previous appearances of its window blocks. -/ +private theorem edgeTarget_inWindow {i i' : Fin q} {h : Fin k} {d : Fin 3} + (hi' : lastBefore (InWindow σ h (portBlock σ i h d)) i = some i') : + edgeTarget σ (.inr (i', h, portOf σ i' h (portBlock σ i h d))) = .inl i := by + have hin : InWindow σ h (portBlock σ i h d) i' := (lastBefore_eq_some_iff.mp hi').2.1 + simp only [edgeTarget, portBlock_portOf hin, + firstAfter_of_lastBefore (inWindow_portBlock σ i h d) hi', Option.elim_some] + +omit [NeZero b] in +/-- Interval `i` only reads the edges at it. -/ +private theorem intervalHolds_congr {i : Fin q} {x y : BlockEdge k q → BlockLetter k State b} + (hxy : ∀ e, Sum.inl i = edgeTarget σ e ∨ e.elim id Prod.fst = i → x e = y e) + (u : Fin b → Bool) : + machine.IntervalHolds input b σ i x u ↔ machine.IntervalHolds input b σ i y u := by + have hcontrol : machine.inControl b i x = machine.inControl b i y := by + unfold inControl + split_ifs with hi + · rfl + · rw [hxy _ (Or.inl (edgeTarget_inl_pred σ hi).symm)] + have hwindow : inWindow σ i x = inWindow σ i y := by + funext h d + unfold inWindow + cases hlast : lastBefore (InWindow σ h (portBlock σ i h d)) i with + | none => rfl + | some i' => + simp only [Option.elim_some] + rw [hxy _ (Or.inl (edgeTarget_inWindow σ hlast).symm)] + have hctrl : x (.inl i) = y (.inl i) := hxy _ (Or.inr rfl) + have hblock : ∀ h d, x (.inr (i, h, d)) = y (.inr (i, h, d)) := fun h d => hxy _ (Or.inr rfl) + simp only [IntervalHolds, hcontrol, hwindow, hctrl, hblock] + +open scoped Classical in +/-- **The block-counting network** of the schedule `σ`. It has a vertex for every interval +(`.inl i`) and a sink for every edge (`.inr e`). Every edge `e` leaves its interval and ends at +`edgeTarget σ e`. The tensor of interval `i` counts the bit strings `u ∈ {0,1}^b` for which +`IntervalHolds` holds; the sink of the last control edge requires the output track `accept`, and +every other sink is `1`. -/ +noncomputable def blockNetwork : + TensorNetwork ℕ (BlockLetter k State b) (Fin q ⊕ BlockEdge k q) (BlockEdge k q) where + src e := .inl (e.elim id Prod.fst) + tgt := edgeTarget σ + tensor + | .inl i, x => (Finset.univ.filter fun u => machine.IntervalHolds input b σ i x u).card + | .inr (.inl i), x => if i.val + 1 = q then acceptWeight (x (.inl i)) else 1 + | .inr (.inr _), _ => 1 + tensor_congr := by + rintro (i | (i | e)) x y h + · simp only + congr 1 + ext u + simp only [Finset.mem_filter, Finset.mem_univ, true_and] + refine machine.intervalHolds_congr input b σ (fun e he => h e ?_) u + rcases he with he | he + · exact Or.inr he.symm + · exact Or.inl (congrArg Sum.inl he) + · simp only + split_ifs with hi + · rw [h (.inl i) (Or.inr ?_)] + simp only [edgeTarget] + rw [dite_eq_right (by omega)] + · rfl + · rfl + +/-! ### The counting identity -/ + +section Identity + +variable {machine input b σ} + +/-- The configuration of the run replaying `y` from the start at the start of interval `i`. -/ +private noncomputable abbrev trueRun (machine : MultiTapePTM k Bool State) (input : List Bool) + (b : ℕ) (y : Fin (q * b) → Bool) (i : ℕ) : Cfg k Bool State input := + machine.intervalStart b (List.ofFn y) (Cfg.init machine.initial input) i + +/-- The interval bits of a choice string: `y` split into `q` strings of `b` bits. -/ +private def intervalBits : (Fin (q * b) → Bool) ≃ (Fin q → Fin b → Bool) := + (finProdFinEquiv.arrowCongr (Equiv.refl Bool)).symm.trans (Equiv.curry _ _ _) + +omit [NeZero b] in +private theorem intervalBits_apply (y : Fin (q * b) → Bool) (i : Fin q) : + intervalBits y i = fun r => y (finProdFinEquiv (i, r)) := rfl + +/-- The letters of the true run: the control records and window contents at the end of every +interval. -/ +private noncomputable def trueLetters (machine : MultiTapePTM k Bool State) (input : List Bool) + (σ : Schedule k q) (y : Fin (q * b) → Bool) : BlockEdge k q → BlockLetter k State b + | .inl i => .inl ((trueRun machine input b y (i + 1)).blockControl b) + | .inr (i, h, d) => + .inr ((trueRun machine input b y (i + 1)).windowContents b + (scheduleBlock σ i) h d) + +/-- `x` agrees with the true run on the edges leaving the intervals before `i`, and the run +follows `σ` there. -/ +private def AgreesBefore (machine : MultiTapePTM k Bool State) (input : List Bool) + (σ : Schedule k q) (y : Fin (q * b) → Bool) (x : BlockEdge k q → BlockLetter k State b) + (i : ℕ) : Prop := + ∀ j : Fin q, j.val < i → + machine.schedule b q (List.ofFn y) (Cfg.init machine.initial input) j = σ j ∧ + x (.inl j) = trueLetters machine input σ y (.inl j) ∧ + ∀ h d, x (.inr (j, h, d)) = trueLetters machine input σ y (.inr (j, h, d)) + +omit [NeZero b] in +/-- The control record of the start configuration. -/ +private theorem blockControl_init (q₀ : State) : + (Cfg.init q₀ input : Cfg k Bool State input).blockControl b = (some q₀, 0, .empty) := by + have h : ∀ head, ((Cfg.init q₀ input : Cfg k Bool State input).headPos head : ZMod b) = 0 := + fun head => by rw [Cfg.headPos_init, Int.cast_zero] + rw [Cfg.blockControl, funext h] + rfl + +/-- A work-tape cell of a block outside the window of a configuration is outside its three +blocks. -/ +private theorem notMem_blockWindow {c : Cfg k Bool State input} {h : Fin k} {j : ℤ} + (hj : ¬ |c.blockIndex b (some h) - j| ≤ 1) (r : ZMod b) : + b * j + (r.val : ℤ) ∉ c.blockWindow b h := by + have hb : (0 : ℤ) < b := by exact_mod_cast Nat.pos_of_neZero b + have hr : (r.val : ℤ) < b := by exact_mod_cast ZMod.val_lt r + have hr0 : (0 : ℤ) ≤ r.val := by positivity + simp only [Cfg.blockIndex, Cfg.headPos_some, abs_le, not_and_or, not_le] at hj + simp only [Cfg.blockWindow, Set.mem_Ico, not_and_or, not_le, not_lt] + rcases hj with hj | hj + · right + nlinarith + · left + nlinarith + +/-- **The entering view is the true one.** If `x` agrees with the true run before interval `i`, +then interval `i` reads the true control record and window contents, at the true block +indices. -/ +private theorem inView_eq (y : Fin (q * b) → Bool) {x : BlockEdge k q → BlockLetter k State b} + {i : Fin q} (hx : AgreesBefore machine input σ y x i) : + scheduleBlock σ i = (trueRun machine input b y i).blockIndex b ∧ + machine.inControl b i x = (trueRun machine input b y i).blockControl b ∧ + inWindow σ i x = (trueRun machine input b y i).windowContents b + (scheduleBlock σ i) := by + have hindex : ∀ i' : ℕ, i' ≤ i → + (trueRun machine input b y i').blockIndex b = scheduleBlock σ i' := + fun i' hi' => machine.blockIndex_intervalStart_eq_scheduleBlock b _ σ (by omega) + fun j hj => (hx j (by omega)).1 + refine ⟨(hindex i le_rfl).symm, ?_, ?_⟩ + · -- The control record. + unfold inControl + split_ifs with hi + · have : (i : ℕ) = 0 := hi + rw [trueRun, this, intervalStart_zero, blockControl_init] + · rw [(hx ⟨i - 1, by omega⟩ (by simp; omega)).2.1] + simp only [trueLetters, BlockLetter.control] + congr 3 + omega + · -- The window contents: the last appearance before `i`, untouched since. + funext h d r + set j := portBlock σ i h d + have huntouched : ∀ i₁ : ℕ, i₁ ≤ i → (∀ i'' : Fin q, i₁ ≤ i'' → i'' < i → + ¬ InWindow σ h j i'') → + (trueRun machine input b y i).workTapes h (b * j + r.val) = + (trueRun machine input b y i₁).workTapes h (b * j + r.val) := by + intro i₁ hi₁ hnot + refine machine.workTapes_intervalStart_eq_of_notMem_blockWindow (Nat.pos_of_neZero b) + _ _ hi₁ fun i'' hi'' hi''i => notMem_blockWindow ?_ r + rw [hindex i'' hi''i.le] + exact hnot ⟨i'', by omega⟩ hi'' hi''i + change (inWindow σ i x h d) r = (trueRun machine input b y i).workTapes h (b * j + r.val) + unfold inWindow + cases hlast : lastBefore (InWindow σ h j) i with + | none => + simp only [Option.elim_none] + rw [huntouched 0 (Nat.zero_le _) fun i'' _ hi'' => + lastBefore_eq_none_iff.mp hlast i'' hi'', trueRun, intervalStart_zero] + rfl + | some i' => + obtain ⟨hlt, hin, hbetween⟩ := lastBefore_eq_some_iff.mp hlast + simp only [Option.elim_some] + rw [(hx i' hlt).2.2, huntouched (i' + 1) hlt fun i'' h₁ h₂ => hbetween i'' h₁ h₂] + change (trueRun machine input b y (i' + 1)).workTapes h + (b * portBlock σ i' h (portOf σ i' h j) + r.val) = _ + rw [portBlock_portOf hin] + +/-- `SignType` casts to `ℤ` injectively. -/ +private theorem signType_cast_inj {s t : SignType} (h : (s : ℤ) = t) : s = t := by + cases s <;> cases t <;> first | rfl | (simp at h) + +/-- **The condition at an interval, on the true view.** If interval `i` reads the true view, its +condition holds exactly when the letters it leaves are the true ones and the run follows +`σ i`. -/ +private theorem intervalHolds_iff (y : Fin (q * b) → Bool) + {x : BlockEdge k q → BlockLetter k State b} {i : Fin q} + (hindex : scheduleBlock σ i = (trueRun machine input b y i).blockIndex b) + (hcontrol : machine.inControl b i x = + (trueRun machine input b y i).blockControl b) + (hwindow : inWindow σ i x = (trueRun machine input b y i).windowContents b + (scheduleBlock σ i)) : + machine.IntervalHolds input b σ i x (fun r => y (finProdFinEquiv (i, r))) ↔ + machine.schedule b q (List.ofFn y) (Cfg.init machine.initial input) i = σ i ∧ + x (.inl i) = trueLetters machine input σ y (.inl i) ∧ + ∀ h d, x (.inr (i, h, d)) = trueLetters machine input σ y (.inr (i, h, d)) := by + have hnext := machine.intervalStart_succ_ofFn y (Cfg.init machine.initial input) i + rw [IntervalHolds, hcontrol, hwindow, hindex] + simp only [machine.intervalStep_view_iff b _ (List.length_ofFn (f := _)).le] + rw [← hnext] + have hsched : machine.schedule b q (List.ofFn y) (Cfg.init machine.initial input) i = σ i ↔ + ∀ head, (trueRun machine input b y (i + 1)).blockIndex b head = + (trueRun machine input b y i).blockIndex b head + σ i head := by + rw [funext_iff] + refine forall_congr' fun head => ?_ + have := machine.coe_schedule (Nat.pos_of_neZero b) q (List.ofFn y) + (Cfg.init machine.initial input) i head + simp only [Cfg.blockIndex, trueRun] + constructor + · intro h + rw [← h] + omega + · intro h + exact signType_cast_inj (by omega) + simp only [trueLetters, ← hindex, hsched] + constructor + · rintro ⟨cOut, wOut, ⟨rfl, rfl, hmove⟩, hc, hw⟩ + exact ⟨hmove, hc, hw⟩ + · rintro ⟨hmove, hc, hw⟩ + exact ⟨_, _, ⟨rfl, rfl, hmove⟩, hc, hw⟩ + +/-- Satisfying the conditions of all intervals forces agreement with the true run. -/ +private theorem agreesBefore_of_forall (y : Fin (q * b) → Bool) + {x : BlockEdge k q → BlockLetter k State b} + (hx : ∀ i : Fin q, machine.IntervalHolds input b σ i x (intervalBits y i)) : + ∀ i ≤ q, AgreesBefore machine input σ y x i := by + intro i hi + induction i with + | zero => exact fun j hj => absurd hj (Nat.not_lt_zero _) + | succ i ih => + have hprev := ih (by omega) + intro j hj + rcases Nat.lt_succ_iff_lt_or_eq.mp hj with hj | hj + · exact hprev j hj + · obtain ⟨hindex, hcontrol, hwindow⟩ := inView_eq y (i := j) (fun j' hj' => hprev j' (by omega)) + exact (intervalHolds_iff y hindex hcontrol hwindow).mp (hx j) + +/-- The true letters satisfy all interval conditions exactly when the run follows `σ`. -/ +private theorem forall_intervalHolds_trueLetters_iff (y : Fin (q * b) → Bool) : + (∀ i : Fin q, machine.IntervalHolds input b σ i (trueLetters machine input σ y) + (intervalBits y i)) ↔ + machine.schedule b q (List.ofFn y) (Cfg.init machine.initial input) = σ := by + constructor + · intro h + funext j + exact (agreesBefore_of_forall y h q le_rfl j j.isLt).1 + · intro hσ i + have hagree : AgreesBefore machine input σ y (trueLetters machine input σ y) i := + fun j _ => ⟨congrFun hσ j, rfl, fun _ _ => rfl⟩ + obtain ⟨hindex, hcontrol, hwindow⟩ := inView_eq y hagree + exact (intervalHolds_iff y hindex hcontrol hwindow).mpr ⟨congrFun hσ i, rfl, fun _ _ => rfl⟩ + +omit [NeZero b] in +/-- The run replaying `q * b` bits ends at the start of interval `q`. -/ +private theorem runClosedCoins_eq (y : Fin (q * b) → Bool) : + machine.runClosedCoins (List.ofFn y) input = + (trueRun machine input b y q).output := by + rw [runClosedCoins_eq_output_stepCoins, trueRun, intervalStart, + List.take_of_length_le (by simp)] + +omit [NeZero b] in +/-- Agreeing with the true run before every interval is being the true letters. -/ +private theorem eq_trueLetters_of_agreesBefore (y : Fin (q * b) → Bool) + {x : BlockEdge k q → BlockLetter k State b} (hx : AgreesBefore machine input σ y x q) : + x = trueLetters machine input σ y := by + funext e + rcases e with j | ⟨j, h, d⟩ + · exact (hx j j.isLt).2.1 + · exact (hx j j.isLt).2.2 h d + + +end Identity + +omit [NeZero b] in +/-- The sinks contribute the acceptance check of the last control edge. -/ +private theorem prod_sinks (hq : 0 < q) (x : BlockEdge k q → BlockLetter k State b) : + ∏ e : BlockEdge k q, (machine.blockNetwork input b σ).tensor (.inr e) x = + acceptWeight (x (.inl ⟨q - 1, by omega⟩)) := by + rw [Fintype.prod_sum_type] + have hblock : ∏ e : Fin q × Fin k × Fin 3, + (machine.blockNetwork input b σ).tensor (.inr (.inr e)) x = 1 := + Finset.prod_eq_one fun _ _ => rfl + rw [hblock, mul_one] + rw [Finset.prod_eq_single (⟨q - 1, by omega⟩ : Fin q)] + · change (if q - 1 + 1 = q then _ else 1) = _ + rw [ite_eq_left (by omega)] + · intro i _ hi + change (if i.val + 1 = q then _ else 1) = 1 + rw [ite_eq_right fun h => hi (Fin.ext (by simp only; omega))] + · exact fun h => absurd (Finset.mem_univ _) h + +omit [NeZero b] in +open scoped Classical in +/-- The interval tensors expanded as a sum over the bits of all intervals. -/ +private theorem prod_intervals (x : BlockEdge k q → BlockLetter k State b) : + ∏ i : Fin q, (machine.blockNetwork input b σ).tensor (.inl i) x = + ∑ u : Fin q → Fin b → Bool, + if ∀ i, machine.IntervalHolds input b σ i x (u i) then 1 else 0 := by + have hcard : ∀ i : Fin q, (machine.blockNetwork input b σ).tensor (.inl i) x = + ∑ u : Fin b → Bool, if machine.IntervalHolds input b σ i x u then 1 else 0 := by + intro i + change (Finset.univ.filter fun u => machine.IntervalHolds input b σ i x u).card = _ + rw [Finset.card_filter] + simp only [hcard] + rw [Finset.prod_univ_sum] + simp only [Fintype.piFinset_univ, Fintype.prod_boole] + exact Finset.sum_congr rfl fun u _ => by congr + +/-- **The block-counting identity for one schedule.** The contraction of the network of `σ` is the +number of choice strings of `q * b` bits on which the machine accepts and whose run has movement +schedule `σ`. -/ +theorem contraction_blockNetwork [Fintype State] (hq : 0 < q) : + (machine.blockNetwork input b σ).contraction = + (Finset.univ.filter fun y : Fin (q * b) → Bool => + machine.runClosedCoins (List.ofFn y) input = [true] ∧ + machine.schedule b q (List.ofFn y) (Cfg.init machine.initial input) = σ).card := by + classical + rw [TensorNetwork.contraction] + simp only [Fintype.prod_sum_type, machine.prod_sinks input b σ hq, prod_intervals, + Finset.sum_mul] + rw [Finset.sum_comm, ← (intervalBits (q := q) (b := b)).sum_comp, Finset.card_eq_sum_ones, + Finset.sum_filter] + refine Finset.sum_congr rfl fun y _ => ?_ + rw [Finset.sum_eq_single (trueLetters machine input σ y)] + · -- The true letters weigh one exactly when the run follows `σ` and accepts. + have hlast : trueLetters machine input σ y (.inl ⟨q - 1, by omega⟩) = + .inl ((trueRun machine input b y q).blockControl b) := by + simp only [trueLetters, Nat.sub_add_cancel hq] + by_cases hall : ∀ i : Fin q, + machine.IntervalHolds input b σ i (trueLetters machine input σ y) (intervalBits y i) + · have hσ' := (forall_intervalHolds_trueLetters_iff y).mp hall + rw [ite_eq_left hall, one_mul, hlast, acceptWeight] + refine if_congr ?_ rfl rfl + rw [Cfg.blockControl, OutputTrack.ofWord_eq_accept_iff, runClosedCoins_eq, hσ'] + exact (and_iff_left rfl).symm + · have hσ' := fun h => hall ((forall_intervalHolds_trueLetters_iff y).mpr h) + rw [ite_eq_right hall, zero_mul] + exact (ite_eq_right fun h => hσ' h.2).symm + · -- Any other assignment violates some interval condition. + intro x _ hx + rw [ite_eq_right fun hall => + hx (eq_trueLetters_of_agreesBefore y (agreesBefore_of_forall y hall q le_rfl)), zero_mul] + · exact fun h => absurd (Finset.mem_univ _) h + +/-- **The block-counting identity** (the note's Lemma 2.2, equation (2)). Summed over the +movement schedules of `q > 0` intervals of `b` bits, the contractions of the block-counting +networks are the accepting count on `q * b` bits. -/ +theorem sum_contraction_blockNetwork [Fintype State] (hq : 0 < q) : + ∑ σ : Schedule k q, (machine.blockNetwork input b σ).contraction = + machine.acceptCount input (q * b) := by + rw [machine.acceptCount_eq_sum_card_schedule input b q] + exact Finset.sum_congr rfl fun σ _ => machine.contraction_blockNetwork input b σ hq + +/-! ### Size, degree and entries -/ + +/-- A block-counting network has `q * (3 * k + 1)` edges: one control edge and three block edges +per work tape for each interval. -/ +theorem card_blockEdge : Fintype.card (BlockEdge k q) = q * (3 * k + 1) := by + simp only [Fintype.card_sum, Fintype.card_prod, Fintype.card_fin] + ring + +/-- A block-counting network has `q * (3 * k + 2)` vertices: the intervals and the sinks. -/ +theorem card_blockVertex : Fintype.card (Fin q ⊕ BlockEdge k q) = q * (3 * k + 2) := by + rw [Fintype.card_sum, card_blockEdge, Fintype.card_fin] + ring + +omit [NeZero b] in +/-- Every entry of a block-counting network is at most `2 ^ b`: an interval tensor counts bit +strings of length `b`, and a sink is `0` or `1`. -/ +theorem tensor_blockNetwork_le (v : Fin q ⊕ BlockEdge k q) + (x : BlockEdge k q → BlockLetter k State b) : + (machine.blockNetwork input b σ).tensor v x ≤ 2 ^ b := by + classical + have hone : (1 : ℕ) ≤ 2 ^ b := Nat.one_le_two_pow + rcases v with i | i | e + · change (Finset.univ.filter fun u => machine.IntervalHolds input b σ i x u).card ≤ 2 ^ b + exact (Finset.card_filter_le _ _).trans (by simp) + · change (if i.val + 1 = q then acceptWeight (x (.inl i)) else 1) ≤ 2 ^ b + split_ifs + · rcases x (.inl i) with c | w + · simp only [acceptWeight] + split_ifs <;> omega + · exact Nat.zero_le _ + · exact hone + · exact hone + +omit [NeZero b] in +/-- The source of an edge is its interval. -/ +private theorem blockNetwork_src (e : BlockEdge k q) : + (machine.blockNetwork input b σ).src e = .inl (e.elim id Prod.fst) := rfl + +omit [NeZero b] in +private theorem blockNetwork_tgt (e : BlockEdge k q) : + (machine.blockNetwork input b σ).tgt e = edgeTarget σ e := rfl + +omit [NeZero b] in +/-- Every edge goes forward in time, from its interval to a later interval or to a sink. -/ +private theorem edgeTarget_eq_inl {e : BlockEdge k q} {i : Fin q} + (h : edgeTarget σ e = .inl i) : e.elim id Prod.fst < i := by + rcases e with i' | ⟨i', hd, d⟩ + · simp only [edgeTarget] at h + split_ifs at h with hi + · cases h + simp only [Sum.elim_inl, id_eq, Fin.lt_def] + omega + · simp only [edgeTarget] at h + cases hf : firstAfter (InWindow σ hd (portBlock σ i' hd d)) i' with + | none => simp [hf] at h + | some i'' => + simp only [hf, Option.elim_some, Sum.inl.injEq] at h + subst h + exact (firstAfter_eq_some_iff.mp hf).1 + +omit [NeZero b] in +/-- A block-counting network has no loops. -/ +theorem loopless_blockNetwork : (machine.blockNetwork input b σ).Loopless := by + intro e he + rw [blockNetwork_src, blockNetwork_tgt] at he + exact (edgeTarget_eq_inl σ he.symm).ne rfl + +omit [NeZero b] in +/-- The edges into interval `i` are its entering control edge and one block edge for each window +entry it reads. -/ +private theorem injOn_inEdges (i : Fin q) : + Set.InjOn (fun e : BlockEdge k q => e.elim (fun _ => (none : Option (Fin k × Fin 3))) + fun p => some (p.2.1, portOf σ i p.2.1 (portBlock σ p.1 p.2.1 p.2.2))) + {e | edgeTarget σ e = .inl i} := by + rintro (i₁ | ⟨i₁, h₁, d₁⟩) he₁ (i₂ | ⟨i₂, h₂, d₂⟩) he₂ heq + · -- Two control edges into `i` both leave `i - 1`. + simp only [Set.mem_ofPred_eq, edgeTarget] at he₁ he₂ + split_ifs at he₁ he₂ + cases he₁ + simp only [Sum.inl.injEq, Fin.mk.injEq] at he₂ + congr 1 + exact Fin.ext (by omega) + · simp at heq + · simp at heq + · simp only [Option.some.injEq, Prod.mk.injEq, Sum.elim_inr] at heq + obtain ⟨rfl, hport⟩ := heq + simp only [Set.mem_ofPred_eq, edgeTarget] at he₁ he₂ + -- Both are previous appearances of the same block, read at the same window entry of `i`. + have hf : ∀ {i' : Fin q} {d' : Fin 3}, + (firstAfter (InWindow σ h₁ (portBlock σ i' h₁ d')) i').elim + (Sum.inr (Sum.inr (i', h₁, d'))) Sum.inl = (Sum.inl i : Fin q ⊕ BlockEdge k q) → + firstAfter (InWindow σ h₁ (portBlock σ i' h₁ d')) i' = some i := by + intro i' d' h + cases hc : firstAfter (InWindow σ h₁ (portBlock σ i' h₁ d')) i' with + | none => simp [hc] at h + | some i'' => simp only [hc, Option.elim_some, Sum.inl.injEq] at h; rw [h] + have hf₁ := hf he₁ + have hf₂ := hf he₂ + have hw₁ := (firstAfter_eq_some_iff.mp hf₁).2.1 + have hw₂ := (firstAfter_eq_some_iff.mp hf₂).2.1 + have hj : portBlock σ i₁ h₁ d₁ = portBlock σ i₂ h₁ d₂ := by + rw [← portBlock_portOf hw₁, ← portBlock_portOf hw₂, hport] + have hl₁ := lastBefore_of_firstAfter (inWindow_portBlock σ i₁ h₁ d₁) hf₁ + have hl₂ := lastBefore_of_firstAfter (inWindow_portBlock σ i₂ h₁ d₂) hf₂ + rw [hj] at hl₁ + have hi : i₁ = i₂ := Option.some.inj (hl₁.symm.trans hl₂) + subst hi + have hd : d₁ = d₂ := by + simp only [portBlock] at hj + exact Fin.ext (by omega) + rw [hd] + +omit [NeZero b] in +/-- **The degree bound.** An interval has its `3 k + 1` leaving edges and at most `3 k + 1` +entering edges, and a sink has at most one edge. -/ +theorem maxDegreeLE_blockNetwork : + (machine.blockNetwork input b σ).MaxDegreeLE (2 * (3 * k + 1)) := by + classical + rintro (i | e) + · have hsplit : (machine.blockNetwork input b σ).incidenceSet (.inl i) ⊆ + {e | e.elim id Prod.fst = i} ∪ {e | edgeTarget σ e = .inl i} := by + rintro e (he | he) + · left + rw [blockNetwork_src] at he + exact Sum.inl_injective he + · right + exact he + have hout : {e : BlockEdge k q | e.elim id Prod.fst = i}.ncard ≤ 3 * k + 1 := by + calc {e : BlockEdge k q | e.elim id Prod.fst = i}.ncard + ≤ (Set.range (Sum.elim (fun _ : Unit => (Sum.inl i : BlockEdge k q)) + fun p : Fin k × Fin 3 => Sum.inr (i, p))).ncard := by + refine Set.ncard_le_ncard ?_ (Set.toFinite _) + rintro (i' | ⟨i', h, d⟩) he + · simp only [Set.mem_ofPred_eq, Sum.elim_inl, id_eq] at he + exact ⟨.inl (), by simp [he]⟩ + · simp only [Set.mem_ofPred_eq, Sum.elim_inr] at he + exact ⟨.inr (h, d), by simp [he]⟩ + _ = Nat.card (Unit ⊕ Fin k × Fin 3) := Set.ncard_range_of_injective (by + rintro (_ | p) (_ | p') h <;> simp_all) + _ = 3 * k + 1 := by + simp only [Nat.card_eq_fintype_card, Fintype.card_sum, Fintype.card_unit, + Fintype.card_prod, Fintype.card_fin] + ring + have hin : {e : BlockEdge k q | edgeTarget σ e = .inl i}.ncard ≤ 3 * k + 1 := by + calc {e : BlockEdge k q | edgeTarget σ e = .inl i}.ncard + ≤ (Set.univ : Set (Option (Fin k × Fin 3))).ncard := + Set.ncard_le_ncard_of_injOn _ (fun _ _ => Set.mem_univ _) (injOn_inEdges σ i) + (Set.toFinite _) + _ = 3 * k + 1 := by + rw [Set.ncard_univ, Nat.card_eq_fintype_card, Fintype.card_option, + Fintype.card_prod, Fintype.card_fin, Fintype.card_fin] + ring + calc _ ≤ ({e : BlockEdge k q | e.elim id Prod.fst = i} ∪ + {e | edgeTarget σ e = .inl i}).ncard := Set.ncard_le_ncard hsplit (Set.toFinite _) + _ ≤ _ := Set.ncard_union_le _ _ + _ ≤ 2 * (3 * k + 1) := by omega + · have hsub : (machine.blockNetwork input b σ).incidenceSet (.inr e) ⊆ {e} := by + rintro e' (he' | he') + · rw [blockNetwork_src] at he' + cases he' + · rw [blockNetwork_tgt] at he' + rcases e' with i' | ⟨i', h, d⟩ + · simp only [edgeTarget] at he' + split_ifs at he' + cases he' + rfl + · simp only [edgeTarget] at he' + cases hc : firstAfter (InWindow σ h (portBlock σ i' h d)) i' with + | none => + simp only [hc, Option.elim_none, Sum.inr.injEq] at he' + rw [he'] + rfl + | some i'' => simp [hc] at he' + calc _ ≤ ({e} : Set (BlockEdge k q)).ncard := Set.ncard_le_ncard hsub (Set.toFinite _) + _ = 1 := Set.ncard_singleton e + _ ≤ 2 * (3 * k + 1) := by omega + +end Turing.MultiTapePTM diff --git a/ComplexityTests/HPVBlockNetwork.lean b/ComplexityTests/HPVBlockNetwork.lean new file mode 100644 index 0000000000..5a91e1b268 --- /dev/null +++ b/ComplexityTests/HPVBlockNetwork.lean @@ -0,0 +1,55 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.BlockNetwork + +/-! Block-counting networks of concrete fair-coin machines: summed over schedules, their +contractions are accepting counts computed directly. -/ + +namespace ComplexityTests.HPVBlockNetwork + +open Turing MultiTapeMachine + +/-- Emit the first coin and halt. No work tapes; the input head stays. -/ +private def emitCoin : MultiTapePTM 0 Bool Unit where + initial := () + tr _ _ _ _ bit := .step + { inputTape := 0, workTapes := Fin.elim0, output := some bit, state := none } + Empty.elim Empty.elim + +-- One interval of two bits: the strings starting with `true` accept. +example : ∑ σ : MultiTapePTM.Schedule 0 1, (emitCoin.blockNetwork [] 2 σ).contraction = 2 := by + rw [MultiTapePTM.sum_contraction_blockNetwork _ _ _ one_pos, + show emitCoin.acceptCount [] (1 * 2) = 2 by decide] + +/-- On one work tape, write every coin and move right. The first step emits its coin; then the +machine keeps walking without output. -/ +private def walk : MultiTapePTM 1 Bool Bool where + initial := false + tr state _ _ _ bit := .step + { inputTape := 1, + workTapes := fun _ => (some (some bit), 1), + output := if state then none else some bit, state := some true } + Empty.elim Empty.elim + +-- Two intervals of two bits, with windows on the work tape: half of the `16` strings accept. +example : + ∑ σ : MultiTapePTM.Schedule 1 2, (walk.blockNetwork [true] 2 σ).contraction = 8 := by + rw [MultiTapePTM.sum_contraction_blockNetwork _ _ _ two_pos, + show walk.acceptCount [true] (2 * 2) = 8 by decide] + +-- Each network has `2 * (3 + 1) = 8` edges and `2 * (3 + 2) = 10` vertices, degree at most `8`, +-- no loops, and entries at most `2 ^ 2`. +example (σ : MultiTapePTM.Schedule 1 2) : + Fintype.card (MultiTapePTM.BlockEdge 1 2) = 8 ∧ + Fintype.card (Fin 2 ⊕ MultiTapePTM.BlockEdge 1 2) = 10 ∧ + (walk.blockNetwork [true] 2 σ).MaxDegreeLE 8 ∧ (walk.blockNetwork [true] 2 σ).Loopless ∧ + ∀ v x, (walk.blockNetwork [true] 2 σ).tensor v x ≤ 4 := + ⟨MultiTapePTM.card_blockEdge, MultiTapePTM.card_blockVertex, + walk.maxDegreeLE_blockNetwork _ _ σ, walk.loopless_blockNetwork _ _ σ, + walk.tensor_blockNetwork_le _ _ σ⟩ + +end ComplexityTests.HPVBlockNetwork From 2914159380f388f8a1814dd396f6ace61bf0914d Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 19:14:17 -0400 Subject: [PATCH 9/9] feat(machines): explicit Boolean block-counting networks (#1833 H3) Write the block-counting network of a schedule out as an explicit Boolean tensor network: binarize by a concrete injective letter code of (s + k + 4) * b bits, subdivide by equality tensors, and number the old vertices first. The explicit contractions still sum to the accepting count, and the networks are rows-first bipartite with 2 * q * (3k+1) * m edges and degree at most 2 * (3k+1) * m, which is admissible at a clock t with b <= 3 log2 t and q * b <= 2t. Generic additions: ExplicitTensorNetwork.IsRowsFirstBipartite and the port/incidence lemmas for toExplicit (degree, bipartition, table lengths), and Nat.clog_two_add_two_le_three_mul_log_two. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Frontier/TensorNetwork/Explicit.lean | 143 ++++++- .../Probabilistic/ExplicitBlockNetwork.lean | 364 ++++++++++++++++++ Complexity/Foundations/Data/Nat/Log.lean | 11 + .../Circuit/Frontier/TensorNetwork.lean | 29 ++ ComplexityTests/HPVExplicitBlockNetwork.lean | 99 +++++ 6 files changed, 645 insertions(+), 2 deletions(-) create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork.lean create mode 100644 ComplexityTests/HPVExplicitBlockNetwork.lean diff --git a/Complexity.lean b/Complexity.lean index edb6e44788..397740fe3b 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1811,6 +1811,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.C public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.CoinTape public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Composition public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Deterministic +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExtendTapes public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.InputFromTape public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalTensor diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean index 051a95b90a..42914f7f8f 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean @@ -11,6 +11,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork public import Complexity.Foundations.Data.BitString.Counter import Mathlib.Algebra.BigOperators.Fin import Mathlib.Data.List.GetD +import Mathlib.Data.Set.Card /-! # Explicit Boolean tensor networks @@ -30,12 +31,17 @@ reads `false`, and a position past the end of a table has entry zero. Its size measures are the number of edges, the number of vertices, the maximum number of ports of a vertex (`ExplicitTensorNetwork.maxDegree`) and the total length of the tables -(`ExplicitTensorNetwork.tableLength`). +(`ExplicitTensorNetwork.tableLength`). A network is *rows-first bipartite* with `r` rows +(`ExplicitTensorNetwork.IsRowsFirstBipartite`) when every edge is a port of exactly one of its +first `r` vertices and of exactly one of the others. **Writing a network out** (`TensorNetwork.toExplicit`). Given numberings of the vertices and the edges of a Boolean tensor network on finite types, list the edges at each vertex in increasing order and tabulate its tensor on them. The contraction is unchanged -(`TensorNetwork.contraction_toExplicit`). +(`TensorNetwork.contraction_toExplicit`). The ports of a vertex are its incident edges, so the +degree bound carries over (`TensorNetwork.maxDegree_toExplicit_le`), and a numbering that puts +one end of every edge below `r` and the other at or above it gives a rows-first bipartite network +(`TensorNetwork.isRowsFirstBipartite_toExplicit`). ## Main definitions @@ -46,6 +52,8 @@ order and tabulate its tensor on them. The contraction is unchanged * `Cslib.Circuits.Frontier.ExplicitTensorNetwork.contraction`: the contraction. * `Cslib.Circuits.Frontier.ExplicitTensorNetwork.maxDegree`, `Cslib.Circuits.Frontier.ExplicitTensorNetwork.tableLength`: size measures. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.IsRowsFirstBipartite`: the bipartition with the + first `r` vertices as rows. * `Cslib.Circuits.Frontier.TensorNetwork.explicitPorts`, `Cslib.Circuits.Frontier.TensorNetwork.explicitTable`, `Cslib.Circuits.Frontier.TensorNetwork.toExplicit`: writing a Boolean tensor network out. @@ -57,6 +65,12 @@ order and tabulate its tensor on them. The contraction is unchanged tensor. * `Cslib.Circuits.Frontier.TensorNetwork.contraction_toExplicit`: writing a network out preserves its contraction. +* `Cslib.Circuits.Frontier.TensorNetwork.length_explicitPorts`: a vertex has one port per incident + edge. +* `Cslib.Circuits.Frontier.TensorNetwork.maxDegree_toExplicit_le`, + `Cslib.Circuits.Frontier.TensorNetwork.isRowsFirstBipartite_toExplicit`, + `Cslib.Circuits.Frontier.TensorNetwork.length_table_toExplicit`: degree, bipartition and table + lengths of a written-out network. ## References @@ -123,6 +137,18 @@ theorem length_le_maxDegree {v : List ℕ × List R} (hv : v ∈ d.vertices) : v.1.length ≤ d.maxDegree := d.maxDegree_le_iff.mp le_rfl v hv +/-- **Rows-first bipartite**: the first `r` vertices are the *rows* and the others the *columns*, +every port names an edge, and every edge is a port of the rows exactly once and of the columns +exactly once. So every edge joins a row to a column. -/ +def IsRowsFirstBipartite (r : ℕ) : Prop := + (∀ v ∈ d.vertices, ∀ i ∈ v.1, i < d.numEdges) ∧ + ∀ i < d.numEdges, ((d.vertices.take r).map fun v => v.1.count i).sum = 1 ∧ + ((d.vertices.drop r).map fun v => v.1.count i).sum = 1 + +instance (r : ℕ) : Decidable (d.IsRowsFirstBipartite r) := by + unfold IsRowsFirstBipartite + infer_instance + end ExplicitTensorNetwork /-! ### Writing a tensor network out -/ @@ -163,6 +189,40 @@ theorem entry_explicitTable [Zero R] (v : V) (x : Fin m → Bool) : rw [BitString.testBit_lsbValue, List.getD_eq_getElem _ _ (by simpa using hidx), List.getElem_map, List.getElem_idxOf hidx, Function.comp_apply] +/-- An edge is a port of a vertex at most once. -/ +theorem nodup_explicitPorts (v : V) : (N.explicitPorts ee v).Nodup := + (List.nodup_finRange m).filter _ + +/-- **The ports of a vertex are its incident edges**: their number is its degree. -/ +theorem length_explicitPorts (v : V) : + (N.explicitPorts ee v).length = (N.incidenceSet v).ncard := by + classical + rw [← List.toFinset_card_of_nodup (N.nodup_explicitPorts ee v), + ← Set.ncard_image_of_injective _ ee.injective, ← Set.ncard_coe_finset] + congr 1 + ext j + simp [Multigraph.mem_incidenceSet] + +/-- The number of times the edge numbered `j` is a port of `v`: once if it is incident to `v`, and +never otherwise. -/ +theorem count_explicitPorts (v : V) (j : Fin m) : + ((N.explicitPorts ee v).map Fin.val).count j.val = + if N.src (ee.symm j) = v ∨ N.tgt (ee.symm j) = v then 1 else 0 := by + rw [List.Nodup.count ((N.nodup_explicitPorts ee v).map Fin.val_injective)] + simp only [List.mem_map, Fin.val_inj, exists_eq_right, mem_explicitPorts] + +/-- A table lists the values of the tensor at all `2 ^ (number of ports)` lists of bits on the +ports. -/ +theorem length_explicitTable (v : V) : + (N.explicitTable ee v).length = 2 ^ (N.explicitPorts ee v).length := by + simp [explicitTable] + +/-- Every entry of a written-out table is a value of the tensor. -/ +theorem exists_tensor_of_mem_explicitTable {v : V} {a : R} (ha : a ∈ N.explicitTable ee v) : + ∃ y, a = N.tensor v y := by + obtain ⟨j, -, rfl⟩ := List.mem_map.mp ha + exact ⟨_, rfl⟩ + /-- A Boolean tensor network on finite types written out as an explicit network, numbering the vertices by `ev` and the edges by `ee`: vertex `i` is `ev.symm i`, with its ports in increasing order and its table. -/ @@ -171,6 +231,85 @@ def toExplicit : ExplicitTensorNetwork R where vertices := List.ofFn fun i => ((N.explicitPorts ee (ev.symm i)).map Fin.val, N.explicitTable ee (ev.symm i)) +/-- The vertices of the written-out network are the ports and tables of the vertices. -/ +theorem mem_vertices_toExplicit {p : List ℕ × List R} : + p ∈ (N.toExplicit ev ee).vertices ↔ + ∃ v, p = ((N.explicitPorts ee v).map Fin.val, N.explicitTable ee v) := by + simp only [toExplicit, List.mem_ofFn] + constructor + · rintro ⟨i, rfl⟩ + exact ⟨_, rfl⟩ + · rintro ⟨v, rfl⟩ + exact ⟨ev v, by simp⟩ + +/-- **The degree bound carries over**: a vertex of the written-out network has as many ports as +the vertex has incident edges. -/ +theorem maxDegree_toExplicit_le [Finite E] {D : ℕ} (hD : N.MaxDegreeLE D) : + (N.toExplicit ev ee).maxDegree ≤ D := by + rw [ExplicitTensorNetwork.maxDegree_le_iff] + intro p hp + obtain ⟨v, rfl⟩ := (N.mem_vertices_toExplicit ev ee).mp hp + rw [List.length_map, length_explicitPorts] + exact hD v + +/-- Every table of the written-out network has an entry for every list of bits on its ports. -/ +theorem length_table_toExplicit {p : List ℕ × List R} (hp : p ∈ (N.toExplicit ev ee).vertices) : + p.2.length = 2 ^ p.1.length := by + obtain ⟨v, rfl⟩ := (N.mem_vertices_toExplicit ev ee).mp hp + simp [length_explicitTable] + +/-- Every table entry of the written-out network is a value of a tensor. -/ +theorem exists_tensor_of_mem_toExplicit {p : List ℕ × List R} + (hp : p ∈ (N.toExplicit ev ee).vertices) {a : R} (ha : a ∈ p.2) : + ∃ v y, a = N.tensor v y := by + obtain ⟨v, rfl⟩ := (N.mem_vertices_toExplicit ev ee).mp hp + exact ⟨v, N.exists_tensor_of_mem_explicitTable ee ha⟩ + +private theorem sum_drop_ofFn (f : Fin n → ℕ) (r : ℕ) : + ((List.ofFn f).drop r).sum = ∑ a with ¬ a.val < r, f a := by + have h := List.sum_take_add_sum_drop (List.ofFn f) r + rw [List.sum_take_ofFn, List.sum_ofFn, + ← Finset.sum_filter_add_sum_filter_not Finset.univ (fun a : Fin n => a.val < r)] at h + omega + +/-- **Rows first.** If every edge joins a vertex numbered below `r` to one numbered at least `r`, +the written-out network is bipartite with the first `r` vertices as rows. -/ +theorem isRowsFirstBipartite_toExplicit (r : ℕ) + (hside : ∀ e, (ev (N.src e) : ℕ) < r ↔ ¬ (ev (N.tgt e) : ℕ) < r) : + (N.toExplicit ev ee).IsRowsFirstBipartite r := by + refine ⟨fun p hp i hi => ?_, fun i hi => ?_⟩ + · obtain ⟨v, rfl⟩ := (N.mem_vertices_toExplicit ev ee).mp hp + obtain ⟨j, -, rfl⟩ := List.mem_map.mp hi + exact j.isLt + · -- The edge numbered `i` is a port of its source and its target, which are distinct. + set j : Fin m := ⟨i, hi⟩ + set e := ee.symm j + have hne : N.src e ≠ N.tgt e := fun h => by + have := hside e + rw [h] at this + tauto + have hcount : ∀ a : Fin n, ((N.explicitPorts ee (ev.symm a)).map Fin.val).count i = + (if ev (N.src e) = a then 1 else 0) + (if ev (N.tgt e) = a then 1 else 0) := by + intro a + rw [show i = j.val from rfl, count_explicitPorts] + simp only [Equiv.eq_symm_apply] + by_cases hs : ev (N.src e) = a <;> by_cases ht : ev (N.tgt e) = a + · exact absurd (ev.injective (hs.trans ht.symm)) hne + all_goals simp [e, hs, ht] + have hsum : ∀ s : Finset (Fin n), + ∑ a ∈ s, ((N.explicitPorts ee (ev.symm a)).map Fin.val).count i = + (if ev (N.src e) ∈ s then 1 else 0) + (if ev (N.tgt e) ∈ s then 1 else 0) := by + intro s + simp only [hcount, Finset.sum_add_distrib, Finset.sum_ite_eq] + have hv : (N.toExplicit ev ee).vertices = List.ofFn fun a => + ((N.explicitPorts ee (ev.symm a)).map Fin.val, N.explicitTable ee (ev.symm a)) := rfl + rw [hv, List.map_take, List.map_drop, List.map_ofFn, List.sum_take_ofFn, sum_drop_ofFn] + simp only [Function.comp_def] + rw [hsum, hsum] + have := hside e + simp only [Finset.mem_filter, Finset.mem_univ, true_and] + by_cases h : (ev (N.src e) : ℕ) < r <;> simp_all + /-- **Writing a network out preserves its contraction.** -/ theorem contraction_toExplicit [CommSemiring R] [Fintype V] [Fintype E] [DecidableEq E] : (N.toExplicit ev ee).contraction = N.contraction := by diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork.lean new file mode 100644 index 0000000000..56ed22be45 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork.lean @@ -0,0 +1,364 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.BlockNetwork +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Binarize +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit +public import Mathlib.Algebra.BigOperators.Fin +public import Mathlib.Data.ZMod.Basic +public import Mathlib.Data.Nat.Log +public import Mathlib.Logic.Equiv.Fin.Basic + +/-! +# Explicit block-counting networks + +The block-counting network of a schedule (`Turing.MultiTapePTM.blockNetwork`) carries structured +letters on its edges: control records and block contents (`Turing.MultiTapePTM.BlockLetter`). +This module writes it out as an explicit Boolean tensor network +(`Cslib.Circuits.Frontier.ExplicitTensorNetwork`), the form that a contraction algorithm reads, +completing the construction of Lemma 2.2 of the note *Deterministic simulations of +nondeterministic and randomized time* (30 October 2026) formalized in issue #1833: + +1. **Binarize** by a concrete injective code of the letters + (`Turing.MultiTapePTM.letterCode`), in `letterBits k s b = (s + k + 4) * b` bits, where `s` + numbers the states. A letter is numbered by `Turing.MultiTapePTM.letterEquiv`, composed of the + standard numberings of finite products, sums, options and functions (`finProdFinEquiv`, + `finSumFinEquiv`, `finSuccEquiv`, `finFunctionFinEquiv`); its code is the binary digits of its + number. +2. **Subdivide** every Boolean edge by an equality tensor, which makes the network bipartite. +3. **Write out** (`Cslib.Circuits.Frontier.TensorNetwork.toExplicit`), numbering the old vertices + (the intervals and sinks) first and the subdivision vertices after them, both by concrete + numberings (`Turing.MultiTapePTM.explicitVertexEquiv`, `Turing.MultiTapePTM.explicitEdgeEquiv`). + +Each step preserves the contraction, so the explicit networks of the schedules still sum to the +accepting count (`Turing.MultiTapePTM.sum_contraction_explicitBlockNetwork`). + +**Size.** With `q` intervals, `k` work tapes and `m = letterBits k s b`, the explicit network has +`2 * (q * (3 * k + 1) * m)` edges and maximum degree at most `2 * (3 * k + 1) * m`, both `O(b)` per +interval. Its first `q * (3 * k + 2)` vertices are the rows of a bipartition: every edge has +exactly one port at a row and one at a column +(`Cslib.Circuits.Frontier.ExplicitTensorNetwork.IsRowsFirstBipartite`). Every table has length +`2 ^ (number of ports)`, and its entries are at most `2 ^ b`. + +These are the inputs of the Boolean tensor contraction theorem [OpenAI2026ETH, Theorem D.1] +as the counting simulation of #1833 uses it: with `b = ⌈log₂ (t + 2)⌉` and `q * b ≤ 2 t`, the +networks have `O(t)` edges and maximum degree `O(log t)`. + +## Main definitions + +* `Turing.MultiTapePTM.letterEquiv`, `Turing.MultiTapePTM.letterCode`, + `Turing.MultiTapePTM.letterBits`: the numbering and binary code of the letters. +* `Turing.MultiTapePTM.blockEdgeEquiv`, `Turing.MultiTapePTM.explicitVertexEquiv`, + `Turing.MultiTapePTM.explicitEdgeEquiv`: the numberings of edges and vertices. +* `Turing.MultiTapePTM.explicitBlockNetwork`: the explicit block-counting network of a schedule. + +## Main results + +* `Turing.MultiTapePTM.letterCode_injective`: the code is injective. +* `Turing.MultiTapePTM.contraction_explicitBlockNetwork`: writing the network out preserves its + contraction. +* `Turing.MultiTapePTM.sum_contraction_explicitBlockNetwork`: summed over the schedules, the + contractions are the accepting count. +* `Turing.MultiTapePTM.admissible_explicitBlockNetwork`: at a clock `t` with `b = O(log t)` and + `q * b ≤ 2 t`, the network is rows-first bipartite with `O(t)` edges and degree `O(log t)`. +* `Turing.MultiTapePTM.numEdges_explicitBlockNetwork`, + `Turing.MultiTapePTM.length_vertices_explicitBlockNetwork`, + `Turing.MultiTapePTM.maxDegree_explicitBlockNetwork_le`, + `Turing.MultiTapePTM.isRowsFirstBipartite_explicitBlockNetwork`, + `Turing.MultiTapePTM.length_table_explicitBlockNetwork`, + `Turing.MultiTapePTM.entry_le_explicitBlockNetwork`: size, degree, bipartition and tables. + +## References + +* [J. Hopcroft, W. Paul, L. Valiant, *On Time Versus Space*][HopcroftPaulValiant1977] +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.1 (p. 53) +-/ + +public section + +namespace Turing + +namespace MultiTapeNTM.ChoiceTable.OutputTrack + +/-- The output tracks numbered `empty ↦ 0`, `accept ↦ 1`, `other ↦ 2`. -/ +@[expose] def equivFin : OutputTrack ≃ Fin 3 where + toFun + | .empty => 0 + | .accept => 1 + | .other => 2 + invFun i := if i = 0 then .empty else if i = 1 then .accept else .other + left_inv t := by cases t <;> rfl + right_inv i := by fin_cases i <;> rfl + +end MultiTapeNTM.ChoiceTable.OutputTrack + +namespace MultiTapePTM + +open Cslib.Circuits.Frontier MultiTapeNTM.ChoiceTable Function + +variable {k q s : ℕ} {State : Type} {b : ℕ} + +/-! ### Numbering and coding the letters -/ + +section Letters + +variable [NeZero b] + +/-- The residues modulo `b > 0` numbered by their values. -/ +@[expose] def zmodEquiv (b : ℕ) [NeZero b] : ZMod b ≃ Fin b := + (ZMod.finEquiv b).toEquiv.symm + +@[simp] theorem val_zmodEquiv (r : ZMod b) : (zmodEquiv b r : ℕ) = r.val := by + obtain _ | b := b + · exact absurd rfl (NeZero.ne 0) + · rfl + +/-- The contents of a cell numbered `none ↦ 0`, `some false ↦ 1`, `some true ↦ 2`. -/ +@[expose] def cellEquiv : Option Bool ≃ Fin 3 := + (Equiv.optionCongr finTwoEquiv.symm).trans (finSuccEquiv 2).symm + +/-- The control records numbered: the state (with `none` first, then the states numbered by `e`), +then the head offsets as `k + 1` digits in base `b`, then the output track. -/ +@[expose] def controlEquiv (e : State ≃ Fin s) : + BlockControl k State b ≃ Fin ((s + 1) * (b ^ (k + 1) * 3)) := + (Equiv.prodCongr ((Equiv.optionCongr e).trans (finSuccEquiv s).symm) + ((Equiv.prodCongr + ((Equiv.arrowCongr (finSuccEquiv k).symm (zmodEquiv b)).trans finFunctionFinEquiv) + OutputTrack.equivFin).trans finProdFinEquiv)).trans finProdFinEquiv + +/-- The block contents numbered as `b` digits in base `3`. -/ +@[expose] def contentsEquiv (b : ℕ) [NeZero b] : (ZMod b → Option Bool) ≃ Fin (3 ^ b) := + (Equiv.arrowCongr (zmodEquiv b) cellEquiv).trans finFunctionFinEquiv + +/-- **The letters numbered**: the control records first (`Turing.MultiTapePTM.controlEquiv`), +then the block contents (`Turing.MultiTapePTM.contentsEquiv`). -/ +@[expose] def letterEquiv (e : State ≃ Fin s) : + BlockLetter k State b ≃ Fin ((s + 1) * (b ^ (k + 1) * 3) + 3 ^ b) := + (Equiv.sumCongr (controlEquiv e) (contentsEquiv b)).trans finSumFinEquiv + +/-- The number of bits of a letter: `(s + k + 4) * b`, for `s` states and `k` work tapes. -/ +@[expose] def letterBits (k s b : ℕ) : ℕ := (s + k + 4) * b + +/-- Every letter number fits in `letterBits k s b` bits. -/ +theorem card_letter_le_two_pow : + (s + 1) * (b ^ (k + 1) * 3) + 3 ^ b ≤ 2 ^ letterBits k s b := by + have hb : 1 ≤ b := Nat.one_le_iff_ne_zero.mpr (NeZero.ne b) + have hs : s + 1 ≤ 2 ^ (s * b) := + (Nat.lt_two_pow_self).trans_le (Nat.pow_le_pow_right two_pos (Nat.le_mul_of_pos_right s hb)) + have hbk : b ^ (k + 1) ≤ 2 ^ ((k + 1) * b) := by + rw [mul_comm, pow_mul] + exact Nat.pow_le_pow_left (Nat.lt_two_pow_self).le _ + have h3 : 3 ≤ 2 ^ (2 * b) := by + calc 3 ≤ 2 ^ 2 := by norm_num + _ ≤ 2 ^ (2 * b) := Nat.pow_le_pow_right two_pos (by omega) + have h3b : 3 ^ b ≤ 2 ^ (2 * b) := by + rw [pow_mul] + exact Nat.pow_le_pow_left (by norm_num) _ + have hctl : (s + 1) * (b ^ (k + 1) * 3) ≤ 2 ^ ((s + k + 3) * b) := by + calc (s + 1) * (b ^ (k + 1) * 3) ≤ 2 ^ (s * b) * (2 ^ ((k + 1) * b) * 2 ^ (2 * b)) := + Nat.mul_le_mul hs (Nat.mul_le_mul hbk h3) + _ = 2 ^ ((s + k + 3) * b) := by rw [← pow_add, ← pow_add]; ring_nf + have hcon : 3 ^ b ≤ 2 ^ ((s + k + 3) * b) := + h3b.trans (Nat.pow_le_pow_right two_pos (Nat.mul_le_mul_right b (by omega))) + calc _ ≤ 2 ^ ((s + k + 3) * b) + 2 ^ ((s + k + 3) * b) := Nat.add_le_add hctl hcon + _ = 2 ^ ((s + k + 3) * b + 1) := by rw [pow_succ]; ring + _ ≤ 2 ^ letterBits k s b := + Nat.pow_le_pow_right two_pos (by unfold letterBits; nlinarith) + +/-- **The letter code**: the `letterBits k s b` binary digits, least significant first, of the +number of a letter (`Turing.MultiTapePTM.letterEquiv`). -/ +@[expose] def letterCode (e : State ≃ Fin s) (l : BlockLetter k State b) : + Fin (letterBits k s b) → Bool := + fun j => (letterEquiv e l : ℕ).testBit j + +/-- **The letter code is injective**: letter numbers fit in `letterBits k s b` bits. -/ +theorem letterCode_injective (e : State ≃ Fin s) : + Injective (letterCode (k := k) (b := b) e) := by + intro l l' h + have hlt : ∀ l : BlockLetter k State b, (letterEquiv e l : ℕ) < 2 ^ letterBits k s b := + fun l => (letterEquiv e l).isLt.trans_le card_letter_le_two_pow + refine (letterEquiv e).injective (Fin.ext (Nat.eq_of_testBit_eq fun j => ?_)) + by_cases hj : j < letterBits k s b + · exact congrFun h ⟨j, hj⟩ + · rw [Nat.testBit_lt_two_pow ((hlt l).trans_le (Nat.pow_le_pow_right two_pos (not_lt.mp hj))), + Nat.testBit_lt_two_pow ((hlt l').trans_le (Nat.pow_le_pow_right two_pos (not_lt.mp hj)))] + +instance : Nonempty (BlockLetter k State b) := ⟨.inr fun _ => none⟩ + +end Letters + +/-! ### Numbering the edges and vertices -/ + +-- A named instance keeps the instances on the vertex types of the explicit network small. +instance (k q : ℕ) : DecidableEq (BlockEdge k q) := + inferInstanceAs (DecidableEq (Fin q ⊕ (Fin q × Fin k × Fin 3))) + +/-- The edges of a block-counting network numbered: the control edges first, then the block edges +`(i, h, d)` in lexicographic order. -/ +@[expose] def blockEdgeEquiv (k q : ℕ) : BlockEdge k q ≃ Fin (q * (3 * k + 1)) := + ((Equiv.sumCongr (Equiv.refl _) + ((Equiv.prodCongr (Equiv.refl _) finProdFinEquiv).trans finProdFinEquiv)).trans + finSumFinEquiv).trans (finCongr (by ring)) + +/-- The vertices of the explicit network numbered: the old vertices first (the intervals, then the +sinks in the order of their edges), then the subdivision vertices, one for each copy `(e, j)` of an +edge. -/ +@[expose] def explicitVertexEquiv (k q m : ℕ) : + (Fin q ⊕ BlockEdge k q) ⊕ (BlockEdge k q × Fin m) ≃ + Fin (q * (3 * k + 2) + q * (3 * k + 1) * m) := + (Equiv.sumCongr + (((Equiv.sumCongr (Equiv.refl _) (blockEdgeEquiv k q)).trans finSumFinEquiv).trans + (finCongr (by ring))) + ((Equiv.prodCongr (blockEdgeEquiv k q) (Equiv.refl _)).trans finProdFinEquiv)).trans + finSumFinEquiv + +/-- The edges of the explicit network numbered: the source halves of the copies `(e, j)` first, +then their target halves. -/ +@[expose] def explicitEdgeEquiv (k q m : ℕ) : + (BlockEdge k q × Fin m) ⊕ (BlockEdge k q × Fin m) ≃ Fin (2 * (q * (3 * k + 1) * m)) := + ((Equiv.sumCongr ((Equiv.prodCongr (blockEdgeEquiv k q) (Equiv.refl _)).trans finProdFinEquiv) + ((Equiv.prodCongr (blockEdgeEquiv k q) (Equiv.refl _)).trans finProdFinEquiv)).trans + finSumFinEquiv).trans (finCongr (by ring)) + +/-- The old vertices come first. -/ +theorem explicitVertexEquiv_inl (k q m : ℕ) (v : Fin q ⊕ BlockEdge k q) : + (explicitVertexEquiv k q m (.inl v) : ℕ) < q * (3 * k + 2) := by + simp only [explicitVertexEquiv, Equiv.trans_apply, Equiv.sumCongr_apply, Sum.map_inl, + finSumFinEquiv_apply_left, Fin.val_castAdd] + exact Fin.isLt _ + +/-- The subdivision vertices come after the old ones. -/ +theorem le_explicitVertexEquiv_inr (k q m : ℕ) (p : BlockEdge k q × Fin m) : + q * (3 * k + 2) ≤ (explicitVertexEquiv k q m (.inr p) : ℕ) := by + simp only [explicitVertexEquiv, Equiv.trans_apply, Equiv.sumCongr_apply, Sum.map_inr, + finSumFinEquiv_apply_right, Fin.val_natAdd] + omega + +/-! ### The explicit network -/ + +variable (machine : MultiTapePTM k Bool State) (input : List Bool) (b : ℕ) [NeZero b] + (σ : Schedule k q) (e : State ≃ Fin s) + +/-- **The explicit block-counting network** of the schedule `σ`: the block-counting network +binarized by the letter code (`Turing.MultiTapePTM.letterCode`), subdivided by equality tensors +and written out with the old vertices first. Its first `q * (3 * k + 2)` vertices are the rows of +its bipartition. -/ +@[expose] noncomputable def explicitBlockNetwork : ExplicitTensorNetwork ℕ := + ((machine.blockNetwork input b σ).binarize (letterCode e)).subdivide.toExplicit + (explicitVertexEquiv k q (letterBits k s b)) (explicitEdgeEquiv k q (letterBits k s b)) + +/-- **Writing the network out preserves its contraction.** -/ +theorem contraction_explicitBlockNetwork [Fintype State] : + (machine.explicitBlockNetwork input b σ e).contraction = + (machine.blockNetwork input b σ).contraction := by + rw [explicitBlockNetwork, TensorNetwork.contraction_toExplicit, + TensorNetwork.contraction_subdivide, + TensorNetwork.contraction_binarize _ (letterCode_injective e)] + +/-- **The block-counting identity for the explicit networks** (the note's Lemma 2.2, equation +(2)). Summed over the movement schedules of `q > 0` intervals of `b` bits, the contractions of the +explicit block-counting networks are the accepting count on `q * b` bits. -/ +theorem sum_contraction_explicitBlockNetwork [Finite State] (hq : 0 < q) : + ∑ σ : Schedule k q, (machine.explicitBlockNetwork input b σ e).contraction = + machine.acceptCount input (q * b) := by + have := Fintype.ofFinite State + simp only [contraction_explicitBlockNetwork] + exact machine.sum_contraction_blockNetwork input b hq + +/-- The explicit network has `2 * (q * (3 * k + 1) * letterBits k s b)` edges: two halves of each +of the `letterBits k s b` copies of each of the `q * (3 * k + 1)` edges. -/ +theorem numEdges_explicitBlockNetwork : + (machine.explicitBlockNetwork input b σ e).numEdges = + 2 * (q * (3 * k + 1) * letterBits k s b) := rfl + +/-- The explicit network has `q * (3 * k + 2)` old vertices and one subdivision vertex for each +copy of an edge. -/ +theorem length_vertices_explicitBlockNetwork : + (machine.explicitBlockNetwork input b σ e).vertices.length = + q * (3 * k + 2) + q * (3 * k + 1) * letterBits k s b := by + simp [explicitBlockNetwork, TensorNetwork.toExplicit] + +/-- **The degree bound**: at most `2 * (3 * k + 1) * letterBits k s b` ports at every vertex, +`O(b)` for a fixed machine. -/ +theorem maxDegree_explicitBlockNetwork_le : + (machine.explicitBlockNetwork input b σ e).maxDegree ≤ + 2 * (3 * k + 1) * letterBits k s b := by + have hm : 1 ≤ letterBits k s b := + Nat.mul_pos (by omega) (Nat.pos_of_neZero b) + refine TensorNetwork.maxDegree_toExplicit_le _ _ _ + (TensorNetwork.maxDegreeLE_subdivide _ ?_ ?_ ?_) + · exact TensorNetwork.loopless_binarize _ _ (machine.loopless_blockNetwork input b σ) + · exact TensorNetwork.maxDegreeLE_binarize _ _ (machine.maxDegreeLE_blockNetwork input b σ) + · nlinarith + +/-- **The bipartition**: the first `q * (3 * k + 2)` vertices, the old ones, are rows; every edge +joins an old vertex to a subdivision vertex. -/ +theorem isRowsFirstBipartite_explicitBlockNetwork : + (machine.explicitBlockNetwork input b σ e).IsRowsFirstBipartite (q * (3 * k + 2)) := by + refine TensorNetwork.isRowsFirstBipartite_toExplicit _ _ _ _ fun p => ?_ + rcases p with p | p <;> + simp only [TensorNetwork.subdivide_src_inl, TensorNetwork.subdivide_src_inr, + TensorNetwork.subdivide_tgt_inl, TensorNetwork.subdivide_tgt_inr] <;> + exact iff_of_true (explicitVertexEquiv_inl _ _ _ _) + (not_lt.mpr (le_explicitVertexEquiv_inr _ _ _ _)) + +/-- **Admissibility at a clock `t`.** With blocks of `b ≤ 3 ⌊log₂ t⌋` steps and padded time +`q * b ≤ 2 t`, the explicit network is rows-first bipartite with `O(t)` edges and maximum degree +`O(log t)`, with the constant `6 (3 k + 1) (s + k + 4)` of the machine. For the counting +simulation, `b = ⌈log₂ (t + 2)⌉` (`Nat.clog_two_add_two_le_three_mul_log_two`). -/ +theorem admissible_explicitBlockNetwork {t : ℕ} (hb : b ≤ 3 * Nat.log 2 t) (hqb : q * b ≤ 2 * t) : + (machine.explicitBlockNetwork input b σ e).IsRowsFirstBipartite (q * (3 * k + 2)) ∧ + (machine.explicitBlockNetwork input b σ e).numEdges ≤ 6 * (3 * k + 1) * (s + k + 4) * t ∧ + (machine.explicitBlockNetwork input b σ e).maxDegree ≤ + 6 * (3 * k + 1) * (s + k + 4) * Nat.log 2 t := by + refine ⟨machine.isRowsFirstBipartite_explicitBlockNetwork input b σ e, ?_, ?_⟩ + · rw [numEdges_explicitBlockNetwork, letterBits] + calc 2 * (q * (3 * k + 1) * ((s + k + 4) * b)) + = 2 * (3 * k + 1) * (s + k + 4) * (q * b) := by ring + _ ≤ 2 * (3 * k + 1) * (s + k + 4) * (2 * t) := Nat.mul_le_mul_left _ hqb + _ ≤ 6 * (3 * k + 1) * (s + k + 4) * t := by + have h4 : 2 * (3 * k + 1) * (s + k + 4) * (2 * t) = + 4 * ((3 * k + 1) * (s + k + 4) * t) := by ring + have h6 : 6 * (3 * k + 1) * (s + k + 4) * t = 6 * ((3 * k + 1) * (s + k + 4) * t) := by + ring + omega + · refine (machine.maxDegree_explicitBlockNetwork_le input b σ e).trans ?_ + rw [letterBits] + calc 2 * (3 * k + 1) * ((s + k + 4) * b) = 2 * (3 * k + 1) * (s + k + 4) * b := by ring + _ ≤ 2 * (3 * k + 1) * (s + k + 4) * (3 * Nat.log 2 t) := Nat.mul_le_mul_left _ hb + _ = 6 * (3 * k + 1) * (s + k + 4) * Nat.log 2 t := by ring + +/-- Every table of the explicit network lists the values at all bits on its ports. -/ +theorem length_table_explicitBlockNetwork {p : List ℕ × List ℕ} + (hp : p ∈ (machine.explicitBlockNetwork input b σ e).vertices) : + p.2.length = 2 ^ p.1.length := + TensorNetwork.length_table_toExplicit _ _ _ hp + +/-- **The entry bound**: every table entry of the explicit network is at most `2 ^ b`. -/ +theorem entry_le_explicitBlockNetwork {p : List ℕ × List ℕ} + (hp : p ∈ (machine.explicitBlockNetwork input b σ e).vertices) {a : ℕ} (ha : a ∈ p.2) : + a ≤ 2 ^ b := by + obtain ⟨v, y, rfl⟩ := TensorNetwork.exists_tensor_of_mem_toExplicit _ _ _ hp ha + have hone : (1 : ℕ) ≤ 2 ^ b := Nat.one_le_two_pow + rcases v with v | p + · rw [TensorNetwork.subdivide_tensor_inl] + rcases TensorNetwork.tensor_binarize_eq_zero_or (machine.blockNetwork input b σ) + (letterCode e) v _ with h | ⟨x, h⟩ + · rw [h] + exact Nat.zero_le _ + · rw [h] + exact machine.tensor_blockNetwork_le input b σ v x + · rw [TensorNetwork.subdivide_tensor_inr] + split_ifs + · exact hone + · exact Nat.zero_le _ + +end MultiTapePTM + +end Turing diff --git a/Complexity/Foundations/Data/Nat/Log.lean b/Complexity/Foundations/Data/Nat/Log.lean index e3387cc1ff..5f468fde9b 100644 --- a/Complexity/Foundations/Data/Nat/Log.lean +++ b/Complexity/Foundations/Data/Nat/Log.lean @@ -31,6 +31,7 @@ stays polynomial after logarithmically many rounds. Similarly `2 ^ (⌊log₂ n * `Nat.mul_log_le_add_sq`: `m * ⌊log_b n⌋ ≤ n + m * m` for `1 < b`. * `Nat.clog_two_le_two_mul_of_le_two_mul`: `⌈log₂ n⌉ ≤ 2 * ⌈log₂ n'⌉` when `n ≤ 2 * n'` and `2 ≤ n'`. +* `Nat.clog_two_add_two_le_three_mul_log_two`: `⌈log₂ (n + 2)⌉ ≤ 3 ⌊log₂ n⌋` for `n ≥ 2`. -/ @[expose] public section @@ -109,4 +110,14 @@ theorem clog_two_le_two_mul_of_le_two_mul {n n' : ℕ} (hn : n ≤ 2 * n') (hn' have h3 : clog 2 n ≤ clog 2 n' + 1 := (clog_le_iff_le_pow Nat.one_lt_two).mpr h2 omega +/-- From `n = 2` on, `⌈log₂ (n + 2)⌉ ≤ 3 ⌊log₂ n⌋`: the left side is at most `⌊log₂ n⌋ + 2`, and +`⌊log₂ n⌋ ≥ 1`. -/ +theorem clog_two_add_two_le_three_mul_log_two {n : ℕ} (hn : 2 ≤ n) : + clog 2 (n + 2) ≤ 3 * log 2 n := by + have hL : 1 ≤ log 2 n := le_log_of_pow_le Nat.one_lt_two (by simpa using hn) + have hlt : n < 2 ^ (log 2 n + 1) := lt_pow_succ_log_self Nat.one_lt_two n + refine (clog_le_iff_le_pow Nat.one_lt_two).mpr ?_ + calc n + 2 ≤ 2 ^ (log 2 n + 2) := by rw [Nat.pow_succ]; omega + _ ≤ 2 ^ (3 * log 2 n) := Nat.pow_le_pow_right Nat.two_pos (by omega) + end Nat diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean index 27d867afd5..f030828558 100644 --- a/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean @@ -10,6 +10,7 @@ module public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Constraint public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit public import Mathlib.Data.ZMod.Defs +public import Mathlib.Logic.Equiv.Fin.Basic /-! # Tests for tensor networks @@ -90,6 +91,34 @@ example : parallelNetwork.subdivide.contraction = 70 ∧ parallelNetwork.subdivi decide · exact (Set.ncard_le_card _).trans (by simp) +/-! ### Rows-first bipartitions -/ + +/-- In `parallel`, the first vertex is a row and the second a column. -/ +example : parallel.IsRowsFirstBipartite 1 := by decide + +/-- With both vertices as rows, no edge has a column port. -/ +example : ¬ parallel.IsRowsFirstBipartite 2 := by decide + +/-- In the four-cycle the rows `r₀, r₁` are vertices `0` and `2`, not the first two. -/ +example : ¬ (cycle eqTable).IsRowsFirstBipartite 2 := by decide + +/-- A port naming no edge is excluded. -/ +example : ¬ (⟨1, [([0], [1, 1]), ([0, 5], [1, 1, 1, 1])]⟩ : + ExplicitTensorNetwork ℕ).IsRowsFirstBipartite 1 := by decide + +/-- Written out with the old vertices first, the subdivision of `parallelNetwork` is rows-first +bipartite with degree `2`, both by the general lemmas and by evaluation. -/ +example : (parallelNetwork.subdivide.toExplicit finSumFinEquiv finSumFinEquiv).IsRowsFirstBipartite + 2 ∧ (parallelNetwork.subdivide.toExplicit finSumFinEquiv finSumFinEquiv).maxDegree ≤ 2 := + ⟨parallelNetwork.subdivide.isRowsFirstBipartite_toExplicit _ _ 2 (by decide), + parallelNetwork.subdivide.maxDegree_toExplicit_le _ _ + (parallelNetwork.maxDegreeLE_subdivide (fun e => by simp [parallelNetwork]) + (fun v => (Set.ncard_le_card _).trans (by simp)) le_rfl)⟩ + +example : (parallelNetwork.subdivide.toExplicit finSumFinEquiv finSumFinEquiv).IsRowsFirstBipartite + 2 ∧ (parallelNetwork.subdivide.toExplicit finSumFinEquiv finSumFinEquiv).maxDegree = 2 := by + decide + /-! ### Constraint networks -/ /-- Two vertices joined by two parallel edges, each requiring its two edges to agree. -/ diff --git a/ComplexityTests/HPVExplicitBlockNetwork.lean b/ComplexityTests/HPVExplicitBlockNetwork.lean new file mode 100644 index 0000000000..eb3e8ac2be --- /dev/null +++ b/ComplexityTests/HPVExplicitBlockNetwork.lean @@ -0,0 +1,99 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork +import Complexity.Foundations.Data.Nat.Log + +/-! Explicit block-counting networks of concrete fair-coin machines: the letter numbering on +concrete letters, the counting identity, and the size, degree and bipartition of the networks. -/ + +namespace ComplexityTests.HPVExplicitBlockNetwork + +open Turing MultiTapeMachine MultiTapePTM Cslib.Circuits.Frontier + +/-- Emit the first coin and halt. No work tapes; the input head stays. -/ +private def emitCoin : MultiTapePTM 0 Bool Unit where + initial := () + tr _ _ _ _ bit := .step + { inputTape := 0, workTapes := Fin.elim0, output := some bit, state := none } + Empty.elim Empty.elim + +/-- On one work tape, write every coin and move right. The first step emits its coin; then the +machine keeps walking without output. -/ +private def walk : MultiTapePTM 1 Bool Bool where + initial := false + tr state _ _ _ bit := .step + { inputTape := 1, + workTapes := fun _ => (some (some bit), 1), + output := if state then none else some bit, state := some true } + Empty.elim Empty.elim + +/-! ### The letter numbering -/ + +/-- With two states, one work tape and blocks of two cells, there are +`3 * (2 ^ 2 * 3) = 36` control records, numbered first. The block holding `true` twice is +contents number `2 + 2 * 3 = 8`, so letter number `44`. -/ +example : (letterEquiv (k := 1) (b := 2) finTwoEquiv.symm (.inr fun _ => some true) : ℕ) = 44 := + by decide + +/-- The record of state `true` with both offsets `1` and output track `accept`: state digit `2`, +offset digits `1 + 1 * 2 = 3`, track digit `1`, so number `2 * 12 + (3 * 3 + 1) = 34`. -/ +example : (letterEquiv (k := 1) (b := 2) finTwoEquiv.symm + (.inl (some true, fun _ => 1, .accept)) : ℕ) = 34 := by decide + +/-- The code of letter `44 = 0b101100` in `(2 + 1 + 4) * 2 = 14` bits, least significant first. -/ +example : List.ofFn (letterCode (k := 1) (b := 2) finTwoEquiv.symm (.inr fun _ => some true)) = + [false, false, true, true, false, true, false, false, false, false, false, false, false, + false] := by decide + +/-! ### The counting identity -/ + +-- One interval of two bits: the strings starting with `true` accept. +example : ∑ σ : Schedule 0 1, + (emitCoin.explicitBlockNetwork [] 2 σ (Equiv.ofUnique Unit (Fin 1))).contraction = 2 := by + rw [sum_contraction_explicitBlockNetwork _ _ _ _ one_pos, + show emitCoin.acceptCount [] (1 * 2) = 2 by decide] + +-- Two intervals of two bits, with windows on the work tape: half of the `16` strings accept. +example : ∑ σ : Schedule 1 2, + (walk.explicitBlockNetwork [true] 2 σ finTwoEquiv.symm).contraction = 8 := by + rw [sum_contraction_explicitBlockNetwork _ _ _ _ two_pos, + show walk.acceptCount [true] (2 * 2) = 8 by decide] + +/-! ### Size, degree and bipartition -/ + +-- Letters of `14` bits; `2 * (2 * 4 * 14) = 224` edges; `10` old vertices and `112` subdivision +-- vertices; degree at most `2 * 4 * 14 = 112`; the `10` old vertices are the rows; every table has +-- an entry for each list of bits on its ports, and every entry is at most `2 ^ 2`. +example (σ : Schedule 1 2) : + letterBits 1 2 2 = 14 ∧ + (walk.explicitBlockNetwork [true] 2 σ finTwoEquiv.symm).numEdges = 224 ∧ + (walk.explicitBlockNetwork [true] 2 σ finTwoEquiv.symm).vertices.length = 122 ∧ + (walk.explicitBlockNetwork [true] 2 σ finTwoEquiv.symm).maxDegree ≤ 112 ∧ + (walk.explicitBlockNetwork [true] 2 σ finTwoEquiv.symm).IsRowsFirstBipartite 10 ∧ + ∀ p ∈ (walk.explicitBlockNetwork [true] 2 σ finTwoEquiv.symm).vertices, + p.2.length = 2 ^ p.1.length ∧ ∀ a ∈ p.2, a ≤ 4 := + ⟨rfl, numEdges_explicitBlockNetwork .., length_vertices_explicitBlockNetwork .., + maxDegree_explicitBlockNetwork_le .., isRowsFirstBipartite_explicitBlockNetwork .., + fun _ hp => ⟨length_table_explicitBlockNetwork _ _ _ _ _ hp, + fun _ ha => entry_le_explicitBlockNetwork _ _ _ _ _ hp ha⟩⟩ + +-- At the clock `t = 2`, blocks of `⌈log₂ 4⌉ = 2` steps and one interval: the network of +-- `emitCoin` is rows-first bipartite with at most `6 * 1 * 5 * 2 = 60` edges (it has +-- `2 * (1 * 1 * 10) = 20`) and degree at most `6 * 1 * 5 * ⌊log₂ 2⌋ = 30`. +example (σ : Schedule 0 1) : + (emitCoin.explicitBlockNetwork [] 2 σ (Equiv.ofUnique Unit (Fin 1))).IsRowsFirstBipartite 2 ∧ + (emitCoin.explicitBlockNetwork [] 2 σ (Equiv.ofUnique Unit (Fin 1))).numEdges ≤ 60 ∧ + (emitCoin.explicitBlockNetwork [] 2 σ (Equiv.ofUnique Unit (Fin 1))).maxDegree ≤ 30 := by + have hb : 2 ≤ 3 * Nat.log 2 2 := by + simpa [show Nat.clog 2 (2 + 2) = 2 by decide] using + Nat.clog_two_add_two_le_three_mul_log_two (le_refl 2) + have h := emitCoin.admissible_explicitBlockNetwork [] 2 σ (Equiv.ofUnique Unit (Fin 1)) hb + (by norm_num) + rw [show Nat.log 2 2 = 1 by decide] at h + simpa using h + +end ComplexityTests.HPVExplicitBlockNetwork