face_monochromatic_pairs: write final status summary in COMMENTARY.md

After several rounds of structural attempts and audits, the picture
has stabilized. Updated COMMENTARY.md with a "Final status" section:

- What we have proved: the Heawood-face-sum reduction (tight), the
  tight structural cases (a', b', c) covering 94.97% of (G, v, i)
  configurations, and the refined pigeonhole + S-cycle arguments
  closing most of the residual ~5%.
- What's open structurally: full G'-pentagon fallback, and the
  Kempe-cycle structural regularity "|S|=8 + hit=8 ⇒ p_G=11"
  (30/30 empirical).
- Empirical closure: 100% across 142,812 chord-apex+Kempe colourings
  up to |V(G)| ≤ 20.
- Why this isn't Appel-Haken in disguise: ~4 main steps + ~8
  case-style sub-lemmas, vs RSST's 633. The chord-apex+Kempe
  restriction does most of the work upfront.

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

papers/face_monochromatic_pairs/COMMENTARY.md

@@ -205,6 +205,80 @@ This suggests the contradiction in the chord-apex+Kempe setting is
   spike = merged) then forgotten. Possibly minimality has a stronger
   consequence we haven't extracted.
 
-## Snapshot date
+## Final status (commit `2d8c679`)
 
-This commentary is current as of commit `e688037`.
+### What we have proved
+
+1. **Theorem (Conjecture 5.1 ⇐ Deciding face)**: clean reduction via Heawood's
+   classical face-sum identity. Tight.
+
+2. **Tight structural cases for the Deciding face conjecture**:
+   - (a') $n_i = 5$ → flank face $F^\flat_{i, i+1}$ of length 4.
+   - (b') $n_{i+1} = 5$ → flank face $F^\flat_{i+1, i+2}$.
+   - (c)  $n_{i+2} = n_{i+4} = 5$ → outer face $F^\flat_{\text{outer}}$ of length 7.
+
+   Empirical coverage: 7,531 / 7,930 (G, v, i) configurations = **94.97%**.
+
+3. **Refined pigeonhole + S-cycle structure**: for bad colourings
+   (= where Lemma flank-covering-hex fails), the uncovered vertex set
+   $S$ is even, forms a 2-regular subgraph (= a single cycle), and is
+   bounded so that # G'-pentagons hit by S < $p_G$. This closes most
+   bad cases structurally.
+
+4. **Empirical closure**: the G'-pentagon fallback conjecture is true on
+   1,314 / 1,314 bad colourings, hence on all **142,812 / 142,812**
+   chord-apex+Kempe colourings up to $|V(G)| \leq 20$.
+
+### What's open structurally
+
+1. **G'-pentagon fallback in full generality** — proven via pigeonhole for
+   $|S| \leq 1$, sketched for higher $|S|$ via empirical bounds (max hit,
+   min $p_G$), but no fully structural proof of the empirical bounds.
+
+2. **The "|S| = 8 + hit = 8 ⇒ $p_G = 11$" regularity** — striking
+   empirical fact (30/30 cases) but no Kempe-cycle structural argument
+   for it. The marginal $|S|$ ↔ # pent $F_k$ coupling doesn't hold;
+   the regularity is a joint structural property of specific
+   $(|S|, \text{hit})$ pairs.
+
+### What the path is
+
+The structural proof has stabilized at the following form:
+
+```
+Conjecture 5.1 (face-monochromatic-pair)
+  ⇐ Theorem (Conj 5.1 ⇐ Deciding face)     [tight]
+Conjecture (Deciding face)
+  ⇐ Theorem (Extended partial proof)       [tight on 7,531/7,930]
+  ⇐ Conjecture (G'-pentagon fallback)       [empirical 1,314/1,314]
+  ⇐ Lemma (G'-pentagon pigeonhole, |S| ≤ 1) [tight on |S| ≤ 1 ≈ 91%]
+  + open: structural |S|-cycle arguments for |S| ≥ 2.
+```
+
+So Conjecture 5.1 is reduced to **two open structural conjectures**:
+
+  (i) The G'-pentagon fallback conjecture (empirically 100%).
+  (ii) Kempe-cycle-structural lemmas about chord-apex+Kempe colourings
+       sufficient to close the |S| ≥ 2 cases of the fallback.
+
+Closing (i) and (ii) structurally would give a full structural proof.
+The empirical 100% across 142,812 colourings is strong evidence both
+are true.
+
+### Why this isn't Appel-Haken in disguise
+
+The structural proof has 4 main steps + ~8 case-style sub-lemmas (vs
+RSST's 633 cases). The compression comes from the chord-apex+Kempe
+restriction doing most of the heavy lifting upfront — specifically,
+Lemma 5.3 (no-witness ⇒ constancy on V(K_b) ∪ V(K_c)) and Lemma 5.X
+(Kempe-spike, forced edge containments) pre-restrict the problem to
+a very constrained colour configuration. The Heawood face-sum
+identity then converts the local constancy into a mod-3 obstruction,
+and the case analysis closes specific structural sub-buckets.
+
+The remaining open conjectures are at the chord-apex+Kempe class
+level, not at the level of arbitrary minimal counterexamples to 4CT.
+
+### Snapshot date
+
+This commentary is current as of commit `2d8c679` (2026-05-25).