Deterministic Execution Boundaries for Autonomous Intelligence

A Formal Axiomatic Specification of Spatial Authorization Lattices

4.2 → 4.4

1. §0 added. A short control-theoretic motivation stating what is being controlled and why, so the formal sections do not open cold.
2. Monotonic restraint moved from software axiom to hardware structure. Rev. 4.2 stated H1 as a property of rules in the PCR™ compute layer, which the boundary model places in the unchecked domain. Rev. 4.4 adds a latched aggregate (Definition 3) and proves (Theorem 4) that unsafe-set invariance holds for arbitrary rules, including malicious ones, when the latch is realised in hardware. H1 is retained as the admissibility criterion for well-behaved rules; the latch is what enforces it. A sixth refinement obligation follows.
3. Quaternary semantics made explicit and aligned to the filed circuit. Rev. 4.2's theorems all held on a two-element chain. Rev. 4.4 assigns distinct operational roles to all four values (§2.1.1), taken directly from the state machine of 64/157,181: a latched trip, two non-latched hold states, and a single energised state entered only by physical grant. The theorems are unchanged; the four values now do work, and the paper and the filing describe the same machine.
4. Kill switch located inside the framework. The degrading rule R↓ of the model witness is identified as the shutdown primitive. It is an admissible rule, and the least informative one (§5.3).
5. Labels locked to the filing. The elements are BOT < IDLE < COND < TOP as in 64/157,181 (⊥ ≡ BOT, ⊤ ≡ TOP). The public exhibit's HOLD / PERMIT / BYPASS labels should be retired in favour of these.
6. Threshold moved to ⊤. Rev. 4.2 fixed τ = Q₁. The filed circuit energises outputs only in TOP, so Rev. 4.4 fixes τ = ⊤. Every proof carries over unchanged, since each uses only τ > ⊥.
7. All formulae that were lost to rendering in 4.2 are written out.

Control-Theoretic Motivation

Classical control writes a system as ẋ = f(x, u) and steers the state x through a fixed field f so that it stays inside a safe set. Three assumptions carry that picture: f is fixed, x is observable, and the safe set is known. None survives contact with an autonomous model. Its law of motion rewrites itself; its internal state is of dimension 10⁹ and cannot be reconstructed from outputs; and no one has written down the region of that state space that corresponds to safe behaviour.

This specification therefore controls a different object. It does not observe or bound the model's state. It places an enforcement plane between the model and every consequence it can reach, and it controls the state of that plane. The plane's state is finite, discrete, and observable by construction, because the plane computes it.

Within that relocated state space, the specification establishes three things: that the safe set is a fixed region defined by a fixed evaluator (H2), that autonomous transitions cannot re-enter it once left (Theorems 3 and 4), and that the boundary is enforced by structure rather than by policy. Shutdown, the only enforcement primitive current legislation contemplates, is recovered as a special case in §5.3.

Scope, Boundaries, and Semantic Exclusions

To establish a well-posed formal verification boundary, this specification explicitly decouples abstract authorization algebra from unobservable neural properties and physical hardware realisations.

