Evidence Ledger — Lutar Invariant Λ

Source: szl-holdings/ouroboros/LUTAR_EVIDENCE.md · test file packages/ouroboros/src/lutar-invariant-proof.test.ts · 22/22 assertions pass · cross-referenced against Doctrine v10 (171 per-version theorem table).

22/22 PASS 749 declarations14 unique axioms 163 tracked sorrieslake build clean Λ uniqueness = Conjecture 1SLSA L1 (honest)

Λ definition (as declared in the evidence doc)

Λ(x₁,…,x₉; w₁,…,w₉) = ∏ xᵢ^wᵢ — the weighted geometric mean of nine independent runtime-trust axis scores in [0,1] under non-negative weights summing to 1.

Discrepancy — Aggregator definition not yet unified.
· Evidence doc (repos/ouroboros/LUTAR_EVIDENCE.md): Λ(x₁..x₉; w₁..w₉) = ∏ xᵢ^wᵢ (weighted GEOMETRIC MEAN)
· Fuzz harness (.clusterfuzzlite/fuzzers/fuzz_receipts.js · computeLambda()): computeLambda() — MIN reduction over axis values
DISCREPANCY: the evidence doc defines Λ as the weighted geometric mean (∏ xᵢ^wᵢ); the fuzz harness comment defines computeLambda() as a MIN reduction. One is the doc, one is the gate. The aggregator definition is NOT yet unified — this is the lutar_unique sorry root cause. Displayed honestly; neither is silently dropped.

Per-claim status (Doctrine v10: PROVEN / AXIOM / CONJECTURE / SORRY)

Status	Claim	Lean file:line	ref-vec	Note
PROVEN	Λ monotonicity (A1)	Lutar/Thesis/TH_V18_01_LambdaMonotonicity.lean	Y	Λ is non-decreasing in each axis; reference-vector exercised (numerical witness).
AXIOM	A1 = IsAuditFibre / audit-fibre	Lutar/Thesis/TH_V18_01_LambdaMonotonicity.lean (A1)	Y	Axiom of the Λ axiom suite.
AXIOM	A2 = IsHomogeneous	Lutar/Invariant.lean	Y	Doctrine v10: A2 is positive homogeneity (degree 1) — NOT the 'zero-pinning' label used in LUTAR_EVIDENCE.md.
AXIOM	A3 = Egyptian inspectability	Lutar/Egyptian.lean	Y	Egyptian unit-fraction weights — 17 theorems, 0 bare sorries (PROVEN family).
AXIOM	A4 = IsBounded	Lutar/Lambda/SchurConcave.lean	N	Doctrine v10: A4 is bounded-by-max-axis — NOT the 'page-curve concavity' label used in LUTAR_EVIDENCE.md. Reference vector NOT exercised.
PROVEN	Schur-concavity (thm:schur-concave)	Lutar/Lambda/SchurConcave.lean	N	Proven in Lean; reference vector not yet exercised.
PROVEN	Dual-witness soundness	Lutar/Thesis/TH_V18_01_LambdaMonotonicity.lean (A1)	Y	Two-witness soundness for high-severity gates.
CONJECTURE	Λ uniqueness	Lutar/Uniqueness.lean:120 (CAUCHY_ND sorry)	Y	Conjecture 1 — NOT Theorem 1. Depends on the OPEN CAUCHY_ND sorry (Uniqueness.lean:120) + a missing symmetry axiom. This is the lutar_unique sorry root cause.
SORRY	Reed-Solomon Singleton achievability	Lutar/CodingTheory/ReedSolomonSingleton.lean	N	Bare sorry — structural skeleton only; do NOT claim proven.
SORRY	PAC-Bayes Madhava bound	Lutar/PACBayes/MadhavaBound.lean	N	Bare sorry — partial.
SORRY	Banach contraction	Lutar/Banach/BabylonianContraction.lean	N	2 holes noted in header — partial.

Doctrine v10 axiom labels: A2 = IsHomogeneous (not "zero-pinning"), A4 = IsBounded (not "page-curve concavity"). The LUTAR_EVIDENCE.md doc uses the older descriptive labels; both are shown so the rename is auditable, not hidden.

Empirical axiom evidence (22/22 — from LUTAR_EVIDENCE.md)

Axiom	Doc label	Tests	Passed
A1	Monotonicity	4	4
A2	Zero-pinning	4	4
A3	Egyptian inspectability	4	4
A4	Page-curve concavity	4	4
Boundary	Boundary / sanity	6	6

