diff --git a/Complexity.lean b/Complexity.lean
index 7a3a01d3cb..04dbd6a72c 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1324,6 +1324,8 @@ public import Complexity.Crypto.Computational.Homomorphic.FixedKey.Security
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Basic
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Decoding
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Decryption
+public import Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters
+public import Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters.Security
 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/DepthParameters.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/DepthParameters.lean
new file mode 100644
index 0000000000..b4cc174b7c
--- /dev/null
+++ b/Complexity/Crypto/Computational/Homomorphic/GSW/DepthParameters.lean
@@ -0,0 +1,245 @@
+/-
+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.Parameters
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
+
+/-!
+# GSW parameters with a logarithmic-depth noise margin
+
+For `t = 1 + clog 2 (λ + 2)`, choose digit width `w = 16384 * t^2`, ciphertext dimension
+`N = (n + 1) * w`, sample count `m = N + 2λ`, and depth budget `L = 512 * t`. The secret and
+positive-noise dimensions reuse `Parameters.dimension` and `Parameters.noise`, both `λ + 1`.
+The complete margin `4 * m * η * (N + 1)^L < 2^w` holds at every security parameter.
+
+All dimensions and the budget have uniform unary native routines. The modulus has a binary
+routine; its value is not claimed polynomially bounded. Security assumes decision LWE for
+exactly this family's centered-binomial law. These numerical bounds do not establish that an
+actual augmented decryption circuit fits the budget, or assert lattice hardness or circular
+security.
+
+## Main definitions
+
+* `logSize`, `width`, `rows`, `samples`, `depthBudget`, `modulus`: the numerical family.
+
+## Main results
+
+* `noise_margin`: the strict decoding margin after the entire declared depth budget.
+* `entropy_margin`, `negligible_statistical_error`: the statistical part of the security bound.
+* `polynomiallyBounded_parameters`: polynomial bounds for the unary numerical parameters.
+* `computableTidilyInPolyTime_modulus`: native computation of the binary modulus.
+
+## References
+
+* [Gentry, Sahai and Waters, Sections 3.3–3.4][GentrySahaiWaters2013]
+
+The constants here supply explicit compatible inequalities for the power-of-two specialization;
+they are not a claim about the paper's hardness parameters.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.Homomorphic.GSW.DepthParameters
+
+open Parameters (dimension noise)
+open Turing.MultiTapeTM Turing.MultiTapeTM.ComputableTidilyInPolyTime
+open scoped NNReal
+
+/-- A positive logarithmic size, at least two even at security parameter zero. -/
+def logSize (security : ℕ) : ℕ := 1 + Nat.clog 2 (security + 2)
+
+/-- Binary digits in each modular coordinate. -/
+def width (security : ℕ) : ℕ := 16384 * logSize security ^ 2
+
+/-- Ciphertext rows and columns. -/
+def rows (security : ℕ) : ℕ := (dimension security + 1) * width security
+
+/-- Public samples and independent source bits in each encryption row. -/
+def samples (security : ℕ) : ℕ := rows security + 2 * security
+
+/-- Number of NAND levels covered by the proved noise margin. -/
+def depthBudget (security : ℕ) : ℕ := 512 * logSize security
+
+/-- Modulus, represented in binary by the native routine below. -/
+def modulus (security : ℕ) : ℕ := 2 ^ width security
+
+/-- The logarithmic size is uniformly bounded away from zero. -/
+theorem two_le_logSize (security : ℕ) : 2 ≤ logSize security := by
+  have := Nat.clog_pos (by decide : 1 < 2) (by omega : 1 < security + 2)
+  unfold logSize
+  omega
+
+/-- A simple linear majorant for the logarithmic size. -/
+theorem logSize_le (security : ℕ) : logSize security ≤ security + 2 := by
+  have hpow : security + 2 ≤ 2 ^ (security + 1) := Nat.lt_two_pow_self
+  have := Nat.clog_le_of_le_pow hpow
+  unfold logSize
+  omega
+
+/-- Every parameter has a nonempty modular word. -/
+theorem width_pos (security : ℕ) : 0 < width security := by
+  have := two_le_logSize security
+  unfold width
+  positivity
+
+/-- The depth budget is positive for every security parameter. -/
+theorem depthBudget_pos (security : ℕ) : 0 < depthBudget security := by
+  have := two_le_logSize security
+  unfold depthBudget
+  positivity
+
+/-- The number of samples has exactly the required entropy surplus. -/
+theorem entropy_margin (security : ℕ) : rows security + 2 * security ≤ samples security := le_rfl
+
+/-- The binary digit width has an explicit quadratic majorant. -/
+theorem width_le (security : ℕ) : width security ≤ 16384 * (security + 2) ^ 2 :=
+  Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (logSize_le security) 2)
+
+/-- The ciphertext dimension has an explicit cubic majorant. -/
+theorem rows_le (security : ℕ) : rows security ≤ 16384 * (security + 2) ^ 3 := by
+  calc
+    rows security ≤ (security + 2) * (16384 * (security + 2) ^ 2) :=
+      Nat.mul_le_mul_left _ (width_le security)
+    _ = _ := by ring
+
+/-- The public sample count has an explicit cubic majorant. -/
+theorem samples_le (security : ℕ) : samples security ≤ 16386 * (security + 2) ^ 3 := by
+  have h := rows_le security
+  have hpow : security + 2 ≤ (security + 2) ^ 3 := by
+    simpa using Nat.pow_le_pow_right (by omega : 1 ≤ security + 2) (by decide : 1 ≤ 3)
+  unfold samples
+  nlinarith
+
+/-- The logarithmic budget also has a linear majorant. -/
+theorem depthBudget_le (security : ℕ) : depthBudget security ≤ 512 * (security + 2) :=
+  Nat.mul_le_mul_left _ (logSize_le security)
+
+private theorem sizes_le_pow (security : ℕ) :
+    rows security + 1 ≤ 2 ^ (11 * logSize security) ∧
+      samples security ≤ 2 ^ (11 * logSize security) ∧ noise security ≤ 2 ^ logSize security := by
+  let t := logSize security
+  have ht : 2 ≤ t := two_le_logSize security
+  have hn : security + 2 ≤ 2 ^ t :=
+    (Nat.le_pow_clog (by decide : 1 < 2) _).trans
+      (Nat.pow_le_pow_right (by decide) (by dsimp [t, logSize]; omega))
+  have hlog : t ≤ 2 ^ t := (Nat.lt_two_pow_self (n := t)).le
+  have hrows : rows security ≤ 2 ^ (14 + 3 * t) := by
+    calc
+      rows security ≤ 2 ^ t * (16384 * (2 ^ t) ^ 2) :=
+        Nat.mul_le_mul hn (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hlog 2))
+      _ = _ := by rw [pow_add, Nat.mul_comm 3 t, pow_mul]; ring
+  have hsmall : 2 * security ≤ rows security := by
+    have hw : 2 ≤ width security := by unfold width; change 2 ≤ 16384 * t ^ 2; nlinarith
+    unfold rows dimension
+    nlinarith
+  have hnext : 2 * 2 ^ (14 + 3 * t) ≤ 2 ^ (11 * t) := by
+    calc
+      _ = 2 ^ (15 + 3 * t) := by
+        rw [show 15 + 3 * t = (14 + 3 * t) + 1 by omega, pow_succ]
+        omega
+      _ ≤ _ := Nat.pow_le_pow_right (by decide) (by omega)
+  have hpos : 0 < 2 ^ (14 + 3 * t) := by positivity
+  refine ⟨(by omega : rows security + 1 ≤ 2 * 2 ^ (14 + 3 * t)).trans hnext, ?_, ?_⟩
+  · exact (by unfold samples; omega : samples security ≤ 2 * 2 ^ (14 + 3 * t)).trans hnext
+  · change security + 1 ≤ 2 ^ t
+    omega
+
+/-- The complete declared NAND depth remains strictly inside the original decoding margin. -/
+theorem noise_margin (security : ℕ) :
+    4 * samples security * noise security * (rows security + 1) ^ depthBudget security <
+      modulus security := by
+  let t := logSize security
+  have ht : 2 ≤ t := two_le_logSize security
+  obtain ⟨hrows, hsamples, hnoise⟩ := sizes_le_pow security
+  calc
+    _ ≤ 4 * 2 ^ (11 * t) * 2 ^ t * (2 ^ (11 * t)) ^ (512 * t) :=
+      Nat.mul_le_mul (Nat.mul_le_mul (Nat.mul_le_mul_left _ hsamples) hnoise)
+        (Nat.pow_le_pow_left hrows _)
+    _ = 2 ^ (5632 * t ^ 2 + 12 * t + 2) := by
+      calc
+        _ = 2 ^ (2 + 11 * t + t + (11 * t) * (512 * t)) := by
+          rw [← pow_mul, pow_add, pow_add, pow_add]
+          norm_num
+        _ = _ := by congr 1; ring
+    _ < modulus security := by
+      apply Nat.pow_lt_pow_right (by decide)
+      change 5632 * t ^ 2 + 12 * t + 2 < 16384 * t ^ 2
+      nlinarith
+
+/-- Every smaller depth also satisfies the full noise margin. -/
+theorem noise_margin_of_le {security depth : ℕ} (hdepth : depth ≤ depthBudget security) :
+    4 * samples security * noise security * (rows security + 1) ^ depth < modulus security :=
+  (Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by omega) hdepth)).trans_lt
+    (noise_margin security)
+
+/-- Fresh ciphertexts satisfy the strict decoding margin. -/
+theorem fresh_margin (security : ℕ) :
+    4 * samples security * noise security < modulus security := by
+  simpa only [pow_zero, mul_one] using
+    noise_margin_of_le (security := security) (depth := 0) (Nat.zero_le _)
+
+/-- A NAND of two fresh ciphertexts satisfies the existing sampler theorem's margin. -/
+theorem nand_margin (security : ℕ) :
+    4 * ((1 + rows security) * (samples security * noise security)) < modulus security := by
+  simpa only [pow_one, Nat.add_comm, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc] using
+    noise_margin_of_le (security := security) (depth := 1) (depthBudget_pos security)
+
+/-- The logarithmic size is uniformly computable with unary input and output. -/
+@[fun_prop]
+theorem computableTidilyInPolyTime_logSize :
+    ComputableTidilyInPolyTime logSize encUnary encUnary := by
+  have := unary_clog_const 2
+  unfold logSize
+  fun_prop
+
+/-- Compute the unary digit width, including its quadratic dependence on the logarithm. -/
+@[fun_prop]
+theorem computableTidilyInPolyTime_width :
+    ComputableTidilyInPolyTime width encUnary encUnary := by unfold width; fun_prop
+
+/-- Compute the unary ciphertext dimension. -/
+@[fun_prop]
+theorem computableTidilyInPolyTime_rows :
+    ComputableTidilyInPolyTime rows encUnary encUnary := by unfold rows; fun_prop
+
+/-- Compute the unary public sample count. -/
+@[fun_prop]
+theorem computableTidilyInPolyTime_samples :
+    ComputableTidilyInPolyTime samples encUnary encUnary := by unfold samples; fun_prop
+
+/-- Compute the unary logarithmic depth budget. -/
+@[fun_prop]
+theorem computableTidilyInPolyTime_depthBudget :
+    ComputableTidilyInPolyTime depthBudget encUnary encUnary := by unfold depthBudget; fun_prop
+
+/-- Compute the modulus in binary; this does not assert efficient unary output. -/
+@[fun_prop]
+theorem computableTidilyInPolyTime_modulus :
+    ComputableTidilyInPolyTime modulus encUnary encNat :=
+  binary_pow' (const 2) computableTidilyInPolyTime_width
+
+/-- All unary parameters have polynomial bounds; the modulus is deliberately excluded. -/
+theorem polynomiallyBounded_parameters :
+    PolynomiallyBounded dimension ∧ PolynomiallyBounded noise ∧ PolynomiallyBounded width ∧
+      PolynomiallyBounded rows ∧ PolynomiallyBounded samples ∧ PolynomiallyBounded depthBudget :=
+  ⟨Parameters.computableTidilyInPolyTime_dimension.polynomiallyBounded,
+    Parameters.computableTidilyInPolyTime_noise.polynomiallyBounded,
+    computableTidilyInPolyTime_width.polynomiallyBounded,
+    computableTidilyInPolyTime_rows.polynomiallyBounded,
+    computableTidilyInPolyTime_samples.polynomiallyBounded,
+    computableTidilyInPolyTime_depthBudget.polynomiallyBounded⟩
+
+/-- The actual shared-public-matrix error bound is negligible for this new family. -/
+theorem negligible_statistical_error :
+    Negligible (fun security => (rows security : ℝ≥0) *
+      NNReal.sqrt ((2 : ℝ≥0) ^ rows security / 2 ^ samples security)) :=
+  negligible_mul_sqrt_pow_two_div_pow_two computableTidilyInPolyTime_rows.polynomiallyBounded
+    (Filter.Eventually.of_forall entropy_margin)
+
+end Cslib.Crypto.Homomorphic.GSW.DepthParameters
diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/DepthParameters/Security.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/DepthParameters/Security.lean
new file mode 100644
index 0000000000..821a227611
--- /dev/null
+++ b/Complexity/Crypto/Computational/Homomorphic/GSW/DepthParameters/Security.lean
@@ -0,0 +1,47 @@
+/-
+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
+public import Complexity.Crypto.Computational.Homomorphic.GSW.Security
+
+/-!
+# Security for the GSW family with a growing noise budget
+
+The explicit depth-compatible family supplies the native dimension routines and entropy surplus
+required by the actual-algorithm security reduction. Its exact decision-LWE assumption remains a
+hypothesis; hardness for the earlier parameter family does not establish hardness for this one.
+No decryption-circuit, bootstrappability or circular-security premise is hidden here.
+
+## Main results
+
+* `DepthParameters.indCPA`: actual serialized encryption security under this family's exact LWE.
+
+## References
+
+* [Gentry, Sahai and Waters, Sections 3.1–3.2][GentrySahaiWaters2013]
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.Homomorphic.GSW.DepthParameters
+
+open Parameters (dimension noise)
+
+/-- The actual serialized algorithms are IND-CPA under decision LWE for this exact new family.
+The LWE premise for the earlier, narrower modulus family is not used. -/
+theorem indCPA
+    (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) (noise k))) :
+    Encryption.INDCPA
+      (fun k => keyGenSerialized (dimension k) (samples k) (width k) (noise k))
+      (fun k => encryptSerialized (dimension k) (samples k) (width k)) :=
+  indCPA_of_decisionLWE Parameters.computableTidilyInPolyTime_dimension
+    computableTidilyInPolyTime_samples computableTidilyInPolyTime_width
+    (Filter.Eventually.of_forall entropy_margin) hLWE
+
+end Cslib.Crypto.Homomorphic.GSW.DepthParameters
diff --git a/ComplexityTests.lean b/ComplexityTests.lean
index 4bf176af40..e1759a1189 100644
--- a/ComplexityTests.lean
+++ b/ComplexityTests.lean
@@ -120,6 +120,7 @@ import ComplexityTests.Crypto.FixedKeySecurity
 import ComplexityTests.Crypto.GMWPointwise
 import ComplexityTests.Crypto.GSW
 import ComplexityTests.Crypto.GSWDecryption