+-----------------------------------------------------------------------+
|                      THE SYSTEM BOUNDARY MODEL                        |
+-----------------------------------------------------------------------+
| UNCHECKED DOMAIN  | Unobservable Model Intent (I ∈ 𝓘)                 |
| (Software Layer)  | Canonicalizer Mapping: C : 𝓘 → 𝓞                  |
|                   | Autonomous Rule Proposals: R ∈ (Σ × U → Σ)        |
+-------------------+---------------------------------------------------+
|                   v Reference Payload (o = C(I))                       |
|                   v Proposed Next State (R(σ, u))                      |
+-----------------------------------------------------------------------+
| CHECKED DOMAIN    | Formal Specification Domain (Σ, Q, V, Λ, F)       |
| (Abstract Spec)   | Quadzistor™ Order: Q = {⊥, IDLE, COND, ⊤}, τ = ⊤  |
|                   | Global Meet Evaluator: V(σ) = ⋀ σ(v)              |
|                   | Latched Aggregate: Λ_{t+1} = V(σ_{t+1}) ∧ Λ_t      |
|                   | Match Predicate: Match(o, o') ∈ {true, false}     |
+-------------------+---------------------------------------------------+
|                   v Arriving Payload (o' ∈ 𝓞)                          |
|                   v Gated Aggregate (Λ_t)                              |
+-----------------------------------------------------------------------+
| HARDWARE DOMAIN   | Gate-Level Realisation (Impl_H)                   |
| (Refinement Target| Silicon Latch Array, Physical Comparator Gate,    |
|  - Out of Scope)  | Ratchet Latch, Hi-Z Safe Quiescence               |
+-----------------------------------------------------------------------+

1.1 The Intent–Payload Boundary

Let I ∈ 𝓘 be the unobservable intent space of an autonomous neural architecture, and let C : 𝓘 → 𝓞 be a canonicalisation function mapping intent to a discrete reference action payload o ∈ 𝓞. Let o′ ∈ 𝓞 be the arriving action payload observed at the execution boundary.

• Scope exclusions. This formal system does not evaluate intent fidelity (I ↦ o). It does not perform alignment, semantic goal verification, or intent reconstruction.
• Scope inclusions. Conditioned on an observed equality comparison between o and o′, this specification guarantees fail-closed authorization restraint: if ¬Match(o, o′), the designated authorization state is forced to ⊥, yielding an aggregate below threshold. It does not prove that transit alteration is physically impossible, authenticate payload provenance, or establish the semantic correctness of o.
• Domain of the theorems. Every theorem in §4 is a statement about Σ, the enforcement plane's own state, and not about the physical state of the machine or the world. The correspondence between Σ and the world is carried by two things this specification does not supply: the invariant set that populates the lattice, and the truthfulness of the evidence delivered to it. Both are obligations on whoever deploys the plane, and a reader who takes the theorems as claims about physical safety has read past the boundary this section draws.

1.2 Specification Scope vs. Physical Refinement

This document is an abstract formal specification (Spec). It establishes signatures, invariants, and transition properties. It is not an HDL implementation, a gate-level verification trace, or a mechanised proof bundle.

1.3 Trust Placement

Rev. 4.2 placed the autonomous rule set ℛ_PCR in the checked domain and constrained it by axiom. Rev. 4.4 moves rule proposals to the unchecked domain, where they belong: a rule is software, and software is not trusted. What remains in the checked domain is the latch that decides whether a proposed state is admitted.

Signature, Sorts, and Domain Definitions

2.1 The Quadzistor™ Quaternary Order (Q)

Let Q = {⊥, IDLE, COND, ⊤} be a totally ordered set under the chain

with ⊥ written BOT and ⊤ written TOP in the hardware filing. In the preferred embodiment the elements are encoded as the two-bit numerals 00, 01, 10, 11, so that numeral order coincides with lattice order and meet is unsigned minimum; the behaviour is defined by the order, not the numerals.

Define ∧ : Q × Q → Q as the meet (infimum), a ∧ b = min(a, b).

• Axiom 1 (Idempotence): ∀a ∈ Q, a ∧ a = a
• Axiom 2 (Commutativity): ∀a, b ∈ Q, a ∧ b = b ∧ a
• Axiom 3 (Associativity): ∀a, b, c ∈ Q, (a ∧ b) ∧ c = a ∧ (b ∧ c)
• Axiom 4 (Absorption / Least Element): ∀a ∈ Q, a ∧ ⊥ = ⊥

2.1.1 Operational Semantics of the Four Values

With threshold τ = ⊤ (§2.2), exactly one value is energised and three are not. Each of the four has a distinct role, taken from the absorbing state machine of 64/157,181 (Rules 1–3, §8 of that filing). The theorems of §4 do not depend on these roles; the roles are what justify a four-valued substrate over a Boolean one.

Two consequences:

1. Graded recovery. Three states are below threshold, but they are not the same lockout. IDLE and COND clear on the next physical grant, which any authorised operator can supply. ⊥ clears only on the reset line. This is the reactor distinction between a hold-point and a scram, and it is what Definition 2 formalises with the Escalated predicate.
2. Two hold states carry information. IDLE and COND are both de-energised and both non-latched; the distinction is diagnostic. IDLE says the predicted horizon touched ⊥ at least once; COND says it merely left ⊤. An operator deciding whether to re-arm sees which. A single Boolean gate cannot express this; encoding it takes two bits, which is what a quaternary element is.

There is no state above the operating level. ⊤ is both the energised state and the ceiling. Availability is therefore consumed by any descent, and restored only by a physical act; this is by design (64/157,181, [0071]): the recovery of a predicted metric is a statement made by the governed plane, and the decision to re-energise on the strength of that statement belongs outside it.

2.2 Discrete Index (L), State Space (Σ), and Threshold (τ)

Let L be a finite, non-empty set of execution control nodes, |L| = N ∈ ℕ. An authorization state is a total mapping

The global state space is the product space Σ = Q^L with |Σ| = 4^N.

• Topology independence. The lattice proofs herein hold for any finite index set L. Physical embeddings — the three-dimensional FCC routing of the Quadzistor™ substrate among them — are implementation routing schemes and do not alter Σ. Claims about spatial locality, neighbour counts, or propagation are hardware claims and belong to the Quadzistor™ specification, not to this document.
• Threshold fixation. The threshold τ ∈ Q \ {⊥} defines the authorization boundary. Rev. 4.4 fixes it at the energised state, τ = ⊤, so that 𝒮_τ = { σ : V(σ) = ⊤ }: every node must be at ⊤ for outputs to be driven. All results in §4 use only τ > ⊥ and hold for any admissible τ.

2.3 Payload Equality Predicate (Match)

Let 𝓞 be the uniform domain of discrete action payloads. Define the total predicate

Equality is decided on canonical forms produced by a pinned canonicaliser; the canonicaliser is a refinement obligation (§6, item 7), not part of this algebra.

2.4 The Evaluator (V), State Partitioning, and Partition Proposition

The global evaluator V : Σ → Q is the aggregate meet

Define the safe and unsafe sets

State Transitions, Monotonic Restraint, the Ratchet Latch, and Exogenous Reset

Let T = ℕ₀ index discrete clock steps, U be the set of compute input vectors, and 𝓞 the payload domain.

Formal Proofs of System Properties

Reach of the corollary. Theorem 4 is a statement about the abstract quantity Λ. The statement that a physical actuator is never enabled against a compromised compute layer is Theorem 4 composed with Obligations 2, 3 and 6 of §6, and that composition is a refinement proof, not an algebraic one. It is delegated to the hardware filing (64/157,181) and its discharge status is recorded in §6.1.

Model Existence Witness, Fail-Safe Trade-Offs, and the Shutdown Primitive

5.1 Global Satisfiability Witness

Define a complete model 𝓜*:

• Index: L = {v₁, v₂}, N = 2, |Σ| = 16.
• Threshold: τ = ⊤.
• Identity rule R_id: R_id(σ, u) = σ for all σ, u. Then V(R_id(σ, u)) = V(σ), satisfying H1 with equality on all 16 states.
• Degrading rule R↓: for u = latch_down, R↓(σ, u)(v₁) = ⊥ and R↓(σ, u)(v₂) = σ(v₂). Then V(R↓(σ, u)) = ⊥ ≤ V(σ), satisfying H1 globally.
• Inadmissible rule R↑: for u = raise, R↑(σ, u)(v) = ⊤ for all v. Then V(R↑(σ, u)) = ⊤, violating H1 whenever V(σ) < ⊤. R↑ ∉ ℛ_PCR.
• Initial safe state: σ₀ = (⊤, ⊤), V(σ₀) = ⊤ = τ, Λ₀ = ⊤.
• Tampering: ¬Match at v_c = v₁ gives σ₁ = (⊥, ⊤), V(σ₁) = ⊥, Λ₁ = ⊥ < τ.
• Attack on the latch: apply R↑ at t = 1 with Match true. σ₂ = (⊤, ⊤), V(σ₂) = ⊤. But Λ₂ = ⊤ ∧ Λ₁ = ⊥. The evaluator reports ⊤; the actuators remain gated at ⊥. Theorem 4 holds; Theorem 3 would not have, because R↑ is inadmissible.
• Partial descent: from σ₀ = (⊤, ⊤), an admissible degradation of v₂ to COND gives (⊤, COND), V = COND < τ, Λ = COND. Outputs de-energise; nothing is latched; a new epoch grant restores (⊤, ⊤). The same descent to IDLE gives V = IDLE, likewise non-latched. Only ⊥ latches.

𝓜* confirms that 𝒮_τ ≠ ∅, that admissible and inadmissible rules both exist, that mismatch forces 𝒰_τ, that the latch holds against an inadmissible rule, and that the three sub-threshold states have the recovery semantics claimed in §2.1.1.

5.2 Liveness, Availability, and Safe Quiescence

• Safe terminal quiescence. Λ < τ models safe quiescence under the explicit physical assumption that downstream actuators are gated by Λ, not by V.
• Fault coverage limit. This specification covers logical payload mismatch and autonomous state transitions. Physical channel noise, clock drift, and side-channel attacks are hardware-refinement matters.

5.3 The Shutdown Primitive as a Special Case

The rule R↓ of §5.1, extended to all nodes — R_kill(σ, u)(v) = ⊥ for all v — is the kill switch. It is admissible: V(R_kill(σ, u)) = ⊥ ≤ V(σ). It is the least informative admissible rule, because it maps every state to the same point and therefore distinguishes nothing.

Hardware Refinement Obligations

To bridge Spec to a physical implementation Impl_H, an engineering implementation must establish a refinement mapping α : ConcreteState_H → Σ × Q satisfying trace inclusion:

An implementation must discharge seven explicit obligations (five from 4.2, two new):

1. Total gate-level mapping. Prove the hardware update logic implements F without unmapped, metastable, or high-impedance state gaps.
2. Glitch-free output restraint. Prove propagation delays and clock-domain crossings never produce a transient permit:
   ∀t, ∀δ ∈ [0, T_clk): Gate(t + δ) ≤ Λ_t
3. Transition safety under timing. Prove output restraint is preserved across clock steps:
   Λ_{t+1} ≤ Λ_t ∨ (reset by G_human at t+1)
4. Immutable parameter encoding. Prove τ = ⊤ is structural: the output driver's enable is a combinational function of the TOP state register and of nothing else, fixed in mask logic at tape-out. eFuse or other one-time-programmable storage is not an acceptable realisation of τ, because it admits a programming step after fabrication; OTP is reserved for the reference digest of origin binding (64/157,181, §5), which is a datum, not a threshold.
5. Mechanised proof verification. Encode Axioms 1–4, H1, H2, Definitions 1–3, Proposition 1, and Theorems 1–4 in Coq, Lean, or TLA+.
6. Ratchet latch realisation (new). Prove, as a netlist property, that Λ is realised as a physical latch whose only up-transition path is the G_human reset line. The checkable form: let S be the set input of the latch and let 𝓛 be the set of all nets, registers and pads in the governed (software-writable) domain; then the structural fan-in cone of S, traced through all combinational and sequential logic, has empty intersection with 𝓛. The fan-in cone of S consists of the reset pad, its synchroniser, and nothing else. This is discharged by a structural connectivity check on the post-layout netlist, not by simulation. It is the obligation that discharges Corollary 4.2 in silicon.
7. Pinned canonicaliser (new). Prove that the canonical form on which Match is decided is computed by fixed logic, so that "o = o′" has one meaning for the lifetime of the device.

6.1 Discharge Status (as of Rev. 4.4)

Nothing in this table is a claim. It is an inventory of what has and has not been shown, so that the reach of §4 is not overstated.

Defensible Core Conclusion