>_PPC/PM_BOUNDED_TAU_CONTROL

Paper → Proof → Code

Formalization of Al-Mayahi's PM-Bounded τ-Control framework for tokamak fusion stability. The Lean lane adds the missing formal bridge: scalar saturation operators as bounded contractions into a genuine set-level boundary nucleus, with risk functionals, adaptive τ-dilation, soft gate blending, and multi-limit vector completion integrated with the SafEDMD energy proxy.

Core construction: pmBoundaryNucleus Q_PM : Nucleus (Set ℝ) — the honest set-level closure operator where SatRational lands in the safe region but is not itself idempotent.

Lean Modules

Public Theorems

Sorry Count

717

Lines

C Files

Rust Modules

>_VERIFICATION.SEAL

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.

44 THEOREMS VERIFIED7 MODULES0 SORRY

PM-Bounded τ-Control • Lean 4 + Mathlib • Apoth3osis Labs

Key Mathematics

\operatorname{Sat}_{Q_{PM}}(x) = \frac{x}{1 + |x|/Q_{PM}} \qquad |\operatorname{Sat}(x)| \le Q_{PM}

Rational saturation — globally bounded, identity-like in the classical regime.

j_{PM}(S) = S \cup [0, Q_{PM}] \;:\; \mathrm{Nucleus}(\mathrm{Set}\;\mathbb{R})

Set-level boundary nucleus — idempotent, extensive, meet-preserving via Order.Nucleus.

\forall t,\; Q(u(t)) \le Q_{PM} \quad \text{(PM invariant)}

Central theorem: PM-completed source preserves the PM boundary for all time.

Downloads

Lean proofs (tar.gz) Verified C (tar.gz) Safe Rust (tar.gz)

Research project page →

>_CORRESPONDENCE

Paper ↔ Proof Correspondence

Al-Mayahi, "PM-Bounded τ-Control for Tokamak Fusion Stability", GFSI, January 2026

PAPER SECTION	LEAN MODULE	STATUS
§3.1 PM-Bounded Completion	CompletionOperator.lean	PROVED
§3.2 Risk Functional & Boundary	RiskFunctional.lean	PROVED
§3.3 τ-Progression	TauProgression.lean	PROVED
§3.4 Soft Gate Blending	SoftTransition.lean	PROVED
§3.5 Multi-Limit Completion	MultiLimit.lean	PROVED
Appendix A: Scalar Benchmark	RiskFunctional.lean	PROVED
Appendix B: 65+ Embodiments	—	N/A
Appendix C: 3D Tokamak Sim	—	N/A

>_PROOF.BLUEPRINT

Proof Blueprint

Click to expand. Switch between Mathematics and Lean 4 views.

Core scalar saturation operators — rational and tanh variants — with the honest set-level boundary nucleus connecting to Mathlib's Order.Nucleus.

Definitions

\operatorname{Sat}_{\mathrm{Q_{PM}}}(x) = \frac{x}{1 + |x|/Q_{PM}}

Rational saturation: bounded by Q_PM, identity-like for |x| ≪ Q_PM.

\operatorname{Sat}_{\tanh}(x) = Q_{PM} \cdot \tanh\!\left(\frac{x}{Q_{PM}}\right)

Smooth tanh variant with the same asymptotic behavior.

j_{PM}(S) = S \cup [0, Q_{PM}]

Set-level boundary nucleus — genuine Order.Nucleus on Set ℝ.

Theorems

sat_rational_boundedQED

|\operatorname{Sat}_{Q_{PM}}(x)| \le Q_{PM}

Global bound: saturation never exceeds the PM boundary.

sat_rational_monotoneQED

\operatorname{Monotone}(\operatorname{Sat}_{Q_{PM}})

Preservation of ordering under saturation.

sat_rational_identity_regimeQED

|x| < \varepsilon Q_{PM} \;\Longrightarrow\; |\operatorname{Sat}(x) - x| \le \varepsilon|x|

In the classical regime, saturation is nearly identity.

sat_rational_mem_safeSetQED

x \ge 0 \;\Longrightarrow\; \operatorname{Sat}(x) \in [0, Q_{PM}]

Nonneg input lands in the PM safe set.

pmBoundaryNucleus_fix_safeSetQED

j_{PM}([0, Q_{PM}]) = [0, Q_{PM}]

The safe set is a fixed point of the boundary nucleus.

Lean artifact inventory

CompletionOperator.lean RiskFunctional.lean TauProgression.lean SoftTransition.lean MultiLimit.lean

>_VERIFIED.C

Verified C Artifacts

completion_operator.c

Rational/tanh saturation + safe set

risk_functional.c

Tokamak risk + scalar benchmark

tau_progression.c

Progression density + effective step

soft_transition.c

Gate weight + convex blend

multi_limit.c

Vector completion + ReLU nucleus

>_SAFE.RUST

Safe Rust Artifacts

Cargo.toml

Crate manifest

src/lib.rs

Module re-exports (5 modules)

src/completion_operator.rs

Saturation + safe set

src/risk_functional.rs

Risk + blow-up benchmark

src/tau_progression.rs

Density + effective step

src/soft_transition.rs

Gate + blend

src/multi_limit.rs

Vector completion + ReLU

>_PROVENANCE

Provenance Chain

Research Paper

Al-Mayahi, GFSI, January 2026. UK Patent GB2600537.1.

Lean 4 Proofs

5 modules, 44 theorems, 0 sorry. Verified by the Lean 4 kernel.

Adversarial Audit

3 consecutive PASS audits. Audit-remediated nucleus and Euclidean norm.

Verified C

5 C files. Compiled with gcc -std=c11 -Wall -Wextra -Werror.

Safe Rust

5 modules + lib.rs + Cargo.toml. 16 tests passing, 0 unsafe.