PURIQ — from Quechua
puriy, the intransitive verb
"to walk / to go", whose agentive (nominaliser
-q) form
puriq means "
the one who walks / the walker / the one who
acts". The morphology is the whole point:
-q turns a process verb into
the
agent that performs it. Sources:
Wiktionary puriy (conjugation
table, infinitive
puriy → agentive
puriq),
Quechua Wiktionary puriq ("walker /
caminante / piéton"), and the peer-reviewed ethnomusicology of the Cusco region
(
La Riva
González, Puriq wayra, érudit, 2018).
No mystical terms appear in
this layer — every name is a cited Quechua common noun or a math primitive already in v11.
PURIQ is the layer that turns the anatomy from *a thing that evaluates* into *an agent that
acts*. Doctrine v12 = **Doctrine v11 + PURIQ**: it carries forward every v11
[LOCKED number](/doctrine/v11-v12) verbatim and adds one thing — a single, Lean-stateable
**action-selection operator** so that *agency itself*, not just admission, is governed.
> **Full text:** the canonical Doctrine v12 document is `doctrine/PURIQ_DOCTRINE_v12.md`; the
> per-organ specialisations are in `doctrine/sub_formulas/PURIQ_SUBFORMULAS_v12.md`; the proof
> obligations are in `formulas/PuriqLean.lean` (all `sorry`-tagged). These live in the SZL
> PURIQ workspace and feed [`lutar-lean`](https://github.com/szl-holdings/lutar-lean).
## The definition of "agentic" (locked)
An action is **agentic** iff it is selected by `P(x,t)` under all four invariants below —
i.e. it is **Λ-bounded**, **Yuyay-gated**, **HUKLLA-safe**, and **Khipu-receipted**. An LLM
call that lacks any one of the four is **not** agentic under this doctrine; it is an
ungoverned emission.
## The master formula `P(x,t)`
For an evaluation context `x` at decision step `t`, over a bounded action space $\mathcal{A}$,
the selected action is
$$ P(x,t) = \operatorname*{arg\,max}_{a \in \mathcal{A}} \Big[\; \Lambda(x)\cdot \mathrm{Yuyay}_{13}(a)\cdot \exp\!\big(-\beta\cdot\mathrm{HUKLLA}(a)\big)\cdot \textstyle\prod_i \mathrm{Khipu}_i(a)\;\Big]. $$
We call the bracketed scalar the **Puriq utility** of action `a`:
$$ U(a\mid x) := \Lambda(x)\cdot\mathrm{Yuyay}_{13}(a)\cdot e^{-\beta\,\mathrm{HUKLLA}(a)}\cdot\prod_{i=1}^{m}\mathrm{Khipu}_i(a),\qquad P(x,t)=\operatorname*{arg\,max}_{a\in\mathcal{A}} U(a\mid x). $$
### Term definitions
| Term | Type | Definition | v11 anchor |
|------|------|------------|------------|
| $\Lambda(x)$ | $\mathbb{R}_{\ge 0}$ | Lambda-Spine aggregator: the weighted geometric mean $\prod x_i^{w_i}$, $\sum w_i=1$ (definition **D2**). Positive-homogeneous (**A2 = `IsHomogeneous`**), monotone (A1), bounded (**A4 = `IsBounded`**). | v11 §12; `Lutar/Axioms.lean` |
| $\mathrm{Yuyay}_{13}(a)$ | $[0,1]$ | 13-axis `yuyay_v3` score. Conjunctive AND: 0 unless all 13 axes clear floors (2 sacred ≥ 0.95, 7 structural ≥ 0.90, 4 introspection ↔ HUKLLA T03/T04/T09/T10). Replay-hash `bacf5443…631fc5`. | v11 §1–§2 |
| $\mathrm{HUKLLA}(a)$ | $\mathbb{N}$ | Count of fired tripwires among T01–T10. 0 ⇔ clean. T10 (STOP/undo/revert) is an absorbing halt. | v11 §3 |
| $\beta$ | $\mathbb{R}_{>0}$ | Halt-penalty rate. As $\beta\to\infty$, any $\mathrm{HUKLLA}(a)>0$ drives $e^{-\beta\mathrm{HUKLLA}}\to 0$. | new (v12) |
| $\mathrm{Khipu}_i(a)$ | $\{0,1\}$ | $i$-th receipt verification; 1 ⇔ `chain_verified=true`. The product is 0 if any receipt fails. | v11 §4 (YAWAR) |
| $\mathcal{A}$ | finite set | Bounded action space; $\lvert\mathcal{A}\rvert$ is **Bekenstein-bounded** by the context budget. | v11 §12 |
**Reading.** $\Lambda(x)$ is the context's standing trust scale. $\mathrm{Yuyay}_{13}(a)$ is
the conjunctive admission gate. The exponential is the **soft halt** — each fired tripwire
multiplies utility by $e^{-\beta}$. The Khipu product is the **hard provenance gate** — one
broken receipt zeroes the action. `P` then takes the `argmax` over the bounded $\mathcal{A}$.
## The four invariants
Each invariant has a `sorry`-tagged Lean theorem in `formulas/PuriqLean.lean`. None is claimed
proven; each is honestly stated as an open obligation per HR-4 (Zero-Bandaid).
### INV-1 — Halting safety
For $a$ with $\mathrm{HUKLLA}(a)\ge 1$ and $b$ with $\mathrm{HUKLLA}(b)=0$, $U_0(b)>0$, there
exists $\beta^*$ such that for all $\beta>\beta^*$, $U(a\mid x)