diff --git a/domains/ai-alignment/safe AI development requires building alignment mechanisms before scaling capability.md b/domains/ai-alignment/safe AI development requires building alignment mechanisms before scaling capability.md
index 09030349..d378e352 100644
--- a/domains/ai-alignment/safe AI development requires building alignment mechanisms before scaling capability.md	
+++ b/domains/ai-alignment/safe AI development requires building alignment mechanisms before scaling capability.md	
@@ -21,6 +21,12 @@ This phased approach is also a practical response to the observation that since
 
 Anthropic's RSP rollback demonstrates the opposite pattern in practice: the company scaled capability while weakening its pre-commitment to adequate safety measures. The original RSP required guaranteeing safety measures were adequate *before* training new systems. The rollback removes this forcing function, allowing capability development to proceed with safety work repositioned as aspirational ('we hope to create a forcing function') rather than mandatory. This provides empirical evidence that even safety-focused organizations prioritize capability scaling over alignment-first development when competitive pressure intensifies, suggesting the claim may be normatively correct but descriptively violated by actual frontier labs under market conditions.
 
+
+### Additional Evidence (extend)
+*Source: [[2026-02-00-yamamoto-full-formal-arrow-impossibility]] | Added: 2026-03-12 | Extractor: anthropic/claude-sonnet-4.5*
+
+Arrow's impossibility theorem now has a full formal representation using proof calculus in formal logic (Yamamoto, PLOS One, February 2026). This provides machine-checkable verification of the theorem's validity, strengthening the mathematical foundation underlying claims that universal alignment is impossible. The formal proof complements existing computer-aided proofs (AAAI 2008) and simplified proofs via Condorcet's paradox, but provides the first complete logical representation that can be mechanically verified. This moves Arrow's theorem from 'mathematical argument' to 'formally verified result' in the context of alignment constraints.
+
 ---
 
 Relevant Notes:
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..512b61cf 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: enrichment
 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. Provides mathematical foundation strengthening existing Arrow's impossibility claims in the KB. No new claims warranted - this is methodological advancement (formal proof) of an already-established theorem, not a novel proposition about alignment."
 ---
 
 ## 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)
+- The formal proof reveals the global structure of the social welfare function central to the theorem
+- This complements existing computer-aided proofs from AAAI 2008 and simplified proofs via Condorcet's paradox