PM-Bounded τ-Control
Formalization of Al-Mayahi's PM-bounded τ-control framework for tokamak fusion stability. The key extension beyond the source paper is the set-level boundary nucleus: the smooth saturation operators are bounded contractions into the PM-safe region, but the genuine Order.Nucleus instance operates on sets, not scalars.
Paper: "PM-Bounded τ-Control for Tokamak Fusion Stability", GFSI, January 2026. UK Patent Application GB2600537.1.
Formal Verification Certificate
Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.
PM-Bounded τ-Control • Lean 4 + Mathlib • Apoth3osis Labs
Core mathematical chain
The completion operator is a bounded contraction into the safe set. The honest nucleus connection is set-level: adjoining [0, Q_{PM}] is idempotent, extensive, and meet-preserving. The central invariant follows from |\mathrm{Sat}(x)| \le Q_{PM}.
Phase 1: Completion Operators
- • Rational and tanh saturation with global boundedness, monotonicity, continuity, oddness
- • Identity regime: |Sat(x)-x| ≤ ε|x| when |x| < εQ_PM
- • Set-level boundary nucleus j(S) = S ∪ [0,Q_PM] via Order.Nucleus
Phase 2–3: Risk + τ-Progression
- • Tokamak risk proxy Q = β·Ψ(q)·(1+T) with monotonicity in β
- • Central invariant: PM-completed source ⇒ Q(u(t)) ≤ Q_PM for all time
- • Progression density ≥ 1 always, effective step vanishes as Q → Q_PM
Phase 4–5: Gate + Multi-Limit
- • Soft gate ω ∈ [0,1]: purely classical when safe, purely completed when critical
- • Norm-bounded radial projection with Euclidean energy norm
- • SafEDMD integration: ReLU ∘ Sat composition preserves n·Q_PM² energy bound