diff --git a/Complexity.lean b/Complexity.lean
index 79d3065071..459dcfccef 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1439,6 +1439,7 @@ public import Complexity.Crypto.Computational.Homomorphic.GSW.DecryptionCircuit.
 public import Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters
 public import Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters.Scheme
 public import Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters.Security
+public import Complexity.Crypto.Computational.Homomorphic.GSW.FullyHomomorphic
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Gadget
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Hiding
 public import Complexity.Crypto.Computational.Homomorphic.GSW.LWE
diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean
new file mode 100644
index 0000000000..fdba4c2dda
--- /dev/null
+++ b/Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.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
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters.Scheme
+public import Complexity.Crypto.Computational.Homomorphic.Leveled.Bootstrapping
+public import Complexity.Crypto.Computational.Homomorphic.FixedKey.Bootstrapping
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
+
+/-!
+# Fully homomorphic encryption from GSW and decision LWE
+
+Gentry's generic bootstrapping constructions are instantiated with GSW at the logarithmic-depth
+parameter family. The base scheme is `DepthParameters.scheme`, its decryption circuits are the
+actual raw-input decryptors, and its bootstrappability, correctness, widths and native runtime
+are proved without computational assumptions. Bootstrappability is for Gentry's gate set
+Γ = {identity, NAND}: the schemes evaluate De Morgan circuits by compiling each De Morgan level
+into two NAND levels.
+
+The security premise is decision LWE for exactly this family: secret dimension `λ + 1`,
+centered-binomial noise of width `λ + 1`, and the quasi-polynomial modulus `2 ^ (16384 * t ^ 2)`
+with `t = 1 + ⌈log₂ (λ + 2)⌉`.
+
+* **Leveled FHE.** One polynomial-size decryption circuit family, one natively computable
+  decryption algorithm and fixed polynomial widths are chosen first. Then every polynomially
+  bounded depth family is covered by an actual scheme with that decryption algorithm, assuming
+  only decision LWE [Gentry2009, Definition 3 and Theorem 3]. Security is asymptotic IND-CPA, a
+  consequence of [Gentry2009, Theorem 4] without its exact loss. Native certificates are uniform
+  for each depth family; key generation reads only the unary security parameter.
+* **Fully homomorphic encryption.** The one-key self-loop construction evaluates every circuit,
+  assuming decision LWE for this family *and* the separate one-key circular-security assumption
+  `Encryption.CircularSecure` for the base scheme [Gentry2009, Section 2, the self-loop
+  construction]. This is a one-key specialization of the KDM security Gentry assumes there.
+  Circular security is not derived from LWE.
+
+Neither theorem asserts lattice hardness, a worst-case reduction, circuit privacy, or an exact
+concrete-security loss.
+
+## Main results
+
+* `Cslib.Crypto.Homomorphic.GSW.DepthParameters.exists_leveled_of_decisionLWE`: leveled FHE.
+* `Cslib.Crypto.Homomorphic.GSW.DepthParameters.fullyHomomorphic_of_decisionLWE_of_circularSecure`:
+  FHE under the additional circular-security assumption.
+
+## References
+
+* [C. Gentry, *Fully homomorphic encryption using ideal lattices*, Section 2, Definitions 1–5,
+  Theorems 3 and 4 and the self-loop construction][Gentry2009]
+* [C. Gentry, A. Sahai and B. Waters, Sections 3.2–3.4][GentrySahaiWaters2013]
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.Homomorphic.GSW.DepthParameters
+
+open Circuits Probability Turing.MultiTapeTM
+open Parameters (dimension noise)
+
+/-- Leveled FHE from GSW under decision LWE for this family, with quasi-polynomial modulus.
+One polynomial-size circuit family computes the common decryption algorithm
+`Leveled.decrypt decryptionCircuits`, which is natively computable, and the key and ciphertext
+widths are fixed polynomials; all of these are chosen before the depth. Every polynomially
+bounded depth family is then covered by an actual scheme with an efficiently computable budget
+and exactly that decryption algorithm: it is correct for every circuit of the requested depth,
+has the fixed widths, native algorithms and IND-CPA security. No circular-security assumption is
+used. -/
+theorem exists_leveled_of_decisionLWE
+    (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) (noise k))) :
+    ∃ circuits : ∀ k, Circuit Boolean.signature
+        ((3 * secretWidth k + 1) + (ciphertextWidth k + 1)) 1,
+      PolynomiallyBounded (fun k => (circuits k).size) ∧
+      (∀ k (sk ciphertext : List Bool), sk.length = 3 * secretWidth k + 1 →
+        ciphertext.length = ciphertextWidth k + 1 →
+        (circuits k).eval Boolean.interpretation
+            (BitString.ofList ((3 * secretWidth k + 1) + (ciphertextWidth k + 1))
+              (sk ++ ciphertext)) 0 =
+          Leveled.decrypt decryptionCircuits k sk ciphertext) ∧
+      ComputableInPolyTime
+        (fun p : ℕ × List Bool × List Bool => Leveled.decrypt decryptionCircuits p.1 p.2.1 p.2.2)
+        (encPair encUnary (encPair encBits encBits)) encBool ∧
+      PolynomiallyBounded (fun k => 3 * secretWidth k + 1) ∧
+      PolynomiallyBounded (fun k => ciphertextWidth k + 1) ∧
+      ∀ depth : ℕ → ℕ, PolynomiallyBounded depth →
+        ∃ budget : ℕ → ℕ,
+          ComputableInPolyTime budget encUnary encUnary ∧
+          (∀ k, depth k ≤ budget k) ∧
+          (Leveled.scheme decryptionCircuits budget).decrypt =
+            Leveled.decrypt decryptionCircuits ∧
+          (Leveled.scheme decryptionCircuits budget).Correct ∧
+          (∀ k c, c.2.depth ≤ depth k → (Leveled.scheme decryptionCircuits budget).permitted k c) ∧
+          (Leveled.scheme decryptionCircuits budget).FixedWidth (fun k => 3 * secretWidth k + 1)
+            (fun k => ciphertextWidth k + 1) ∧
+          IsPPTOn encUnary (encPair encBits encBits)
+            (Leveled.scheme decryptionCircuits budget).keyGen ∧
+          IsPPTOn (encPair encUnary (encPair encBits encBool)) encBits
+            (fun p => (Leveled.scheme decryptionCircuits budget).encrypt p.1 p.2.1 p.2.2) ∧
+          IsPPTOn
+            (encPair encUnary (encPair encBits
+              (encPair (Boolean.encCircuit 1) (encList encBits))))
+            encBits
+            (fun p =>
+              (Leveled.scheme decryptionCircuits budget).evaluate p.1 p.2.1 p.2.2.1 p.2.2.2) ∧
+          Encryption.INDCPA (Leveled.scheme decryptionCircuits budget).keyGen
+            (Leveled.scheme decryptionCircuits budget).encrypt := by
+  have hD := computableInPolyTime_decryptionCircuits.tidy
+  obtain ⟨circuits, hsize, hcircuits⟩ := Leveled.exists_decrypt_circuits decryptionCircuits hD
+  have hdecrypt := (Leveled.computableTidilyInPolyTime_scheme_decrypt decryptionCircuits hD
+    (fun _ => 0)).computableInPolyTime
+  obtain ⟨hsecret, hciphertext⟩ := Leveled.polynomiallyBounded_widths decryptionCircuits hD
+  refine ⟨circuits, hsize, fun k sk c hsk hc => hcircuits (fun _ => 0) k sk c hsk hc, hdecrypt,
+    hsecret, hciphertext, fun depth hdepth => ?_⟩
+  obtain ⟨budget, hbudget, hle, hcorrect, hpermitted, hwidth, -, -, hkeyGen, hencrypt, -,
+      hevaluate, hsecure⟩ :=
+    Leveled.exists_scheme_of_polynomiallyBounded decryptionCircuits correct fixedWidth
+      bootstrappable (indCPA_scheme hLWE) isPPTOn_keyGen isPPTOn_encrypt isPPTOn_evaluate hD
+      hdepth
+  exact ⟨budget, hbudget.computableInPolyTime, hle, rfl, hcorrect, hpermitted, hwidth, hkeyGen,
+    hencrypt, hevaluate, hsecure⟩
+
+/-- Fully homomorphic encryption from GSW: under decision LWE for this family, with
+quasi-polynomial modulus, and the explicit one-key circular-security assumption for the base
+scheme, the self-loop construction correctly evaluates every finite circuit. Its widths are those
+of GSW, its decryption circuits have polynomial size, its four algorithms are native, and it is
+IND-CPA. -/
+theorem fullyHomomorphic_of_decisionLWE_of_circularSecure
+    (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) (noise k)))
+    (hcircular : Encryption.CircularSecure scheme.keyGen scheme.encrypt) :
+    (FixedKey.scheme decryptionCircuits).Correct ∧
+      (∀ k c, (FixedKey.scheme decryptionCircuits).permitted k c) ∧
+      (FixedKey.scheme decryptionCircuits).FixedWidth secretWidth ciphertextWidth ∧
+      PolynomiallyBounded secretWidth ∧ PolynomiallyBounded ciphertextWidth ∧
+      PolynomiallyBounded
+        (fun k => ((FixedKey.decryptionCircuits decryptionCircuits).circuit k).size) ∧
+      IsPPTOn encUnary (encPair encBits encBits) (FixedKey.scheme decryptionCircuits).keyGen ∧
+      IsPPTOn (encPair encUnary (encPair encBits encBool)) encBits
+        (fun p => (FixedKey.scheme decryptionCircuits).encrypt p.1 p.2.1 p.2.2) ∧
+      ComputableInPolyTime
+        (fun p : ℕ × List Bool × List Bool =>
+          (FixedKey.scheme decryptionCircuits).decrypt p.1 p.2.1 p.2.2)
+        (encPair encUnary (encPair encBits encBits)) encBool ∧
+      IsPPTOn
+        (encPair encUnary (encPair encBits
+          (encPair (Boolean.encCircuit 1) (encList encBits))))
+        encBits
+        (fun p => (FixedKey.scheme decryptionCircuits).evaluate p.1 p.2.1 p.2.2.1 p.2.2.2) ∧
+      Encryption.INDCPA (FixedKey.scheme decryptionCircuits).keyGen
+        (FixedKey.scheme decryptionCircuits).encrypt := by
+  obtain ⟨hcorrect, hpermitted, hwidth, hsecret, hciphertext, hsize, hkeyGen, hencrypt,
+      hdecrypt, hevaluate, hsecure⟩ :=
+    FixedKey.fullyHomomorphic decryptionCircuits correct fixedWidth bootstrappable
+      (indCPA_scheme hLWE) hcircular isPPTOn_keyGen isPPTOn_encrypt isPPTOn_evaluate
+      computableInPolyTime_decryptionCircuits.tidy
+  exact ⟨hcorrect, hpermitted, hwidth, hsecret, hciphertext, hsize, hkeyGen, hencrypt,
+    hdecrypt.computableInPolyTime, hevaluate, hsecure⟩
+
+end Cslib.Crypto.Homomorphic.GSW.DepthParameters
diff --git a/ComplexityTests/Crypto/GSWFullyHomomorphic.lean b/ComplexityTests/Crypto/GSWFullyHomomorphic.lean
new file mode 100644
index 0000000000..af4a9ed19b
--- /dev/null
+++ b/ComplexityTests/Crypto/GSWFullyHomomorphic.lean
@@ -0,0 +1,89 @@
+/-
+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.Crypto.Computational.Homomorphic.GSW.FullyHomomorphic
+
+/-!
+Clients of the concrete GSW endpoints. The base widths are computed at security parameter zero.
+Under the stated assumptions, the leveled scheme for a constant depth family and the fixed-key
+scheme both evaluate the actual compiled NAND circuit correctly on fresh encryptions. The
+decision-LWE and circular-security premises remain hypotheses; nothing here instantiates them.
+-/
+
+namespace ComplexityTests.Crypto.GSWFullyHomomorphic
+
+open Cslib Cslib.Crypto Cslib.Circuits Cslib.Circuits.Boolean Cslib.Crypto.Homomorphic
+open Cslib.Crypto.Homomorphic.GSW Cslib.Crypto.Homomorphic.GSW.DepthParameters
+open Cslib.Probability
+open Parameters (dimension noise)
+
+-- At security parameter zero the base secret holds one 65536-bit residue, and a ciphertext is a
+-- square bit matrix with `2 * 65536` rows. The leveled widths add only an endpoint secret pair
+-- and a tag, whatever the depth budget.
+example : secretWidth 0 = 65536 ∧ ciphertextWidth 0 = 131072 ^ 2 ∧
+    3 * secretWidth 0 + 1 = 196609 := by
+  decide +kernel
+
+/-- Under decision LWE alone, one leveled scheme evaluates the compiled NAND circuit, whose
+depth is two, on all supported fresh encryptions. -/
+example (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) (noise k))) :
+    ∃ budget : ℕ → ℕ, ∀ k keys,
+      keys ∈ (ProbComp.eval ((Leveled.scheme decryptionCircuits budget).keyGen k)).support →
+      ∀ a b inputs, (Leveled.scheme decryptionCircuits budget).FreshInputs k keys.1 [a, b] inputs →
+      ∀ c ∈ (ProbComp.eval
+          ((Leveled.scheme decryptionCircuits budget).evaluate k keys.1 ⟨2, nandCircuit⟩
+            inputs)).support,
+        (Leveled.scheme decryptionCircuits budget).decrypt k keys.2 c = !(a && b) := by
+  obtain ⟨-, -, -, -, -, -, hleveled⟩ := exists_leveled_of_decisionLWE hLWE
+  obtain ⟨budget, -, -, -, hcorrect, hpermitted, -⟩ := hleveled _ (PolynomiallyBounded.const 2)
+  refine ⟨budget, fun k keys hkeys a b inputs hinputs c hc => ?_⟩
+  have h := hcorrect.decrypt_evaluate k keys hkeys ⟨2, nandCircuit⟩
+    (hpermitted k _ (by decide +kernel)) [a, b] inputs rfl hinputs c hc
+  rw [h, eval_nandCircuit]
+  rfl
+
+/-- The schemes for two different depth families share one decryption algorithm, computed by one
+polynomial-size circuit family chosen before either depth, as in Gentry's Definition 3. -/
+example (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) (noise k))) :
+    ∃ circuits : ∀ k, Circuit Boolean.signature
+        ((3 * secretWidth k + 1) + (ciphertextWidth k + 1)) 1,
+      PolynomiallyBounded (fun k => (circuits k).size) ∧
+      ∃ shallow deep : ℕ → ℕ, (∀ k, 2 ≤ shallow k ∧ k ≤ deep k) ∧
+        (Leveled.scheme decryptionCircuits shallow).decrypt =
+          (Leveled.scheme decryptionCircuits deep).decrypt ∧
+        ∀ k sk c, sk.length = 3 * secretWidth k + 1 → c.length = ciphertextWidth k + 1 →
+          (circuits k).eval Boolean.interpretation
+              (BitString.ofList ((3 * secretWidth k + 1) + (ciphertextWidth k + 1)) (sk ++ c)) 0 =
+            (Leveled.scheme decryptionCircuits deep).decrypt k sk c := by
+  obtain ⟨circuits, hsize, hcircuits, -, -, -, hleveled⟩ := exists_leveled_of_decisionLWE hLWE
+  obtain ⟨shallow, -, hshallow, hdecShallow, -⟩ := hleveled _ (PolynomiallyBounded.const 2)
+  obtain ⟨deep, -, hdeep, hdecDeep, -⟩ := hleveled _ PolynomiallyBounded.id
+  refine ⟨circuits, hsize, shallow, deep, fun k => ⟨hshallow k, hdeep k⟩,
+    hdecShallow.trans hdecDeep.symm, fun k sk c hsk hc => ?_⟩
+  rw [hdecDeep]
+  exact hcircuits k sk c hsk hc
+
+/-- With the additional circular-security premise, the fixed-key scheme permits the NAND circuit
+at every security parameter and evaluates it correctly, with no depth budget in key generation. -/
+example (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) (noise k)))
+    (hcircular : Encryption.CircularSecure scheme.keyGen scheme.encrypt) (k : ℕ)
+    (keys : List Bool × List Bool)
+    (hkeys : keys ∈ (ProbComp.eval ((FixedKey.scheme decryptionCircuits).keyGen k)).support)
+    (a b : Bool) (inputs : List (List Bool))
+    (hinputs : (FixedKey.scheme decryptionCircuits).FreshInputs k keys.1 [a, b] inputs)
+    (c : List Bool) (hc : c ∈ (ProbComp.eval
+      ((FixedKey.scheme decryptionCircuits).evaluate k keys.1 ⟨2, nandCircuit⟩ inputs)).support) :
+    (FixedKey.scheme decryptionCircuits).decrypt k keys.2 c = !(a && b) ∧
+      c.length = ciphertextWidth k := by
+  obtain ⟨hcorrect, hpermitted, hwidth, -⟩ :=
+    fullyHomomorphic_of_decisionLWE_of_circularSecure hLWE hcircular
+  refine ⟨?_, hwidth.evaluate_length k keys hkeys _ (hpermitted k _) [a, b] inputs rfl hinputs c
+    hc⟩
+  rw [hcorrect.decrypt_evaluate k keys hkeys _ (hpermitted k _) [a, b] inputs rfl hinputs c hc,
+    eval_nandCircuit]
+  rfl
+
+end ComplexityTests.Crypto.GSWFullyHomomorphic
diff --git a/ROADMAP.md b/ROADMAP.md
index 7062df1633..c55e3f271a 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -60,13 +60,12 @@ Priorities live in this list and in the tiers of [#897].
   polynomial-length messages. Authentication trees from one-time signatures and
   collision-resistant hashing are an intermediate development step; for the theorem itself,
   universal one-way hash functions replace the collision-resistance assumption.
-- **Gentry's bootstrapping, instantiated** ([#486]). A concrete LWE-based scheme satisfying the
-  correctness, security, bootstrappability and native-efficiency hypotheses of the generic
-  theorem: full native evaluation of the augmented GSW decryption circuit, bootstrappability
-  with compatible parameters, and the joint circular-security assumption needed for the
-  fixed-key endpoint. Further targets: a uniform generator for the leveled scheme's wrapper
-  decryption circuits (uniform compactness), reuse of evaluated ciphertexts as fresh inputs
-  (multi-hop evaluation), and Gentry's exact concrete-security loss.
+- **Gentry's bootstrapping, instantiated** ([#486]). GSW at its logarithmic-depth parameter
+  family instantiates the generic theorem: leveled FHE under decision LWE with quasi-polynomial
+  modulus for exactly that family, and FHE under the additional one-key circular-security
+  assumption. Open: the checked formal abstract of these endpoints, a uniform generator for the
+  leveled scheme's wrapper decryption circuits (uniform compactness), reuse of evaluated
+  ciphertexts as fresh inputs (multi-hop evaluation), and Gentry's exact concrete-security loss.
 - **Completeness of oblivious transfer.** In the ideal OT-hybrid model, every polynomial-time
   multiparty functionality admits a protocol secure against static malicious corruptions, with
   real/ideal simulation and abort, under the standard communication assumptions.