corpus/lean/lutar-lean__VERIFIED_THEOREMS.md

Verified Theorems

AUTO-GENERATED — do not edit by hand. Produced by .github/scripts/gen_verified_theorems.py from the real lake build, and gated in CI by check_verified_theorems_drift.py (any hand edit or drift fails the build). Each entry below is a theorem/lemma on the governed uniqueness / identifiability surface that the Lean kernel checks with zero sorry and whose #print axioms footprint stays within {propext, Classical.choice, Quot.sound} plus the already-declared, cited repo axioms in .github/data/lean_numbers.json.

Honesty doctrine v11. The locked-proven set stays exactly 5. Conjecture 1 (unconditional Λ uniqueness, ∀ Φ, LutarAxioms Φ → Φ = Λ k) is machine-checked FALSE under A1–A5 — Lutar.Round13.maxAgg_ne_Lambda exhibits the max aggregator as an A1–A5 counterexample — so it can never appear here. Only the conditional uniqueness (lambda_unique_of_factors) is REAL.

Lutar/Round13/Lambda_Uniqueness.lean

• lambda_satisfiesAxioms_round13 {k : ℕ} (hk : 0 < k) : LutarAxioms (Λ k)
• lambda_unique_of_factors {k : ℕ} (hk : 0 < k) (Φ : Aggregator k) (hL : LutarAxioms Φ) (αs : Fin k → NNReal) (hfac : Factors Φ αs) : Φ = Λ k
• maxAgg_A5 : IsPermutationInvariant maxAgg
• maxAgg_A3 : ∀ c : NNReal, maxAgg (fun _ => c) = c
• maxAgg_A2 : ∀ (c : NNReal) (x : Axes 2), maxAgg (fun i => c * x i) = c * maxAgg x
• maxAgg_ne_Lambda : maxAgg ≠ Λ 2

Lutar/Uniqueness.lean

• lambda_isMonotone {k : Nat} (hk : 0 < k) : IsMonotone (Λ k)
• lambda_isHomogeneous {k : Nat} (hk : 0 < k) : IsHomogeneous (Λ k)
• lambda_isEgyptianExact {k : Nat} (hk : 0 < k) : IsEgyptianExact k (Λ k)
• lambda_isBounded {k : Nat} (hk : 0 < k) : IsBounded hk (Λ k)
• Lambda_A5_perm_invariant {k : Nat} (hk : 0 < k) (x : Axes k) (σ : Fin k ≃ Fin k) : Λ k (x ∘ ↑σ) = Λ k x
• lambda_isPermutationInvariant {k : Nat} (hk : 0 < k) : IsPermutationInvariant (Λ k)
• lambda_satisfiesAxioms {k : Nat} (hk : 0 < k) : LutarAxioms (Λ k)

Lutar/Uniqueness/AxiomCheck.lean

• theoremU_axiom_sets_kernel_only : theoremUDisclosed.all (fun p => axiomsAllowed p.2) = true
• locked_count_five : lockedNames.length = 5
• theoremU_excluded_from_locked : theoremUDisclosed.all (fun p => ! lockedNames.contains p.1) = true
• conjecture1_still_open : openConjectures.length = 1

Lutar/Uniqueness/LambdaEquiv.lean

• lambdaEquiv_refl {k : ℕ} (Φ : Aggregator k) : LambdaEquiv Φ Φ
• lambdaEquiv_symm {k : ℕ} {Φ Ψ : Aggregator k} (h : LambdaEquiv Φ Ψ) : LambdaEquiv Ψ Φ
• lambdaEquiv_trans {k : ℕ} {Φ Ψ Χ : Aggregator k} (h₁ : LambdaEquiv Φ Ψ) (h₂ : LambdaEquiv Ψ Χ) : LambdaEquiv Φ Χ
• lambdaEquiv_equivalence {k : ℕ} : Equivalence (@LambdaEquiv k)
• auditProbe_two : auditProbe 2 = (![4, 1] : Axes 2)
• lambdaEquiv_nondegenerate : ∃ Φ Ψ : Aggregator 2, ¬ LambdaEquiv Φ Ψ

Lutar/Uniqueness/TheoremU.lean

• CorollaryU2_LambdaUnique_Factors {k : ℕ} (Φ : Aggregator k) (fa : FactorAssumptions Φ) : Φ = Λ k
• CorollaryU1_LambdaUnique_Separable {k : ℕ} (Φ : Aggregator k) (sa : SeparableAssumptions Φ) : Φ = Λ k
• identifiability_forces_lambda {k : ℕ} (Φ : Aggregator k) (ia : IdentifiabilityAssumptions Φ) : Φ = Λ k
• TheoremU_LambdaUnique {k : ℕ} (Φ Ψ : Aggregator k) (iaΦ : IdentifiabilityAssumptions Φ) (iaΨ : IdentifiabilityAssumptions Ψ) : LambdaEquiv Φ Ψ
• TheoremU_LambdaUnique_eq {k : ℕ} (Φ Ψ : Aggregator k) (iaΦ : IdentifiabilityAssumptions Φ) (iaΨ : IdentifiabilityAssumptions Ψ) : Φ = Ψ
• lambda_equiv_to_eq_of_anchored {k : ℕ} {Φ Ψ : Aggregator k} (_h : LambdaEquiv Φ Ψ) (hΦ : Anchored Φ) (hΨ : Anchored Ψ) : Φ = Ψ