refactor: golf proofs from Aristotle optimization run

.github/CODEOWNERS

@@ -0,0 +1,2 @@
+# Default code owners for all files
+* @Fieldnote-Echo @project-navi-bot

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.

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

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.

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),