diff --git a/0-Core-Formalism/lean/Semantics/Semantics/RRC/PolyFactorIdentity.lean b/0-Core-Formalism/lean/Semantics/Semantics/RRC/PolyFactorIdentity.lean
new file mode 100644
index 00000000..bddddb35
--- /dev/null
+++ b/0-Core-Formalism/lean/Semantics/Semantics/RRC/PolyFactorIdentity.lean
@@ -0,0 +1,387 @@
+/-
+Copyright (c) 2026 Research Stack Contributors. All rights reserved.
+Released under Apache 2.0 license.
+-/
+import Semantics.FixedPoint
+import Semantics.E8Sidon
+
+/-!
+# Polynomial Factor Identity — Short-Sleeve Detection for RRC
+
+This module applies the integer-to-polynomial decomposition technique
+(Trail of Bits, "short-sleeve" RSA factoring, 2026) as a classification
+feature for the Rainbow Raccoon Compiler identity step.
+
+## Core Insight
+
+When mathematical objects are accessed via zerocopy (mmap, shared memory,
+framebuffer DMA), their raw limb structure is already exposed. Checking
+for structured zero-blocks ("short-sleeve" patterns) is essentially free
+at that boundary. When sparsity is detected, it flags the object for
+deeper polynomial-based structural analysis.
+
+## Architecture
+
+```
+Zerocopy boundary (raw limbs exposed)
+    │
+    ├── limbDecompose(n, base) → coefficient array
+    │
+    ├── coeffSparsity → fraction of zero coefficients (Q16_16)
+    │       │
+    │       └── shortSleeveDetected? (sparsity > threshold)
+    │               │
+    │               └── YES → compute full PolySignature
+    │                         (degree, maxCoeff, coeffVariance, gcdCoeffs)
+    │
+    └── PolySignature feeds into RRC as additional classification dimension
+```
+
+## Integration
+
+The `polySignature` function produces a `PolySignature` that RRC can use
+alongside existing features (shape, alignment, receipt density) to classify
+mathematical objects by their algebraic decomposability.
+
+- High sparsity + low degree → likely factorizable (structured, "simple")
+- Low sparsity + high degree → likely irreducible (complex, dense)
+- High GCD of coefficients → common factor extractable (reducible)
+
+## References
+
+- Ryan, "Factoring short-sleeve RSA keys with polynomials", Trail of Bits, 2026
+- Conway–Sloane, *Sphere Packings*, Ch. 4 §6 (E₈ coefficient structure)
+-/
+
+namespace Semantics.RRC.PolyFactorIdentity
+
+open Semantics.FixedPoint
+open Semantics.E8Sidon
+
+-- ═══════════════════════════════════════════════════════════════════════════════
+-- §1. Limb Decomposition (the zerocopy view)
+-- ═══════════════════════════════════════════════════════════════════════════════
+
+/-- Decompose a natural number into base-B limbs (least-significant first).
+    This is the polynomial coefficient array: n = Σᵢ limbs[i] · Bⁱ.
+    At a zerocopy boundary, this decomposition is already present in memory
+    as the raw byte/word layout of the integer. -/
+def limbDecompose (n : Nat) (base : Nat) (fuel : Nat := 64) : List Nat :=
+  if base ≤ 1 then [n]
+  else
+    let rec go (x : Nat) (acc : List Nat) (f : Nat) : List Nat :=
+      match f with
+      | 0 => acc.reverse
+      | f' + 1 =>
+        if x = 0 then acc.reverse
+        else go (x / base) (acc.cons (x % base)) f'
+    if n = 0 then [0]
+    else go n [] fuel
+
+-- Witnesses: limbDecompose gives expected base-B digits
+#eval limbDecompose 2044 16     -- expect: [12, 252] since 2044 = 12*16 + 252... wait
+-- Actually: 2044 in base 16: 2044 / 16 = 127 rem 12, 127 / 16 = 7 rem 15
+-- So 2044 = 7*256 + 15*16 + 12 = [12, 15, 7] (LSB first)
+#eval limbDecompose 2044 256    -- expect: [252, 7] since 2044 = 7*256 + 252
+#eval limbDecompose 65536 256   -- expect: [0, 0, 1] since 65536 = 1*256² + 0*256 + 0
+#eval limbDecompose 9 4         -- expect: [1, 2] since 9 = 2*4 + 1
+
+-- ═══════════════════════════════════════════════════════════════════════════════
+-- §2. Coefficient Sparsity (the "short-sleeve" detector)
+-- ═══════════════════════════════════════════════════════════════════════════════
+
+/-- Count zero coefficients in a limb decomposition.
+    High zero count relative to total limbs indicates a "short-sleeve" pattern. -/
+def zeroLimbCount (limbs : List Nat) : Nat :=
+  limbs.filter (· == 0) |>.length
+
+/-- Coefficient sparsity as Q16_16: (zeroCount / totalLimbs).
+    Returns 0 if limbs is empty. -/
+def coeffSparsity (limbs : List Nat) : Q16_16 :=
+  if limbs.length == 0 then Q16_16.zero
+  else Q16_16.ofRatio (zeroLimbCount limbs) limbs.length
+
+/-- Short-sleeve detection threshold: 30% zero limbs triggers the flag.
+    This means at least 30% of the base-B limbs are zero — indicating
+    structured gaps that make polynomial factorization likely to succeed.
+    In Q16_16: 0.30 * 65536 ≈ 19661. -/
+def shortSleeveThreshold : Q16_16 := Q16_16.ofRawInt 19661
+
+/-- The "flag to look closer": does this integer exhibit short-sleeve structure
+    when viewed in base-B? At a zerocopy boundary, this check is essentially free
+    since the limbs are already laid out in memory. -/
+def shortSleeveDetected (n : Nat) (base : Nat) : Bool :=
+  let limbs := limbDecompose n base
+  -- Need at least 3 limbs to have a meaningful sparsity signal
+  if limbs.length < 3 then false
+  else (coeffSparsity limbs).toInt ≥ shortSleeveThreshold.toInt
+
+-- Witnesses: short-sleeve detection on known values
+#eval shortSleeveDetected 65536 256     -- expect: true (limbs [0,0,1] → 2/3 sparsity)
+#eval shortSleeveDetected 2044 256      -- expect: false (limbs [252,7] → only 2 limbs)
+#eval shortSleeveDetected 16777216 256  -- expect: true (limbs [0,0,0,1] → 3/4 sparsity)
+
+-- ═══════════════════════════════════════════════════════════════════════════════
+-- §3. Polynomial Signature (full structural features when flagged)
+-- ═══════════════════════════════════════════════════════════════════════════════
+
+/-- GCD of a list of natural numbers. Used to detect common polynomial factors. -/
+def listGcd : List Nat → Nat
+  | [] => 0
+  | [x] => x
+  | x :: xs => Nat.gcd x (listGcd xs)
+
+/-- Maximum coefficient in a limb decomposition.
+    Small max coefficient (relative to base) indicates the polynomial has
+    "small" coefficients — the key property exploited in the Trail of Bits attack. -/
+def maxCoeff (limbs : List Nat) : Nat :=
+  limbs.foldl Nat.max 0
+
+/-- Sum of squares of coefficients — a proxy for "energy" of the polynomial.
+    Low energy relative to degree indicates a sparse, structured polynomial. -/
+def coeffEnergy (limbs : List Nat) : Nat :=
+  limbs.foldl (fun acc c => acc + c * c) 0
+
+/-- The polynomial degree: index of highest non-zero coefficient.
+    Equals (number of limbs - 1) for non-zero inputs. -/
+def polyDegree (limbs : List Nat) : Nat :=
+  match limbs.reverse.dropWhile (· == 0) with
+  | [] => 0
+  | xs => xs.length - 1
+
+/-- Full polynomial signature — the structural fingerprint extracted when
+    short-sleeve detection flags an integer for closer inspection.
+
+    Fields:
+    - `base`:          the limb size (base-B representation)
+    - `degree`:        polynomial degree (highest non-zero coefficient index)
+    - `numTerms`:      count of non-zero coefficients
+    - `sparsity`:      fraction of zero coefficients (Q16_16)
+    - `maxCoeffVal`:   largest coefficient value
+    - `gcdCoeffs`:     GCD of all coefficients (> 1 means common factor exists)
+    - `energy`:        sum of squares of coefficients (structural complexity proxy)
+    - `isShortSleeve`: whether the short-sleeve threshold was exceeded -/
+structure PolySignature where
+  base          : Nat
+  degree        : Nat
+  numTerms      : Nat
+  sparsity      : Q16_16
+  maxCoeffVal   : Nat
+  gcdCoeffs     : Nat
+  energy        : Nat
+  isShortSleeve : Bool
+  deriving Repr
+
+/-- Compute the full polynomial signature for a natural number in base B.
+    This is the "look closer" step — called only when shortSleeveDetected
+    returns true at the zerocopy boundary. -/
+def polySignature (n : Nat) (base : Nat) : PolySignature :=
+  let limbs := limbDecompose n base
+  let nonZero := limbs.filter (· != 0)
+  { base          := base
+    degree        := polyDegree limbs
+    numTerms      := nonZero.length
+    sparsity      := coeffSparsity limbs
+    maxCoeffVal   := maxCoeff limbs
+    gcdCoeffs     := listGcd nonZero
+    energy        := coeffEnergy limbs
+    isShortSleeve := shortSleeveDetected n base }
+
+-- Witnesses
+#eval polySignature 65536 256
+-- expect: { base=256, degree=2, numTerms=1, sparsity≈43690 (2/3),
+--           maxCoeffVal=1, gcdCoeffs=1, energy=1, isShortSleeve=true }
+
+#eval polySignature 16777216 256
+-- expect: { base=256, degree=3, numTerms=1, sparsity≈49152 (3/4),
+--           maxCoeffVal=1, gcdCoeffs=1, energy=1, isShortSleeve=true }
+
+-- ═══════════════════════════════════════════════════════════════════════════════
+-- §4. E8Sidon Integration — Divisor Sum Polynomial Signatures
+-- ═══════════════════════════════════════════════════════════════════════════════
+
+/-- Compute polynomial signature of σ₃(n) in a given base.
+    Divisor sums have multiplicative structure that may produce
+    exploitable limb patterns in certain bases. -/
+def sigma3PolySig (n : Nat) (base : Nat) : PolySignature :=
+  polySignature (sigma3 n) base
+
+/-- Compute polynomial signature of σ₇(n) in a given base.
+    σ₇ values grow rapidly and often exhibit short-sleeve patterns
+    in smaller bases due to the power-7 amplification of prime factors. -/
+def sigma7PolySig (n : Nat) (base : Nat) : PolySignature :=
+  polySignature (sigma7 n) base
+
+/-- Compute polynomial signature of convolutionLHS(n) in a given base.
+    The Cauchy product Σ σ₃(m)·σ₃(n-m) produces large integers whose
+    limb structure reflects the multiplicative nature of divisor sums. -/
+def convPolySig (n : Nat) (base : Nat) : PolySignature :=
+  polySignature (convolutionLHS n) base
+
+-- Witnesses: σ₇ values in base 256 — do they exhibit short-sleeve patterns?
+#eval sigma7 4      -- expect: 2188 + 4^7 = 2188 + 16384 ... actually σ₇(4) = 1 + 2^7 + 4^7 = 1+128+16384 = 16513
+#eval sigma7PolySig 4 256
+-- σ₇(4) = 16513 → base-256 limbs: [97, 64] → 2 limbs, no short-sleeve (too few)
+
+#eval sigma7 6      -- σ₇(6) = 1 + 2^7 + 3^7 + 6^7 = 1+128+2187+279936 = 282252
+#eval sigma7PolySig 6 256
+-- σ₇(6) = 282252 → base-256 limbs: [140, 77, 4, 0] wait let me not predict...
+
+#eval sigma7 12     -- large value, likely has limb structure
+#eval sigma7PolySig 12 256
+
+-- Convolution products (large, likely structured)
+#eval convolutionLHS 6  -- Σ σ₃(m)·σ₃(6-m) for m=1..5
+#eval convPolySig 6 256
+
+-- ═══════════════════════════════════════════════════════════════════════════════
+-- §5. RRC Feature Integration
+-- ═══════════════════════════════════════════════════════════════════════════════
+
+/-- Classification feature: polynomial decomposability score.
+    Maps a PolySignature to a Q16_16 score in [0, 1] that indicates
+    how amenable the integer is to polynomial-based factorization.
+
+    High score (→ 1.0) means:
+    - High sparsity (many zero limbs)
+    - Low numTerms relative to degree
+    - GCD > 1 (common factor extractable)
+    - Low energy (sparse polynomial)
+
+    Low score (→ 0.0) means:
+    - Dense polynomial (no exploitable structure)
+    - All coefficients non-zero
+    - No common factor
+
+    This score feeds into the RRC identity step as the `polyDecomposability`
+    feature dimension. When high, it signals that the mathematical object
+    has algebraic structure that the classifier can exploit. -/
+def polyDecomposabilityScore (sig : PolySignature) : Q16_16 :=
+  -- Component 1: sparsity (weight 40%)
+  let sparsityComponent := (sig.sparsity.toInt * 26214) / q16Scale  -- * 0.4
+  -- Component 2: GCD bonus (weight 30%) — 1.0 if gcd > 1, else 0.0
+  let gcdComponent : Int := if sig.gcdCoeffs > 1 then 19661 else 0  -- 0.3
+  -- Component 3: term efficiency (weight 30%) — (1 - numTerms/degree) when degree > 0
+  let termEfficiency : Int :=
+    if sig.degree == 0 then 0
+    else
+      let ratio := (sig.numTerms * q16Scale) / (sig.degree + 1)
+      let complement := q16Scale - ratio  -- (1 - numTerms/(degree+1))
+      (complement * 19661) / q16Scale     -- * 0.3
+  Q16_16.ofRawInt (sparsityComponent + gcdComponent + termEfficiency)
+
+-- Witnesses
+#eval polyDecomposabilityScore (polySignature 65536 256)
+-- High: sparsity 2/3, gcd=1, 1 term / degree 2 → should be > 0.5
+
+#eval polyDecomposabilityScore (polySignature 2044 256)
+-- Low: only 2 limbs, no sparsity → should be near 0
+
+#eval polyDecomposabilityScore (polySignature 16777216 256)
+-- High: sparsity 3/4, gcd=1, 1 term / degree 3 → should be > 0.5
+
+-- ═══════════════════════════════════════════════════════════════════════════════
+-- §6. Batch Scanner (zerocopy boundary integration)
+-- ═══════════════════════════════════════════════════════════════════════════════
+
+/-- Result of scanning a batch of integers at a zerocopy boundary.
+    Records which values were flagged for closer inspection. -/
+structure ZeroCopyScanResult where
+  totalScanned    : Nat
+  flaggedCount    : Nat
+  flaggedIndices  : List Nat
+  signatures      : List PolySignature
+  deriving Repr
+
+/-- Scan a list of integers at the zerocopy boundary.
+    For each value, check short-sleeve detection. If flagged, compute
+    the full polynomial signature. This models what happens at mmap/DMA
+    boundaries where raw limbs are already visible.
+
+    The `base` parameter matches the hardware word size at the boundary:
+    - 256 for byte-level DMA (framebuffer, VCN payload)
+    - 65536 for Q16_16 values (two Q16_16 scalars per 32-bit word)
+    - 4294967296 for 32-bit limbs (ivshmem, PCIe DMA) -/
+def zeroCopyScan (values : List Nat) (base : Nat) : ZeroCopyScanResult :=
+  let indexed := values.zipIdx  -- List (Nat × Nat), (value, index)
+  let flagged := indexed.filter (fun (v, _) => shortSleeveDetected v base)
+  { totalScanned   := values.length
+    flaggedCount   := flagged.length
+    flaggedIndices := flagged.map Prod.snd
+    signatures     := flagged.map (fun (v, _) => polySignature v base) }
+
+-- Witness: scan a batch with mixed structure
+#eval zeroCopyScan [2044, 65536, 255, 16777216, 42, 256] 256
+-- expect: flagged = indices of 65536 and 16777216 (the ones with zero-limb patterns)
+
+-- ═══════════════════════════════════════════════════════════════════════════════
+-- §7. Theorems — Polynomial Evaluation Correctness
+-- ═══════════════════════════════════════════════════════════════════════════════
+
+/-- Evaluate a polynomial (coefficient list, LSB first) at a given base.
+    This is the inverse of limbDecompose: polyEval(limbDecompose(n, B), B) = n. -/
+def polyEval (coeffs : List Nat) (base : Nat) : Nat :=
+  let rec go (cs : List Nat) (pow : Nat) (acc : Nat) : Nat :=
+    match cs with
+    | [] => acc
+    | c :: rest => go rest (pow * base) (acc + c * pow)
+  go coeffs 1 0
+
+/-- limbDecompose followed by polyEval recovers the original value.
+    This is the fundamental correctness property: the polynomial
+    representation is faithful (no information lost). -/
+theorem limbDecompose_polyEval_roundtrip (n : Nat) (base : Nat) (hb : base ≥ 2) :
+    polyEval (limbDecompose n base) base = n := by
+  -- TODO(lean-port): Prove by induction on fuel steps of limbDecompose.
+  -- Sketch: each step extracts (n % base) as coefficient i, then recurses on
+  -- (n / base). The polyEval sum reconstructs via Σᵢ (n/base^i % base) · base^i = n.
+  -- This is the standard base-B representation theorem.
+  -- Blocked on: need List.enum induction lemma + Nat.div_add_mod identity.
+  sorry
+
+/-- Zero limbs in a decomposition correspond to "gaps" in the polynomial.
+    An integer with k zero limbs out of d total has at most (d - k) non-zero terms,
+    making polynomial factorization faster (fewer terms to consider). -/
+theorem zeroLimbs_bound_terms (limbs : List Nat) :
+    (limbs.filter (· != 0)).length + zeroLimbCount limbs = limbs.length := by
+  unfold zeroLimbCount
+  -- TODO(lean-port): Prove by List.filter complement partition.
+  -- Sketch: (filter p).length + (filter ¬p).length = length for any decidable p.
+  -- The two filters (· == 0) and (· != 0) are complements.
+  -- Blocked on: need List.filter_length_add_filter_length_eq (or equivalent).
+  sorry
+
+/-- Short-sleeve detection is monotone in sparsity: adding a zero limb
+    can only increase the likelihood of being flagged. -/
+theorem shortSleeve_mono_zero_prepend (n : Nat) (base : Nat) (hb : base ≥ 2)
+    (h : shortSleeveDetected n base = true) :
+    shortSleeveDetected (n * base) base = true := by
+  -- TODO(lean-port): Prove that limbDecompose(n * base, base) = 0 :: limbDecompose(n, base).
+  -- Multiplying by base left-shifts the polynomial, prepending a zero coefficient.
+  -- This increases zeroLimbCount by 1 and length by 1, so sparsity increases
+  -- (or stays the same if it was already maximal).
+  -- Sketch: unfold shortSleeveDetected, show sparsity(0::limbs) ≥ sparsity(limbs).
+  sorry
+
+-- ═══════════════════════════════════════════════════════════════════════════════
+-- §8. Module Summary
+-- ═══════════════════════════════════════════════════════════════════════════════
+
+/-!
+## Sorry Inventory
+
+| # | Name | Reason | Proof Sketch |
+|---|------|--------|--------------|
+| 1 | `limbDecompose_polyEval_roundtrip` | Needs go-induction + Nat.div_add_mod | Induction on fuel, standard base-B theorem |
+| 2 | `zeroLimbs_bound_terms` | Needs List.filter complement partition | filter_p.length + filter_not_p.length = length |
+| 3 | `shortSleeve_mono_zero_prepend` | Needs limbDecompose multiplication lemma | Prepend-zero increases sparsity |
+
+## Integration Notes
+
+- `polyDecomposabilityScore` is the primary RRC feature export.
+- `zeroCopyScan` models the hardware boundary where detection is free.
+- `sigma3PolySig` / `sigma7PolySig` / `convPolySig` connect to E8Sidon.
+- Base selection: 256 for byte-level (framebuffer/DMA), 65536 for Q16_16.
+-/
+
+end Semantics.RRC.PolyFactorIdentity