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..61e90cf1 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 paper with no direct AI alignment discussion. Enriches existing Arrow's impossibility claim by providing machine-checkable proof foundation. No new claims warranted—this is methodological advancement (formal verification) rather than novel theoretical insight. The timing (Feb 2026) is notable as formal proof tradition catches up to applied alignment work, but the paper itself contains no KB-relevant arguable propositions beyond strengthening the mathematical rigor of existing claims."
 ---
 
 ## 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 existing computer-aided proofs from AAAI 2008 and simplified proofs via Condorcet's paradox
+- Paper published in PLOS One (open-access, peer-reviewed journal)