Invariant arithmetic isn't a tag-propagation hack. Its
operations form precise algebraic structures: a product of
monoids for combine, a phase-graded category
for chain, idempotent endomorphisms for
reconcile and deliberate. This
document states the laws, tests them on random values until
either they hold or a counterexample falsifies them, and
sketches the typed version that turns the substrate into a
small language.
Each family of invariants gives combine a
different algebraic personality. Most are commutative
monoids — addition for ℝ, OR for κ, min for β, union for σ.
The temporal and governance fields are non-commutative free
monoids (first-non-null wins, or list concatenation). The
whole value space is the product, and a product of monoids
is a monoid. The non-commutative components are why
combine(a, b) ≠ combine(b, a) in general — but
they're also exactly what makes the substrate aware of
order, which it must be.
type Value = { n: ℝ, // + with identity 0, commutative monoid topological: { κ: Bool, // ∨ with identity false, idempotent commutative monoid β: [0, 1] // min with identity 1, idempotent commutative monoid }, spatial: { σ: Set<Tag> // ∪ with identity ∅, idempotent commutative monoid (join-semilattice) }, temporal: { π: Phase | null, // first-non-null monoid, NOT commutative, NOT idempotent ι: IdemKey | null, // first-non-null monoid (same structure) ψ: Cadence | null // first-non-null monoid (same structure) }, governance: { authority_path: List<Cap>, // concat with identity [], free monoid (NOT commutative) deny_default: Bool, // ∧ with identity true, idempotent commutative monoid audit: List<Event> // concat (free monoid) } }
combine : Value × Value → Value componentwise application of each family's monoid op ⇒ non-commutative monoid (because of temporal & governance components) chain : Value × Value → Value // partial defined only when phase(a) ≤ phase(b) in PULSE phase order ⇒ morphism in the phase-graded category PHASE objects: phases {retrieve, route, act, learn, consolidate} morphisms: values tagged with entry/exit phase composition: chain, identity: V(0) with matching phase promote : Value × Evidence → Value β-monotone endomorphism on Value promote(v).β ≥ v.β always reconcile : Value × Set<Tag> → Value σ-antitone, idempotent endomorphism reconcile(v, T).σ = v.σ \ T; reconcile(reconcile(v, T), T) = reconcile(v, T) deliberate : Value × String → Value κ-antitone, idempotent endomorphism deliberate(v).κ = false (regardless of input κ) consume : Value × Requirements → {ok, failures, value} predicate on (Value, Req), not an operation on Value itself ⇒ the substrate's correctness check
If the substrate is a real algebraic system rather than a heuristic, these laws hold. Some are familiar (associativity, identity); some are family-specific (per-component idempotence); some are about composition between operations (promote commutes with combine on β). Below, each law is stated formally, then verified live by the property-test runner in §III.
A tiny QuickCheck-style harness runs each law against randomly generated values. Green = the law holds across the requested number of trials; red surfaces the counterexample so you can read what broke. This is the proof-in-the-pudding pattern: not a proof of correctness, but strong evidence the algebra holds, and a way to instantly catch regressions when the substrate changes.
Runtime checks are the prototype. The "language mechanics" version puts invariants in the type system, so the compiler refuses ill-formed compositions before the program runs. This is a sketch — TypeScript's type system isn't quite expressive enough for everything below (β-min would need full dependent types), but the shape is informative. A Liquid Haskell or Idris implementation could fully enforce this.
A retrieval-augmented question-answering pipeline. Two sources retrieved, an answer generated, the answer reused as context for a follow-up. Without invariant arithmetic, the follow-up confidently echoes a contradiction. With invariant arithmetic, the substrate refuses at the right step — citing which family, which invariant, why. Click run at the bottom to execute the pipeline and see each step's value digest.
The algebraic structure in §I is the substrate's
contract, not a description of one program. The
claim is implementation-independent: any value type exposing
combine, chain,
promote, reconcile,
deliberate, and consume must
satisfy laws L1–L15, and the §III property tests are the
regression suite for every port. Break associativity or
idempotence and the harness falsifies it on the next run.
That contract now has two independent witnesses.
The first is the in-page QuickCheck harness you just ran —
JavaScript, in your browser. The second is a full
Elixir reference implementation
(invariant_arithmetic v0.1.0, in
AmpersandBoxDesign/reference/elixir/): the same
four families and six operations, ported directly from this
page, with laws L1–L14 written as
ExUnitProperties tests and checked against 1000
randomly generated values on every run —
14 properties, 11 tests, 0 failures. It is not a
sketch and not "future work"; it runs on the BEAM, the same
runtime Graphonomous, PRISM, and Delegatic already run on.
Two languages, two random generators, one set of laws holding
in both — that is the cross-implementation conformance that
turns "the JS happens to pass" into "the substrate is real."
The TypeScript in §IV is still a type-level sketch.
It does not fully type-check today (β-min needs dependent
types, σ-union needs effect rows) but its shape is concrete
enough to translate into Liquid Haskell, Idris, or a
refinement-extended TS. The chain example —
where a reversed phase order is a compile error, not
a runtime exception — is what moving the contract from
"property-tested at runtime" to "language mechanics" looks
like. The Elixir port sits in between: chain/2
returns {:error, π-violation} at runtime rather
than refusing at compile time — proof the refusal is real and
executed, not merely aspirational.
The RAG example in §V is still the most consequential piece. Multi-family composition catches a realistic bug: an LLM agent confidently citing a contradiction it created itself, on the second loop, with σ aggregating across retrievals, β downranked by the weakest source, κ raised by self-citation, and π catching the wrong-order operation. No single invariant catches it; together they do — and the same scenario runs against the Elixir implementation unchanged, which is the whole point of a shared contract.
What's still wanted next, in order of leverage: (1) a fully typed implementation in Idris or Liquid Haskell where the compiler — not a generator — discharges the laws (the Elixir port closes the "second-runtime" gap but is still dynamically checked); (2) a categorical statement of the substrate as a small monoidal category with the invariants as natural transformations (gestured at in §I, not yet formal); (3) a deployed-system benchmark showing invariant arithmetic catches bugs in a live agent that ordinary arithmetic misses — the operationally decisive one, and the natural job for PRISM.