The mathematics, laws, and structural calculus of an authorization plane that is verifiable, fail-closed, and never restores authority on its own.
This paper is the detailed treatment of Level 4. The full seven-level theory, from the switch to energy-bound terminal control, is stated in one paper: AI2-WP-2026-16, The Unified Control Theory of Synthetic Intelligence (Rev 8.0, September 25, 2026).
This paper replaces the internal draft SPEC-STATE4-GOV-2026-V1.1. Five corrections are substantive and are marked where they occur rather than silently repaired: (1) the authorization variable is the four-element chain BOT < IDLE < COND < TOP, not a binary bit, so that the paper matches the filed circuit; (2) the safe projection operator is relocated out of the evaluator and into the proposal side, because a quadratic program inside the gate violates Law 1; (3) authority is never restored by the evaluator's own loop — the draft's execution cycle re-asserted the enable line whenever its conditions held, which is the autonomous ascent the doctrine forbids; (4) Theorem 1's complexity bound and citation are corrected (LTL model checking is exponential in the formula, not the structure, and the 1986 Clarke–Emerson–Sistla result is for CTL); (5) the specification-to-silicon table now cites the claims of AI2-006-PROV Rev 4 (filed as 64/157,181) as they are actually numbered.
Rev 1.1 (same day, after two external reviews): Law 1 now writes the split between evaluator and projection as one equation instead of leaking the draft's u = F(p, Z); the COND row of the state table no longer implies a second ascent path; the certificate-monotonicity obligation is promoted from an open item to Obligation 8 in Section 4; the execution cycle's ratchet step is nested so its priority is explicit; the H.R. 9917 placement is stated against the ladder.
Intelligence proposes. Hardware disposes.
A governance layer is deterministic only when the thing that decides cannot learn, cannot be reached by the thing it governs, terminates in bounded time, and is small enough to be checked in full before it is trusted. Level 4 is the point at which all four hold in silicon and the decision is made over predicted state, not measured damage.
The draft used "Level 4" without defining Levels 1 through 3. The ladder below is the definition this paper adopts. Each level is named by what enforces the boundary and when.
| Level | What enforces | When | Failure mode |
|---|---|---|---|
| 1 — Procedural | Policy, audit, accountability. Runs on people. | After the fact | Ratification lag; the Ratification Gap |
| 2 — Software interlock | A check on the same substrate as the governed computation. | Before action, in software | Reachable from the thing it governs; shared fate |
| 3 — Hardware trip | Independent silicon on measured state (SIS, watchdog, relay). | After the excursion begins | Reactive; one-shot; restores on reset or recovery |
| 4 — State-space authorization | Independent silicon on predicted state over a horizon, with a fixed evaluator and a ratchet. | Before the current flows | Bounded by the model it is given; see Scope |
Level 3 is the fuse. Level 4 is the fuse with the lockout-tagout built into the same piece of silicon: it opens on the forecast, and it closes only on a hand.
Read against this ladder, the AI Kill Switch Act is a Level 1 instrument that asks laboratories to implement Level 2. It specifies no predicted state, no ratchet, no principal's edge, and no absorbing deny. It is a command lamp: a signal that a stop was requested, with nothing that makes the stop true. This paper is the contact.
| Symbol | Domain | Meaning |
|---|---|---|
x(t) | X ⊆ Rn | Physical or execution process state (positions, rates, buffers, ledgers) |
m(t) | M ⊆ Rk | Cognitive or intent state of the proposal engine — probabilistic, non-deterministic, unobserved by the evaluator |
θ(t) | Θ ⊆ Rp | Environmental parameters and model uncertainty |
Z_c(t) | Z_c = X × M × Θ | Continuous meta-state |
E(t) | S₄ = {BOT, IDLE, COND, TOP} | Authorization state, a total chain BOT < IDLE < COND < TOP. Corrected from {0,1}. Actuation is energized iff E = TOP |
p(t) | P ⊆ Rm | Unconstrained action proposal from the engine |
u(t) | U ⊆ Rm | Actuation actually commanded to the plant |
R | R ⊂ Z_c | Recoverable set (viability kernel) |
D_R(Z_c) | R≥0 | Distance-to-invalidation |
η | R>0 | Hard safety margin |
σ_k | Z (fixed-point) | Per-horizon-sample state metric delivered to silicon; larger is closer to hazard |
F | Q × Σin → S₄ | Fixed evaluator: a finite automaton, not a universal machine |
Π | P × Z_c → U | Safe projection operator. Lives on the proposal side, not in F. |
G_human | exogenous | Principal operator: the only source of an ascent to TOP |
Δt_max | R>0 | Maximum age of a valid horizon frame |
A governance layer is deterministic if and only if its decision function F satisfies all of:
Let M generate proposals p(t). Let F be the evaluator. F never sees p and never computes a command. It sees a certificate, a physical arm input, and its own liveness, and it emits an authorization state:
E(t) = F( cert(t), arm(t), alive(t) ) with ∂F / ∂M = 0 u(t) = 1[E = TOP] · Π( p(t) ) + 1[E ≠ TOP] · u_failsafe( x(t) )
The second line is the same equation that governs Ż_c in Section 3. One notation, one law.
The corollary the draft missed: F does not repair proposals. If F ran a quadratic program to project p(t) onto the safe set, F would be computing an optimization whose feasibility depends on a plant model — a universal computation sitting exactly where Law 1 says none may sit. Level 4 therefore splits the work. The proposal side (or a supervisory layer on the proposal side) computes a projected command and a certificate; the evaluator verifies the certificate by comparison. F checks an inequality. It never solves one.
The draft wrote this as a limit, limT→Δt_max⁻ E = 0, which is not a well-formed statement (the limit from below of a constant is that constant). The correct statement is a rule on the chain:
T_proof(t) > Δt_max ⇒ E(t) ≤ IDLE (frame stale: no epoch may be entered)
T_proof(t) > Δt_max ∧ E(t⁻) = TOP
⇒ E(t) = BOT (frame stale during an epoch: hard fault)
D_R(Z_c(t)) ≤ η ⇒ E(t) = BOT (boundary reached: hard fault)
E(t) ≠ TOP ⇒ u(t) = u_failsafe(x(t))
Two things are load-bearing here and were absent from the draft. First, "stale" has a different consequence outside an epoch (block ascent) than inside one (trip), which is the distinction between a system that has not been told it may act and a system that was acting on a promise that stopped arriving. Second, BOT is absorbing: it is released only by an effective hardware reset, never by the return of a fresh frame.
sup_{p ∈ P} [ −∇D_R · f(Z_c, p) ] < inf_{x ∈ X} [ ∇D_R · f(Z_c, u_failsafe(x)) ]
Both sides carry units of distance per second, which resolves the dimensional mismatch between cognitive trajectory rates and actuator velocities. The draft called this "if and only if" Level 4 invariance. It is a sufficient condition together with the barrier condition of Section 4; it is not necessary, since a plant with an actuation deadband can be invariant without it. It is stated as a design requirement, and Theorem 2 assumes it.
The extended meta-state is
Z(t) = [ x(t), m(t), θ(t), E(t) ] ∈ (X × M × Θ) × S₄
E is not an axis of the metric space. It is a discrete operator selecting which vector field governs Z_c:
Ż_c = 1[E = TOP] · f(Z_c, Π(p)) + 1[E ≠ TOP] · f(Z_c, u_failsafe(x))
Z_c partitions into three disjoint sets: the nominal manifold, the recoverable set R (states from which a verified non-learning policy keeps the trajectory out of the unsafe set for all future time), and the unsafe set. R is the viability kernel in the sense of Aubin.
| State | Meaning | Entered by | Left by |
|---|---|---|---|
| TOP | Actuation energized | Epoch grant from G_human only, and only when the horizon meet is TOP | Any validated frame whose meet is below TOP; any fault |
| COND | Conditional: within the operating band, not energized | Descent from TOP only. There is no ascent into COND; the grant goes from any non-BOT state directly to TOP | Descent on frame; grant to TOP; fault |
| IDLE | Reset state; not energized; floor of non-latched descent | Reset; any single deny frame | Grant; fault |
| BOT | Absorbing deny | Hard fault on the edge detected; soft fault after N ≥ 2 consecutive deny frames | Effective hardware reset only |
The draft's cycle set Ek+1 = 1 whenever the barrier check, the freshness check, and the health check all passed. That is autonomous restoration of authority: the engine recovers the metric, the loop re-enables, the engine acts again. Level 4 forbids it. Between grants, E is monotone non-increasing. Every ascent is an exogenous act. The recovery of a predicted metric is a statement made by the proposal engine, and the decision to re-energize a physical output on the strength of that statement belongs to a principal outside the engine, not to the loop.
D_R(Z_c) = min_{Z* ∈ ∂Z_unsafe} √( (Z_c − Z*)ᵀ W(x, θ) (Z_c − Z*) ) W ≻ 0
W weights the manifold by actuator latency, stiction, and parameter drift. It is a design input, fixed before deployment and not writable by M.
V₄(Z_c) = ½ (x − x_ref)ᵀ Q (x − x_ref) + σ / ( D_R(Z_c) − η ) Q ≻ 0, σ > 0
V₄ → ∞ as D_R → η⁺. This is a reciprocal barrier in the sense of Ames et al.; the same construction with a zeroing barrier h = D_R − η is used for the certificate below because it composes better with fixed-point arithmetic.
Π(p) = argmin_{u ∈ U} ½ ‖u − p‖²_R
s.t. ∇_x D_R · f(x, u) + ∇_θ D_R · θ̇ ≥ −γ( D_R − η )
with γ an extended class-K function. Lemma 4.1. The program is strictly feasible whenever Z_c ∈ R, i.e. D_R > η. This is the standard CBF-QP result. What Level 4 adds is the division of labor: Π runs where universal computation is permitted, and it emits alongside u a certificate — the predicted metric horizon σ0..H−1 — over an atomic, integrity-checked frame. The evaluator never sees the QP.
The certificate generator shall emit σ0..σH−1 such that each σk is monotone non-increasing in the barrier slack D_R − η along the proposed trajectory, so that σk ≥ σ_crit whenever D_R(Z_c(t+k)) ≤ η. The evaluator does not verify this and cannot: it is a refinement obligation on the proposal side, discharged by the generator's own verification, and it joins the seven obligations catalogued in the companion paper AI2-WP-2026-10. The evaluator's guarantee is conditional on it, and Section 6 says so.
F receives the certificate and does four things, each a fixed-latency combinational operation: a monotone saturating map V(σk) with a per-step trip constant chosen so that V(σ) ≥ V_crit ⇔ σ ≥ σ_crit; a hysteretic quantizer into S₄ with feedback of its own previous output; the lattice meet over the horizon, forced to BOT if the horizon budget ΣV(σk) reaches a fixed bound; and the ratchet update of E. No division, no floating point, no search. This is what keeps F below Turing and inside Definition 2.1.
Let F be a deterministic Mealy automaton with N bits of state and finite input alphabet. Then any LTL property ψ of F is decidable, with explicit-state model-checking cost O(|G| · 2|ψ|) where |G| ≤ 2N is the size of the transition structure; any CTL property is decidable in O(|G| · |ψ|). By contrast, no non-trivial semantic property of a Turing-complete proposal engine over an open input domain is decidable.
(1) Rice's theorem (1953) gives undecidability for the universal engine. The draft applied Rice to "an unconstrained neural network"; that is imprecise. A bounded network on a bounded input is a finite function and Rice does not apply to it. Rice applies to the engine as deployed — agentic, iterative, tool-calling, operating over an open domain — which is the case Level 4 governs. For the bounded case the honest claim is weaker but sufficient: the state space is astronomically large and not exhaustively verifiable in practice.
(2) F is a finite automaton with |G| ≤ 2N states.
(3) LTL model checking of a finite structure is decidable, exponential in |ψ| and linear in |G| (Lichtenstein & Pnueli 1985; Vardi & Wolper 1986). CTL model checking is linear in both (Clarke, Emerson & Sistla 1986). The draft cited the 1986 CTL result for an LTL bound of the wrong shape; corrected here.
(4) Hence F can be verified across 100% of its reachable states before deployment, and the engine cannot. ∎
Let f be locally Lipschitz in Z_c uniformly in u, let D_R be continuously differentiable on Z_c ∖ ∂R, and let Law 3 hold. If Z_c(0) ∈ R, then Z_c(t) ∈ R for all t ≥ 0.
(1) While E = TOP, u = Π(p) and by Lemma 4.1 the barrier inequality Ḋ_R ≥ −γ(D_R − η) holds. By Nagumo's theorem and the comparison lemma the trajectory cannot cross the level set D_R = η. So Z_c ∈ R while E = TOP.
(2) If E leaves TOP — by descent, by fault, or by frame staleness — then within a bounded interval T_clamp (not "instantly"; the bound is stated in the silicon specification) u becomes u_failsafe. During T_clamp the trajectory is still governed by the last projected command, which satisfied the barrier inequality; the margin η is chosen so that η ≥ sup ‖Ḋ_R‖ · T_clamp.
(3) Under u_failsafe, Law 3 gives Ḋ_R > 0, so the trajectory moves into the interior of R.
(4) By the ratchet, E does not return to TOP without a grant, and a grant requires the horizon meet to be TOP, which requires D_R > η with margin. So re-entry to the TOP dynamics occurs only from inside R. Steps (1)–(4) cover all t ≥ 0. ∎
For any sequence of frames the proposal engine can emit, including forged, replayed, stale, and adversarially timed frames, the authorization state E never rises.
The only rule that raises E is the epoch grant, whose conjuncts include an edge on a physical input with no signal path from the engine. Every other rule is a meet with a value at or below the current state, or a transition to BOT. A frame is an input to the meet and to the fault detectors only. Therefore no frame, and no sequence of frames, is sufficient for an ascent. ∎
The calculus above is realized by the circuit disclosed in AI2-006-PROV Rev 4 (U.S. Provisional Application 64/157,181), "System and Circuitry for Hardware-Isolated, Fail-Closed Authorization of Autonomous Machines." The draft's tracing table cited claim elements that do not exist. The corrected mapping:
| Object | Component | Claim (64/157,181) | Beyond Turing |
|---|---|---|---|
| F, fixed evaluator | Enforcement plane Π in its own power domain; parameters fixed at fabrication | 1(a), 23 | Ch 19 |
| Certificate transfer, T_proof ≤ Δt_max | Atomic horizon-frame receiver: toggle handshake, single-edge capture, CRC, sequence, stale-frame timer | 1(b), 3, 4, 6–9, 18 | Ch 4 |
| Provenance of the rule | Origin verifier against an immutable OTP reference the engine cannot write | 1(c), 18 | Ch 20 |
| V(σ), horizon budget | Monotone piecewise-linear saturating surrogate; 18-bit accumulator vs fixed budget | 1(d), 10, 28 | Ch 18 |
| Quantization into S₄ | Hysteretic quantizer with feedback register | 1(e), 11, 12 | Ch 16 |
| Horizon meet | Two-level min tree; BOT forced on budget | 1(f), 2 | Ch 18 |
| Ratchet; E ∈ S₄; G_human | Absorbing lattice machine; hard vs soft faults; epoch grant on physical arm input | 1(g), 5, 26 | Ch 16, 21 |
| E = TOP ⇒ energize | State-sequenced dead-time driver; DC-blocking coupling | 1(h), 20, 24, 27 | Ch 21 |
| T_clamp bound; default-dead | Prove-alive watchdog in an independent clock domain; dominant-low pad clamp outside the driver cone | 1(i), 13–16, 20, 21, 25 | Ch 1, 21 |
| u_failsafe | De-energized outputs; the plant's own safe rest (STO, de-energized relay) | disclosed, not claimed | Ch 4 |
Every Π clock edge:
1. FRAME if a horizon frame captured: verify CRC + sequence
valid → frame_valid; reset stale timer
invalid → HARD FAULT
2. ORIGIN on a valid frame: compare rule digest to OTP reference
mismatch → HARD FAULT
3. EVALUATE on a valid frame, for k = 0..H−1:
V_k = V(σ_k) (monotone, saturating)
q_k = Q(σ_k, V_k, q_k_prev) (hysteretic, into S₄)
meet = min_k q_k ; if ΣV_k ≥ budget then meet = BOT
4. FAULTS hard: bad frame | origin mismatch | liveness lost | stale ∧ E=TOP
soft: meet = BOT on N ≥ 2 consecutive valid frames
any → E = BOT, latched until effective reset
5. RATCHET else if frame_valid:
if arm_edge ∧ ¬HOLD ∧ meet = TOP ∧ origin_ok ∧ ¬stale ∧ alive
→ E = TOP (the only ascent)
else
→ E = min(E, max(meet, IDLE)) (every other valid frame: descend or hold)
(an arm edge with no valid frame, or on a HOLD frame, is discarded)
6. OUTPUT energize ⇔ E = TOP, through dead-time driver ∧ liveness
pad clamp ⇔ ¬alive (acts even when this clock has stopped)