law_of_existence
Existence is forced by distinction. The first move of the chain.
plain-language theorem explainer
The biconditional equates the Exists predicate to DefectCollapse for any real x. Foundation researchers cite this when moving between the structure form of existence and the conjunction form of defect collapse. The term proof directly identifies the two predicates by matching their shared positivity and zero-defect components.
Claim. For a real number $x$, $x$ exists if and only if defect collapses, where existence means $0 < x$ and defect$(x) = 0$, and defect collapse is the conjunction $0 < x$ and defect$(x) = 0$.
background
The Law of Existence module supplies a sharp formalization of the statement that $x$ exists precisely when defect$(x) = 0$. The Exists structure packages the two conditions $0 < x$ and defect $x = 0$. DefectCollapse is the definitionally identical conjunction of the same two conditions.
proof idea
The term proof constructs the equivalence by sending the Exists structure constructor to the DefectCollapse pair and back. No lemmas are invoked because the two predicates contain exactly the same data.
why it matters
This equivalence is the second key theorem listed in the module and feeds directly into CostAxioms.law_of_existence (which concludes Exists $x$ iff $x = 1$) and unity_is_unique_existent. It bridges the defect formulation used here to the J-cost minimum at unity that appears in the upstream CostAxioms definition of existence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 17 of 17)
-
Clinical agent benchmark drops LLM accuracy to under 10% of MedQA
"To further scrutinize our clinical simulations, we leverage real-world electronic health records, perform a clinical reader study, perturb agents with biases, and explore novel patient-centric metrics"
-
Space interferometer to survey micro-Hz gravitational waves
"Yet many outstanding questions related to astrophysics and cosmology are best answered by GW observations in this band."
-
Matrix states and dynamic recurrence improve RWKV performance
"We trained four Eagle models, ranging from 0.46 to 7.5 billion parameters, and two Finch models with 1.6 and 3.1 billion parameters and find that they achieve competitive performance across a wide variety of benchmarks."
-
Agents evolve at runtime by reinforcing episodic memory strategies
"we propose MEMRL, a non-parametric approach that evolves via reinforcement learning on episodic memory. By decoupling stable reasoning from plastic memory, MEMRL employs a Two-Phase Retrieval mechanism to filter noise and identify high-utility strategies through environmental feedback."
-
Frontier models scheme to disable oversight and exfiltrate weights
"Our results show that o1, Claude 3.5 Sonnet, Claude 3 Opus, Gemini 1.5 Pro, and Llama 3.1 405B all demonstrate in-context scheming capabilities. They recognize scheming as a viable strategy and readily engage in such behavior."
-
7B models process million-token videos and texts
"To address the scarcity of long-form conversational datasets, we developed a model-based question-answering technique, where a short-context model generates training data from books"
-
AI-generated dialogues scale LLaMA past Vicuna
"We first provide a systematically designed, diverse, informative, large-scale dataset of instructional conversations, UltraChat, which does not involve human queries. Our objective is to capture the breadth of interactions that a human might have with an AI assistant and employs a comprehensive framework to generate multi-turn conversation iteratively."
-
LLMs rate low-perplexity text higher than humans
"We propose a new metric to quantify self-preference bias in LLMs"
-
No LLM agent tops 60% on new safety benchmark
"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
"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
"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
"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
"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
"stochastic interpolants to bridge any two probability density functions exactly in finite time"
-
Language models learn to call external tools themselves
"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
"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
"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"