>_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.

⊢⊣⊢⊣

>_MENTAT.JOIN

“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.

ONTOLOGICAL ENGINEER8 designations

IDEA

A valid, original framing or conjecture

THEORY

Formal argument with paper-level rigor

APPLICATION

Connecting theory to observable outcomes

CODE

Working software the project depends on

EXPERIMENT

Reproducible research with methodology and data

PROOF

Machine-verified claim checked by a proof assistant

KERNEL

Foundational, load-bearing implementation

BRIDGE

Connecting subsystems or knowledge domains end-to-end

NOETIC ENGINEER8 designations

VISIONARY

Strategic direction & roadmaps

NARRATOR

Writing, documentation & papers

DESIGNER

Visual, UX & information design

EDUCATOR

Teaching, tutorials & workshops

CULTIVATOR

Community, outreach & events

DIPLOMAT

Partnerships, governance & policy

INTERPRETER

Translation, media & accessibility

SENTINEL

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.

APPLY TO MENTAT EXPLORE PROJECTSMESH-ENCRYPTED NETWORK FOR TRUSTED AUTONOMOUS TRANSACTIONS