id: H19 title: The 9-step local collision holds with probability 1 in the XOR-linearised model and with low, position-dependent probability in the real step function axis: C kind: sha256 statement: The 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. motivation: C3/C4. assumptions: Linearisation of Ch and Maj as in Gilbert–Handschuh 2003. expected_contribution: Reproduction of a classical result with a formal proof of the linear part. related_work:

• chabaud1998differential
• gilbert2003security
• nikolic2008collisions possible_counterexamples: Linearised cancellation failing for some δ (ruled out by bv_decide). verification_strategy: experiments/reduced_round_sha256/local_collision.py + formal/ Lean theorem. computational_budget: minutes status: running classification: pending evidence: [] verdict: pending

# 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 function

The 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.