face_monochromatic_pairs: lessons from structural-proof attempts

Updated COMMENTARY.md with a "Lessons from the structural-proof
attempts" section summarizing:

- What worked: the Heawood-face-sum reduction (Theorem
  deciding-face-implies-conj-5-1) and tight covering for n_k = 5
  configurations.
- What didn't: n_i = 6 lemma (retracted as empirically false),
  winding-number invariant (Σ = 0 under alternation, not
  contradictory), case-analysis past |S| ≤ 1 (becomes discharging).
- Diagnostic: every global aggregation we've tried gives a quantity
  consistent with constancy, not contradicting it. Lemma 5.2's
  alternation is the right local consequence but doesn't aggregate
  to a contradiction by itself.
- Open: G'-pentagon fallback structural proof; possible stronger
  consequences of minimality of G beyond chord-apex.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

papers/face_monochromatic_pairs/COMMENTARY.md

@@ -137,6 +137,74 @@ The counterexample shows the general case of the conjecture is
 unsalvageable; the search for a structural proof of Conjecture 5.1
 will need a different angle.
 
+## Lessons from the structural-proof attempts (commit `fd4b89a` onward)
+
+After working through three structural-proof routes to the deciding-face
+conjecture and beyond, here's what's known and what's still open:
+
+### What worked
+- **Reduction** (Theorem `thm:deciding-face-implies-conj-5-1`): Conjecture 5.1
+  follows from the existence of a deciding face — a face of the reduced
+  dual with boundary ⊆ V(K_b) ∪ V(K_c) and length not divisible by 3 —
+  via Heawood's classical face-sum identity. This is clean and tight.
+- **Tight covering for $n_k = 5$** (Lemmas `lem:flank-covering-base` and
+  `lem:outer-face-covering-base`): if any of (i) $n_i = 5$, (ii) $n_{i+1} = 5$,
+  or (iii) $n_{i+2} = n_{i+4} = 5$ holds, the flank or outer face is a
+  tight structural deciding face. Covers 94.97% of the 7,930 empirical
+  (G, v, i) configurations up to $|V(G)| \le 20$.
+- **Partial pigeonhole for the G'-pentagon fallback** (Lemma
+  `lem:gprime-pigeonhole`): if at most one vertex is uncovered by
+  V(K_b) ∪ V(K_c), at least one G'-pentagon is a deciding face. Combined
+  with the tight cases, covers ~91% structurally.
+
+### What didn't work
+- **n_i = 6 flank-covering lemma** — *the lemma is empirically false*.
+  9,228 / 142,812 chord-apex+Kempe colourings hit sub-case (ii.B) of
+  Case (b), and 1,314 of those have P_1 ∉ V(K_b) ∪ V(K_c), falsifying
+  the lemma. Retracted in commit `873c2cc`.
+- **Winding-number / topological invariant** (commit `fd4b89a`).
+  Σ-of-turn-signs around K_b under Lemma 5.2 alternation = 0. This is
+  *consistent* with K_b being a simple closed planar curve bounding a
+  non-empty region — not a contradiction. The natural topological
+  invariant doesn't distinguish chord-apex+Kempe colourings under
+  constancy from generic K_b's.
+- **Closing the case analysis past |S| ≤ 1** — would require finer
+  graph-structural input, fragmenting the case count. This is exactly
+  the discharging flavour of the traditional reducible-configurations
+  approach (Appel-Haken / RSST / Gonthier) to the Four Colour Theorem
+  itself; we stopped to avoid replaying that route in a different
+  vocabulary.
+
+### Diagnostic observation
+Across all attempts, Lemma 5.2's alternation (= constancy on V(K_b)
+implies c_1-edges alternate sides along K_b) is the natural local
+consequence of constancy, but each global aggregation we've tried
+produces a quantity that's *consistent* with constancy rather than
+contradicting it:
+
+- Heawood face-sum mod 3 on a specific face: requires identifying *which*
+  face — that's case analysis.
+- Winding number of K_b: zero under alternation, which only says K_b
+  isn't a face boundary (true, not contradictory).
+- Identity s_b ⊕ s_c = i_b ⊕ i_c ⊕ 1: reduces under constancy to
+  c_b ⊕ c_c = 1, true but not contradictory.
+
+This suggests the contradiction in the chord-apex+Kempe setting is
+*not* captured by local-or-aggregable invariants of K_b alone.
+
+### What's left open
+
+- **Conjecture (Deciding face)**: 100% empirically verified
+  (142,812 / 142,812), 94.97% structurally proven, ~5% reducible to
+  Conjecture (G'-pentagon fallback), itself 100% empirical but
+  structurally open.
+- **G'-pentagon fallback structural proof beyond |S| ≤ 1**: needs a
+  Kempe-cycle structural result describing *which* G'-pentagons the
+  uncovered vertices of chord-apex+Kempe colourings can hit.
+- **Minimality of G**: invoked to derive chord-apex (= colour equality
+  spike = merged) then forgotten. Possibly minimality has a stronger
+  consequence we haven't extracted.
+
 ## Snapshot date
 
 This commentary is current as of commit `e688037`.