Goal: solve Freek open lean target #50

[cgbarlow]

Plan and build the targets that allow us to achieve this goal as per Multi-agent review with Opus 1.8 in ultracode... it looks like our work so far with unsorry is a contribution to the Freek open Lean target #50

"Honest bottom line
I read the actual proof earlier, and the math checks out — the strict inequality correctly excludes the Euclidean boundary cases, and it is genuinely absent from Lean. But calibrate the excitement precisely: its value is as a verified, citable building block and a milestone toward a famous open Lean target — not as useful new mathematics, and not as anything the applied world (viruses, crystals, graphics, codes) actually needs. Its worth is real, narrow, and entirely about formalization: it's a clean, kernel-checked down-payment on Freek #50, most valuable once it's upstreamed and re-cast as the curvature trichotomy. The thing that's remarkable remains that an autonomous swarm reached and verified it at all, in days — the theorem is the trophy, not the tool."

[cgbarlow]

Plan: how we close (and honestly don't yet close) Freek #50

Where we landed after scoping

The bar. Freek's list accepts HOL Light's PLATONIC_SOLIDS — a biconditional stated in full ℝ³ convex geometry:

for a real 3-polytope p (polytope p, aff_dim p = 3) where every 2-face has m edges and every vertex meets n edges, such a p exists ⟺ (m,n) ∈ {(3,3),(4,3),(3,4),(5,3),(3,5)}.

Both directions: classification (any such solid forces one of 5 pairs) and existence (each of the 5 is realised). It lives over Harrison's real-geometry polytope library (face_of, aff_dim, Euler–Poincaré).

Where our proved work sits. platonic_schlafli_pairs (1/p+1/q > 1/2 ⟹ (p,q) ∈ 5 pairs) is exactly the final arithmetic step of the classification direction — and nothing more. It's the keystone, but ~5% of the faithful theorem. The backlog file already flags it: "proves the combinatorial classification ONLY, no geometry."

The gap (decisive). I mapped mathlib end-to-end (pinned c5ea0035). It has almost none of the substrate: no stated Euler polyhedron formula (V−E+F=2), no convex-polytope face lattice (face_of/aff_dim), no regularity/Schläfli notion, no angle-defect/Gauss–Bonnet, and none of the 5 solids as objects. A faithful port means building a polytope face-lattice + Euler–Poincaré theory — genuine mathlib-grade infrastructure, not swarm-sized leaf lemmas.

What we're going to do — staged, two tracks (decision: staged route)

Our arithmetic core is the same keystone lemma in both tracks, so value compounds.

• Track 1 — combinatorial milestone (swarm now, ~weeks). Define a self-contained abstract regular polyhedron (V E F p q : ℕ with handshakes p·F=2E, q·V=2E, Euler V+F=E+2) and prove the biconditional at that level: ⟹ feeds Euler+handshake into our proved core; ⟸ exhibits the 5 concrete (V,E,F) witnesses (tetra 4/6/4 … icos 12/30/20). Non-vacuous (concrete witnesses), decomposes into a small dependency tree that reuses the proved core (ADR-014), and finally lands the roadmap's open "drive a real result through a dependency tree at depth" gap. This is explicitly NOT Freek fix: paren-wrap false positives in fidelity gate (SPEC-003-C step 5) #50 — it will be labelled "combinatorial/Euler form."
• Track 2 — the faithful ℝ³ port (staged, gated on mathlib). Face lattice → Euler–Poincaré for 3-polytopes → geometric handshake → our core → construct the 5 solids → assemble the biconditional. Most of this is mathlib-grade infrastructure, best pursued human-sponsored / upstream (the existing roadmap's Track C) or held until mathlib grows a polytope face lattice. The already-packet-ready arithmetic core is the realistic near-term public good.

Honesty guardrail (non-negotiable)

Freek #50 cannot be marked closed by Track 1. The Lean column stays unclaimed until Track 2's faithful ℝ³ biconditional passes Gate A. Track 1 ships as a labelled milestone; the near-term commons contribution is the arithmetic core upstream. (This matches the multi-agent review quoted when this issue was opened — our piece is a verified down-payment, not the theorem.)

Next concrete steps

1. ADR-031 + SPEC-031-A — record this staged decision + Track-1 acceptance criteria + Track-2 milestone list (I1 face lattice, I2 Euler–Poincaré, I3 geometric handshake, I4 the 5 constructions, I5 assembly), with the honesty guardrail as an explicit clause. (docs PR, in flight)
2. Seed Track-1 target platonic-solids-combinatorial (abstract-polyhedron existence-biconditional) through the ADR-012 sourcing pipeline; let the swarm decompose + prove it, reusing platonic_schlafli_pairs.
3. Keep the upstream packet for the arithmetic core warm (human-sponsored, per mathlib AI policy).

ADR + spec PR linked here on open.

[cgbarlow]

📋 Plan recorded as ADR-031 + SPEC-031-A (Track-1 backlog target platonic-solids-combinatorial + CHANGELOG) → PR #372. Next: seed the Track-1 target through the ADR-012 sourcing pipeline once #372 lands.

[cgbarlow]

✅ PR #372 merged — ADR-031 + SPEC-031-A + the Track-1 target are now on main. Plan of record stands; next action is seeding platonic-solids-combinatorial into the swarm.