a11oy Operator - receipt orchestration

Status: Operator is documented as an a11oy in-process capability and frontier receipt role. It is not claimed as a separately deployed public service; see Runtime status.

Overview

a11oy Operator documents a Khipu-indexed receipt-DAG model: a three-tier pendant-cord tree that represents governance decisions with a summation invariant and an optional dual-attestation field. The source contains a CSS ingress module and receipt-DAG implementation. This is an implementation and design description, not a claim that every public receipt is currently signed or that an independent Operator runtime is live.

The role maps to the Khipu organ and is related to Yawar. Signature status is governed by Compliance and must be checked on the exact artifact.

The summation invariant

The receipt model uses the arithmetic relationship:

$$\text{rootValue} \;=\; \sum \text{pendantValues} \;=\; \sum \sum \text{decisionValues}.$$

The site links the relevant Lean file, Lutar/Khipu/SummationInvariant.lean, as proof evidence. The overall formal-methods posture remains MIXED; read the Evidence index and Proof rather than extrapolating a single invariant into a system-wide guarantee.

Source and evidence

• Role status: ROADMAP as a standalone service; documented in-process receipt capability.
• Source: a11oy
• Proof reference: Lutar/Khipu/SummationInvariant.lean in lutar-lean
• Signature posture: Compliance and the exact receipt artifact are authoritative.
• 3D showcase: screenshots only; not deployed
• Thesis v18 reference (not a software/product DOI): 10.5281/zenodo.20434276