We just eliminated “trust the solver” for Optimal Transmission Switching. For the first time, anyone can independently re-verify global optimality and tight objective bounds for both DC and AC Optimal Transmission Switching in exact rational arithmetic — with Lean 4 kernel proofs on the core claims. Yesterday (DC): We closed the IEEE 118-bus gap from 0.39% to an absolute gap of 5.33×10⁻¹⁰ and replayed certificates on networks up to 78,478 buses on a single laptop. Today (AC): Full enumeration of all 64 topologies on PGLib case5 certifies a unique globally optimal topology. On case57, case118 and case500 we deliver exactly checked all-topology intervals of relative width ≤ 0.94% and a certified positive value of switching — again with no tolerance. These are classic NP-hard problems that the field has accepted as floating-point black boxes. The certificates, checkers, and Lean proofs are now public. Replay them yourself: AC: zenodo.org/records/23590482 DC: zenodo.org/records/23552323 If this holds under scrutiny, topology optimization for the grid just became auditable. #PowerSystems #GET #Lean4 #FormalVerification #EnergyTransition @ENERGY @ieee_pes @FERC @SPPorg @MISOenergy @pjminterconnect @CaliforniaISO @ERCOT_ISO @NewGrid @ARPAE

Sharing again: The Democratization of Sacral Kingship, a vertical prosopography of one Anglo-American lineage across ~45 generations. From the sacral kings of Wessex and the Gaelic overlords of Inishowen (Ó Dochartaigh) to the laboring and middle classes of industrial Buffalo and the Kansas prairie. One result that continues to stand out: medieval Gaelic genealogists tracing the Ó Dochartaigh line from Niall of the Nine Hostages were recording biological descent with considerable accuracy. The R-M222 haplogroup supplies genetic corroboration roughly 1,700 years later, concentrated in the same northwest Irish heartland the historical sources describe. Downward mobility treated as structural (partible inheritance, demographic surplus, religious dissent) rather than decline, with a side-by-side comparison of two lines descending from Ethelred II. Happy to discuss the method, the genetics, or the broader argument. #Genealogy #RM222 #IrishHistory #Prosopography

We just crossed a line that used to look impossible. Independently checkable certificates for DC Optimal Transmission Switching, now running on every network in PGLib, up to 78,478 buses and 126,015 lines, on a single laptop. DC-OTS is a classic NP-hard mixed-integer problem. For years the field has lived with floating-point solver output that is difficult to audit independently. Today we are releasing certificates that let anyone re-verify feasible upper bounds and globally valid lower bounds in exact rational arithmetic without trusting the machine that produced them. What changed: → A new residual-bounded witness rule that keeps certificates linear in network size (no more quadratic angle blow-up) → Exact-rational replay of objective intervals across the full PGLib-OPF suite → Lean 4 proofs of interval soundness and the residual-witness theorem → On the IEEE 118-bus system, a previous 0.39 % gap reduced to an absolute gap below 10⁻⁹ The largest certificates still use economic-dispatch lower bounds, so they prove verification scale rather than tight optimality. That distinction is deliberate. The infrastructure to check 78 k-bus claims on commodity hardware is now real. The producer remains proprietary. The certificates, verifier, residual-witness checker, conversion tools, and Lean development are released so the results can be examined and replayed by anyone. This is for everyone working on transmission topology, Grid-Enhancing Technologies, large-scale MIP, or formal verification of optimization claims. Paper + full verification bundle: doi.org/10.5281/zenodo.23552… @SPPorg @MISOenergy @pjminterconnect @CaliforniaISO @ERCOT_ISO @FERC @NewGrid @IEEE_PES @ENERGY Researchers & practitioners in topology optimization, certified optimization, and Lean: would value your eyes on this. #PowerSystems #OptimalTransmissionSwitching #GETS #MIP #FormalVerification #Lean4 #ExactArithmetic #PGLib #GridEnhancingTechnologies

Just put up a Lean 4 formalization of Dusart’s bound on the sum of 1/p. The kernel checks pretty much the whole argument and reduces it to one published Chebyshev estimate. Includes the certificates, generators, and a full replay: zenodo.org/records/23479494