diff --git a/telperion/missions/anduril/nodes/AND_checkline_correct.toml b/telperion/missions/anduril/nodes/AND_checkline_correct.toml index e841f3e40..271c68f9d 100644 --- a/telperion/missions/anduril/nodes/AND_checkline_correct.toml +++ b/telperion/missions/anduril/nodes/AND_checkline_correct.toml @@ -5,7 +5,14 @@ name = "AND.checkline_correct" statement_module = "Statements.AND_checkline_correct" status = "proved" title = "A4 reflection core: checkLine_correct -- the once-proven correctness theorem for the Boolean band checker over dyadic-interval sign boxes (BandData -> Bool; per-band certificates become data discharged by decide, not tactic scripts)" -updated = "2026-09-14" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "2d2122b5ea765096f79c75eb7e15e2bca990abde91eeb2892ed60cf3e9003ca9" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "ZetaReflection.checkLine_correct" [proof] artifact = "../../examples/zeta_reflection/lean/CheckBand.lean" diff --git a/telperion/missions/anduril/nodes/AND_edge_clear_glue.toml b/telperion/missions/anduril/nodes/AND_edge_clear_glue.toml index 7faa86a69..848c977ad 100644 --- a/telperion/missions/anduril/nodes/AND_edge_clear_glue.toml +++ b/telperion/missions/anduril/nodes/AND_edge_clear_glue.toml @@ -5,7 +5,14 @@ name = "AND_edge_clear_glue" statement_module = "Statements.AND_edge_clear_glue" status = "proved" title = "Edge-clear glue K1, H2b discharged: riemannZeta(-1 + iy) != 0 for every real y (every band edge), hypothesis-free (zeta_zero_re_mem_strip off the real axis, zeta(-1) = -1/12 on it). Removes the hnzl Arb input from all 10,379 bands. conjecture1_proved = False" -updated = "2026-09-23" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "87b49f69b0fc1d45d63554cde4871c0892c47794deaab1ba9dd93a5b963766e4" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "EdgeClearGlue.hnzl_discharged" [proof] artifact = "../../examples/zeta_reflection/lean/EdgeClearGlue.lean" diff --git a/telperion/missions/anduril/nodes/AND_em_tail3_number.toml b/telperion/missions/anduril/nodes/AND_em_tail3_number.toml index 25806757f..dd91f0f19 100644 --- a/telperion/missions/anduril/nodes/AND_em_tail3_number.toml +++ b/telperion/missions/anduril/nodes/AND_em_tail3_number.toml @@ -5,7 +5,14 @@ name = "AND.em_tail3_number" statement_module = "Statements.AND_em_tail3_number" status = "proved" title = "Order-K EM tail engine, THE NUMBER: the order-3 Euler-Maclaurin tail remainder is kernel-decided below 10^-3 (em_tail3_number; the shared substrate for Stirling K=4 and the A3 theta branch)" -updated = "2026-09-14" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "e6bc26aa570d9a5a6b777cb109ca9264fc347bb2ecd9cc97f034aef55ecc1971" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "ZetaReflection.em_tail3_number" [proof] artifact = "../../examples/zeta_reflection/lean/EMZetaTail.lean" diff --git a/telperion/missions/anduril/nodes/AND_em_zeta_strip.toml b/telperion/missions/anduril/nodes/AND_em_zeta_strip.toml index 2b753ffc0..9bd2a381b 100644 --- a/telperion/missions/anduril/nodes/AND_em_zeta_strip.toml +++ b/telperion/missions/anduril/nodes/AND_em_zeta_strip.toml @@ -5,7 +5,14 @@ name = "AND.em_zeta_strip" statement_module = "Statements.AND_em_zeta_strip" status = "proved" title = "A2 E-track headliner: the verified Euler-Maclaurin representation of zeta continued into the critical strip -- zeta(s) = 1/(s-1) + 1/2 + integral of sawBernoulli-weighted power tail, for 0 < Re s, s /= 1 (em_zeta_strip, E3 of the em-complex agent)" -updated = "2026-09-14" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "ce7031478870c994999a64a2a30b3f5f54fbd0bb0c4e0dc2971bc8481aee4694" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "ZetaReflection.em_zeta_strip" [proof] artifact = "../../examples/zeta_reflection/lean/EMZetaComplex.lean" diff --git a/telperion/missions/anduril/nodes/AND_first_zero_kernel.toml b/telperion/missions/anduril/nodes/AND_first_zero_kernel.toml index 4caaef83c..3cb51ceed 100644 --- a/telperion/missions/anduril/nodes/AND_first_zero_kernel.toml +++ b/telperion/missions/anduril/nodes/AND_first_zero_kernel.toml @@ -5,7 +5,14 @@ name = "AND.first_zero_kernel" statement_module = "Statements.AND_first_zero_kernel" status = "proved" title = "REFLECTION CAPSTONE: first_zero_kernel -- an argument-free, hypothesis-free nontrivial zeta zero in (14, 15), verified entirely by kernel computation over rational certificates (no Arb enclosure hypotheses). The first purely-kernel-COMPUTED nontrivial zero of the completed zeta function; the reflection track's answer to what the T5 band certificates supply as data." -updated = "2026-09-15" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "006066975be65a7dd48b5abb0d01d8dc48226bf3c7d1a501ac40e25a703c8d2d" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "ForgeFirstZeroKernel.first_zero_kernel" [proof] artifact = "../../examples/zeta_reflection/lean/ForgeFirstZeroKernel.lean" diff --git a/telperion/missions/anduril/nodes/AND_g2_reflected_band_kernel.toml b/telperion/missions/anduril/nodes/AND_g2_reflected_band_kernel.toml index a683bb860..cc8506101 100644 --- a/telperion/missions/anduril/nodes/AND_g2_reflected_band_kernel.toml +++ b/telperion/missions/anduril/nodes/AND_g2_reflected_band_kernel.toml @@ -5,7 +5,14 @@ name = "AND_g2_reflected_band_kernel" statement_module = "Statements.AND_g2_reflected_band_kernel" status = "proved" title = "G2 hypothesis-free companion: two zeros of completedRiemannZeta on the critical line with heights in [14, 22], proved entirely in the kernel (wide kernel-proved boxes dK replace the tight Arb boxes of AND_g2_reflected_band; no Arb or oracle input). Finite verification only, NOT RH. conjecture1_proved = False" -updated = "2026-09-23" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "856fe02ed950c1a75152fcbf37e45ac3ef49081f2073ec191d639f666d6e540a" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "ReflectedBand_t14_Kernel.pilot_kernel" [proof] artifact = "../../examples/zeta_reflection/lean/ReflectedBand_t14_Kernel.lean" diff --git a/telperion/missions/anduril/nodes/AND_height_floor_kernel.toml b/telperion/missions/anduril/nodes/AND_height_floor_kernel.toml index caff0a349..777c30de6 100644 --- a/telperion/missions/anduril/nodes/AND_height_floor_kernel.toml +++ b/telperion/missions/anduril/nodes/AND_height_floor_kernel.toml @@ -5,7 +5,14 @@ name = "AND_height_floor_kernel" statement_module = "Statements.AND_height_floor_kernel" status = "proved" title = "Height floor, hypothesis-free: no zero of riemannZeta has 0 < Im rho < 55/16 (for every height bound H). Kernel-proved (order-3 Euler-Maclaurin at N = 2 plus 32 exact interval boxes); discharges the ladder capstones' hgamma input at every height. Finite verification only, NOT RH. conjecture1_proved = False" -updated = "2026-09-23" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "7a44c94b06aabc1c8a43fa7684238986833573ce71a0de68a24c3ab040d41529" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "HeightFloor.height_floor" [proof] artifact = "../../examples/zeta_reflection/lean/HeightFloor.lean" diff --git a/telperion/missions/anduril/nodes/AND_stirling_binet_k1.toml b/telperion/missions/anduril/nodes/AND_stirling_binet_k1.toml index 2ed8d652c..afee71d8e 100644 --- a/telperion/missions/anduril/nodes/AND_stirling_binet_k1.toml +++ b/telperion/missions/anduril/nodes/AND_stirling_binet_k1.toml @@ -5,7 +5,14 @@ name = "AND.stirling_binet_k1" statement_module = "Statements.AND_stirling_binet_k1" status = "proved" title = "A2 Stirling/Binet K=1: logDeriv_gammaR_stirling -- the Gamma_R logarithmic derivative with explicit Binet remainder on Re z > 0 (serves both the Gamma_R edges and, at K=4 via the tail engine, the A3 theta branch)" -updated = "2026-09-14" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "4fbeebdc3b84d1b5486cf6a2fd71ccda6200424ca79c96f3cc3a384f4818860f" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "ZetaReflection.logDeriv_gammaR_stirling" [proof] artifact = "../../examples/zeta_reflection/lean/StirlingBinet.lean" diff --git a/telperion/missions/anduril/nodes/AND_theta_branch.toml b/telperion/missions/anduril/nodes/AND_theta_branch.toml index f34f20712..960d1b803 100644 --- a/telperion/missions/anduril/nodes/AND_theta_branch.toml +++ b/telperion/missions/anduril/nodes/AND_theta_branch.toml @@ -5,7 +5,14 @@ name = "AND_theta_branch" statement_module = "Statements.AND_theta_branch" status = "proved" title = "Riemann-Siegel brick B0 (theta): for every t > 0 the Gauss-product branch limit of Im log Gamma(1/4 + it/2) exists and lies within 1/t of the RS main term after the (t/2) log pi shift. A height-uniform phase bound for the finite-verification ladder, NOT RH. conjecture1_proved = False" -updated = "2026-09-23" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "35c4dcb74e8b56cc7362ac49a664707a786ccce38598355f5dd798fa760cb3c3" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RSDesignTheta.gaussBranch_theta_sub_thetaMain_le" [proof] artifact = "../../examples/zeta_reflection/lean/RSTheta.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_effective_gaussian_dominance.toml b/telperion/missions/mirrormere/nodes/MM_effective_gaussian_dominance.toml index 5ebcd741e..5a7efa5d7 100644 --- a/telperion/missions/mirrormere/nodes/MM_effective_gaussian_dominance.toml +++ b/telperion/missions/mirrormere/nodes/MM_effective_gaussian_dominance.toml @@ -5,7 +5,14 @@ name = "MM.effective_gaussian_dominance" statement_module = "Statements.MM_effective_gaussian_dominance" status = "proved" title = "OPEN LEMMA 1 DISCHARGED (2026-09-21): EFFECTIVE Gaussian dominance -- an off-line zero of maximal distance y0 from the line within its height window (radius D >= 1), with local spacing floor xmin > 0, window multiplicity count <= N and tail constant B, makes the Gaussian zero sum at its ordinate strictly negative for every width above the EXPLICIT effectiveThreshold(y0, xmin, N, B, D) = max(1, log(4N(D^2+1/4)/y0^2)/(2 xmin^2), log(4B/y0^2)/(2 y0^2)). The spacing floor is load-bearing (threshold unbounded as xmin -> 0): this is the short-range clustering control the wall sweep named as the open input. Nothing about RH. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "fdfa6ea5470a0d113182a9ad6d7b8e4543203d584314516ea9a01fe8590dbd1e" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge14.effective_gaussian_dominance" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge14.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_effective_threshold_unbounded.toml b/telperion/missions/mirrormere/nodes/MM_effective_threshold_unbounded.toml index 2358094a0..e0816c3bb 100644 --- a/telperion/missions/mirrormere/nodes/MM_effective_threshold_unbounded.toml +++ b/telperion/missions/mirrormere/nodes/MM_effective_threshold_unbounded.toml @@ -5,7 +5,14 @@ name = "MM.effective_threshold_unbounded" statement_module = "Statements.MM_effective_threshold_unbounded" status = "proved" title = "OPEN LEMMA 1, the load-bearing hypothesis made explicit (2026-09-21): the spacing floor in effective Gaussian dominance cannot be dropped -- for every distance floor 0 < y0 <= 1/2, window count N >= 1, window half-width D >= 1, tail constant B and every bound K, there is a spacing floor xmin > 0 with effectiveThreshold(y0, xmin, N, B, D) >= K, i.e. the explicit threshold max(1, log(4N(D^2+1/4)/y0^2)/(2 xmin^2), log(4B/y0^2)/(2 y0^2)) is unbounded as xmin -> 0. Pure real arithmetic on the threshold formula; this is why short-range clustering control (the wall sweep's named open input) is exactly the data a consumer must certify. The main theorem RvMBridge14.effective_gaussian_dominance (E6Bridge14, 14 guarded theorems, 3-axiom) IS registered as MM_effective_gaussian_dominance (2026-09-21, zeroWindow mirrored via the zeroFinset sorry-scaffold precedent). Nothing about RH. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "fdfa6ea5470a0d113182a9ad6d7b8e4543203d584314516ea9a01fe8590dbd1e" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge14.effectiveThreshold_unbounded_of_small_spacing" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge14.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_gaussian_approx.toml b/telperion/missions/mirrormere/nodes/MM_gaussian_approx.toml index 38b89188a..fabe935e7 100644 --- a/telperion/missions/mirrormere/nodes/MM_gaussian_approx.toml +++ b/telperion/missions/mirrormere/nodes/MM_gaussian_approx.toml @@ -5,7 +5,14 @@ name = "MM.gaussian_approx" statement_module = "Statements.MM_gaussian_approx" status = "proved" title = "Obligation O1' (GaussianApprox): for every centre c and lam > 0 there are Weil tests g_n whose Hermitian transforms converge to the Gaussian-derivative transform G_{c,lam} pointwise on the strip |Im z| <= 1/2 with a truncation-uniform bound C/(1+|z|^2). A statement about test functions only, no zeros: pure Fourier analysis (complex-argument Gaussian transform via integral_cexp_quadratic + truncation-uniform integration by parts against a ContDiffBump cutoff). Open-research-grade formalization; NOT RH-hard; discharges O1 through the proved RvMBridge6.gaussianTransfer_of_approx. Stopped 2026-09-20 at the Fourier side (memo WEIL_CONVERSE_ATTACK_2026-09-20 section 4). conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "185113ae9651ab22a133146d82d2e1614f2838a9e09119a238bdd9e809d7558b" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge8.gaussian_approx" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge8.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_gaussian_dominance.toml b/telperion/missions/mirrormere/nodes/MM_gaussian_dominance.toml index e1890f108..e7a65f21d 100644 --- a/telperion/missions/mirrormere/nodes/MM_gaussian_dominance.toml +++ b/telperion/missions/mirrormere/nodes/MM_gaussian_dominance.toml @@ -5,7 +5,14 @@ name = "MM.gaussian_dominance" statement_module = "Statements.MM_gaussian_dominance" status = "proved" title = "Obligation O2 (GaussianDominance), the analytic heart of the Weil converse: if rho_0 is a nontrivial zero off the critical line then for some real centre c and some lam > 0 the Gaussian-weighted zero sum Sum_rho m(rho) (gamma_rho - c)^2 exp(-2 lam (gamma_rho - c)^2) has strictly negative real part. Weil/Bombieri localisation: generic centre within |1/2 - Re rho_0| of Im rho_0, the argmax of (Im gamma)^2 - (Re gamma - c)^2 over the zeros (attained, off-line, unique up to the pair rho <-> 1 - conj rho), a phase choice along lam_k -> infinity, and a tail bound from the local zero count. A statement about the zeros of zeta alone; vacuously true under RH, but its intended proof does not use RH; NOT RH-hard; open. This is where the converse attack stopped on 2026-09-20. conjecture1_proved = False." -updated = "2026-09-20" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "15759dbb3e20249bdc4b044900289ed0293e80c58f7c4eef41e82ba27eb63090" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge7.gaussian_dominance" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge7.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_gaussian_explicit_formula.toml b/telperion/missions/mirrormere/nodes/MM_gaussian_explicit_formula.toml index 14bd834f1..01a2d26df 100644 --- a/telperion/missions/mirrormere/nodes/MM_gaussian_explicit_formula.toml +++ b/telperion/missions/mirrormere/nodes/MM_gaussian_explicit_formula.toml @@ -5,7 +5,14 @@ name = "MM.gaussian_explicit_formula" statement_module = "Statements.MM_gaussian_explicit_formula" status = "proved" title = "WALL ASSAULT seam A: the Gaussian explicit formula -- the Gaussian-weighted zero sum equals archSide minus primeSide of the Hermitian autocorrelation of the Gaussian-derivative test gaussPhi (not compactly supported): E8 on the truncations gaussTests, passed to the limit by dominated convergence on all three sides; honest values (integrability/summability proved in the audit probes). Unconditional. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "58ca7db520d1288f11da9424ce9563563903891ffe6c31c294e7c1e90db6d550" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge10.zeroSide_gaussTest_eq" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge10.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_envelope.toml b/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_envelope.toml index dc3cb5ab2..f77a8c563 100644 --- a/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_envelope.toml +++ b/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_envelope.toml @@ -5,7 +5,14 @@ name = "MM.gaussian_positivity_envelope" statement_module = "Statements.MM_gaussian_positivity_envelope" status = "proved" title = "WALL ASSAULT seam B, envelope form (2026-09-21), UNCONDITIONAL: for every width lam > 0 there is an explicit height envelopeC(lam) beyond which the Gaussian-weighted zero sum is nonnegative at every centre |c| >= envelopeC(lam) -- archimedean dominance at large height (Re digamma grows like log|c|/2 via Zeta23 Stirling) against a lam-uniform prime bound 16 A e^{16 lam}; the constant carries the crude e^{16 lam} and is not sharpened (the sharp c1(lam) ~ 2 pi e^{2P(lam)} is the sweep's P3). Nothing about RH: the Wall proper is the bounded-height complement above lam0. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "a0eab11f5cfd9fa375c51dd374fd31e40eef72ee742d338aab4f5746ad02739e" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge11.gaussian_positivity_envelope" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge11.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_envelope_sharp.toml b/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_envelope_sharp.toml index 09e4a8ce1..6ed82877b 100644 --- a/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_envelope_sharp.toml +++ b/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_envelope_sharp.toml @@ -5,7 +5,14 @@ name = "MM.gaussian_positivity_envelope_sharp" statement_module = "Statements.MM_gaussian_positivity_envelope_sharp" status = "proved" title = "SEAM B SHARPENED (2026-09-21), UNCONDITIONAL: the sharp c-uniform envelope of the two-parameter Wall -- for every width lam > 0 the Gaussian-weighted zero sum is nonnegative at every centre |c| >= envelopeCsharp(lam) = 2 pi e^{primeAbs(lam) + 1/2} + small lam-only terms, where primeAbs(lam) is the EXACT absolute prime-side constant (explicit convergent series; 8.74 at lam = 0.5, 23.7 at lam = 1). Consequence: at the ladder height T = 640000 the band T - D < |c| < envelopeCsharp(lam) is EMPTY for lam <= 0.597, and 2 pi e^{primeAbs} is the floor of ANY c-uniform argument (the exact constant is sharp by Bohr almost-periodicity), so envelopeCsharp(1) = 2.07e11 cannot be improved below 1.26e11 by this method. No overlap with the ladder instrument (needs lam >= 1). Nothing about RH. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "6a315fcb7ffa941de6fba72be9245f9776292fc15352785fed42affa015db97b" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge16.gaussian_positivity_envelope_sharp" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge16.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_of_window.toml b/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_of_window.toml index 551872009..bdda4051e 100644 --- a/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_of_window.toml +++ b/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_of_window.toml @@ -5,7 +5,14 @@ name = "MM.gaussian_positivity_of_window" statement_module = "Statements.MM_gaussian_positivity_of_window" status = "proved" title = "WALL ASSAULT seam C (2026-09-21): the ladder-certified region of the two-parameter Wall as a kernel INSTRUMENT -- if every nontrivial zero within D of the centre c is on the line (WindowOnLine c D, the cross-island hypothesis the Turing ladder supplies for |c| <= T - D by registry-level composition, NOT a Lean import) and one certified zero sits at distance in [delta, d] of c with lam above the explicit threshold lamThreshold(c, D, d, delta), then the Gaussian zero sum at c is nonnegative. REGISTERED STATEMENT = this single-near-zero form; the sharper dominance form gaussian_positivity_of_window_dominance (finite certified window sum >= explicit tail envelope, the form the numerics validate) lives in the same artifact but its vocabulary rests on a finiteness THEOREM (zetaSeam.finite_window) and cannot be mirrored as a definition on the v4.32 statement island. The on-line hypothesis is load-bearing (audit probes). Proves NOTHING about RH; certifies a region of the (c, lam) half-plane from finite data. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "a3d868597e06f55d9744d82c180d9359c5d1c22e00f7045b79a396e6eac2c427" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge12.gaussian_positivity_of_window" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge12.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_small_lam.toml b/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_small_lam.toml index 1adef0b99..7d5fb0a9c 100644 --- a/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_small_lam.toml +++ b/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_small_lam.toml @@ -5,7 +5,14 @@ name = "MM.gaussian_positivity_small_lam" statement_module = "Statements.MM_gaussian_positivity_small_lam" status = "proved" title = "WALL ASSAULT seam B, zero-side form, UNCONDITIONAL: for every centre and every width <= lam0 the Gaussian-weighted zero sum is nonnegative (seam A's Gaussian explicit formula discharges seam B's hypothesis). conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "9ba76cde0a3872ea470704a77b60edd1fed1003bc4b3eb3703f7fa3182df01db" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge13.gaussian_positivity_small_lam" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge13.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_small_lam_3e3.toml b/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_small_lam_3e3.toml index 17d50ddea..edbb50adb 100644 --- a/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_small_lam_3e3.toml +++ b/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_small_lam_3e3.toml @@ -5,7 +5,14 @@ name = "MM.gaussian_positivity_small_lam_3e3" statement_module = "Statements.MM_gaussian_positivity_small_lam_3e3" status = "proved" title = "THE GAUSSIAN PRIME-FREE WINDOW, WIDENED 15000x (rvm_bridge island, E6Bridge30, 2026-09-22): the Wall functional F(c, lam) is nonnegative for EVERY centre c and every 0 < lam <= 3/2000, hypothesis-free (was lam0 = 1e-7 in E6Bridge11). Route: twelve-band layer cake over |r| with rigorous rational digamma floors (series partial sums, integral tail, gamma <= 0.58112 from eulerMascheroniSeq' 128), c-uniform window caps rho e^{-1}/lam from bumpR <= e^{-1}/(2 lam), the exact pole floor -e^{lam/2}/2, E6Bridge11's prime bound; certified margin 0.052 (and 0.168 at lam <= 1/1000). The measured ceiling of any c-uniform prime-side argument for this family is lam = 0.0115 (GAUSS_WINDOW_DESIGN_2026-09-22.md); the literature's 0.03-0.12 window is for compactly supported tests and is NOT reachable this way. A statement about one explicit test function's prime-side functional; involves no zeros; NOT a proof of anything about RH. conjecture1_proved = False." -updated = "2026-09-22" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "0f6f81f28d2862906988353b0043b1393499750ffb85c6105125304503e90f42" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge30.gaussian_positivity_small_lam_3e3" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge30.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_small_lam_prime_side.toml b/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_small_lam_prime_side.toml index 27f52c514..c990e8ad1 100644 --- a/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_small_lam_prime_side.toml +++ b/telperion/missions/mirrormere/nodes/MM_gaussian_positivity_small_lam_prime_side.toml @@ -5,7 +5,14 @@ name = "MM.gaussian_positivity_small_lam_prime_side" statement_module = "Statements.MM_gaussian_positivity_small_lam_prime_side" status = "proved" title = "WALL ASSAULT seam B (2026-09-21), UNCONDITIONAL: the small-width region of the two-parameter Wall -- for EVERY real centre c and every width 0 < lam <= lam0 = 1e-7, the archimedean side of the Gaussian-derivative test exceeds its prime side (archimedean dominance: the prime side is exponentially small in 1/lam, the pole terms decay in c, Re digamma bounded below via Zeta23 Stirling). Yoshida-type positivity (Yoshida 1992 primary UNRESOLVED). Nothing about RH: the Wall proper is lam > lam0. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "a0eab11f5cfd9fa375c51dd374fd31e40eef72ee742d338aab4f5746ad02739e" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge11.re_weilForm_gauss_nonneg" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge11.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_gaussian_transfer.toml b/telperion/missions/mirrormere/nodes/MM_gaussian_transfer.toml index f4af878fc..c53bc9619 100644 --- a/telperion/missions/mirrormere/nodes/MM_gaussian_transfer.toml +++ b/telperion/missions/mirrormere/nodes/MM_gaussian_transfer.toml @@ -5,7 +5,14 @@ name = "MM.gaussian_transfer" statement_module = "Statements.MM_gaussian_transfer" status = "proved" title = "Obligation O1 (GaussianTransfer): the Gaussian-derivative Hermitian transform G_{c,lam} is a limit of Hermitian transforms of smooth compactly supported Weil tests FOR THE ZERO-SIDE FUNCTIONAL, Re zeroSide (hermitianTransform g_n) -> Re zeroSide G_{c,lam}. Discharged by O1' (MM_gaussian_approx) via the PROVED RvMBridge6.gaussianTransfer_of_approx (Tannery's theorem against the local zero count Sum m(rho)/(1+|gamma_rho|^2) < infinity, Zeta23.WeilEF.zero_sum_inv_sq); so this node closes the moment O1' does. Independent of RH; NOT RH-hard. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "83f25395d1251b2e1ba75494effe65d285769c866e88a350a01ffc293a10377c" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge9.gaussian_transfer" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge9.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_rh_iff_gaussian_positivity.toml b/telperion/missions/mirrormere/nodes/MM_rh_iff_gaussian_positivity.toml index fb3d08249..532b60c39 100644 --- a/telperion/missions/mirrormere/nodes/MM_rh_iff_gaussian_positivity.toml +++ b/telperion/missions/mirrormere/nodes/MM_rh_iff_gaussian_positivity.toml @@ -5,7 +5,14 @@ name = "MM.rh_iff_gaussian_positivity" statement_module = "Statements.MM_rh_iff_gaussian_positivity" status = "proved" title = "WALL ASSAULT seam A (2026-09-21): the Wall in two real parameters -- Mathlib's RiemannHypothesis is EQUIVALENT to Gaussian positivity: for every centre c and width lam > 0 the Gaussian-weighted zero sum Re Sum_rho m(rho) (gamma_rho - c)^2 exp(-2 lam (gamma_rho - c)^2) is nonnegative. Forward: on-line zeros + summability; converse: MM_gaussian_dominance. The C_c^infinity quantifier is gone; each off-line zero would carve a negative region of the (c, lam) half-plane. An equivalence; proves NOTHING about either side. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "58ca7db520d1288f11da9424ce9563563903891ffe6c31c294e7c1e90db6d550" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge10.rh_iff_gaussian_positivity" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge10.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_rh_iff_gaussian_prime_le_arch.toml b/telperion/missions/mirrormere/nodes/MM_rh_iff_gaussian_prime_le_arch.toml index 97f37ad13..d79956288 100644 --- a/telperion/missions/mirrormere/nodes/MM_rh_iff_gaussian_prime_le_arch.toml +++ b/telperion/missions/mirrormere/nodes/MM_rh_iff_gaussian_prime_le_arch.toml @@ -5,7 +5,14 @@ name = "MM.rh_iff_gaussian_prime_le_arch" statement_module = "Statements.MM_rh_iff_gaussian_prime_le_arch" status = "proved" title = "WALL ASSAULT seam A: RH as a PRIME-SIDE inequality with no zeros in it -- for every centre c and width lam > 0, the prime side of the Gaussian-derivative test does not exceed its archimedean side. The Wall is the sign of one explicit function on the (c, lam) half-plane. An equivalence; proves NOTHING about either side. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "58ca7db520d1288f11da9424ce9563563903891ffe6c31c294e7c1e90db6d550" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge10.rh_iff_gaussian_prime_le_arch" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge10.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_rh_iff_theta_positivity.toml b/telperion/missions/mirrormere/nodes/MM_rh_iff_theta_positivity.toml index a30d9fc97..6bb7eee2d 100644 --- a/telperion/missions/mirrormere/nodes/MM_rh_iff_theta_positivity.toml +++ b/telperion/missions/mirrormere/nodes/MM_rh_iff_theta_positivity.toml @@ -5,7 +5,14 @@ name = "MM.rh_iff_theta_positivity" statement_module = "Statements.MM_rh_iff_theta_positivity" status = "proved" title = "THE THETA FACE (2026-09-21): Mathlib's RiemannHypothesis is EQUIVALENT to positivity of the PLAIN Gaussian face Theta(c, lam) = Re Sum m(rho) e^{-2 lam (gamma_rho - c)^2} at every centre and width (F = -(1/2) d Theta/d lam is the Wall face). Converse: the Gaussian-dominance argument with the bracket cos(4 lam x y) and a generic centre off the window ordinates. An equivalence; proves NOTHING about either side. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "d7778c3f3df56bbac314b53a0cdc24f02eac6ee1c5abd5bbd0670b09fb780f52" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge17.rh_iff_theta_positivity" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge17.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_rh_iff_theta_widths.toml b/telperion/missions/mirrormere/nodes/MM_rh_iff_theta_widths.toml index a3563c762..d33060dc7 100644 --- a/telperion/missions/mirrormere/nodes/MM_rh_iff_theta_widths.toml +++ b/telperion/missions/mirrormere/nodes/MM_rh_iff_theta_widths.toml @@ -5,7 +5,14 @@ name = "MM.rh_iff_theta_widths" statement_module = "Statements.MM_rh_iff_theta_widths" status = "proved" title = "LAMBDA_THETA (2026-09-21): RH is EQUIVALENT to every positive width being Theta-free, i.e. to the de Bruijn-Newman-type constant of the zero measure being infinite; an off-line zero bounds the free widths (not_thetaFree_of_offline, rh_or_thetaWidths_bddAbove). A certified width lam_cert (ladder + envelope) gives Lambda_Theta >= lam_cert and every smaller width -- a wall, not a crossing. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "d7778c3f3df56bbac314b53a0cdc24f02eac6ee1c5abd5bbd0670b09fb780f52" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge17.rh_iff_thetaWidths_eq" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge17.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_rh_implies_weil_positivity.toml b/telperion/missions/mirrormere/nodes/MM_rh_implies_weil_positivity.toml index 6891ea0d0..21416d67f 100644 --- a/telperion/missions/mirrormere/nodes/MM_rh_implies_weil_positivity.toml +++ b/telperion/missions/mirrormere/nodes/MM_rh_implies_weil_positivity.toml @@ -5,7 +5,14 @@ name = "MM.rh_implies_weil_positivity" statement_module = "Statements.MM_rh_implies_weil_positivity" status = "proved" title = "Weil's criterion, forward half, on the E8 vocabulary: Mathlib's RiemannHypothesis implies Weil positivity of weilForm on Hermitian autocorrelations over IsWeilTest -- discharges the hypothesis hpos that weil_negative_refutes_rh (weil_form_enclosure island) has carried undischarged; proves NOTHING about RH itself. conjecture1_proved = False." -updated = "2026-09-20" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "56ce428b2c875125128bdd8c9d86b737f2a320ff4e7a57c9121781f50e30dd50" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge5.rh_implies_weil_positivity" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge5.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_rvm_unbounded_mean_density.toml b/telperion/missions/mirrormere/nodes/MM_rvm_unbounded_mean_density.toml index 526cf0a09..250e445c5 100644 --- a/telperion/missions/mirrormere/nodes/MM_rvm_unbounded_mean_density.toml +++ b/telperion/missions/mirrormere/nodes/MM_rvm_unbounded_mean_density.toml @@ -5,7 +5,14 @@ name = "MM.rvm_unbounded_mean_density" statement_module = "Statements.MM_rvm_unbounded_mean_density" status = "proved" title = "The W2c residual, named: RvMUnboundedMeanDensity -- the zeta-ordinate mean density exceeds every finite bound (Riemann-von Mangoldt growth input). 2026-09-15 SURVEY VERDICT (W2c agent, d859b064): NO unconditional kernel proof exists in corpus or Mathlib -- Mathlib has only discreteness, the li-island RvM machinery is per-window/conditional, and linear zero-count bounds provably do NOT suffice (they give constant gaps, not gaps -> 0). Discharge = a FUTURE BRICK from the RvM box-counting engine + zero-free edges, not a cross-island grant" -updated = "2026-09-17" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "537b9d4c5ce5512d5bf20d4af47cc3251749b3b96c162b54dd497ecda8243d82" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge.rvm_unbounded_mean_density" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_theta_heat_monotone.toml b/telperion/missions/mirrormere/nodes/MM_theta_heat_monotone.toml index 9d9d2fe78..ee8e8fd1a 100644 --- a/telperion/missions/mirrormere/nodes/MM_theta_heat_monotone.toml +++ b/telperion/missions/mirrormere/nodes/MM_theta_heat_monotone.toml @@ -5,7 +5,14 @@ name = "MM.theta_heat_monotone" statement_module = "Statements.MM_theta_heat_monotone" status = "proved" title = "THE HEAT INSTRUMENT (2026-09-21), UNCONDITIONAL: the plain Gaussian face is heat-monotone in width -- Theta(., lam') = sqrt(lam/lam') P_s Theta(., lam) for lam' < lam (theta_heat, valid for off-line zeros by the termwise complex-centre Gaussian identity), so positivity on the WHOLE LINE at one width implies it at every smaller width. The free widths form an initial segment; one certified width closes all smaller. The Wall face F has no such monotonicity (negative source term), which is why the F-Wall is a diagonal. Asserts nothing detectable about zeros by itself. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "d7778c3f3df56bbac314b53a0cdc24f02eac6ee1c5abd5bbd0670b09fb780f52" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge17.theta_pos_mono" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge17.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_wall_map.toml b/telperion/missions/mirrormere/nodes/MM_wall_map.toml index 09b09cf2d..2659b348f 100644 --- a/telperion/missions/mirrormere/nodes/MM_wall_map.toml +++ b/telperion/missions/mirrormere/nodes/MM_wall_map.toml @@ -5,7 +5,14 @@ name = "MM.wall_map" statement_module = "Statements.MM_wall_map" status = "proved" title = "THE WALL MAP (2026-09-21): Mathlib's RiemannHypothesis is EQUIVALENT to Gaussian positivity on widths strictly above lam0 = 1e-7 only; below lam0 positivity is a theorem (MM_gaussian_positivity_small_lam). With MM_gaussian_positivity_of_window certifying |c| <= T - D from ladder data, the residual region {|c| > T - D, lam > lam0} IS the Wall. An equivalence; proves NOTHING about either side. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "9ba76cde0a3872ea470704a77b60edd1fed1003bc4b3eb3703f7fa3182df01db" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge13.rh_iff_gaussian_positivity_above_lam₀" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge13.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_weil_positivity_implies_rh.toml b/telperion/missions/mirrormere/nodes/MM_weil_positivity_implies_rh.toml index 27e91d3b2..54487c2c8 100644 --- a/telperion/missions/mirrormere/nodes/MM_weil_positivity_implies_rh.toml +++ b/telperion/missions/mirrormere/nodes/MM_weil_positivity_implies_rh.toml @@ -5,7 +5,14 @@ name = "MM.weil_positivity_implies_rh" statement_module = "Statements.MM_weil_positivity_implies_rh" status = "proved" title = "Weil's criterion, converse half (Weil 1952; Bombieri 2000 on C_c^infinity): Weil positivity on Hermitian autocorrelations over IsWeilTest implies Mathlib's RiemannHypothesis -- classical analysis, NOT RH-hard, never before formalized here; an off-line zero must be turned into a test function with strictly negative pairing. conjecture1_proved = False. REDUCED 2026-09-20 to the two Gaussian obligations (see MM_weil_positivity_implies_rh_of_gaussian)." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "83f25395d1251b2e1ba75494effe65d285769c866e88a350a01ffc293a10377c" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge9.weil_positivity_implies_rh" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge9.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_weil_positivity_implies_rh_of_gaussian.toml b/telperion/missions/mirrormere/nodes/MM_weil_positivity_implies_rh_of_gaussian.toml index 9206ca180..c1d58944f 100644 --- a/telperion/missions/mirrormere/nodes/MM_weil_positivity_implies_rh_of_gaussian.toml +++ b/telperion/missions/mirrormere/nodes/MM_weil_positivity_implies_rh_of_gaussian.toml @@ -5,7 +5,14 @@ name = "MM.weil_positivity_implies_rh_of_gaussian" statement_module = "Statements.MM_weil_positivity_implies_rh_of_gaussian" status = "proved" title = "The Weil converse, REDUCED: Weil positivity implies Mathlib's RiemannHypothesis GIVEN the two named analytic obligations GaussianTransfer (transfer of the zero-side functional from the IsWeilTest class to the Gaussian-derivative test) and GaussianDominance (an off-line zero makes some Gaussian-weighted zero sum strictly negative). Kernel-checked reduction; proves nothing about RH; the obligations are their own nodes. conjecture1_proved = False." -updated = "2026-09-20" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "1b95410ca70ab08f1e2b73ebaea43f97c3becf19b3549f1e496d106e58735294" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge6.weil_positivity_implies_rh_of" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge6.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_zeta_comb_membership_iff_rh.toml b/telperion/missions/mirrormere/nodes/MM_zeta_comb_membership_iff_rh.toml index 3413d382f..49b0d8ef4 100644 --- a/telperion/missions/mirrormere/nodes/MM_zeta_comb_membership_iff_rh.toml +++ b/telperion/missions/mirrormere/nodes/MM_zeta_comb_membership_iff_rh.toml @@ -5,7 +5,14 @@ name = "MM.zeta_comb_membership_iff_rh" statement_module = "Statements.MM_zeta_comb_membership_iff_rh" status = "proved" title = "The dictionary theorem: the MIRRORMERE goal statement is EQUIVALENT to Mathlib's RiemannHypothesis, in-kernel -- replaces the 2026-09-14 placeholder's by-fiat identification (CharacterizationStatements.zeta_FQ_iff_RH is a def : Prop over opaque variables, never a theorem) with a proved equivalence; the goal node stays draft and RH-hard, now for a proved reason. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "83f25395d1251b2e1ba75494effe65d285769c866e88a350a01ffc293a10377c" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge9.zeta_comb_membership_iff_rh" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge9.lean" diff --git a/telperion/missions/mirrormere/nodes/MM_zeta_ordinates_not_uniformly_discrete.toml b/telperion/missions/mirrormere/nodes/MM_zeta_ordinates_not_uniformly_discrete.toml index e1b130ebd..773f1d8f8 100644 --- a/telperion/missions/mirrormere/nodes/MM_zeta_ordinates_not_uniformly_discrete.toml +++ b/telperion/missions/mirrormere/nodes/MM_zeta_ordinates_not_uniformly_discrete.toml @@ -5,7 +5,14 @@ name = "MM.zeta_ordinates_not_uniformly_discrete" statement_module = "Statements.MM_zeta_ordinates_not_uniformly_discrete" status = "proved" title = "W2c target, unconditional form: the zeta ordinates are not uniformly discrete, no hypotheses -- lands when the RvM residual is discharged into the conditional brick" -updated = "2026-09-18" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "f33ad4e7bdcaeec579597ca18a20cda3d530ee24e1619218416753271f9fa86d" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge.zeta_ordinates_not_uniformly_discrete" [proof] artifact = "../../examples/rvm_bridge/lean/W2cAssembly.lean" diff --git a/telperion/missions/rh/nodes/RH_bl_closed_form_five_nonneg.toml b/telperion/missions/rh/nodes/RH_bl_closed_form_five_nonneg.toml index 51ecad296..40dc38542 100644 --- a/telperion/missions/rh/nodes/RH_bl_closed_form_five_nonneg.toml +++ b/telperion/missions/rh/nodes/RH_bl_closed_form_five_nonneg.toml @@ -5,7 +5,14 @@ name = "RH.bl_closed_form_five_nonneg" statement_module = "Statements.RH_bl_closed_form_five_nonneg" status = "proved" title = "BOMBIERI-LAGARIAS CLOSED FORM, RUNG 5, NO HYPOTHESIS (rvm_bridge island, E6Bridge28, 2026-09-21): 0 <= Re(archSide 5 + finiteSide 5), i.e. the explicit expression in gamma, log pi, log 2, zeta(2..5) and the Laurent constants eta_0..eta_4 is nonnegative, unconditionally in the kernel (via liValue and the box-region positivity of the pair terms for N <= 5; rungs 1..4 likewise in the module). Not RH. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "914cd3bb64c69e6849cc76a704cfc2fa6abd99bc26cda441b484f1b47633e59d" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge28.archSide_add_finiteSide_five_re_nonneg" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge28.lean" diff --git a/telperion/missions/rh/nodes/RH_bl_explicit_formula.toml b/telperion/missions/rh/nodes/RH_bl_explicit_formula.toml index 69bb46601..0535e223b 100644 --- a/telperion/missions/rh/nodes/RH_bl_explicit_formula.toml +++ b/telperion/missions/rh/nodes/RH_bl_explicit_formula.toml @@ -5,7 +5,14 @@ name = "RH.bl_explicit_formula" statement_module = "Statements.RH_bl_explicit_formula" status = "proved" title = "The BOMBIERI-LAGARIAS EXPLICIT FORMULA on Li's test class (routes-roadmap B7-ii, the B6 -> B7 test-class extension of E8): for every n >= 1 the SYMMETRIC window sums sum_{|Im rho| <= T} m(rho) (1 - (1 - 1/rho)^n) over the nontrivial zeros (RvMCount / E8 multiplicity) converge as T -> infinity to S_inf(n) + S_f(n), S_inf(n) = 1 - (n/2)(gamma + log pi + 2 log 2) + sum_{j=2}^n (-1)^j C(n,j)(1 - 2^{-j}) zeta(j) the archimedean closed form and S_f(n) = -sum_{j=1}^n C(n,j) eta_{j-1} the finite part, eta_j the Taylor coefficients at s = 1 of -zeta'/zeta(s) - 1/(s-1) (BL 1999 Thm 2, Li 1997); the limit is Li's lambda_n. Li's kernel decays like 1/|r| on the line, is in neither the E8 nor the Guinand class, the family is NOT summable (HasSum false, one-sided windows diverge), and the naive prime sum diverges: the arithmetic side is the residue form, not a prime comb. PROVED hypothesis-free 2026-09-21 (E6Bridge27, blind audit AUDIT_TESTIMONY_B7_UNCONDITIONAL_2026-09-21.md); conjecture1_proved = False REDUCED 2026-09-21 to LiValue (see RH_bl_explicit_formula_of_livalue) REDUCED 2026-09-21 to LocalCountSum + StripDerivBound + NoRealZeroInUnitInterval REDUCED 2026-09-21 to StripDerivBound ALONE" -updated = "2026-09-22" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "dab21c2217d3da02a478d2e708ab2b50289d5668a324987f0966d6e1055382dc" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge27.bl_explicit_formula" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge27.lean" diff --git a/telperion/missions/rh/nodes/RH_bl_explicit_formula_of_livalue.toml b/telperion/missions/rh/nodes/RH_bl_explicit_formula_of_livalue.toml index 15441315b..0b6405a36 100644 --- a/telperion/missions/rh/nodes/RH_bl_explicit_formula_of_livalue.toml +++ b/telperion/missions/rh/nodes/RH_bl_explicit_formula_of_livalue.toml @@ -5,7 +5,14 @@ name = "RH.bl_explicit_formula_of_livalue" statement_module = "Statements.RH_bl_explicit_formula_of_livalue" status = "proved" title = "B7 REDUCED (2026-09-21): the node RH_bl_explicit_formula holds verbatim GIVEN the named value obligation LiValue n : liLimit n = archSide n + finiteSide n (Bombieri-Lagarias Thm 2; needs the derivative partial fraction of xi'/xi, in flight as E6Bridge18/19). LiValue is FALSE at n = 0, so the node's 0 < n is load-bearing. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "e33d2e2f42aa30e4ce84cca72fae9b30673568e675f471db686c8b4cd420ac03" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge15.bl_explicit_formula_of" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge15.lean" diff --git a/telperion/missions/rh/nodes/RH_bl_explicit_formula_of_partial_fraction.toml b/telperion/missions/rh/nodes/RH_bl_explicit_formula_of_partial_fraction.toml index 8a3de910a..3a53a4f11 100644 --- a/telperion/missions/rh/nodes/RH_bl_explicit_formula_of_partial_fraction.toml +++ b/telperion/missions/rh/nodes/RH_bl_explicit_formula_of_partial_fraction.toml @@ -5,7 +5,14 @@ name = "RH.bl_explicit_formula_of_partial_fraction" statement_module = "Statements.RH_bl_explicit_formula_of_partial_fraction" status = "proved" title = "B7 (RH_bl_explicit_formula) holds GIVEN the derivative partial fraction of xi and no real zero in (0,1); with E6Bridge22 the partial fraction rests on LocalCountSum + StripDerivBound, so B7 = three named classical facts, all in flight (E6Bridge23/24/25). conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "ad5f083f36efced07f8b3b6a4301f73c13cc5a4b2fac98da6ab7691cf5b85f99" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge19.bl_explicit_formula_of_partialFraction" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge19.lean" diff --git a/telperion/missions/rh/nodes/RH_bl_explicit_formula_of_strip.toml b/telperion/missions/rh/nodes/RH_bl_explicit_formula_of_strip.toml index f7a454b4b..7071cbb7b 100644 --- a/telperion/missions/rh/nodes/RH_bl_explicit_formula_of_strip.toml +++ b/telperion/missions/rh/nodes/RH_bl_explicit_formula_of_strip.toml @@ -5,7 +5,14 @@ name = "RH.bl_explicit_formula_of_strip" statement_module = "Statements.RH_bl_explicit_formula_of_strip" status = "proved" title = "B7 (RH_bl_explicit_formula) MODULO STRIPDERIVBOUND ALONE (2026-09-21): the Bombieri-Lagarias explicit formula on Li's class holds given one remaining classical inequality (Landau's local partial fraction transferred to the derivative on the strip, E6Bridge24 in flight). conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "f5c883401a82561922194a5ca55c4a392b0ac483f10589a5277cdecb946a086b" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge26.bl_explicit_formula_of_strip" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge26.lean" diff --git a/telperion/missions/rh/nodes/RH_corridor_bound.toml b/telperion/missions/rh/nodes/RH_corridor_bound.toml index 80a6716c4..5aa04cc76 100644 --- a/telperion/missions/rh/nodes/RH_corridor_bound.toml +++ b/telperion/missions/rh/nodes/RH_corridor_bound.toml @@ -5,7 +5,14 @@ name = "RH.corridor_bound" statement_module = "Statements.RH_corridor_bound" status = "proved" title = "The CORRIDOR BOUND (routes-roadmap E7 = A3 = B5 = D6, the unique four-consumer blocker): for every T >= 2 some height T' in [T, T+1] has a zero-free horizontal segment -1 <= sigma <= 2 on which |zeta'/zeta(sigma + iT')| <= C log^2 T; O-form constant, effective form queued" -updated = "2026-09-18" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "b420c40ad672cf684a847b137462bb602663812f3cb3d6a514f46f3ee7d2cb7f" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge3.corridor_bound" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge3.lean" diff --git a/telperion/missions/rh/nodes/RH_dbn_H0_eq_xi.toml b/telperion/missions/rh/nodes/RH_dbn_H0_eq_xi.toml index fdac6f512..d0293f9bb 100644 --- a/telperion/missions/rh/nodes/RH_dbn_H0_eq_xi.toml +++ b/telperion/missions/rh/nodes/RH_dbn_H0_eq_xi.toml @@ -5,7 +5,14 @@ name = "RH.dbn_H0_eq_xi" statement_module = "Statements.RH_dbn_H0_eq_xi" status = "proved" title = "Route C / C2 representation theorem: H_0(z) = (1/8) xi(1/2 + iz/2) for every complex z -- the heat-flow family at t = 0 is the Riemann xi function (Polymath15 eq. (3), Titchmarsh 10.1). PROVED on the dbn island (DBNXi, modules A-E), an identity between entire functions, not RH-equivalent" -updated = "2026-09-22" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "482bd3d1f3c231d22170fc338a9035fea11765b2f33183384808e6badaf07cd2" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "dbn_H0_eq_xi" [proof] artifact = "../../examples/dbn/lean/DBNXi.lean" diff --git a/telperion/missions/rh/nodes/RH_dbn_H0_zero_strip.toml b/telperion/missions/rh/nodes/RH_dbn_H0_zero_strip.toml index 334546ef5..25842cefc 100644 --- a/telperion/missions/rh/nodes/RH_dbn_H0_zero_strip.toml +++ b/telperion/missions/rh/nodes/RH_dbn_H0_zero_strip.toml @@ -5,7 +5,14 @@ name = "RH.dbn_H0_zero_strip" statement_module = "Statements.RH_dbn_H0_zero_strip" status = "proved" title = "Route C, the C2-free zero strip: every zero of H_0 lies in the strip |Im z| <= 1. PROVED on the dbn island (DBNStrip) from the absolutely convergent half-plane via the Euler product and reflection; no theta FE, no Hadamard; says nothing about zeros inside the strip" -updated = "2026-09-22" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "45d46b39f5db3fc38339e03301215509d059e78c6d1f5a7e9c1fc8da1e77098e" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "dbn_H0_zero_strip" [proof] artifact = "../../examples/dbn/lean/DBNStrip.lean" diff --git a/telperion/missions/rh/nodes/RH_dbn_rh_iff_H0_real_zeros.toml b/telperion/missions/rh/nodes/RH_dbn_rh_iff_H0_real_zeros.toml index 69e2c6957..a16a4ae1d 100644 --- a/telperion/missions/rh/nodes/RH_dbn_rh_iff_H0_real_zeros.toml +++ b/telperion/missions/rh/nodes/RH_dbn_rh_iff_H0_real_zeros.toml @@ -5,7 +5,14 @@ name = "RH.dbn_rh_iff_H0_real_zeros" statement_module = "Statements.RH_dbn_rh_iff_H0_real_zeros" status = "proved" title = "Route C / C4: RH (AND_ladder grammar: every nontrivial zero in the open strip has real part 1/2) iff every zero of H_0 is real. PROVED unconditionally as an EQUIVALENCE (DBNRealZerosIffFinal, via C2); proves neither side" -updated = "2026-09-22" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "cc4483fde12753f20b2c121ea4f3a9272fdd36b2b5a2f75cf2b2ca71a1b52498" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "dbn_rh_iff_H0_real_zeros" [proof] artifact = "../../examples/dbn/lean/DBNRealZerosIffFinal.lean" diff --git a/telperion/missions/rh/nodes/RH_li_forward_half.toml b/telperion/missions/rh/nodes/RH_li_forward_half.toml index 9f37d78e5..72d68769b 100644 --- a/telperion/missions/rh/nodes/RH_li_forward_half.toml +++ b/telperion/missions/rh/nodes/RH_li_forward_half.toml @@ -5,7 +5,14 @@ name = "RH.li_forward_half" statement_module = "Statements.RH_li_forward_half" status = "proved" title = "LI'S CRITERION, FORWARD HALF, on the rvm_bridge island (2026-09-21): under Mathlib's RiemannHypothesis every paired Li coefficient is nonnegative (on the line |1 - 1/rho| = 1). The converse lives on the v4.34 li_positivity island (li_criterion_rh_iff) and is not re-proved here. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "e33d2e2f42aa30e4ce84cca72fae9b30673568e675f471db686c8b4cd420ac03" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge15.rh_implies_liLimit_re_nonneg" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge15.lean" diff --git a/telperion/missions/rh/nodes/RH_li_ladder_liLimit.toml b/telperion/missions/rh/nodes/RH_li_ladder_liLimit.toml index f6e4828f2..6e4816d01 100644 --- a/telperion/missions/rh/nodes/RH_li_ladder_liLimit.toml +++ b/telperion/missions/rh/nodes/RH_li_ladder_liLimit.toml @@ -5,7 +5,14 @@ name = "RH.li_ladder_liLimit" statement_module = "Statements.RH_li_ladder_liLimit" status = "proved" title = "THE LI LADDER IN THE B7 VOCABULARY (rvm_bridge island, E6Bridge28, 2026-09-21): if every nontrivial zero with |Im| <= T (T >= 1) is on the line then 0 <= Re(liLimit N) for N <= 3 pi T / 2 (regrouping over reflect rho -> 1 - conj rho, termwise nonnegativity for |Im| >= 2N/(3 pi)). Through RvMBridge27.liValue the same gives 0 <= Re(archSide N + finiteSide N). Consumes zero localisation, produces none. Not RH. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "914cd3bb64c69e6849cc76a704cfc2fa6abd99bc26cda441b484f1b47633e59d" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge28.liLimit_re_nonneg_of_line_below" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge28.lean" diff --git a/telperion/missions/rh/nodes/RH_li_ladder_liLimit_sharp.toml b/telperion/missions/rh/nodes/RH_li_ladder_liLimit_sharp.toml index be19ff5da..f156369e7 100644 --- a/telperion/missions/rh/nodes/RH_li_ladder_liLimit_sharp.toml +++ b/telperion/missions/rh/nodes/RH_li_ladder_liLimit_sharp.toml @@ -5,7 +5,14 @@ name = "RH.li_ladder_liLimit_sharp" statement_module = "Statements.RH_li_ladder_liLimit_sharp" status = "proved" title = "THE LI LADDER, SHARPENED (rvm_bridge island, E6Bridge29, 2026-09-22): zeros on the line up to T >= 1 give 0 <= Re(liLimit N) for N <= 2 pi (T - 1/2). Window lemma: for 3 pi/2 < |b| <= 2 pi with |a| <= 2 pi - |b|, cosh a cos b <= 1 (cos b = cos(2 pi - |b|)); |theta| + |log r| <= 1/(|Im| - 1/2). Numerically the true termwise threshold is N/(2 pi) + 1/2 + o(1), so this rate is sharp for the termwise method. Consumes localisation, produces none. Not RH. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "385db99e45ff23d97f1b0189f32000ec0f482d7fd5049ce11a41a381ff88d05e" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge29.liLimit_re_nonneg_of_line_below_sharp" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge29.lean" diff --git a/telperion/missions/rh/nodes/RH_li_zero_sums_converge.toml b/telperion/missions/rh/nodes/RH_li_zero_sums_converge.toml index 1d8822990..d76d26b1a 100644 --- a/telperion/missions/rh/nodes/RH_li_zero_sums_converge.toml +++ b/telperion/missions/rh/nodes/RH_li_zero_sums_converge.toml @@ -5,7 +5,14 @@ name = "RH.li_zero_sums_converge" statement_module = "Statements.RH_li_zero_sums_converge" status = "proved" title = "B7 CONVERGENCE HALF (2026-09-21, open lemma 2): for every n the SYMMETRIC window sums of Li's kernel over the nontrivial zeros converge as T -> infinity, to the absolutely convergent paired sum liLimit n = Sum m(rho) Re(1 - (1 - 1/rho)^n); the pairing rho <-> conj rho is necessary (the unpaired family is not summable) and sufficient (|Re K_n| <= 2^n/|rho|^2 + the local-count majorant). Unconditional. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "e33d2e2f42aa30e4ce84cca72fae9b30673568e675f471db686c8b4cd420ac03" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge15.liZeroSum_tendsto" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge15.lean" diff --git a/telperion/missions/rh/nodes/RH_limit_explicit_formula.toml b/telperion/missions/rh/nodes/RH_limit_explicit_formula.toml index 59cfa3efd..f953a006e 100644 --- a/telperion/missions/rh/nodes/RH_limit_explicit_formula.toml +++ b/telperion/missions/rh/nodes/RH_limit_explicit_formula.toml @@ -5,7 +5,14 @@ name = "RH.limit_explicit_formula" statement_module = "Statements.RH_limit_explicit_formula" status = "proved" title = "The LIMIT EXPLICIT FORMULA (routes-roadmap E8 = B6 = D6, the T -> infinity Guinand-Weil identity in diffraction form): for every smooth compactly supported g : R -> C, Sum_rho m(rho) H_g(rho) = h(i/2) + h(-i/2) - g(0) log pi + (1/2pi) int h(r) Re psi(1/4+ir/2) dr - Sum_n Lambda(n)/sqrt n (g(log n)+g(-log n)), zero side over ALL nontrivial zeros with the RvMCount multiplicity, stated as HasSum (summability is part of the claim); the limit of rect_explicit_formula, consumes the corridor bound and RvM; Weil 1952 / Iwaniec-Kowalski 5.12 normalisation, no evenness hypothesis" -updated = "2026-09-18" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "24bb0f8fc324305accd30ba6dd011f11429cef287a871199586ad677a80e7f9a" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge4.limit_explicit_formula" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge4.lean" diff --git a/telperion/missions/rh/nodes/RH_livalue.toml b/telperion/missions/rh/nodes/RH_livalue.toml index 4f253704d..9b2d31804 100644 --- a/telperion/missions/rh/nodes/RH_livalue.toml +++ b/telperion/missions/rh/nodes/RH_livalue.toml @@ -5,7 +5,14 @@ name = "RH.livalue" statement_module = "Statements.RH_livalue" status = "proved" title = "THE BOMBIERI-LAGARIAS VALUE IDENTITY, UNCONDITIONAL (2026-09-21): liLimit n = archSide n + finiteSide n for every n >= 1. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "dab21c2217d3da02a478d2e708ab2b50289d5668a324987f0966d6e1055382dc" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge27.liValue" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge27.lean" diff --git a/telperion/missions/rh/nodes/RH_livalue_of_partial_fraction.toml b/telperion/missions/rh/nodes/RH_livalue_of_partial_fraction.toml index 4be3042d7..21ed6b251 100644 --- a/telperion/missions/rh/nodes/RH_livalue_of_partial_fraction.toml +++ b/telperion/missions/rh/nodes/RH_livalue_of_partial_fraction.toml @@ -5,7 +5,14 @@ name = "RH.livalue_of_partial_fraction" statement_module = "Statements.RH_livalue_of_partial_fraction" status = "proved" title = "THE BOMBIERI-LAGARIAS VALUE IDENTITY, Taylor bookkeeping PROVED (2026-09-21): LiValue n (liLimit n = archSide n + finiteSide n) for every n >= 1, GIVEN the derivative partial fraction of xi and no real zero of zeta in (0,1). Power sums j >= 2 from the Taylor data of (log xi)'' at 0; the paired first power sum from the FTC on [0,1] and the functional equation; the closed forms through eta_j and the polygamma values at 1/2 (the (1 - 2^{-j}) zeta(j) terms). Numerically checked to 1e-27 against Li's generating function. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "ad5f083f36efced07f8b3b6a4301f73c13cc5a4b2fac98da6ab7691cf5b85f99" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge19.liValue_of" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge19.lean" diff --git a/telperion/missions/rh/nodes/RH_local_count_sum.toml b/telperion/missions/rh/nodes/RH_local_count_sum.toml index 3cc54690e..0d7f1537f 100644 --- a/telperion/missions/rh/nodes/RH_local_count_sum.toml +++ b/telperion/missions/rh/nodes/RH_local_count_sum.toml @@ -5,7 +5,14 @@ name = "RH.local_count_sum" statement_module = "Statements.RH_local_count_sum" status = "proved" title = "LOCAL COUNT SUM DISCHARGED (2026-09-21): Sum m(rho)/(1 + (Im rho - a)^2) <= C(1 + log(2 + |a|)) for every real a -- finite partial sums regrouped on integer ceilings, each fiber bounded by Zeta23's per-unit-window zero count, two absolute constants from the integer p-series. Unconditional; nothing about RH. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "aa492e5e013618bcafd0695a1db03ba728ba50f7e35cd6e114104c4033ff0c07" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge23.local_count_sum" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge23.lean" diff --git a/telperion/missions/rh/nodes/RH_no_real_zero_unit_interval.toml b/telperion/missions/rh/nodes/RH_no_real_zero_unit_interval.toml index f880315f2..56e782b7b 100644 --- a/telperion/missions/rh/nodes/RH_no_real_zero_unit_interval.toml +++ b/telperion/missions/rh/nodes/RH_no_real_zero_unit_interval.toml @@ -5,7 +5,14 @@ name = "RH.no_real_zero_unit_interval" statement_module = "Statements.RH_no_real_zero_unit_interval" status = "proved" title = "NO REAL ZERO IN (0,1) DISCHARGED (2026-09-21): Re zeta(sigma) < 0 for 0 < sigma < 1, from the summation-by-parts representation zeta(s) = 1/2 + 1/(s-1) + s J(s) with the sharp bound |J(sigma)| <= 1/(2 sigma) (the eta-series continuation, absent from this pin, is avoided). Unconditional; nothing about RH. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "87f364039398bb3de29908dedaa9aea9cdcd4f984be09c7668122412b40b845d" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge25.noRealZeroInUnitInterval" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge25.lean" diff --git a/telperion/missions/rh/nodes/RH_rvm_unconditional.toml b/telperion/missions/rh/nodes/RH_rvm_unconditional.toml index 08d61b8a9..9cc424df7 100644 --- a/telperion/missions/rh/nodes/RH_rvm_unconditional.toml +++ b/telperion/missions/rh/nodes/RH_rvm_unconditional.toml @@ -5,7 +5,14 @@ name = "RH.rvm_unconditional" statement_module = "Statements.RH_rvm_unconditional" status = "proved" title = "Riemann-von Mangoldt UNCONDITIONAL (routes-roadmap A4/D5, the E6 target): |N(T) - (T/2pi log(T/2pi) - T/2pi + 7/8)| <= C log T for all T >= 2, N(T) the multiplicity RECTANGLE count -- no edge/ball/winding hypotheses (contrast nt_count_effective_bound); implies MM_rvm_unbounded_mean_density" -updated = "2026-09-18" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "952368f82f3a5d67cceec97ba6b705c1b0024ca99b7eec42f4f19539d7717dbe" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge2.rvm_unconditional" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge2.lean" diff --git a/telperion/missions/rh/nodes/RH_strip_deriv_bound.toml b/telperion/missions/rh/nodes/RH_strip_deriv_bound.toml index ed93b8d63..b72e3aceb 100644 --- a/telperion/missions/rh/nodes/RH_strip_deriv_bound.toml +++ b/telperion/missions/rh/nodes/RH_strip_deriv_bound.toml @@ -5,7 +5,14 @@ name = "RH.strip_deriv_bound" statement_module = "Statements.RH_strip_deriv_bound" status = "proved" title = "STRIP DERIVATIVE BOUND DISCHARGED (2026-09-21): Landau's local partial fraction transferred to the derivative of xi'/xi on 1/4 <= Re s <= 9/4, |Im s| >= 5 -- divide out the window zeros, Cauchy on a zero-free circle of radius in (1/4, 1/2), the symmetric difference of Landau's ball and the window bounded by the local zero count, Stirling for the digamma, the functional equation for the left half, the compact bound for |Im s| <= 7. Unconditional; nothing about RH. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "c4c6fc5c1d844c27e81e7737c5e762de8e990abe276e10cba94ec18093ba6611" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge24.stripDerivBound" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge24.lean" diff --git a/telperion/missions/rh/nodes/RH_weil_criterion_iff.toml b/telperion/missions/rh/nodes/RH_weil_criterion_iff.toml index e90f3ff1e..730e2fbdf 100644 --- a/telperion/missions/rh/nodes/RH_weil_criterion_iff.toml +++ b/telperion/missions/rh/nodes/RH_weil_criterion_iff.toml @@ -5,7 +5,14 @@ name = "RH.weil_criterion_iff" statement_module = "Statements.RH_weil_criterion_iff" status = "proved" title = "WEIL'S CRITERION, in-kernel (routes-roadmap section 1, the Positivity face pinned by theorem, 2026-09-21): Weil positivity of the E8 primes-side functional on Hermitian autocorrelations over IsWeilTest is EQUIVALENT to Mathlib's RiemannHypothesis -- cross-campaign consumption of MIRRORMERE's zeta_comb_membership_iff_rh (E6Bridge5-9, four blind audits). An equivalence; proves NOTHING about whether either side holds. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "83f25395d1251b2e1ba75494effe65d285769c866e88a350a01ffc293a10377c" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge9.zeta_comb_membership_iff_rh" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge9.lean" diff --git a/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction.toml b/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction.toml index 1a942d9a6..0fb117ff0 100644 --- a/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction.toml +++ b/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction.toml @@ -5,7 +5,14 @@ name = "RH.xi_derivative_partial_fraction" statement_module = "Statements.RH_xi_derivative_partial_fraction" status = "proved" title = "THE XI PARTIAL FRACTION, DERIVATIVE FORM, UNCONDITIONAL (2026-09-21): (log xi)''(s) = -Sum m(rho)/(s - rho)^2 for every s that is not a nontrivial zero, proved WITHOUT the Hadamard product (entire difference of logarithmic growth is constant, and vanishes on the real axis). An identity valid whether or not RH holds. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "dab21c2217d3da02a478d2e708ab2b50289d5668a324987f0966d6e1055382dc" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge27.xi_logDeriv_deriv_eq" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge27.lean" diff --git a/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction_of.toml b/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction_of.toml index 94830cea6..46cb25613 100644 --- a/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction_of.toml +++ b/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction_of.toml @@ -5,7 +5,14 @@ name = "RH.xi_derivative_partial_fraction_of" statement_module = "Statements.RH_xi_derivative_partial_fraction_of" status = "proved" title = "THE XI PARTIAL FRACTION, DERIVATIVE FORM, WITHOUT HADAMARD (2026-09-21): (log xi)''(s) = -Sum m(rho)/(s - rho)^2 for every s that is not a nontrivial zero, PROVED modulo two named analytic obligations -- XiDiffRegular (the difference extends to an entire function of logarithmic growth) and XiLogDerivDerivDecay (real-axis decay). Proved outright: summability, the log-growth Liouville lemma, the sum's decay, the assembly. Consumer: LiValue (the Bombieri-Lagarias value identity). Nothing about RH. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "ac33ecf766daded30992b4d1d808ceede0057c2325cd64353f35a7bdbfebdff1" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge18.xi_logDeriv_deriv_eq_of" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge18.lean" diff --git a/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction_of_regular.toml b/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction_of_regular.toml index 75b562a0a..7e59b9c91 100644 --- a/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction_of_regular.toml +++ b/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction_of_regular.toml @@ -5,7 +5,14 @@ name = "RH.xi_derivative_partial_fraction_of_regular" statement_module = "Statements.RH_xi_derivative_partial_fraction_of_regular" status = "proved" title = "THE XI PARTIAL FRACTION now rests on ONE obligation (2026-09-21): (log xi)'' = -Sum m(rho)/(s-rho)^2 GIVEN XiDiffRegular (equivalently, via E6Bridge20, the log-growth bound on Re s >= 1/2, in flight as E6Bridge22). conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "dc2b59ea253aae355eb23b92eb634d74e06300ce452da1dcc2ad435183071e95" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge21.xi_logDeriv_deriv_eq_of_regular" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge21.lean" diff --git a/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction_of_strip.toml b/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction_of_strip.toml index 2e5717bf1..3bf0aa951 100644 --- a/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction_of_strip.toml +++ b/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction_of_strip.toml @@ -5,7 +5,14 @@ name = "RH.xi_derivative_partial_fraction_of_strip" statement_module = "Statements.RH_xi_derivative_partial_fraction_of_strip" status = "proved" title = "THE XI PARTIAL FRACTION rests on StripDerivBound ALONE (2026-09-21). conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "aa492e5e013618bcafd0695a1db03ba728ba50f7e35cd6e114104c4033ff0c07" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge23.xiLogDerivDerivEq_of_strip" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge23.lean" diff --git a/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction_of_two.toml b/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction_of_two.toml index b4c48fb43..5ee677b5a 100644 --- a/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction_of_two.toml +++ b/telperion/missions/rh/nodes/RH_xi_derivative_partial_fraction_of_two.toml @@ -5,7 +5,14 @@ name = "RH.xi_derivative_partial_fraction_of_two" statement_module = "Statements.RH_xi_derivative_partial_fraction_of_two" status = "proved" title = "THE XI PARTIAL FRACTION, full chain (2026-09-21): (log xi)'' = -Sum m(rho)/(s-rho)^2 GIVEN only LocalCountSum and StripDerivBound (Liouville with log growth + entire extension + real-axis decay all proved). conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "a69865ddcb587d059c1935397bd7cd4e8f22aede32abc7d27fb34452a9c6bca2" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge22.xiLogDerivDerivEq_of_two" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge22.lean" diff --git a/telperion/missions/rh/nodes/RH_xi_diff_entire_extension.toml b/telperion/missions/rh/nodes/RH_xi_diff_entire_extension.toml index fabed981e..e16c799d3 100644 --- a/telperion/missions/rh/nodes/RH_xi_diff_entire_extension.toml +++ b/telperion/missions/rh/nodes/RH_xi_diff_entire_extension.toml @@ -5,7 +5,14 @@ name = "RH.xi_diff_entire_extension" statement_module = "Statements.RH_xi_diff_entire_extension" status = "proved" title = "XI PARTIAL FRACTION, obligation 1 part A (2026-09-21): deriv(logDeriv xi) + Sum m(rho)/(s-rho)^2 extends to an ENTIRE function (order of xi at every point = the E8 multiplicity; the double pole at a zero of order m is cancelled exactly by its own term; xiDiffExt(1-s) = xiDiffExt(s)). Nothing about RH. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "e398fa71adceb80f40ad6be48b9b8de8e75425693c4dd675ab0ac38549fff749" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge20.xiDiffExt_differentiable" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge20.lean" diff --git a/telperion/missions/rh/nodes/RH_xi_diff_regular_of_growth.toml b/telperion/missions/rh/nodes/RH_xi_diff_regular_of_growth.toml index bde8bf2f2..d28166b09 100644 --- a/telperion/missions/rh/nodes/RH_xi_diff_regular_of_growth.toml +++ b/telperion/missions/rh/nodes/RH_xi_diff_regular_of_growth.toml @@ -5,7 +5,14 @@ name = "RH.xi_diff_regular_of_growth" statement_module = "Statements.RH_xi_diff_regular_of_growth" status = "proved" title = "XI PARTIAL FRACTION, obligation 1 reduced (2026-09-21): XiDiffRegular follows from a logarithmic growth bound on Re s >= 1/2 (XiDiffExtGrowthRight: Landau + Cauchy + Stirling on the strip, Dirichlet-series and digamma bounds on Re s >= 2 -- in flight as E6Bridge22). conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "e398fa71adceb80f40ad6be48b9b8de8e75425693c4dd675ab0ac38549fff749" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge20.xiDiffRegular_of_right" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge20.lean" diff --git a/telperion/missions/rh/nodes/RH_xi_growth_of_two.toml b/telperion/missions/rh/nodes/RH_xi_growth_of_two.toml index 49188f099..e8461c671 100644 --- a/telperion/missions/rh/nodes/RH_xi_growth_of_two.toml +++ b/telperion/missions/rh/nodes/RH_xi_growth_of_two.toml @@ -5,7 +5,14 @@ name = "RH.xi_growth_of_two" statement_module = "Statements.RH_xi_growth_of_two" status = "proved" title = "XI PARTIAL FRACTION, obligation 1 REDUCED to two classical inequalities (2026-09-21): the log-growth bound on Re s >= 1/2 follows from LocalCountSum (Sum m(rho)/(1+(Im rho - a)^2) = O(log a), the textbook consequence of the local zero count) and StripDerivBound (Landau's local partial fraction transferred to the derivative on 1/4 <= Re s <= 9/4 by Cauchy + Stirling). Plan correction recorded: on Re s >= 2 the double-pole sum is O(log t), not O(1). Both in flight (E6Bridge23/24). conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "a69865ddcb587d059c1935397bd7cd4e8f22aede32abc7d27fb34452a9c6bca2" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge22.xiDiffExtGrowthRight_of_two" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge22.lean" diff --git a/telperion/missions/rh/nodes/RH_xi_logDeriv_deriv_decay.toml b/telperion/missions/rh/nodes/RH_xi_logDeriv_deriv_decay.toml index fbfc80851..270245e73 100644 --- a/telperion/missions/rh/nodes/RH_xi_logDeriv_deriv_decay.toml +++ b/telperion/missions/rh/nodes/RH_xi_logDeriv_deriv_decay.toml @@ -5,7 +5,14 @@ name = "RH.xi_logDeriv_deriv_decay" statement_module = "Statements.RH_xi_logDeriv_deriv_decay" status = "proved" title = "XI PARTIAL FRACTION, obligation 2 DISCHARGED (2026-09-21): (log xi)''(sigma) -> 0 along the positive real axis -- termwise differentiation on Re s > 1 (rational terms, the trigamma series with the telescoping bound 1/(x - 1/2), and L(log Lambda)(sigma) -> 0 by Tannery). Unconditional. Nothing about RH. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "dc2b59ea253aae355eb23b92eb634d74e06300ce452da1dcc2ad435183071e95" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge21.xi_logDeriv_deriv_decay" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge21.lean" diff --git a/telperion/missions/rh/nodes/RH_xi_right_deriv_bound.toml b/telperion/missions/rh/nodes/RH_xi_right_deriv_bound.toml index 4c9fcab2c..1ccbe81f7 100644 --- a/telperion/missions/rh/nodes/RH_xi_right_deriv_bound.toml +++ b/telperion/missions/rh/nodes/RH_xi_right_deriv_bound.toml @@ -5,7 +5,14 @@ name = "RH.xi_right_deriv_bound" statement_module = "Statements.RH_xi_right_deriv_bound" status = "proved" title = "XI PARTIAL FRACTION, region C PROVED (2026-09-21): on Re s >= 2, (log xi)'' is bounded (rational terms, the trigamma series on Re z >= 1, and the L-series of log·Lambda for Re s >= 2). Unconditional. conjecture1_proved = False." -updated = "2026-09-21" +updated = "2026-09-24" + +[comparator] +artifact_sha256 = "a69865ddcb587d059c1935397bd7cd4e8f22aede32abc7d27fb34452a9c6bca2" +date = "2026-09-24" +run_id = "36054938938" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36054938938" +theorem = "RvMBridge22.rightDerivBound" [proof] artifact = "../../examples/rvm_bridge/lean/E6Bridge22.lean"