e8b2e47e44
Section 5.6 sketches an inductive route to the simple-resolution md4 surjectivity conjecture: - Lemma 5.8 (good contraction): every md4 triangulation on n >= 7 vertices has a degree-4 vertex with an md4-preserving diagonal contraction. Empirically true at n=7..11; proof obligation called out. - Lemma 5.9 (lift): given a labelled preimage of the contracted triangulation, reinserting the contracted vertex at the diagonal-bounded quadrilateral yields a preimage of the original triangulation. Proof obligation called out. - Inductive scheme paragraph chains the two lemmas with the octahedron at n=6 as the base case, citing the n=7 hand-verification (already scripted in experiments/inductive_lift_check.py). Lemmas are stated without proof; the three remaining proof obligations are explicit. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>