corpus/doctrine/docs-site__docs__doctrine__puriq.md

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

$$P(x,t)=\underset{a\in \mathcal{A}}{\mathrm{arg\hspace{0.17em}max}}[\mathrm{\Lambda }(x)\cdot {\mathrm{Y}\mathrm{u}\mathrm{y}\mathrm{a}\mathrm{y}}_{13}(a)\cdot \exp \text{\hspace{0.17em}⁣}(-\beta \cdot \mathrm{H}\mathrm{U}\mathrm{K}\mathrm{L}\mathrm{L}\mathrm{A}(a))\cdot {\prod }_i{\mathrm{K}\mathrm{h}\mathrm{i}\mathrm{p}\mathrm{u}}_i(a)]\mathrm{.}P(x,t)\; =\; \backslash operatorname*\{arg\backslash ,max\}\_\{a\; \backslash in\; \backslash mathcal\{A\}\}\; \backslash Big[\backslash ;\; \backslash Lambda(x)\backslash cdot\; \backslash mathrm\{Yuyay\}\_\{13\}(a)\backslash cdot\; \backslash exp\backslash !\backslash big(-\backslash beta\backslash cdot\backslash mathrm\{HUKLLA\}(a)\backslash big)\backslash cdot\; \backslash textstyle\backslash prod\_i\; \backslash mathrm\{Khipu\}\_i(a)\backslash ;\backslash Big].$$

We call the bracketed scalar the Puriq utility of action a:

$$U(a\mid x):=\mathrm{\Lambda }(x)\cdot {\mathrm{Y}\mathrm{u}\mathrm{y}\mathrm{a}\mathrm{y}}_{13}(a)\cdot e^{-\beta \mathrm{H}\mathrm{U}\mathrm{K}\mathrm{L}\mathrm{L}\mathrm{A}(a)}\cdot \prod _{i=1}^m{\mathrm{K}\mathrm{h}\mathrm{i}\mathrm{p}\mathrm{u}}_i(a),P(x,t)=\underset{a\in \mathcal{A}}{\mathrm{arg\hspace{0.17em}max}}U(a\mid x)\mathrm{.}U(a\backslash mid\; x)\; :=\; \backslash Lambda(x)\backslash cdot\backslash mathrm\{Yuyay\}\_\{13\}(a)\backslash cdot\; e^\{-\backslash beta\backslash ,\backslash mathrm\{HUKLLA\}(a)\}\backslash cdot\backslash prod\_\{i=1\}^\{m\}\backslash mathrm\{Khipu\}\_i(a),\backslash qquad\; P(x,t)=\backslash operatorname*\{arg\backslash ,max\}\_\{a\backslash in\backslash mathcal\{A\}\}\; U(a\backslash 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)<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 $\Lambda(x)$; since $U(a\mid x)$ is $\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(a\mid x)>0$ implies $\prod_i \mathrm{Khipu}_i(a)=1$. Contrapositive: any failed receipt forces $U=0$, so a provenance-broken action can never be selected over a verified one. (Lean: puriq_khipu_integrity.)

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

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

SF	Organ	Extra factor	Anchor
SF-01 {#sf-01}	Yuyaq — cortex	$e^{-\gamma\mathrm{KL}}$ drift penalty	Pinsker / DPI
SF-02 {#sf-02}	Yuyay — heart	identity (the gate)	13-axis AND
SF-03 {#sf-03}	Yawar — blood	$C(a)$ chain-link	SHA-256 chain
SF-04 {#sf-04}	Hukulla — immune	$e^{-\beta H}$, $\beta\gg0$	Egyptian doubling
SF-05 {#sf-05}	Kallpa — wires	$B(a)$ Butler–Volmer budget	electrochemistry
SF-06 {#sf-06}	Khipu — DAG	Merkle / sum invariant	khipu sum-of-sums
SF-07 {#sf-07}	Lambda — spine	$\Lambda(x)$ geometric mean	A1–A4
SF-08 {#sf-08}	OTel — nerves	$O(a)$ trace-continuity	W3C trace-context
SF-09 {#sf-09}	Kanchay — brand	$K(a)$ sacred-axis	T01/T02
SF-10 {#sf-10}	Hatun — doctrine	$D(a)$ additivity	HR-3 / HR-7
SF-11 {#sf-11}	Sumaq — designer	$S(a)$ honest-proof	status tags
SF-12 {#sf-12}	Killinchu — bridge	$G(a)$ 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); $\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.