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: running21classification: pending22evidence: []23verdict: pending24---2526# 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 function2728The 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.29