A1

✓ A1 — Monotonicity Λ is non-decreasing in each axis (equal weights)

✓ A1 — Monotonicity Λ is non-decreasing in each axis (Egyptian weights)

✓ A1 — Monotonicity Λ is non-increasing when any axis is lowered

✓ A1 — Monotonicity strict monotonicity when weight is positive

A2

✓ A2 — Zero-pinning any single axis at 0 collapses Λ to 0

✓ A2 — Zero-pinning multiple axes at 0 still yield Λ = 0

✓ A2 — Zero-pinning Λ = 0 only when at least one axis with positive weight is 0

✓ A2 — Zero-pinning a zero-weight axis at 0 does NOT collapse Λ (definitional edge case)

A3

✓ A3 — Egyptian inspectability the standard weight set is a sum of distinct unit fractions

✓ A3 — Egyptian inspectability weight set is bit-exact reproducible (rational reconstruction)

✓ A3 — Egyptian inspectability Λ under Egyptian weights matches a rational evaluator on rational inputs

✓ A3 — Egyptian inspectability the equal-weight set 9 × (1/9) is also a valid Egyptian decomposition

A4

✓ A4 — Page-curve concavity concavity along a line segment in [ε, 1]^9

✓ A4 — Page-curve concavity concavity on a stress segment (one axis varying, others held)

✓ A4 — Page-curve concavity Λ ≤ weighted arithmetic mean (AM–GM corollary)

✓ A4 — Page-curve concavity Λ achieves arithmetic mean iff all axes equal (corollary)

Boundary

✓ Boundary and sanity Λ(perfect) = 1

✓ Boundary and sanity Λ(typical) ≈ 0.7

✓ Boundary and sanity Λ(degraded with one axis at 0.1) drops below arithmetic mean

✓ Boundary and sanity Λ is symmetric under axis permutation when weights are uniform

✓ Boundary and sanity axes are labeled as the thesis declares

✓ Boundary and sanity weights sum to 1 (both standard sets)

Theorem → Lean file:line · reference-vector exercised (Y/N)

Ver	Theorem / axiom	Type	Lean file	ref-vec
v3	A1	axiom	Lutar/Thesis/TH_V18_01_LambdaMonotonicity.lean	Y
v3	A2	axiom	Lutar/Invariant.lean (A2)	Y
v3	A3	axiom	Lutar/Egyptian.lean	Y
v3	A4	axiom	Lutar/Lambda/SchurConcave.lean (A4 concavity)	N
v12	3.3 Theorem 1 (Uniqueness)	theorem	Lutar/Uniqueness.lean (axiom; Conjecture 1)	N
v18	thm:lambda-monotone	theorem	Lutar/Thesis/TH_V18_01_LambdaMonotonicity.lean	Y
v18	thm:path-integral	theorem	Lutar/Thesis/TH_V18_01_LambdaMonotonicity.lean	Y
v18	thm:schur-concave	theorem	Lutar/Lambda/SchurConcave.lean	N
v18	def:lutar-axioms	definition	Lutar/Thesis/TH_V18_01_LambdaMonotonicity.lean	Y
v18	def:audit-fibre	definition	Lutar/Thesis/TH_V18_01_LambdaMonotonicity.lean (A1)	Y
v18	thm:dual-witness-soundness	theorem	Lutar/Thesis/TH_V18_01_LambdaMonotonicity.lean (A1)	Y
v19	conj:lambda-uniqueness	conjecture	Lutar/Thesis/TH_V18_01_LambdaMonotonicity.lean	Y
v20	conj:lambda-uniqueness	conjecture	Lutar/Thesis/TH_V18_01_LambdaMonotonicity.lean	Y

What this evidence does and does not establish.
Establishes: The closed-form Λ = ∏ xᵢ^wᵢ, evaluated in IEEE-754 double precision, satisfies its four axioms (monotonicity, zero-pinning, Egyptian inspectability, Page-curve concavity) on the test points exercised above.

Does NOT establish: That any specific runtime configuration in production has been audited, that any third-party body has reviewed this work, or that the runtime is deployed in any product. Empire APEX (administered by NYSTEC) is a procurement-counseling resource the founder engaged with on 2026-04-30; it is not an audit.

Reproduce: pnpm install && npx vitest run packages/ouroboros/src/lutar-invariant-proof.test.ts