Sourcing the A1 twelve-port carrier from the binary icosahedral group

[dmobius3]

Hello, I am the author of Mode Identity Theory (MIT) and have an upstream candidate for row 4 of the selection ledger. It asks nothing of OPH beyond a bounded reconstruction check, and it carries no suggestion that either project adopt the other's physical interpretation.

What row 4 declares

Row 4 is an EXPOSED PREMISE. A1 declares that each finite local carrier has twelve primitive ports with the unlabeled 12-vertex, 30-edge, 20-face, degree-five, coherently oriented boundary complex of the icosahedron. The menu passed over is 3: tetrahedral, octahedral, icosahedral antipodal port families.

Rows 2, 3, and 11 are FORCED conditional on row 4, so a source for row 4 would sit under the antipodal pairing and six axes, the $A_5$ port frame, and the $\mathfrak{u}(1)\oplus\mathfrak{su}(2)\oplus\mathfrak{su}(3)$ port-current type.

The candidate source

MIT's observable domain is $S^3/2I$, with $2I \subset SU(2)$ the binary icosahedral group, $|2I| = 120$.

The finite subgroups of $SU(2)$ carry the ADE classification: two open families (cyclic $Z_n$, binary dihedral $2D_n$) and three exceptional groups. OPH's three-way row-4 menu is exactly the projective image of those three exceptional groups.

Exceptional subgroup of $SU(2)$	Order	Projective image	Row-4 family
$2T$	24	$A_4$	tetrahedral
$2O$	48	$S_4$	octahedral
$2I$	120	$A_5$	icosahedral

The routes to those structures are independent. OPH reaches the menu through the antipodal port requirement. MIT reaches the exceptional list from the spherical-quotient and flat-connection problem, scanning the full ADE classification including the open families.

Two discriminants inside that menu

MIT carries two results that separate $2I$ from the other two members of the same three.

Perfectness. $2I$ is the unique nontrivial perfect finite subgroup of $SU(2)$: it equals its own commutator subgroup, so its only one-dimensional character is the trivial one. $2T$ abelianizes to $Z_3$, and $2O$ to $Z_2$.

The coexact gap. For the adjoint of an irreducible flat $SU(2)$ connection on $S^3/\Gamma$, the coexact 1-form gap is $4/R^2$ across the whole ADE classification, with exactly one break: $36/R^2$ for the Galois connection $Q'$ on $S^3/2I$, whose adjoint sits at McKay distance six on affine $E_8$.

Neither result was built to produce twelve ports. Both came out of the flat-connection problem on spherical space forms.

What this does and does not do

MIT has not closed the framework-level implication "physical requirements $\Rightarrow 2I$." Perfectness and terminality converge on $2I$ from two directions, and the single theorem folding them into one forcing argument is open on MIT's side.

So the proposal moves OPH's declaration upstream. It leaves a source assumption in place. The mathematical classification theorem and the physical selection problem stay separate here, in the same way OPH separates a source theorem from a physical attachment.

The reconstruction receipt

Given $2I$, the carrier combinatorics follow from subgroup structure rather than from three declared numbers.

Write $G = 2I/Z(2I) \cong A_5$. The three cyclic stabilizers give

$$|A_5/C_5| = 12, \qquad |A_5/C_3| = 20, \qquad |A_5/C_2| = 30,$$

equivalently upstairs on the preimages $C_{10}$, $C_6$, $C_4$, each of which is cyclic because $2I$ has a unique involution:

$$120/10 = 12, \qquad 120/6 = 20, \qquad 120/4 = 30.$$

Cardinalities alone would be weak evidence. The content is the coset geometry with incidence

$$gH \sim kK \iff gH \cap kK \neq \varnothing,$$

which produces the vertex, face, and edge sets together with their incidences from one object, and returns the degrees as a consequence: $12 \times 5 = 30 \times 2 = 20 \times 3$.

The cosets are therefore the receipt that an independently selected group reconstructs the carrier, rather than the reason for selecting it.

Two residues, stated up front

The duality bit. The coset geometry leaves the icosahedron and the dodecahedron on equal footing. Naming the $C_5$-cosets as ports rather than the $C_3$-cosets is one declared bit. A1's own degree-five clause already pins it, so the residue is one bit rather than a combinatorial complex.

