Skip to content

PURIQ Doctrine (v12) — the agentic-action layer

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 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.

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 A\mathcal{A}, the selected action is

P(x,t)=arg maxaA[  Λ(x)Yuyay13(a)exp ⁣(βHUKLLA(a))iKhipui(a)  ].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(ax):=Λ(x)Yuyay13(a)eβHUKLLA(a)i=1mKhipui(a),P(x,t)=arg maxaAU(ax).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

TermTypeDefinitionv11 anchor
Λ(x)\Lambda(x)R0\mathbb{R}_{\ge 0}Lambda-Spine aggregator: the weighted geometric mean xiwi\prod x_i^{w_i}, wi=1\sum w_i=1 (definition D2). Positive-homogeneous (A2 = IsHomogeneous), monotone (A1), bounded (A4 = IsBounded).v11 §12; Lutar/Axioms.lean
Yuyay13(a)\mathrm{Yuyay}_{13}(a)[0,1][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
HUKLLA(a)\mathrm{HUKLLA}(a)N\mathbb{N}Count of fired tripwires among T01–T10. 0 ⇔ clean. T10 (STOP/undo/revert) is an absorbing halt.v11 §3
β\betaR>0\mathbb{R}_{>0}Halt-penalty rate. As β\beta\to\infty, any HUKLLA(a)>0\mathrm{HUKLLA}(a)>0 drives eβHUKLLA0e^{-\beta\mathrm{HUKLLA}}\to 0.new (v12)
Khipui(a)\mathrm{Khipu}_i(a){0,1}\{0,1\}ii-th receipt verification; 1 ⇔ chain_verified=true. The product is 0 if any receipt fails.v11 §4 (YAWAR)
A\mathcal{A}finite setBounded action space; A\lvert\mathcal{A}\rvert is Bekenstein-bounded by the context budget.v11 §12

Reading. Λ(x)\Lambda(x) is the context's standing trust scale. Yuyay13(a)\mathrm{Yuyay}_{13}(a) is the conjunctive admission gate. The exponential is the soft halt — each fired tripwire multiplies utility by eβe^{-\beta}. The Khipu product is the hard provenance gate — one broken receipt zeroes the action. P then takes the argmax over the bounded A\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 aa with HUKLLA(a)1\mathrm{HUKLLA}(a)\ge 1 and bb with HUKLLA(b)=0\mathrm{HUKLLA}(b)=0, U0(b)>0U_0(b)>0, there exists β\beta^* such that for all β>β\beta>\beta^*, U(ax)<U(bx)U(a\mid x)<U(b\mid x). 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 Λ(x)\Lambda(x); since U(ax)U(a\mid x) is Λ(x)\Lambda(x) 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

U(ax)>0U(a\mid x)>0 implies iKhipui(a)=1\prod_i \mathrm{Khipu}_i(a)=1. Contrapositive: any failed receipt forces U=0U=0, so a provenance-broken action can never be selected over a verified one. (Lean: puriq_khipu_integrity.)

INV-4 — Bekenstein bound on A\lvert\mathcal{A}\rvert

ANBek(x)\lvert\mathcal{A}\rvert \le N_{\text{Bek}}(x), 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 A\mathcal{A}, (b) re-weighting the 13 Yuyay axes, and/or (c) adding one organ-specific non-negative factor in [0,1][0,1] that cannot break any invariant. See Anatomy + Organs for each organ's full derivation.

SFOrganExtra factorAnchor
SF-01Yuyaq — cortexeγKLe^{-\gamma\mathrm{KL}} drift penaltyPinsker / DPI
SF-02Yuyay — heartidentity (the gate)13-axis AND
SF-03Yawar — bloodC(a)C(a) chain-linkSHA-256 chain
SF-04Hukulla — immuneeβHe^{-\beta H}, β0\beta\gg0Egyptian doubling
SF-05Kallpa — wiresB(a)B(a) Butler–Volmer budgetelectrochemistry
SF-06Khipu — DAGMerkle / sum invariantkhipu sum-of-sums
SF-07Lambda — spineΛ(x)\Lambda(x) geometric meanA1–A4
SF-08OTel — nervesO(a)O(a) trace-continuityW3C trace-context
SF-09Kanchay — brandK(a)K(a) sacred-axisT01/T02
SF-10Hatun — doctrineD(a)D(a) additivityHR-3 / HR-7
SF-11Sumaq — designerS(a)S(a) honest-proofstatus tags
SF-12Killinchu — bridgeG(a)G(a) geofenceBekenstein / 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); Khipui(a)\mathrm{Khipu}_i(a) 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.

Doctrine v11 LOCKED · 749/14/163 · kernel c7c0ba17 · Λ = Conjecture 1 · SLSA L1 honest. Math-grounded, Quechua-rooted, zero mysticism (PURIQ v12 agentic layer is additive).