Field Guard: A Machine-Checked Governed-Map Contraction Stabilizer with Composition Certificate

Field Guard (FG) is the hard stabilizing layer of the REAL E3 stack. It constrains a six-dimensional control vector toward per-state targets by a certified contraction, then enforces hard safety bounds. The certified object is the governed map H = FG_proj ∘ F, where F is a linear normal-matrix contraction and FG_proj is a coordinate-wise box projection. H is a contraction with factor κ = √0.95 ≈ 0.97468 in the Lyapunov norm, giving an ISS gain 1/(1−κ) ≈ 39.494. The contraction, the projection non-expansiveness, and the assembled ISS bound are machine-checked in Lean 4 with zero sorries and no added axioms. This restricted edition contains the proofs and the deployed governance configuration. Extends WP-FG-002 (Zenodo 10.5281/zenodo.18838465). Access rights Restricted Access conditions (the text Zenodo shows to people who request access) Restricted to authorised collaborators and reviewers of REAL E3 Systems Oy. Contact [email protected] to request access. The core contraction method is subject to national patent application PRH1 Application 20265235, filed with the Finnish Patent and Registration Office (PRH), March 11 2026. RE3 are proprietary systems of REAL E3 Systems Oy, Finland. This document discloses the mathematical stability certificate for independent verification purposes only. The harness implementation code, state extraction methodology, and REAL-E3 internal architecture are proprietary and not disclosed. Publication does not constitute a licence to implement, reproduce, or deploy any component of the REAL-E3 architecture. This notice also applies to all prior publications by REAL E3 Systems Oy, including WP-FG-002 (DOI: 10.5281/zenodo.18838465). Licensing enquiries: [email protected]