{"source":"ouroboros/LUTAR_EVIDENCE.md","lean_repo":"https://github.com/szl-holdings/lutar-lean","doctrine":"v10","canonical":{"declarations":749,"axioms":14,"sorries":163},"date":"2026-05-02","total_assertions":22,"passed":22,"failed":0,"lambda_definition":"Λ(x₁,...,x₉;w₁,...,w₉) = ∏ xᵢ^wᵢ","status_counts":{"proven":22,"sorry":0,"axiom":0,"conjecture":0},"axiom_summary":[{"axiom":"A1","tests":4,"passed":4,"failed":0,"status":"demonstrated"},{"axiom":"A2","tests":4,"passed":4,"failed":0,"status":"demonstrated"},{"axiom":"A3","tests":4,"passed":4,"failed":0,"status":"demonstrated"},{"axiom":"A4","tests":4,"passed":4,"failed":0,"status":"demonstrated"},{"axiom":"Boundary","tests":6,"passed":6,"failed":0,"status":"demonstrated"}],"claims":[{"id":"A1.1","axiom":"A1","name":"Monotonicity — non-decreasing (equal weights)","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/Monotonicity.lean"},{"id":"A1.2","axiom":"A1","name":"Monotonicity — non-decreasing (Egyptian weights)","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/Monotonicity.lean"},{"id":"A1.3","axiom":"A1","name":"Monotonicity — non-increasing when axis lowered","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/Monotonicity.lean"},{"id":"A1.4","axiom":"A1","name":"Monotonicity — strict (positive weight)","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/Monotonicity.lean"},{"id":"A2.1","axiom":"A2","name":"Zero-pinning — single axis at 0 collapses Λ","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/ZeroPinning.lean"},{"id":"A2.2","axiom":"A2","name":"Zero-pinning — multiple axes at 0 yield Λ = 0","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/ZeroPinning.lean"},{"id":"A2.3","axiom":"A2","name":"Zero-pinning — Λ = 0 iff positive-weight axis is 0","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/ZeroPinning.lean"},{"id":"A2.4","axiom":"A2","name":"Zero-pinning — zero-weight axis at 0 does NOT collapse Λ","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/ZeroPinning.lean"},{"id":"A3.1","axiom":"A3","name":"Egyptian inspectability — standard weight set","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/EgyptianWeights.lean"},{"id":"A3.2","axiom":"A3","name":"Egyptian inspectability — bit-exact reproducible","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/EgyptianWeights.lean"},{"id":"A3.3","axiom":"A3","name":"Egyptian inspectability — rational evaluator match","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/EgyptianWeights.lean"},{"id":"A3.4","axiom":"A3","name":"Egyptian inspectability — equal weight set valid","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/EgyptianWeights.lean"},{"id":"A4.1","axiom":"A4","name":"Page-curve concavity — line segment in [ε, 1]^9","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/PageCurve.lean"},{"id":"A4.2","axiom":"A4","name":"Page-curve concavity — stress segment","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/PageCurve.lean"},{"id":"A4.3","axiom":"A4","name":"Page-curve concavity — Λ ≤ AM–GM corollary","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/PageCurve.lean"},{"id":"A4.4","axiom":"A4","name":"Page-curve concavity — Λ = AM when all axes equal","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/PageCurve.lean"},{"id":"B.1","axiom":"Boundary","name":"Boundary — Λ(perfect) = 1","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/Boundary.lean"},{"id":"B.2","axiom":"Boundary","name":"Boundary — Λ(typical) ≈ 0.7","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/Boundary.lean"},{"id":"B.3","axiom":"Boundary","name":"Boundary — degraded drops below AM","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/Boundary.lean"},{"id":"B.4","axiom":"Boundary","name":"Boundary — symmetry under permutation","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/Boundary.lean"},{"id":"B.5","axiom":"Boundary","name":"Boundary — axis labels match thesis","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/Boundary.lean"},{"id":"B.6","axiom":"Boundary","name":"Boundary — weights sum to 1","status":"PROVEN","lean_file":"Lutar/LambdaInvariant/Boundary.lean"}]}