Crux3: kernel-checked ζ vs Davenport–Heilbronn separation on a 2-mode Weil band (x = e^{9π/7})

[DrMurphyIsIn]

This PR adds a kernel-checked certificate on one explicit test function. On that test, ζ's Weil form is positive, and the same construction applied to the Davenport–Heilbronn function D is provably negative. D is the standard counterexample-in-waiting: it has a functional equation but zeros off the line. So this is a small, fully formal instance of a positivity certificate that separates ζ from D. It's the check that round 2 of the crux research asked for. It is a finite 2-mode instance, not RH.

The instance

• The window is A = 9π/14, so x = e^{9π/7} ≈ 56.78.
• The test is v = c₁ cos(763u/9) + c₂ cos(259u/3) on [−A, A]. This band sits at heights of roughly 83–88.

Kernel-checked (rvm_bridge island, stacked on #615 for KWin_Data / KWin_Taylor)

• Crux3.band_floor: Re W(v ⋆ ṽ) ≥ ½‖v‖² for every (c₁, c₂). It has no hypotheses and is stated on the registry's own functional (archSide − primeSide, with Mathlib's vonMangoldt). In round-2 form, band_comb_le / band_arch_ge show comb ≤ 1.92‖v‖² < 2.49‖v‖² ≤ arch.
• Crux3.dh_band_negative: D's explicit-formula functional is ≤ −½‖v‖² at c* = (−3, 2). The certified majorant is −0.544.
  • That functional is log(5/π)g(0) + (1/2π)∫h Re ψ(3/4+ir/2) − Σ c(n)/√n (g(log n)+g(−log n)), and it is defined outside the registry.
  • Its only hypothesis is the defining identity of the −D′/D coefficients on [1, 56], which covers every n the sum uses. band_separation_cD discharges it with cD_conv, so it's not vacuous.
• Crux3.band_separation: both statements hold on the same nonzero test.
• Other ingredients: an exact-rational κ/log/cos table checked by decide +kernel (dtab_ok), with tamper negative controls (dtab_tamper, tab_tamper).
• Peer-session skeptic (different session, same git identity; unverified under missions: grant provenance, self-audit refusal, independent Comparator judge #607), at 50fd1bc: NOT REFUTED. Its own mpmath reproduces every number, and it confirms the dh hypothesis is D's true −D′/D recursion (unique and non-vacuous), not a list.

Verification

• My rebuild on this branch: lake build AxiomGuardRvMBridge ran 8881 jobs. All 54 Crux3.* guard lines (in a 1005-report guard) print exactly [propext, Classical.choice, Quot.sound], with no sorryAx and no errors.
• Merge hygiene: the lakefile and guard were merged structurally, adding only the 7 Crux3 libraries.
• Lane skeptic (a subagent of my own session, so NOT independent under missions: grant provenance, self-audit refusal, independent Comparator judge #607), not refuted:
  • It re-elaborated all 7 files from scratch (peak 7.2 GB, 27 s for Crux3_BandDH).
  • It re-derived D's explicit formula itself: gamma factor Γ((s+1)/2), conductor 5, no pole. It matches archSideD/primeSideD exactly.
  • Its own c(n) recursion matches the Lean table on all 40 nonzero entries.
  • Its own mpmath numerics give ζ band λ_min = +0.699 and D band λ_min = −0.6546. D's off-line zero is at 0.808517 + 85.699348i, and its quadruple contributes −1.046‖v‖².

Limits (stated, not hidden)

• Test class: band_floor's tests are Lipschitz band functions cut off at ±A, so they lie OUTSIDE IsWeilTest (which requires C∞). The functional is evaluated on them directly, and the integrability that needs is proved. This is the disclosure in Crux3_BandDH.lean.
• The explicit formula linking weilFormD to D's zeros is not formalized. It is checked only numerically: the zero side gives −0.65464 and the arithmetic side −0.65462.
• Partial no-go, computed evidence only: at round 2's target x = 40, no height-local band of up to 16 modes detects D's zero; D's least band eigenvalue there is ≥ +0.095. The band-local horizon is x ≈ 42.1, against x ≈ 31 for the full window.
• No registry nodes yet. The proposed nodes are listed (unregistered) in the doc's "Proposed registry nodes" section.

conjecture1_proved = False.

🤖 Generated with Claude Code

https://claude.ai/code/session_01LMeoWeTz2Q3iSeLfqxfYo6