Add exact coset-carrier reconstruction certificate for a supplied SL(2,5) source (#769)

[dmobius3]

This PR adds the bounded reconstruction check proposed in discussion #769, taking SL(2, F_5) as the supplied binary icosahedral source. All 900 placements of the three cyclic stabilizers reproduce the local incidence counts of the A1 carrier. Exactly 120 close into the committed oriented carrier under an explicit relabelling: precisely the placements whose generators can be chosen with xyz = 1. A further 180 reproduce the committed edge graph and face vertex sets and fail the coset edge-face incidence, which is the failure mode the placement caveat in #769 anticipated, in its subtlest form.

The construction forms the central quotient G and builds the coset geometry with vertices G/C5, faces G/C3, edges G/C2, and incidence by nonempty coset intersection, for all 900 placements of the three cyclic subgroups. The companion note states the result as Theorem 769.1. Its central lemma, 769.3, is proved by hand: the base edge C2 lies on the base face C3 exactly when the generators can be chosen with xyz = 1, and every incident edge-face pair is a translate of that base pair. The note pairs such proofs with exhaustive finite verification; the sizes of the four placement classes come from the verifier.

Acceptance

Request in #769	Discharge
Explicit 2I/Z(2I) ≅ A5 identification and compatible choices of C5, C3, C2	SL(2, F_5) is checked for order 120, centre {+I, -I}, a unique involution, perfectness, and the binary icosahedral order profile. The quotient identification G ≅ A5 is computed from the faithful action of G on its five Klein four-subgroups; the step SL(2, 5) ≅ 2I is cited, as the conditionality row states. All 900 placements are classified, and compatibility is exactly xyz = 1.
Full incidence complex (triangular faces, coherent orientation, antipodal pairing) with an explicit relabelling into PortFrameGram and A5PortAction, and a Lean bridge	Every compatible placement is checked on all three incidences and relabelled onto PortFrameGram.neighbors, CoreAxioms.orientedFaces, PortFrameGram.antipode, and the sixty A5PortAction.perms rows. Of its 120 graph relabellings, 60 carry the coset orientation onto orientedFaces and the other 60 are exactly their compositions with the antipode. The Lean bridge is scoped below as a follow-up under Lean/Screen/.
Accounting of placement, duality, and orientation choices, with negative controls for incompatible choices	The placement is unique up to Aut(G): the certificate enumerates Aut(G) exhaustively (120 automorphisms, all induced by conjugation in GL(2, F_5), with Aut(G) ≅ S5), and the 120 compatible placements form one orbit under Aut(G) and two orbits under inner automorphisms. Twelve ports select C5, which removes the duality choice. The construction outputs the orientation and the relabelling matches it. No placement, duality, or orientation choice survives as an assumption; the supplied group is the only residual premise. Fifteen typed controls are recorded, and the 780 incompatible placements are classified by their first failing check.
Conditionality on the supplied group	Stated in the receipt and in the note's claim boundary. The identification SL(2, 5) ≅ 2I rests on one cited fact, that the Schur multiplier of A5 is Z/2 (Schur 1911; the full reference is in the note).
A verified obstruction or nonuniqueness result	The 180-placement family below, which agrees with the committed packet on all vertex-level data and fails the coset edge-face incidence.

Placement classes

Class	Placements	Per (C5, C3) pair
Carrier (xyz = 1)	120	2
Committed edge graph and face vertex sets, wrong edge-face incidence	180	3
Faces not triangles of the coset edge graph	300	5
Collapsed edges (C2 inside the normalizer of C5)	300	5

A check restricted to vertex-level data accepts 300 placements; the full check accepts 120. In port labels, one of the 180 places the coset edge {0, 6} on the faces {0, 1, 2} and {6, 9, 10}, while the faces containing it are {0, 3, 6} and {0, 4, 6}. A regression test corrupts one edge-face incidence of a compatible placement and confirms that the check rejects it.

Lean follow-up

The Lean bridge is scoped as a separate PR under Lean/Screen/. CoreAxioms.BoundaryPacket and CarrierUniqueness.BoundaryComplex store edges and faces as sets of ports, so their edge-face incidence is containment by definition, and the 180 placements above agree with the committed packet on exactly that data. The bridge therefore carries the coset edge-face relation as its own object and proves that it coincides with containment exactly when xyz = 1 holds (edgeFaceContainment_iff_triangleRelation), before faces_determined or counts_forced apply. Section 7 of the companion note records the proposed interface.

Scope

This PR edits no ledger file. Selection-ledger row 4 keeps its class, menu, and compression accounting; the certificate supplies a conditional replacement route in which, given SL(2, F_5) as the source, the committed boundary complex is reconstructed rather than separately supplied. Amending the row's where and receipts entries is a separate change. The reconstruction factors through the central quotient, so it cannot distinguish the source from its quotient, and it makes no physical selection of the source and no physical identification of the ports. The binary icosahedral double cover derived downstream from the port frame is not an input. The certificate makes no claim about excluding the cyclic and binary dihedral families, so the convergence question parked in #769 is untouched.

The controls file carries the discussion number because row 4 has no owner issue. If an issue is opened for this lane, the file can take the issue_NNN_negative_controls.json name.

Files

• code/a5_closure/coset_carrier_certificate.py: the certificate; Python standard library, exact integer arithmetic.
• code/a5_closure/coset_carrier_certificate.md: Theorem 769.1 with proofs, exact values, controls, formal model, acceptance matrix, and claim boundary.
• code/a5_closure/manifests/coset_carrier_reference.json, receipts/coset_carrier_reference.receipt.json, negative_controls/coset_carrier_negative_controls.json.
• code/a5_closure/tests/test_coset_carrier_certificate.py: 18 regression and adversarial tests.
• code/a5_closure/README.md: a Run line and a row in the certified table.
• tools/run_mandatory_suite.py: the test file joins the existing certificate pytest group.

Reproduction

python3 code/a5_closure/coset_carrier_certificate.py all
python3 code/a5_closure/coset_carrier_certificate.py verify --manifest code/a5_closure/manifests/coset_carrier_reference.json --receipt code/a5_closure/receipts/coset_carrier_reference.receipt.json
python3 -m pytest -q code/a5_closure/tests/test_coset_carrier_certificate.py

The certificate runs in about five seconds, and the receipt and the control bundle are byte-identical across runs and hash seeds. The patterns of tools/check_reader_style.py, applied by hand to the added files, report no hits; the tool's own globs do not cover code/a5_closure/.