From 6a4c0a723c0cf042171dfa6a64fef8041b595755 Mon Sep 17 00:00:00 2001 From: Nelson Spence Date: Sat, 28 Mar 2026 18:06:44 -0500 Subject: [PATCH 1/2] refactor: golf proofs from Aristotle optimization run Cherry-picked clean proof golfs from Aristotle's optimization pass, verified against Lean 4.28.0 + current Mathlib. All theorem statements unchanged; modifications are proof-internal only. - CoefficientLemmas: a_nonneg, a_le_one to term mode (drop by unfold) - OperatorLemmas: laplacian_zero, laplacian_linear via simpa - LinftyAlgebraic: rpow_le_of_mul_rpow_le backward proof, inline helper - Theorems: spectral_characterization_1d one-liner, nlinarith with hint, inline linfty_bound Rejected scaling_uniqueness golf (readability loss, fragile ring tactic). Net: -17 lines, zero sorries, axiom dashboard unchanged. --- CdFormal/CoefficientLemmas.lean | 13 ++++--------- CdFormal/LinftyAlgebraic.lean | 19 +++++++------------ CdFormal/OperatorLemmas.lean | 9 ++------- CdFormal/Theorems.lean | 15 ++++----------- 4 files changed, 17 insertions(+), 39 deletions(-) diff --git a/CdFormal/CoefficientLemmas.lean b/CdFormal/CoefficientLemmas.lean index 5016376..6ce9faf 100644 --- a/CdFormal/CoefficientLemmas.lean +++ b/CdFormal/CoefficientLemmas.lean @@ -47,21 +47,16 @@ variable (ctx : SemioticContext n M) Axiom dependencies: `κ_bounds`, `γ_bounds`, `μ_bounds`. Upstream candidate: no — paper-specific coefficient structure. -/ -theorem a_nonneg (x : M) : 0 ≤ ctx.a x := by - unfold SemioticContext.a - exact mul_nonneg - (mul_nonneg (ctx.κ_bounds x).1 (ctx.γ_bounds x).1) - (ctx.μ_bounds x).1 +theorem a_nonneg (x : M) : 0 ≤ ctx.a x := + mul_nonneg (mul_nonneg (ctx.κ_bounds x).1 (ctx.γ_bounds x).1) (ctx.μ_bounds x).1 /-- The creative drive a(x) = κ(x)·γ(x)·μ(x) ≤ 1, since each factor lies in [0,1]. Axiom dependencies: `κ_bounds`, `γ_bounds`, `μ_bounds`. Upstream candidate: no — paper-specific coefficient structure. -/ -theorem a_le_one (x : M) : ctx.a x ≤ 1 := by - unfold SemioticContext.a - exact mul_le_one₀ - (mul_le_one₀ (ctx.κ_bounds x).2 (ctx.γ_bounds x).1 (ctx.γ_bounds x).2) +theorem a_le_one (x : M) : ctx.a x ≤ 1 := + mul_le_one₀ (mul_le_one₀ (ctx.κ_bounds x).2 (ctx.γ_bounds x).1 (ctx.γ_bounds x).2) (ctx.μ_bounds x).1 (ctx.μ_bounds x).2 /-- The saturation exponent satisfies p - 1 > 0. diff --git a/CdFormal/LinftyAlgebraic.lean b/CdFormal/LinftyAlgebraic.lean index 9711875..83e5ce5 100644 --- a/CdFormal/LinftyAlgebraic.lean +++ b/CdFormal/LinftyAlgebraic.lean @@ -45,12 +45,8 @@ lemma rpow_le_of_mul_rpow_le (v b c p : ℝ) (hv : v > 0) (hc : c > 0) (h : b * v ≥ c * v ^ p) : v ^ (p - 1) ≤ b / c := by - have h_div : b * v / (c * v) ≥ c * v ^ p / (c * v) := - div_le_div_of_nonneg_right h (mul_nonneg hc.le hv.le) - have h_simplified : b / c ≥ v ^ p / v := by - field_simp [mul_comm, mul_assoc, mul_left_comm] at h_div ⊢ - exact h_div - rwa [Real.rpow_sub_one hv.ne'] at * + rw [Real.rpow_sub, Real.rpow_one] <;> try linarith + rw [div_le_div_iff₀] <;> linarith /-- From `b·v ≥ c·v^p` conclude `v ≤ (b/c)^{1/(p-1)}` by taking the `(p-1)`-th root. This is the algebraic core of Paper Lemma 3.10. @@ -59,11 +55,10 @@ lemma rpow_le_of_mul_rpow_le theorem linfty_bound_algebraic (v b c p : ℝ) (hv : v > 0) (hc : c > 0) (hp : p > 1) (h : b * v ≥ c * v ^ p) : - v ≤ (b / c) ^ (1 / (p - 1)) := by - have h_root : v ^ (p - 1) ≤ b / c → v ≤ (b / c) ^ (1 / (p - 1)) := - fun h ↦ le_trans - (by rw [← Real.rpow_mul hv.le, mul_one_div_cancel (by linarith), Real.rpow_one]) - (Real.rpow_le_rpow (by positivity) h (one_div_nonneg.mpr (by linarith))) - exact h_root (rpow_le_of_mul_rpow_le v b c p hv hc h) + v ≤ (b / c) ^ (1 / (p - 1)) := + le_trans + (by rw [← Real.rpow_mul hv.le, mul_one_div_cancel (by linarith), Real.rpow_one]) + (Real.rpow_le_rpow (by positivity) (rpow_le_of_mul_rpow_le v b c p hv hc h) + (one_div_nonneg.mpr (by linarith))) end diff --git a/CdFormal/OperatorLemmas.lean b/CdFormal/OperatorLemmas.lean index c7901aa..7ccf2cd 100644 --- a/CdFormal/OperatorLemmas.lean +++ b/CdFormal/OperatorLemmas.lean @@ -47,9 +47,7 @@ variable {n : ℕ} {M : Type*} @[simp] lemma laplacian_zero : ops.laplacian (fun _ : M ↦ (0 : ℝ)) = fun _ ↦ 0 := by - have h := ops.laplacian_smul (fun _ ↦ (0 : ℝ)) 0 - simp only [zero_mul] at h - exact h + simpa using ops.laplacian_smul (fun _ ↦ (0 : ℝ)) 0 /-- Full linearity of the Laplacian: Δ(c·f + g) = c·Δf + Δg. Composed from `laplacian_add` and `laplacian_smul`. @@ -60,10 +58,7 @@ lemma laplacian_zero : lemma laplacian_linear (f g : M → ℝ) (c : ℝ) : ops.laplacian (fun x ↦ c * f x + g x) = fun x ↦ c * ops.laplacian f x + ops.laplacian g x := by - have h_add := ops.laplacian_add (fun x ↦ c * f x) g - have h_smul := ops.laplacian_smul f c - simp only [h_smul] at h_add - exact h_add + simpa [ops.laplacian_smul] using ops.laplacian_add (fun x ↦ c * f x) g /-- The gradient norm of the zero function is zero. Direct consequence of `gradNorm_const` with a = 0. diff --git a/CdFormal/Theorems.lean b/CdFormal/Theorems.lean index af5cb40..a947f63 100644 --- a/CdFormal/Theorems.lean +++ b/CdFormal/Theorems.lean @@ -70,11 +70,7 @@ theorem spectral_characterization_1d (L : ℝ) (b : ℝ) (beta : ℝ) (hb : b > 0) : let beta_star := viabilityThreshold L b beta > beta_star → (Real.pi / L) ^ 2 - beta * b < 0 := by - intro beta_star h_beta - have h1 : beta > (Real.pi / L) ^ 2 / b := h_beta - have h2 : beta * b > (Real.pi / L) ^ 2 := by - rwa [gt_iff_lt, div_lt_iff₀ hb] at h1 - linarith + intro _ h; have := (div_lt_iff₀ hb).mp h; linarith /-! ## Scaling Algebraic Contradiction @@ -92,10 +88,8 @@ lemma scaling_algebraic_contradiction (hp : p > 1) (hk : k > 1) (hc : c > 0) (hPhi : Phi_val > 0) (h_eq : -c * k * Phi_val ^ p ≤ -c * k ^ p * Phi_val ^ p) : False := by - have hcΦp : (0 : ℝ) < c * Phi_val ^ p := by positivity - have h_div : k ≥ k ^ p := by nlinarith - have h_lt : k < k ^ p := Real.self_lt_rpow_of_one_lt hk hp - linarith + have : (0 : ℝ) < c * Phi_val ^ p := by positivity + nlinarith [Real.self_lt_rpow_of_one_lt hk hp] /-! ## Existence Theorems (from PDEInfra typeclass) @@ -119,8 +113,7 @@ theorem SemioticBVP.exists_isWeakCoherentConfiguration ∃ Phi : M → ℝ, IsWeakCoherentConfiguration bvp Phi ∧ (∀ x, Phi x ≥ 0) := by - have h_bounded := infra.linfty_bound B hB - obtain ⟨Phi, hfix⟩ := infra.schaefer infra.T_compact h_bounded + obtain ⟨Phi, hfix⟩ := infra.schaefer infra.T_compact (infra.linfty_bound B hB) exact ⟨Phi, solOp.T_fixed_point Phi hfix, infra.fixed_point_nonneg Phi hfix⟩ /-- Paper Theorem 3.16: When viability exceeds dissipation (eigval < 0), From 8a0b3f091da3fd1f81eeafee61465ef292414e23 Mon Sep 17 00:00:00 2001 From: Nelson Spence Date: Sat, 28 Mar 2026 18:08:38 -0500 Subject: [PATCH 2/2] chore: add CODEOWNERS for Fieldnote-Echo and project-navi-bot --- .github/CODEOWNERS | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 .github/CODEOWNERS diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS new file mode 100644 index 0000000..70a0eb4 --- /dev/null +++ b/.github/CODEOWNERS @@ -0,0 +1,2 @@ +# Default code owners for all files +* @Fieldnote-Echo @project-navi-bot