  77    Exists x := ⟨hpos, hdef⟩
  78
  79/-- **Law of Existence (Biconditional)**: x exists ⟺ defect collapses. -/
  80theorem law_of_existence (x : ℝ) : Exists x ↔ DefectCollapse x :=
  81  ⟨fun ⟨hpos, hdef⟩ => ⟨hpos, hdef⟩, fun ⟨hpos, hdef⟩ => ⟨hpos, hdef⟩⟩
  82
  83/-- **Existence Characterization**: x exists ⟺ x = 1. -/
  84theorem exists_iff_unity {x : ℝ} (hx : 0 < x) : Exists x ↔ x = 1 :=
  85  ⟨fun ⟨_, hdef⟩ => (defect_zero_iff_one hx).mp hdef,
  86   fun h => ⟨hx, (defect_zero_iff_one hx).mpr h⟩⟩
  87
  88/-- **Unity is Unique Existent**: ∀ x, Exists x ⟺ x = 1. -/
  89theorem unity_unique_existent : ∀ x : ℝ, Exists x ↔ x = 1 := by
  90  intro x
  91  constructor
  92  · intro ⟨hpos, hdef⟩; exact (defect_zero_iff_one hpos).mp hdef
  93  · intro h; subst h; exact ⟨one_pos, defect_at_one⟩
  94
  95/-- Alias for `defect_at_one`. -/
  96theorem defect_one : defect 1 = 0 := defect_at_one
  97
  98/-- Defect is strictly positive for x ≠ 1. -/
  99theorem defect_pos_of_ne_one {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) : 0 < defect x := by
 100  have h_nn := defect_nonneg hx
 101  have h_ne_zero : defect x ≠ 0 := fun h => hne ((defect_zero_iff_one hx).mp h)
 102  exact lt_of_le_of_ne h_nn (Ne.symm h_ne_zero)
 103
 104/-! ## Nothing Cannot Exist: J(0) → ∞ -/
 105
 106/-- As x → 0⁺, defect(x) → +∞.
 107
 108Technical proof: J(x) = (x + 1/x)/2 - 1 ≥ 1/(2x) - 1 → +∞ as x → 0⁺. -/
 109theorem defect_tendsto_atTop_at_zero :
 110    Filter.Tendsto defect (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop := by

papers checked against this theorem (showing 9 of 9)

No LLM agent tops 60% on new safety benchmark
unclear · 2412.14470

"Our evaluation of 16 popular LLM agents reveals a concerning result: none of the agents achieves a safety score above 60%."
DINO reaches 49.4 AP on COCO in 12 epochs via refined DETR denoising
unclear · 2203.03605

"DINO improves over previous DETR-like models in performance and efficiency by using a contrastive way for denoising training, a mixed query selection method for anchor initialization, and a look forward twice scheme for box prediction"
Intelligence is skill-acquisition efficiency, not task performance
echoes · 1911.01547

"We then articulate a new formal definition of intelligence based on Algorithmic Information Theory, describing intelligence as skill-acquisition efficiency and highlighting the concepts of scope, generalization difficulty, priors, and experience."
Survey organizes in-context learning techniques and challenges
unclear · 2301.00234

"The key idea of in-context learning is to learn from analogy. Figure 1 gives an example that describes how language models make decisions via ICL."
Curated skills raise agent pass rates by 16 points on average
unclear · 2602.12670

"Curated Skills raise average pass rate by 16.2 percentage points(pp), but effects vary widely by domain (+4.5pp for Software Engineering to +51.9pp for Healthcare) and 16 of 84 tasks show negative deltas."
Stochastic interpolants bridge any two densities exactly
echoes · 2303.08797

"stochastic interpolants to bridge any two probability density functions exactly in finite time"
Language models learn to call external tools themselves
unclear · 2302.04761

"We introduce Toolformer, a model trained to decide which APIs to call, when to call them, what arguments to pass, and how to best incorporate the results into future token prediction. This is done in a self-supervised way, requiring nothing more than a handful of demonstrations for each API."
Adam: one optimizer, one default setting, many models
unclear · 1412.6980

"We propose Adam, a method for efficient stochastic optimization that only requires first-order gradients with little memory requirement."
A 16-rule constitution replaces human harm labels in RLHF
unclear · 2212.08073

"These principles were chosen in a fairly ad hoc and iterative way for research purposes... such principles should be redeveloped and refined by a larger set of stakeholders"