Prove the c4 h7 Tq sibling-entry lemma

[lieoric]

What this adds

• a pure proof eliminating the same-z Tq sibling-entry family at c=4, k=2, h=7
• an exact fixed-future checker for every labeled residual word in that family
• an independent census/report checker and a scoped GitHub Actions proof run

Verified result

GitHub Actions run 31422112992 completed successfully:

• 23 canonical sibling parents / 32 bad Tq entrance edges
• 2,958 feasible fixed-next decorations
• 10,073,448 / 10,073,448 complete residual words are checkpoint-YES
• 0 local-NO residuals
• both q-siblings are safe first moves in 10,073,448 / 10,073,448 cases

Run: https://github.com/lieoric/water-sort-counterexample/actions/runs/31422112992

Claim boundary

This eliminates the same-z Tq sibling-entry family. It does not claim that every c4/k2/h7 layout is solvable. The machine run corroborates a general proof in docs/c4-h7-tq-sibling-lemma.md.

Local and independent validation

• MSVC Release /W4 /WX
• focused CTest and bounded production/independent differential checks
• independent reconstruction and witness replay
• strict report-schema and SHA-256 artifact validation