feat(telperion): three new dVP entire-part certificate emitters - #232
Merged
Conversation
…modulus, bc_deriv_re, entire_part_bound)
Promotes the reusable, function-agnostic certificate shapes distilled from this session's
obligation-(i-b') Lean work into first-class Telperion emitters (per the build standing order):
* max_modulus — maximum-modulus propagation: ‖f‖≤B on sphere c R ⟹ ‖f‖≤B on ball c R
(wraps Complex.norm_le_of_forall_mem_frontier_norm_le). NC: R ≤ 0.
* bc_deriv_re — real-part → derivative bound: (h z).re-(h c).re ≤ M' ⟹ ‖deriv h c‖ ≤ 2M'/(R-r)
(Borel-Caratheodory + Cauchy composite; the engine nothing else in the
registry provides — cauchy_deriv only wraps the raw sphere-NORM estimate).
NC: r ≤ 0, r ≥ R, M' ≤ 0; exact self-check (2M'r/(R-r))/r = 2M'/(R-r).
* entire_part_bound — ‖logDeriv g c‖ ≤ 2M'/(R-r) from the log‖g‖ oscillation; self-contained via a
3-lemma preamble (log branch + BC-Cauchy + composition). NC as bc_deriv_re.
Each: cert dataclass + sympy self-check/negative-control + Lean emit + family + certify_point,
registered in certify._SPECIAL_KINDS/_SPECIAL_DISPATCH, exported in __init__. Example project
examples/dvp_bc_atoms (3 lean_libs, drift-checkable generate.py) — all three emitted files build
kernel-clean (#print axioms → [propext, Classical.choice, Quot.sound]). tests/test_emit_dvp_bc_atoms.py
(6). CI: dvp-bc-atoms-compiles. Complements the 2026-09-02 bc_split/jensen_zero_count/sphere_bound
batch. conjecture1_proved = False (NOT a proof of RH).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01NzN1Gt4Fqo9uKNst5zhred
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Promotes the reusable certificate shapes distilled from this session's obligation-(i-b') Lean work into first-class Telperion emitters (per
telperion_build_standing_order), complementing the 2026-09-02bc_split/jensen_zero_count/sphere_boundbatch. All three are function-agnostic and self-contained (import Mathlib).max_modulus‖f‖ ≤ Bonsphere c R⟹‖f‖ ≤ Bonball c R(maximum modulus)R ≤ 0bc_deriv_re(h z).re − (h c).re ≤ M'⟹‖deriv h c‖ ≤ 2M'/(R−r)(Borel–Carathéodory + Cauchy)r ≤ 0,r ≥ R,M' ≤ 0; exact(2M'r/(R−r))/r = 2M'/(R−r)self-checkentire_part_bound‖logDeriv g c‖ ≤ 2M'/(R−r)from thelog‖g‖oscillation (self-contained 3-lemma preamble)bc_deriv_reWhy
bc_deriv_reis the notable new shape: the existingcauchy_derivemitter only wraps the raw Cauchy estimate (‖f'‖ ≤ M/Rfrom a sphere norm bound).bc_deriv_regoes from a bound on the real part to the derivative — the full BC→Cauchy composite — which nothing else in the ~90-emitter registry provides.Recipe (each emitter)
cert dataclass + sympy self-check/negative-control + Lean
emit_body+family+certify_point, registered incertify._SPECIAL_KINDS/_SPECIAL_DISPATCH, exported in__init__.Verification
examples/dvp_bc_atoms(3lean_libs, drift-checkablegenerate.py) — all three emitted files build kernel-clean;#print axioms→[propext, Classical.choice, Quot.sound].tests/test_emit_dvp_bc_atoms.py(6 passing) — positive certs + negative controls + emitted-Lean shape.dvp-bc-atoms-compiles(pytest + drift-check +lake build).conjecture1_proved = False— reusable certificate tooling, not a proof of RH.🤖 Generated with Claude Code
https://claude.ai/code/session_01NzN1Gt4Fqo9uKNst5zhred