Add QuantumArithmetic specification

README.md

@@ -106,6 +106,7 @@ Here is a list of specs included in this repository which are validated by the C
 | [Buffered Random Access File](specifications/braf)                                                  | Calvin Loncaric                                     |          |             |         |     ✔     |          |
 | [Disruptor](specifications/Disruptor)                                                               | Nicholas Schultz-Møller                             |          |             |         |     ✔     |          |
 | [DAG-based Consensus](specifications/dag-consensus)                                                 | Giuliano Losa                                       |          |             |    ✔    |     ✔     |          |
+| [Quantum Arithmetic Axiom System](specifications/QuantumArithmetic)                                 | Will Dale                                           |          |             |         |     ✔     |          |
 
 
 ## Other Examples

specifications/QuantumArithmetic/LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2026 Will Dale
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

specifications/QuantumArithmetic/NOTICE.md

@@ -0,0 +1,51 @@
+Attribution Notice
+------------------
+
+This package is extracted from the `signal_experiments` monorepo (Will
+Dale, 2026) for submission to `github.com/tlaplus/examples`. The TLA+
+logic (generator algebra, axiom invariants, non-vacuity specs) is
+unchanged from its repo-internal canonical form; only the module
+identifiers and file names were renamed (to `QuantumArithmetic` /
+`QuantumArithmeticAxioms` / `QuantumArithmeticAxioms_negative_*`) to
+match the naming conventions of the upstream `tlaplus/examples` corpus.
+The MIT `LICENSE` in this directory governs use of the package; this
+`NOTICE.md` records the requested citation form.
+
+You may copy and reuse this construction and the accompanying TLC
+configurations for research or teaching.
+
+If you publish results that depend on:
+
+  - the QARM generator semantics (sigma, mu, lambda_k with paired
+    failure actions and absorbing-stutter on failure),
+  - the duo-modular qtag packing `qtag = 24*phi9(a) + phi24(a)`,
+  - the observer-layer firewall encoding (`obs_float`,
+    `obs_cross_count`, `Project` action, `Inv_T2_FirewallRespected`,
+    `Inv_NT_NoObserverFeedback`),
+  - the specific invariant set (A1/A2/S1/S2/T1/T2/NT) as named here,
+  - the paired non-vacuity discipline (one negative spec per
+    runtime-checkable invariant, producing a minimal counterexample),
+
+please cite:
+
+  Dale, W. (2026). *Quantum Arithmetic Axiom System as TLA+ Temporal
+  Invariants.* `github.com/tlaplus/examples/specifications/QuantumArithmetic`
+  (extracted from the `signal_experiments` research monorepo).
+
+and preserve:
+
+  - the invariant names (`Inv_A1_NoZero`, etc.),
+  - the observer-layer variable names (`obs_float`, `obs_cross_count`),
+  - the `Project` action signature (writes `obs_cross_count' = 2`,
+    reads `a`).
+
+## References (primary)
+
+- Lamport, L. (1994). *The Temporal Logic of Actions.* ACM TOPLAS 16(3),
+  872-923. DOI: 10.1145/177492.177726.
+- Lamport, L. (2002). *Specifying Systems: The TLA+ Language and Tools
+  for Hardware and Software Engineers.* Addison-Wesley. ISBN
+  978-0-321-14306-8.
+
+These primary references are not subject to this attribution notice and
+should be cited independently per their own terms.

specifications/QuantumArithmetic/QuantumArithmetic.cfg

@@ -0,0 +1,13 @@
+CONSTANTS
+  CAP = 20
+  KSet = {2, 3}
+
+INIT Init
+NEXT Next
+
+INVARIANTS
+  Inv_TupleClosed
+  Inv_InBounds
+  Inv_QDef
+  Inv_FailDomain
+  Inv_MoveDomain

specifications/QuantumArithmetic/QuantumArithmetic.tla

