Counterfeit ladder: kernel-checked ζ_K (ℚ(√−5)) vs Epstein x²+5y² window separation + orbit-6 witnesses

[DrMurphyIsIn]

Stacked on #622 (Crux3), which is stacked on #615.

This PR adds the first kernel-checked window separation between an L-function that has an Euler product and a same-functional-equation counterfeit that doesn't.

theorem CF.window_separation_cE :
    0 < ∫ x, ‖v x‖^2 ∧ 3 * ∫‖v‖^2 ≤ Re W_{ζ_K}(v⋆ṽ) ∧ Re W_E(v⋆ṽ) ≤ -(3/20) * ∫‖v‖^2

The objects

• Test function: one nonzero 9-mode test at window x = e^{18π/17} ≈ 27.8.
• ζ_K: the Dedekind zeta of ℚ(√−5), with weights Λ(n)(1+χ₋₂₀(n)).
• E: the Epstein zeta ½Σ′(x²+5y²)^{−s}, normalized so a(1) = 1. Its lattice counts are computed in the kernel.
  • E's −E′/E coefficient recursion is a hypothesis of the theorem. It is discharged by cE_conv, and eq_cE_of_conv proves the coefficients are unique.
• Archimedean side: Γ_ℂ with conductor 20, with both pole terms kept.

Other results

• Lemma O witnesses: c_D(6) = (1+κ²) log 6 ≠ 0, c_E(6) = 2 log 6 ≠ 0, and 6 is not a prime power. Each counterfeit has a "prime orbit" at a composite length.
• Tamper controls: the kernel rejects all three.

Verification

• Guard: CF_AxiomGuard has 54 lines, all standard. My rebuild ran 8788 jobs.
• CI: the anchors are also appended to the required AxiomGuardRvMBridge.
• Own-session skeptic: not refuted. It re-derived Γ_ℂ with conductor 20 and reproduced the −E′/E recursion, the zero-side cross-checks and E's off-line quadruple (−1.825).

Not formalized

• The explicit formula linking these functionals to their zero sums. It's checked numerically, to about 4e-5.
• ζ_K positivity on the whole 9-mode family. Only at-the-test positivity is proved; the span's minimum eigenvalue is about 1e-4.

Lane B numerics

These are in telperion/research/counterfeit_ladder_CF/laneB/.

• Certified gap: full-class λ_min(ζ_K) ≥ 3.44e-3 at x = 20, where E is certified negative (x_E ≈ 19.82).
• Independent confirmation: a peer-session skeptic confirmed this and proved the Loewner off-diagonal identity (PEER_SKEPTIC_VERDICT.md).
• Lean cost: a full-class Lean theorem is about 10³–10⁴× current budgets unless restructured. That restructuring is the Step 2 lane.

conjecture1_proved = False.

🤖 Generated with Claude Code

https://claude.ai/code/session_01LMeoWeTz2Q3iSeLfqxfYo6