1---2id: H223title: σ0 and σ1 are not injective on 32-bit words (kernel of positive dimension), unlike Σ0 and Σ14axis: D5kind: formal6statement: The logical shift in σ0, σ1 makes the GF(2)-linear maps non-bijective; bv_decide or a rank computation exhibits7 the kernel; Σ0, Σ1 (rotations only) are bijective.8motivation: A small, decidable algebraic question whose answer matters for message-schedule analyses.9assumptions: None.10expected_contribution: Exact kernel dimensions and counterexamples.11related_work:12- nist2015fips18013possible_counterexamples: σ0 injective (would contradict the rank computation).14verification_strategy: formal/ + GF(2) rank script15computational_budget: minutes16status: evaluated17classification: rejected18evidence:19- formal/README.md20- formal/build.log21- tests/test_formal_lean.py22- formal/scripts/gf2_rank.py23verdict: 'Conjecture refuted: σ0 and σ1 are bijective (bv_decide UNSAT certificates for injectivity; GF(2) rank 32 by two24 independent eliminations; explicit 32×32 inverse matrices verified in Lean). The shift makes each summand singular (x≫325 has rank 29; rotr7⊕rotr18 kills 0xFFFFFFFF) but the sum is a unit. A wrong belief caught by the formal layer.'26---2728# H22 — σ0 and σ1 are not injective on 32-bit words (kernel of positive dimension), unlike Σ0 and Σ12930The 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.31