DrMurphyIsIn · DrMurphyIsIn · Sep 24, 2026
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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"