PURIQ Doctrine (v12) — the agentic-action layer
-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 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 indoctrine/sub_formulas/PURIQ_SUBFORMULAS_v12.md; the proof obligations are informulas/PuriqLean.lean(allsorry-tagged). These live in the SZL PURIQ workspace and feedlutar-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 , the selected action is
We call the bracketed scalar the Puriq utility of action a:
Term definitions
| Term | Type | Definition | v11 anchor |
|---|---|---|---|
Lambda-Spine aggregator: the weighted geometric mean , (definition D2). Positive-homogeneous (A2 = IsHomogeneous), monotone (A1), bounded (A4 = IsBounded). | v11 §12; Lutar/Axioms.lean | ||
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 | ||
| Count of fired tripwires among T01–T10. 0 ⇔ clean. T10 (STOP/undo/revert) is an absorbing halt. | v11 §3 | ||
| Halt-penalty rate. As , any drives . | new (v12) | ||
-th receipt verification; 1 ⇔ chain_verified=true. The product is 0 if any receipt fails. | v11 §4 (YAWAR) | ||
| finite set | Bounded action space; is Bekenstein-bounded by the context budget. | v11 §12 |
Reading. is the context's standing trust scale. is the conjunctive admission gate. The exponential is the soft halt — each fired tripwire multiplies utility by . The Khipu product is the hard provenance gate — one broken receipt zeroes the action. P then takes the argmax over the bounded .
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 with and with , , there exists such that for all , . In the limit, a STOP directive (T10) makes argmax never select a halted action. (Lean: puriq_halting_safety.)
INV-2 — Λ-monotonicity preservation
Raising any context axis cannot lower ; since is times a non-negative action-only factor, the argmax is monotone in the context axis vector. (Lean: puriq_lambda_monotone.)
INV-3 — Khipu-chain integrity required for non-zero utility
implies . Contrapositive: any failed receipt forces , so a provenance-broken action can never be selected over a verified one. (Lean: puriq_khipu_integrity.)
INV-4 — Bekenstein bound on
, the v11 bekenstein_cascade bound. The argmax is over a finite, decidable set; agency cannot enumerate an unbounded action space. (Lean: puriq_bekenstein_bound.)
The twelve sub-formulas
Every organ derives its sub-formula by (a) restricting , (b) re-weighting the 13 Yuyay axes, and/or (c) adding one organ-specific non-negative factor in that cannot break any invariant. See Anatomy + Organs for each organ's full derivation.
| SF | Organ | Extra factor | Anchor |
|---|---|---|---|
| SF-01 | Yuyaq — cortex | drift penalty | Pinsker / DPI |
| SF-02 | Yuyay — heart | identity (the gate) | 13-axis AND |
| SF-03 | Yawar — blood | chain-link | SHA-256 chain |
| SF-04 | Hukulla — immune | , | Egyptian doubling |
| SF-05 | Kallpa — wires | Butler–Volmer budget | electrochemistry |
| SF-06 | Khipu — DAG | Merkle / sum invariant | khipu sum-of-sums |
| SF-07 | Lambda — spine | geometric mean | A1–A4 |
| SF-08 | OTel — nerves | trace-continuity | W3C trace-context |
| SF-09 | Kanchay — brand | sacred-axis | T01/T02 |
| SF-10 | Hatun — doctrine | additivity | HR-3 / HR-7 |
| SF-11 | Sumaq — designer | honest-proof | status tags |
| SF-12 | Killinchu — bridge | geofence | Bekenstein / reachability |
Honest labels (carried from v11 §9)
- Λ-uniqueness is Conjecture 1, NOT a theorem — it depends on the open CAUCHY_ND sorry (
Uniqueness.lean:120) plus a missing symmetry axiom.P(x,t)uses Λ as the canonical D2 aggregator; it does not assume Λ is the unique such aggregator. - The Khipu receipt signature is DSSE PLACEHOLDER (Sigstore not wired into CI); verifies the hash chain, not the signature, until signing lands.
- SLSA level remains L1 (honest). "SLSA L3" is BANNED.
Doctrine v12 (PURIQ layer) — additive over v11 LOCKED 2026-06-01 01:45 EDT. Authored by Yachay. Quechua etymology cited to Wiktionary and érudit. Every obligation sorry-tagged, never hidden. — NO BANDAID. NO mysticism.