diff --git a/.github/workflows/telperion-lean-e2e.yml b/.github/workflows/telperion-lean-e2e.yml
index f3da925d..2ee441ca 100644
--- a/.github/workflows/telperion-lean-e2e.yml
+++ b/.github/workflows/telperion-lean-e2e.yml
@@ -2722,3 +2722,36 @@ jobs:
       - name: Build the dVP boundary-growth decomposition (kernel verification)
         working-directory: telperion/examples/zero_free_bridge/lean
         run: lake build DlvpBoundaryDecomp
+
+  # dVP entire-part (i-b') certificate shapes (max_modulus, bc_deriv_re, entire_part_bound):
+  # regenerate from the emitters, drift-check, and kernel-verify the emitted Lean.
+  dvp-bc-atoms-compiles:
+    runs-on: ubuntu-latest
+    timeout-minutes: 60
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+      - run: pip install sympy pytest
+      - name: Emitter self-check / negative-control tests
+        working-directory: telperion
+        run: PYTHONPATH=src python -m pytest tests/test_emit_dvp_bc_atoms.py -q
+      - name: Regenerate the dVP entire-part Lean from the emitters (certify -> emit -> check)
+        working-directory: telperion
+        run: PYTHONPATH=src python examples/dvp_bc_atoms/generate.py --check
+      - name: Cache elan toolchain
+        uses: actions/cache@v4
+        with:
+          path: ~/.elan
+          key: elan-${{ runner.os }}-${{ hashFiles('telperion/examples/dvp_bc_atoms/lean/lean-toolchain') }}
+      - name: Install elan
+        run: |
+          curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Fetch Mathlib olean cache
+        working-directory: telperion/examples/dvp_bc_atoms/lean
+        run: lake exe cache get
+      - name: Build the emitted Lean (the actual verification — dVP entire-part certificates)
+        working-directory: telperion/examples/dvp_bc_atoms/lean
+        run: lake build MaxModulus BCDerivRe EntirePartBound
diff --git a/telperion/examples/dvp_bc_atoms/generate.py b/telperion/examples/dvp_bc_atoms/generate.py
new file mode 100644
index 00000000..41d3b3e4
--- /dev/null
+++ b/telperion/examples/dvp_bc_atoms/generate.py
@@ -0,0 +1,82 @@
+"""Generate the dVP entire-part (i-b') atoms example: certify -> emit -> write.
+
+    python examples/dvp_bc_atoms/generate.py           # write the three lean/*.lean files
+    python examples/dvp_bc_atoms/generate.py --check    # drift check (no write)
+
+Three self-contained certificate families (only ``import Mathlib``), distilled from the
+de la Vallee Poussin entire-part argument:
+  * max_modulus       — maximum-modulus propagation: ‖f‖≤B on the sphere ⟹ ‖f‖≤B on the disk;
+  * bc_deriv_re       — real-part → derivative bound: Re h - Re h(c) ≤ M' ⟹ ‖deriv h c‖ ≤ 2M'/(R-r)
+                        (Borel-Caratheodory + Cauchy);
+  * entire_part_bound — ‖logDeriv g c‖ ≤ 2M'/(R-r) from the log‖g‖ oscillation (self-contained
+                        3-lemma preamble: log branch + BC-Cauchy + composition).
+
+conjecture1_proved = False.
+"""
+import argparse
+import sys
+from pathlib import Path
+
+sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "src"))
+
+from telperion import (  # noqa: E402
+    BCDerivReEmitter, EntirePartBoundEmitter, GridSpec, LeanProfile, MaxModulusEmitter,
+    ValidationReport, bc_deriv_re_family, certify, emit, entire_part_bound_family,
+    max_modulus_family,
+)
+
+_HERE = Path(__file__).resolve().parent
+
+# (module name, kind, family builder, emitter, {case: spec}, {case: lean_name})
+_JOBS = [
+    ("MaxModulus", "max_modulus", max_modulus_family, MaxModulusEmitter,
+     {0: {"R": "1/2", "B": 12}, 1: {"R": "1/4", "B": 3}},
+     {0: "max_modulus_half", 1: "max_modulus_qtr"}),
+    ("BCDerivRe", "bc_deriv_re", bc_deriv_re_family, BCDerivReEmitter,
+     {0: {"R": "3/2", "r": "1/2", "Mp": 6}, 1: {"R": 1, "r": "1/4", "Mp": 2}},
+     {0: "bc_deriv_re_a", 1: "bc_deriv_re_b"}),
+    ("EntirePartBound", "entire_part_bound", entire_part_bound_family, EntirePartBoundEmitter,
+     {0: {"R": "3/2", "r": "1/2", "Mp": 6}},
+     {0: "entire_part_bound_a"}),
+]
+
+
+def _build_one(module, kind, fam_fn, emitter, specs, names) -> str:
+    fam = fam_fn(
+        module,
+        GridSpec([("case", sorted(specs))]),
+        lambda pt: names[pt["case"]],
+        spec=lambda pt: specs[pt["case"]],
+    )
+    report = emit(
+        certify(fam),
+        LeanProfile(namespace=(module,)),
+        [emitter()],
+        ValidationReport(checks=((kind, True),)),
+    )
+    return next(iter(report.files.values()))
+
+
+def main(*, check: bool = False) -> int:
+    rc = 0
+    for module, kind, fam_fn, emitter, specs, names in _JOBS:
+        text = _build_one(module, kind, fam_fn, emitter, specs, names)
+        out = _HERE / "lean" / f"{module}.lean"
+        if check:
+            if not out.exists() or out.read_text(encoding="utf-8") != text:
+                print(f"DRIFT: {module}.lean does not match regeneration")
+                rc = 1
+            else:
+                print(f"check OK: {module}.lean matches regeneration")
+        else:
+            out.parent.mkdir(exist_ok=True)
+            out.write_text(text, encoding="utf-8")
+            print(f"wrote {out.relative_to(_HERE)}")
+    return rc
+
+
+if __name__ == "__main__":
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--check", action="store_true", help="drift check (no write)")
+    args = ap.parse_args()
+    raise SystemExit(main(check=args.check))
diff --git a/telperion/examples/dvp_bc_atoms/lean/BCDerivRe.lean b/telperion/examples/dvp_bc_atoms/lean/BCDerivRe.lean
new file mode 100644
index 00000000..d86bbeee
--- /dev/null
+++ b/telperion/examples/dvp_bc_atoms/lean/BCDerivRe.lean
@@ -0,0 +1,115 @@
+/- telperion 0.1.6 | family BCDerivRe | input-hash bfaa1a7c5f05d721
+   2 theorems, 2 generation-time self-checks passed.
+   Regenerate & verify:  forge diff --family <module:attr> --manifest <manifest.json> --check
+   DO NOT EDIT BY HAND — edits are flagged by the regeneration diff.  -/
+
+import Mathlib
+
+namespace BCDerivRe
+
+open Complex Metric
+
+/-- Real-part → derivative bound on `ball c (3 / 2)`: `h` holomorphic with
+    `(h z).re - (h c).re ≤ 6` throughout implies `‖deriv h c‖ ≤ 2·6/((3 / 2) - (1 / 2))`
+    (Borel-Caratheodory + Cauchy).  A concrete copy of `norm_deriv_le_of_re_le`. -/
+theorem bc_deriv_re_a (h : ℂ → ℂ) (c : ℂ)
+    (hana : DifferentiableOn ℂ h (ball c ((3 / 2) : ℝ)))
+    (hbound : ∀ z ∈ ball c ((3 / 2) : ℝ), (h z).re - (h c).re ≤ (6 : ℝ)) :
+    ‖deriv h c‖ ≤ 2 * (6 : ℝ) / (((3 / 2) : ℝ) - (1 / 2)) := by
+  have hr : (0 : ℝ) < (1 / 2) := by norm_num
+  have hrR : ((1 / 2) : ℝ) < (3 / 2) := by norm_num
+  have hM' : (0 : ℝ) < 6 := by norm_num
+  have hR : (0 : ℝ) < (3 / 2) := by norm_num
+  have hRr : (0 : ℝ) < ((3 / 2) - (1 / 2)) := by norm_num
+  set f : ℂ → ℂ := fun w => h (c + w) - h c with hf_def
+  have hcball : c ∈ ball c ((3 / 2) : ℝ) := mem_ball_self hR
+  have hhc : DifferentiableAt ℂ h c :=
+    (hana c hcball).differentiableAt (isOpen_ball.mem_nhds hcball)
+  have hmaps : ∀ w ∈ ball (0 : ℂ) ((3 / 2) : ℝ), c + w ∈ ball c ((3 / 2) : ℝ) := by
+    intro w hw
+    rw [mem_ball_zero_iff] at hw
+    rw [mem_ball_iff_norm]
+    simpa using hw
+  have hf_deriv0 : HasDerivAt f (deriv h c) 0 := by
+    have hbase : HasDerivAt h (deriv h c) (c + 0) := by simpa using hhc.hasDerivAt
+    exact (hbase.comp_const_add c 0).sub_const (h c)
+  have hf_diffR : DifferentiableOn ℂ f (ball 0 ((3 / 2) : ℝ)) := by
+    intro w hw
+    have hcw : DifferentiableAt ℂ h (c + w) :=
+      (hana _ (hmaps w hw)).differentiableAt (isOpen_ball.mem_nhds (hmaps w hw))
+    have h1 : DifferentiableAt ℂ (fun w => h (c + w)) w := hcw.comp w (by fun_prop)
+    exact (h1.sub_const (h c)).differentiableWithinAt
+  have hf0 : f 0 = 0 := by simp [hf_def]
+  have hmaps_re : Set.MapsTo f (ball 0 ((3 / 2) : ℝ)) {z | z.re ≤ (6 : ℝ)} := by
+    intro w hw
+    simp only [Set.mem_setOf_eq, hf_def, Complex.sub_re]
+    exact hbound _ (hmaps w hw)
+  have hsphere : ∀ z ∈ sphere (0 : ℂ) ((1 / 2) : ℝ),
+      ‖f z‖ ≤ 2 * (6 : ℝ) * (1 / 2) / ((3 / 2) - (1 / 2)) := by
+    intro z hz
+    rw [mem_sphere_zero_iff_norm] at hz
+    have hzball : z ∈ ball (0 : ℂ) ((3 / 2) : ℝ) := by
+      rw [mem_ball_zero_iff, hz]; exact hrR
+    have := Complex.borelCaratheodory_zero hM' hf_diffR hmaps_re hR hzball hf0
+    rwa [hz] at this
+  have hdcc : DiffContOnCl ℂ f (ball 0 ((1 / 2) : ℝ)) := by
+    refine ⟨hf_diffR.mono (ball_subset_ball hrR.le), ?_⟩
+    rw [closure_ball 0 hr.ne']
+    exact hf_diffR.continuousOn.mono (closedBall_subset_ball hrR)
+  have hcauchy := Complex.norm_deriv_le_of_forall_mem_sphere_norm_le hr hdcc hsphere
+  rw [hf_deriv0.deriv] at hcauchy
+  calc ‖deriv h c‖ ≤ 2 * (6 : ℝ) * (1 / 2) / ((3 / 2) - (1 / 2)) / (1 / 2) := hcauchy
+    _ = 2 * (6 : ℝ) / (((3 / 2) : ℝ) - (1 / 2)) := by field_simp
+/-- Real-part → derivative bound on `ball c 1`: `h` holomorphic with
+    `(h z).re - (h c).re ≤ 2` throughout implies `‖deriv h c‖ ≤ 2·2/(1 - (1 / 4))`
+    (Borel-Caratheodory + Cauchy).  A concrete copy of `norm_deriv_le_of_re_le`. -/
+theorem bc_deriv_re_b (h : ℂ → ℂ) (c : ℂ)
+    (hana : DifferentiableOn ℂ h (ball c (1 : ℝ)))
+    (hbound : ∀ z ∈ ball c (1 : ℝ), (h z).re - (h c).re ≤ (2 : ℝ)) :
+    ‖deriv h c‖ ≤ 2 * (2 : ℝ) / ((1 : ℝ) - (1 / 4)) := by
+  have hr : (0 : ℝ) < (1 / 4) := by norm_num
+  have hrR : ((1 / 4) : ℝ) < 1 := by norm_num
+  have hM' : (0 : ℝ) < 2 := by norm_num
+  have hR : (0 : ℝ) < 1 := by norm_num
+  have hRr : (0 : ℝ) < (1 - (1 / 4)) := by norm_num
+  set f : ℂ → ℂ := fun w => h (c + w) - h c with hf_def
+  have hcball : c ∈ ball c (1 : ℝ) := mem_ball_self hR
+  have hhc : DifferentiableAt ℂ h c :=
+    (hana c hcball).differentiableAt (isOpen_ball.mem_nhds hcball)
+  have hmaps : ∀ w ∈ ball (0 : ℂ) (1 : ℝ), c + w ∈ ball c (1 : ℝ) := by
+    intro w hw
+    rw [mem_ball_zero_iff] at hw
+    rw [mem_ball_iff_norm]
+    simpa using hw
+  have hf_deriv0 : HasDerivAt f (deriv h c) 0 := by
+    have hbase : HasDerivAt h (deriv h c) (c + 0) := by simpa using hhc.hasDerivAt
+    exact (hbase.comp_const_add c 0).sub_const (h c)
+  have hf_diffR : DifferentiableOn ℂ f (ball 0 (1 : ℝ)) := by
+    intro w hw
+    have hcw : DifferentiableAt ℂ h (c + w) :=
+      (hana _ (hmaps w hw)).differentiableAt (isOpen_ball.mem_nhds (hmaps w hw))
+    have h1 : DifferentiableAt ℂ (fun w => h (c + w)) w := hcw.comp w (by fun_prop)
+    exact (h1.sub_const (h c)).differentiableWithinAt
+  have hf0 : f 0 = 0 := by simp [hf_def]
+  have hmaps_re : Set.MapsTo f (ball 0 (1 : ℝ)) {z | z.re ≤ (2 : ℝ)} := by
+    intro w hw
+    simp only [Set.mem_setOf_eq, hf_def, Complex.sub_re]
+    exact hbound _ (hmaps w hw)
+  have hsphere : ∀ z ∈ sphere (0 : ℂ) ((1 / 4) : ℝ),
+      ‖f z‖ ≤ 2 * (2 : ℝ) * (1 / 4) / (1 - (1 / 4)) := by
+    intro z hz
+    rw [mem_sphere_zero_iff_norm] at hz
+    have hzball : z ∈ ball (0 : ℂ) (1 : ℝ) := by
+      rw [mem_ball_zero_iff, hz]; exact hrR
+    have := Complex.borelCaratheodory_zero hM' hf_diffR hmaps_re hR hzball hf0
+    rwa [hz] at this
+  have hdcc : DiffContOnCl ℂ f (ball 0 ((1 / 4) : ℝ)) := by
+    refine ⟨hf_diffR.mono (ball_subset_ball hrR.le), ?_⟩
+    rw [closure_ball 0 hr.ne']
+    exact hf_diffR.continuousOn.mono (closedBall_subset_ball hrR)
+  have hcauchy := Complex.norm_deriv_le_of_forall_mem_sphere_norm_le hr hdcc hsphere
+  rw [hf_deriv0.deriv] at hcauchy
+  calc ‖deriv h c‖ ≤ 2 * (2 : ℝ) * (1 / 4) / (1 - (1 / 4)) / (1 / 4) := hcauchy
+    _ = 2 * (2 : ℝ) / ((1 : ℝ) - (1 / 4)) := by field_simp
+
+end BCDerivRe
diff --git a/telperion/examples/dvp_bc_atoms/lean/EntirePartBound.lean b/telperion/examples/dvp_bc_atoms/lean/EntirePartBound.lean
new file mode 100644
index 00000000..cfe5bf80
--- /dev/null
+++ b/telperion/examples/dvp_bc_atoms/lean/EntirePartBound.lean
@@ -0,0 +1,137 @@
+/- telperion 0.1.6 | family EntirePartBound | input-hash aef4a7abfa6840cb
+   4 theorems, 1 generation-time self-checks passed.
+   Regenerate & verify:  forge diff --family <module:attr> --manifest <manifest.json> --check
+   DO NOT EDIT BY HAND — edits are flagged by the regeneration diff.  -/
+
+import Mathlib
+
+namespace EntirePartBound
+
+open Complex Metric
+
+/-- Analytic log branch on a disk (helper): a zero-free holomorphic `g` on `ball c r`
+    admits an analytic branch `h` of `log g`. -/
+private theorem log_branch_of_analytic_nonvanishing {g : ℂ → ℂ} {c : ℂ} {r : ℝ} (hr : 0 < r)
+    (hg : DifferentiableOn ℂ g (ball c r)) (hne : ∀ z ∈ ball c r, g z ≠ 0) :
+    ∃ h : ℂ → ℂ, (∀ z ∈ ball c r, HasDerivAt h (logDeriv g z) z) ∧
+      h c = Complex.log (g c) ∧
+      (∀ z ∈ ball c r, Complex.exp (h z) = g z) ∧
+      (∀ z ∈ ball c r, (h z).re = Real.log ‖g z‖) := by
+  have hcball : c ∈ ball c r := mem_ball_self hr
+  have hg_an : AnalyticOnNhd ℂ g (ball c r) := hg.analyticOnNhd isOpen_ball
+  have hlog_diff : DifferentiableOn ℂ (logDeriv g) (ball c r) := by
+    intro z hz
+    have hderivg : DifferentiableAt ℂ (deriv g) z := (hg_an z hz).deriv.differentiableAt
+    have hgz : DifferentiableAt ℂ g z := (hg_an z hz).differentiableAt
+    exact (hderivg.div hgz (hne z hz)).differentiableWithinAt
+  obtain ⟨h, hhc, hh⟩ := (hlog_diff.isExactOn_ball).with_val_at c (Complex.log (g c))
+  have hφ : ∀ z ∈ ball c r, HasDerivAt (fun w => g w * Complex.exp (-h w)) 0 z := by
+    intro z hz
+    have hgz : HasDerivAt g (deriv g z) z := (hg_an z hz).differentiableAt.hasDerivAt
+    have hexp : HasDerivAt (fun w => Complex.exp (-h w))
+        (Complex.exp (-h z) * (-(logDeriv g z))) z := ((hh z hz).neg).cexp
+    have hprod := hgz.mul hexp
+    have hgz0 := hne z hz
+    have hderiv0 : deriv g z * Complex.exp (-h z)
+        + g z * (Complex.exp (-h z) * (-(logDeriv g z))) = 0 := by
+      rw [logDeriv_apply]; field_simp; ring
+    rw [hderiv0] at hprod
+    exact hprod
+  have hconst : ∀ z ∈ ball c r,
+      (fun w => g w * Complex.exp (-h w)) z = (fun w => g w * Complex.exp (-h w)) c := by
+    intro z hz
+    refine (convex_ball c r).is_const_of_fderivWithin_eq_zero
+      (fun x hx => (hφ x hx).differentiableAt.differentiableWithinAt) ?_ hz hcball
+    intro x hx
+    rw [fderivWithin_of_isOpen isOpen_ball hx]
+    simpa using (hφ x hx).hasFDerivAt.fderiv
+  have hφc : g c * Complex.exp (-h c) = 1 := by
+    rw [hhc, Complex.exp_neg, Complex.exp_log (hne c hcball), mul_inv_cancel₀ (hne c hcball)]
+  have hexp_eq : ∀ z ∈ ball c r, Complex.exp (h z) = g z := by
+    intro z hz
+    have key : g z * Complex.exp (-h z) = 1 := (hconst z hz).trans hφc
+    rw [Complex.exp_neg] at key
+    have hexpne : Complex.exp (h z) ≠ 0 := Complex.exp_ne_zero _
+    field_simp [hexpne] at key
+    exact key.symm
+  refine ⟨h, hh, hhc, hexp_eq, ?_⟩
+  intro z hz
+  have hnorm : ‖g z‖ = Real.exp (h z).re := by rw [← hexp_eq z hz, Complex.norm_exp]
+  rw [hnorm, Real.log_exp]
+
+/-- Real-part → derivative bound (helper): Borel-Caratheodory + Cauchy. -/
+private theorem norm_deriv_le_of_re_le {h : ℂ → ℂ} {c : ℂ} {R r M' : ℝ}
+    (hr : 0 < r) (hrR : r < R)
+    (hana : DifferentiableOn ℂ h (ball c R)) (hM' : 0 < M')
+    (hbound : ∀ z ∈ ball c R, (h z).re - (h c).re ≤ M') :
+    ‖deriv h c‖ ≤ 2 * M' / (R - r) := by
+  have hR : 0 < R := hr.trans hrR
+  have hRr : (0 : ℝ) < R - r := by linarith
+  set f : ℂ → ℂ := fun w => h (c + w) - h c with hf_def
+  have hcball : c ∈ ball c R := mem_ball_self hR
+  have hhc : DifferentiableAt ℂ h c := (hana c hcball).differentiableAt (isOpen_ball.mem_nhds hcball)
+  have hmaps : ∀ w ∈ ball (0 : ℂ) R, c + w ∈ ball c R := by
+    intro w hw
+    rw [mem_ball_zero_iff] at hw
+    rw [mem_ball_iff_norm]
+    simpa using hw
+  have hf_deriv0 : HasDerivAt f (deriv h c) 0 := by
+    have hbase : HasDerivAt h (deriv h c) (c + 0) := by simpa using hhc.hasDerivAt
+    exact (hbase.comp_const_add c 0).sub_const (h c)
+  have hf_diffR : DifferentiableOn ℂ f (ball 0 R) := by
+    intro w hw
+    have hcw : DifferentiableAt ℂ h (c + w) :=
+      (hana _ (hmaps w hw)).differentiableAt (isOpen_ball.mem_nhds (hmaps w hw))
+    have h1 : DifferentiableAt ℂ (fun w => h (c + w)) w := hcw.comp w (by fun_prop)
+    exact (h1.sub_const (h c)).differentiableWithinAt
+  have hf0 : f 0 = 0 := by simp [hf_def]
+  have hmaps_re : Set.MapsTo f (ball 0 R) {z | z.re ≤ M'} := by
+    intro w hw
+    simp only [Set.mem_setOf_eq, hf_def, Complex.sub_re]
+    exact hbound _ (hmaps w hw)
+  have hsphere : ∀ z ∈ sphere (0 : ℂ) r, ‖f z‖ ≤ 2 * M' * r / (R - r) := by
+    intro z hz
+    rw [mem_sphere_zero_iff_norm] at hz
+    have hzball : z ∈ ball (0 : ℂ) R := by rw [mem_ball_zero_iff, hz]; exact hrR
+    have := Complex.borelCaratheodory_zero hM' hf_diffR hmaps_re hR hzball hf0
+    rwa [hz] at this
+  have hdcc : DiffContOnCl ℂ f (ball 0 r) := by
+    refine ⟨hf_diffR.mono (ball_subset_ball hrR.le), ?_⟩
+    rw [closure_ball 0 hr.ne']
+    exact hf_diffR.continuousOn.mono (closedBall_subset_ball hrR)
+  have hcauchy := Complex.norm_deriv_le_of_forall_mem_sphere_norm_le hr hdcc hsphere
+  rw [hf_deriv0.deriv] at hcauchy
+  calc ‖deriv h c‖ ≤ 2 * M' * r / (R - r) / r := hcauchy
+    _ = 2 * M' / (R - r) := by field_simp
+
+/-- Entire-part bound (helper): compose the two above via `Re h = log‖g‖`. -/
+private theorem norm_logDeriv_le_of_log_norm_le {g : ℂ → ℂ} {c : ℂ} {R r M' : ℝ}
+    (hr : 0 < r) (hrR : r < R) (hM' : 0 < M')
+    (hg : DifferentiableOn ℂ g (ball c R)) (hne : ∀ z ∈ ball c R, g z ≠ 0)
+    (hbound : ∀ z ∈ ball c R, Real.log ‖g z‖ - Real.log ‖g c‖ ≤ M') :
+    ‖logDeriv g c‖ ≤ 2 * M' / (R - r) := by
+  have hR : 0 < R := hr.trans hrR
+  have hcball : c ∈ ball c R := mem_ball_self hR
+  obtain ⟨h, hh, _hhc, _hexp, hre⟩ := log_branch_of_analytic_nonvanishing hR hg hne
+  have hh_diff : DifferentiableOn ℂ h (ball c R) :=
+    fun z hz => (hh z hz).differentiableAt.differentiableWithinAt
+  have hderiv_c : deriv h c = logDeriv g c := (hh c hcball).deriv
+  have hre_bound : ∀ z ∈ ball c R, (h z).re - (h c).re ≤ M' := by
+    intro z hz
+    rw [hre z hz, hre c hcball]
+    exact hbound z hz
+  have := norm_deriv_le_of_re_le hr hrR hh_diff hM' hre_bound
+  rwa [hderiv_c] at this
+
+/-- Entire-part bound on `ball c (3 / 2)`: zero-free holomorphic `g` with
+    `log‖g z‖ - log‖g c‖ ≤ 6` throughout implies `‖logDeriv g c‖ ≤ 2·6/((3 / 2) - (1 / 2))`.
+    A concrete copy of `norm_logDeriv_le_of_log_norm_le`. -/
+theorem entire_part_bound_a (g : ℂ → ℂ) (c : ℂ)
+    (hg : DifferentiableOn ℂ g (ball c ((3 / 2) : ℝ)))
+    (hne : ∀ z ∈ ball c ((3 / 2) : ℝ), g z ≠ 0)
+    (hbound : ∀ z ∈ ball c ((3 / 2) : ℝ),
+      Real.log ‖g z‖ - Real.log ‖g c‖ ≤ (6 : ℝ)) :
+    ‖logDeriv g c‖ ≤ 2 * (6 : ℝ) / (((3 / 2) : ℝ) - (1 / 2)) :=
+  norm_logDeriv_le_of_log_norm_le (by norm_num) (by norm_num) (by norm_num) hg hne hbound
+
+end EntirePartBound
diff --git a/telperion/examples/dvp_bc_atoms/lean/MaxModulus.lean b/telperion/examples/dvp_bc_atoms/lean/MaxModulus.lean
new file mode 100644
index 00000000..9b25a909
--- /dev/null
+++ b/telperion/examples/dvp_bc_atoms/lean/MaxModulus.lean
@@ -0,0 +1,39 @@
+/- telperion 0.1.6 | family MaxModulus | input-hash bd8b6bed8e3cd9f1
+   2 theorems, 2 generation-time self-checks passed.
+   Regenerate & verify:  forge diff --family <module:attr> --manifest <manifest.json> --check
+   DO NOT EDIT BY HAND — edits are flagged by the regeneration diff.  -/
+
+import Mathlib
+
+namespace MaxModulus
+
+open Complex Metric
+
+/-- Maximum-modulus propagation on the disk of radius `(1 / 2)` about `c`:
+    `f` holomorphic on `ball c (1 / 2)` (continuous up to the boundary) with
+    `‖f z‖ ≤ 12` on `sphere c (1 / 2)` implies `‖f z‖ ≤ 12` throughout `ball c (1 / 2)`.
+    A concrete-radius wrapper of `Complex.norm_le_of_forall_mem_frontier_norm_le`. -/
+theorem max_modulus_half (f : ℂ → ℂ) (c : ℂ)
+    (hd : DiffContOnCl ℂ f (ball c ((1 / 2) : ℝ)))
+    (hB : ∀ z ∈ sphere c ((1 / 2) : ℝ), ‖f z‖ ≤ (12 : ℝ)) :
+    ∀ z ∈ ball c ((1 / 2) : ℝ), ‖f z‖ ≤ (12 : ℝ) := by
+  intro z hz
+  refine Complex.norm_le_of_forall_mem_frontier_norm_le isBounded_ball hd ?_
+    (subset_closure hz)
+  rw [frontier_ball c (by norm_num : ((1 / 2) : ℝ) ≠ 0)]
+  exact hB
+/-- Maximum-modulus propagation on the disk of radius `(1 / 4)` about `c`:
+    `f` holomorphic on `ball c (1 / 4)` (continuous up to the boundary) with
+    `‖f z‖ ≤ 3` on `sphere c (1 / 4)` implies `‖f z‖ ≤ 3` throughout `ball c (1 / 4)`.
+    A concrete-radius wrapper of `Complex.norm_le_of_forall_mem_frontier_norm_le`. -/
+theorem max_modulus_qtr (f : ℂ → ℂ) (c : ℂ)
+    (hd : DiffContOnCl ℂ f (ball c ((1 / 4) : ℝ)))
+    (hB : ∀ z ∈ sphere c ((1 / 4) : ℝ), ‖f z‖ ≤ (3 : ℝ)) :
+    ∀ z ∈ ball c ((1 / 4) : ℝ), ‖f z‖ ≤ (3 : ℝ) := by
+  intro z hz
+  refine Complex.norm_le_of_forall_mem_frontier_norm_le isBounded_ball hd ?_
+    (subset_closure hz)
+  rw [frontier_ball c (by norm_num : ((1 / 4) : ℝ) ≠ 0)]
+  exact hB
+
+end MaxModulus
diff --git a/telperion/examples/dvp_bc_atoms/lean/lake-manifest.json b/telperion/examples/dvp_bc_atoms/lean/lake-manifest.json
new file mode 100644
index 00000000..187458b8
--- /dev/null
+++ b/telperion/examples/dvp_bc_atoms/lean/lake-manifest.json
@@ -0,0 +1,117 @@
+{
+  "version": "1.2.0",
+  "packagesDir": ".lake/packages",
+  "packages": [
+    {
+      "url": "https://github.com/leanprover-community/mathlib4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "81a5d257c8e410db227a6665ed08f64fea08e997",
+      "name": "mathlib",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v4.32.0",
+      "inherited": false,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover-community/plausible",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62",
+      "name": "plausible",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/LeanSearchClient",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+      "name": "LeanSearchClient",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/import-graph",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12",
+      "name": "importGraph",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/ProofWidgets4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "6e311e2a844da9b2cc3971187df2fe0066947b93",
+      "name": "proofwidgets",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover-community/aesop",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3",
+      "name": "aesop",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/quote4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc",
+      "name": "Qq",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/batteries",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff",
+      "name": "batteries",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover/lean4-cli",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover",
+      "rev": "88679d088c9720c27ebdf2ba4dafe17341747f94",
+      "name": "Cli",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v4.32.0",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    }
+  ],
+  "name": "Toy",
+  "lakeDir": ".lake",
+  "fixedToolchain": false
+}
\ No newline at end of file
diff --git a/telperion/examples/dvp_bc_atoms/lean/lakefile.toml b/telperion/examples/dvp_bc_atoms/lean/lakefile.toml
new file mode 100644
index 00000000..7ef70755
--- /dev/null
+++ b/telperion/examples/dvp_bc_atoms/lean/lakefile.toml
@@ -0,0 +1,16 @@
+name = "DvpBcAtoms"
+defaultTargets = ["MaxModulus", "BCDerivRe", "EntirePartBound"]
+
+[[require]]
+name = "mathlib"
+scope = "leanprover-community"
+rev = "v4.32.0"
+
+[[lean_lib]]
+name = "MaxModulus"
+
+[[lean_lib]]
+name = "BCDerivRe"
+
+[[lean_lib]]
+name = "EntirePartBound"
diff --git a/telperion/examples/dvp_bc_atoms/lean/lean-toolchain b/telperion/examples/dvp_bc_atoms/lean/lean-toolchain
new file mode 100644
index 00000000..94b9f495
--- /dev/null
+++ b/telperion/examples/dvp_bc_atoms/lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.32.0
diff --git a/telperion/src/telperion/__init__.py b/telperion/src/telperion/__init__.py
index acd8a423..51396485 100644
--- a/telperion/src/telperion/__init__.py
+++ b/telperion/src/telperion/__init__.py
@@ -174,6 +174,18 @@
     SphereBoundEmitter, sphere_bound_certificate,
     sphere_bound_family, certify_sphere_bound_point,
 )
+from .emit_max_modulus import (  # noqa: F401
+    MaxModulusEmitter, max_modulus_certificate,
+    max_modulus_family, certify_max_modulus_point,
+)
+from .emit_bc_deriv_re import (  # noqa: F401
+    BCDerivReEmitter, bc_deriv_re_certificate,
+    bc_deriv_re_family, certify_bc_deriv_re_point,
+)
+from .emit_entire_part_bound import (  # noqa: F401
+    EntirePartBoundEmitter, entire_part_bound_certificate,
+    entire_part_bound_family, certify_entire_part_bound_point,
+)
 from .emit_unimodal import (  # noqa: F401
     UNIMODAL_PRELUDE, UnimodalMaxEmitter, unimodal_max_family,
 )
diff --git a/telperion/src/telperion/certify.py b/telperion/src/telperion/certify.py
index 69f10b1b..badfb22c 100644
--- a/telperion/src/telperion/certify.py
+++ b/telperion/src/telperion/certify.py
@@ -191,6 +191,13 @@ class _Guard:
     "bc_split",
     "jensen_zero_count",
     "sphere_bound",
+    # dVP entire-part (i-b') atoms (2026-09-05, distilled from DlvpMaxMod/DlvpBCDeriv/
+    # DlvpEntireBound): max_modulus (sphere norm bound -> disk, maximum-modulus principle),
+    # bc_deriv_re (real-part -> derivative bound, Borel-Caratheodory + Cauchy), entire_part_bound
+    # (‖logDeriv g c‖ from log‖g‖ oscillation; self-contained 3-lemma preamble). All import Mathlib.
+    "max_modulus",
+    "bc_deriv_re",
+    "entire_part_bound",
 )
 
 # kind -> "module:certify_point_fn" for the generic (family.special) emitters.
@@ -255,6 +262,9 @@ class _Guard:
     "bc_split": ("emit_bc_split", "certify_bc_split_point"),
     "jensen_zero_count": ("emit_jensen_zero_count", "certify_jensen_zero_count_point"),
     "sphere_bound": ("emit_sphere_bound", "certify_sphere_bound_point"),
+    "max_modulus": ("emit_max_modulus", "certify_max_modulus_point"),
+    "bc_deriv_re": ("emit_bc_deriv_re", "certify_bc_deriv_re_point"),
+    "entire_part_bound": ("emit_entire_part_bound", "certify_entire_part_bound_point"),
 }
 
 
diff --git a/telperion/src/telperion/emit_bc_deriv_re.py b/telperion/src/telperion/emit_bc_deriv_re.py
new file mode 100644
index 00000000..5fec45a0
--- /dev/null
+++ b/telperion/src/telperion/emit_bc_deriv_re.py
@@ -0,0 +1,251 @@
+"""Real-part → derivative bound emitter — the Borel-Caratheodory + Cauchy engine.
+
+The composite estimate at the heart of the de la Vallee Poussin entire-part
+argument: an analytic function's derivative at the CENTRE of a disk is controlled
+by the sup of its REAL PART (not, as in the plain Cauchy estimate `cauchy_deriv`,
+by a boundary NORM bound).  For `h : ℂ → ℂ` holomorphic on `Metric.ball c R`, if
+
+    (h z).re - (h c).re ≤ M'   for all z ∈ ball c R   (M' > 0),
+
+then for any `0 < r < R`
+
+    ‖deriv h c‖ ≤ 2 M' / (R - r).
+
+Proof (verbatim `examples/zero_free_bridge/lean/DlvpBCDeriv.lean:norm_deriv_le_of_re_le`):
+shift `f(w) = h(c+w) - h(c)` (centred, `f 0 = 0`, `Re f ≤ M'`);
+`Complex.borelCaratheodory_zero` bounds `‖f‖ ≤ 2 M' r/(R-r)` on the sphere `‖z‖ = r`;
+`Complex.norm_deriv_le_of_forall_mem_sphere_norm_le` (Cauchy) gives
+`‖deriv f 0‖ = ‖deriv h c‖ ≤ (2 M' r/(R-r))/r = 2 M'/(R-r)`.
+
+Certificate: `(R, r, M')` with `0 < r < R` and `M' > 0`.  The EXACT self-check is
+the collapse of the two-step constant `(2 M' r/(R-r))/r = 2 M'/(R-r)` over ℚ (the
+`field_simp` step), plus the well-posedness `0 < r < R`, `0 < M'`.
+
+NEGATIVE CONTROL: `r ≤ 0`, `r ≥ R`, or `M' ≤ 0` is REFUSED at certification with a
+``ValueError`` (the bound `2 M'/(R-r)` would be degenerate or the geometry empty).
+conjecture1_proved = False.
+"""
+from __future__ import annotations
+
+from dataclasses import dataclass
+from typing import Callable
+
+import sympy as sp
+
+try:  # normal package import
+    from .certify import CertifiedInstance
+    from .expr import rat_lean
+    from .family import GridSpec, InequalityFamily
+    from .lean import LeanProfile
+    from .workflow import Emitter
+except ImportError:  # run directly
+    import os
+    import sys
+
+    sys.path.insert(0, os.path.dirname(os.path.dirname(os.path.abspath(__file__))))
+    from telperion.certify import CertifiedInstance
+    from telperion.expr import rat_lean
+    from telperion.family import GridSpec, InequalityFamily
+    from telperion.lean import LeanProfile
+    from telperion.workflow import Emitter
+
+
+@dataclass(frozen=True)
+class BCDerivReCertificate:
+    """A verified real-part → derivative bound certificate.
+
+    ``R`` (outer radius), ``r`` (Cauchy radius, ``0 < r < R``) and ``M'`` (the
+    real-part oscillation bound, ``> 0``).  The certified facts are the
+    well-posedness ``0 < r < R``, ``0 < M'`` and the EXACT rational identity
+    ``(2 M' r/(R-r))/r = 2 M'/(R-r)`` (checked over ℚ).  The Lean is a
+    concrete-parameter copy of `norm_deriv_le_of_re_le`.
+    """
+
+    R: sp.Rational
+    r: sp.Rational
+    Mp: sp.Rational
+
+
+def bc_deriv_re_certificate(R, r, Mp) -> BCDerivReCertificate:
+    """Build and EXACTLY self-check a real-part → derivative bound certificate.
+
+    Refuses (``ValueError``): ``r ≤ 0`` / ``r ≥ R`` (empty geometry) or ``M' ≤ 0``
+    (degenerate bound) — the negative controls.
+    """
+    Rq, rq, Mq = sp.nsimplify(R), sp.nsimplify(r), sp.nsimplify(Mp)
+    for nm, v in (("R", Rq), ("r", rq), ("M'", Mq)):
+        if not v.is_rational:
+            raise ValueError(f"bc_deriv_re parameter {nm} must be rational; got {v!r}")
+    if rq <= 0:
+        raise ValueError(f"bc_deriv_re needs r > 0 (Cauchy radius); got r={rq}")
+    if rq >= Rq:
+        raise ValueError(f"bc_deriv_re needs r < R (nested disks); got r={rq}, R={Rq}")
+    if Mq <= 0:
+        raise ValueError(f"bc_deriv_re needs M' > 0 (real-part oscillation); got M'={Mq}")
+    # EXACT self-check of the two-step constant collapse over ℚ.
+    lhs = (2 * Mq * rq / (Rq - rq)) / rq
+    rhs = 2 * Mq / (Rq - rq)
+    if sp.simplify(lhs - rhs) != 0:
+        raise ValueError(
+            "bc_deriv_re constant self-check failed (2 M' r/(R-r)/r ≠ 2 M'/(R-r)) — rejected"
+        )
+    return BCDerivReCertificate(R=Rq, r=rq, Mp=Mq)
+
+
+def certify_bc_deriv_re_point(family, pt, name):
+    """Certify one bc_deriv_re instance from ``family.special[1](pt)``.
+
+    ``spec(pt)`` returns a dict ``{"R":…, "r":…, "Mp":…}`` or a tuple ``(R, r, Mp)``.
+    """
+    spec = family.special[1](pt)
+    if isinstance(spec, dict):
+        cert = bc_deriv_re_certificate(spec["R"], spec["r"], spec["Mp"])
+    elif isinstance(spec, (tuple, list)):
+        cert = bc_deriv_re_certificate(spec[0], spec[1], spec[2])
+    else:
+        raise ValueError(f"bc_deriv_re spec must be a dict or (R, r, Mp) tuple; got {spec!r}")
+    inst = CertifiedInstance(point=dict(pt), lean_name=name, corners=(), payload=cert)
+    return inst, 1
+
+
+@dataclass
+class BCDerivReEmitter(Emitter):
+    """Emit the real-part → derivative bound ``‖deriv h c‖ ≤ 2 M'/(R - r)`` from
+    ``(h z).re - (h c).re ≤ M'`` on the disk (Borel-Caratheodory + Cauchy), a
+    concrete-parameter copy of `norm_deriv_le_of_re_le`.  One theorem per instance."""
+
+    def __post_init__(self):
+        self.kind = "bc_deriv_re"
+
+    def emit_body(self, fam, profile: LeanProfile) -> tuple[str, int]:
+        lines: list[str] = ["open Complex Metric\n\n"]
+        nthm = 0
+        for inst in fam.instances:
+            cert: BCDerivReCertificate = inst.payload  # type: ignore[assignment]
+            base = inst.lean_name
+            Rr, rr, Mr = rat_lean(cert.R), rat_lean(cert.r), rat_lean(cert.Mp)
+            lines.append(
+                f"/-- Real-part → derivative bound on `ball c {Rr}`: `h` holomorphic with\n"
+                f"    `(h z).re - (h c).re ≤ {Mr}` throughout implies `‖deriv h c‖ ≤ 2·{Mr}/({Rr} - {rr})`\n"
+                f"    (Borel-Caratheodory + Cauchy).  A concrete copy of `norm_deriv_le_of_re_le`. -/\n"
+                f"theorem {base} (h : ℂ → ℂ) (c : ℂ)\n"
+                f"    (hana : DifferentiableOn ℂ h (ball c ({Rr} : ℝ)))\n"
+                f"    (hbound : ∀ z ∈ ball c ({Rr} : ℝ), (h z).re - (h c).re ≤ ({Mr} : ℝ)) :\n"
+                f"    ‖deriv h c‖ ≤ 2 * ({Mr} : ℝ) / (({Rr} : ℝ) - {rr}) := by\n"
+                f"  have hr : (0 : ℝ) < {rr} := by norm_num\n"
+                f"  have hrR : ({rr} : ℝ) < {Rr} := by norm_num\n"
+                f"  have hM' : (0 : ℝ) < {Mr} := by norm_num\n"
+                f"  have hR : (0 : ℝ) < {Rr} := by norm_num\n"
+                f"  have hRr : (0 : ℝ) < ({Rr} - {rr}) := by norm_num\n"
+                f"  set f : ℂ → ℂ := fun w => h (c + w) - h c with hf_def\n"
+                f"  have hcball : c ∈ ball c ({Rr} : ℝ) := mem_ball_self hR\n"
+                f"  have hhc : DifferentiableAt ℂ h c :=\n"
+                f"    (hana c hcball).differentiableAt (isOpen_ball.mem_nhds hcball)\n"
+                f"  have hmaps : ∀ w ∈ ball (0 : ℂ) ({Rr} : ℝ), c + w ∈ ball c ({Rr} : ℝ) := by\n"
+                f"    intro w hw\n"
+                f"    rw [mem_ball_zero_iff] at hw\n"
+                f"    rw [mem_ball_iff_norm]\n"
+                f"    simpa using hw\n"
+                f"  have hf_deriv0 : HasDerivAt f (deriv h c) 0 := by\n"
+                f"    have hbase : HasDerivAt h (deriv h c) (c + 0) := by simpa using hhc.hasDerivAt\n"
+                f"    exact (hbase.comp_const_add c 0).sub_const (h c)\n"
+                f"  have hf_diffR : DifferentiableOn ℂ f (ball 0 ({Rr} : ℝ)) := by\n"
+                f"    intro w hw\n"
+                f"    have hcw : DifferentiableAt ℂ h (c + w) :=\n"
+                f"      (hana _ (hmaps w hw)).differentiableAt (isOpen_ball.mem_nhds (hmaps w hw))\n"
+                f"    have h1 : DifferentiableAt ℂ (fun w => h (c + w)) w := hcw.comp w (by fun_prop)\n"
+                f"    exact (h1.sub_const (h c)).differentiableWithinAt\n"
+                f"  have hf0 : f 0 = 0 := by simp [hf_def]\n"
+                f"  have hmaps_re : Set.MapsTo f (ball 0 ({Rr} : ℝ)) {{z | z.re ≤ ({Mr} : ℝ)}} := by\n"
+                f"    intro w hw\n"
+                f"    simp only [Set.mem_setOf_eq, hf_def, Complex.sub_re]\n"
+                f"    exact hbound _ (hmaps w hw)\n"
+                f"  have hsphere : ∀ z ∈ sphere (0 : ℂ) ({rr} : ℝ),\n"
+                f"      ‖f z‖ ≤ 2 * ({Mr} : ℝ) * {rr} / ({Rr} - {rr}) := by\n"
+                f"    intro z hz\n"
+                f"    rw [mem_sphere_zero_iff_norm] at hz\n"
+                f"    have hzball : z ∈ ball (0 : ℂ) ({Rr} : ℝ) := by\n"
+                f"      rw [mem_ball_zero_iff, hz]; exact hrR\n"
+                f"    have := Complex.borelCaratheodory_zero hM' hf_diffR hmaps_re hR hzball hf0\n"
+                f"    rwa [hz] at this\n"
+                f"  have hdcc : DiffContOnCl ℂ f (ball 0 ({rr} : ℝ)) := by\n"
+                f"    refine ⟨hf_diffR.mono (ball_subset_ball hrR.le), ?_⟩\n"
+                f"    rw [closure_ball 0 hr.ne']\n"
+                f"    exact hf_diffR.continuousOn.mono (closedBall_subset_ball hrR)\n"
+                f"  have hcauchy := Complex.norm_deriv_le_of_forall_mem_sphere_norm_le hr hdcc hsphere\n"
+                f"  rw [hf_deriv0.deriv] at hcauchy\n"
+                f"  calc ‖deriv h c‖ ≤ 2 * ({Mr} : ℝ) * {rr} / ({Rr} - {rr}) / {rr} := hcauchy\n"
+                f"    _ = 2 * ({Mr} : ℝ) / (({Rr} : ℝ) - {rr}) := by field_simp\n"
+            )
+            nthm += 1
+        return "".join(lines), nthm
+
+
+def bc_deriv_re_family(
+    name: str,
+    grid: GridSpec,
+    lean_name: Callable,
+    spec: Callable,
+    constants: dict | None = None,
+) -> InequalityFamily:
+    """Build a real-part → derivative bound family (kind='bc_deriv_re').
+
+    ``spec``: a callable ``pt -> {"R":…, "r":…, "Mp":…}`` or ``pt -> (R, r, Mp)``.
+    Refuses ``r ≤ 0``, ``r ≥ R``, or ``M' ≤ 0`` at certification."""
+    return InequalityFamily(
+        name=name,
+        symbols=(),
+        grid=grid,
+        lean_name=lean_name,
+        special=("bc_deriv_re", spec),
+        constants=dict(constants or {}),
+    )
+
+
+if __name__ == "__main__":
+    print("=== positive certificate R=3/2, r=1/2, M'=6 ===")
+    cert = bc_deriv_re_certificate(sp.Rational(3, 2), sp.Rational(1, 2), 6)
+    print(f"cert OK: R={cert.R}, r={cert.r}, M'={cert.Mp}")
+
+    print("\n=== NEGATIVE CONTROL: r ≥ R (r=2, R=1) must raise ===")
+    try:
+        bc_deriv_re_certificate(1, 2, 6)
+        raise SystemExit("FAIL: r ≥ R was NOT refused")
+    except ValueError as e:
+        print(f"refused as expected: {e}")
+
+    print("\n=== NEGATIVE CONTROL: M' ≤ 0 (M'=0) must raise ===")
+    try:
+        bc_deriv_re_certificate(2, 1, 0)
+        raise SystemExit("FAIL: M'=0 was NOT refused")
+    except ValueError as e:
+        print(f"refused as expected: {e}")
+
+    print("\n=== NEGATIVE CONTROL: r ≤ 0 (r=0) must raise ===")
+    try:
+        bc_deriv_re_certificate(2, 0, 6)
+        raise SystemExit("FAIL: r=0 was NOT refused")
+    except ValueError as e:
+        print(f"refused as expected: {e}")
+
+    print("\n=== emitted Lean: R=3/2,r=1/2,M'=6 and R=1,r=1/4,M'=2 ===")
+    _SPECS = {0: {"R": sp.Rational(3, 2), "r": sp.Rational(1, 2), "Mp": 6},
+              1: {"R": 1, "r": sp.Rational(1, 4), "Mp": 2}}
+    _NAMES = {0: "bc_deriv_re_a", 1: "bc_deriv_re_b"}
+    fam = bc_deriv_re_family(
+        "BCDerivReSelfTest",
+        GridSpec([("case", [0, 1])]),
+        lambda pt: _NAMES[pt["case"]],
+        spec=lambda pt: _SPECS[pt["case"]],
+    )
+    insts = []
+    for case in (0, 1):
+        inst, _ = certify_bc_deriv_re_point(fam, {"case": case}, _NAMES[case])
+        insts.append(inst)
+
+    class _View:
+        instances = insts
+
+    body, nthm = BCDerivReEmitter().emit_body(_View(), LeanProfile(namespace=("X",)))
+    print(f"\n-- {nthm} theorems --\n")
+    print(body)
diff --git a/telperion/src/telperion/emit_entire_part_bound.py b/telperion/src/telperion/emit_entire_part_bound.py
new file mode 100644
index 00000000..7fac84fb
--- /dev/null
+++ b/telperion/src/telperion/emit_entire_part_bound.py
@@ -0,0 +1,316 @@
+"""Entire-part bound emitter — ‖logDeriv g c‖ bounded by the oscillation of log‖g‖.
+
+The full (i-b') composition of the de la Vallee Poussin entire-part argument, for
+a zero-free holomorphic `g` on a disk: the log-derivative at the centre is bounded
+by the boundary oscillation of `log‖g‖`.  For `g : ℂ → ℂ` holomorphic and zero-free
+on `Metric.ball c R`, if
+
+    log‖g z‖ - log‖g c‖ ≤ M'   for all z ∈ ball c R   (M' > 0),
+
+then for any `0 < r < R`
+
+    ‖logDeriv g c‖ ≤ 2 M' / (R - r).
+
+This is `examples/zero_free_bridge/lean/DlvpEntireBound.lean:norm_logDeriv_le_of_log_norm_le`,
+composed from the analytic log branch (`DlvpLogBranch`, giving `deriv h = logDeriv g`
+and `Re h = log‖g‖`) and the real-part → derivative bound (`DlvpBCDeriv`, Borel-
+Caratheodory + Cauchy).  The emitted file is SELF-CONTAINED (`import Mathlib`): it
+carries the three generic helper lemmas as a preamble, then a concrete-parameter
+wrapper per instance.
+
+Certificate: `(R, r, M')` with `0 < r < R` and `M' > 0` — identical shape (and
+constant self-check `(2 M' r/(R-r))/r = 2 M'/(R-r)`) to `bc_deriv_re`, since the
+entire-part bound reuses the same geometry.
+
+NEGATIVE CONTROL: `r ≤ 0`, `r ≥ R`, or `M' ≤ 0` is REFUSED with a ``ValueError``.
+conjecture1_proved = False.
+"""
+from __future__ import annotations
+
+from dataclasses import dataclass
+from typing import Callable
+
+import sympy as sp
+
+try:  # normal package import
+    from .certify import CertifiedInstance
+    from .expr import rat_lean
+    from .family import GridSpec, InequalityFamily
+    from .lean import LeanProfile
+    from .workflow import Emitter
+except ImportError:  # run directly
+    import os
+    import sys
+
+    sys.path.insert(0, os.path.dirname(os.path.dirname(os.path.abspath(__file__))))
+    from telperion.certify import CertifiedInstance
+    from telperion.expr import rat_lean
+    from telperion.family import GridSpec, InequalityFamily
+    from telperion.lean import LeanProfile
+    from telperion.workflow import Emitter
+
+
+# The three generic helper lemmas (verbatim from DlvpLogBranch / DlvpBCDeriv /
+# DlvpEntireBound), emitted once so the file is self-contained under `import Mathlib`.
+# A plain string (NOT an f-string): the set-builder `{z | z.re ≤ M'}` is literal.
+_PREAMBLE = r"""open Complex Metric
+
+/-- Analytic log branch on a disk (helper): a zero-free holomorphic `g` on `ball c r`
+    admits an analytic branch `h` of `log g`. -/
+private theorem log_branch_of_analytic_nonvanishing {g : ℂ → ℂ} {c : ℂ} {r : ℝ} (hr : 0 < r)
+    (hg : DifferentiableOn ℂ g (ball c r)) (hne : ∀ z ∈ ball c r, g z ≠ 0) :
+    ∃ h : ℂ → ℂ, (∀ z ∈ ball c r, HasDerivAt h (logDeriv g z) z) ∧
+      h c = Complex.log (g c) ∧
+      (∀ z ∈ ball c r, Complex.exp (h z) = g z) ∧
+      (∀ z ∈ ball c r, (h z).re = Real.log ‖g z‖) := by
+  have hcball : c ∈ ball c r := mem_ball_self hr
+  have hg_an : AnalyticOnNhd ℂ g (ball c r) := hg.analyticOnNhd isOpen_ball
+  have hlog_diff : DifferentiableOn ℂ (logDeriv g) (ball c r) := by
+    intro z hz
+    have hderivg : DifferentiableAt ℂ (deriv g) z := (hg_an z hz).deriv.differentiableAt
+    have hgz : DifferentiableAt ℂ g z := (hg_an z hz).differentiableAt
+    exact (hderivg.div hgz (hne z hz)).differentiableWithinAt
+  obtain ⟨h, hhc, hh⟩ := (hlog_diff.isExactOn_ball).with_val_at c (Complex.log (g c))
+  have hφ : ∀ z ∈ ball c r, HasDerivAt (fun w => g w * Complex.exp (-h w)) 0 z := by
+    intro z hz
+    have hgz : HasDerivAt g (deriv g z) z := (hg_an z hz).differentiableAt.hasDerivAt
+    have hexp : HasDerivAt (fun w => Complex.exp (-h w))
+        (Complex.exp (-h z) * (-(logDeriv g z))) z := ((hh z hz).neg).cexp
+    have hprod := hgz.mul hexp
+    have hgz0 := hne z hz
+    have hderiv0 : deriv g z * Complex.exp (-h z)
+        + g z * (Complex.exp (-h z) * (-(logDeriv g z))) = 0 := by
+      rw [logDeriv_apply]; field_simp; ring
+    rw [hderiv0] at hprod
+    exact hprod
+  have hconst : ∀ z ∈ ball c r,
+      (fun w => g w * Complex.exp (-h w)) z = (fun w => g w * Complex.exp (-h w)) c := by
+    intro z hz
+    refine (convex_ball c r).is_const_of_fderivWithin_eq_zero
+      (fun x hx => (hφ x hx).differentiableAt.differentiableWithinAt) ?_ hz hcball
+    intro x hx
+    rw [fderivWithin_of_isOpen isOpen_ball hx]
+    simpa using (hφ x hx).hasFDerivAt.fderiv
+  have hφc : g c * Complex.exp (-h c) = 1 := by
+    rw [hhc, Complex.exp_neg, Complex.exp_log (hne c hcball), mul_inv_cancel₀ (hne c hcball)]
+  have hexp_eq : ∀ z ∈ ball c r, Complex.exp (h z) = g z := by
+    intro z hz
+    have key : g z * Complex.exp (-h z) = 1 := (hconst z hz).trans hφc
+    rw [Complex.exp_neg] at key
+    have hexpne : Complex.exp (h z) ≠ 0 := Complex.exp_ne_zero _
+    field_simp [hexpne] at key
+    exact key.symm
+  refine ⟨h, hh, hhc, hexp_eq, ?_⟩
+  intro z hz
+  have hnorm : ‖g z‖ = Real.exp (h z).re := by rw [← hexp_eq z hz, Complex.norm_exp]
+  rw [hnorm, Real.log_exp]
+
+/-- Real-part → derivative bound (helper): Borel-Caratheodory + Cauchy. -/
+private theorem norm_deriv_le_of_re_le {h : ℂ → ℂ} {c : ℂ} {R r M' : ℝ}
+    (hr : 0 < r) (hrR : r < R)
+    (hana : DifferentiableOn ℂ h (ball c R)) (hM' : 0 < M')
+    (hbound : ∀ z ∈ ball c R, (h z).re - (h c).re ≤ M') :
+    ‖deriv h c‖ ≤ 2 * M' / (R - r) := by
+  have hR : 0 < R := hr.trans hrR
+  have hRr : (0 : ℝ) < R - r := by linarith
+  set f : ℂ → ℂ := fun w => h (c + w) - h c with hf_def
+  have hcball : c ∈ ball c R := mem_ball_self hR
+  have hhc : DifferentiableAt ℂ h c := (hana c hcball).differentiableAt (isOpen_ball.mem_nhds hcball)
+  have hmaps : ∀ w ∈ ball (0 : ℂ) R, c + w ∈ ball c R := by
+    intro w hw
+    rw [mem_ball_zero_iff] at hw
+    rw [mem_ball_iff_norm]
+    simpa using hw
+  have hf_deriv0 : HasDerivAt f (deriv h c) 0 := by
+    have hbase : HasDerivAt h (deriv h c) (c + 0) := by simpa using hhc.hasDerivAt
+    exact (hbase.comp_const_add c 0).sub_const (h c)
+  have hf_diffR : DifferentiableOn ℂ f (ball 0 R) := by
+    intro w hw
+    have hcw : DifferentiableAt ℂ h (c + w) :=
+      (hana _ (hmaps w hw)).differentiableAt (isOpen_ball.mem_nhds (hmaps w hw))
+    have h1 : DifferentiableAt ℂ (fun w => h (c + w)) w := hcw.comp w (by fun_prop)
+    exact (h1.sub_const (h c)).differentiableWithinAt
+  have hf0 : f 0 = 0 := by simp [hf_def]
+  have hmaps_re : Set.MapsTo f (ball 0 R) {z | z.re ≤ M'} := by
+    intro w hw
+    simp only [Set.mem_setOf_eq, hf_def, Complex.sub_re]
+    exact hbound _ (hmaps w hw)
+  have hsphere : ∀ z ∈ sphere (0 : ℂ) r, ‖f z‖ ≤ 2 * M' * r / (R - r) := by
+    intro z hz
+    rw [mem_sphere_zero_iff_norm] at hz
+    have hzball : z ∈ ball (0 : ℂ) R := by rw [mem_ball_zero_iff, hz]; exact hrR
+    have := Complex.borelCaratheodory_zero hM' hf_diffR hmaps_re hR hzball hf0
+    rwa [hz] at this
+  have hdcc : DiffContOnCl ℂ f (ball 0 r) := by
+    refine ⟨hf_diffR.mono (ball_subset_ball hrR.le), ?_⟩
+    rw [closure_ball 0 hr.ne']
+    exact hf_diffR.continuousOn.mono (closedBall_subset_ball hrR)
+  have hcauchy := Complex.norm_deriv_le_of_forall_mem_sphere_norm_le hr hdcc hsphere
+  rw [hf_deriv0.deriv] at hcauchy
+  calc ‖deriv h c‖ ≤ 2 * M' * r / (R - r) / r := hcauchy
+    _ = 2 * M' / (R - r) := by field_simp
+
+/-- Entire-part bound (helper): compose the two above via `Re h = log‖g‖`. -/
+private theorem norm_logDeriv_le_of_log_norm_le {g : ℂ → ℂ} {c : ℂ} {R r M' : ℝ}
+    (hr : 0 < r) (hrR : r < R) (hM' : 0 < M')
+    (hg : DifferentiableOn ℂ g (ball c R)) (hne : ∀ z ∈ ball c R, g z ≠ 0)
+    (hbound : ∀ z ∈ ball c R, Real.log ‖g z‖ - Real.log ‖g c‖ ≤ M') :
+    ‖logDeriv g c‖ ≤ 2 * M' / (R - r) := by
+  have hR : 0 < R := hr.trans hrR
+  have hcball : c ∈ ball c R := mem_ball_self hR
+  obtain ⟨h, hh, _hhc, _hexp, hre⟩ := log_branch_of_analytic_nonvanishing hR hg hne
+  have hh_diff : DifferentiableOn ℂ h (ball c R) :=
+    fun z hz => (hh z hz).differentiableAt.differentiableWithinAt
+  have hderiv_c : deriv h c = logDeriv g c := (hh c hcball).deriv
+  have hre_bound : ∀ z ∈ ball c R, (h z).re - (h c).re ≤ M' := by
+    intro z hz
+    rw [hre z hz, hre c hcball]
+    exact hbound z hz
+  have := norm_deriv_le_of_re_le hr hrR hh_diff hM' hre_bound
+  rwa [hderiv_c] at this
+
+"""
+
+
+@dataclass(frozen=True)
+class EntirePartBoundCertificate:
+    """A verified entire-part bound certificate: ``(R, r, M')`` with ``0 < r < R``
+    and ``M' > 0``.  Self-checked identity ``(2 M' r/(R-r))/r = 2 M'/(R-r)`` over ℚ."""
+
+    R: sp.Rational
+    r: sp.Rational
+    Mp: sp.Rational
+
+
+def entire_part_bound_certificate(R, r, Mp) -> EntirePartBoundCertificate:
+    """Build and EXACTLY self-check an entire-part bound certificate.
+
+    Refuses (``ValueError``): ``r ≤ 0`` / ``r ≥ R`` (empty geometry) or ``M' ≤ 0``
+    (degenerate bound) — the negative controls.
+    """
+    Rq, rq, Mq = sp.nsimplify(R), sp.nsimplify(r), sp.nsimplify(Mp)
+    for nm, v in (("R", Rq), ("r", rq), ("M'", Mq)):
+        if not v.is_rational:
+            raise ValueError(f"entire_part_bound parameter {nm} must be rational; got {v!r}")
+    if rq <= 0:
+        raise ValueError(f"entire_part_bound needs r > 0; got r={rq}")
+    if rq >= Rq:
+        raise ValueError(f"entire_part_bound needs r < R; got r={rq}, R={Rq}")
+    if Mq <= 0:
+        raise ValueError(f"entire_part_bound needs M' > 0; got M'={Mq}")
+    lhs = (2 * Mq * rq / (Rq - rq)) / rq
+    rhs = 2 * Mq / (Rq - rq)
+    if sp.simplify(lhs - rhs) != 0:
+        raise ValueError(
+            "entire_part_bound constant self-check failed (2 M' r/(R-r)/r ≠ 2 M'/(R-r)) — rejected"
+        )
+    return EntirePartBoundCertificate(R=Rq, r=rq, Mp=Mq)
+
+
+def certify_entire_part_bound_point(family, pt, name):
+    """Certify one entire_part_bound instance from ``family.special[1](pt)``.
+
+    ``spec(pt)`` returns a dict ``{"R":…, "r":…, "Mp":…}`` or a tuple ``(R, r, Mp)``.
+    """
+    spec = family.special[1](pt)
+    if isinstance(spec, dict):
+        cert = entire_part_bound_certificate(spec["R"], spec["r"], spec["Mp"])
+    elif isinstance(spec, (tuple, list)):
+        cert = entire_part_bound_certificate(spec[0], spec[1], spec[2])
+    else:
+        raise ValueError(f"entire_part_bound spec must be a dict or (R, r, Mp) tuple; got {spec!r}")
+    inst = CertifiedInstance(point=dict(pt), lean_name=name, corners=(), payload=cert)
+    return inst, 1
+
+
+@dataclass
+class EntirePartBoundEmitter(Emitter):
+    """Emit the entire-part bound ``‖logDeriv g c‖ ≤ 2 M'/(R - r)`` from the boundary
+    oscillation ``log‖g z‖ - log‖g c‖ ≤ M'`` of a zero-free `g`.  Self-contained: a
+    fixed 3-lemma preamble (log branch + BC-Cauchy + composition) followed by a
+    concrete-parameter wrapper per instance."""
+
+    def __post_init__(self):
+        self.kind = "entire_part_bound"
+
+    def emit_body(self, fam, profile: LeanProfile) -> tuple[str, int]:
+        lines: list[str] = [_PREAMBLE]
+        nthm = 3  # the three preamble helper lemmas are proved too
+        for inst in fam.instances:
+            cert: EntirePartBoundCertificate = inst.payload  # type: ignore[assignment]
+            base = inst.lean_name
+            Rr, rr, Mr = rat_lean(cert.R), rat_lean(cert.r), rat_lean(cert.Mp)
+            lines.append(
+                f"/-- Entire-part bound on `ball c {Rr}`: zero-free holomorphic `g` with\n"
+                f"    `log‖g z‖ - log‖g c‖ ≤ {Mr}` throughout implies `‖logDeriv g c‖ ≤ 2·{Mr}/({Rr} - {rr})`.\n"
+                f"    A concrete copy of `norm_logDeriv_le_of_log_norm_le`. -/\n"
+                f"theorem {base} (g : ℂ → ℂ) (c : ℂ)\n"
+                f"    (hg : DifferentiableOn ℂ g (ball c ({Rr} : ℝ)))\n"
+                f"    (hne : ∀ z ∈ ball c ({Rr} : ℝ), g z ≠ 0)\n"
+                f"    (hbound : ∀ z ∈ ball c ({Rr} : ℝ),\n"
+                f"      Real.log ‖g z‖ - Real.log ‖g c‖ ≤ ({Mr} : ℝ)) :\n"
+                f"    ‖logDeriv g c‖ ≤ 2 * ({Mr} : ℝ) / (({Rr} : ℝ) - {rr}) :=\n"
+                f"  norm_logDeriv_le_of_log_norm_le (by norm_num) (by norm_num) (by norm_num) hg hne hbound\n"
+            )
+            nthm += 1
+        return "".join(lines), nthm
+
+
+def entire_part_bound_family(
+    name: str,
+    grid: GridSpec,
+    lean_name: Callable,
+    spec: Callable,
+    constants: dict | None = None,
+) -> InequalityFamily:
+    """Build an entire-part bound family (kind='entire_part_bound').
+
+    ``spec``: a callable ``pt -> {"R":…, "r":…, "Mp":…}`` or ``pt -> (R, r, Mp)``.
+    Refuses ``r ≤ 0``, ``r ≥ R``, or ``M' ≤ 0`` at certification."""
+    return InequalityFamily(
+        name=name,
+        symbols=(),
+        grid=grid,
+        lean_name=lean_name,
+        special=("entire_part_bound", spec),
+        constants=dict(constants or {}),
+    )
+
+
+if __name__ == "__main__":
+    print("=== positive certificate R=3/2, r=1/2, M'=6 ===")
+    cert = entire_part_bound_certificate(sp.Rational(3, 2), sp.Rational(1, 2), 6)
+    print(f"cert OK: R={cert.R}, r={cert.r}, M'={cert.Mp}")
+
+    print("\n=== NEGATIVE CONTROL: r ≥ R must raise ===")
+    try:
+        entire_part_bound_certificate(1, 2, 6)
+        raise SystemExit("FAIL: r ≥ R was NOT refused")
+    except ValueError as e:
+        print(f"refused as expected: {e}")
+
+    print("\n=== NEGATIVE CONTROL: M' ≤ 0 must raise ===")
+    try:
+        entire_part_bound_certificate(2, 1, 0)
+        raise SystemExit("FAIL: M'=0 was NOT refused")
+    except ValueError as e:
+        print(f"refused as expected: {e}")
+
+    print("\n=== emitted Lean (preamble + 1 wrapper R=3/2,r=1/2,M'=6) ===")
+    _SPECS = {0: {"R": sp.Rational(3, 2), "r": sp.Rational(1, 2), "Mp": 6}}
+    _NAMES = {0: "entire_part_bound_a"}
+    fam = entire_part_bound_family(
+        "EntirePartBoundSelfTest",
+        GridSpec([("case", [0])]),
+        lambda pt: _NAMES[pt["case"]],
+        spec=lambda pt: _SPECS[pt["case"]],
+    )
+    inst, _ = certify_entire_part_bound_point(fam, {"case": 0}, _NAMES[0])
+
+    class _View:
+        instances = [inst]
+
+    body, nthm = EntirePartBoundEmitter().emit_body(_View(), LeanProfile(namespace=("X",)))
+    print(f"\n-- {nthm} theorems (3 helpers + wrappers) --\n")
+    print(body[:1500])
+    print("...\n[truncated]")
diff --git a/telperion/src/telperion/emit_max_modulus.py b/telperion/src/telperion/emit_max_modulus.py
new file mode 100644
index 00000000..1a0e19f0
--- /dev/null
+++ b/telperion/src/telperion/emit_max_modulus.py
@@ -0,0 +1,191 @@
+"""Maximum-modulus propagation emitter — a sphere norm bound propagates to the disk.
+
+Maximum-modulus principle (norm form): for `f : ℂ → ℂ` holomorphic on the open
+disk `Metric.ball c R` and continuous up to the boundary (`DiffContOnCl`), if
+`‖f z‖ ≤ B` on the boundary sphere `Metric.sphere c R`, then
+
+    ‖f z‖ ≤ B   for all z ∈ Metric.ball c R   (for R ≠ 0).
+
+This is exactly Mathlib's `Complex.norm_le_of_forall_mem_frontier_norm_le`
+(v4.32.0) specialised to a ball, whose frontier is the sphere (`frontier_ball`).
+It is the reusable engine behind the de la Vallee Poussin entire-part argument:
+`log‖g‖ = Re(log g)` is harmonic, so its sup over a disk is attained on the
+boundary, letting a boundary-sphere growth bound propagate inward
+(`examples/zero_free_bridge/lean/DlvpMaxMod.lean:norm_le_on_ball_of_sphere`).
+
+Certificate: `(R, B)` with `R > 0` (refuse `R ≤ 0` — the ball/sphere geometry is
+degenerate and `frontier_ball` needs `R ≠ 0`).
+
+NEGATIVE CONTROL: `R ≤ 0` is REFUSED at certification with a ``ValueError``.
+conjecture1_proved = False.
+"""
+from __future__ import annotations
+
+from dataclasses import dataclass
+from typing import Callable
+
+import sympy as sp
+
+try:  # normal package import
+    from .certify import CertifiedInstance
+    from .expr import rat_lean
+    from .family import GridSpec, InequalityFamily
+    from .lean import LeanProfile
+    from .workflow import Emitter
+except ImportError:  # run directly
+    import os
+    import sys
+
+    sys.path.insert(0, os.path.dirname(os.path.dirname(os.path.abspath(__file__))))
+    from telperion.certify import CertifiedInstance
+    from telperion.expr import rat_lean
+    from telperion.family import GridSpec, InequalityFamily
+    from telperion.lean import LeanProfile
+    from telperion.workflow import Emitter
+
+
+@dataclass(frozen=True)
+class MaxModulusCertificate:
+    """A verified maximum-modulus propagation certificate.
+
+    ``R`` is the disk radius (strictly positive) and ``B`` the boundary bound.
+    The certified fact is the well-posedness ``R > 0`` (so `frontier (ball c R) =
+    sphere c R` holds and the propagation is non-degenerate); the Lean is a
+    concrete-radius wrapper of `Complex.norm_le_of_forall_mem_frontier_norm_le`.
+    """
+
+    R: sp.Rational
+    B: sp.Rational
+
+
+def max_modulus_certificate(R, B) -> MaxModulusCertificate:
+    """Build and EXACTLY self-check a maximum-modulus propagation certificate.
+
+    Refuses (``ValueError``): ``R ≤ 0`` — the negative control (degenerate
+    ball/sphere; `frontier_ball` requires ``R ≠ 0``).
+    """
+    Rq = sp.nsimplify(R)
+    Bq = sp.nsimplify(B)
+    if not Rq.is_rational:
+        raise ValueError(f"max-modulus radius R must be rational; got {R!r}")
+    if not Bq.is_rational:
+        raise ValueError(f"max-modulus boundary bound B must be rational; got {B!r}")
+    if Rq <= 0:
+        raise ValueError(
+            f"max-modulus propagation needs strictly positive radius R > 0; got R={Rq}"
+        )
+    return MaxModulusCertificate(R=Rq, B=Bq)
+
+
+def certify_max_modulus_point(family, pt, name):
+    """Certify one maximum-modulus instance from ``family.special[1](pt)``.
+
+    ``spec(pt)`` returns a dict ``{"R": ..., "B": ...}`` or a tuple ``(R, B)``.
+    """
+    spec = family.special[1](pt)
+    if isinstance(spec, dict):
+        cert = max_modulus_certificate(spec["R"], spec["B"])
+    elif isinstance(spec, (tuple, list)):
+        cert = max_modulus_certificate(spec[0], spec[1])
+    else:
+        raise ValueError(f"max_modulus spec must be a dict or (R, B) tuple; got {spec!r}")
+    inst = CertifiedInstance(point=dict(pt), lean_name=name, corners=(), payload=cert)
+    return inst, 1
+
+
+@dataclass
+class MaxModulusEmitter(Emitter):
+    """Emit the maximum-modulus propagation ``(‖f‖ ≤ B on sphere) → (‖f‖ ≤ B on
+    ball)`` on a disk of concrete radius ``R`` (a wrapper of
+    `Complex.norm_le_of_forall_mem_frontier_norm_le`).  One theorem per instance."""
+
+    def __post_init__(self):
+        self.kind = "max_modulus"
+
+    def emit_body(self, fam, profile: LeanProfile) -> tuple[str, int]:
+        lines: list[str] = ["open Complex Metric\n\n"]
+        nthm = 0
+        for inst in fam.instances:
+            cert: MaxModulusCertificate = inst.payload  # type: ignore[assignment]
+            base = inst.lean_name
+            Rr = rat_lean(cert.R)
+            Br = rat_lean(cert.B)
+            lines.append(
+                f"/-- Maximum-modulus propagation on the disk of radius `{Rr}` about `c`:\n"
+                f"    `f` holomorphic on `ball c {Rr}` (continuous up to the boundary) with\n"
+                f"    `‖f z‖ ≤ {Br}` on `sphere c {Rr}` implies `‖f z‖ ≤ {Br}` throughout `ball c {Rr}`.\n"
+                f"    A concrete-radius wrapper of `Complex.norm_le_of_forall_mem_frontier_norm_le`. -/\n"
+                f"theorem {base} (f : ℂ → ℂ) (c : ℂ)\n"
+                f"    (hd : DiffContOnCl ℂ f (ball c ({Rr} : ℝ)))\n"
+                f"    (hB : ∀ z ∈ sphere c ({Rr} : ℝ), ‖f z‖ ≤ ({Br} : ℝ)) :\n"
+                f"    ∀ z ∈ ball c ({Rr} : ℝ), ‖f z‖ ≤ ({Br} : ℝ) := by\n"
+                f"  intro z hz\n"
+                f"  refine Complex.norm_le_of_forall_mem_frontier_norm_le isBounded_ball hd ?_\n"
+                f"    (subset_closure hz)\n"
+                f"  rw [frontier_ball c (by norm_num : ({Rr} : ℝ) ≠ 0)]\n"
+                f"  exact hB\n"
+            )
+            nthm += 1
+        return "".join(lines), nthm
+
+
+def max_modulus_family(
+    name: str,
+    grid: GridSpec,
+    lean_name: Callable,
+    spec: Callable,
+    constants: dict | None = None,
+) -> InequalityFamily:
+    """Build a maximum-modulus propagation family (kind='max_modulus').
+
+    ``spec``: a callable ``pt -> {"R":…, "B":…}`` or ``pt -> (R, B)``.  Refuses
+    ``R ≤ 0`` at certification (the negative control)."""
+    return InequalityFamily(
+        name=name,
+        symbols=(),
+        grid=grid,
+        lean_name=lean_name,
+        special=("max_modulus", spec),
+        constants=dict(constants or {}),
+    )
+
+
+if __name__ == "__main__":
+    print("=== positive certificate R=1/2, B=12 ===")
+    cert = max_modulus_certificate(sp.Rational(1, 2), 12)
+    print(f"cert OK: R={cert.R}, B={cert.B}")
+
+    print("\n=== NEGATIVE CONTROL: R=0 must raise ValueError ===")
+    try:
+        max_modulus_certificate(0, 12)
+        raise SystemExit("FAIL: R=0 was NOT refused")
+    except ValueError as e:
+        print(f"refused as expected: {e}")
+
+    print("\n=== NEGATIVE CONTROL: R=-1 must raise ValueError ===")
+    try:
+        max_modulus_certificate(-1, 12)
+        raise SystemExit("FAIL: R=-1 was NOT refused")
+    except ValueError as e:
+        print(f"refused as expected: {e}")
+
+    print("\n=== emitted Lean: R=1/2,B=12 and R=1/4,B=3 ===")
+    _SPECS = {0: {"R": sp.Rational(1, 2), "B": 12}, 1: {"R": sp.Rational(1, 4), "B": 3}}
+    _NAMES = {0: "max_modulus_half", 1: "max_modulus_qtr"}
+    fam = max_modulus_family(
+        "MaxModulusSelfTest",
+        GridSpec([("case", [0, 1])]),
+        lambda pt: _NAMES[pt["case"]],
+        spec=lambda pt: _SPECS[pt["case"]],
+    )
+    insts = []
+    for case in (0, 1):
+        inst, _ = certify_max_modulus_point(fam, {"case": case}, _NAMES[case])
+        insts.append(inst)
+
+    class _View:
+        instances = insts
+
+    body, nthm = MaxModulusEmitter().emit_body(_View(), LeanProfile(namespace=("X",)))
+    print(f"\n-- {nthm} theorems --\n")
+    print(body)
diff --git a/telperion/tests/test_emit_dvp_bc_atoms.py b/telperion/tests/test_emit_dvp_bc_atoms.py
new file mode 100644
index 00000000..798241ac
--- /dev/null
+++ b/telperion/tests/test_emit_dvp_bc_atoms.py
@@ -0,0 +1,108 @@
+"""dVP entire-part (i-b') emitters (max_modulus, bc_deriv_re, entire_part_bound):
+self-check / negative-control + emitted-Lean shape.  Kernel verification of the emitted
+Lean is in CI (job `dvp-bc-atoms-compiles`) + examples/dvp_bc_atoms.  conjecture1_proved = False.
+"""
+from fractions import Fraction
+
+import pytest
+
+from telperion.emit_bc_deriv_re import (
+    BCDerivReEmitter, bc_deriv_re_certificate, bc_deriv_re_family, certify_bc_deriv_re_point,
+)
+from telperion.emit_entire_part_bound import (
+    EntirePartBoundEmitter, certify_entire_part_bound_point, entire_part_bound_certificate,
+    entire_part_bound_family,
+)
+from telperion.emit_max_modulus import (
+    MaxModulusEmitter, certify_max_modulus_point, max_modulus_certificate, max_modulus_family,
+)
+from telperion.family import GridSpec
+from telperion.lean import LeanProfile
+
+
+def _emit_one(fam_fn, emitter_cls, spec, name):
+    fam = fam_fn(
+        "T", GridSpec([("case", [0])]), lambda pt: name, spec=lambda pt: spec
+    )
+    kind = fam.special[0]
+    certify_fn = {
+        "max_modulus": certify_max_modulus_point,
+        "bc_deriv_re": certify_bc_deriv_re_point,
+        "entire_part_bound": certify_entire_part_bound_point,
+    }[kind]
+    inst, nchk = certify_fn(fam, {"case": 0}, name)
+    assert nchk == 1
+
+    class _View:
+        instances = [inst]
+
+    e = emitter_cls()
+    e.__post_init__()
+    body, nthm = e.emit_body(_View(), LeanProfile(namespace=("T",)))
+    return body, nthm
+
+
+# ---- max_modulus --------------------------------------------------------------------
+def test_max_modulus_certificate_and_shape():
+    c = max_modulus_certificate(Fraction(1, 2), 12)
+    assert (c.R, c.B) == (Fraction(1, 2), Fraction(12, 1))
+    body, nthm = _emit_one(max_modulus_family, MaxModulusEmitter, {"R": "1/2", "B": 12}, "mm")
+    assert nthm == 1
+    assert "open Complex Metric" in body
+    assert "Complex.norm_le_of_forall_mem_frontier_norm_le isBounded_ball hd" in body
+    assert "rw [frontier_ball c (by norm_num : ((1 / 2) : ℝ) ≠ 0)]" in body
+    assert "∀ z ∈ ball c ((1 / 2) : ℝ), ‖f z‖ ≤ (12 : ℝ)" in body
+
+
+def test_max_modulus_negative_control_nonpositive_radius():
+    with pytest.raises(ValueError, match="strictly positive radius"):
+        max_modulus_certificate(0, 12)
+    with pytest.raises(ValueError, match="strictly positive radius"):
+        max_modulus_certificate(-1, 12)
+
+
+# ---- bc_deriv_re --------------------------------------------------------------------
+def test_bc_deriv_re_certificate_and_shape():
+    c = bc_deriv_re_certificate(Fraction(3, 2), Fraction(1, 2), 6)
+    assert (c.R, c.r, c.Mp) == (Fraction(3, 2), Fraction(1, 2), Fraction(6, 1))
+    body, nthm = _emit_one(
+        bc_deriv_re_family, BCDerivReEmitter, {"R": "3/2", "r": "1/2", "Mp": 6}, "bd"
+    )
+    assert nthm == 1
+    assert "Complex.borelCaratheodory_zero hM' hf_diffR hmaps_re hR hzball hf0" in body
+    assert "Complex.norm_deriv_le_of_forall_mem_sphere_norm_le hr hdcc hsphere" in body
+    assert "‖deriv h c‖ ≤ 2 * (6 : ℝ) / (((3 / 2) : ℝ) - (1 / 2))" in body
+
+
+def test_bc_deriv_re_negative_controls():
+    with pytest.raises(ValueError, match="r < R"):
+        bc_deriv_re_certificate(1, 2, 6)
+    with pytest.raises(ValueError, match="M' > 0"):
+        bc_deriv_re_certificate(2, 1, 0)
+    with pytest.raises(ValueError, match="r > 0"):
+        bc_deriv_re_certificate(2, 0, 6)
+
+
+# ---- entire_part_bound --------------------------------------------------------------
+def test_entire_part_bound_certificate_and_shape():
+    c = entire_part_bound_certificate(Fraction(3, 2), Fraction(1, 2), 6)
+    assert (c.R, c.r, c.Mp) == (Fraction(3, 2), Fraction(1, 2), Fraction(6, 1))
+    body, nthm = _emit_one(
+        entire_part_bound_family, EntirePartBoundEmitter, {"R": "3/2", "r": "1/2", "Mp": 6}, "ep"
+    )
+    # 3 preamble helper lemmas + 1 wrapper
+    assert nthm == 4
+    assert "private theorem log_branch_of_analytic_nonvanishing" in body
+    assert "private theorem norm_deriv_le_of_re_le" in body
+    assert "private theorem norm_logDeriv_le_of_log_norm_le" in body
+    assert (
+        "norm_logDeriv_le_of_log_norm_le (by norm_num) (by norm_num) (by norm_num) hg hne hbound"
+        in body
+    )
+
+
+def test_entire_part_bound_negative_controls():
+    with pytest.raises(ValueError, match="r < R"):
+        entire_part_bound_certificate(1, 2, 6)
+    with pytest.raises(ValueError, match="M' > 0"):
+        entire_part_bound_certificate(2, 1, 0)