+import ComplexityTests.Crypto.GSWDepthParameters
 import ComplexityTests.Crypto.GSWEvaluation
 import ComplexityTests.Crypto.GSWHiding
 import ComplexityTests.Crypto.GSWNative
diff --git a/ComplexityTests/Crypto/GSWDepthParameters.lean b/ComplexityTests/Crypto/GSWDepthParameters.lean
new file mode 100644
index 0000000000..f4819d2adb
--- /dev/null
+++ b/ComplexityTests/Crypto/GSWDepthParameters.lean
@@ -0,0 +1,153 @@
+/-
+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.DepthParameters.Security
+
+/-!
+The new family's zero and growing parameters, full depth margin, positive supported noise,
+honest native algorithms and exact-family security premise. The tests do not assert that an
+augmented decryption circuit fits the budget or assume security of an insecure fixture.
+-/
+
+namespace ComplexityTests.GSWDepthParameters
+
+open Cslib Cslib.Crypto Cslib.Probability Cslib.Crypto.Homomorphic.GSW
+open Turing.MultiTapeTM
+
+-- Zero is included; neither the dimensions, noise nor depth collapses to an empty case.
+example : Parameters.dimension 0 = 1 ∧ Parameters.noise 0 = 1 ∧
+    DepthParameters.logSize 0 = 2 ∧ DepthParameters.width 0 = 65536 ∧
+    DepthParameters.rows 0 = 131072 ∧ DepthParameters.samples 0 = 131072 ∧
+    DepthParameters.depthBudget 0 = 1024 := by decide +kernel
+
+example : DepthParameters.logSize 1 = 3 ∧ DepthParameters.width 1 = 147456 ∧
+    DepthParameters.samples 1 = 442370 ∧ DepthParameters.depthBudget 1 = 1536 ∧
+    DepthParameters.logSize 6 = 4 ∧ DepthParameters.depthBudget 6 = 2048 := by decide +kernel
+
+-- The earlier family retains its narrower modulus and original API.
+example : Parameters.width 0 = 16 ∧ Parameters.width 1 = 24 := by decide +kernel
+
+example (security : ℕ) : 0 < Parameters.dimension security ∧ 0 < Parameters.noise security ∧
+    0 < DepthParameters.width security ∧ 0 < DepthParameters.rows security ∧
+    0 < DepthParameters.samples security ∧ 0 < DepthParameters.depthBudget security := by
+  have hw := DepthParameters.width_pos security
+  have hdepth := DepthParameters.depthBudget_pos security
+  refine ⟨by simp [Parameters.dimension], Parameters.noise_pos security, hw, ?_, ?_, hdepth⟩
+  · unfold DepthParameters.rows
+    positivity
+  · unfold DepthParameters.samples DepthParameters.rows
+    positivity
+
+example : 4 * DepthParameters.samples 0 * Parameters.noise 0 *
+    (DepthParameters.rows 0 + 1) ^ DepthParameters.depthBudget 0 <
+      2 ^ DepthParameters.width 0 := DepthParameters.noise_margin 0
+
+example (security depth : ℕ) (hdepth : depth ≤ DepthParameters.depthBudget security) :
+    4 * DepthParameters.samples security * Parameters.noise security *
+      (DepthParameters.rows security + 1) ^ depth < 2 ^ DepthParameters.width security :=
+  DepthParameters.noise_margin_of_le hdepth
+
+-- A nonzero error is actually supported at every parameter, including zero.
+example (security : ℕ) :
+    (1 : ℤ) ∈ (ProbComp.eval (sampleCenteredBinomial (Parameters.noise security))).support := by
+  rw [mem_support_sampleCenteredBinomial_iff]
+  simp [Parameters.noise]
+
+-- Nonempty actual key and encryption supports realize the proved fresh and NAND margins.
+-- State the finite-type client at arbitrary dimensions before specializing its large moduli.
+private theorem supported_correct (n m w η : ℕ) (hw : 0 < w)
+    (hfresh : 4 * (m * η) < 2 ^ w)
+    (hnand : 4 * ((1 + (n + 1) * w) * (m * η)) < 2 ^ w) (left right : Bool) :
+    ∃ keys ∈ (ProbComp.eval (keyGen n m w η)).support,
+      ∃ c₁ ∈ (ProbComp.eval (encrypt keys.1 left)).support,
+        ∃ c₂ ∈ (ProbComp.eval (encrypt keys.1 right)).support,
+          decrypt keys.2 c₁ = left ∧ decrypt keys.2 (nand c₁ c₂) = !(left && right) := by
+  obtain ⟨keys, hkeys⟩ := (ProbComp.eval (keyGen n m w η)).support_nonempty
+  obtain ⟨c₁, hc₁⟩ := (ProbComp.eval (encrypt keys.1 left)).support_nonempty
+  obtain ⟨c₂, hc₂⟩ := (ProbComp.eval (encrypt keys.1 right)).support_nonempty
+  refine ⟨keys, hkeys, c₁, hc₁, c₂, hc₂, ?_, ?_⟩
+  · exact keyGen_encrypt_correct hw hfresh hkeys left hc₁
+  · exact keyGen_nand_correct hw hnand hkeys left right hc₁ hc₂
+
+example (security : ℕ) (left right : Bool) :=
+  supported_correct (Parameters.dimension security) (DepthParameters.samples security)
+    (DepthParameters.width security) (Parameters.noise security)
+    (DepthParameters.width_pos security)
+    (by simpa only [Nat.mul_assoc, DepthParameters.modulus] using
+      DepthParameters.fresh_margin security)
+    (DepthParameters.nand_margin security) left right
+
+-- Native routines return the full varying parameters, not a fixed finite-type code.
+example : ComputableTidilyInPolyTime
+    (fun security => (DepthParameters.width security,
+      DepthParameters.samples security, DepthParameters.depthBudget security))
+    encUnary (encPair encUnary (encPair encUnary encUnary)) := by fun_prop
+
+-- The much larger modulus is returned in binary, not unary.
+example : ComputableTidilyInPolyTime DepthParameters.modulus encUnary encNat := by fun_prop
+
+example : PolynomiallyBounded (fun security => DepthParameters.rows security ^ 2) := by
+  have := DepthParameters.computableTidilyInPolyTime_rows.polynomiallyBounded
+  fun_prop
+
+example : IsPPTOn encUnary (encPair encBits encBits)
+    (fun security => keyGenSerialized (Parameters.dimension security)
+      (DepthParameters.samples security) (DepthParameters.width security)
+      (Parameters.noise security)) :=
+  isPPTOn_keyGenSerialized Parameters.computableTidilyInPolyTime_dimension
+    DepthParameters.computableTidilyInPolyTime_samples
+    DepthParameters.computableTidilyInPolyTime_width Parameters.computableTidilyInPolyTime_noise
+
+-- This certificate includes every raw public word and bit, including malformed input words.
+example : IsPPTOn (encPair encUnary (encPair encBits encBool)) encBits
+    (fun p => encryptSerialized (Parameters.dimension p.1) (DepthParameters.samples p.1)
+      (DepthParameters.width p.1) p.2.1 p.2.2) :=
+  isPPTOn_encryptSerialized (by fun_prop) (by fun_prop) (by fun_prop)
+    (by fun_prop) (by fun_prop)
+
+-- Only this exact family's LWE hypothesis is supplied: no old-family or encryption-security
+-- assumption, efficient-width premise, or unproved decryption-circuit contract is added.
+example
+    (hLWE : DecisionLWE Parameters.dimension DepthParameters.samples DepthParameters.width
+      (fun k => noiseLaw (DepthParameters.width k) (Parameters.noise k))) :
+    Encryption.INDCPA
+      (fun k => keyGenSerialized (Parameters.dimension k) (DepthParameters.samples k)
+        (DepthParameters.width k) (Parameters.noise k))
+      (fun k => encryptSerialized (Parameters.dimension k) (DepthParameters.samples k)
+        (DepthParameters.width k)) := DepthParameters.indCPA hLWE
+
+end ComplexityTests.GSWDepthParameters
+
+open Cslib.Crypto.Homomorphic.GSW
+
+/--
+info: 'Cslib.Crypto.Homomorphic.GSW.DepthParameters.noise_margin' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms DepthParameters.noise_margin
+
+/--
+info: 'Cslib.Crypto.Homomorphic.GSW.DepthParameters.computableTidilyInPolyTime_modulus'
+depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms DepthParameters.computableTidilyInPolyTime_modulus
+
+/--
+info: 'Cslib.Crypto.Homomorphic.GSW.DepthParameters.negligible_statistical_error' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms DepthParameters.negligible_statistical_error
+
+/--
+info: 'Cslib.Crypto.Homomorphic.GSW.DepthParameters.indCPA' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms DepthParameters.indCPA
diff --git a/ROADMAP.md b/ROADMAP.md
index a5e648d29c..97aaab90ca 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -261,8 +261,17 @@ existing developments, source credit and saved branches remain available for a f
    spells out both algorithms, their native efficiency and this precise conditional security
    result. It remains outside the curated headline catalogue while the full FHE recovery is open.
    Hardness for the specified noise family is assumed; no worst-case lattice reduction is supplied.