@@ -0,0 +1,249 @@
+------------------------------ MODULE QuantumArithmetic ------------------------------
+EXTENDS Naturals, Integers, TLC
+
+(*
+  QuantumArithmetic.tla — Quantum Arithmetic generator algebra.
+  ------------------------------------------------------------------------
+
+  This module specifies the state machine of the Quantum Arithmetic
+  Reachability Module (QARM): a discrete system over pairs (b, e) with
+  derived coordinates d = b + e, a = b + 2e (equivalently a = d + e), a
+  duo-modular invariant qtag = 24*phi9(a) + phi24(a) \in [0, 239], and
+  three generator actions:
+
+    sigma  : e -> e + 1                            (e-growth)
+    mu     : swap b <-> e                          (coordinate swap)
+    lambda : (b, e) -> (k*b, k*e) for k in KSet    (scaling)
+
+  Each generator is paired with explicit failure actions — OUT_OF_BOUNDS
+  when the successor tuple would exceed CAP, FIXED_Q_VIOLATION when the
+  successor would break duo-modular invariance. Failure states are
+  absorbing: once fail /= "OK", the tuple is frozen.
+
+  This file restricts Init to b, e \in 1..CAP (rather than 0..CAP), so
+  QA Axiom A1 (No-Zero) holds structurally over the reachable state
+  graph. See README.md and the sibling module QuantumArithmeticAxioms.tla
+  for the full axiom set.
+
+  Primary references:
+    - Lamport, L. (1994). The Temporal Logic of Actions. ACM TOPLAS 16(3),
+      872-923. DOI: 10.1145/177492.177726.
+    - Lamport, L. (2002). Specifying Systems: The TLA+ Language and Tools
+      for Hardware and Software Engineers. Addison-Wesley.
+      ISBN 978-0-321-14306-8.
+
+  TLC requirements:
+    - CAP finite (e.g. 20..50)
+    - KSet finite (e.g. {2, 3})
+
+  See QuantumArithmetic.cfg for the standard bounded model.
+*)
+
+CONSTANTS
+  CAP,          \* bound on b,e,d,a
+  KSet          \* finite set of scaling factors for lambda (e.g. {2,3})
+
+VARIABLES
+  b, e, d, a,
+  qtag,
+  fail,         \* {"OK","OUT_OF_BOUNDS","FIXED_Q_VIOLATION","ILLEGAL"}
+  lastMove      \* {"NONE","σ","μ","λ"}
+
+(*** Helpers ***)
+
+InCap(x) == x \in 0..CAP
+
+DR(n) ==
+  IF n = 0 THEN 0 ELSE 1 + ((n - 1) % 9)
+
+Phi24(n) == n % 24
+Phi9(n)  == DR(n)
+
+QDef(bv, ev, dv, av) == 24 * Phi9(av) + Phi24(av)
+
+TupleClosed(bv, ev, dv, av) ==
+  /\ bv \in Nat /\ ev \in Nat /\ dv \in Nat /\ av \in Nat
+  /\ dv = bv + ev
+  /\ av = dv + ev
+
+InBounds(bv, ev, dv, av) ==
+  /\ InCap(bv) /\ InCap(ev) /\ InCap(dv) /\ InCap(av)
+
+StateOK ==
+  /\ TupleClosed(b, e, d, a)
+  /\ InBounds(b, e, d, a)
+  /\ qtag = QDef(b, e, d, a)
+  /\ fail \in {"OK","OUT_OF_BOUNDS","FIXED_Q_VIOLATION","ILLEGAL"}
+  /\ lastMove \in {"NONE","σ","μ","λ"}
+
+(*** Init — A1-corrected: b, e \in 1..CAP (not 0..CAP) ***)
+
+Init ==
+  /\ b \in 1..CAP             \* A1: No-Zero.
+  /\ e \in 1..CAP             \* A1: No-Zero.
+  /\ d = b + e
+  /\ a = d + e
+  /\ TupleClosed(b, e, d, a)
+  /\ InBounds(b, e, d, a)
+  /\ qtag = QDef(b, e, d, a)
+  /\ fail = "OK"
+  /\ lastMove = "NONE"
+
+(*** Move actions — generator algebra ***)
+
+(*** σ : growth on e by +1; close tuple canonically ***)
+
+SigmaSucc ==
+  LET e2 == e + 1 IN
+  LET b2 == b IN
+  LET d2 == b2 + e2 IN
+  LET a2 == d2 + e2 IN
+  /\ fail = "OK"
+  /\ InBounds(b2, e2, d2, a2)
+  /\ QDef(b2, e2, d2, a2) = qtag
+  /\ b' = b2 /\ e' = e2 /\ d' = d2 /\ a' = a2
+  /\ qtag' = qtag
+  /\ fail' = "OK"
+  /\ lastMove' = "σ"
+
+SigmaFail_OUT_OF_BOUNDS ==
+  LET e2 == e + 1 IN
+  LET b2 == b IN
+  LET d2 == b2 + e2 IN
+  LET a2 == d2 + e2 IN
+  /\ fail = "OK"
+  /\ ~InBounds(b2, e2, d2, a2)
+  /\ UNCHANGED <<b,e,d,a,qtag>>
+  /\ fail' = "OUT_OF_BOUNDS"
+  /\ lastMove' = "σ"
+
+SigmaFail_FIXED_Q ==
+  LET e2 == e + 1 IN
+  LET b2 == b IN
+  LET d2 == b2 + e2 IN
+  LET a2 == d2 + e2 IN
+  /\ fail = "OK"
+  /\ InBounds(b2, e2, d2, a2)
+  /\ QDef(b2, e2, d2, a2) # qtag
+  /\ UNCHANGED <<b,e,d,a,qtag>>
+  /\ fail' = "FIXED_Q_VIOLATION"
+  /\ lastMove' = "σ"
+
+Sigma ==
+  SigmaSucc \/ SigmaFail_OUT_OF_BOUNDS \/ SigmaFail_FIXED_Q
+
+
+(*** μ : swap b <-> e; close tuple canonically ***)
+
+MuSucc ==
+  LET b2 == e IN
+  LET e2 == b IN
+  LET d2 == b2 + e2 IN
+  LET a2 == d2 + e2 IN
+  /\ fail = "OK"
+  /\ InBounds(b2, e2, d2, a2)
+  /\ QDef(b2, e2, d2, a2) = qtag
+  /\ b' = b2 /\ e' = e2 /\ d' = d2 /\ a' = a2
+  /\ qtag' = qtag
+  /\ fail' = "OK"
+  /\ lastMove' = "μ"
+
+MuFail_OUT_OF_BOUNDS ==
+  LET b2 == e IN
+  LET e2 == b IN
+  LET d2 == b2 + e2 IN
+  LET a2 == d2 + e2 IN
+  /\ fail = "OK"
+  /\ ~InBounds(b2, e2, d2, a2)
+  /\ UNCHANGED <<b,e,d,a,qtag>>
+  /\ fail' = "OUT_OF_BOUNDS"
+  /\ lastMove' = "μ"
+
+MuFail_FIXED_Q ==
+  LET b2 == e IN
+  LET e2 == b IN
+  LET d2 == b2 + e2 IN
+  LET a2 == d2 + e2 IN
+  /\ fail = "OK"
+  /\ InBounds(b2, e2, d2, a2)
+  /\ QDef(b2, e2, d2, a2) # qtag
+  /\ UNCHANGED <<b,e,d,a,qtag>>
+  /\ fail' = "FIXED_Q_VIOLATION"
+  /\ lastMove' = "μ"
+
+Mu ==
+  MuSucc \/ MuFail_OUT_OF_BOUNDS \/ MuFail_FIXED_Q
+
+
+(*** λ_k : scale (b,e) by k; close tuple canonically ***)
+
+LambdaSucc ==
+  \E k \in KSet :
+    LET b2 == k * b IN
+    LET e2 == k * e IN
+    LET d2 == b2 + e2 IN
+    LET a2 == d2 + e2 IN
+    /\ fail = "OK"
+    /\ InBounds(b2, e2, d2, a2)
+    /\ QDef(b2, e2, d2, a2) = qtag
+    /\ b' = b2 /\ e' = e2 /\ d' = d2 /\ a' = a2
+    /\ qtag' = qtag
+    /\ fail' = "OK"
+    /\ lastMove' = "λ"
+
+LambdaFail_OUT_OF_BOUNDS ==
+  \E k \in KSet :
+    LET b2 == k * b IN
+    LET e2 == k * e IN
+    LET d2 == b2 + e2 IN
+    LET a2 == d2 + e2 IN
+    /\ fail = "OK"
+    /\ ~InBounds(b2, e2, d2, a2)
+    /\ UNCHANGED <<b,e,d,a,qtag>>
+    /\ fail' = "OUT_OF_BOUNDS"
+    /\ lastMove' = "λ"
+
+LambdaFail_FIXED_Q ==
+  \E k \in KSet :
+    LET b2 == k * b IN
+    LET e2 == k * e IN
+    LET d2 == b2 + e2 IN
+    LET a2 == d2 + e2 IN
+    /\ fail = "OK"
+    /\ InBounds(b2, e2, d2, a2)
+    /\ QDef(b2, e2, d2, a2) # qtag
+    /\ UNCHANGED <<b,e,d,a,qtag>>
+    /\ fail' = "FIXED_Q_VIOLATION"
+    /\ lastMove' = "λ"
+
+Lambda ==
+  LambdaSucc \/ LambdaFail_OUT_OF_BOUNDS \/ LambdaFail_FIXED_Q
+
+
+(*** Global Next ***************************************************************)
+
+Next ==
+  \/ Sigma
+  \/ Mu
+  \/ Lambda
+  \/ /\ fail # "OK" /\ UNCHANGED <<b,e,d,a,qtag,fail,lastMove>>
+     \* absorbing stutter once failure recorded (keeps failure states distinct)
+
+Spec ==
+  Init /\ [][Next]_<<b,e,d,a,qtag,fail,lastMove>>
+
+(*** Invariants ****************************************************************)
+
+Inv_TupleClosed == TupleClosed(b,e,d,a)
+Inv_InBounds    == InBounds(b,e,d,a)
+Inv_QDef        == qtag = QDef(b,e,d,a)
+Inv_FailDomain  == fail \in {"OK","OUT_OF_BOUNDS","FIXED_Q_VIOLATION","ILLEGAL"}
+Inv_MoveDomain  == lastMove \in {"NONE","σ","μ","λ"}
+
+THEOREM Spec => []Inv_TupleClosed
+THEOREM Spec => []Inv_InBounds
+THEOREM Spec => []Inv_QDef
+THEOREM Spec => []Inv_FailDomain
+THEOREM Spec => []Inv_MoveDomain
+
+===============================================================================

specifications/QuantumArithmetic/QuantumArithmeticAxioms.cfg

@@ -0,0 +1,15 @@
+CONSTANTS
+  CAP = 20
+  KSet = {2, 3}
+
+INIT Init_ext
+NEXT Next_ext
+
+INVARIANTS
+  Inv_A1_NoZero
+  Inv_A2_DerivedCoords
+  Inv_S1_NoSquareOperator
+  Inv_S2_IntegerState
+  Inv_T1_IntegerPathTime
+  Inv_T2_FirewallRespected
+  Inv_NT_NoObserverFeedback