diff --git a/inbox/archive/2026-02-00-yamamoto-full-formal-arrow-impossibility.md b/inbox/archive/2026-02-00-yamamoto-full-formal-arrow-impossibility.md
index fe5851b6..731d4c75 100644
--- a/inbox/archive/2026-02-00-yamamoto-full-formal-arrow-impossibility.md
+++ b/inbox/archive/2026-02-00-yamamoto-full-formal-arrow-impossibility.md
@@ -7,9 +7,14 @@ date: 2026-02-01
 domain: ai-alignment
 secondary_domains: [critical-systems]
 format: paper
-status: unprocessed
+status: null-result
 priority: medium
 tags: [arrows-theorem, formal-proof, proof-calculus, social-choice]
+processed_by: theseus
+processed_date: 2026-03-11
+enrichments_applied: ["safe AI development requires building alignment mechanisms before scaling capability.md"]
+extraction_model: "anthropic/claude-sonnet-4.5"
+extraction_notes: "Pure formal verification work with no direct AI alignment connection in the paper itself. Strengthens mathematical foundation for existing Arrow's impossibility claims by providing machine-checkable proof. No new claims warranted—this is infrastructure for existing arguments rather than novel insight."
 ---
 
 ## Content
@@ -30,3 +35,9 @@ Key contribution: meticulous derivation revealing the global structure of the so
 PRIMARY CONNECTION: universal alignment is mathematically impossible because Arrows impossibility theorem applies to aggregating diverse human preferences into a single coherent objective
 WHY ARCHIVED: Provides formal verification foundation for our Arrow's impossibility claim
 EXTRACTION HINT: Likely enrichment to existing claim rather than standalone — add as evidence that Arrow's theorem is now formally machine-verifiable
+
+
+## Key Facts
+- Arrow's impossibility theorem received full formal representation using proof calculus (Yamamoto, PLOS One, February 2026)
+- Formal proof complements AAAI 2008 computer-aided proofs and Condorcet's paradox simplifications
+- Proof reveals global structure of social welfare function central to the theorem