+   A separate [depth-margin family](Complexity/Crypto/Computational/Homomorphic/GSW/DepthParameters.lean)
+   takes `t = 1+ceil(log₂(λ+2))`, `n = η = λ+1`, `w = 16384*t²`, `N = (n+1)*w`,
+   `m = N+2λ` and `L = 512*t`. It proves `4*m*η*(N+1)^L < 2^w` for every parameter,
+   including zero, together with the entropy surplus, polynomial bounds and uniform native
+   unary parameter routines. Only the modulus is returned in binary.
+   Its [security corollary](Complexity/Crypto/Computational/Homomorphic/GSW/DepthParameters/Security.lean)
+   assumes decision LWE for this exact new family; the earlier family's hardness premise is
+   insufficient. The actual augmented-decryption circuit still has to be constructed and proved
+   to fit `L`; this arithmetic result does not establish bootstrappability.
    Full native circuit evaluation, shallow decryption circuits, bootstrappability with compatible
-   parameters and the concrete FHE instantiation remain open in #486. This parameter family
+   parameters and the concrete FHE instantiation remain open in #486. The earlier parameter family
    proves fresh and one-NAND correctness; it does not yet supply the augmented-decryption circuit
    or the separate joint circular-security assumption needed for the fixed-key endpoint.
    The [code-composition API](Complexity/Computability/Circuit/Boolean/CodeComposition.lean)