GOLDEN-LIFT-2: typed twelve-port rotation group bridge (PSL2F5 ≃* PortGroup)

[gift-framework]

Summary

Packages the sixty committed twelve-port rotations as a typed subgroup PortGroup of Equiv.Perm (Fin 12) (carrier = Set.range portEl) and proves the group isomorphism PortGroup ≃* SixAxisGroup, hence PSL2F5 ≃* PortGroup by composition with psl_equiv_six_axis_group.

• Lean/Screen/A5PortGroupBridge.lean: multiplication and inversion checked by kernel decide on the actual Fin 12 permutations (twelve five-row bands) against the rowEquiv-transported six-axis tables; portEl injective via the certified antipodal faithfulness; portToSix injective and surjective; MulEquiv.ofBijective.
• Registered in OPHScreen and the lakefile; PROOF_INDEX entry; active-surface inventory regenerated (363 surfaces after rebase on main).

Boundary

Does not prove an abstract PSL(2,5) ≅ A5 classification, identify SL(2,5) with the binary icosahedral group, invoke McKay, transport the golden sectors as typed representations, select φ or a mass law, or make a physical claim.

Verification

• Local lake build: success, 8700 jobs, 0 errors, 0 sorryAx; #print axioms on the eight surfaced declarations: propext, Classical.choice, Quot.sound only; no native_decide.
• Lean CI: green on the rebased branch.
• Mandatory Suite: green (4 shards).
• tools/check_axiom_consistency.py --check-inventory: OK.

Notes

• Rebased on main (1443e0a); the only conflict was the generated inventory, regenerated with tools/check_axiom_consistency.py --inventory.
• Minor prose debt: the PROOF_INDEX entry says "the carrier has cardinality sixty"; injectivity of portEl is proved but no typed lemma states Nat.card PortGroup = 60.

🤖 Generated with Claude Code

https://claude.ai/code/session_01WSJVBCnUZ6DQoYqp1CFt8Q