diff --git a/0-Core-Formalism/lean/Semantics/Semantics.lean b/0-Core-Formalism/lean/Semantics/Semantics.lean
index a13d13ed..571b783b 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics.lean
@@ -218,6 +218,7 @@ import Semantics.NKHodgeFAMM
 import Semantics.Goxel
 import Semantics.N3L_Energy
 import Semantics.SieveLemmas
+import Semantics.InteractionGraphSidon
 
 namespace Semantics
 
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/InteractionGraphSidon.lean b/0-Core-Formalism/lean/Semantics/Semantics/InteractionGraphSidon.lean
new file mode 100644
index 00000000..72bc270f
--- /dev/null
+++ b/0-Core-Formalism/lean/Semantics/Semantics/InteractionGraphSidon.lean
@@ -0,0 +1,191 @@
+/-
+InteractionGraphSidon.lean — RRC weak-axis reconstruction via interaction-graph freeness
+
+The atproto/Mastodon observation (and the RRC "weak axis" problem) are the same
+abstract structure: an object's full identity/classification is hidden from any
+single partial view.  Multiple independent weak projections must be reconciled
+via a CRT/Sidon-type uniqueness condition.
+
+This module formalizes:
+
+1. Interaction graphs as finite typed-transition systems.
+2. Word products in the matrix semigroup generated by typed edges.
+3. A bounded Sidon witness: all words up to length L are distinct.
+4. RRC weak axes as sieve projections of an underlying classification.
+5. Reconstruction: independent weak axes recover the underlying class
+   uniquely modulo their product — the "weak-portion is the atproto problem".
+
+All computation uses rational matrices; no Float is used in the compute path.
+-/
+
+import Mathlib.Data.Matrix.Basic
+import Mathlib.Data.Matrix.Mul
+import Mathlib.Data.Finset.Basic
+import Mathlib.Data.List.FinRange
+import Mathlib.Tactic
+
+namespace Semantics.InteractionGraphSidon
+
+open Matrix Finset List
+
+-- ═══════════════════════════════════════════════════════════════════════════
+-- §1  Typed interaction graphs and word products
+-- ═══════════════════════════════════════════════════════════════════════════
+
+/-- A typed interaction graph on `n` nodes with edge types indexed by `ι`. -/
+structure InteractionGraph (ι : Type) (n : Nat) where
+  nodeCount : Nat := n
+  edgeTypes : Finset ι
+  gen : ι → Matrix (Fin n) (Fin n) Rat
+
+/-- Word product: multiply generator matrices in the order of the word.
+    The empty word is the identity matrix. -/
+def wordProduct {ι : Type} {n : Nat} (g : InteractionGraph ι n) (w : List ι) :
+    Matrix (Fin n) (Fin n) Rat :=
+  w.foldl (fun M t => M * g.gen t) 1
+
+/-- A bounded Sidon witness: no two distinct words of length ≤ L collapse to
+    the same matrix.  This is the finite, checkable version of semigroup
+    freeness; the full infinite property is the limit as L → ∞. -/
+def isSidonWitness {ι : Type} [DecidableEq ι]
+    (g : InteractionGraph ι n) (L : Nat) : Prop :=
+  ∀ w1 w2 : List ι,
+    w1.length ≤ L → w2.length ≤ L →
+    wordProduct g w1 = wordProduct g w2 → w1 = w2
+
+-- ═══════════════════════════════════════════════════════════════════════════
+-- §2  RRC weak axes as independent projections
+-- ═══════════════════════════════════════════════════════════════════════════
+
+/-- A weak axis is a sieve modulus: a partial observation of an underlying
+    RRC class.  In RRC terms, each weak axis is one independent reason the
+    classifier cannot commit to a single label; the axis records the residue
+    of the true class modulo `modulus`. -/
+structure WeakAxis where
+  modulus : Nat
+  pos : modulus > 0
+  deriving Repr
+
+/-- Project an underlying class through a weak axis. -/
+def project (a : WeakAxis) (cls : Nat) : Nat := cls % a.modulus
+
+/-- Two weak axes are independent when their moduli are coprime.
+    Independence is the analogue of atproto's separation of identity,
+    hosting, and application: no axis is a refinement of another. -/
+def independentAxes (a b : WeakAxis) : Prop :=
+  Nat.Coprime a.modulus b.modulus
+
+instance {a b : WeakAxis} : Decidable (independentAxes a b) := by
+  unfold independentAxes; infer_instance
+
+/-- Reconstruct the underlying class modulo m₁·m₂ from two independent
+    weak-axis observations via CRT. -/
+def reconstructWeakAxes (a b : WeakAxis) (r1 r2 : Nat)
+    (hc : independentAxes a b) : Nat :=
+  (Nat.chineseRemainder hc r1 r2).val
+
+/-- Correctness modulo the first weak axis. -/
+theorem reconstructWeakAxes_mod_a (a b : WeakAxis) (r1 r2 : Nat)
+    (hc : independentAxes a b) :
+    reconstructWeakAxes a b r1 r2 hc % a.modulus = r1 % a.modulus := by
+  simp [reconstructWeakAxes]
+  exact (Nat.chineseRemainder hc r1 r2).property.left
+
+/-- Correctness modulo the second weak axis. -/
+theorem reconstructWeakAxes_mod_b (a b : WeakAxis) (r1 r2 : Nat)
+    (hc : independentAxes a b) :
+    reconstructWeakAxes a b r1 r2 hc % b.modulus = r2 % b.modulus := by
+  simp [reconstructWeakAxes]
+  exact (Nat.chineseRemainder hc r1 r2).property.right
+
+/-- Two independent weak-axis observations uniquely determine the underlying
+    class modulo the product of their moduli.  This is the RRC weak-axis
+    analogue of depth_token_coprime_intersect in SieveLemmas.lean. -/
+theorem weakAxis_coprime_intersect
+    (a b : WeakAxis) (cls : Nat) (hc : independentAxes a b) :
+    let r1 := project a cls
+    let r2 := project b cls
+    reconstructWeakAxes a b r1 r2 hc % (a.modulus * b.modulus) =
+      cls % (a.modulus * b.modulus) := by
+  intro r1 r2
+  have h1 : reconstructWeakAxes a b r1 r2 hc % a.modulus = cls % a.modulus := by
+    rw [reconstructWeakAxes_mod_a a b r1 r2 hc]
+    simp [project, r1]
+  have h2 : reconstructWeakAxes a b r1 r2 hc % b.modulus = cls % b.modulus := by
+    rw [reconstructWeakAxes_mod_b a b r1 r2 hc]
+    simp [project, r2]
+  exact (Nat.modEq_and_modEq_iff_modEq_mul hc).mp ⟨h1, h2⟩
+
+-- ═══════════════════════════════════════════════════════════════════════════
+-- §3  The atproto connection (informal→formal bridge)
+-- ═══════════════════════════════════════════════════════════════════════════
+
+/-  The atproto design says:
+
+      identity  (D)  ≠  hosting projection  (H)  ≠  application projection (A)
+
+    In RRC terms this is exactly a set of weak axes that are independent:
+    no single axis determines the full classification; the full object is
+    recovered only by reconciling independent partial observations.
+
+    We encode this as a tiny concrete instance below.
+-/
+
+/-- A toy atproto-style observer set: identity/host/app are three independent
+    weak axes with pairwise-coprime moduli 7, 11, 13. -/
+def identityAxis : WeakAxis := ⟨7, by decide⟩
+def hostingAxis  : WeakAxis := ⟨11, by decide⟩
+def appAxis      : WeakAxis := ⟨13, by decide⟩
+
+/-- Any underlying class, observed through the three axes. -/
+def toyClass : Nat := 61
+
+def idShadow    : Nat := project identityAxis toyClass
+def hostShadow  : Nat := project hostingAxis toyClass
+def appShadow   : Nat := project appAxis toyClass
+
+#eval idShadow    -- 61 % 7 = 5
+#eval hostShadow  -- 61 % 11 = 6
+#eval appShadow   -- 61 % 13 = 9
+
+-- Reconstruct class mod 7·11 = 77 from identity + hosting axes.
+def reconstructedTwo : Nat :=
+  reconstructWeakAxes identityAxis hostingAxis idShadow hostShadow (by decide)
+
+#eval! reconstructedTwo  -- 61
+
+-- Reconstruct class mod 7·11·13 = 1001 from all three axes.
+def reconstructedThree : Nat :=
+  let r := reconstructWeakAxes identityAxis hostingAxis idShadow hostShadow (by decide)
+  let combinedMod := identityAxis.modulus * hostingAxis.modulus
+  let combinedAxis : WeakAxis := ⟨combinedMod, by decide⟩
+  reconstructWeakAxes combinedAxis appAxis r appShadow (by decide)
+
+#eval! reconstructedThree  -- 61
+
+-- ═══════════════════════════════════════════════════════════════════════════
+-- §4  A bounded Sidon witness for a concrete interaction graph
+-- ═══════════════════════════════════════════════════════════════════════════
+
+/-- Two-node, two-type interaction graph.
+    Type 0: edge 1→2 with weight 1
+    Type 1: edge 2→1 with weight 1
+    This is the simplest graph whose path words encode direction changes. -/
+def toyGraph : InteractionGraph (Fin 2) 2 where
+  edgeTypes := {0, 1}
+  gen t :=
+    if t = 0 then
+      !![(0 : Rat), 1; 0, 0]  -- 1→2
+    else
+      !![0, 0; 1, 0]          -- 2→1
+
+#eval wordProduct toyGraph []       -- identity
+#eval wordProduct toyGraph [0]      -- 1→2
+#eval wordProduct toyGraph [0, 1]   -- 1→2→1
+#eval wordProduct toyGraph [0, 1, 0] -- 1→2→1→2
+
+-- This is a meta-theorem stating the property; the actual witness for L=4
+-- can be checked by native_decide or enumeration in a future tactic.
+#check isSidonWitness toyGraph 4
+
+end Semantics.InteractionGraphSidon