Fusion plant with engineering gain > 1 (net electricity)

No fusion device has produced net electricity as of 2026. NIF has repeatedly achieved target gain > 1 (a record ~3.8 in 2026) but its lasers draw roughly 300 MJ of wall-plug energy to deliver ~2 MJ to the target, so the facility is far from engineering breakeven; magnetic-confinement devices (SPARC, Helion Polaris) have not yet reported Q > 1.

Source: lasers.llnl.gov

import Mathlib

/-!
# Fusion plant with engineering gain Q_eng > 1 (net electricity)

What counts as SOLVED: over a single continuous, metered operating window, a fusion
plant exports more electrical energy than the whole facility draws, with the
electricity traceable to fusion reactions, and no credit for pre-charged storage.

Q_eng := E_gross_electric / E_recirculating, where E_recirculating is ALL electrical
input to the facility during the window (heating/drivers, magnets, cryogenics, pumps,
tritium plant, controls, hotel load). This is stricter than scientific gain Q_sci.

Concrete in Lean: the gain and net-energy arithmetic, the acceptance predicate,
rungs, and a proved lemma that Q_eng > 1 is the same as positive net energy.

Opaque oracle (`Measurement`): revenue-grade meter readings at the plant boundary,
energy-storage state of charge, and the attestation that the output is fusion-derived
(neutron/fusion-product diagnostics consistent with the claimed fusion power).
Attesters: an independent metering auditor / grid operator plus a diagnostics review
panel (e.g. the milestone reviewer in a DOE Milestone-Based program).

Units: energy in joules, time in seconds.
-/

namespace OpenSpur.Problems.FusionNetElectricity

/-- Attested measurements for one operating window (oracle). -/
structure Measurement where
  duration : ℝ              -- s
  grossElectric : ℝ         -- J, generator terminal output
  recirculating : ℝ         -- J, all facility electrical input
  storageStart : ℝ          -- J, on-site stored energy at window start
  storageEnd : ℝ            -- J, at window end
  fusionOrigin : Prop       -- attested: output derives from fusion reactions
  independentlyMetered : Prop

noncomputable def qEng (m : Measurement) : ℝ := m.grossElectric / m.recirculating

def netElectric (m : Measurement) : ℝ := m.grossElectric - m.recirculating

structure Thresholds where
  minQEng : ℝ         -- ≥ 1; e.g. 1 for the headline claim
  minDuration : ℝ     -- s; e.g. 3600 for a sustained hour

def Solved (T : Thresholds) (m : Measurement) : Prop :=
  m.fusionOrigin ∧ m.independentlyMetered ∧
  0 < m.recirculating ∧
  T.minDuration ≤ m.duration ∧
  m.storageStart ≤ m.storageEnd ∧      -- no net discharge of stored energy
  0 < netElectric m ∧
  T.minQEng ≤ qEng m

/-- Rung k: Q_eng ≥ 1 + k/2 and duration ≥ base · (k+1). -/
noncomputable def rung (base : ℝ) (k : ℕ) : Thresholds :=
  { minQEng := 1 + (k : ℝ) / 2, minDuration := base * ((k : ℝ) + 1) }

/-- With positive recirculating energy, Q_eng > 1 iff net electricity is positive. -/
theorem qEng_gt_one_iff (m : Measurement) (h : 0 < m.recirculating) :
    1 < qEng m ↔ 0 < netElectric m := by
  unfold qEng netElectric
  rw [one_lt_div h, sub_pos]

theorem rung_mono (base : ℝ) (hb : 0 ≤ base) (m : Measurement) {j k : ℕ} (hjk : j ≤ k)
    (h : Solved (rung base k) m) : Solved (rung base j) m := by
  have hc : (j : ℝ) ≤ k := by exact_mod_cast hjk
  obtain ⟨h1, h2, h3, hd, hs, hn, hq⟩ := h
  refine ⟨h1, h2, h3, ?_, hs, hn, ?_⟩
  · simp only [rung] at hd ⊢
    have : base * ((j : ℝ) + 1) ≤ base * ((k : ℝ) + 1) :=
      mul_le_mul_of_nonneg_left (by linarith) hb
    linarith
  · simp only [rung] at hq ⊢; linarith

end OpenSpur.Problems.FusionNetElectricity

• LLNL NIF ignition shot record (yields and target gains)
• DOE Milestone-Based Fusion Development Program (public milestone reviews)
• Retrospective on the DOE Milestone program (arXiv 2609.28398)