1---2id: H193title: The 9-step local collision holds with probability 1 in the XOR-linearised model and with low, position-dependent probability4 in the real step function5axis: C6kind: sha2567statement: The Chabaud–Joux/Gilbert–Handschuh correction pattern cancels any single-bit difference after 9 linearised steps8 (machine-checked); with modular additions the same pattern succeeds with probability ≈ 2^-c (c measured per bit position,9 highest at the MSB), and SAT finds conforming message words in seconds.10motivation: C3/C4.11assumptions: Linearisation of Ch and Maj as in Gilbert–Handschuh 2003.12expected_contribution: Reproduction of a classical result with a formal proof of the linear part.13related_work:14- chabaud1998differential15- gilbert2003security16- nikolic2008collisions17possible_counterexamples: Linearised cancellation failing for some δ (ruled out by bv_decide).18verification_strategy: experiments/reduced_round_sha256/local_collision.py + formal/ Lean theorem.19computational_budget: minutes20status: evaluated21classification: known_reproduced22evidence:23- results/reduced_round_sha256/summary.json24- results/reduced_round_sha256/local_collision.json25- formal/README.md26verdict: 'Pattern (δ, Σ0δ⊕Σ1δ, Σ1(Σ0δ), 0, δ, Σ0δ⊕Σ1δ, 0, 0, δ) cancels in the linearised model for all δ (GF(2) check + Lean27 theorem localCollision_absorb). Real step: 0 collisions in 32 × 100 000 samples (bound 3·10⁻⁵); survival after step i 0.2528 (bits 0–30) / 1.0 (bit 31), after i+1 ≈ 10⁻⁴, after i+2 zero. SAT finds conforming pairs for all 32 positions in 4.4–11829 s, all verified.'30---3132# H19 — The 9-step local collision holds with probability 1 in the XOR-linearised model and with low, position-dependent probability in the real step function3334The Chabaud–Joux/Gilbert–Handschuh correction pattern cancels any single-bit difference after 9 linearised steps (machine-checked); with modular additions the same pattern succeeds with probability ≈ 2^-c (c measured per bit position, highest at the MSB), and SAT finds conforming message words in seconds.35