From f12bab50958b2ab504e015ae5c6618dce117508a Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 10:52:46 -0400 Subject: [PATCH 1/8] feat(Degree): retain charged output degree from InO bounds Add ComputableInO.computableInDegree: independent degree-d time and degree-e charged workspace bounds with e <= d give cost degree d and output degree e. Reuse the same realizing machine, promote only the workspace cost exponent, and retain the existing encoded-output charge instead of coarsening it to the time degree. This supplies the 2/1 addition client required by #1631 without a new tidy-global bridge. Worker B for #1631, separate bridge commit. Strict focused Degree.Bounds build passes (3534 jobs); targeted hygiene with --check-simp and diff checks pass. No new imports, normalization, algorithm, aliases or qualitative shortcut. Actual addition clients/tests, full six gates and outside-fleet resource-statement review remain for the shared final integration. AI-assisted implementation; source credit retained. --- .../Turing/MultiTape/Complexity/Degree/Bounds.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Degree/Bounds.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Degree/Bounds.lean index 01b160263..f113daefa 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Degree/Bounds.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Degree/Bounds.lean @@ -70,4 +70,18 @@ theorem inO_one (h : ComputableInDegree f encIn encOut 1 e) : end ComputableInDegree +/-- Charged workspace of degree `e` bounds the encoded output at that same degree. When +`e ≤ d`, independent degree bounds on time and workspace give cost degree `d` and output +degree `e`, retaining the realizing machine and its original resource bounds. -/ +theorem ComputableInO.computableInDegree + {α β : Type*} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} + {T S : α → ℕ} {d e : ℕ} (h : ComputableInO f encIn encOut T S) + (hT : DegreeBounded (fun a => (encIn a).length) T d) + (hS : DegreeBounded (fun a => (encIn a).length) S e) (hed : e ≤ d) : + ComputableInDegree f encIn encOut d e := by + obtain ⟨c, hc, hl⟩ := h + have ht := (hT.add_const 1).smul c + have hs := (hS.add_const 1).smul c + exact ⟨⟨_, _, ht, hs.mono_deg hed, hc⟩, hs.mono hl⟩ + end Turing.MultiTapeTM From b3cae19b2dd9dd3addfa15b6070a1f58c4598f17 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 10:56:53 -0400 Subject: [PATCH 2/8] perf(MultiTape): certify consuming binary addition in quadratic time Reuse NatAdd.addStep and the existing final carry fold with charged plain resource certificates. Reachable states remain linear in the framed input length, so both folds and their composition preserve quadratic time and independent linear workspace. The result uses the unchanged foldl_addStep/addBits_bits correctness laws and needs no normalizer. Share the existing plain carry callbacks with successor, remove the value-iteration proof and the superseded public tidy natAdd wrapper, and preserve both pure iterate_succ_eq helpers for their current clients. Worker A /root/review_mpc_api for #1631; AI-assisted with Codex. Existing Christian Reitwiessner, Samuel Schlesinger and Karn Seth source credit preserved. Strict BinaryAddition and LinearSpaceArith build passed3710 jobs after cache bootstrap, focused hygiene/simp and diff checks pass; low local import closure excludes LogSpace/QueryMachine/CounterProgram. B owns immediate Degree/PPT/InSpace clients, C owns behavioral/resource tests; final aggregate/full six gates and outside resource review remain pending. --- .../Complexity/LinearSpaceArith.lean | 43 +---- .../MultiTape/Internal/BinaryAddition.lean | 153 ++++++++++++++++++ .../MultiTape/Internal/BinaryPrimitives.lean | 16 +- scripts/tidy_surface_baseline.json | 1 - 4 files changed, 170 insertions(+), 43 deletions(-) create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryAddition.lean diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LinearSpaceArith.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LinearSpaceArith.lean index 629b994a2..a5eb828e8 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LinearSpaceArith.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LinearSpaceArith.lean @@ -7,24 +7,22 @@ Authors: Christian Reitwiessner module -- upstream: candidate -public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO -public import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCountedIteration -public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.IterateWhile +public import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryAddition public import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryComparison public import Mathlib.Data.Nat.Size /-! # Arithmetic in binary within linear work space -Addition of binary naturals, by iterating the successor with a binary counter. The time is -polynomial in the values, not in their lengths, but the work space is linear in the lengths of the -encodings. This suits space-bounded algorithms, where only the work space matters. +Binary addition reexports the shared consuming schoolbook certificate: time is quadratic in the +encoded input length and charged workspace is linear. The remaining facts bound lengths of +arithmetic outputs and identify successor iteration, for clients with fixed workspace budgets. ## Main results * `Turing.MultiTapeTM.length_encNat_mono`, `.length_encNat_add_le_add`, `.length_encNat_mul_le`: monotonicity and lengths of sums and products in binary. -* `Turing.MultiTapeTM.ComputableInO.natAdd`: addition in binary within linear work space. +* `Turing.MultiTapeTM.ComputableInO.natAdd`: binary addition in quadratic time and linear space. -/ @[expose] public section @@ -67,30 +65,6 @@ namespace ComputableInO theorem iterate_succ_eq (k n : ℕ) : (· + 1)^[k] n = n + k := by simp -/-- **Addition in binary**, within linear work space. -/ -public theorem natAdd : - ComputableInO (fun p : ℕ × ℕ => p.1 + p.2) (encPair encNat encNat) encNat - (fun p => (p.2 + 1) * ((encPair encNat encNat p).length + 2) ^ 2) - fun p => (encPair encNat encNat p).length + 1 := by - have hle (p : ℕ × ℕ) (k : ℕ) (hk : k ≤ p.2) : - (encNat ((· + 1)^[k] p.1)).length ≤ (encNat p.1).length + (encNat p.2).length + 1 := by - rw [iterate_succ_eq] - exact (Turing.MultiTapeTM.length_encNat_mono (by omega : p.1 + k ≤ p.1 + p.2)).trans - (length_encNat_add_le_add _ _) - have h := ComputableInO.iterate (n := fun p : ℕ × ℕ => p.2) (init := fun p => p.1) - (step := (· + 1)) (snd encNat encNat) (fst encNat encNat) ComputableInO.natSucc - (R := fun p => ((encNat p.1).length + (encNat p.2).length + 2) ^ 2) - (Q := fun p => (encNat p.1).length + (encNat p.2).length + 2) - (B := fun p => (encNat p.1).length + (encNat p.2).length + 1) - (fun p k hk => Nat.pow_le_pow_left (by have := hle p k hk; omega) 2) - (fun p k hk => by have := hle p k hk; omega) (fun p k hk => hle p k hk) - refine (h.mono 8 (fun p => ?_) fun p => ?_).of_enc_eq fun p => by rw [iterate_succ_eq] - · simp only [length_encPair] - nlinarith [Nat.zero_le ((encNat p.1).length), Nat.zero_le ((encNat p.2).length), - Nat.zero_le (p.2 * (encNat p.1).length), Nat.zero_le (p.2 * (encNat p.2).length)] - · simp only [length_encPair] - omega - end ComputableInO namespace ComputableTidilyInO @@ -98,13 +72,6 @@ namespace ComputableTidilyInO theorem iterate_succ_eq (k n : ℕ) : (· + 1)^[k] n = n + k := ComputableInO.iterate_succ_eq k n -/-- **Addition in binary**, within linear work space. -/ -public theorem natAdd : - ComputableTidilyInO (fun p : ℕ × ℕ => p.1 + p.2) (encPair encNat encNat) encNat - (fun p => (p.2 + 1) * ((encPair encNat encNat p).length + 2) ^ 2) - fun p => (encPair encNat encNat p).length + 1 := - ComputableInO.natAdd.tidy - end ComputableTidilyInO end Turing.MultiTapeTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryAddition.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryAddition.lean new file mode 100644 index 000000000..dd98e28c1 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryAddition.lean @@ -0,0 +1,153 @@ +/- +Copyright (c) 2026 Christian Reitwiessner, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner, Samuel Schlesinger, Karn Seth +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryPrimitives +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Arithmetic +import Complexity.Computability.Machines.Turing.MultiTape.Internal.DecoderPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree.Bounds +import Complexity.Computability.Machines.Turing.MultiTape.Internal.DegreeClosure +import Complexity.Computability.Machines.Turing.MultiTape.Internal.DegreeComposition +import Complexity.Computability.Machines.Turing.MultiTape.Internal.DegreePrimitives +import Mathlib.Tactic.Linarith + +/-! +# Quadratic schoolbook binary addition + +The existing `NatAdd.addStep` fold consumes the first input's bits and the remaining bits of the +second input, emitting one sum digit per round. A second consuming fold adds the carry to the +remaining second input. Both folds have linear-sized states and linear-cost rounds, so addition +takes quadratic time and independent linear output-charged workspace in the encoded input length. +No iteration by the numeric operands or normalization of the result is needed. + +## Main results + +* `ComputableInO.natAdd`: binary addition in quadratic time and linear charged workspace. +-/ + +public section + +namespace Turing.MultiTapeTM.ComputableInO + +private abbrev encAdd := encPair encBool (encPair encBits encBits) + +private theorem addStep_inO : + ComputableInO (fun p => NatAdd.addStep p.1 p.2) (encPair encAdd encBool) encAdd + (fun p => (encPair encAdd encBool p).length) + (fun p => (encPair encAdd encBool p).length) := by + have hs := ComputableInDegree.fst encAdd encBool + have hrest := (ComputableInDegree.snd encBool (encPair encBits encBits)).comp hs + have hr := (ComputableInDegree.fst encBits encBits).comp hrest + have hflag := (ComputableInDegree.fst encBool (encPair encBits encBits)).comp hs + have hout := (ComputableInDegree.snd encBits encBits).comp hrest + have habc := (ComputableInDegree.snd encAdd encBool).prod + (Internal.DecoderWords.bool_degree.comp hr |>.prod hflag) + have hcarry := (ComputableInDegree.of_finite + (encIn := encPair encBool (encPair encBool encBool)) + (encMid := encBool) fun t : Bool × Bool × Bool => NatAdd.carry t.1 t.2.1 t.2.2).comp habc + have hdigit := (ComputableInDegree.of_finite + (encIn := encPair encBool (encPair encBool encBool)) + (encMid := encBool) fun t : Bool × Bool × Bool => t.1 ^^ (t.2.1 ^^ t.2.2)).comp habc + exact (show ComputableInDegree (fun p => NatAdd.addStep p.1 p.2) + (encPair encAdd encBool) encAdd 1 1 from + (hcarry.prod ((Internal.DecoderWords.tail_degree.comp hr).prod + (hout.append hdigit (encOut := encBits) fun _ => rfl))).mono).inO_one + +private theorem finish_inO : + ComputableInO (fun s : Bool × List Bool × List Bool => + NatSucc.succFinish (s.2.1.foldl NatSucc.succStep (s.1, s.2.2))) encAdd encBits + (fun s => ((encAdd s).length + 1) ^ 2) (fun s => (encAdd s).length + 1) := by + have hs : ComputableInO id encAdd encAdd (fun s => (encAdd s).length) + (fun s => (encAdd s).length) := of_eq fun _ => rfl + have hstate (s : Bool × List Bool × List Bool) (i : ℕ) : + (encPair encBool encBits ((s.2.1.take i).foldl NatSucc.succStep (s.1, s.2.2))).length ≤ + (encAdd s).length + 3 := by + simp only [NatSucc.length_foldl_succStep, encAdd, length_encPair, encBool_apply, + List.length_singleton, encBits_apply] + have := List.length_take_le' i s.2.1 + omega + have hround (s : Bool × List Bool × List Bool) (i : ℕ) (hi : i < s.2.1.length) : + (encPair (encPair encBool encBits) encBool + ((s.2.1.take i).foldl NatSucc.succStep (s.1, s.2.2), s.2.1[i])).length ≤ + 2 * (encAdd s).length + 8 := by + have := hstate s i + rw [length_encPair] + simp only [encBool_apply, List.length_singleton] + omega + have hfold := (foldl hs.snd'.fst' (hs.fst'.prod hs.snd'.snd') succStep + (R := fun s => 2 * (encAdd s).length + 8) + (Q := fun s => 2 * (encAdd s).length + 8) (B := fun s => (encAdd s).length + 3) + hround hround (fun s i _ => hstate s i)).mono + (T' := fun s => ((encAdd s).length + 1) ^ 2) + (S' := fun s => (encAdd s).length + 1) 20 + (fun s => by + simp only [encAdd, encBits_apply, length_encPair, encBool_apply, List.length_singleton, + id_eq] + nlinarith) + (fun s => by + simp only [encAdd, encBits_apply, length_encPair, encBool_apply, List.length_singleton, + id_eq] + omega) + exact succFinish.comp_linear hfold + +/-- **Binary addition**, using the existing consuming carry folds. Time is quadratic and charged +workspace linear in the framed input length, independently of the numeric operands. -/ +theorem natAdd : + ComputableInO (fun p : ℕ × ℕ => p.1 + p.2) (encPair encNat encNat) encNat + (fun p => ((encPair encNat encNat p).length + 1) ^ 2) + (fun p => (encPair encNat encNat p).length + 1) := by + have hbits : ComputableInO Nat.bits encNat encBits (fun n => (encNat n).length) + (fun n => (encNat n).length) := of_eq fun _ => rfl + have hlist := hbits.comp_linear (fst encNat encNat) + have hinit := (const (encMid := encBool) false).prod + ((hbits.comp_linear (snd encNat encNat)).prod (const (encMid := encBits) [])) + have hstate (p : ℕ × ℕ) (i : ℕ) : + (encAdd ((p.1.bits.take i).foldl NatAdd.addStep (false, p.2.bits, []))).length ≤ + 2 * (encPair encNat encNat p).length + 4 := by + obtain ⟨hr, ho⟩ := NatAdd.length_foldl_addStep (p.1.bits.take i) (false, p.2.bits, []) + have := List.length_take_le' i p.1.bits + dsimp only at hr ho + simp only [List.length_nil, Nat.zero_add] at ho + simp only [encAdd, length_encPair, encBool_apply, List.length_singleton, encBits_apply, + encNat_apply] + omega + have hround (p : ℕ × ℕ) (i : ℕ) (hi : i < p.1.bits.length) : + (encPair encAdd encBool + ((p.1.bits.take i).foldl NatAdd.addStep (false, p.2.bits, []), p.1.bits[i])).length ≤ + 4 * (encPair encNat encNat p).length + 10 := by + have := hstate p i + rw [length_encPair] + simp only [encBool_apply, List.length_singleton] + omega + have hfold := (foldl hlist hinit addStep_inO + (R := fun p => 4 * (encPair encNat encNat p).length + 10) + (Q := fun p => 4 * (encPair encNat encNat p).length + 10) + (B := fun p => 2 * (encPair encNat encNat p).length + 4) + hround hround (fun p i _ => hstate p i)).mono + (T' := fun p => ((encPair encNat encNat p).length + 1) ^ 2) + (S' := fun p => (encPair encNat encNat p).length + 1) 30 + (fun p => by + simp only [encBits_apply, length_encPair, encNat_apply, Function.comp_apply] + nlinarith) + (fun p => by + simp only [encBits_apply, length_encPair, encNat_apply, Function.comp_apply] + omega) + refine ((finish_inO.comp hfold).mono 30 (fun p => ?_) (fun p => ?_)).of_enc_eq fun p => ?_ + · have := hstate p p.1.bits.length + rw [List.take_length] at this + simp only [Function.comp_apply] + nlinarith + · have := hstate p p.1.bits.length + rw [List.take_length] at this + simp only [Function.comp_apply] + omega + · simp only [Function.comp_apply, encBits_apply, encNat_apply] + rw [NatSucc.succFinish_foldl, ← NatAdd.foldl_addStep, List.nil_append, NatAdd.addBits_bits] + rfl + +end Turing.MultiTapeTM.ComputableInO diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean index 5c06c4537..ffe6bb41e 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean @@ -19,6 +19,12 @@ The original carry, borrow and leading-zero normalization folds compute successo Their time is quadratic and their charged workspace linear in the binary input length. The zero test uses the existing empty-word machine. All round certificates are plain; normalization occurs only when the internal machine combinators construct the fold. + +## Main results + +* `ComputableInO.succStep`, `ComputableInO.succFinish`: shared linear carry-round certificates. +* `ComputableInO.natSucc`, `ComputableInO.natPred`: quadratic-time, linear-space binary counters. +* `ComputableInO.natIsZero`: linear zero testing. -/ @[expose] public section @@ -58,7 +64,8 @@ private theorem decrStep_inO : (fun p => (encPair (encPair encBool encBits) encBool p).length) := digitStep (op := fun c b => c && !b) (· ^^ ·) -private theorem succStep_inO : +/-- One consuming carry round has linear time and charged workspace. -/ +theorem succStep : ComputableInO (fun p : (Bool × List Bool) × Bool => NatSucc.succStep p.1 p.2) (encPair (encPair encBool encBits) encBool) (encPair encBool encBits) (fun p => (encPair (encPair encBool encBits) encBool p).length) @@ -99,7 +106,8 @@ private theorem normFinish_inO : (S' := fun p => (encPair (encOption encBool) encBits p).length) 3 (fun _ => by split_ifs <;> omega) (fun _ => by split_ifs <;> omega) -private theorem succFinish_inO : +/-- Appending the final carry has linear time and charged workspace. -/ +theorem succFinish : ComputableInO NatSucc.succFinish (encPair encBool encBits) encBits (fun p => (encPair encBool encBits p).length) (fun p => (encPair encBool encBits p).length) := by @@ -139,12 +147,12 @@ theorem foldl_bits {β : Type} {encB : β ↪ List Bool} {init : β} {step : β theorem natSucc : ComputableInO (· + 1) encNat encNat (fun n => ((encNat n).length + 1) ^ 2) (fun n => (encNat n).length + 1) := by - have hfold := foldl_bits (init := (true, [])) succStep_inO 3 fun l i => by + have hfold := foldl_bits (init := (true, [])) succStep 3 fun l i => by rw [NatSucc.length_encAcc, NatSucc.length_foldl_succStep] simp only [List.length_nil, Nat.zero_add] have := List.length_take_le' i l omega - have h := (succFinish_inO.comp_linear hfold).of_encIn_eq (encD := encNat) Nat.bits (fun _ => rfl) + have h := (succFinish.comp_linear hfold).of_encIn_eq (encD := encNat) Nat.bits (fun _ => rfl) refine h.of_enc_eq fun n => ?_ simp only [encNat_apply, encBits_apply, Function.comp_apply, NatSucc.succFinish_foldl, List.nil_append, NatSucc.bits_succ] diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json index 7176bb26d..3611268f6 100644 --- a/scripts/tidy_surface_baseline.json +++ b/scripts/tidy_surface_baseline.json @@ -10,7 +10,6 @@ "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Bit.lean": 1, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean": 4, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean": 45, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LinearSpaceArith.lean": 1, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Lists.lean": 14, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace.lean": 2, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Radix.lean": 3, From 8c4e35e045c2525dad7e814b85082639bd618218 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 11:00:52 -0400 Subject: [PATCH 3/8] refactor(MultiTape): derive addition clients from shared bounds Replace duplicate plain Degree, tidy Degree and PolyTime schoolbook fold proofs with consequences of the shared quadratic-time/linear-charged-space natAdd certificate. Preserve existing FQNs, degree2/1 statements, encodings and attribute registrations. Derive the tidy PolyTime facade from the plain certificate and use the plain InO tidy consequence in the existing legacy InSpace addition proof. The low LinearSpaceArith cleanup exposes one actual provider dependency: InSpace publicly defines its legacy predicate using ComputableTidilyInO. Import BigO directly in that owning module instead of restoring an incidental high-layer reexport below the arithmetic certificate. Its declarations are unchanged. Add the requested Degree.Bounds module-doc explanation of the lower output degree. Worker B for #1631. Final focused strict build passes3856jobs for all7 affected modules and InDegreePlain, BinaryArithmetic, InSpacePlain, BinaryMultiplicationFacade tests. Public headers/registrations, exact InSpace numeric contracts, source identities, targeted hygiene with --check-simp, diff and import-DAG checks pass. Degree.Bounds low closure14modules and BinaryAddition73 have no LogSpace/QueryMachine/CounterProgram dependencies. No new algorithm, normalizer, tidy-global bridge or alias. A integrates aggregate/Ctests, runs all six gates and requests outside-fleet resource review before publication. AI-assisted client consolidation; original source credit preserved. --- .../Turing/MultiTape/Complexity/Arith.lean | 60 +++------------- .../MultiTape/Complexity/Degree/Bounds.lean | 3 + .../Turing/MultiTape/Complexity/InSpace.lean | 1 + .../MultiTape/Complexity/InSpaceLib.lean | 2 +- .../Complexity/PolyTime/Nat/Binary.lean | 2 +- .../MultiTape/Complexity/Quantitative.lean | 70 ++---------------- .../Internal/PolyTimeBinaryPrimitives.lean | 71 ++----------------- 7 files changed, 28 insertions(+), 181 deletions(-) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Arith.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Arith.lean index 517dcf941..38ba796a5 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Arith.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Arith.lean @@ -10,6 +10,8 @@ module public import Mathlib.Data.Nat.Size public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Arithmetic public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Primitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryAddition +import Complexity.Computability.Machines.Turing.MultiTape.Internal.NormalForm import Mathlib.Tactic.Linarith import Mathlib.Tactic.Ring @@ -30,59 +32,19 @@ the second factor shifted by the digits read, adding the shifted factor for ever namespace Turing.MultiTapeTM -open NatSucc - - -open NatAdd ComputableTidilyInDegree +open ComputableTidilyInDegree /-- **Addition is tidily computable in quadratic time and space**, in the binary encoding. -/ public theorem computableTidilyInDegree_add : ComputableTidilyInDegree (fun p : ℕ × ℕ => p.1 + p.2) (encPair encNat encNat) encNat 2 1 := by - let encS := encPair encBool (encPair encBits encBits) - -- a round of the first fold - have hstep : ComputableTidilyInDegree (fun p : _ × Bool => addStep p.1 p.2) - (encPair encS encBool) encS 1 1 := by - have hs := fst encS encBool - have hr := hs.snd'.fst' - have habc := (snd encS encBool).prod (((headD (enc₁ := encBool) false).comp hr).prod hs.fst') - have hcarry := (of_finite (encIn := encPair encBool (encPair encBool encBool)) - (encMid := encBool) fun t : Bool × Bool × Bool => carry t.1 t.2.1 t.2.2).comp habc - have hdigit := (of_finite (encIn := encPair encBool (encPair encBool encBool)) - (encMid := encBool) fun t : Bool × Bool × Bool => t.1 ^^ (t.2.1 ^^ t.2.2)).comp habc - exact (hcarry.prod ((tail (enc₁ := encBool)).comp hr |>.prod - (hs.snd'.snd'.append hdigit (encOut := encBits) fun _ => rfl))).mono - have hsize : DegreeBounded (fun p : ℕ × ℕ => (encPair encNat encNat p).length) - (fun p => 2 * (encPair encNat encNat p).length + 4) 1 := - (DegreeBounded.self.smul 2).add_const 4 - -- the first fold, over the digits of the first summand - have hfold := foldl' (encL := encBits) (encB := encS) - (list := fun p : ℕ × ℕ => p.1.bits) (init := fun p => (false, p.2.bits, [])) - (of_eq (encIn := encNat) (encMid := encBits) (f := Nat.bits) (fun _ => rfl) |>.comp - (fst encNat encNat)) - ((const false).prod ((of_eq (encIn := encNat) (encMid := encBits) (f := Nat.bits) - (fun _ => rfl) |>.comp (snd encNat encNat)).prod (const []))) - hstep hsize ?_ - rotate_left - · intro p i hi - obtain ⟨h₁, h₂⟩ := length_foldl_addStep (p.1.bits.take i) (false, p.2.bits, []) - simp only [encS, length_encPair, encBool_apply, List.length_singleton, encBits_apply, - encNat_apply, List.length_take, List.length_nil] at h₁ h₂ ⊢ - omega - -- the second fold adds the carry to the rest of the second summand - have hfin : ComputableTidilyInDegree (fun s : Bool × List Bool × List Bool => - succFinish (s.2.1.foldl succStep (s.1, s.2.2))) encS encBits 2 1 := by - have hs := of_eq (encIn := encS) (encMid := encS) (f := id) fun _ => rfl - refine ((of_linear linear_succFinish).comp (foldl' (encL := encBits) (encB := encAcc) - hs.snd'.fst' (hs.fst'.prod hs.snd'.snd') - (of_linear linear_succStep) (B := fun s => (encS s).length + 3) - (DegreeBounded.self.add_const 3) fun s i hi => ?_)).mono - simp only [length_foldl_succStep, encS, length_encPair, encBool_apply, id_eq, - List.length_singleton, encBits_apply, List.length_take] - omega - refine ((hfin.comp hfold).of_enc_eq fun p => ?_).mono - simp only [Function.comp_apply, encBits_apply, encNat_apply] - rw [succFinish_foldl, ← foldl_addStep, List.nil_append, addBits_bits] - rfl + obtain ⟨c, hc, hl⟩ := Internal.NormalForm.inO ComputableInO.natAdd + have hT : DegreeBounded (fun p => (encPair encNat encNat p).length) + (fun p => ((encPair encNat encNat p).length + 1) ^ 2) 2 := ⟨1, fun _ => by simp⟩ + have hS : DegreeBounded (fun p => (encPair encNat encNat p).length) + (fun p => (encPair encNat encNat p).length + 1) 1 := ⟨1, fun _ => by simp⟩ + have ht := (hT.add_const 1).smul c + have hs := (hS.add_const 1).smul c + exact ⟨⟨_, _, ht, hs.mono_deg (by decide), hc⟩, hs.mono hl⟩ open NatMul in diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Degree/Bounds.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Degree/Bounds.lean index f113daefa..c70c9777e 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Degree/Bounds.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Degree/Bounds.lean @@ -17,6 +17,9 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Internal.Resour The original three plain rules are moved unchanged from the degree-calculus module to keep ordinary clients independent of its legacy construction calculus. + +Charged `ComputableInO` bounds also give degree certificates: a lower workspace degree bounds +encoded output at that lower degree, even when the time bound has a higher degree. -/ @[expose] public section diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean index 7b93f8094..f25bb455b 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean @@ -7,6 +7,7 @@ Authors: Christian Reitwiessner module -- upstream: candidate +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LinearSpaceArith /-! diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean index ea1f44a10..2600098e1 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean @@ -798,7 +798,7 @@ theorem natSub : theorem natAdd : ComputableTidilyInSpace (fun p : ℕ × ℕ => p.1 + p.2) (encPair encNat encNat) encNat fun p => (encPair encNat encNat p).length + 1 := - of_inO ComputableTidilyInO.natAdd + of_inO ComputableInO.natAdd.tidy theorem dispatch {κ : Type*} (l : List κ) (d : κ) (F : κ → α → β) (hF : ∀ x, ComputableTidilyInSpace (F x) encIn encB fun a => (encIn a).length) {i : α → ℕ} diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean index 5990f07b5..f4d3bdd43 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean @@ -185,7 +185,7 @@ theorem natBits : ComputableTidilyInPolyTime Nat.bits encNat encBits := of_eq fu @[fun_prop] theorem binary_add : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => p.1 + p.2) (encPair encNat encNat) encNat := - computableTidilyInDegree_add.computableTidilyInPolyTime + ComputableInPolyTime.binary_add.tidy /-- Multiplication of binary naturals. -/ @[fun_prop] diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean index 03dfd7887..e051e45ed 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean @@ -12,6 +12,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Internal.Equali public import Mathlib.Tactic.FunProp import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Arithmetic import Complexity.Computability.Machines.Turing.MultiTape.Internal.OLoops +import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryAddition import Mathlib.Data.Nat.Size import Mathlib.Tactic.FinCases import Mathlib.Tactic.Linarith @@ -373,74 +374,13 @@ theorem eq {α : Type} [DecidableEq α] (enc : α ↪ List Bool) : end ComputableInDegree -open NatSucc NatAdd in /-- **Addition is computable in quadratic time and space**, with linear output length, in the binary encoding. -/ theorem computableInDegree_add : - ComputableInDegree (fun p : ℕ × ℕ => p.1 + p.2) (encPair encNat encNat) encNat 2 1 := by - let encS := encPair encBool (encPair encBits encBits) - have hstep : ComputableInDegree (fun p : _ × Bool => addStep p.1 p.2) - (encPair encS encBool) encS 1 1 := by - have hs := ComputableInDegree.fst encS encBool - have hr := hs.snd'.fst' - have habc := (ComputableInDegree.snd encS encBool).prod - (((ComputableInDegree.headD (enc₁ := encBool) false).comp hr).prod hs.fst') - have hcarry := (ComputableInDegree.of_finite - (encIn := encPair encBool (encPair encBool encBool)) - (encMid := encBool) fun t : Bool × Bool × Bool => carry t.1 t.2.1 t.2.2).comp habc - have hdigit := (ComputableInDegree.of_finite - (encIn := encPair encBool (encPair encBool encBool)) - (encMid := encBool) fun t : Bool × Bool × Bool => t.1 ^^ (t.2.1 ^^ t.2.2)).comp habc - exact (hcarry.prod (((ComputableInDegree.tail (enc₁ := encBool)).comp hr).prod - (hs.snd'.snd'.append hdigit (encOut := encBits) fun _ => rfl))).mono - have hsize : DegreeBounded (fun p : ℕ × ℕ => (encPair encNat encNat p).length) - (fun p => 2 * (encPair encNat encNat p).length + 4) 1 := - (DegreeBounded.self.smul 2).add_const 4 - have hfold := ComputableInDegree.foldl' (encL := encBits) (encB := encS) - (list := fun p : ℕ × ℕ => p.1.bits) (init := fun p => (false, p.2.bits, [])) - (ComputableInDegree.of_eq (encIn := encNat) (encMid := encBits) (f := Nat.bits) - (fun _ => rfl) |>.comp (ComputableInDegree.fst encNat encNat)) - ((ComputableInDegree.const false).prod - ((ComputableInDegree.of_eq (encIn := encNat) (encMid := encBits) (f := Nat.bits) - (fun _ => rfl) |>.comp (ComputableInDegree.snd encNat encNat)).prod - (ComputableInDegree.const []))) - hstep hsize (by - intro p i _ - obtain ⟨h₁, h₂⟩ := length_foldl_addStep (p.1.bits.take i) (false, p.2.bits, []) - simp only [encS, length_encPair, encBool_apply, List.length_singleton, encBits_apply, - encNat_apply, List.length_take, List.length_nil] at h₁ h₂ ⊢ - omega) - let encAcc := encPair encBool encBits - have hsuccStep : ComputableInDegree (fun p : (Bool × List Bool) × Bool => succStep p.1 p.2) - (encPair encAcc encBool) encAcc 1 1 := by - have hs := ComputableInDegree.fst encAcc encBool - have hb := ComputableInDegree.snd encAcc encBool - have hc := (ComputableInDegree.of_finite (encIn := encPair encBool encBool) (encMid := encBool) - fun q : Bool × Bool => q.1 && q.2).comp (hs.fst'.prod hb) - have hd := (ComputableInDegree.of_finite (encIn := encPair encBool encBool) (encMid := encBool) - fun q : Bool × Bool => q.1 ^^ q.2).comp (hs.fst'.prod hb) - exact (hc.prod (hs.snd'.append hd (encOut := encBits) fun _ => rfl)).mono - have hsuccFin : ComputableInDegree succFinish encAcc encBits 1 1 := by - have hword := ComputableInDegree.snd encBool encBits - have hyes : ComputableInDegree (fun p : Bool × List Bool => p.2 ++ [true]) - encAcc encBits 1 1 := - hword.append (ComputableInDegree.const (encMid := encBool) true) - (encOut := encBits) (fun _ => rfl) - exact ((ComputableInDegree.fst encBool encBits).ite (hyes.restrict _) - (hword.restrict _)).mono - have hfin : ComputableInDegree (fun s : Bool × List Bool × List Bool => - succFinish (s.2.1.foldl succStep (s.1, s.2.2))) encS encBits 2 1 := by - have hs := ComputableInDegree.of_eq (encIn := encS) (encMid := encS) (f := id) fun _ => rfl - refine (hsuccFin.comp (ComputableInDegree.foldl' (encL := encBits) (encB := encAcc) - hs.snd'.fst' (hs.fst'.prod hs.snd'.snd') hsuccStep - (B := fun s => (encS s).length + 3) (DegreeBounded.self.add_const 3) fun s i _ => ?_)).mono - simp only [length_foldl_succStep, encS, encAcc, length_encPair, encBool_apply, id_eq, - List.length_singleton, encBits_apply, List.length_take] - omega - refine ((hfin.comp hfold).of_enc_eq fun p => ?_).mono - simp only [Function.comp_apply, encBits_apply, encNat_apply] - rw [succFinish_foldl, ← foldl_addStep, List.nil_append, addBits_bits] - rfl + ComputableInDegree (fun p : ℕ × ℕ => p.1 + p.2) (encPair encNat encNat) encNat 2 1 := + ComputableInO.natAdd.computableInDegree + ⟨1, fun _ => by simp⟩ ⟨1, fun _ => by simp⟩ (by decide) + open NatMul in /-- **Multiplication is computable in cubic time and space**, with linear output length, in the diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeBinaryPrimitives.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeBinaryPrimitives.lean index d74f35969..4bd891c3e 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeBinaryPrimitives.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeBinaryPrimitives.lean @@ -10,6 +10,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.A public import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends public import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives public import Complexity.Computability.Machines.Turing.MultiTape.Internal.DegreeClosure +import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryAddition import Mathlib.Data.Nat.Bitwise import Mathlib.Data.List.GetD @@ -24,7 +25,7 @@ with the unchanged full-prefix state bound; its pair certificate remains private @[expose] public section namespace Turing.MultiTapeTM -open Cslib NatAdd NatSucc +open Cslib namespace ComputableInPolyTime @@ -33,70 +34,10 @@ Compose this certificate with the producers' `.prod` certificate. Global automat remains separate from this named rule, since an unconstrained intermediate encoding can select a binary branch where a surrounding computation needs a unary size. -/ theorem binary_add : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 + p.2) - (encPair encNat encNat) encNat := by - let encS := encPair encBool (encPair encBits encBits) - have hstep : ComputableInDegree (fun p : (Bool × List Bool × List Bool) × Bool => - addStep p.1 p.2) (encPair encS encBool) encS 1 1 := by - have hs := ComputableInDegree.fst encS encBool - have hrest := (ComputableInDegree.snd encBool (encPair encBits encBits)).comp hs - have hr := (ComputableInDegree.fst encBits encBits).comp hrest - have hflag := (ComputableInDegree.fst encBool (encPair encBits encBits)).comp hs - have hout := (ComputableInDegree.snd encBits encBits).comp hrest - have habc := (ComputableInDegree.snd encS encBool).prod - (Internal.DecoderWords.bool_degree.comp hr |>.prod hflag) - have hcarry := (ComputableInDegree.of_finite - (encIn := encPair encBool (encPair encBool encBool)) - (encMid := encBool) fun t : Bool × Bool × Bool => carry t.1 t.2.1 t.2.2).comp habc - have hdigit := (ComputableInDegree.of_finite - (encIn := encPair encBool (encPair encBool encBool)) - (encMid := encBool) fun t : Bool × Bool × Bool => t.1 ^^ (t.2.1 ^^ t.2.2)).comp habc - exact (hcarry.prod ((Internal.DecoderWords.tail_degree.comp hr).prod - (hout.append hdigit (encOut := encBits) fun _ => rfl))).mono - have hbits : ComputableInPolyTime Nat.bits encNat encBits := of_eq fun _ => rfl - have hfold := foldl' (encA := encBool) (encL := encBits) (encB := encS) - (list := fun p : ℕ × ℕ => p.1.bits) (init := fun p => (false, p.2.bits, [])) - (hbits.comp (fst encNat encNat)) - ((const false).prod ((hbits.comp (snd encNat encNat)).prod (const []))) - hstep.computableInPolyTime - (B := fun p => 2 * (encPair encNat encNat p).length + 4) - (PolyBounded.of_forall_le 4 1 fun _ => by simp only [pow_one]; omega) (by - intro p i _ - obtain ⟨h₁, h₂⟩ := length_foldl_addStep (p.1.bits.take i) (false, p.2.bits, []) - simp only [encS, length_encPair, encBool_apply, List.length_singleton, encBits_apply, - encNat_apply, List.length_take, List.length_nil] at h₁ h₂ ⊢ - omega) - let encAcc := encPair encBool encBits - have hsuccStep : ComputableInDegree (fun p : (Bool × List Bool) × Bool => - succStep p.1 p.2) (encPair encAcc encBool) encAcc 1 1 := by - have hs := ComputableInDegree.fst encAcc encBool - have hb := ComputableInDegree.snd encAcc encBool - have hflag := (ComputableInDegree.fst encBool encBits).comp hs - have hout := (ComputableInDegree.snd encBool encBits).comp hs - have hc := (ComputableInDegree.of_finite (encIn := encPair encBool encBool) (encMid := encBool) - fun q : Bool × Bool => q.1 && q.2).comp (hflag.prod hb) - have hd := (ComputableInDegree.of_finite (encIn := encPair encBool encBool) (encMid := encBool) - fun q : Bool × Bool => q.1 ^^ q.2).comp (hflag.prod hb) - exact (hc.prod (hout.append hd (encOut := encBits) fun _ => rfl)).mono - have hfinish : ComputableInPolyTime succFinish encAcc encBits := by - have hword := ComputableInDegree.snd encBool encBits - have hyes : ComputableInDegree (fun p : Bool × List Bool => p.2 ++ [true]) - encAcc encBits 1 1 := - hword.append (ComputableInDegree.const (encMid := encBool) true) - (encOut := encBits) (fun _ => rfl) - exact ite (fst encBool encBits) hyes.computableInPolyTime (snd encBool encBits) - have hs : ComputableInPolyTime id encS encS := id' - have hfin := foldl' (encA := encBool) (encL := encBits) (encB := encAcc) - hs.snd'.fst' (hs.fst'.prod hs.snd'.snd') hsuccStep.computableInPolyTime - (B := fun s => (encS s).length + 3) - (PolyBounded.of_forall_le 3 1 fun _ => by simp only [pow_one]; omega) (by - intro s i _ - simp only [length_foldl_succStep, encS, encAcc, length_encPair, encBool_apply, id_eq, - List.length_singleton, encBits_apply, List.length_take] - omega) - refine ((hfinish.comp hfin).comp hfold).of_enc_eq fun p => ?_ - simp only [Function.comp_apply, id_eq, encBits_apply, encNat_apply] - rw [succFinish_foldl, ← foldl_addStep, List.nil_append, addBits_bits] - rfl + (encPair encNat encNat) encNat := + ComputableInO.natAdd.computableInPolyTime + (PolyBounded.of_forall_le 1 2 (fun _ => by simp)) + (PolyBounded.of_forall_le 1 1 (fun _ => by simp)) /-- Strict comparison by scanning binary bit positions, never the numeric operand range. -/ @[fun_prop] From 4b6fdb3959199e0dd3dd593a31f0afb9c405ed63 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 11:03:28 -0400 Subject: [PATCH 4/8] test(MultiTape): exercise shared binary addition certificate Exercise the existing consuming addStep/finish folds at zero, equal, asymmetric, no-carry and long-carry inputs. Check the actual remaining cursor/carry states, final seventeenth bit and asymmetric encoded budgets. Consume the actual shared natAdd certificate through a linear zero check, and compose addition twice at Degree (2,1) and the original InSpace budget. Keep the intentional explicit-addition/fun_prop inference boundary. Validation: cache bootstrap; LEAN_NUM_THREADS=2 lake build --wfail --iofail ComplexityTests.P2SchoolbookAddition PASS (3786 jobs), on A core b3cae19b2 and B client delta cb63ab14; hygiene --check-simp and diff check PASS. The changed-file scanner needs an unrelated missing WordRAM .ilean; its complete scan and all six gates are delegated to A's final integrated run. Abstract impact: none. All 22 catalogue entries, 35 selected declaration links and 66 abstract Lean sources are unchanged, as are rendering inputs. The 14 groups with transitive helper imports retain their meanings and bounds. NatAdd word algorithms, binary/pair encodings and ResourceBounds are byte-identical; only a stronger helper certificate and reused proofs change. Existing Degree (2,1), qualitative addition, charged workspace and uniform machine semantics remain available. No helper headline or new PDF campaign is proposed; the integrated abstract audit remains required. AI assistance: Codex worker /root/review_ready_c implemented and checked these fixtures under #1631. This is authoring-fleet validation, not an independent review of the new public resource statements. --- ComplexityTests/P2SchoolbookAddition.lean | 97 +++++++++++++++++++++++ 1 file changed, 97 insertions(+) create mode 100644 ComplexityTests/P2SchoolbookAddition.lean diff --git a/ComplexityTests/P2SchoolbookAddition.lean b/ComplexityTests/P2SchoolbookAddition.lean new file mode 100644 index 000000000..a8a3c6457 --- /dev/null +++ b/ComplexityTests/P2SchoolbookAddition.lean @@ -0,0 +1,97 @@ +/- +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.Machines.Turing.MultiTape.Encodings.Nat.Arithmetic +public import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryAddition +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.InSpaceLib + +/-! +# Schoolbook addition: consuming carry execution and independent resource clients + +The first fold consumes the first operand and a cursor into the second. The finishing fold +consumes the remaining cursor and emits the final carry. Asymmetric executions distinguish these +stages even though addition is commutative. The composed client doubles a computed sum while +retaining resource degree two, output degree one and the original space budget. +-/ + +open Turing.MultiTapeTM + +-- Empty inputs, equality and a no-carry sum inspect the consuming fold's actual state. +example : + let run (a b : ℕ) := a.bits.foldl NatAdd.addStep (false, b.bits, []); + run 0 0 = (false, [], []) ∧ + run 0 9 = (false, [true, false, false, true], []) ∧ + run 9 0 = (false, [], [true, false, false, true]) ∧ + run 7 7 = (true, [], [false, true, true]) ∧ + run 10 5 = (false, [], [true, true, true, true]) := by + decide +kernel + +-- Swapping a long-carry input moves work from the first fold to the finishing fold. Both +-- executions must emit the seventeenth digit, including when the right cursor is already empty. +example : + let run (a b : ℕ) := a.bits.foldl NatAdd.addStep (false, b.bits, []); + let finish (s : Bool × List Bool × List Bool) := + NatSucc.succFinish (s.2.1.foldl NatSucc.succStep (s.1, s.2.2)); + run 65535 1 = (true, [], List.replicate 16 false) ∧ + run 1 65535 = (true, List.replicate 15 true, [false]) ∧ + finish (run 65535 1) = List.replicate 16 false ++ [true] ∧ + finish (run 1 65535) = List.replicate 16 false ++ [true] ∧ + finish (run 0 9) = [true, false, false, true] ∧ + finish (run 7 7) = [false, true, true, true] ∧ + finish (run 0 0) = [] := by + decide +kernel + +-- Reuse the retained correctness laws to connect precisely those two folds to addition. +example (a b : ℕ) : + let s := a.bits.foldl NatAdd.addStep (false, b.bits, []); + NatSucc.succFinish (s.2.1.foldl NatSucc.succStep (s.1, s.2.2)) = (a + b).bits := by + dsimp only + rw [NatSucc.succFinish_foldl, ← NatAdd.foldl_addStep, List.nil_append, NatAdd.addBits_bits] + rfl + +-- Pair framing is asymmetric despite the equal sums. A seventeenth output bit must be charged. +example : + let L (p : ℕ × ℕ) := (encPair encNat encNat p).length; + L (65535, 1) = 34 ∧ L (1, 65535) = 19 ∧ + (L (65535, 1) + 1) ^ 2 = 1225 ∧ (L (1, 65535) + 1) ^ 2 = 400 ∧ + (encNat (65535 + 1)).length = 17 ∧ (encNat (1 + 65535)).length = 17 := by + decide +kernel + +-- Testing whether a computed sum is empty consumes the independent quadratic-time/linear-space +-- contract through a linear outer machine; the workspace budget must not become quadratic. +example : + let emptySum (p : ℕ × ℕ) := decide (p.1 + p.2 = 0); + ComputableInO emptySum (encPair encNat encNat) encBool + (fun p => ((encPair encNat encNat p).length + 1) ^ 2) + (fun p => (encPair encNat encNat p).length + 1) ∧ + emptySum (0, 0) = true ∧ emptySum (0, 9) = false ∧ emptySum (9, 0) = false := by + exact ⟨ComputableInO.natIsZero.comp_linear ComputableInO.natAdd, + by decide +kernel, by decide +kernel, by decide +kernel⟩ + +-- A supplied addition certificate composes at degree (2,1), rather than multiplying time +-- degrees to four or replacing linear output degree by the quadratic time degree. +example : + let total (p : ℕ × ℕ) := (p.1 + p.2) + (p.1 + p.2); + ComputableInDegree total (encPair encNat encNat) encNat 2 1 ∧ + ComputableInSpace total (encPair encNat encNat) encNat + (fun p => (encPair encNat encNat p).length) ∧ + total (0, 0) = 0 ∧ total (3, 10) = 26 ∧ total (10, 3) = 26 ∧ + total (65535, 1) = 131072 := by + dsimp only + refine ⟨?_, ?_, by decide +kernel, by decide +kernel, by decide +kernel, by decide +kernel⟩ + · fail_if_success fun_prop + have hinputs : ComputableInDegree (fun p : ℕ × ℕ => (p.1, p.2)) + (encPair encNat encNat) (encPair encNat encNat) 1 1 := by + fun_prop (disch := first | apply le_refl | omega) + have hsum := computableInDegree_add.comp hinputs + exact (computableInDegree_add.comp (hsum.prod hsum)).mono + · have hsum := ComputableInSpace.budget_natAdd + (ComputableInSpace.fst encNat encNat) (ComputableInSpace.snd encNat encNat) + exact ComputableInSpace.budget_natAdd hsum hsum From 12e5c8fd0c57e4403333d218ae43560f2c885751 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 11:04:03 -0400 Subject: [PATCH 5/8] chore(MultiTape): index shared addition certificate Canonical mk_all regeneration adds the one BinaryAddition import. Integrates #1631 worker A's quadratic-time/linear-space certificate, worker B's retained2/1 Degree/PPT/InSpace clients and worker C's actual carry/resource regressions. Source freeze for required full six-gate validation; outside-fleet review remains required for new resource statements and public carry certificates. No claim on the wider #1368/#862 objectives. AI-assisted integration by /root/review_mpc_api. --- Complexity.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Complexity.lean b/Complexity.lean index 227ff8d31..ac42bd0cf 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1590,6 +1590,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Halting.Partrec public import Complexity.Computability.Machines.Turing.MultiTape.Halting.Reduction public import Complexity.Computability.Machines.Turing.MultiTape.Halting.Rice public import Complexity.Computability.Machines.Turing.MultiTape.Halting.SMN +public import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryAddition public import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryComparison public import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryCounter public import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryPrimitives From 179d01f1cb0ffb8e3173e306bf68fe5aed27a57e Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 11:19:22 -0400 Subject: [PATCH 6/8] fix(MultiTape): import counted iteration in space proof owners Combining frozen addition 12e5c8fd0c57e4403333d218ae43560f2c885751 with actual main ab91dd674840c0a23b46c4af873142452bdccf7d cleanly produced merge 51ea02b9b6de9e33f73e6edddd3c68e387a49a7b, tree a155c4089a81302f0be5fa1dc0d9cec3c193fea4. Both arithmetic certificates now stop accidentally reexporting counted iteration. Strict InSpace checking reproduced the unknown ComputableInO.iterate at InSpace.lean:150. Its direct proof-only provider import fixed that owner; actual-client checking then reproduced the same missing name at InSpace/Plain.lean:213. Add a direct proof-only import in each owner. All other bytes in both modules, including declarations, proofs and budgets, are unchanged. No public reexport or arithmetic workaround. Validation on the actual-main composition: strict InSpace, InSpace.Plain, P2SchoolbookAddition and InSpacePlain PASS (3812 jobs); diff check PASS. Hygiene passed after the first import; the second adds only the same proof-only provider line. A read-only full-tree search found 17 direct ComputableInO.iterate consumers, all with provider routes after the fix. IndexFold and Universal.Machine retain valid explicit public import paths. The default integrated six gates remain with worker A. Abstract impact: none; only proof imports change, preserving public models, resource conventions, selected statements and declaration links. Diagnostic logs are retained in C's isolated checkout session; this commit records the exact composition, failures and validation. AI assistance: Codex worker /root/review_ready_c reproduced and fixed this #1631/#608 integration issue. This is implementation validation, not an independent review or human approval. --- .../Machines/Turing/MultiTape/Complexity/InSpace.lean | 1 + .../Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean | 1 + 2 files changed, 2 insertions(+) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean index f25bb455b..2f886f4a8 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean @@ -9,6 +9,7 @@ module public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LinearSpaceArith +import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCountedIteration /-! # Tidy computability within a space bound diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean index 33901d92e..f29fc656f 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean @@ -13,6 +13,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree.Bounds import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree.Primitives import Complexity.Computability.Machines.Turing.MultiTape.Internal.OLoops +import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCountedIteration /-! # Space bounds on plain machines From 8f2cfb64801522ad5a8075cb007871def13aa817 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 17:01:43 +0000 Subject: [PATCH 7/8] refactor(Machines): binary successor as one linear-time streaming transducer (#608) Prove binary successor on `encNat` once, by a two-state carry transducer: `computableInTimeAndSpace_succ` gives time `2 * (encNat n).length + 3` and zero work space. `ComputableInLinearTimeAndSpace.natSucc`, `ComputableInDegree.natSucc`, `ComputableInO.natSucc` and `computableTidilyInPolyTime_succ` are one-line weakenings of it. Delete the independent successor proofs: the fold-based proof of `ComputableInO.natSucc`, `computableTidilyInTimeAndSpace_succ` with its round lemmas `NatSucc.linear_succStep`/`linear_succFinish`, and the unused `Encodings/NatStream.lean` (`computableTidilyInTimeAndSpace_succ_stream`). Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 - .../Turing/MultiTape/Complexity/PolyTime.lean | 9 +- .../MultiTape/Complexity/Quantitative.lean | 6 + .../Turing/MultiTape/Encodings/Nat.lean | 138 +++++------------- .../Turing/MultiTape/Encodings/NatStream.lean | 117 --------------- .../MultiTape/Internal/BinaryPrimitives.lean | 31 ++-- ComplexityTests/Encodings.lean | 14 +- 7 files changed, 73 insertions(+), 243 deletions(-) delete mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatStream.lean diff --git a/Complexity.lean b/Complexity.lean index f121a534f..ce2039f8a 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1568,7 +1568,6 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.S public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Words public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatLength public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatPower -public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatStream public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Option public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Padding public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean index 11bd50bbb..c4a458a8f 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean @@ -12,6 +12,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds. public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Foldl public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Basic public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Combinators.TidyNormalForm /-! # Tidy computability in polynomial time @@ -281,10 +282,12 @@ public theorem ComputableTidilyInPolyTime.foldl {γ α β : Type u} {encIn : γ ((hlen.add (.const 1)).mul ((hmax.add hlMax').add (.const 1)))), (PolyBounded.const c).mul ((((hs₁.add hs₂).add hmax).add hlMax').add (.const 1)), h⟩ -/-- The successor is tidily computable in polynomial time, in the binary encoding `encNat`. -/ +/-- The successor is tidily computable in polynomial time, in the binary encoding `encNat`, from +the transducer certificate `computableInTimeAndSpace_succ`. -/ @[fun_prop] public theorem computableTidilyInPolyTime_succ : ComputableTidilyInPolyTime (· + 1) encNat encNat := - let ⟨c, h⟩ := computableTidilyInTimeAndSpace_succ - ⟨_, _, .of_forall_le c 2 (fun _ => le_rfl), .of_forall_le c 1 (fun _ => by simp), h⟩ + let ⟨c, h⟩ := computableInTimeAndSpace_succ.exists_computableTidilyInTimeAndSpace + ⟨_, _, .of_forall_le (c + 6) 1 (fun _ => by simp only [pow_one]; nlinarith), + .of_forall_le c 0 (fun _ => by simp), h⟩ end Turing.MultiTapeTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean index e051e45ed..7570c4bcb 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean @@ -34,6 +34,7 @@ Framed-list and option rules infer the payload encoding from the representation * `Turing.MultiTapeTM.ComputableInDegree.foldl'`, `Turing.MultiTapeTM.ComputableInDegree.foldlWith`: plain left folds with degree bounds. +* `Turing.MultiTapeTM.ComputableInDegree.natSucc`: binary successor with degrees one. * `Turing.MultiTapeTM.computableInDegree_add`, `Turing.MultiTapeTM.computableInDegree_mul`: plain binary addition (quadratic) and multiplication (cubic). * `Turing.MultiTapeTM.ComputableInO.comp_enc`: reuse a bit-word computation on encoded @@ -305,6 +306,11 @@ private lemma run_copy_fin3 (T : Transducer Bool (Fin 3)) (hT : ∀ b, T.step 2 | nil => simp [hf] | cons b w ih => simp [hT, ih] +/-- Binary successor has cost and output degree one, from the transducer certificate +`computableInTimeAndSpace_succ`. -/ +theorem natSucc : ComputableInDegree (· + 1) encNat encNat 1 1 := + of_linear .natSucc + /-- Adding one on unary-magnitude signed integers. -/ theorem int_succ : ComputableInDegree (· + 1) encInt encInt 1 1 := by refine of_linear (.of_transducer intSuccT fun z => ?_) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat.lean index 9587f63f8..c9e1f8bef 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat.lean @@ -8,31 +8,26 @@ module -- upstream: vendored crei:crei/tidy-universal @7f7c0696 (unsubmitted) public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Bits -public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Foldl public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Option public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair -import Mathlib.Data.Nat.Bitwise -import Mathlib.Tactic.Ring +public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds +import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelTransducer /-! # The successor in binary `encNat`, reexported from `Encodings.Nat.Bits`, encodes a natural number by its binary digits, least significant first (`Nat.bits`). -The successor is a left fold over the digits that keeps a carry and appends one digit per round, -followed by a final carry digit. Its tidy computability is derived from that of the fold -(`Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl`) and of the parts of a round. - -## Main definitions - -* `Turing.MultiTapeTM.encNat`: natural numbers encoded by their binary digits. -* `Turing.MultiTapeTM.encNat3`: triples of natural numbers encoded in binary. +The successor is computed by one streaming transducer whose state is the carry: on each digit `b` +in carry `c` it emits `c ^^ b` and keeps the carry `c && b`, and at the end it emits a final `1` +exactly when a carry remains. The machine reads its input once and uses no work tape. ## Main results -* `Turing.MultiTapeTM.computableTidilyInTimeAndSpace_succ`: the successor is tidily computable in - quadratic time and linear space. +* `Turing.MultiTapeTM.computableInTimeAndSpace_succ`: the successor is computable within + `2 * (encNat n).length + 3` steps and zero work space. +* `Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.natSucc`: its linear form. -/ namespace Turing.MultiTapeTM @@ -42,96 +37,39 @@ public abbrev encNat3 : ℕ × ℕ × ℕ ↪ List Bool := encPair encNat (encPa namespace NatSucc -open ComputableInLinearTimeAndSpace - -/-- A round is tidily computable in linear time and space. -/ -public lemma linear_succStep : - ComputableTidilyInLinearTimeAndSpace (fun p => succStep p.1 p.2) - (encPair encAcc encBool) encAcc := by - apply Internal.NormalForm.linear - have hacc : ComputableInLinearTimeAndSpace Prod.fst (encPair encAcc encBool) encAcc := - PairEncoding.fst encBool - have hcarry : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool => p.1.1) - (encPair encAcc encBool) encBool := - (PairEncoding.fst encBits).comp hacc - have hdigit : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool => p.2) - (encPair encAcc encBool) encBool := - PairEncoding.snd encAcc - have hdigits : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool => p.1.2) - (encPair encAcc encBool) encBits := - (PairEncoding.snd encBool).comp hacc - have hand : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool => - p.1.1 && p.2) (encPair encAcc encBool) encBool := by - convert hdigit.ite (hcarry.restrict _) ((const false).restrict _) using 1 - funext p - cases p.2 <;> simp - have hnot : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool => !p.1.1) - (encPair encAcc encBool) encBool := by - convert hcarry.ite ((const false).restrict _) ((const true).restrict _) using 1 - funext p - cases p.1.1 <;> rfl - have hxor : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool => - p.1.1 ^^ p.2) (encPair encAcc encBool) encBool := by - convert hdigit.ite (hnot.restrict _) (hcarry.restrict _) using 1 - funext p - cases p.2 <;> simp - exact hand.pair (hdigits.append hxor (encOut := encBits) fun _ => rfl) - -/-- The final carry digit is appended in linear time and space. -/ -public lemma linear_succFinish : - ComputableTidilyInLinearTimeAndSpace succFinish encAcc encBits := by - apply Internal.NormalForm.linear - have hdigits : ComputableInLinearTimeAndSpace Prod.snd encAcc encBits := - PairEncoding.snd encBool - have happend : ComputableInLinearTimeAndSpace (fun p => p.2 ++ [true]) encAcc encBits := - hdigits.append (const (encMid := encBool) true) (encOut := encBits) fun _ => rfl - have hcarry : ComputableInLinearTimeAndSpace Prod.fst encAcc encBool := - PairEncoding.fst encBits - exact hcarry.ite (happend.restrict _) (hdigits.restrict _) +/-- The successor as a transducer: the state is the carry, initially set. -/ +private def succTransducer : Transducer Bool Bool where + q₀ := true + step c b := (c && b, [c ^^ b]) + final c := if c then [true] else [] + length_step_le _ _ := by simp + length_final_le c := by cases c <;> simp + +private lemma run_succTransducer (c : Bool) (l : List Bool) : + succTransducer.run c l = incr c l := by + induction l generalizing c with + | nil => cases c <;> rfl + | cons b l ih => + rw [Transducer.run_cons, ih] + cases c <;> cases b <;> simp [succTransducer, incr] end NatSucc open NatSucc in -/-- The successor is tidily computable in quadratic time and linear space, in the binary encoding -`encNat`. -/ -public theorem computableTidilyInTimeAndSpace_succ : - ∃ c, ComputableTidilyInTimeAndSpace (· + 1) encNat encNat - (fun n => c * ((encNat n).length + 1) ^ 2) (fun n => c * ((encNat n).length + 1)) := by - obtain ⟨cl, hlist⟩ := ComputableTidilyInLinearTimeAndSpace.of_eq (f := Nat.bits) - (encIn := encNat) (encMid := encBits) fun _ => rfl - obtain ⟨ci, hinit⟩ := ComputableTidilyInLinearTimeAndSpace.const (encIn := encNat) - (encMid := encAcc) (true, []) - obtain ⟨cs, hstep⟩ := linear_succStep - -- the bounds of a round and of the state of the fold - have hlen (n i : ℕ) : (((n.bits.take i).foldl succStep (true, [])).2).length ≤ n.bits.length := by - rw [length_foldl_succStep] - simp - obtain ⟨cf, hfold⟩ := ComputableTidilyInTimeAndSpace.foldl (encA := encBool) (encL := encBits) - (encBA := encPair encAcc encBool) (encS := encPair encBits encAcc) - (encO := encOption (encPair encBits encAcc)) - (hlist.mono (t' := fun n => (cl + ci) * ((encNat n).length + 1)) - (s' := fun n => (cl + ci) * ((encNat n).length + 1)) - (fun n => by ring_nf; omega) (fun n => by ring_nf; omega)) - (hinit.mono (fun n => by ring_nf; omega) (fun n => by ring_nf; omega)) hstep - (tMax := fun n => cs * (2 * (encNat n).length + 9)) - (sMax := fun n => cs * (2 * (encNat n).length + 9)) - (lMax := fun n => 2 * (encNat n).length + 4) - (fun n i _ => Nat.mul_le_mul_left cs (by simp; have := hlen n i; omega)) - (fun n i _ => Nat.mul_le_mul_left cs (by simp; have := hlen n i; omega)) - (fun n i hi => by simp [length_foldl_succStep]; omega) - obtain ⟨cg, hfinish⟩ := linear_succFinish - -- vendored: crei's `comp` is `comp_linear` here, as cslib #1111 restates `comp` - obtain ⟨cc, h⟩ := ComputableTidilyInTimeAndSpace.comp_linear hfinish hfold - obtain ⟨k, S, _, tm, htm⟩ := h - refine ⟨cf * (cl + ci + 9 * cs + 5) + 4 * (cg + cc), k, S, inferInstance, tm, fun n => ?_⟩ - have hmid : (encAcc (n.bits.foldl succStep (true, []))).length = n.bits.length + 3 := by - rw [length_encAcc, length_foldl_succStep] - simp - change tm.ComputesTidilyInTimeAndSpace _ (n + 1).bits _ _ - rw [bits_succ_eq_foldl] - refine (htm n).mono ?_ ?_ <;> - · simp only [hmid, encNat_apply] - ring_nf - omega +/-- **Binary successor in linear time and zero work space.** One streaming transducer computes +`n + 1` from `encNat n` within `2 * (encNat n).length + 3` steps without work tapes. -/ +public theorem computableInTimeAndSpace_succ : + ComputableInTimeAndSpace (· + 1) encNat encNat (fun n => 2 * (encNat n).length + 3) + (fun _ => 0) := + ⟨0, _, inferInstance, succTransducer.toTM, fun n => by + rw [encNat_apply, encNat_apply, bits_succ, ← run_succTransducer] + exact succTransducer.computesInTimeAndSpace_toTM n.bits⟩ + +/-- Binary successor in linear time and work space, from `computableInTimeAndSpace_succ`. -/ +public theorem ComputableInLinearTimeAndSpace.natSucc : + ComputableInLinearTimeAndSpace (· + 1) encNat encNat := + let ⟨k, Q, hQ, tm, h⟩ := computableInTimeAndSpace_succ + ⟨3, k, Q, hQ, tm, fun n => + ⟨(h n).1, (h n).2.1.mono (by dsimp; omega), (h n).2.2.mono (Nat.zero_le _)⟩⟩ end Turing.MultiTapeTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatStream.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatStream.lean deleted file mode 100644 index bb7508453..000000000 --- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatStream.lean +++ /dev/null @@ -1,117 +0,0 @@ -/- -Copyright (c) 2026 Christian Reitwiessner. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Christian Reitwiessner --/ - -module --- upstream: vendored crei:crei/tidy-universal @7f7c0696 (unsubmitted) - -public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat -public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.StreamFold -import Mathlib.Tactic.Linarith - -/-! -# The successor in binary, as a streaming fold - -The successor on `Turing.MultiTapeTM.encNat` reads the digits once, least significant first, -keeping the carry as its state: it emits each digit plus the carry and, at the end, a final carry -digit. As a streaming fold (`Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.streamFold`) it is -tidily computable in linear time and constant space. - -## Main results - -* `Turing.MultiTapeTM.computableTidilyInTimeAndSpace_succ_stream`: the successor is tidily - computable in linear time and constant space. --/ - -namespace Turing.MultiTapeTM - -namespace NatStream - -open NatSucc - -/-- Reads one digit and emits it. -/ -def digitReader : InputReader Bool Unit := ⟨(), fun _ b => (none, some b)⟩ - -/-- The carry after a digit. -/ -def carry (p : Bool × Bool) : Bool := p.1 && p.2 - -/-- The digit plus the carry. -/ -def sumDigit (p : Bool × Bool) : Bool := p.1 ^^ p.2 - -/-- The final carry digit. -/ -def finalDigit (c : Bool) : List Bool := if c then [true] else [] - -lemma streamEmit_append_finalDigit (c : Bool) (l : List Bool) : - streamEmit carry (fun p => encBool (sumDigit p)) c l ++ - encBits (finalDigit (streamState c carry l l.length)) = incr c l := by - induction l generalizing c with - | nil => cases c <;> rfl - | cons b l ih => - have h := ih (c && b) - simp only [streamEmit, streamState, List.length_cons, List.take_succ_cons, List.foldl_cons, - List.take_length] at h ⊢ - cases c <;> cases b <;> simp_all [incr, carry, sumDigit] - -open ComputableTidilyInLinearTimeAndSpace in -/-- The parts of a round, on the carry and a digit, in linear time and space. -/ -lemma linear_parts : - ComputableTidilyInLinearTimeAndSpace carry (encPair encBool encBool) encBool ∧ - ComputableTidilyInLinearTimeAndSpace sumDigit (encPair encBool encBool) encBool := by - have hc : ComputableTidilyInLinearTimeAndSpace Prod.fst (encPair encBool encBool) encBool := - Internal.NormalForm.linear (PairEncoding.fst encBool) - have hd : ComputableTidilyInLinearTimeAndSpace Prod.snd (encPair encBool encBool) encBool := - Internal.NormalForm.linear (PairEncoding.snd encBool) - have hnot : ComputableTidilyInLinearTimeAndSpace (fun p : Bool × Bool => !p.1) - (encPair encBool encBool) encBool := by - convert hc.ite ((const false).restrict _) ((const true).restrict _) using 1 - funext ⟨a, b⟩ - cases a <;> rfl - refine ⟨?_, ?_⟩ - · convert hd.ite (hc.restrict _) ((const false).restrict _) using 1 - funext ⟨a, b⟩ - cases a <;> cases b <;> rfl - · convert hd.ite (hnot.restrict _) (hc.restrict _) using 1 - funext ⟨a, b⟩ - cases a <;> cases b <;> rfl - -open ComputableTidilyInLinearTimeAndSpace in -lemma linear_finalDigit : ComputableTidilyInLinearTimeAndSpace finalDigit encBool encBits := by - convert (of_eq (f := id) (encIn := encBool) (encMid := encBool) fun _ => rfl).ite - ((const [true]).restrict _) ((const []).restrict _) using 1 - funext c - cases c <;> rfl - -end NatStream - -open NatSucc NatStream in -/-- The successor is tidily computable in linear time and constant space, in the binary encoding -`encNat`. -/ -public theorem computableTidilyInTimeAndSpace_succ_stream : - ∃ c, ComputableTidilyInTimeAndSpace (· + 1) encNat encNat - (fun n => c * ((encNat n).length + 1)) (fun _ => c) := by - obtain ⟨cI, hI⟩ := computableInTimeAndSpace_of_const (encIn := encNat) (encOut := encBool) true - obtain ⟨⟨cN, hN⟩, ⟨cE, hE⟩⟩ := linear_parts - obtain ⟨cF, hF⟩ := linear_finalDigit - have hpair (p : Bool × Bool) : (encPair encBool encBool p).length = 4 := by simp - obtain ⟨c, h⟩ := ComputableTidilyInTimeAndSpace.streamFold (g := (· + 1)) (encOut := encNat) - digitReader (fun b => [b]) - (fun _ => List.cons_ne_nil _ _) (fun a rest => by simp [digitReader, InputReader.read]) - Nat.bits (fun n => by simp) hI.computableTidilyInTimeAndSpace hN hE hF - (fun n => by - change (n + 1).bits = _ - rw [bits_succ, ← streamEmit_append_finalDigit] - rfl) - (tMax := fun _ => 5 * (cN + cE)) (sMax := fun _ => 5 * (cN + cE)) (lMax := fun _ => 4) - (fun _ _ _ => by simp only [hpair]; omega) (fun _ _ _ => by simp only [hpair]; omega) - (fun _ _ _ => by simp) (fun _ _ _ => by simp) - refine ⟨c * (2 * cI + 2 * cF + 5 * (cN + cE) + 20), h.mono (fun n => ?_) (fun n => ?_)⟩ - · simp only [encBool_apply, List.length_singleton, encNat_apply] - rw [Nat.mul_assoc] - refine Nat.mul_le_mul_left c ?_ - nlinarith - · simp only [encBool_apply, List.length_singleton] - exact Nat.mul_le_mul_left c (by omega) - -end Turing.MultiTapeTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean index ffe6bb41e..38a816b7f 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean @@ -8,21 +8,24 @@ module -- upstream: candidate public import Complexity.Computability.Machines.Turing.MultiTape.Internal.OLoops -public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Bits +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat import Mathlib.Tactic.Linarith import Mathlib.Tactic.Ring /-! # Direct binary counter resource certificates -The original carry, borrow and leading-zero normalization folds compute successor and predecessor. -Their time is quadratic and their charged workspace linear in the binary input length. The zero -test uses the existing empty-word machine. All round certificates are plain; normalization occurs -only when the internal machine combinators construct the fold. +The original borrow and leading-zero normalization folds compute the predecessor. Its time is +quadratic and its charged workspace linear in the binary input length. The successor's +certificate here is a weakening of the streaming transducer `computableInTimeAndSpace_succ`; the +carry rounds remain as the shared step of binary addition. The zero test uses the existing +empty-word machine. All round certificates are plain; normalization occurs only when the internal +machine combinators construct the fold. ## Main results -* `ComputableInO.succStep`, `ComputableInO.succFinish`: shared linear carry-round certificates. +* `ComputableInO.succStep`, `ComputableInO.succFinish`: shared linear carry-round certificates + for binary addition. * `ComputableInO.natSucc`, `ComputableInO.natPred`: quadratic-time, linear-space binary counters. * `ComputableInO.natIsZero`: linear zero testing. -/ @@ -143,19 +146,13 @@ theorem foldl_bits {β : Type} {encB : β ↪ List Bool} {init : β} {step : β · simp only [encBits_apply] nlinarith -/-- Binary successor with the original quadratic clock and linear output-charged workspace. -/ +/-- Binary successor within the quadratic clock and linear charged workspace used by its +clients, weakened from the linear-time, zero-work-space transducer certificate +`computableInTimeAndSpace_succ`. -/ theorem natSucc : ComputableInO (· + 1) encNat encNat (fun n => ((encNat n).length + 1) ^ 2) - (fun n => (encNat n).length + 1) := by - have hfold := foldl_bits (init := (true, [])) succStep 3 fun l i => by - rw [NatSucc.length_encAcc, NatSucc.length_foldl_succStep] - simp only [List.length_nil, Nat.zero_add] - have := List.length_take_le' i l - omega - have h := (succFinish.comp_linear hfold).of_encIn_eq (encD := encNat) Nat.bits (fun _ => rfl) - refine h.of_enc_eq fun n => ?_ - simp only [encNat_apply, encBits_apply, Function.comp_apply, NatSucc.succFinish_foldl, - List.nil_append, NatSucc.bits_succ] + (fun n => (encNat n).length + 1) := + (of_linear .natSucc).mono_le (fun n => by simp only [encNat_apply]; nlinarith) fun _ => by omega /-- Binary predecessor keeps zero at zero and preserves the original independent resource bounds. -/ theorem natPred : diff --git a/ComplexityTests/Encodings.lean b/ComplexityTests/Encodings.lean index a3b506811..91f45fb43 100644 --- a/ComplexityTests/Encodings.lean +++ b/ComplexityTests/Encodings.lean @@ -8,6 +8,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Encoding +import Complexity.Computability.Machines.Turing.MultiTape.Internal.ResourceFacts /-! # Tests for the framed encodings @@ -27,10 +28,13 @@ example : encList encBool [true, false] = [true, true, false, true, false, false example (w u : List Bool) : unframe (frame w ++ u) = w := unframe_frame_append w u -- Binary successor can expose its raw output word with precisely the same time/space bounds. -example : ∃ c, ComputableTidilyInTimeAndSpace (fun n : ℕ => encNat (n + 1)) encNat encBits - (fun n => c * ((encNat n).length + 1) ^ 2) - (fun n => c * ((encNat n).length + 1)) := - let ⟨c, h⟩ := computableTidilyInTimeAndSpace_succ - ⟨c, h.of_enc_eq fun _ => rfl⟩ +example : ComputableInTimeAndSpace (fun n : ℕ => encNat (n + 1)) encNat encBits + (fun n => 2 * (encNat n).length + 3) (fun _ => 0) := + let ⟨k, Q, hQ, tm, h⟩ := computableInTimeAndSpace_succ + ⟨k, Q, hQ, tm, h⟩ + +-- The encoded successor, one digit longer after a carry out, is written within the linear clock. +example (n : ℕ) : (encNat (n + 1)).length ≤ 2 * (encNat n).length + 3 := + computableInTimeAndSpace_succ.length_le n end ComplexityTests.Encodings From 8046a251d583ae779b037ba7e1d7e6687392a411 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 17:11:28 +0000 Subject: [PATCH 8/8] chore(scripts): lower tidy baseline after successor consolidation (#608) Co-Authored-By: Claude Opus 5.5 --- scripts/tidy_surface_baseline.json | 2 -- 1 file changed, 2 deletions(-) diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json index 3611268f6..3e9ba0f44 100644 --- a/scripts/tidy_surface_baseline.json +++ b/scripts/tidy_surface_baseline.json @@ -54,9 +54,7 @@ "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Translate.lean": 2, "Complexity/Computability/Machines/Turing/MultiTape/Encodings/Basic.lean": 7, "Complexity/Computability/Machines/Turing/MultiTape/Encodings/MultiPass.lean": 1, - "Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat.lean": 3, "Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatPower.lean": 1, - "Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatStream.lean": 1, "Complexity/Computability/Machines/Turing/MultiTape/Encodings/StreamFold.lean": 4, "Complexity/Computability/Machines/Turing/MultiTape/Halting/Computable.lean": 5, "Complexity/Computability/Machines/Turing/MultiTape/Halting/Rice.lean": 2,