id: H22 title: σ0 and σ1 are not injective on 32-bit words (kernel of positive dimension), unlike Σ0 and Σ1 axis: D kind: formal statement: The logical shift in σ0, σ1 makes the GF(2)-linear maps non-bijective; bv_decide or a rank computation exhibits the kernel; Σ0, Σ1 (rotations only) are bijective. motivation: A small, decidable algebraic question whose answer matters for message-schedule analyses. assumptions: None. expected_contribution: Exact kernel dimensions and counterexamples. related_work:

• nist2015fips180 possible_counterexamples: σ0 injective (would contradict the rank computation). verification_strategy: formal/ + GF(2) rank script computational_budget: minutes status: evaluated classification: rejected evidence:
• formal/README.md
• formal/build.log
• tests/test_formal_lean.py
• formal/scripts/gf2_rank.py verdict: 'Conjecture refuted: σ0 and σ1 are bijective (bv_decide UNSAT certificates for injectivity; GF(2) rank 32 by two independent eliminations; explicit 32×32 inverse matrices verified in Lean). The shift makes each summand singular (x≫3 has rank 29; rotr7⊕rotr18 kills 0xFFFFFFFF) but the sum is a unit. A wrong belief caught by the formal layer.'

# H22 — σ0 and σ1 are not injective on 32-bit words (kernel of positive dimension), unlike Σ0 and Σ1

The logical shift in σ0, σ1 makes the GF(2)-linear maps non-bijective; bv_decide or a rank computation exhibits the kernel; Σ0, Σ1 (rotations only) are bijective.