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
Lean modules
Open PPC pageMENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerPM-Bounded τ-Control for Fusion Stability
Contributor
Abdulsalam Al-Mayahi
GFSI
Core framework: replace divergent source terms with smooth saturation operators Sat_{Q_PM}(x) = x/(1+|x|/Q_PM), combined with internal time dilation τ that freezes effective steps near the PM boundary, and a convex soft gate for smooth transition between classical and controlled regimes.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerSet-Level Boundary Nucleus Bridge
Contributor
Apoth3osis Labs
R&D Division
Extension beyond the source paper: the smooth saturations are bounded contractions into the PM-safe region [0, Q_PM], but are not themselves idempotent. The genuine Order.Nucleus connection is the set-level operator j(S) = S ∪ [0, Q_PM], which is idempotent, extensive, and meet-preserving on Set ℝ.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Lean 4 Formalization — PMBoundedControl
Contributor
Apoth3osis Labs
R&D Division
Machine-checked Lean 4 lane covering completion operators, risk functionals, τ-progression, soft transition gate, and multi-limit vector completion with SafEDMD energy proxy integration. Three consecutive adversarial audits PASS. Zero sorry on the full surface.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
Verified C + Safe Rust Runtime Surface
Contributor
Apoth3osis Labs
R&D Division
Reference C and Rust artifacts mirror all five Lean modules: saturation operators, risk functionals, progression density, soft gate, and vector completion. C compiled with -Wall -Wextra -Werror. Rust: 16 tests passing, 0 unsafe.
Builds Upon
MENTAT Contribution Record
BRIDGE
Cross-Level Connection
CONTRIBUTION LEVEL: BRIDGE
SafEDMD Multi-Limit Integration
Contributor
Apoth3osis Labs
R&D Division
Multi-limit completion layer connects PM-bounded control to the existing SafEDMD energy proxy infrastructure: componentwise saturation → ReLU nucleus → sqSum energy bound. Proves relu_after_componentwise_sqSum_le ≤ n·Q_PM².
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026
“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune
A janitor who proves a theorem outranks a tenured professor who publishes noise.
Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
Ethics, review & quality assurance
Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.