corpus/thesis/szl-papers__thesis__v24__main.md

# The Ouroboros Thesis

### Axiom-Free Conditional Uniqueness of the Lutar Invariant: A Machine-Verified Trust Foundation for Governed Agentic AI

**Thesis v24 "Axiom-Free Conditional Uniqueness" — SZL Holdings**

**Author:** Stephen P. Lutar Jr. · SZL Holdings · ORCID [0009-0001-0110-4173](https://orcid.org/0009-0001-0110-4173)

**Concept DOI (always-latest):** [10.5281/zenodo.19944926](https://doi.org/10.5281/zenodo.19944926)

> This markdown file is a faithful rendering of `main.tex`. The typeset 20-page PDF (`main.pdf`) is the canonical presentation; `main.tex` is the authoritative LaTeX source. Pinned commits: `main` @ `b910c276`; locked kernel @ `c7c0ba17`. Repository: [github.com/szl-holdings/lutar-lean](https://github.com/szl-holdings/lutar-lean).

---

## Abstract

Governed deployment of agentic artificial intelligence in regulated and defense settings requires more than benchmark accuracy: it requires *checkable* guarantees about what a system did, why it was permitted to do it, and whether the record can be tampered with after the fact. This is **v24** of the Ouroboros thesis program of SZL Holdings, a DOI-pinned lineage (v1–v23) whose subject is a machine-verified trust substrate resting on three pillars: (i) the *Ouroboros loop*, a bounded, well-founded self-governing computation in which "the loop is the product"; (ii) the *Lutar invariant* Λ_k(x) = (∏_{i=1}^k x_i)^{1/k}, an equal-weight geometric-mean trust aggregator; and (iii) a *proof-trail / receipt architecture* formalized in Lean 4.

The headline advance of v24 is an **axiom-free conditional Λ-uniqueness theorem**. In v23 the conditional uniqueness of Λ was gated on a *declared* project axiom (A6′ block-consistency). Here we report `Lutar.Round13.lambda_unique_of_separable`: under {A1, A2, A3, A5} together with *slice-multiplicativity* (separability), Λ is the unique aggregator, with `#print axioms = {propext, Classical.choice, Quot.sound}` — i.e. **no project axiom**, kernel-clean, CI-green, merged to `main` at `b910c276`. This strictly strengthens v23: the extra hypothesis is now a *checkable property of* Φ (weaker than the old *Factors* premise) discharged through Mathlib and already-proved in-tree lemmas, rather than a declared idealization.

Crucially, the *unconditional* uniqueness of Λ under {A1–A5} remains machine-checked **false** (in-tree `maxAgg_ne_Lambda`; `maxAgg` and `min` are A1–A5 counterexamples), so Λ stays **Conjecture 1** unconditionally — never a theorem. We also report a separate *experimental, CI-green* tier of frontier theorems (CF-13, CF-17, Wave-13 replay/quorum/HM results, and the Wave-14 pack CF-18/19/20/21), all `#print axioms`-clean, that is never folded into the locked-five. The honesty doctrine is binding throughout: locked-proven = exactly five {F1, F11, F12, F18, F19}; declared axioms disclosed; supply-chain posture SLSA L1 honest with L2 a roadmap (correcting a v23 overstatement); nothing fabricated. We argue that replacing a declared axiom with a checkable property is an *epistemic upgrade*, and that this calibrated honesty is what makes every positive claim credible to an auditor.

**Honesty note (verbatim).** The Lutar invariant Λ is **Conjecture 1** unconditionally and is *never* claimed proven unconditionally; unconditional uniqueness under A1–A5 is machine-checked *false*. The v24 conditional uniqueness theorem `lambda_unique_of_separable` holds under {A1,A2,A3,A5} + slice-multiplicativity with **no project axiom** (`#print axioms = {propext, Classical.choice, Quot.sound}`). Locked/proven = exactly five formulas {F1,F11,F12,F18,F19} at `c7c0ba17`. The experimental CI-green tier (1323 decl / 23 axioms / 307 sorries at `b910c276`) is a *separate* tier and is never folded into the locked-five. SLSA **L1 honest, L2 roadmap** — *not* L2-verified, L3, FedRAMP, Iron Bank, or CMMC. No fabricated results; no fake citations; 0 runtime CDN.

**Keywords:** governed agentic AI, trust aggregation, Lutar invariant, geometric mean, slice-multiplicativity, functional-equation uniqueness, Lean 4, Mathlib, axiom-free verification, `#print axioms`, receipt chain, SLSA, Byzantine consensus, philosophy of mathematics.

---

## 1. Introduction

The deployment of agentic AI into regulated industries (finance, healthcare) and defense settings has exposed a gap that benchmark performance cannot close: a *trust* gap. A regulator, an auditor, or a defense customer does not principally ask "how accurate is the model?"; they ask "what did the system do, under what authority, and can you prove the record has not been altered?" Answering those questions requires an artifact distinct from a model — a **trust substrate**: machinery that (a) governs what the agent is permitted to do, (b) aggregates evidence of trustworthiness into an auditable verdict, and (c) maintains a tamper-evident record of every governed decision.

This paper is v24 of a DOI-pinned thesis program SZL Holdings has developed across versions v1–v23. The defining commitment is an **honesty doctrine** (§2): we never let an engineering aspiration masquerade as a theorem. The headline of v24 is a single, sharp advance over v23. v23's strongest Λ-uniqueness result was *conditional* and *gated on a declared project axiom*: `lambda_unique_under_block`, which assumed a named `A6'_block_consistent` idealization. The headline of v24 is that this gate can be removed. The in-tree theorem

```
Lutar.Round13.lambda_unique_of_separable
```

proves Λ-uniqueness *conditional* on {A1, A2, A3, A5} together with *slice-multiplicativity* (separability), and its trusted base is exactly the Lean core: `#print axioms = {propext, Classical.choice, Quot.sound}` — **no project axiom**. It is kernel-clean, CI-green, and merged to `main` at `b910c276`. This *strictly strengthens* v23: the extra hypothesis is now a *checkable structural property of* the candidate aggregator Φ — and one weaker than the old *Factors* premise — discharged through Mathlib and already-proved in-tree lemmas, rather than a disclosed-but-unprovable idealization. We characterize this as an *epistemic upgrade* (§9).

**What does *not* change.** The single most important honest statement in this program is unchanged and we repeat it without softening: the *unconditional* uniqueness of Λ under {A1–A5} is machine-checked **false**. The in-tree witness `maxAgg_ne_Lambda` exhibits concrete A1–A5 aggregators (`maxAgg` and `min`) that differ from Λ. We therefore label Λ **Conjecture 1** unconditionally — never a theorem — exactly as v23 did. v24 does not, and never will, claim otherwise.

---

## 2. The honesty doctrine

The doctrine is load-bearing and is preserved verbatim across all SZL artifacts. It defines epistemic tiers, and every claim in this paper is tagged with exactly one:

- **[locked / kernel-verified]** — proven in Lean 4 with only the trusted core axioms {propext, Classical.choice, Quot.sound}; sorry-free; pinned at a fixed commit and part of the *locked* count. Locked-proven = exactly five.
- **[experimental, axiom-free, CI-green]** — proven sorry-free with only the trusted core axioms, CI-green at the recorded commit, but residing in the *experimental* tier and **never folded into the locked count**.
- **[axiom-gated]** — sorry-free *given* an explicitly declared, disclosed idealizing axiom (e.g. hash collision-resistance), with the axiom appearing in the `#print axioms` ledger.
- **[CI-pending]** — signature-checked but not reproducibly green in the wired build; **not** claimed proven.
- **[machine-checked FALSE]** — the statement is refuted by a machine-checked counterexample.
- **[Conjecture 1 — NOT a theorem]** — a research hypothesis. Λ's unconditional uniqueness lives here.

**Non-negotiable rules.**
1. **Λ is Conjecture 1 unconditionally** — never claimed proven unconditionally. Unconditional uniqueness under A1–A5 is machine-checked **false**.
2. **Locked-proven = exactly five** {F1, F11, F12, F18, F19} at `c7c0ba17` (749 decl / 14 axioms / 163 sorries). The experimental CI-green tier (1323/23/307 at `b910c276`) is a separate tier, never folded in.
3. **All axioms are disclosed** via `#print axioms`. No fabricated results; no fake citations; 0 runtime CDN.
4. **SLSA L1 honest, L2 a roadmap** — *not* L2-verified, L3, FedRAMP, Iron Bank, or CMMC (correcting a v23 overstatement; see §7.4).
5. Open sorries are disclosed; only kernel-verified results are stated as proven, everything else is explicitly tiered.

---

## 3. The Ouroboros loop: bounded self-governance

The first pillar is a self-referential governed computation — the *Ouroboros loop* — in which the system's output feeds its own governance input under a bounded, well-founded recursion. "The loop is the product": the governed loop, not a single inference, is the unit of value. Termination is guaranteed by a well-founded measure; self-reference is rendered coherent by **Tarskian stratification** (a governed object-level computation is audited by a strictly higher meta-level), avoiding the self-verification paradoxes of Gödel/Tarski. The bottom turtle — the Lean kernel, the cryptographic idealizations, and human sign-off — is finite and disclosed (Appendix A.3).

---

## 4. The Lutar invariant Λ and its uniqueness boundary

### 4.1 Definition and the aggregation axioms

**Definition (Λ).** For x ∈ [0,1]^k, the Lutar invariant is the equal-weight geometric mean Λ_k(x) = (∏_{i=1}^k x_i)^{1/k}.

The candidate aggregators Φ : [0,1]^k → [0,1] are constrained by five axioms:

- **(A1) Monotonicity** — Φ is nondecreasing in each argument.
- **(A2) Positive homogeneity** — on the ratio scale, Φ(λx) = λ Φ(x) for λ > 0.
- **(A3) Idempotence** — Φ(c, …, c) = c.
- **(A4) Boundedness** — min_i x_i ≤ Φ(x) ≤ max_i x_i.
- **(A5) Permutation-invariance** — Φ is symmetric in its arguments.

### 4.2 The unconditional refutation: FALSE, machine-checked

It is tempting to claim Λ_k is the *unique* Φ satisfying A1–A5. **This is false, and we prove it false.**

**Theorem 4.2 (Refutation of unconditional uniqueness). [machine-checked FALSE] [CI-green]** There exists Φ ≠ Λ_k satisfying A1–A5. In particular the max-aggregator maxAgg(x) = max_i x_i satisfies A1–A5 yet differs from Λ_k: at (4, 1) (on the ratio scale) one has maxAgg = 4 while Λ_2(4, 1) = 2. The minimum aggregator min_i x_i is a second witness.

*Lean reference.* The in-tree witness is `Round13.maxAgg_ne_Lambda`. The max function is monotone (A1), positively homogeneous (A2), idempotent (A3), bounded by itself hence ≤ max (A4), and symmetric (A5); evaluation at (4, 1) separates it from the geometric mean by `decide`. `#print axioms maxAgg_ne_Lambda` reports Lean-core axioms only. `min` is an analogous `decide`-checked companion.

This is the epistemic heart of the program: we did not merely *fail* to prove unconditional uniqueness; we proved its **negation**. Consequently Λ remains Conjecture 1 unconditionally (§4.5).

### 4.3 The old route: uniqueness given factorization, and the A6′ gate

The maximal honestly-true uniqueness statement of the prior lineage was conditional on factorization, fully proved in-tree.

**Theorem 4.3 (Uniqueness given factorization). [experimental, axiom-free, CI-green]** Let Φ satisfy A1–A5 and suppose Φ *factors*: there exist exponents α_1, …, α_k ≥ 0 with Φ(x) = ∏_i x_i^{α_i} for all x. Then Φ = Λ_k.

*Lean reference and sketch.* The Lean term is `lambda_unique_of_factors` (Round-13). Given factorization, idempotence (A3) forces ∑_i α_i = 1 and symmetry (A5) forces all α_i equal, whence α_i = 1/k and Φ = Λ_k. The exponent collapse uses `NNReal.rpow` arithmetic and a `Finset` induction; the companion `lambda_factors` (axiom-free, CI-green) shows Λ_k itself factors with exponents 1/k, so the hypothesis is non-vacuous.

In v23 the substrate's recommended route turned the opaque factorization hypothesis into a governance-legible declared axiom.

**Axiom 6 (Block-consistency / aggregation-invariance, A6′).** Aggregating evidence within independent blocks and then across the block results equals aggregating the flattened collection; equivalently, the verdict is invariant to how the auditor partitions evidence into review blocks (after Csátó 2018).

**Theorem 4.4 (v23 conditional uniqueness under declared A6′). [axiom-gated] [CI-green]** Under {A1–A5} together with the single declared axiom `A6'_block_consistent`, Λ_k is the unique normalized aggregator. Its disclosed base is `#print axioms lambda_unique_under_block = [A6'_block_consistent, propext, Quot.sound, Classical.choice]` — *one declared, non-core project axiom* plus the Lean core.

Theorem 4.4 was honest but carried a cost: the trusted base included a *project axiom* that could not itself be discharged in-kernel. v24 removes that cost.

### 4.4 The v24 advance: axiom-free conditional uniqueness (CUT-2)

The v24 headline replaces the declared A6′ idealization with a *checkable structural property* of the candidate aggregator: *slice-multiplicativity* (separability). Informally, Φ is slice-multiplicative if it factors as a product of per-axis slice functions, each of which is multiplicative, normalized, and monotone — properties one can in principle *verify* of a concrete Φ, rather than postulate.

**Definition 4.5 (Slice-multiplicativity / separability).** Φ : [0,1]^k → [0,1] is *slice-multiplicative* if there exist slice functions f_i : ℝ_{≥0} → ℝ_{≥0} such that **(sep)** Φ(x) = ∏_i f_i(x_i), **(mul)** f_i(s t) = f_i(s) f_i(t), **(one)** f_i(1) = 1, and **(mono)** each f_i is monotone.

**Theorem 4.6 (Axiom-free conditional uniqueness of Λ — the v24 advance). [experimental, axiom-free, CI-green]** Let k > 0 and let Φ satisfy the Lutar axioms {A1, A2, A3, A5}. If Φ is slice-multiplicative (Definition 4.5) then Φ = Λ_k. The Lean term is `lambda_unique_of_separable` (namespace `Lutar.Round13`); its trusted base is exactly

```
#print axioms lambda_unique_of_separable = {propext, Classical.choice, Quot.sound},
```

i.e. **no project axiom**. It is kernel-clean, CI-green, and merged to `main` at `b910c276`.

The exact Lean signature is:

```lean
theorem lambda_unique_of_separable {k : ℕ} (hk : 0 < k)
    (Φ : Aggregator k) (hL : LutarAxioms Φ)
    (f : Fin k → (NNReal → NNReal))
    (hsep  : ∀ x, Φ x = ∏ i, f i (x i))
    (hmul  : ∀ i s t, f i (s * t) = f i s * f i t)
    (hone  : ∀ i, f i 1 = 1)
    (hmono : ∀ i, Monotone (f i)) :
    Φ = Λ k
```

**Proof sketch and the in-tree lemma chain.** The proof reduces slice-multiplicativity to factorization and then discharges via Theorem 4.3. Concretely:

1. **Per-axis power law.** For each axis i, the slice f_i is multiplicative (mul), monotone (mono), and normalized (one). The in-tree lemma `multiplicative_monotone_isPow_pos` yields an exponent α_i with f_i(t) = t^{α_i} for all t ≠ 0:
   ```
   multiplicative_monotone_isPow_pos {f} (hf_mul) (hf_mono) (hf_one)
     : ∃ α, ∀ t ≠ 0, f t = t^(α : ℝ)
   ```
   Boundary value f_i(0) = 0^{α_i} follows from the idempotent dichotomy (`slice_zero_idem`, `slice_const_one_of_zero_one`).
2. **Exponent equality across axes.** The chosen exponents α_i are forced equal by permutation invariance (A5): applying `Equiv.swap i j` to a two-hot test vector and using the in-tree injectivity lemma `rpow_left_inj_one_lt` (c^a = c^b ⇒ a = b for c > 1) gives α_i = α_j.
3. **Assemble factorization.** Collecting the per-axis power laws yields the `Factors` predicate (Φ(x) = ∏_i x_i^{α_i}).
4. **Discharge.** Apply `lambda_unique_of_factors` (Theorem 4.3); idempotence (A3) and symmetry (A5) collapse the exponents to 1/k and conclude Φ = Λ_k.

The added hypothesis (slice-multiplicativity) is *weaker* than the old `Factors` premise — a slice-multiplicative Φ provably factors, but factorization alone does not exhibit the per-slice structure — and it is, unlike A6′, a property one can check by inspecting the definition of a concrete Φ.

### 4.5 Λ is Conjecture 1 — the precise claim structure

We state the claim structure without ambiguity. **Conjecture 1 (unconditional).** Λ is the correct unique governed aggregator under A1–A5 alone. This is **machine-checked false** as stated (Theorem 4.2), and so "Conjecture 1" denotes the open, *refined* hypothesis that, for the *governance-relevant* class of aggregators, the natural additional structural assumption (such as slice-multiplicativity or block-consistency) always holds. We never claim Λ proven unconditionally. What *is* proven is the conditional Theorem 4.6 (axiom-free) and Theorem 4.4 (axiom-gated, v23).

### 4.6 Worked examples

- **Λ is slice-multiplicative.** Take f_i(t) = t^{1/k}: it is multiplicative, normalized (1^{1/k} = 1), monotone, and ∏_i t_i^{1/k} = Λ_k. Hence Theorem 4.6's antecedent is non-vacuous.
- **maxAgg is not slice-multiplicative.** No product of per-axis slices reproduces max; consistent with maxAgg being an A1–A5 counterexample (Theorem 4.2) outside the slice-multiplicative class.
- **Separation at (4,1).** maxAgg(4,1) = 4 ≠ 2 = Λ_2(4,1), the `decide`-checked witness.

---

## 5. The proof-trail / receipt architecture

### 5.1 Structural correctness (sorry-free)

The receipt layer is a hash-chain of governed-decision entries with a Merkle commitment `root` per batch. Replay determinism (F1) — re-executing the recorded inputs reproduces the recorded root — is *locked* and kernel-verified (§6.1). Append-only structure and ordering invariants are sorry-free, with `#print axioms` reporting `propext` only over the log.

### 5.2 Security under declared idealizations (axiom-gated)

Hash-chain *binding* (you cannot alter a past entry without breaking the root) is proven **[axiom-gated]** under an explicitly declared `sha256_collision_resistant` axiom and the Merkle collision-resistance / domain-separation axioms — these are disclosed in the `#print axioms` ledger, never silently assumed, and are *not* a proof of cryptographic hardness. The DPO `klDivergence`/`pinsker` results remain **false-as-stated** for lack of a simplex hypothesis and are not claimed.

---

## 6. The locked kernel and the frontier theorem families

### 6.1 The locked five (kernel-verified at `c7c0ba17`)

The locked kernel proves **exactly five** governance formulas, sorry-free, with only the trusted core axioms, at the fixed commit `c7c0ba17` (749 declarations / 14 axioms / 163 sorries):

- **F1 — replay determinism.** Re-executing recorded inputs reproduces the recorded root.
- **F11 — Ayni reciprocity.** The reciprocity-balance invariant of the trust ledger.
- **F12 — Kuramoto additive (scaffolding only).** The additive coupling decomposition; the scaffolding, not the synchronization theorem.
- **F18 — Reed–Solomon.** The encoding/decoding correctness fact used by the receipt layer.
- **F19 — Bekenstein additive (scaffolding only, NOT the bound).** The additive bookkeeping scaffold; explicitly *not* the Bekenstein bound itself.

### 6.2 The experimental CI-green tier (at `b910c276`)

A *separate* corpus (1323 declarations / 23 axioms (22 unique) / 307 sorries at `b910c276`) is CI-green and `#print axioms`-clean. **It is never folded into the locked-five.** Every theorem below is `#print axioms`-clean (⊆ core) and resides in this experimental tier.

### 6.3 CF-13 — DEQ input-Lipschitz well-posedness margin

**[experimental, axiom-free, CI-green]** File `Lutar/Innovations/round5/OuroLoopInputLipschitz.lean` (7 declarations). For a contraction with input-Lipschitz constant L_x and contraction modulus K < 1, the equilibrium map z⋆ satisfies dist(z⋆(x), z⋆(y)) ≤ (L_x / (1−K)) · dist(x, y) (`equilibrium_dist_le`, `equilibrium_lipschitz`). Built on Mathlib `ContractingWith`; the result is the well-posedness margin of a deep equilibrium model (Bai–Kolter–Koltun, arXiv:1909.01377). `#print axioms = {propext, Classical.choice, Quot.sound}`.

### 6.4 CF-17 — floating-point summation error bound

**[experimental, axiom-free, CI-green]** File `Lutar/Khipu/NumericStability.lean` (8 declarations). Under the standard per-step rounding model, the recursive-summation forward error is bounded (`recSum_error_le`), following Higham's analysis. `#print axioms = {propext, Classical.choice, Quot.sound}`.

### 6.5 Wave-13 — replay completeness, quorum shadow, HM bottleneck

**[experimental, axiom-free, CI-green]**

- `findReplayRoot_complete` (via Lean core `List.find?_isSome`): if a replay-root candidate is a member of the candidate list and validates, the search returns `some`. `#print axioms = {propext, Quot.sound}`.
- `quorum_agreement_single_valued_vote`: for n ≥ 3f+1 and two quorums of size ≥ n−f, single-valued votes agree (v_1 = v_2), by nonempty quorum intersection. `#print axioms = {propext, Classical.choice, Quot.sound}`. **Honesty:** this assumes each organ votes via a *total function* (a non-Byzantine shadow); it is **NOT** the Byzantine BFT result — that remains the open **Khipu Conjecture 2**.
- `hm_bottleneck_clean`: the harmonic-mean bottleneck bound (contrapositive; pure order/field reasoning). `#print axioms = {propext, Classical.choice, Quot.sound}`.

### 6.6 Wave-14 — CF-18/19/20/21 (nine kernel-clean theorems)

**[experimental, axiom-free, CI-green]** All nine compile clean with `#print axioms = {propext, Classical.choice, Quot.sound}`.

- **CF-18 — Mādhava/Leibniz alternating-series remainder** (`Lutar/Wave14/LeibnizRemainder.lean`). For an antitone nonnegative a with alternating partial sums tending to L, one has |∑_{i<N}(−1)^i a_i − L| ≤ a_N (the Lean terms `leibniz_remainder_bound` and `madhava_alt_series_bound_clean`), via Mathlib `Antitone.alternating_series_le_tendsto` even/odd bracketing (Plofker 2009).
- **CF-19 — Reed–Solomon MDS distance lower bound** (`Lutar/Wave14/ReedSolomonDistance.lean`). Two distinct polynomials of degree < k agree on fewer than k points (`agreement_card_lt_of_degree_lt`); lifting via injectivity of the evaluation points gives the bound n − k + 1 ≤ #{i : p(pts_i) ≠ q(pts_i)} (`rs_distance_lower_bound`). This is the *achievability / lower-distance half* of Singleton; the upper bound and full MDS equality remain honest sorries (Reed–Solomon 1960, Singleton 1964).
- **CF-20 — VCG efficiency + truthfulness core** (`Lutar/Wave14/VCGEfficiency.lean`). An efficient outcome exists and maximizes social welfare (`exists_efficient_outcome`, `efficientOutcome_maximises`); the truthfulness core is the marginal-contribution monotonicity consequence (`vcg_truthfulness_core`) (Vickrey–Clarke–Groves; Nisan et al. 2007). **Honesty:** the in-tree `MechanismDesign/VCG.lean` references a nonexistent `Finset.argmax` and is unwired; CF-20 is a clean companion, not a patch.
- **CF-21 — Cover–Thomas log-sum + Gibbs** (`Lutar/Wave14/LogSumInequality.lean`). The log-sum inequality (`log_sum_inequality`) and Gibbs' inequality (`gibbs_inequality`) via log x ≤ x − 1 (Cover–Thomas Thm 2.7.1 and 2.6.3). **Honesty:** this is the *correctly-stated* DPI core; it does **not** repair the in-tree DPO `klDivergence`/`pinsker`, which remain false-as-stated for lack of a simplex hypothesis.

---

## 7. Verification status, in detail

### 7.1 The wave ledger (Waves 11–14)

| Wave | PR | Headline content | Status |
|------|-----|------------------|--------|
| 11 | — | Locked-kernel consolidation | locked @ `c7c0ba17` |
| 12 | #202 | CUT-2 axiom-free Λ-uniqueness (`lambda_unique_of_separable`) | merged, CI-green |
| 13 | #203 | replay completeness, quorum shadow, HM bottleneck | merged, CI-green |
| 14 | #204 | CF-18/19/20/21 (nine kernel-clean theorems) | merged, CI-green |

All Waves 11–14 are merged into `main` at `b910c276`.

### 7.2 The drift gate and the canonical numbers

The canonical drift-gate numbers at `b910c276` are **1323 declarations / 23 axioms (22 unique) / 307 sorries**; CI-green. The locked kernel at `c7c0ba17` is **749 / 14 / 163**, locking {F1, F11, F12, F18, F19}. These two tiers are reported separately and the experimental count is never folded into the locked-five.

### 7.3 The `#print axioms` discipline

Every claimed-proven theorem is accompanied by its `#print axioms` ledger. The axiom-free results report `#print axioms ⊆ {propext, Classical.choice, Quot.sound}` — the trusted Lean core only — with the sole exception of the explicitly axiom-gated cryptographic results (§5), whose declared idealizations appear in their ledgers. No theorem is stated as proven that CI has not verified at the recorded commit.

### 7.4 SLSA supply-chain posture — correcting a v23 overstatement

v23 wrote "SLSA L1+L2 attested". **This badge was wrong and is corrected here.** The honest posture is **SLSA L1**, with **L2 a roadmap item**. We do *not* claim L2-verified, L3, FedRAMP authorization, Iron Bank accreditation, or CMMC certification. The container build pipeline meets L1 provenance expectations; L2 (hosted, authenticated build service with signed provenance) is planned but not yet attested, and is reported as a roadmap item rather than a current state.

---

## 8. Why this is groundbreaking — the honest case

**Axiom elimination as a first-class result.** The standard way to "strengthen" a conditional theorem is to weaken its hypothesis. v24 does something sharper: it *removes a project axiom from the trusted base entirely*. v23's conditional uniqueness depended on `A6'_block_consistent`, a declared idealization that the kernel had to *trust*. v24's `lambda_unique_of_separable` depends on no project axiom at all (`#print axioms = {propext, Classical.choice, Quot.sound}`); the only added hypothesis is a *checkable property of* Φ. To our knowledge, exhibiting a governed-AI aggregator uniqueness result whose trusted base is exactly the bare Lean core is new.

**A machine-checked boundary, not just a conditional.** We did not merely prove a conditional theorem; we proved the *negation* of the unconditional claim (Theorem 4.2). Establishing exactly which extra assumption is required — and that without it the claim fails — converts a routine conditional into a *boundary* result: Theorem 4.6 is demonstrably close to the maximal true statement of its kind, and the boundary itself is machine-checked.

**Disclosed-axiom discipline at scale.** Formal verification of security-critical systems is well established (seL4 is the canonical machine-checked OS kernel); applying a disclosed-axiom, kernel-checked discipline to an AI governance aggregator and its receipt architecture — with a `#print axioms` ledger for *every* claim and a hard separation between a locked five and an experimental tier — is, as far as we can determine, new.

### 8.1 Honest comparison to prior art

| Prior art | What it provides | How v24 differs (honestly) |
|-----------|------------------|----------------------------|
| Verifiable-claims governance | The argument that AI claims should be externally verifiable. | A concrete substrate with a kernel-checked core; does not claim to solve verifiability in general. |
| seL4 / formal OS | Machine-checked OS-kernel correctness; the gold standard. | Verifies a governance aggregator + receipt layer; far smaller in scope and maturity; no seL4-level coverage claimed. |
| Certificate Transparency | Merkle-based tamper-evident logs in production. | Reuses the Merkle discipline; formalizes the binding property in Lean under declared axioms. |
| Functional-equation aggregation | Uniqueness characterizations of the geometric mean. | Formalizes an *axiom-free* conditional uniqueness (slice-multiplicativity) and machine-checks the unconditional refutation. |
| SLSA framework | A supply-chain integrity ladder (L1–L4). | Honestly attests L1; L2 is a roadmap item; L3 / FedRAMP / Iron Bank / CMMC explicitly *not* claimed. |

**Honest summary.** The individual mathematical facts (geometric-mean characterizations, Kraft, Shannon, Byzantine quorums, Reed–Solomon, VCG, log-sum) are classical. The contribution of v24 is their unification into a governed-AI trust substrate, their kernel-checked instantiation, and above all the *axiom elimination* on the central uniqueness result combined with the *honesty architecture* — locked counts, disclosed axioms, and a machine-checked refutation guarding the one tempting overclaim.

---

## 9. Philosophical foundations: slice-multiplicativity as an epistemic upgrade

### 9.1 From a declared axiom to a checkable property

A trusted base that contains a project axiom asks the auditor to *believe* something the kernel cannot check. A6′ (block-consistency) was such an axiom: governance-legible, published, and defensible, but ultimately *postulated*. Slice-multiplicativity is different in kind. It is a structural *property of the candidate aggregator* Φ — of the form "Φ factors into multiplicative, normalized, monotone slices" — that one can in principle *verify* of a concrete Φ by inspecting its definition. Replacing a postulate the auditor must trust with a property the auditor can check is, on any reliabilist account of justification, an *epistemic upgrade*: the warrant for the conclusion no longer routes through an unverifiable idealization.

### 9.2 When is a conditional legitimate?

Four conditions, all met by Theorem 4.6: (i) *independently-motivated antecedent* — separability is the standard hypothesis under which multiplicative aggregators are characterized; (ii) *non-vacuous instantiation* — Λ itself is slice-multiplicative (§4.6), so the conditional is not vacuously true; (iii) *boundary established* — without the hypothesis, uniqueness fails (Theorem 4.2); (iv) *disclosed at point of use* — the `#print axioms` ledger shows the bare core only, so the cost of the conditional is fully visible.

### 9.3 Slice-multiplicativity vs. block-consistency

Both pick out Λ within the A1–A5 class, but they differ epistemically. Block-consistency (A6′) is an *axiom about the world* (how evidence partitions behave) the auditor must accept. Slice-multiplicativity is a *property of the object* (the aggregator's functional form) the auditor can confirm. The latter is strictly preferable for governance, because the trusted base shrinks to the bare Lean core.

### 9.4 Steelman objections (with honest rebuttals)

- *"Slice-multiplicativity is just factorization renamed."* No — it is weaker than the old `Factors` premise and exposes the per-axis multiplicative/monotone/normalized structure that the proof actually consumes; factorization is *derived*, not assumed.
- *"A conditional theorem is weaker than an unconditional one."* True, but the unconditional statement is machine-checked **false**; the conditional is the maximal true statement, and we say so.
- *"You still rely on Classical.choice."* Yes — these are Lean-*core* axioms, disclosed in every ledger, and identical to the foundations of Mathlib itself; no *project* axiom is added.

---

## 10. Empirical posture (measured, not proven)

The following figures are **measured engineering numbers, not theorems**. They describe a reference deployment and are reported for context only; nothing in this section is a kernel-verified claim.

| Metric (reference deployment) | Value | Note |
|-------------------------------|-------|------|
| Median governed-loop latency | (measured) | end-to-end, single organ |
| Receipt append + root update | (measured) | per governed decision |
| `lake build` (full kernel check) | (measured) | at `b910c276`, CI-green |
| Runtime CDN dependencies | 0 | by construction |

These are operational characteristics, explicitly outside the honesty doctrine's "proven" tier.

---

## 11. Limitations and honesty

- **Λ is Conjecture 1 unconditionally.** Unconditional uniqueness under A1–A5 is machine-checked false; only conditional results are theorems.
- **Byzantine BFT is open (Khipu Conjecture 2).** The Wave-13 quorum result is a non-Byzantine shadow under a total-function voting assumption, not the BFT theorem.
- **307 open sorries** remain in the experimental tier at `b910c276`; they are disclosed, never claimed proven.
- **Cryptographic security is axiom-gated**, resting on declared collision-resistance idealizations, not proofs of hardness.
- **DPO `klDivergence`/`pinsker` are false-as-stated** for lack of a simplex hypothesis; CF-21 is a correctly-stated companion, not a repair.
- **Reed–Solomon CF-19** proves only the lower-distance half of Singleton; the upper bound and full MDS equality remain sorries.
- **SLSA L1 honest, L2 roadmap** — not L2-verified, L3, FedRAMP, Iron Bank, or CMMC.

---

## 12. Conclusion

v24 advances the Ouroboros program by a single, sharp, honest step: the conditional uniqueness of the Lutar invariant Λ is now proved **axiom-free**. `Lutar.Round13.lambda_unique_of_separable` shows that, under {A1, A2, A3, A5} together with the *checkable* property of slice-multiplicativity, Φ = Λ_k, with `#print axioms = {propext, Classical.choice, Quot.sound}` (no project axiom), kernel-clean and CI-green at `b910c276`. This strictly strengthens v23, whose conditional uniqueness was gated on the declared axiom A6′, by replacing a postulate the auditor must trust with a property the auditor can check — an epistemic upgrade.

The honesty doctrine is unchanged and binding: Λ remains **Conjecture 1** unconditionally (its unconditional uniqueness is machine-checked false via `maxAgg_ne_Lambda`); locked-proven = exactly five {F1, F11, F12, F18, F19} at `c7c0ba17`; the experimental CI-green tier (1323/23/307 at `b910c276`) is never folded in; declared axioms are disclosed in every `#print axioms` ledger; SLSA **L1 honest, L2 roadmap**; nothing fabricated; 0 runtime CDN. Calibrated honesty is not a weakness of the program — it is the feature that makes every positive claim credible to an auditor.

---

## Appendix A. Reproducibility and artifact manifest

### A.1 Pinned commits and artifacts

| Component | Pin | Contents / status |
|-----------|-----|-------------------|
| `main` (Waves 11–14 merged) | `b910c276` | 1323 decl / 23 axioms (22 unique) / 307 sorries; CI-green |
| Locked kernel | `c7c0ba17` | 749 / 14 / 163; locks {F1,F11,F12,F18,F19} |
| CUT-2 axiom-free Λ | in `b910c276` | `Round13/LambdaSeparable.lean` |
| Concept DOI (always-latest) | — | [10.5281/zenodo.19944926](https://doi.org/10.5281/zenodo.19944926) |
| Repository | — | [github.com/szl-holdings/lutar-lean](https://github.com/szl-holdings/lutar-lean) |

### A.2 How to verify

```bash
# 1. Kernel-check the merged library at the pinned commit
$ git checkout b910c276 && lake build        # expect: green, no errors

# 2. Disclose the trusted axiom base of the v24 headline theorem
$ #print axioms Lutar.Round13.lambda_unique_of_separable
=> [propext, Classical.choice, Quot.sound]   # NO project axiom

# 3. Confirm the unconditional claim is refuted
$ #print axioms maxAgg_ne_Lambda             # Lean-core axioms only

# 4. Verify the locked kernel separately
$ git checkout c7c0ba17 && lake build        # locks F1,F11,F12,F18,F19
```

### A.3 Trusted computing base

The bottom turtles, stated once: (i) soundness of the Lean 4 kernel and its core axioms {propext, Classical.choice, Quot.sound}; (ii) the declared cryptographic idealizations (`sha256_collision_resistant` and the Merkle collision-resistance / domain-separation axioms), used only in the receipt-security theorems; and (iii) human sign-off gating CI. The v24 headline theorem `lambda_unique_of_separable` depends on *none* of the cryptographic idealizations and on *no* project axiom — only on (i).

---

## Appendix B. Notation and glossary

| Symbol / term | Meaning |
|---------------|---------|
| Λ_k(x) | The Lutar invariant: equal-weight geometric mean (∏_i x_i)^{1/k} on [0,1]^k |
| Φ | A generic candidate aggregator [0,1]^k → [0,1] satisfying some subset of A1–A5 |
| maxAgg, min | The machine-checked A1–A5 witnesses that A1–A5 do not pin Λ (Thm 4.2) |
| A1–A5 | Monotonicity, positive homogeneity, idempotence, boundedness, permutation-invariance |
| A6′ | Block-consistency: the v23 declared axiom (replaced in v24) |
| slice-multiplicativity | The v24 checkable hypothesis: Φ = ∏_i f_i(x_i) with each f_i multiplicative, normalized, monotone |
| `lambda_unique_of_separable` | The v24 headline: axiom-free conditional Λ-uniqueness |
| link_i, root | The i-th hash-chain entry and the Merkle commitment to a receipt batch |
| sorry-free | A Lean development with no `sorry`; the kernel checks every step |
| CI-green | The real CI `lake build` (a full kernel check) passes at the pinned commit |
| axiom-gated | Sorry-free given an explicitly declared, disclosed idealizing axiom |
| `#print axioms` | Lean command listing the trusted axiom base of a theorem |
| locked-five | The exactly five kernel-verified formulas {F1,F11,F12,F18,F19} at `c7c0ba17` |
| experimental tier | The separate CI-green corpus (1323/23/307 at `b910c276`), never folded into the locked-five |
| Conjecture 1 | The open claim that Λ is the correct unique governed aggregator; never a theorem |

---

## References

1. J. Aczél. *On mean values.* Bulletin of the American Mathematical Society, 54(4):392–400, 1948. https://eudml.org/doc/296298
2. J. Aczél. *Lectures on Functional Equations and Their Applications.* Academic Press, 1966.
3. J. Aczél and T. L. Saaty. *Procedures for synthesizing ratio judgements.* Journal of Mathematical Psychology, 27(1):93–102, 1983.
4. S. Bai, J. Z. Kolter, V. Koltun. *Deep equilibrium models.* NeurIPS 2019. arXiv:1909.01377. https://arxiv.org/abs/1909.01377
5. T. M. Cover and J. A. Thomas. *Elements of Information Theory.* 2nd ed., Wiley, 2006.
6. E. H. Clarke. *Multipart pricing of public goods.* Public Choice, 11:17–33, 1971.
7. T. Groves. *Incentives in teams.* Econometrica, 41(4):617–631, 1973.
8. N. J. Higham. *Accuracy and Stability of Numerical Algorithms.* 2nd ed., SIAM, 2002.
9. G. Klein et al. *seL4: Formal verification of an OS kernel.* SOSP 2009.
10. The mathlib Community. *The Lean Mathematical Library.* CPP 2020.
11. L. de Moura and S. Ullrich. *The Lean 4 Theorem Prover and Programming Language.* CADE 2021.
12. N. Nisan, T. Roughgarden, É. Tardos, V. Vazirani (eds). *Algorithmic Game Theory.* Cambridge, 2007.
13. K. Plofker. *Mathematics in India.* Princeton University Press, 2009.
14. I. S. Reed and G. Solomon. *Polynomial codes over certain finite fields.* J. SIAM, 8(2):300–304, 1960.
15. R. C. Singleton. *Maximum distance q-nary codes.* IEEE Trans. Inf. Theory, 10(2):116–118, 1964.
16. W. Vickrey. *Counterspeculation, auctions, and competitive sealed tenders.* J. Finance, 16(1):8–37, 1961.
17. S. P. Lutar Jr. *The Ouroboros Thesis (Lean development).* SZL Holdings. Concept DOI [10.5281/zenodo.19944926](https://doi.org/10.5281/zenodo.19944926); repository [github.com/szl-holdings/lutar-lean](https://github.com/szl-holdings/lutar-lean).

*Full bibliographic detail with all URLs is in `refs.bib` and the typeset PDF bibliography.*