Orientation. $2I \subset SU(2)$ covers rotations only, so the projection $SU(2) \to SO(3)$ carries it to $2I/{\pm 1} \cong A_5$ rather than to the reflection-extended $A_5 \times C_2$. Row 3 currently beats a two-element menu between the oriented $A_5$ frame and the orientation-forgetting $A_5 \times C_2$ frame. Whether a $2I$ source makes that orientation receipt redundant or merely consistent with it is a question for OPH's machinery rather than a claim from here.

The proposed experiment

1. Take $2I$ as the declared source.
2. Derive $G = 2I/Z(2I) \cong A_5$.
3. Construct the transitive $G$-sets $G/C_5$, $G/C_3$, $G/C_2$ with the coset-intersection incidence above.
4. Determine whether the resulting oriented incidence complex is uniquely the A1 carrier, enumerating every choice consumed along the way.
5. Feed the generated object into the existing proofs unchanged.

A negative counts at the same bar. If the reconstruction is non-unique, or consumes choices beyond the duality bit, that is a sharper statement of what row 4 declares than the row currently carries.

Why the existing no-go leaves this route open

Row 4 cites Lean/Screen/PhysicalA5ForcingNoGo.lean (noSourceOnlyChargeReconstruction) for the result that the bare total-charge reduct fails to reconstruct even the boundary choice. A group source is a different and richer input, so this route sits outside that theorem's stated domain rather than trying to work around it.

Existing machinery

Lean/Screen/A5PortAction.lean and Lean/Screen/PortFrameGram.lean look like the components that would keep step 4 bounded. Whether the coset construction lands in the same representation those files use is something the maintainers would judge faster than I can.

One question back

Does OPH's exclusion of the cyclic and binary-dihedral families agree with MIT's? MIT drops the open families because each requires an external choice of $n$. If the antipodal port requirement drops them on different grounds, that is a second independent convergence and worth recording on its own.

References

MIT, mathematical side:

• Coexact gap (bedrock)
• Yang-Mills and the three flat vacua (I'm aware of the tongue-in-cheek 😅)

[muellerberndt]

Hey @dmobius3, thanks for the proposal! A bounded reconstruction check would be useful, and I’d welcome a pull request.
Please keep the initial contribution focused on an exact, reproducible construction from the declared (2I) source, with:

• An explicit (2I/Z(2I)\cong A_5) identification and compatible choices of the (C_5,C_3,C_2) subgroups. Their orders give the correct cardinalities, but arbitrary relative placements can fail to produce valid face boundaries.
• Verification of the full incidence complex, including triangular faces, coherent orientation, and antipodal pairing, together with an explicit relabelling into our existing PortFrameGram and A5PortAction fixtures. A Lean bridge would be particularly valuable.
• An accounting of subgroup placement, duality, and orientation choices: which disappear under isomorphism, and which remain additional assumptions? Please include negative controls for incompatible choices.
• A clear statement that the reconstruction is conditional on the supplied group and any remaining choices. Physical selection of (2I) remains a separate question.
  The executable construction and verification would fit under code/a5_closure/, with any Lean component under Lean/Screen/ and reproduction instructions alongside the code. A verified obstruction or nonuniqueness result would also be useful.
  On your final question: our selection ledger records a declared three-family comparison. It does not establish that antipodality excludes all cyclic and binary-dihedral alternatives, so we should leave the proposed independent convergence open pending a precise argument.

P.s.: Please join our R&D Telegram group, you can email me at bernhard [at] floatingpragma [dot] ai for the invite!

[dmobius3]

Thanks, @muellerberndt. The PR is up: #784

Your placement caveat ended up being the heart of it. Of the 900 ways to place the three subgroups, only 120 give back the carrier, exactly the ones where the generators satisfy xyz = 1. The surprise was the next 180: they look right at the vertex level and only fail on edge-face incidence. The certificate takes the group as given and doesn't touch the ledger. Everything else is in the PR.

Happy to leave the convergence question where you put it. The Lean bridge will follow as its own PR, and I've emailed you about the Telegram group. 🍻