This is not a résumé. It is the inside of the workshop. Everything below runs:
the formula computes, the theorem re-checks in a kernel, and your visit just minted a receipt
in the same Khipu chain the work is about.
org map · live mesh · 3D
The five organs, wired live
An interactive 3D chord map of the SZL mesh. Five organ nodes, the Wire D/E/F/G traces that
carry receipts between them, and a heartbeat pulse driven by each organ's /healthz
(polled every 5 seconds). Drag to rotate; tap a node to open its Space.
Wire D/E/F/G are the real inter-organ receipt traces. Health badges read each organ's live /healthz from this device; when an organ is unreachable from your network the badge shows “—”.
today · auto-pulled
What I shipped most recently
latest commit
loading from GitHub…
this morning's thought
PURIQ — the agentic layer — only ships once the 13-axis Yuyay gate
and the HUKLLA tripwire penalty are both Lean-stateable. A thought that can't be stated as a
proof obligation isn't done; it's a draft wearing a suit.
P1 hook: this line will be machine-pulled from the private journal repo (feature #5).
what I built · last 10 commits
The work, as it lands
The ten most recent commits across the szl-holdings
organization, pulled live from the public GitHub API — no auth, no cache.
loading recent commits from GitHub…
receipts · live counter
Signed receipts, minted across the mesh
Every governed action emits a signed Khipu receipt. This counter sums the
*_receipts_total metric from each organ's /metrics endpoint, live.
The chain is append-only and Reed-Solomon coded on disk — error-correcting parity, not magic.
…
summing live from organ /metrics endpoints…
thesis · ouroboros v20
The Ouroboros Thesis
The argument: a system can carry its own proof of trustworthiness as a verifiable artifact,
so that every act it takes leaves a checkable receipt. The PDF is below; each theorem in it has a
machine-checkable obligation.
P1 hook: HTML thesis where every theorem is clickable → shows its Lean code (feature #6). Theorem heads already wired to the kernel below.
formula · live calculator
PURIQ Master Formula
The agentic decision rule. Move the sliders — the per-action score recomputes live. Break the
Khipu chain (set provenance to 0) and the score is forced to zero: provenance is not optional.
Drag (or tap) up to four primitives onto the bench. The page composes them with a real symbolic
algebra into a new objective, renders the LaTeX, names the resulting law — then hands the obligation
to the Lean kernel below.
Λ-Spine homogeneous aggregator
Yuyay-13 13-axis wisdom
Noether conserved quantity
Shannon information
Khipu provenance
Bekenstein action bound
—
theorem of the week · lutar-lean
Halting safety holds
One proved theorem, re-checked in a lutar-lean-lite kernel running in a Web Worker
(real CPU, off the main thread). Edit-and-recheck: add sorry and watch the badge flip.
-- lutar-lean · doctrine v11 · halting safety
theorem huklla_penalty_collapses
(a : Action) (beta : Real) (h : HUKLLA a > 0) (hb : beta > 3) :
puriq_score a < epsilon := by
-- large beta with any tripwire drives exp(-beta*HUKLLA) below epsilon
have hp : Real.exp (-beta * HUKLLA a) < epsilon := by
apply exp_neg_lt ; positivity
calc puriq_score a = lambda * yuyay * Real.exp (-beta * HUKLLA a) * khipu := rfl
_ < epsilon := by nlinarith [hp]
P1 hook: each Monday auto-pull one PROVED theorem from lutar-lean + plain-English narration via Wallpa voice (feature #2 full / #7).
proof tree · live from lutar-lean
The proofs, as a tree
Each node is a real theorem or lemma in
szl-holdings/lutar-lean.
The page fetches the live Lean source, checks each declaration's body for an open
sorry, and renders proven nodes in gold. Click any node to jump to its exact line.
doctrine · v11 LOCKED · v12/v13 in flight
The doctrine, by the numbers
These are not marketing figures. They are the locked counts from the v11 replay — the same numbers
the 3D khipu below knots into its cords.
The doctrine as a khipu — drag to rotate, click to enter
loading 3D khipu…
how it works · architecture
How the mesh actually works
No mysticism — just an event-sourced, cryptographically-signed control plane. The Quechua names
are brand naming for the components; the mechanics underneath are standard, auditable systems.
decision
Λ-aggregator + Yuyay-13
Every candidate action is scored by the Λ spine aggregator (a proven homogeneous,
monotone, bounded mean) weighted across the 13 axes of Yuyay-13. The score and its
bounds are Lean-proved in lutar-lean (see the proof tree above).
gate
HUKLLA tripwire
A violation drives e^(-β·HUKLLA) toward zero, collapsing the action's score below
threshold. Provenance is multiplicative: break the Khipu chain and the product is forced to 0.
record
Khipu DAG + Wire D
Each governed act appends a signed receipt to the Khipu directed-acyclic log.
Wire D (and E/F/G) carry receipts between organs. The log is append-only and
event-sourced — a replayable history, not “time travel.”
durability
Reed-Solomon parity
Receipts are stored with Reed-Solomon error-correcting codes so the chain survives disk
corruption. That is coding theory — redundancy and recovery — not anything holographic.
flagships · live status from HF
The fleet
Five flagships, one 3D Space, one org card. Each status badge is polled live from Hugging Face
(with a sovereign offline fallback to last-known stage).
A system can carry its own proof of trustworthiness as a first-class, verifiable
artifact. Every agentic act emits a Khipu receipt; the receipt chain is the audit trail; the audit trail is
Lean-checkable. We formalize the decision rule $P(x,t)=\arg\max_a \Lambda(x)\,Y_{13}(a)\,e^{-\beta H(a)}\prod_i K_i(a)$
and prove halting safety, Λ-monotonicity, and chain-integrity necessity.
