Formalize Jensen, Li, and Weil RH route foundations

[FluffyAIcode]

Dependency

Stacked on PR #236 (AgentMemory/architecture9-cursor-oprover-0727, head dc44e199e45f2abea1e7b4f5f7c168e0309b4a1a). This PR must not merge before its base dependency.

Summary

• preserve the first three route-foundation stages already present at df12d665
• reconcile all reported stage-4 Git histories and integrate only the clean verified frozen snapshots:
  • Jensen c860dde0cc3e3f68ecdf2ebbe394a31c1d8b01bf
  • Li b754dac71f5a7c66e4e611f50e9ec3338764681e
  • Weil 45a0279cb436ac2961b8cfde97e5b4895db2caa8
• keep the unverified iter24 Weil contour worktree diff out of this PR; it remains a separate 35-line local modification
• update the Jensen source-card validator for the route's more precise, anti-overclaim statuses

Certification outcome

Architecture 9 processed eight content-addressed high-value artifacts across Jensen, Li, and Weil. Existing theorem bodies were hidden from OProver prompts and candidates were checked in isolated Lean source prefixes.

• all eight existing theorems remain Lean-verified
• OProver Q4 independently reconstructed none of the eight; each is recorded as INDEPENDENT_RECONSTRUCTION_FAILED
• supporting lemmas therefore remain Lean-verified but are not multi-model certified
• conditional bridges are recorded separately and do not close any RH obligation
• Gemma Critic reviewed meaning, assumptions, circularity, RH relation, and overclaim risk after residency restore
• Host/Judge made no production proof-ledger updates and no artifact claims an RH proof

Private certification artifacts, residency journals, model output, weights, and runtime state are not committed.

Proof status and exact non-claims

• Jensen: riemannHypothesis_of_allJensenHyperbolic is conditional on every shifted Jensen polynomial being hyperbolic. The remaining coefficient-side blocker is the all-degree unshifted family, equivalently the finite weighted Schur--Szego/matching theorem or full finite ASW bridge.
• Li: the genus-one Hadamard representation, slope identity, and all-order change-of-variables coefficient identity are unconditional. RH → Li positivity still requires the all-index zero-window formula; no positivity-to-RH equivalence is claimed here.
• Weil: local separator negativity and the formula contradiction are conditional support. Actual use still requires RvM-scale xi boundary growth, the outer-minus-inner contour/residue decomposition, finite Guinand--Weil with prime/Gamma evaluation, normal convergence/tail domination, and arithmetic-side positivity.
• no theorem in this PR proves RH; no sorry, admit, or axiom is introduced.

Validation

• lake build — 3,782 jobs, success
• lake env lean tests/lean/RHJensenTest.lean — success
• lake env lean tests/lean/LiCriterionTest.lean — success
• lake env lean KakeyaLeanGate/WeilPositivity.lean — success
• route/source validators — 11 passed
• scripts/run_local_ci.sh — 1,384 passed, 10 skipped; shipping-module coverage 100%
• exact frozen-snapshot comparisons for Jensen, Li, and Weil — clean
• git diff --check, no-sorry/admit/axiom scan, and changed-route secret scan — clean

Operational safety

The proof supervisor stayed idle. Ledger, live checkpoint, and residency state were snapshotted before and after certification. OProver used its separate Q4 cache namespace under the exclusive residency scheduler, was unloaded, and Gemma was restored. Final health showed Primary and Allens online with Gemma resident and no OProver process.

No production worktree source, weights, caches, candidate.py, private logs, secrets, or runtime artifacts are included. Do not merge this PR as part of certification.

Made with Cursor

[cursor]

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.