import Mathlib.Tactic import Mathlib.Topology.Order.IntermediateValue import Mathlib.Analysis.SpecificLimits.Basic import Mathlib.Topology.MetricSpace.Contracting import Mathlib.Data.Nat.Pairing import Mathlib.Topology.Algebra.Order.Archimedean import Mathlib.Topology.Instances.Rat import Mathlib.Analysis.Normed.Group.Continuity /-! Exact-real algebraic certificates used by the 443 implementation. These do not certify IEEE-754 rounding, derivative estimates, existence of roots for arbitrary callbacks, or global convergence of a single-start solver. No `sorry`, custom axiom, or numerical oracle is used. -/ namespace Pandrosion444Base noncomputable section /-- The expanded model decrease used instead of subtracting squared norms. -/ theorem model_decrease (r v : ℝ) : (r^2 - (r+v)^2)/2 = -(r*v) - v^2/2 := by ring /-- The difference-product expression used for measured merit decrease. -/ theorem actual_decrease (r new : ℝ) : (r^2-new^2)/2 = (r-new)*(r+new)/2 := by ring /-- A strictly accepted ratio guarantees an exact-real decrease in merit. -/ theorem accepted_decreases (old new predicted eta : ℝ) (hp : 0 < predicted) (he : 0 < eta) (hr : eta < (old-new)/predicted) : new < old := by have h := (lt_div_iff₀ hp).mp hr have hpos := mul_pos he hp linarith /-- The normalized circle discriminant avoids coefficients quadratic in p. -/ theorem circle_discriminant (p t : ℝ) : (-6*((p-2)+(p+2)*t))^2 - 4*((p-1)*(p-2)-t*(p+1)*(p+2))*(12*(1-t)) = 12*(12*p^2*t-(p^2-4)*(1-t)^2) := by ring /-- This is precisely `disc` evaluated by the normalized Python expression. -/ theorem circle_discriminant_normalized (p t : ℝ) (hp : p ≠ 0) : 12*(12*p^2*t-(p^2-4)*(1-t)^2)/(144*p^2) = t-(1-4/p^2)*(1-t)^2/12 := by field_simp; ring /-- The rationalized small root satisfies the original quadratic. The positive sqrt choice and denominator assumptions must be checked separately. -/ theorem rationalized_quadratic (a b c d : ℝ) (hd : d^2=b^2-4*a*c) (hden : -b+d ≠ 0) : a*(2*c/(-b+d))^2+b*(2*c/(-b+d))+c=0 := by field_simp have hm := congrArg (fun x : ℝ => c*x) hd nlinarith only [hm] /-- Symmetry used to evaluate the arc correction with exp(-abs(log_t)). -/ theorem reciprocal_correction (t g : ℝ) (ht : t ≠ 0) (h1 : 1+g ≠ 0) (h2 : t+g ≠ 0) : ((1+g/t)/(1/t+g/t))*((1+g)/(t+g))=1 := by field_simp /-- Positive arc radicand on the supported degree and positive-real domain. -/ theorem arc_radicand_positive (p t : ℝ) (hp : 2 < p) (ht : 0 < t) : 0 < ((p-2)*(t^2+1)+(10*p+4)*t)/(12*p) := by have hp0 : 0 < p := by linarith have h1 : 0 < p-2 := by linarith have h2 : 0 < 10*p+4 := by linarith positivity /-- Monotonicity of one squared coefficient in the SVD secular equation. -/ theorem spectral_filter_monotone (s a lo hi : ℝ) (hs : 0 < s) (hlo : 0 ≤ lo) (hle : lo ≤ hi) : (s*a/(s^2+hi))^2 ≤ (s*a/(s^2+lo))^2 := by have h0 : 0 < s^2+lo := by nlinarith [sq_pos_of_pos hs] have h1 : 0 < s^2+hi := by linarith have hden : (s^2+lo)^2 ≤ (s^2+hi)^2 := by nlinarith rw [div_pow, div_pow] exact div_le_div_of_nonneg_left (sq_nonneg (s*a)) (sq_pos_of_pos h0) hden /-- Summing the coefficient inequality gives squared spectral-norm monotonicity. -/ theorem spectral_norm_monotone {ι : Type*} (I : Finset ι) (s a : ι → ℝ) (lo hi : ℝ) (hlo : 0 ≤ lo) (hle : lo ≤ hi) (hs : ∀ i ∈ I, 0 < s i) : (∑ i ∈ I, (s i*a i/(s i^2+hi))^2) ≤ ∑ i ∈ I, (s i*a i/(s i^2+lo))^2 := by exact Finset.sum_le_sum fun i hiI => spectral_filter_monotone (s i) (a i) lo hi (hs i hiI) hlo hle /-- Additive log residual update; Python evaluates this with compensated sums. -/ theorem log_residual_update (c p q step : ℝ) : c+p*(q+step)=(c+p*q)+p*step := by ring end end Pandrosion444Base namespace Pandrosion444Base noncomputable section /-- Preconditioning changes coordinates, not the modeled residual. -/ theorem precondition_component (a q d : ℂ) : a*(q/d)=(a/d)*q := by simp only [div_eq_mul_inv] ring theorem precondition_sum {ι : Type*} (I : Finset ι) (a q d : ι → ℂ) : (∑ j ∈ I, a j*(q j/d j))=∑ j ∈ I, (a j/d j)*q j := by exact Finset.sum_congr rfl fun j _ => precondition_component (a j) (q j) (d j) /-- Signed extrapolation: negative as well as positive linear contractions. -/ theorem geometric_extrapolation (x next root rho : ℝ) (hr : 1-rho ≠ 0) (h : next-root=rho*(x-root)) : x+(next-x)/(1-rho)=root := by field_simp nlinarith [h] /-- The inverse update satisfies its vector secant equation, row by row. -/ theorem inverse_rank_one_secant {ι : Type*} [Fintype ι] (H : ι → ι → ℂ) (s y row : ι → ℂ) (hd : (∑ j, row j*y j) ≠ 0) (i : ι) : (∑ j, (H i j+(s i-∑ k, H i k*y k)*row j/(∑ k, row k*y k))*y j)=s i := by simp_rw [add_mul, Finset.sum_add_distrib] have he : (∑ j, ((s i-∑ k, H i k*y k)*row j/(∑ k, row k*y k))*y j)= (s i-∑ k, H i k*y k)*(∑ j, row j*y j)/(∑ k, row k*y k) := by simp only [div_mul_eq_mul_div, ← Finset.sum_div, Finset.mul_sum] congr 1 apply Finset.sum_congr rfl intro j _ ring rw [he] field_simp ring /-- A cached true inverse gives exactly the Newton model equation. -/ theorem cached_newton_step {V : Type*} [AddCommGroup V] [Module ℂ V] (J H : V →ₗ[ℂ] V) (hinv : J.comp H=LinearMap.id) (r : V) : J (-H r)=-r := by have h := LinearMap.congr_fun hinv r change J (H r)=r at h simp only [map_neg, h] /-- Retaining the best evaluated point cannot worsen its exact norm. -/ theorem retain_best (best trial : ℝ) : min best trial ≤ best := min_le_left _ _ theorem retain_success (best trial tol : ℝ) (h : best ≤ tol) : min best trial ≤ tol := (min_le_left _ _).trans h /-- The callback boundary increments only below the global budget. -/ theorem budget_increment (count budget : ℕ) (h : count < budget) : count+1 ≤ budget := by omega end end Pandrosion444Base namespace Pandrosion444Base /-- A same-sign correction contracts the true residual, including overshoot. -/ theorem positive_log_contract (e delta : ℝ) (he : 0 < e) (hd : 0 < delta) (hu : delta < 2*e) : |e-delta| < |e| := by rw [abs_of_pos he] exact abs_lt.mpr ⟨by linarith, by linarith⟩ /-- Clipping to a contracting positive domain lifts to all larger residuals. -/ theorem clipped_log_contract (e bound delta : ℝ) (hb : 0 < bound) (he : bound ≤ e) (hd : 0 < delta) (hu : delta < 2*bound) : |e-delta| < |e| := by apply positive_log_contract e delta (by linarith) hd linarith /-- Batching identical positive corrections preserves strict decrease. The Python guard checks decrease after the floating-point batch as well. -/ theorem batched_log_contract (e bound delta : ℝ) (hb : 0 ≤ bound) (hd : 0 < delta) (hu : delta ≤ e-bound) : bound ≤ e-delta ∧ |e-delta| < |e| := by have he : 0 < e := by linarith constructor · linarith · rw [abs_of_nonneg (by linarith : 0 ≤ e-delta), abs_of_pos he] linarith theorem batch_budget (count batch budget : ℕ) (hc : count ≤ budget) (hb : batch ≤ budget-count) : count+batch ≤ budget := by omega end Pandrosion444Base namespace Pandrosion444Base /-- Row and column equilibration preserve the exact linear equation. -/ theorem two_sided_precondition (a q col row : ℂ) (hc : col ≠ 0) (hr : row ≠ 0) : ((a/col)/row)*(col*q)=(a*q)/row := by field_simp end Pandrosion444Base namespace Pandrosion444Base /-- Compact complex derivatives equal the real block representation. -/ theorem compact_product_re (a z : ℂ) : (a*z).re=a.re*z.re-a.im*z.im := by simp [Complex.mul_re] theorem compact_product_im (a z : ℂ) : (a*z).im=a.re*z.im+a.im*z.re := by simp [Complex.mul_im] /-- Scaling before squaring preserves the exact squared norm. The Python guard uses this identity for overflow and underflow cases. -/ theorem scaled_squared_norm {ι : Type*} (I : Finset ι) (a : ι → ℝ) (scale : ℝ) (hs : scale ≠ 0) : scale^2*(∑ i ∈ I, (a i/scale)^2)=∑ i ∈ I, (a i)^2 := by simp_rw [div_pow] rw [← Finset.sum_div] field_simp end Pandrosion444Base namespace Pandrosion444Exact /-- Executable exact-rational kernel; no IEEE-754 operations. -/ def sumSquares : List ℚ → ℚ | [] => 0 | x :: xs => x*x + sumSquares xs def checkResidual (values : List ℚ) (tolerance : ℚ) : Bool := decide (0 < tolerance ∧ sumSquares values ≤ tolerance*tolerance) def realSquares : List ℚ → ℝ | [] => 0 | x :: xs => (x : ℝ)*(x : ℝ)+realSquares xs theorem sumSquares_cast (values : List ℚ) : (sumSquares values : ℝ) = realSquares values := by induction values with | nil => simp [sumSquares, realSquares] | cons x xs ih => simp [sumSquares, realSquares, ih] theorem checkResidual_sound (values : List ℚ) (tolerance : ℚ) (h : checkResidual values tolerance=true) : 0 < (tolerance : ℝ) ∧ realSquares values ≤ (tolerance : ℝ)^2 := by have hh : 0 < tolerance ∧ sumSquares values ≤ tolerance*tolerance := by simpa [checkResidual] using h constructor · exact_mod_cast hh.1 · rw [← sumSquares_cast] have hc : (sumSquares values : ℝ) ≤ (tolerance : ℝ)*(tolerance : ℝ) := by exact_mod_cast hh.2 simpa [pow_two] using hc def checkPositiveBracket (X : ℚ) (p : ℕ) (a b : ℚ) : Bool := decide (0 < X ∧ 0 < p ∧ 0 ≤ a ∧ a ≤ b ∧ a^p ≤ X ∧ X ≤ b^p) theorem checkPositiveBracket_sound (X : ℚ) (p : ℕ) (a b : ℚ) (h : checkPositiveBracket X p a b=true) : ∃! r : ℝ, r ∈ Set.Icc (a : ℝ) (b : ℝ) ∧ r^p=(X : ℝ) := by have hh : 0 < X ∧ 0 < p ∧ 0 ≤ a ∧ a ≤ b ∧ a^p ≤ X ∧ X ≤ b^p := by simpa [checkPositiveBracket] using h have hab : (a : ℝ) ≤ (b : ℝ) := by exact_mod_cast hh.2.2.2.1 have ha : (a : ℝ)^p ≤ (X : ℝ) := by exact_mod_cast hh.2.2.2.2.1 have hb : (X : ℝ) ≤ (b : ℝ)^p := by exact_mod_cast hh.2.2.2.2.2 obtain ⟨r, hr, he⟩ := intermediate_value_Icc hab (continuousOn_id.pow p) ⟨ha, hb⟩ change r^p=(X : ℝ) at he refine ⟨r, ⟨hr, he⟩, ?_⟩ intro y hy have har : (0 : ℝ) ≤ (a : ℝ) := by exact_mod_cast hh.2.2.1 have hr0 : 0 ≤ r := har.trans hr.1 have hy0 : 0 ≤ y := har.trans hy.1.1 by_contra hn rcases lt_or_gt_of_ne hn with hlt | hgt · have hx : y^p < r^p := pow_lt_pow_left₀ hlt hy0 (Nat.ne_of_gt hh.2.1) rw [he, hy.2] at hx exact (lt_irrefl _ hx) · have hx : r^p < y^p := pow_lt_pow_left₀ hgt hr0 (Nat.ne_of_gt hh.2.1) rw [he, hy.2] at hx exact (lt_irrefl _ hx) def charge (count budget : ℕ) : Option ℕ := if count < budget then some (count+1) else none theorem charge_sound (count budget new : ℕ) (h : charge count budget=some new) : new=count+1 ∧ new ≤ budget := by unfold charge at h by_cases hc : count < budget · rw [if_pos hc] at h simp only [Option.some.injEq] at h constructor <;> omega · rw [if_neg hc] at h simp at h def boundedRun {S : Type} (step : S → Option S) : ℕ → S → S | 0, s => s | n+1, s => match step s with | none => s | some next => boundedRun step n next theorem boundedRun_preserves {S : Type} (step : S → Option S) (P : S → Prop) (hstep : ∀ s t, P s → step s=some t → P t) (n : ℕ) (s : S) (hs : P s) : P (boundedRun step n s) := by induction n generalizing s with | zero => exact hs | succ n ih => simp only [boundedRun] split · exact hs · next t ht => exact ih t (hstep s t hs ht) end Pandrosion444Exact /-! Independent convergence obligations for a future 444. These theorems are not a verification of the Python/NumPy implementation. In particular, `hstep` below is an obligation, not an established property of the 443's strict-decrease acceptance rule. -/ namespace Pandrosion444Audit open Filter Function open scoped Topology theorem constant_nonzero_has_no_root : ¬ ∃ x : ℝ, (fun _ : ℝ => (1 : ℝ)) x = 0 := by norm_num theorem no_universal_root_solver : ¬ ∃ solver : (ℝ → ℝ) → ℝ, ∀ f : ℝ → ℝ, f (solver f) = 0 := by rintro ⟨solver, h⟩ have hc := h (fun _ => 1) norm_num at hc /-- Even a continuous function with a unique root can hide that root beyond every prescribed bounded exploration region. This is not a claim that an unbounded exact algorithm cannot solve a restricted class of functions. -/ theorem root_beyond_bounded_search (B : ℝ) : ∃ f : ℝ → ℝ, Continuous f ∧ (∃! r, f r=0) ∧ (∀ x, x ≤ B → f x=1) := by let f : ℝ → ℝ := fun x => min 1 (B+1-x) refine ⟨f, continuous_const.min (continuous_const.sub continuous_id), ?_, ?_⟩ · refine ⟨B+1, ?_, ?_⟩ · dsimp [f]; simp · intro y hy change min 1 (B+1-y)=0 at hy by_cases h : 1 ≤ B+1-y · rw [min_eq_left h] at hy; norm_num at hy · rw [min_eq_right (le_of_not_ge h)] at hy; linarith · intro x hx dsimp [f] exact min_eq_left (by linarith) noncomputable def decreasingResidual (n : ℕ) : ℝ := 1 + (1/2 : ℝ)^n theorem decreasing_residual_strict (n : ℕ) : decreasingResidual (n+1) < decreasingResidual n := by have hp : 0 < (1/2 : ℝ)^n := pow_pos (by norm_num) _ unfold decreasingResidual rw [pow_succ] linarith theorem decreasing_residual_above_one (n : ℕ) : 1 < decreasingResidual n := by have hp : 0 < (1/2 : ℝ)^n := pow_pos (by norm_num) _ unfold decreasingResidual linarith theorem strict_descent_can_converge_to_nonzero : Tendsto decreasingResidual atTop (𝓝 1) := by have h := tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num : (0 : ℝ) ≤ 1/2) (by norm_num : (1 : ℝ)/2 < 1) change Tendsto (fun n : ℕ => 1+(1/2 : ℝ)^n) atTop (𝓝 1) simpa using (tendsto_const_nhds (x := (1 : ℝ))).add h /-- Quantitative decrease is enough, unlike strict decrease alone. -/ theorem residual_bound (r : ℕ → ℝ) (q : ℝ) (hq : 0 ≤ q) (hstep : ∀ n, r (n+1) ≤ q * r n) (n : ℕ) : r n ≤ q^n * r 0 := by induction n with | zero => simp | succ n ih => calc r (n+1) ≤ q * r n := hstep n _ ≤ q * (q^n * r 0) := mul_le_mul_of_nonneg_left ih hq _ = q^(n+1) * r 0 := by ring theorem residual_converges (r : ℕ → ℝ) (q : ℝ) (hq : 0 ≤ q) (hq1 : q < 1) (hnonneg : ∀ n, 0 ≤ r n) (hstep : ∀ n, r (n+1) ≤ q * r n) : Tendsto r atTop (𝓝 0) := by have h := (tendsto_pow_atTop_nhds_zero_of_lt_one hq hq1).mul_const (r 0) have ht : Tendsto (fun n : ℕ => q^n * r 0) atTop (𝓝 0) := by simpa using h exact squeeze_zero hnonneg (residual_bound r q hq hstep) ht /-- Fixed absolute rounding noise yields an error floor, not convergence to zero. -/ theorem perturbed_residual_bound (r : ℕ → ℝ) (q delta : ℝ) (hq : 0 ≤ q) (hq1 : q < 1) (hstep : ∀ n, r (n+1) ≤ q * r n + delta) (n : ℕ) : r n ≤ q^n * r 0 + delta/(1-q)*(1-q^n) := by have hd : 1-q ≠ 0 := by linarith induction n with | zero => simp | succ n ih => calc r (n+1) ≤ q * r n + delta := hstep n _ ≤ q * (q^n*r 0 + delta/(1-q)*(1-q^n)) + delta := by have hm := mul_le_mul_of_nonneg_left ih hq linarith _ = q^(n+1)*r 0 + delta/(1-q)*(1-q^(n+1)) := by rw [pow_succ] field_simp [hd] ring variable {E : Type*} [NormedAddCommGroup E] /-- Residual convergence implies iterate convergence only with an error bound. -/ theorem iterate_converges_of_residual (x : ℕ → E) (z : E) (r : ℕ → ℝ) (sigma : ℝ) (hsigma : 0 < sigma) (herror : ∀ n, sigma * ‖x n-z‖ ≤ r n) (hresidual : Tendsto r atTop (𝓝 0)) : Tendsto x atTop (𝓝 z) := by apply Metric.tendsto_atTop.mpr intro epsilon hepsilon have he : ∀ᶠ n : ℕ in atTop, r n < sigma*epsilon := (tendsto_order.mp hresidual).2 _ (by simpa using mul_pos hsigma hepsilon) obtain ⟨N, hN⟩ := eventually_atTop.mp he refine ⟨N, fun n hn => ?_⟩ rw [dist_eq_norm] have h := herror n have ht := hN n hn nlinarith end Pandrosion444Audit namespace Pandrosion444Exploration open Filter Function Set open scoped Topology def encodeInt : ℤ → ℕ | .ofNat n => 2*n | .negSucc n => 2*n+1 def decodeInt (k : ℕ) : ℤ := if k%2=0 then ((k/2 : ℕ) : ℤ) else -((k/2 : ℕ) : ℤ)-1 theorem decodeInt_encodeInt (z : ℤ) : decodeInt (encodeInt z)=z := by cases z with | ofNat n => change decodeInt (2*n)=(n : ℤ) unfold decodeInt have hm : (2*n)%2=0 := by omega rw [if_pos hm] have hd : (2*n)/2=n := by omega rw [hd] | negSucc n => change decodeInt (2*n+1)=Int.negSucc n unfold decodeInt have hm : (2*n+1)%2 ≠ 0 := by omega rw [if_neg hm] omega def encodeRat (q : ℚ) : ℕ := Nat.pair (encodeInt q.num) (q.den-1) def decodeRat (k : ℕ) : ℚ := (decodeInt (Nat.unpair k).1 : ℚ) / ((Nat.unpair k).2+1 : ℕ) theorem decodeRat_encodeRat (q : ℚ) : decodeRat (encodeRat q)=q := by unfold decodeRat encodeRat rw [Nat.unpair_pair] simp only [decodeInt_encodeInt] rw [Nat.sub_add_cancel q.den_pos] exact q.num_div_den def encodeVec : (n : ℕ) → (Fin n → ℚ) → ℕ | 0, _ => 0 | n+1, v => Nat.pair (encodeRat (v 0)) (encodeVec n (fun i => v i.succ)) def decodeVec : (n : ℕ) → ℕ → (Fin n → ℚ) | 0, _ => Fin.elim0 | n+1, k => Fin.cases (decodeRat (Nat.unpair k).1) (decodeVec n (Nat.unpair k).2) theorem decodeVec_encodeVec (n : ℕ) (v : Fin n → ℚ) : decodeVec n (encodeVec n v)=v := by induction n with | zero => funext i; exact Fin.elim0 i | succ n ih => funext i refine Fin.cases ?_ (fun j => ?_) i · simp [decodeVec, encodeVec, decodeRat_encodeRat] · simp [decodeVec, encodeVec, ih] noncomputable def seed (n k : ℕ) : Fin n → ℝ := fun i => decodeVec n k i theorem seeds_dense (n : ℕ) : DenseRange (seed n) := by have hd : DenseRange (fun v : Fin n → ℚ => fun i => (v i : ℝ)) := by exact DenseRange.piMap (fun _ => Rat.denseRange_cast) apply hd.mono rintro x ⟨v, rfl⟩ refine ⟨encodeVec n v, ?_⟩ funext i change (decodeVec n (encodeVec n v) i : ℝ)=(v i : ℝ) rw [decodeVec_encodeVec] variable {E : Type*} [NormedAddCommGroup E] /-- Existence plus continuity at a root is enough for eventual positive tolerance in the infinite exact-rational stream. No Jacobian is needed. This is a finite hitting theorem, not a practical complexity bound. -/ theorem eventual_hit (n : ℕ) (F : (Fin n → ℝ) → E) (r : Fin n → ℝ) (hr : F r=0) (hc : ContinuousAt F r) (epsilon : ℝ) (he : 0 < epsilon) : ∃ k : ℕ, ‖F (seed n k)‖ < epsilon := by have hmem : {x | ‖F x‖ < epsilon} ∈ 𝓝 r := hc.norm.preimage_mem_nhds (Iio_mem_nhds (by simpa [hr] using he)) exact (seeds_dense n).mem_nhds hmem /-- Three other families can be interleaved without starving dense samples. -/ theorem interleaved_eventual_hit (n : ℕ) (stream : ℕ → Fin n → ℝ) (hstream : ∀ k, stream (4*k)=seed n k) (F : (Fin n → ℝ) → E) (r : Fin n → ℝ) (hr : F r=0) (hc : ContinuousAt F r) (epsilon : ℝ) (he : 0 < epsilon) : ∃ k : ℕ, ‖F (stream k)‖ < epsilon := by obtain ⟨k, hk⟩ := eventual_hit n F r hr hc epsilon he exact ⟨4*k, by rwa [hstream]⟩ def best (residual : ℕ → ℝ) : ℕ → ℝ | 0 => residual 0 | n+1 => min (best residual n) (residual (n+1)) theorem best_le_current (residual : ℕ → ℝ) (n : ℕ) : best residual n ≤ residual n := by cases n with | zero => exact le_rfl | succ n => exact min_le_right _ _ theorem best_antitone (residual : ℕ → ℝ) : Antitone (best residual) := by apply antitone_nat_of_succ_le intro n exact min_le_left _ _ theorem best_nonnegative (residual : ℕ → ℝ) (h : ∀ n, 0 ≤ residual n) (n : ℕ) : 0 ≤ best residual n := by induction n with | zero => exact h 0 | succ n ih => exact le_min ih (h _) theorem best_finite_tolerance (n : ℕ) (F : (Fin n → ℝ) → E) (r : Fin n → ℝ) (hr : F r=0) (hc : ContinuousAt F r) (epsilon : ℝ) (he : 0 < epsilon) : ∃ N : ℕ, ∀ k ≥ N, best (fun j => ‖F (seed n j)‖) k < epsilon := by obtain ⟨N, hN⟩ := eventual_hit n F r hr hc epsilon he refine ⟨N, fun k hk => ?_⟩ exact ((best_antitone _ hk).trans (best_le_current _ N)).trans_lt hN theorem best_residual_converges (n : ℕ) (F : (Fin n → ℝ) → E) (r : Fin n → ℝ) (hr : F r=0) (hc : ContinuousAt F r) : Tendsto (best (fun j => ‖F (seed n j)‖)) atTop (𝓝 0) := by apply Metric.tendsto_atTop.mpr intro epsilon he obtain ⟨N, hN⟩ := best_finite_tolerance n F r hr hc epsilon he refine ⟨N, fun k hk => ?_⟩ rw [Real.dist_eq, sub_zero, abs_of_nonneg (best_nonnegative _ (fun _ => norm_nonneg _) _)] exact hN k hk noncomputable def argBest (residual : ℕ → ℝ) : ℕ → ℕ | 0 => 0 | k+1 => if residual (k+1) < best residual k then k+1 else argBest residual k theorem best_witness (residual : ℕ → ℝ) (k : ℕ) : residual (argBest residual k)=best residual k := by induction k with | zero => rfl | succ k ih => change residual (if residual (k+1) < best residual k then k+1 else argBest residual k) = min (best residual k) (residual (k+1)) split_ifs with h · exact (min_eq_right h.le).symm · rw [ih] exact (min_eq_left (le_of_not_gt h)).symm /-- The selected points converge to a specific root when a global residual error bound is also supplied. Dense sampling alone only proves residual convergence, especially when there are several roots or small residuals at infinity. -/ theorem selected_points_converge (n : ℕ) (F : (Fin n → ℝ) → E) (z : Fin n → ℝ) (hz : F z=0) (hc : ContinuousAt F z) (sigma : ℝ) (hsigma : 0 < sigma) (herror : ∀ x, sigma * ‖x-z‖ ≤ ‖F x‖) : Tendsto (fun k => seed n (argBest (fun j => ‖F (seed n j)‖) k)) atTop (𝓝 z) := by apply Metric.tendsto_atTop.mpr intro epsilon he obtain ⟨N, hN⟩ := best_finite_tolerance n F z hz hc (sigma*epsilon) (mul_pos hsigma he) refine ⟨N, fun k hk => ?_⟩ rw [dist_eq_norm] have hb := best_witness (fun j => ‖F (seed n j)‖) k have hl := herror (seed n (argBest (fun j => ‖F (seed n j)‖) k)) have ht := hN k hk nlinarith end Pandrosion444Exploration namespace Pandrosion444Sphere noncomputable section def horizontal (x t : ℝ) := 2*x/(1+t) def height (t : ℝ) := (t-1)/(1+t) def northGap (t : ℝ) := 2/(1+t) theorem north_gap_identity (t : ℝ) (ht : 0 ≤ t) : 1-height t=northGap t := by have hd : 1+t ≠ 0 := by linarith unfold height northGap field_simp ring theorem finite_points_exclude_north (t : ℝ) (ht : 0 ≤ t) : 0 < northGap t := by unfold northGap positivity theorem roundtrip_component (x t : ℝ) (ht : 0 ≤ t) : horizontal x t/(1-height t)=x := by rw [north_gap_identity t ht] have hd : 1+t ≠ 0 := by linarith unfold horizontal northGap field_simp theorem sphere_identity (t : ℝ) (ht : 0 ≤ t) : 4*t/(1+t)^2+(height t)^2=1 := by have hd : 1+t ≠ 0 := by linarith unfold height field_simp ring theorem inverse_projection_on_sphere {ι : Type*} [Fintype ι] (u : ι → ℝ) : let t := ∑ i, (u i)^2 (∑ i, (horizontal (u i) t)^2)+(height t)^2=1 := by dsimp only have ht : 0 ≤ ∑ i, (u i)^2 := Finset.sum_nonneg (fun _ _ => sq_nonneg _) have hsum : (∑ i, (horizontal (u i) (∑ j, (u j)^2))^2)= 4*(∑ i, (u i)^2)/(1+∑ i, (u i)^2)^2 := by unfold horizontal simp_rw [div_pow, mul_pow] rw [← Finset.sum_div, ← Finset.mul_sum] norm_num rw [hsum] exact sphere_identity _ ht theorem root_equivalence {ι Y : Type*} [Fintype ι] [Zero Y] (F : (ι → ℝ) → Y) (u : ι → ℝ) : F (fun i => horizontal (u i) (∑ j, (u j)^2)/(1-height (∑ j, (u j)^2)))=0 ↔ F u=0 := by have ht : 0 ≤ ∑ i, (u i)^2 := Finset.sum_nonneg (fun _ _ => sq_nonneg _) simp_rw [roundtrip_component _ _ ht] /-- Far regions shrink toward the pole; compactifying does not remove this conditioning issue or turn the pole into an ordinary finite root. -/ theorem far_regions_near_pole (t T : ℝ) (hT : 0 ≤ T) (h : T ≤ t) : northGap t ≤ northGap T := by unfold northGap apply div_le_div_of_nonneg_left (by norm_num) (by linarith) (by linarith) end end Pandrosion444Sphere #print axioms Pandrosion444Base.model_decrease #print axioms Pandrosion444Base.actual_decrease #print axioms Pandrosion444Base.accepted_decreases #print axioms Pandrosion444Base.circle_discriminant #print axioms Pandrosion444Base.circle_discriminant_normalized #print axioms Pandrosion444Base.rationalized_quadratic #print axioms Pandrosion444Base.reciprocal_correction #print axioms Pandrosion444Base.arc_radicand_positive #print axioms Pandrosion444Base.spectral_filter_monotone #print axioms Pandrosion444Base.spectral_norm_monotone #print axioms Pandrosion444Base.log_residual_update #print axioms Pandrosion444Base.precondition_component #print axioms Pandrosion444Base.precondition_sum #print axioms Pandrosion444Base.geometric_extrapolation #print axioms Pandrosion444Base.inverse_rank_one_secant #print axioms Pandrosion444Base.cached_newton_step #print axioms Pandrosion444Base.retain_best #print axioms Pandrosion444Base.retain_success #print axioms Pandrosion444Base.budget_increment #print axioms Pandrosion444Base.positive_log_contract #print axioms Pandrosion444Base.clipped_log_contract #print axioms Pandrosion444Base.batched_log_contract #print axioms Pandrosion444Base.batch_budget #print axioms Pandrosion444Base.two_sided_precondition #print axioms Pandrosion444Base.compact_product_re #print axioms Pandrosion444Base.compact_product_im #print axioms Pandrosion444Base.scaled_squared_norm #print axioms Pandrosion444Exact.sumSquares_cast #print axioms Pandrosion444Exact.checkResidual_sound #print axioms Pandrosion444Exact.checkPositiveBracket_sound #print axioms Pandrosion444Exact.charge_sound #print axioms Pandrosion444Exact.boundedRun_preserves #print axioms Pandrosion444Audit.constant_nonzero_has_no_root #print axioms Pandrosion444Audit.no_universal_root_solver #print axioms Pandrosion444Audit.root_beyond_bounded_search #print axioms Pandrosion444Audit.decreasing_residual_strict #print axioms Pandrosion444Audit.decreasing_residual_above_one #print axioms Pandrosion444Audit.strict_descent_can_converge_to_nonzero #print axioms Pandrosion444Audit.residual_bound #print axioms Pandrosion444Audit.residual_converges #print axioms Pandrosion444Audit.perturbed_residual_bound #print axioms Pandrosion444Audit.iterate_converges_of_residual #print axioms Pandrosion444Exploration.decodeInt_encodeInt #print axioms Pandrosion444Exploration.decodeRat_encodeRat #print axioms Pandrosion444Exploration.decodeVec_encodeVec #print axioms Pandrosion444Exploration.seeds_dense #print axioms Pandrosion444Exploration.eventual_hit #print axioms Pandrosion444Exploration.interleaved_eventual_hit #print axioms Pandrosion444Exploration.best_le_current #print axioms Pandrosion444Exploration.best_antitone #print axioms Pandrosion444Exploration.best_nonnegative #print axioms Pandrosion444Exploration.best_finite_tolerance #print axioms Pandrosion444Exploration.best_residual_converges #print axioms Pandrosion444Exploration.best_witness #print axioms Pandrosion444Exploration.selected_points_converge #print axioms Pandrosion444Sphere.north_gap_identity #print axioms Pandrosion444Sphere.finite_points_exclude_north #print axioms Pandrosion444Sphere.roundtrip_component #print axioms Pandrosion444Sphere.sphere_identity #print axioms Pandrosion444Sphere.inverse_projection_on_sphere #print axioms Pandrosion444Sphere.root_equivalence #print axioms Pandrosion444Sphere.far_regions_near_pole /-! Exact arithmetic identities for the new scaled spherical chart. The finite floating-point search and the adaptive merit heuristics are not verified by these theorems. The coverage theorem explicitly assumes a fair infinite stream and uses the inherited exact rational enumeration. -/ namespace Pandrosion445Adaptive noncomputable section def height (t : ℝ) := (t-1)/(1+t) def horizontal (x t : ℝ) := 2*x/(1+t) theorem scaled_roundtrip (x scale t : ℝ) (hs : 0 < scale) (ht : 0 ≤ t) : scale * (horizontal (x/scale) t / (1-height t)) = x := by have hd : 1+t ≠ 0 := by linarith have hg : 1-height t ≠ 0 := by unfold height intro h have he : (t-1)/(1+t)=1 := by linarith have := (div_eq_iff hd).mp he linarith unfold horizontal height field_simp <;> ring theorem scaled_root_equivalence {ι Y : Type*} [Fintype ι] [Zero Y] (F : (ι → ℝ) → Y) (x scale : ι → ℝ) (hs : ∀ i, 0 < scale i) : let t := ∑ i, (x i/scale i)^2 F (fun i => scale i * (horizontal (x i/scale i) t / (1-height t)))=0 ↔ F x=0 := by dsimp only have ht : 0 ≤ ∑ i, (x i/scale i)^2 := Finset.sum_nonneg (fun _ _ => sq_nonneg _) have he : (fun i => scale i * (horizontal (x i/scale i) (∑ j, (x j/scale j)^2) / (1-height (∑ j, (x j/scale j)^2)))) = x := by funext i exact scaled_roundtrip _ _ _ (hs i) ht rw [he] theorem positive_scale_injective {ι : Type*} (scale : ι → ℝ) (hs : ∀ i, 0 < scale i) : Function.Injective (fun x : ι → ℝ => fun i => x i / scale i) := by intro x y h funext i have hi := congrFun h i change x i / scale i = y i / scale i at hi have hx : x i / scale i * scale i = x i := div_mul_cancel₀ _ (ne_of_gt (hs i)) have hy : y i / scale i * scale i = y i := div_mul_cancel₀ _ (ne_of_gt (hs i)) calc x i = x i / scale i * scale i := hx.symm _ = y i / scale i * scale i := by rw [hi] _ = y i := hy theorem reciprocal_horizontal (radius : ℝ) (hr : 0 < radius) : 2*radius/(1+radius^2) = 2*(1/radius)/(1+(1/radius)^2) := by have h1 : 1+radius^2 ≠ 0 := by positivity have h2 : 1+(1/radius)^2 ≠ 0 := by positivity field_simp <;> ring theorem reciprocal_height (radius : ℝ) (hr : 0 < radius) : height (radius^2) = 1-2*(1/radius)^2/(1+(1/radius)^2) := by have h1 : 1+radius^2 ≠ 0 := by positivity have h2 : 1+(1/radius)^2 ≠ 0 := by positivity unfold height field_simp <;> ring theorem finite_radius_not_north (radius : ℝ) : height (radius^2) < 1 := by unfold height apply (div_lt_iff₀ (by positivity : 0 < 1+radius^2)).mpr linarith theorem scaled_projection_unit {ι : Type*} [Fintype ι] (x scale : ι → ℝ) : let t := ∑ i, (x i/scale i)^2 (∑ i, (horizontal (x i/scale i) t)^2)+(height t)^2=1 := by dsimp only have ht : 0 ≤ ∑ i, (x i/scale i)^2 := Finset.sum_nonneg (fun _ _ => sq_nonneg _) have hd : 1+∑ i, (x i/scale i)^2 ≠ 0 := by linarith have hsum : (∑ i, (horizontal (x i/scale i) (∑ j, (x j/scale j)^2))^2) = 4*(∑ i, (x i/scale i)^2)/(1+∑ i, (x i/scale i)^2)^2 := by unfold horizontal simp_rw [div_pow, mul_pow] rw [← Finset.sum_div, ← Finset.mul_sum] simp only [div_pow] norm_num rw [hsum] unfold height field_simp ring /-- Independence from merit is an explicit fairness hypothesis. -/ theorem fair_stream_hits {n : ℕ} {E : Type*} [NormedAddCommGroup E] (seed : ℕ → Fin n → ℝ) (hdense : DenseRange seed) (stream : ℕ → Fin n → ℝ) (hfair : ∀ j, stream (5+4*j)=seed j) (F : (Fin n → ℝ) → E) (root : Fin n → ℝ) (hroot : F root=0) (hc : ContinuousAt F root) (epsilon : ℝ) (he : 0 < epsilon) : ∃ k, ‖F (stream k)‖ < epsilon := by have hmem : {x | ‖F x‖ < epsilon} ∈ nhds root := hc.norm.preimage_mem_nhds (Iio_mem_nhds (by simpa [hroot] using he)) obtain ⟨j, hj⟩ := hdense.mem_nhds hmem exact ⟨5+4*j, by rwa [hfair]⟩ end end Pandrosion445Adaptive #print axioms Pandrosion445Adaptive.scaled_roundtrip #print axioms Pandrosion445Adaptive.scaled_root_equivalence #print axioms Pandrosion445Adaptive.positive_scale_injective #print axioms Pandrosion445Adaptive.reciprocal_horizontal #print axioms Pandrosion445Adaptive.reciprocal_height #print axioms Pandrosion445Adaptive.finite_radius_not_north #print axioms Pandrosion445Adaptive.scaled_projection_unit #print axioms Pandrosion445Adaptive.fair_stream_hits #print axioms Pandrosion444Exact.boundedRun_preserves /-! Exact relations for 446. These are not a verification of the NumPy implementation, global optimal spherical configurations, or universal convergence. The openai/math family 090 inspired finite log-score selection; its planar/S^2 asymptotic theorems are not used in arbitrary dimension. -/ namespace Pandrosion446 noncomputable section theorem unit_chord_squared {ι : Type*} [Fintype ι] (x y : ι → ℝ) (hx : ∑ i, x i^2=1) (hy : ∑ i, y i^2=1) : (∑ i, (x i-y i)^2)=2-2*(∑ i, x i*y i) := by calc _ = (∑ i, x i^2)+(∑ i, y i^2)-2*(∑ i, x i*y i) := by rw [← Finset.sum_add_distrib, Finset.mul_sum, ← Finset.sum_sub_distrib] apply Finset.sum_congr rfl intro i _ ring _ = _ := by rw [hx,hy]; ring theorem clipped_chord_positive (floor distance : ℝ) (hfloor : 0 weights i*values i)=0 ↔ values=0 := by constructor · intro h funext i have he := congrFun h i change weights i*values i=0 at he exact (mul_eq_zero.mp he).resolve_left (ne_of_gt (hw i)) · intro h funext i simp [h] theorem two_sided_real_model (a q col row : ℝ) (hc : col≠0) (hr : row≠0) : ((a/col)/row)*q*row=a*(q/col) := by field_simp theorem absolute_filter_energy (c : ℝ) (z : ℂ) : Complex.normSq ((c:ℂ)*z)=c^2*Complex.normSq z := by rw [Complex.normSq_mul] simp [Complex.normSq,pow_two] theorem absolute_spectral_energy {ι : Type*} [Fintype ι] (c : ι → ℝ) (z : ι → ℂ) : (∑ i, Complex.normSq ((c i:ℂ)*z i))=∑ i, c i^2*Complex.normSq (z i) := by apply Finset.sum_congr rfl intro i _ exact absolute_filter_energy _ _ def run {S : Type*} (step : S → Option S) : ℕ → S → S | 0, s => s | n+1, s => match step s with | none => s | some next => run step n next /-- Complete-state continuation, for a deterministic exact transition. The floating Python engine and its callback evaluation scheduling are separate. -/ theorem resumed_run_equals_unsplit {S : Type*} (step : S → Option S) (n m : ℕ) (s : S) : run step (n+m) s=run step m (run step n s) := by induction n generalizing s with | zero => simp [run] | succ n ih => rw [Nat.succ_add] simp only [run] cases he : step s with | none => have hh : ∀ k, run step k s=s := by intro k cases k <;> simp [run,he] simp [hh] | some next => simpa only [he] using ih next theorem run_preserves_best {S : Type*} (step : S → Option S) (best : S → ℝ) (h : ∀ s t, step s=some t → best t≤best s) (n : ℕ) (s : S) : best (run step n s)≤best s := by induction n generalizing s with | zero => simp [run] | succ n ih => simp only [run] cases he : step s with | none => simp | some next => simpa [he] using (ih next).trans (h s next he) /-- Fixed point existence and nonexpansiveness alone do not give contraction of the iteration error. This elementary example does not refute family 328. -/ theorem nonexpansive_fixed_point_without_error_reduction : (∀ x y : ℝ, |(-x)-(-y)|=|x-y|) ∧ (-(0:ℝ)=0) ∧ (∀ x : ℝ, |-x|=|x|) ∧ (-( -(1:ℝ))=1) := by refine ⟨?_, by norm_num, ?_, by norm_num⟩ · intro x y rw [show (-x)-(-y)=-(x-y) by ring,abs_neg] · exact fun x => abs_neg x end end Pandrosion446 #print axioms Pandrosion446.unit_chord_squared #print axioms Pandrosion446.clipped_chord_positive #print axioms Pandrosion446.selected_energy_no_worse #print axioms Pandrosion446.positive_row_scaling_zero_iff #print axioms Pandrosion446.two_sided_real_model #print axioms Pandrosion446.absolute_filter_energy #print axioms Pandrosion446.absolute_spectral_energy #print axioms Pandrosion446.resumed_run_equals_unsplit #print axioms Pandrosion446.run_preserves_best #print axioms Pandrosion446.nonexpansive_fixed_point_without_error_reduction /-! Exact identities supporting the single 447 model. This file does not verify Python, NumPy, rounding, arbitrary callbacks or universal convergence. The ETH manuscript is not imported and its counting theorem is not applied to continuous black-box systems. -/ namespace Pandrosion447 noncomputable section theorem positive_rows_preserve_roots {ι : Type*} (f weights : ι → ℝ) (positive : ∀ i, 0 < weights i) : (∀ i, f i / weights i = 0) ↔ (∀ i, f i = 0) := by constructor · intro h i exact (div_eq_zero_iff.mp (h i)).resolve_right (ne_of_gt (positive i)) · intro h i rw [h i, zero_div] theorem scaled_linear_model {ι κ : Type*} [Fintype κ] (J : ι → κ → ℝ) (p : κ → ℝ) (f weights : ι → ℝ) (positive : ∀ i, 0 < weights i) (i : ι) : (∑ j, J i j / weights i * p j) + f i / weights i = 0 ↔ (∑ j, J i j * p j) + f i = 0 := by have factor : (∑ j, J i j / weights i * p j) + f i / weights i = ((∑ j, J i j * p j) + f i) / weights i := by simp_rw [div_mul_eq_mul_div] rw [add_div, Finset.sum_div] rw [factor, div_eq_zero_iff] simp [ne_of_gt (positive i)] theorem rectangular_inverse_secant {ι κ : Type*} [Fintype κ] (H : ι → κ → ℂ) (s : ι → ℂ) (y row : κ → ℂ) (nonzero : (∑ j, row j * y j) ≠ 0) (i : ι) : (∑ j, (H i j + (s i - ∑ k, H i k * y k) * row j / (∑ k, row k * y k)) * y j) = s i := by simp_rw [add_mul] rw [Finset.sum_add_distrib] have factor : (∑ j, (s i - ∑ k, H i k * y k) * row j / (∑ k, row k * y k) * y j) = (s i - ∑ k, H i k * y k) * (∑ j, row j * y j) / (∑ k, row k * y k) := by rw [Finset.mul_sum, Finset.sum_div] apply Finset.sum_congr rfl intro j _ ring rw [factor, mul_div_cancel_right₀ _ nonzero] ring theorem weighted_acceptance_decreases (oldMerit newMerit predicted eta : ℝ) (predictedPositive : 0 < predicted) (etaPositive : 0 < eta) (accepted : eta < (oldMerit-newMerit)/predicted) : newMerit < oldMerit := by have h := (lt_div_iff₀ predictedPositive).mp accepted have hp := mul_pos etaPositive predictedPositive linarith theorem retained_best_survives_nonmonotone_trial (best trial : ℝ) : min best trial ≤ best ∧ min best trial ≤ trial := ⟨min_le_left _ _, min_le_right _ _⟩ theorem initial_radius_cap (requested scale : ℝ) (requestPositive : 0 < requested) (scalePositive : 0 < scale) : 0 < min requested scale ∧ min requested scale ≤ scale := by exact ⟨lt_min requestPositive scalePositive, min_le_right _ _⟩ theorem geometric_extrapolation (x root ratio : ℝ) (notOne : ratio ≠ 1) : x + ((1-ratio)*(root-x))/(1-ratio) = root := by have h : 1-ratio ≠ 0 := sub_ne_zero.mpr (Ne.symm notOne) field_simp ring theorem dual_verification (central forward tolerance : ℝ) (verified : max |central| |forward| ≤ tolerance) : |central| ≤ tolerance ∧ |forward| ≤ tolerance := ⟨(le_max_left _ _).trans verified, (le_max_right _ _).trans verified⟩ theorem midpoint_minimizes_bias_lower_bound (gradient bias : ℝ) : |bias| / 2 ≤ max |gradient| |gradient+bias| := by have triangle : |bias| ≤ |gradient| + |gradient+bias| := by calc |bias| = |(gradient+bias)-gradient| := by congr 1; ring _ ≤ |gradient+bias| + |gradient| := abs_sub _ _ _ = _ := by ring have a := le_max_left |gradient| |gradient+bias| have b := le_max_right |gradient| |gradient+bias| linarith theorem midpoint_attains_bias_lower_bound (bias : ℝ) : max |(-bias/2)| |(-bias/2)+bias| = |bias|/2 := by have a : |(-bias/2)| = |bias|/2 := by rw [abs_div, abs_neg]; norm_num have b : |(-bias/2)+bias| = |bias|/2 := by have h : (-bias/2)+bias = bias/2 := by ring rw [h, abs_div]; norm_num rw [a,b,max_self] theorem objective_equivalence_bound (oldNorm newNorm slack : ℝ) (bounded : newNorm ≤ oldNorm*(1+slack)) : newNorm-oldNorm ≤ oldNorm*slack := by nlinarith end end Pandrosion447 #print axioms Pandrosion447.positive_rows_preserve_roots #print axioms Pandrosion447.scaled_linear_model #print axioms Pandrosion447.rectangular_inverse_secant #print axioms Pandrosion447.weighted_acceptance_decreases #print axioms Pandrosion447.retained_best_survives_nonmonotone_trial #print axioms Pandrosion447.initial_radius_cap #print axioms Pandrosion447.geometric_extrapolation #print axioms Pandrosion447.dual_verification #print axioms Pandrosion447.midpoint_minimizes_bias_lower_bound #print axioms Pandrosion447.midpoint_attains_bias_lower_bound #print axioms Pandrosion447.objective_equivalence_bound /-! Exact mathematical bounds supporting the 448 rounding-aware search. These statements do not model IEEE-754, establish callback derivative bounds, verify NumPy, or prove convergence for arbitrary finite-budget root requests. No openai/math theorem is imported as a numerical convergence guarantee. -/ namespace Pandrosion448 noncomputable section /-- Componentwise perturbation bound for an exact complex linear model. -/ theorem coordinate_resolution_bound {ι : Type*} [Fintype ι] (a delta : ι → ℂ) (radius : ι → ℝ) (bounded : ∀ j, ‖delta j‖ ≤ radius j) : ‖∑ j, a j * delta j‖ ≤ ∑ j, ‖a j‖ * radius j := by calc ‖∑ j, a j * delta j‖ ≤ ∑ j, ‖a j * delta j‖ := norm_sum_le _ _ _ = ∑ j, ‖a j‖ * ‖delta j‖ := by simp_rw [norm_mul] _ ≤ ∑ j, ‖a j‖ * radius j := by exact Finset.sum_le_sum (fun j _ => mul_le_mul_of_nonneg_left (bounded j) (norm_nonneg _)) /-- A linearized rounding footprint must be augmented by a nonlinear remainder. -/ theorem perturbation_with_remainder {ι : Type*} [Fintype ι] (a delta : ι → ℂ) (radius : ι → ℝ) (error : ℂ) (eta : ℝ) (bounded : ∀ j, ‖delta j‖ ≤ radius j) (remainder : ‖error‖ ≤ eta) : ‖(∑ j, a j * delta j) + error‖ ≤ (∑ j, ‖a j‖ * radius j) + eta := by exact (norm_add_le _ _).trans (add_le_add (coordinate_resolution_bound a delta radius bounded) remainder) /-- Relating computed and ideal residuals requires an independently supplied error bound. -/ theorem ideal_residual_bound {E : Type*} [SeminormedAddCommGroup E] (ideal computed : E) (error tolerance : ℝ) (evaluationError : ‖ideal-computed‖ ≤ error) (margin : ‖computed‖ + error ≤ tolerance) : ‖ideal‖ ≤ tolerance := by calc ‖ideal‖ = ‖(ideal-computed)+computed‖ := by congr 1; abel _ ≤ ‖ideal-computed‖ + ‖computed‖ := norm_add_le _ _ _ ≤ error + ‖computed‖ := by linarith _ ≤ tolerance := by linarith /-- A coordinate trial is accepted only on measured physical merit improvement. -/ theorem accepted_poll_improves_best (best measured : ℝ) (accepted : measured < best) : min best measured = measured ∧ min best measured < best := by rw [min_eq_right (le_of_lt accepted)] exact ⟨rfl, accepted⟩ /-- Local polls share both the remaining physical budget and their own quota. -/ theorem bounded_poll_budget (used spent total quota : ℕ) (physical : used + spent ≤ total) (quotaBound : spent ≤ quota) : used ≤ total ∧ spent ≤ total-used ∧ spent ≤ quota := by omega /-- The conservative sphere-start radius remains inside the caller's trust ball. -/ theorem conservative_sphere_radius (requested scale : ℝ) (requestPositive : 0 < requested) (scalePositive : 0 < scale) : 0 < min requested scale ∧ min requested scale ≤ requested ∧ min requested scale ≤ scale := by exact ⟨lt_min requestPositive scalePositive, min_le_left _ _, min_le_right _ _⟩ /-- Positive diagonal coordinate changes preserve exact zeros in both directions. -/ theorem invertible_coordinate_change {ι : Type*} (F : (ι → ℝ) → ℝ) (center scale u : ι → ℝ) (nonzero : ∀ j, scale j ≠ 0) : F (fun j => center j + scale j * ((u j-center j)/scale j)) = 0 ↔ F u = 0 := by have recover : (fun j => center j + scale j * ((u j-center j)/scale j)) = u := by funext j field_simp [nonzero j] ring rw [recover] end end Pandrosion448 #print axioms Pandrosion448.coordinate_resolution_bound #print axioms Pandrosion448.perturbation_with_remainder #print axioms Pandrosion448.ideal_residual_bound #print axioms Pandrosion448.accepted_poll_improves_best #print axioms Pandrosion448.bounded_poll_budget #print axioms Pandrosion448.conservative_sphere_radius #print axioms Pandrosion448.invertible_coordinate_change /-! Exact resource-allocation facts for the 449 local-poll quota. They do not verify Python/NumPy or prove convergence for arbitrary callbacks. -/ namespace Pandrosion449 /-- A more accurate candidate cannot receive a smaller quota in the two-tier policy. -/ theorem precision_quota_antitone (fine coarse threshold : ℝ) (early total : ℕ) (precision : fine ≤ coarse) (quotas : early ≤ total) : (if threshold < coarse then early else total) ≤ (if threshold < fine then early else total) := by by_cases hf : threshold < fine · have hc : threshold < coarse := lt_of_lt_of_le hf precision simp [hf, hc] · by_cases hc : threshold < coarse · simpa [hf, hc] using quotas · simp [hf, hc] /-- The early quota leaves the promised capacity inside the original total budget. -/ theorem reserved_capacity (used early reserve total : ℕ) (spent : used ≤ early) (split : early + reserve ≤ total) : reserve ≤ total-used := by omega end Pandrosion449 #print axioms Pandrosion449.precision_quota_antitone #print axioms Pandrosion449.reserved_capacity