From 7b08973614db110a104bf92b2565b209474191a8 Mon Sep 17 00:00:00 2001
From: Brieuc <brieuc.dlf@gmail.com>
Date: Sun, 6 Sep 2026 13:15:04 +0200
Subject: [PATCH 1/7] Seed GOLDEN-LIFT-2 port-group plan

---
 .../work/golden-lift-2-port-group-plan.md     | 335 ++++++++++++++++++
 1 file changed, 335 insertions(+)
 create mode 100644 contributions/work/golden-lift-2-port-group-plan.md

diff --git a/contributions/work/golden-lift-2-port-group-plan.md b/contributions/work/golden-lift-2-port-group-plan.md
new file mode 100644
index 000000000..3b72c88c7
--- /dev/null
+++ b/contributions/work/golden-lift-2-port-group-plan.md
@@ -0,0 +1,335 @@
+---
+status: work-plan
+claim_level: planning
+physical_claim: false
+branch: arithmon/golden-lift-2-port-group
+base: c711eef134ea4290519759bc1524bad9f9004f75
+---
+
+# GOLDEN-LIFT-2A — type the twelve-port rotation group
+
+## Goal
+
+Close the explicit group-theoretic gap left by GOLDEN-LIFT-0/1.
+
+Current exact chain:
+
+- `A5PortSixAxesBridge` gives a pointwise `60 × 6` identification between the antipodal quotient of the sixty committed twelve-port rotations and `A5SixAxes.L60`, under the fixed axis relabeling and `rowEquiv`.
+- `PSL2F5SixAxesBridge` gives a typed group isomorphism
+  `PSL2F5 ≃* SixAxisGroup`, where `SixAxisGroup` is exactly the subgroup carried by `A5SixAxes.L60`.
+
+Missing edge:
+
+```text
+PortGroup ≃* SixAxisGroup
+```
+
+where `PortGroup` is the actual subgroup of `Equiv.Perm (Fin 12)` carried by the sixty committed port rotations.
+
+Headline target:
+
+```text
+PSL2F5 ≃* PortGroup
+```
+
+This is a purely finite algebraic bridge. It does not identify the group with abstract `A5`, construct `2I`, invoke McKay, transport the golden sectors as typed representations, select `φ`, or make a physical claim.
+
+## Fresh base
+
+This branch was created from the fork's synchronized `main` at
+
+```text
+c711eef134ea4290519759bc1524bad9f9004f75
+```
+
+which is byte-identical at the ref level to `FloatingPragma/main` at branch creation time.
+
+## Recommended module
+
+```text
+Lean/Screen/A5PortGroupBridge.lean
+```
+
+Suggested namespace:
+
+```lean
+namespace OPH.A5PortGroupBridge
+```
+
+Imports:
+
+```lean
+import A5PortSixAxesBridge
+import PSL2F5SixAxesBridge
+```
+
+Do not modify the older bridges merely to make the new theorem easier unless a tiny reusable lemma is genuinely cleaner there.
+
+## 1. Reuse the existing row data rather than reclassifying the group
+
+Use:
+
+```lean
+OPH.A5PortSixAxesBridge.portEl   : Fin 60 → Equiv.Perm (Fin 12)
+OPH.A5PortSixAxesBridge.rowEquiv : Fin 60 ≃ Fin 60
+OPH.A5SixAxes.mulT               : Fin 60 → Fin 60 → Fin 60
+OPH.A5SixAxes.invT               : Fin 60 → Fin 60
+```
+
+Define multiplication and inverse indices for the port rows by transport through the already certified row equivalence:
+
+```lean
+def portMulIndex (i j : Fin 60) : Fin 60 :=
+  rowEquiv.symm (OPH.A5SixAxes.mulT (rowEquiv i) (rowEquiv j))
+
+def portInvIndex (i : Fin 60) : Fin 60 :=
+  rowEquiv.symm (OPH.A5SixAxes.invT (rowEquiv i))
+```
+
+The load-bearing new check is that these transported indices reproduce multiplication and inverse of the *actual twelve-port permutations*.
+
+Targets:
+
+```lean
+theorem portEl_zero : portEl 0 = 1
+
+theorem portEl_mul (i j : Fin 60) :
+  portEl i * portEl j = portEl (portMulIndex i j)
+
+theorem portEl_inv (i : Fin 60) :
+  (portEl i)⁻¹ = portEl (portInvIndex i)
+```
+
+Preferred proof style: pointwise equality of permutations followed by kernel-checked finite tables. Avoid asking `decide` to compare `Equiv.Perm` proof structures directly at quadratic scale.
+
+For example, prove `portEl_mul` with `Equiv.ext` and a closed finite check over `(i,j,k) : Fin 60 × Fin 60 × Fin 12`. If one monolithic `decide` is too expensive, copy `A5SixAxes.rowF_mul`'s banded strategy (5 rows of `i` per private lemma, then dispatch by bounds). This is acceptable and preferable to a cardinality argument.
+
+## 2. Define the actual port subgroup as the range of the committed rows
+
+Do not make membership depend on an arbitrary generated closure if it can be avoided. Once the three row-law lemmas above are available, define:
+
+```lean
+def PortGroup : Subgroup (Equiv.Perm (Fin 12)) where
+  carrier := Set.range portEl
+  one_mem' := ⟨0, portEl_zero.symm⟩
+  mul_mem' := by
+    rintro _ _ ⟨i, rfl⟩ ⟨j, rfl⟩
+    exact ⟨portMulIndex i j, portEl_mul i j⟩
+  inv_mem' := by
+    rintro _ ⟨i, rfl⟩
+    exact ⟨portInvIndex i, portEl_inv i⟩
+```
+
+Adjust equality directions as Lean requires.
+
+This definition makes the scientific object exact: `PortGroup` contains exactly the sixty committed permutations, not a larger generated subgroup inferred afterward.
+
+## 3. Prove row indexing is faithful
+
+Reuse the existing antipodal quotient faithfulness rather than a fresh brute-force distinctness theorem if convenient:
+
+```lean
+theorem portEl_injective : Function.Injective portEl
+```
+
+Route:
+
+- if `portEl i = portEl j`, then `quotientAxis i = quotientAxis j` pointwise;
+- apply `A5PortSixAxesBridge.quotient_action_faithful`.
+
+Then define a canonical row index for a subgroup element using its range witness:
+
+```lean
+noncomputable def portIndex (g : PortGroup) : Fin 60 :=
+  Classical.choose g.property
+
+theorem portIndex_spec (g : PortGroup) :
+  portEl (portIndex g) = g.1 := Classical.choose_spec g.property
+```
+
+and derive the expected uniqueness lemma for row elements.
+
+No scientific claim depends on the choice: injectivity proves the witness unique.
+
+## 4. Build the homomorphism to the typed six-axis subgroup
+
+`PSL2F5SixAxesBridge.SixAxisGroup` is already the exact subgroup carried by `A5SixAxes.L60`.
+
+Define:
+
+```lean
+noncomputable def portToSix :
+    PortGroup →* OPH.PSL2F5SixAxesBridge.SixAxisGroup := ...
+```
+
+Underlying map:
+
+```lean
+g ↦ ⟨OPH.A5SixAxes.el (rowEquiv (portIndex g)), OPH.A5SixAxes.el_mem _⟩
+```
+
+For the homomorphism law, first expose the row-level six-axis multiplication lemma if needed:
+
+```lean
+theorem sixEl_mul (i j : Fin 60) :
+  OPH.A5SixAxes.el i * OPH.A5SixAxes.el j =
+    OPH.A5SixAxes.el (OPH.A5SixAxes.mulT i j)
+```
+
+This should follow structurally from `A5SixAxes.el_apply` and `A5SixAxes.rowF_mul`; do not recompute the 60×60 table.
+
+The port index of a product should be forced by `portEl_mul` and `portEl_injective`.
+
+## 5. Prove bijectivity by explicit row realization
+
+Targets:
+
+```lean
+theorem portToSix_injective : Function.Injective portToSix
+
+theorem portToSix_surjective : Function.Surjective portToSix
+```
+
+Injectivity:
+
+- equality in `SixAxisGroup` gives equality of the corresponding `A5SixAxes.el` rows;
+- use `A5PortSixAxesBridge.six_axis_rows_injective` / `A5SixAxes.el_apply` as appropriate;
+- `rowEquiv` and `portEl` are injective.
+
+Surjectivity:
+
+- for `g : SixAxisGroup`, use `A5SixAxes.mem_iff_el g.property` to obtain its unique row `j`;
+- take the port row `i = rowEquiv.symm j`;
+- package `portEl i` into `PortGroup` by its range witness;
+- show it maps to `g`.
+
+Then define:
+
+```lean
+noncomputable def portGroupEquivSixAxisGroup :
+    PortGroup ≃* OPH.PSL2F5SixAxesBridge.SixAxisGroup :=
+  MulEquiv.ofBijective portToSix
+    ⟨portToSix_injective, portToSix_surjective⟩
+```
+
+## 6. Compose with GOLDEN-LIFT-1
+
+Final exact interface:
+
+```lean
+noncomputable def pslEquivPortGroup :
+    OPH.PSL2F5SixAxesBridge.PSL2F5 ≃* PortGroup :=
+  OPH.PSL2F5SixAxesBridge.psl_equiv_six_axis_group.trans
+    portGroupEquivSixAxisGroup.symm
+```
+
+Check the orientation of `.trans` / `.symm` in Lean and use the shortest typed expression that compiles.
+
+The final theorem should mean exactly:
+
+```text
+Mathlib PSL(2,F5)
+    ≃* committed six-axis subgroup
+    ≃* committed twelve-port rotation subgroup.
+```
+
+It is not an abstract classification theorem.
+
+## 7. Useful corollaries, only after the equivalence compiles
+
+Good optional facts:
+
+```lean
+theorem portGroup_card : Fintype.card PortGroup = 60
+
+theorem every_port_group_element_is_committed_row (g : PortGroup) :
+  ∃ i : Fin 60, g.1 = portEl i
+```
+
+The latter is definitionally true from `Set.range`; keep it concise.
+
+Cardinality is a corollary, never the proof of the isomorphism.
+
+Do not use `|PortGroup| = |SixAxisGroup| = 60` as the load-bearing identification.
+
+## 8. Deliberate scope boundary
+
+This revision MUST NOT claim or implement:
+
+- abstract `PSL(2,5) ≅ A5` classification;
+- `SL(2,5) ≅ 2I` / binary-icosahedral identification;
+- an `SU(2)` or quaternion realization;
+- McKay correspondence or the affine `E8` graph;
+- typed golden `3` / `3'` representations of `PSL2F5` (that is the next revision);
+- derivation or selection of `φ`;
+- `27^φ`, Koide, or any mass law;
+- physical rotations, physical Spin, or an observable.
+
+The only promotion is from a pointwise row/action bridge to a typed isomorphism of the two already committed finite groups.
+
+## 9. Suggested two-revision workflow
+
+### Revision 1 — proof surface
+
+Implement only `Lean/Screen/A5PortGroupBridge.lean` and the minimum umbrella/lake registration required to build it.
+
+Required checks before any scientific documentation promotion:
+
+```bash
+cd Lean
+lake build A5PortGroupBridge
+lake build OPHScreen
+```
+
+Run `#print axioms` on at least:
+
+- `portEl_mul`
+- `portEl_inv`
+- `portToSix_injective`
+- `portToSix_surjective`
+- the final group equivalence or its supporting theorem if the definition itself is not printable in the same way.
+
+No `sorry`, `admit`, `axiom`, or `native_decide`.
+
+Suggested commit:
+
+```text
+Add typed twelve-port rotation group bridge
+```
+
+### Revision 2 — promotion / bookkeeping
+
+Only after Revision 1 builds:
+
+- import the module from `OPHScreen.lean`;
+- register it in `Lean/lakefile.lean` if not already done in Rev.1;
+- update `Lean/docs/PROOF_INDEX.md`;
+- update the golden-sector/projective-cover claim wording only to the exact new level;
+- update novelty/falsification matrices consistently;
+- update the owning paper paragraph, replacing the old caveat that the port bridge is only pointwise;
+- regenerate the active-surface inventory;
+- refresh theorem-count floors if the threshold crosses;
+- run structural gates and the mandatory suite.
+
+Suggested commit:
+
+```text
+Document typed port-group identification
+```
+
+## 10. Falsifiers / no-cheating checks
+
+GL2A fails if any of the following occurs:
+
+- `portEl_mul` disagrees for one committed row pair and port;
+- `portEl_inv` disagrees for one committed row and port;
+- the transported row map fails the monoid law;
+- `portToSix` has a kernel or misses a committed six-axis row;
+- the proof uses only equal cardinalities to infer identification;
+- the new claim is promoted to abstract `A5`, `2I`, McKay, golden-representation transport, or physics.
+
+If `rowEquiv` does not respect multiplication, that is a scientifically useful negative result: keep the existing pointwise bridge and stop rather than altering `rowEquiv` post hoc to force the theorem without documenting the change.
+
+## 11. Next step, explicitly out of this PR
+
+If GL2A closes, GOLDEN-LIFT-2B can transport the already certified golden `3` and `3'` sectors to typed `PSL2F5` representations and prove their pullbacks to `SL2F5` are center-trivial (`-I` acts as identity). That separation should be established before any binary-spinor or McKay step.

From bc641dddbfae29561a29f9a6df954edd38ddf7f5 Mon Sep 17 00:00:00 2001
From: Brieuc <brieuc.dlf@gmail.com>
Date: Sun, 6 Sep 2026 13:17:06 +0200
Subject: [PATCH 2/7] Draft typed twelve-port rotation group bridge

---
 Lean/Screen/A5PortGroupBridge.lean | 356 +++++++++++++++++++++++++++++
 1 file changed, 356 insertions(+)
 create mode 100644 Lean/Screen/A5PortGroupBridge.lean

diff --git a/Lean/Screen/A5PortGroupBridge.lean b/Lean/Screen/A5PortGroupBridge.lean
new file mode 100644
index 000000000..9313c6478
--- /dev/null
+++ b/Lean/Screen/A5PortGroupBridge.lean
@@ -0,0 +1,356 @@
+import A5PortSixAxesBridge
+import PSL2F5SixAxesBridge
+
+namespace OPH.A5PortGroupBridge
+
+open OPH.A5PortSixAxesBridge
+open OPH.PSL2F5SixAxesBridge
+
+/-!
+# The committed twelve-port rotations as a typed finite group
+
+GOLDEN-LIFT-2A upgrades the existing pointwise bridge between the antipodal
+quotient of the sixty committed twelve-port rotations and `A5SixAxes.L60` to
+a genuine group isomorphism.
+
+The load-bearing check is multiplication on the actual `Fin 12`
+permutations.  The port-row multiplication and inverse indices are transported
+through the already certified `rowEquiv` into the exact multiplication and
+inverse tables of `A5SixAxes`; the resulting identities are then checked
+pointwise on the committed port permutations.  `PortGroup` is defined as the
+range of those sixty rows, so it contains exactly the committed rotations.
+
+The final interface composes this group with the GOLDEN-LIFT-1 equivalence and
+gives
+
+    PSL2F5 ≃* PortGroup.
+
+BOUNDARY.  This file does not prove `PSL(2,5) ≅ A5`, identify `SL(2,5)` with
+the binary icosahedral group, construct an `SU(2)` lift, invoke McKay, transport
+the golden sectors as typed representations, derive or select `φ`, state a
+mass law, or identify physical rotations. -/
+
+/-! ## 1. Transport the six-axis row law back to the committed port rows -/
+
+/-- Multiplication index for the port rows, transported through the certified
+row equivalence to the exact six-axis multiplication table. -/
+def portMulIndex (i j : Fin 60) : Fin 60 :=
+  rowEquiv.symm (OPH.A5SixAxes.mulT (rowEquiv i) (rowEquiv j))
+
+/-- Inverse index for a port row, transported through the certified row
+equivalence to the exact six-axis inverse table. -/
+def portInvIndex (i : Fin 60) : Fin 60 :=
+  rowEquiv.symm (OPH.A5SixAxes.invT (rowEquiv i))
+
+@[simp]
+theorem rowEquiv_portMulIndex (i j : Fin 60) :
+    rowEquiv (portMulIndex i j) =
+      OPH.A5SixAxes.mulT (rowEquiv i) (rowEquiv j) := by
+  simp [portMulIndex]
+
+@[simp]
+theorem rowEquiv_portInvIndex (i : Fin 60) :
+    rowEquiv (portInvIndex i) = OPH.A5SixAxes.invT (rowEquiv i) := by
+  simp [portInvIndex]
+
+@[simp]
+theorem rowEquiv_zero : rowEquiv (0 : Fin 60) = 0 := by decide
+
+/-- Row zero is the identity port permutation. -/
+theorem portEl_zero : portEl 0 = 1 := by
+  apply Equiv.ext
+  intro k
+  revert k
+  decide
+
+/- The quadratic check is split into the same five-row bands used by
+`A5SixAxes.rowF_mul`.  This keeps kernel reduction on raw action values rather
+than asking `decide` to compare `Equiv.Perm` proof structures. -/
+
+set_option maxHeartbeats 4000000 in
+set_option maxRecDepth 16384 in
+private theorem portEl_mul_band0 :
+    ∀ (i j : Fin 60) (k : Fin 12), i.val < 5 →
+      (portEl i * portEl j) k = portEl (portMulIndex i j) k := by decide
+
+set_option maxHeartbeats 4000000 in
+set_option maxRecDepth 16384 in
+private theorem portEl_mul_band1 :
+    ∀ (i j : Fin 60) (k : Fin 12), 5 ≤ i.val → i.val < 10 →
+      (portEl i * portEl j) k = portEl (portMulIndex i j) k := by decide
+
+set_option maxHeartbeats 4000000 in
+set_option maxRecDepth 16384 in
+private theorem portEl_mul_band2 :
+    ∀ (i j : Fin 60) (k : Fin 12), 10 ≤ i.val → i.val < 15 →
+      (portEl i * portEl j) k = portEl (portMulIndex i j) k := by decide
+
+set_option maxHeartbeats 4000000 in
+set_option maxRecDepth 16384 in
+private theorem portEl_mul_band3 :
+    ∀ (i j : Fin 60) (k : Fin 12), 15 ≤ i.val → i.val < 20 →
+      (portEl i * portEl j) k = portEl (portMulIndex i j) k := by decide
+
+set_option maxHeartbeats 4000000 in
+set_option maxRecDepth 16384 in
+private theorem portEl_mul_band4 :
+    ∀ (i j : Fin 60) (k : Fin 12), 20 ≤ i.val → i.val < 25 →
+      (portEl i * portEl j) k = portEl (portMulIndex i j) k := by decide
+
+set_option maxHeartbeats 4000000 in
+set_option maxRecDepth 16384 in
+private theorem portEl_mul_band5 :
+    ∀ (i j : Fin 60) (k : Fin 12), 25 ≤ i.val → i.val < 30 →
+      (portEl i * portEl j) k = portEl (portMulIndex i j) k := by decide
+
+set_option maxHeartbeats 4000000 in
+set_option maxRecDepth 16384 in
+private theorem portEl_mul_band6 :
+    ∀ (i j : Fin 60) (k : Fin 12), 30 ≤ i.val → i.val < 35 →
+      (portEl i * portEl j) k = portEl (portMulIndex i j) k := by decide
+
+set_option maxHeartbeats 4000000 in
+set_option maxRecDepth 16384 in
+private theorem portEl_mul_band7 :
+    ∀ (i j : Fin 60) (k : Fin 12), 35 ≤ i.val → i.val < 40 →
+      (portEl i * portEl j) k = portEl (portMulIndex i j) k := by decide
+
+set_option maxHeartbeats 4000000 in
+set_option maxRecDepth 16384 in
+private theorem portEl_mul_band8 :
+    ∀ (i j : Fin 60) (k : Fin 12), 40 ≤ i.val → i.val < 45 →
+      (portEl i * portEl j) k = portEl (portMulIndex i j) k := by decide
+
+set_option maxHeartbeats 4000000 in
+set_option maxRecDepth 16384 in
+private theorem portEl_mul_band9 :
+    ∀ (i j : Fin 60) (k : Fin 12), 45 ≤ i.val → i.val < 50 →
+      (portEl i * portEl j) k = portEl (portMulIndex i j) k := by decide
+
+set_option maxHeartbeats 4000000 in
+set_option maxRecDepth 16384 in
+private theorem portEl_mul_band10 :
+    ∀ (i j : Fin 60) (k : Fin 12), 50 ≤ i.val → i.val < 55 →
+      (portEl i * portEl j) k = portEl (portMulIndex i j) k := by decide
+
+set_option maxHeartbeats 4000000 in
+set_option maxRecDepth 16384 in
+private theorem portEl_mul_band11 :
+    ∀ (i j : Fin 60) (k : Fin 12), 55 ≤ i.val →
+      (portEl i * portEl j) k = portEl (portMulIndex i j) k := by decide
+
+/-- Pointwise multiplication law for all committed port rows. -/
+theorem portEl_mul_apply :
+    ∀ (i j : Fin 60) (k : Fin 12),
+      (portEl i * portEl j) k = portEl (portMulIndex i j) k := by
+  intro i j k
+  rcases Nat.lt_or_ge i.val 5 with h | h0
+  · exact portEl_mul_band0 i j k h
+  rcases Nat.lt_or_ge i.val 10 with h | h1
+  · exact portEl_mul_band1 i j k h0 h
+  rcases Nat.lt_or_ge i.val 15 with h | h2
+  · exact portEl_mul_band2 i j k h1 h
+  rcases Nat.lt_or_ge i.val 20 with h | h3
+  · exact portEl_mul_band3 i j k h2 h
+  rcases Nat.lt_or_ge i.val 25 with h | h4
+  · exact portEl_mul_band4 i j k h3 h
+  rcases Nat.lt_or_ge i.val 30 with h | h5
+  · exact portEl_mul_band5 i j k h4 h
+  rcases Nat.lt_or_ge i.val 35 with h | h6
+  · exact portEl_mul_band6 i j k h5 h
+  rcases Nat.lt_or_ge i.val 40 with h | h7
+  · exact portEl_mul_band7 i j k h6 h
+  rcases Nat.lt_or_ge i.val 45 with h | h8
+  · exact portEl_mul_band8 i j k h7 h
+  rcases Nat.lt_or_ge i.val 50 with h | h9
+  · exact portEl_mul_band9 i j k h8 h
+  rcases Nat.lt_or_ge i.val 55 with h | h10
+  · exact portEl_mul_band10 i j k h9 h
+  exact portEl_mul_band11 i j k h10
+
+/-- Multiplication of the actual twelve-port permutations is exactly the
+transported six-axis multiplication table. -/
+theorem portEl_mul (i j : Fin 60) :
+    portEl i * portEl j = portEl (portMulIndex i j) := by
+  apply Equiv.ext
+  exact portEl_mul_apply i j
+
+set_option maxHeartbeats 4000000 in
+set_option maxRecDepth 16384 in
+/-- Pointwise inverse law on the committed port rows. -/
+theorem portEl_inv_apply :
+    ∀ (i : Fin 60) (k : Fin 12),
+      (portEl i)⁻¹ k = portEl (portInvIndex i) k := by decide
+
+/-- Inversion of the actual twelve-port permutations is exactly the
+transported six-axis inverse table. -/
+theorem portEl_inv (i : Fin 60) :
+    (portEl i)⁻¹ = portEl (portInvIndex i) := by
+  apply Equiv.ext
+  exact portEl_inv_apply i
+
+/-! ## 2. The exact subgroup carried by the committed port rows -/
+
+/-- The subgroup consisting exactly of the sixty committed twelve-port
+rotations.  Range membership makes the row ancestry explicit. -/
+def PortGroup : Subgroup (Equiv.Perm (Fin 12)) where
+  carrier := Set.range portEl
+  one_mem' := ⟨0, portEl_zero⟩
+  mul_mem' := by
+    intro g h hg hh
+    obtain ⟨i, rfl⟩ := hg
+    obtain ⟨j, rfl⟩ := hh
+    exact ⟨portMulIndex i j, (portEl_mul i j).symm⟩
+  inv_mem' := by
+    intro g hg
+    obtain ⟨i, rfl⟩ := hg
+    exact ⟨portInvIndex i, (portEl_inv i).symm⟩
+
+/-- Distinct row indices give distinct committed port permutations.  The proof
+reuses the already certified faithfulness of the antipodal quotient. -/
+theorem portEl_injective : Function.Injective portEl := by
+  intro i j hij
+  apply quotient_action_faithful
+  funext x
+  simp only [quotientAxis]
+  rw [hij]
+
+/-- Choose the unique committed row underlying a `PortGroup` element. -/
+noncomputable def portIndex (g : PortGroup) : Fin 60 :=
+  Classical.choose (show ∃ i : Fin 60, portEl i = g.1 from g.property)
+
+/-- The chosen row really is the underlying port permutation. -/
+theorem portIndex_spec (g : PortGroup) : portEl (portIndex g) = g.1 :=
+  Classical.choose_spec (show ∃ i : Fin 60, portEl i = g.1 from g.property)
+
+/-- The range witness is unique, so choosing the index of a committed row
+returns that row's index. -/
+theorem portIndex_portEl (i : Fin 60) :
+    portIndex (⟨portEl i, ⟨i, rfl⟩⟩ : PortGroup) = i := by
+  apply portEl_injective
+  exact portIndex_spec _
+
+/-- The identity element has row index zero. -/
+theorem portIndex_one : portIndex (1 : PortGroup) = 0 := by
+  apply portEl_injective
+  calc
+    portEl (portIndex (1 : PortGroup)) = (1 : PortGroup).1 := portIndex_spec _
+    _ = 1 := rfl
+    _ = portEl 0 := portEl_zero.symm
+
+/-- The unique row index of a product is the transported multiplication
+index. -/
+theorem portIndex_mul (g h : PortGroup) :
+    portIndex (g * h) = portMulIndex (portIndex g) (portIndex h) := by
+  apply portEl_injective
+  calc
+    portEl (portIndex (g * h)) = (g * h).1 := portIndex_spec _
+    _ = g.1 * h.1 := rfl
+    _ = portEl (portIndex g) * portEl (portIndex h) := by
+      rw [portIndex_spec g, portIndex_spec h]
+    _ = portEl (portMulIndex (portIndex g) (portIndex h)) :=
+      portEl_mul _ _
+
+/-! ## 3. The typed homomorphism to the exact six-axis subgroup -/
+
+/-- Row zero is the identity in the explicit six-axis list. -/
+theorem sixEl_zero : OPH.A5SixAxes.el 0 = 1 := by
+  apply Equiv.ext
+  intro x
+  rw [OPH.A5SixAxes.el_apply, Equiv.Perm.one_apply]
+  revert x
+  decide
+
+/-- Multiplication of explicit six-axis rows, exposed from the already
+certified raw row table. -/
+theorem sixEl_mul (i j : Fin 60) :
+    OPH.A5SixAxes.el i * OPH.A5SixAxes.el j =
+      OPH.A5SixAxes.el (OPH.A5SixAxes.mulT i j) := by
+  apply Equiv.ext
+  intro x
+  rw [Equiv.Perm.mul_apply, OPH.A5SixAxes.el_apply,
+    OPH.A5SixAxes.el_apply, OPH.A5SixAxes.el_apply]
+  exact OPH.A5SixAxes.rowF_mul i j x
+
+/-- Send a committed port rotation to the corresponding committed six-axis
+rotation. -/
+noncomputable def portToSix : PortGroup →*
+    OPH.PSL2F5SixAxesBridge.SixAxisGroup where
+  toFun g :=
+    ⟨OPH.A5SixAxes.el (rowEquiv (portIndex g)), OPH.A5SixAxes.el_mem _⟩
+  map_one' := by
+    apply Subtype.ext
+    change OPH.A5SixAxes.el (rowEquiv (portIndex (1 : PortGroup))) = 1
+    rw [portIndex_one, rowEquiv_zero, sixEl_zero]
+  map_mul' g h := by
+    apply Subtype.ext
+    change OPH.A5SixAxes.el (rowEquiv (portIndex (g * h))) =
+      OPH.A5SixAxes.el (rowEquiv (portIndex g)) *
+        OPH.A5SixAxes.el (rowEquiv (portIndex h))
+    rw [portIndex_mul, rowEquiv_portMulIndex]
+    exact (sixEl_mul _ _).symm
+
+/-- The port-to-six-axis homomorphism has trivial kernel. -/
+theorem portToSix_injective : Function.Injective portToSix := by
+  intro g h hgh
+  have hval :
+      OPH.A5SixAxes.el (rowEquiv (portIndex g)) =
+        OPH.A5SixAxes.el (rowEquiv (portIndex h)) :=
+    congrArg Subtype.val hgh
+  have hrow :
+      OPH.A5SixAxes.rowF (rowEquiv (portIndex g)) =
+        OPH.A5SixAxes.rowF (rowEquiv (portIndex h)) := by
+    funext x
+    have hx := congrFun hval x
+    simpa only [OPH.A5SixAxes.el_apply] using hx
+  have hidx : rowEquiv (portIndex g) = rowEquiv (portIndex h) :=
+    six_axis_rows_injective hrow
+  have hpidx : portIndex g = portIndex h := rowEquiv.injective hidx
+  apply Subtype.ext
+  calc
+    g.1 = portEl (portIndex g) := (portIndex_spec g).symm
+    _ = portEl (portIndex h) := congrArg portEl hpidx
+    _ = h.1 := portIndex_spec h
+
+/-- Every committed six-axis group element comes from one committed port
+rotation. -/
+theorem portToSix_surjective : Function.Surjective portToSix := by
+  intro g
+  obtain ⟨j, hj⟩ := OPH.A5SixAxes.mem_iff_el g.property
+  let i : Fin 60 := rowEquiv.symm j
+  let p : PortGroup := ⟨portEl i, ⟨i, rfl⟩⟩
+  refine ⟨p, ?_⟩
+  apply Subtype.ext
+  change OPH.A5SixAxes.el (rowEquiv (portIndex p)) = g.1
+  have hpi : portIndex p = i := by
+    dsimp [p]
+    exact portIndex_portEl i
+  rw [hpi]
+  change OPH.A5SixAxes.el (rowEquiv (rowEquiv.symm j)) = g.1
+  rw [rowEquiv.apply_symm_apply]
+  exact hj.symm
+
+/-- The actual twelve-port rotation subgroup is isomorphic to the exact
+committed six-axis subgroup. -/
+noncomputable def portGroupEquivSixAxisGroup :
+    PortGroup ≃* OPH.PSL2F5SixAxesBridge.SixAxisGroup :=
+  MulEquiv.ofBijective portToSix
+    ⟨portToSix_injective, portToSix_surjective⟩
+
+/-- GOLDEN-LIFT-2A headline interface: Mathlib's abstract projective group is
+isomorphic to the subgroup of the sixty committed twelve-port rotations. -/
+noncomputable def pslEquivPortGroup :
+    OPH.PSL2F5SixAxesBridge.PSL2F5 ≃* PortGroup :=
+  OPH.PSL2F5SixAxesBridge.psl_equiv_six_axis_group.trans
+    portGroupEquivSixAxisGroup.symm
+
+end OPH.A5PortGroupBridge
+
+/- Axiom audit: standard axioms only are intended; no `sorry`, `admit`, new
+axioms, or `native_decide`. -/
+
+#print axioms OPH.A5PortGroupBridge.portEl_mul
+#print axioms OPH.A5PortGroupBridge.portEl_inv
+#print axioms OPH.A5PortGroupBridge.portEl_injective
+#print axioms OPH.A5PortGroupBridge.portToSix_injective
+#print axioms OPH.A5PortGroupBridge.portToSix_surjective

From dc7cd4b76a5008ff706103d3a85cf096b6de4243 Mon Sep 17 00:00:00 2001
From: Brieuc <brieuc.dlf@gmail.com>
Date: Sun, 6 Sep 2026 13:38:14 +0200
Subject: [PATCH 3/7] Drop GOLDEN-LIFT-2 work plan from proof branch

---
 .../work/golden-lift-2-port-group-plan.md     | 335 ------------------
 1 file changed, 335 deletions(-)
 delete mode 100644 contributions/work/golden-lift-2-port-group-plan.md

diff --git a/contributions/work/golden-lift-2-port-group-plan.md b/contributions/work/golden-lift-2-port-group-plan.md
deleted file mode 100644
index 3b72c88c7..000000000
--- a/contributions/work/golden-lift-2-port-group-plan.md
+++ /dev/null
@@ -1,335 +0,0 @@
----
-status: work-plan
-claim_level: planning
-physical_claim: false
-branch: arithmon/golden-lift-2-port-group
-base: c711eef134ea4290519759bc1524bad9f9004f75
----
-
-# GOLDEN-LIFT-2A — type the twelve-port rotation group
-
-## Goal
-
-Close the explicit group-theoretic gap left by GOLDEN-LIFT-0/1.
-
-Current exact chain:
-
-- `A5PortSixAxesBridge` gives a pointwise `60 × 6` identification between the antipodal quotient of the sixty committed twelve-port rotations and `A5SixAxes.L60`, under the fixed axis relabeling and `rowEquiv`.
-- `PSL2F5SixAxesBridge` gives a typed group isomorphism
-  `PSL2F5 ≃* SixAxisGroup`, where `SixAxisGroup` is exactly the subgroup carried by `A5SixAxes.L60`.
-
-Missing edge:
-
-```text
-PortGroup ≃* SixAxisGroup
-```
-
-where `PortGroup` is the actual subgroup of `Equiv.Perm (Fin 12)` carried by the sixty committed port rotations.
-
-Headline target:
-
-```text
-PSL2F5 ≃* PortGroup
-```
-
-This is a purely finite algebraic bridge. It does not identify the group with abstract `A5`, construct `2I`, invoke McKay, transport the golden sectors as typed representations, select `φ`, or make a physical claim.
-
-## Fresh base
-
-This branch was created from the fork's synchronized `main` at
-
-```text
-c711eef134ea4290519759bc1524bad9f9004f75
-```
-
-which is byte-identical at the ref level to `FloatingPragma/main` at branch creation time.
-
-## Recommended module
-
-```text
-Lean/Screen/A5PortGroupBridge.lean
-```
-
-Suggested namespace:
-
-```lean
-namespace OPH.A5PortGroupBridge
-```
-
-Imports:
-
-```lean
-import A5PortSixAxesBridge
-import PSL2F5SixAxesBridge
-```
-
-Do not modify the older bridges merely to make the new theorem easier unless a tiny reusable lemma is genuinely cleaner there.
-
-## 1. Reuse the existing row data rather than reclassifying the group
-
-Use:
-
-```lean
-OPH.A5PortSixAxesBridge.portEl   : Fin 60 → Equiv.Perm (Fin 12)
-OPH.A5PortSixAxesBridge.rowEquiv : Fin 60 ≃ Fin 60
-OPH.A5SixAxes.mulT               : Fin 60 → Fin 60 → Fin 60
-OPH.A5SixAxes.invT               : Fin 60 → Fin 60
-```
-
-Define multiplication and inverse indices for the port rows by transport through the already certified row equivalence:
-
-```lean
-def portMulIndex (i j : Fin 60) : Fin 60 :=
-  rowEquiv.symm (OPH.A5SixAxes.mulT (rowEquiv i) (rowEquiv j))
-
-def portInvIndex (i : Fin 60) : Fin 60 :=
-  rowEquiv.symm (OPH.A5SixAxes.invT (rowEquiv i))
-```
-
-The load-bearing new check is that these transported indices reproduce multiplication and inverse of the *actual twelve-port permutations*.
-
-Targets:
-
-```lean
-theorem portEl_zero : portEl 0 = 1
-
-theorem portEl_mul (i j : Fin 60) :
-  portEl i * portEl j = portEl (portMulIndex i j)
-
-theorem portEl_inv (i : Fin 60) :
-  (portEl i)⁻¹ = portEl (portInvIndex i)
-```
-
-Preferred proof style: pointwise equality of permutations followed by kernel-checked finite tables. Avoid asking `decide` to compare `Equiv.Perm` proof structures directly at quadratic scale.
-
-For example, prove `portEl_mul` with `Equiv.ext` and a closed finite check over `(i,j,k) : Fin 60 × Fin 60 × Fin 12`. If one monolithic `decide` is too expensive, copy `A5SixAxes.rowF_mul`'s banded strategy (5 rows of `i` per private lemma, then dispatch by bounds). This is acceptable and preferable to a cardinality argument.
-
-## 2. Define the actual port subgroup as the range of the committed rows
-
-Do not make membership depend on an arbitrary generated closure if it can be avoided. Once the three row-law lemmas above are available, define:
-
-```lean
-def PortGroup : Subgroup (Equiv.Perm (Fin 12)) where
-  carrier := Set.range portEl
-  one_mem' := ⟨0, portEl_zero.symm⟩
-  mul_mem' := by
-    rintro _ _ ⟨i, rfl⟩ ⟨j, rfl⟩
-    exact ⟨portMulIndex i j, portEl_mul i j⟩
-  inv_mem' := by
-    rintro _ ⟨i, rfl⟩
-    exact ⟨portInvIndex i, portEl_inv i⟩
-```
-
-Adjust equality directions as Lean requires.
-
-This definition makes the scientific object exact: `PortGroup` contains exactly the sixty committed permutations, not a larger generated subgroup inferred afterward.
-
-## 3. Prove row indexing is faithful
-
-Reuse the existing antipodal quotient faithfulness rather than a fresh brute-force distinctness theorem if convenient:
-
-```lean
-theorem portEl_injective : Function.Injective portEl
-```
-
-Route:
-
-- if `portEl i = portEl j`, then `quotientAxis i = quotientAxis j` pointwise;
-- apply `A5PortSixAxesBridge.quotient_action_faithful`.
-
-Then define a canonical row index for a subgroup element using its range witness:
-
-```lean
-noncomputable def portIndex (g : PortGroup) : Fin 60 :=
-  Classical.choose g.property
-
-theorem portIndex_spec (g : PortGroup) :
-  portEl (portIndex g) = g.1 := Classical.choose_spec g.property
-```
-
-and derive the expected uniqueness lemma for row elements.
-
-No scientific claim depends on the choice: injectivity proves the witness unique.
-
-## 4. Build the homomorphism to the typed six-axis subgroup
-
-`PSL2F5SixAxesBridge.SixAxisGroup` is already the exact subgroup carried by `A5SixAxes.L60`.
-
-Define:
-
-```lean
-noncomputable def portToSix :
-    PortGroup →* OPH.PSL2F5SixAxesBridge.SixAxisGroup := ...
-```
-
-Underlying map:
-
-```lean
-g ↦ ⟨OPH.A5SixAxes.el (rowEquiv (portIndex g)), OPH.A5SixAxes.el_mem _⟩
-```
-
-For the homomorphism law, first expose the row-level six-axis multiplication lemma if needed:
-
-```lean
-theorem sixEl_mul (i j : Fin 60) :
-  OPH.A5SixAxes.el i * OPH.A5SixAxes.el j =
-    OPH.A5SixAxes.el (OPH.A5SixAxes.mulT i j)
-```
-
-This should follow structurally from `A5SixAxes.el_apply` and `A5SixAxes.rowF_mul`; do not recompute the 60×60 table.
-
-The port index of a product should be forced by `portEl_mul` and `portEl_injective`.
-
-## 5. Prove bijectivity by explicit row realization
-
-Targets:
-
-```lean
-theorem portToSix_injective : Function.Injective portToSix
-
-theorem portToSix_surjective : Function.Surjective portToSix
-```
-
-Injectivity:
-
-- equality in `SixAxisGroup` gives equality of the corresponding `A5SixAxes.el` rows;
-- use `A5PortSixAxesBridge.six_axis_rows_injective` / `A5SixAxes.el_apply` as appropriate;
-- `rowEquiv` and `portEl` are injective.
-
-Surjectivity:
-
-- for `g : SixAxisGroup`, use `A5SixAxes.mem_iff_el g.property` to obtain its unique row `j`;
-- take the port row `i = rowEquiv.symm j`;
-- package `portEl i` into `PortGroup` by its range witness;
-- show it maps to `g`.
-
-Then define:
-
-```lean
-noncomputable def portGroupEquivSixAxisGroup :
-    PortGroup ≃* OPH.PSL2F5SixAxesBridge.SixAxisGroup :=
-  MulEquiv.ofBijective portToSix
-    ⟨portToSix_injective, portToSix_surjective⟩
-```
-
-## 6. Compose with GOLDEN-LIFT-1
-
-Final exact interface:
-
-```lean
-noncomputable def pslEquivPortGroup :
-    OPH.PSL2F5SixAxesBridge.PSL2F5 ≃* PortGroup :=
-  OPH.PSL2F5SixAxesBridge.psl_equiv_six_axis_group.trans
-    portGroupEquivSixAxisGroup.symm
-```
-
-Check the orientation of `.trans` / `.symm` in Lean and use the shortest typed expression that compiles.
-
-The final theorem should mean exactly:
-
-```text
-Mathlib PSL(2,F5)
-    ≃* committed six-axis subgroup
-    ≃* committed twelve-port rotation subgroup.
-```
-
-It is not an abstract classification theorem.
-
-## 7. Useful corollaries, only after the equivalence compiles
-
-Good optional facts:
-
-```lean
-theorem portGroup_card : Fintype.card PortGroup = 60
-
-theorem every_port_group_element_is_committed_row (g : PortGroup) :
-  ∃ i : Fin 60, g.1 = portEl i
-```
-
-The latter is definitionally true from `Set.range`; keep it concise.
-
-Cardinality is a corollary, never the proof of the isomorphism.
-
-Do not use `|PortGroup| = |SixAxisGroup| = 60` as the load-bearing identification.
-
-## 8. Deliberate scope boundary
-
-This revision MUST NOT claim or implement:
-
-- abstract `PSL(2,5) ≅ A5` classification;
-- `SL(2,5) ≅ 2I` / binary-icosahedral identification;
-- an `SU(2)` or quaternion realization;
-- McKay correspondence or the affine `E8` graph;
-- typed golden `3` / `3'` representations of `PSL2F5` (that is the next revision);
-- derivation or selection of `φ`;
-- `27^φ`, Koide, or any mass law;
-- physical rotations, physical Spin, or an observable.
-
-The only promotion is from a pointwise row/action bridge to a typed isomorphism of the two already committed finite groups.
-
-## 9. Suggested two-revision workflow
-
-### Revision 1 — proof surface
-
-Implement only `Lean/Screen/A5PortGroupBridge.lean` and the minimum umbrella/lake registration required to build it.
-
-Required checks before any scientific documentation promotion:
-
-```bash
-cd Lean
-lake build A5PortGroupBridge
-lake build OPHScreen
-```
-
-Run `#print axioms` on at least:
-
-- `portEl_mul`
-- `portEl_inv`
-- `portToSix_injective`
-- `portToSix_surjective`
-- the final group equivalence or its supporting theorem if the definition itself is not printable in the same way.
-
-No `sorry`, `admit`, `axiom`, or `native_decide`.
-
-Suggested commit:
-
-```text
-Add typed twelve-port rotation group bridge
-```
-
-### Revision 2 — promotion / bookkeeping
-
-Only after Revision 1 builds:
-
-- import the module from `OPHScreen.lean`;
-- register it in `Lean/lakefile.lean` if not already done in Rev.1;
-- update `Lean/docs/PROOF_INDEX.md`;
-- update the golden-sector/projective-cover claim wording only to the exact new level;
-- update novelty/falsification matrices consistently;
-- update the owning paper paragraph, replacing the old caveat that the port bridge is only pointwise;
-- regenerate the active-surface inventory;
-- refresh theorem-count floors if the threshold crosses;
-- run structural gates and the mandatory suite.
-
-Suggested commit:
-
-```text
-Document typed port-group identification
-```
-
-## 10. Falsifiers / no-cheating checks
-
-GL2A fails if any of the following occurs:
-
-- `portEl_mul` disagrees for one committed row pair and port;
-- `portEl_inv` disagrees for one committed row and port;
-- the transported row map fails the monoid law;
-- `portToSix` has a kernel or misses a committed six-axis row;
-- the proof uses only equal cardinalities to infer identification;
-- the new claim is promoted to abstract `A5`, `2I`, McKay, golden-representation transport, or physics.
-
-If `rowEquiv` does not respect multiplication, that is a scientifically useful negative result: keep the existing pointwise bridge and stop rather than altering `rowEquiv` post hoc to force the theorem without documenting the change.
-
-## 11. Next step, explicitly out of this PR
-
-If GL2A closes, GOLDEN-LIFT-2B can transport the already certified golden `3` and `3'` sectors to typed `PSL2F5` representations and prove their pullbacks to `SL2F5` are center-trivial (`-I` acts as identity). That separation should be established before any binary-spinor or McKay step.

From 7b87385d18d5516df6a95288c32a9466a38c1bf8 Mon Sep 17 00:00:00 2001
From: Brieuc <brieuc.dlf@gmail.com>
Date: Sun, 6 Sep 2026 13:38:43 +0200
Subject: [PATCH 4/7] Register twelve-port group bridge in OPHScreen

---
 Lean/lakefile.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Lean/lakefile.lean b/Lean/lakefile.lean
index edce0eaa0..ee0948f3e 100644
--- a/Lean/lakefile.lean
+++ b/Lean/lakefile.lean
@@ -75,7 +75,7 @@ lean_lib «OPHScreen» where
     `PortFrameGram, `A5PortAction, `A5CouplingSymmetry, `A5OPH,
     `A2HolonomyBridge, `HolonomyInterference, `A5CharacterField, `A5SixAxes,
     `PSL2F5SixAxesBridge,
-    `A5PortModule, `A5PortSixAxesBridge, `A5Commutant, `A5ResponseWordAlgebra,
+    `A5PortModule, `A5PortSixAxesBridge, `A5PortGroupBridge, `A5Commutant, `A5ResponseWordAlgebra,
     `A5IncidenceResponse, `TraceBalancedKernel, `TrichotomyCases, `Z6Descent,
     `A5AngularMultiplets, `A5AngularBands, `A5AngularKernels,
     `ExteriorSelection, `WeylYukawaConventions, `QuarkMeanDomain, `EqualStateWeights,
@@ -126,4 +126,4 @@ lean_lib «OPHConstruction» where
     `QFT, `Variational]
 
 lean_exe «oph» where
-  root := `Main
+  root := `Main
\ No newline at end of file

From c55d4ef51712ac271f8b0be1ff67445d740aadf9 Mon Sep 17 00:00:00 2001
From: Brieuc <brieuc.dlf@gmail.com>
Date: Sun, 6 Sep 2026 13:38:53 +0200
Subject: [PATCH 5/7] Import twelve-port group bridge in OPHScreen

---
 Lean/Screen/OPHScreen.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Lean/Screen/OPHScreen.lean b/Lean/Screen/OPHScreen.lean
index e03f3c297..63fc2bc57 100644
--- a/Lean/Screen/OPHScreen.lean
+++ b/Lean/Screen/OPHScreen.lean
@@ -50,6 +50,7 @@ import QuantumMatterIntegration
 import B10EdgeCenterAction
 import B10QuantumLimitations
 import PSL2F5SixAxesBridge
+import A5PortGroupBridge
 
 /-!
 # OPH screen arithmetic umbrella
@@ -57,4 +58,4 @@ import PSL2F5SixAxesBridge
 Root module for the independently configured `OPHScreen` Lean library. Each
 import retains its own stated scope boundary; this file adds no theorem or
 physical identification.
--/
+-/
\ No newline at end of file

From 3c7edfd4b4cb05529f3c0b129f9514866d4d603f Mon Sep 17 00:00:00 2001
From: Brieuc <brieuc.dlf@gmail.com>
Date: Sun, 6 Sep 2026 13:39:41 +0200
Subject: [PATCH 6/7] Align port-group bridge with upstream proof conventions

---
 Lean/Screen/A5PortGroupBridge.lean | 46 +++++++++++++++---------------
 1 file changed, 23 insertions(+), 23 deletions(-)

diff --git a/Lean/Screen/A5PortGroupBridge.lean b/Lean/Screen/A5PortGroupBridge.lean
index 9313c6478..3eacf6dec 100644
--- a/Lean/Screen/A5PortGroupBridge.lean
+++ b/Lean/Screen/A5PortGroupBridge.lean
@@ -9,23 +9,21 @@ open OPH.PSL2F5SixAxesBridge
 /-!
 # The committed twelve-port rotations as a typed finite group
 
-GOLDEN-LIFT-2A upgrades the existing pointwise bridge between the antipodal
-quotient of the sixty committed twelve-port rotations and `A5SixAxes.L60` to
-a genuine group isomorphism.
+The sixty committed twelve-port rotations are packaged as a subgroup of
+`Equiv.Perm (Fin 12)` and identified with the committed six-axis subgroup.
 
 The load-bearing check is multiplication on the actual `Fin 12`
-permutations.  The port-row multiplication and inverse indices are transported
-through the already certified `rowEquiv` into the exact multiplication and
-inverse tables of `A5SixAxes`; the resulting identities are then checked
-pointwise on the committed port permutations.  `PortGroup` is defined as the
-range of those sixty rows, so it contains exactly the committed rotations.
+permutations. The port-row multiplication and inverse indices are transported
+through the certified `rowEquiv` into the exact multiplication and inverse
+tables of `A5SixAxes`; the resulting identities are then checked pointwise on
+the committed port permutations. `PortGroup` is defined as the range of those
+sixty rows, so it contains exactly the committed rotations.
 
-The final interface composes this group with the GOLDEN-LIFT-1 equivalence and
-gives
+Composing this group isomorphism with `psl_equiv_six_axis_group` gives
 
     PSL2F5 ≃* PortGroup.
 
-BOUNDARY.  This file does not prove `PSL(2,5) ≅ A5`, identify `SL(2,5)` with
+BOUNDARY. This file does not prove `PSL(2,5) ≅ A5`, identify `SL(2,5)` with
 the binary icosahedral group, construct an `SU(2)` lift, invoke McKay, transport
 the golden sectors as typed representations, derive or select `φ`, state a
 mass law, or identify physical rotations. -/
@@ -64,7 +62,7 @@ theorem portEl_zero : portEl 0 = 1 := by
   decide
 
 /- The quadratic check is split into the same five-row bands used by
-`A5SixAxes.rowF_mul`.  This keeps kernel reduction on raw action values rather
+`A5SixAxes.rowF_mul`. This keeps kernel reduction on raw action values rather
 than asking `decide` to compare `Equiv.Perm` proof structures. -/
 
 set_option maxHeartbeats 4000000 in
@@ -192,7 +190,7 @@ theorem portEl_inv (i : Fin 60) :
 /-! ## 2. The exact subgroup carried by the committed port rows -/
 
 /-- The subgroup consisting exactly of the sixty committed twelve-port
-rotations.  Range membership makes the row ancestry explicit. -/
+rotations. Range membership makes the row ancestry explicit. -/
 def PortGroup : Subgroup (Equiv.Perm (Fin 12)) where
   carrier := Set.range portEl
   one_mem' := ⟨0, portEl_zero⟩
@@ -206,8 +204,8 @@ def PortGroup : Subgroup (Equiv.Perm (Fin 12)) where
     obtain ⟨i, rfl⟩ := hg
     exact ⟨portInvIndex i, (portEl_inv i).symm⟩
 
-/-- Distinct row indices give distinct committed port permutations.  The proof
-reuses the already certified faithfulness of the antipodal quotient. -/
+/-- Distinct row indices give distinct committed port permutations. The proof
+reuses the certified faithfulness of the antipodal quotient. -/
 theorem portEl_injective : Function.Injective portEl := by
   intro i j hij
   apply quotient_action_faithful
@@ -219,7 +217,7 @@ theorem portEl_injective : Function.Injective portEl := by
 noncomputable def portIndex (g : PortGroup) : Fin 60 :=
   Classical.choose (show ∃ i : Fin 60, portEl i = g.1 from g.property)
 
-/-- The chosen row really is the underlying port permutation. -/
+/-- The chosen row is the underlying port permutation. -/
 theorem portIndex_spec (g : PortGroup) : portEl (portIndex g) = g.1 :=
   Classical.choose_spec (show ∃ i : Fin 60, portEl i = g.1 from g.property)
 
@@ -261,8 +259,8 @@ theorem sixEl_zero : OPH.A5SixAxes.el 0 = 1 := by
   revert x
   decide
 
-/-- Multiplication of explicit six-axis rows, exposed from the already
-certified raw row table. -/
+/-- Multiplication of explicit six-axis rows, exposed from the certified raw
+row table. -/
 theorem sixEl_mul (i j : Fin 60) :
     OPH.A5SixAxes.el i * OPH.A5SixAxes.el j =
       OPH.A5SixAxes.el (OPH.A5SixAxes.mulT i j) := by
@@ -290,7 +288,7 @@ noncomputable def portToSix : PortGroup →*
     rw [portIndex_mul, rowEquiv_portMulIndex]
     exact (sixEl_mul _ _).symm
 
-/-- The port-to-six-axis homomorphism has trivial kernel. -/
+/-- The port-to-six-axis homomorphism is injective. -/
 theorem portToSix_injective : Function.Injective portToSix := by
   intro g h hgh
   have hval :
@@ -337,8 +335,8 @@ noncomputable def portGroupEquivSixAxisGroup :
   MulEquiv.ofBijective portToSix
     ⟨portToSix_injective, portToSix_surjective⟩
 
-/-- GOLDEN-LIFT-2A headline interface: Mathlib's abstract projective group is
-isomorphic to the subgroup of the sixty committed twelve-port rotations. -/
+/-- Mathlib's abstract projective group is isomorphic to the subgroup of the
+sixty committed twelve-port rotations. -/
 noncomputable def pslEquivPortGroup :
     OPH.PSL2F5SixAxesBridge.PSL2F5 ≃* PortGroup :=
   OPH.PSL2F5SixAxesBridge.psl_equiv_six_axis_group.trans
@@ -346,11 +344,13 @@ noncomputable def pslEquivPortGroup :
 
 end OPH.A5PortGroupBridge
 
-/- Axiom audit: standard axioms only are intended; no `sorry`, `admit`, new
-axioms, or `native_decide`. -/
+/- Axiom audit: no `sorry`, `admit`, new axioms, or `native_decide`. -/
 
+#print axioms OPH.A5PortGroupBridge.portEl_zero
 #print axioms OPH.A5PortGroupBridge.portEl_mul
 #print axioms OPH.A5PortGroupBridge.portEl_inv
 #print axioms OPH.A5PortGroupBridge.portEl_injective
 #print axioms OPH.A5PortGroupBridge.portToSix_injective
 #print axioms OPH.A5PortGroupBridge.portToSix_surjective
+#print axioms OPH.A5PortGroupBridge.portGroupEquivSixAxisGroup
+#print axioms OPH.A5PortGroupBridge.pslEquivPortGroup
\ No newline at end of file

From 2742ad7788e3dfa7cfe85883d094755d8063976b Mon Sep 17 00:00:00 2001
From: Brieuc <153361179+Brieuc@users.noreply.github.com>
Date: Sun, 6 Sep 2026 16:43:40 +0200
Subject: [PATCH 7/7] Fix port-group injectivity and register the Screen
 surface

portToSix_injective compared Equiv.Perm values with congrFun, so the
module failed to elaborate and the iso depended on sorryAx. Evaluate
through el_apply instead, restore trailing newlines, add the PROOF_INDEX
entry, and regenerate the active-surface inventory.
---
 Lean/Screen/A5PortGroupBridge.lean   |  6 +++---
 Lean/Screen/OPHScreen.lean           |  2 +-
 Lean/docs/PROOF_INDEX.md             | 17 +++++++++++++++--
 Lean/lakefile.lean                   |  2 +-
 claims/active_surface_inventory.json |  7 ++++++-
 5 files changed, 26 insertions(+), 8 deletions(-)

diff --git a/Lean/Screen/A5PortGroupBridge.lean b/Lean/Screen/A5PortGroupBridge.lean
index 3eacf6dec..f4c0b0ae0 100644
--- a/Lean/Screen/A5PortGroupBridge.lean
+++ b/Lean/Screen/A5PortGroupBridge.lean
@@ -299,8 +299,8 @@ theorem portToSix_injective : Function.Injective portToSix := by
       OPH.A5SixAxes.rowF (rowEquiv (portIndex g)) =
         OPH.A5SixAxes.rowF (rowEquiv (portIndex h)) := by
     funext x
-    have hx := congrFun hval x
-    simpa only [OPH.A5SixAxes.el_apply] using hx
+    simpa [OPH.A5SixAxes.el_apply] using
+      congrArg (fun e : Equiv.Perm (Fin 6) => e x) hval
   have hidx : rowEquiv (portIndex g) = rowEquiv (portIndex h) :=
     six_axis_rows_injective hrow
   have hpidx : portIndex g = portIndex h := rowEquiv.injective hidx
@@ -353,4 +353,4 @@ end OPH.A5PortGroupBridge
 #print axioms OPH.A5PortGroupBridge.portToSix_injective
 #print axioms OPH.A5PortGroupBridge.portToSix_surjective
 #print axioms OPH.A5PortGroupBridge.portGroupEquivSixAxisGroup
-#print axioms OPH.A5PortGroupBridge.pslEquivPortGroup
\ No newline at end of file
+#print axioms OPH.A5PortGroupBridge.pslEquivPortGroup
diff --git a/Lean/Screen/OPHScreen.lean b/Lean/Screen/OPHScreen.lean
index 63fc2bc57..a47b66a2e 100644
--- a/Lean/Screen/OPHScreen.lean
+++ b/Lean/Screen/OPHScreen.lean
@@ -58,4 +58,4 @@ import A5PortGroupBridge
 Root module for the independently configured `OPHScreen` Lean library. Each
 import retains its own stated scope boundary; this file adds no theorem or
 physical identification.
--/
\ No newline at end of file
+-/
diff --git a/Lean/docs/PROOF_INDEX.md b/Lean/docs/PROOF_INDEX.md
index 1aa79e9e8..1fe428a4d 100644
--- a/Lean/docs/PROOF_INDEX.md
+++ b/Lean/docs/PROOF_INDEX.md
@@ -1179,8 +1179,21 @@ Mapping between Lean 4 theorems in this project and statements in
   `PSL2F5 ≃* SixAxisGroup`.  This does not prove an abstract `PSL(2,5) ≅ A5`
   classification, identify `SL(2,5)` with `2I`, invoke McKay, transport the
   golden sectors as typed `PSL2F5` representations, select `φ` or a mass law,
-  or make a physical claim.  The preceding port bridge remains a pointwise
-  indexed-row bridge, not a group-homomorphism arrow in this chain.
+  or make a physical claim.  The preceding antipodal port bridge remains a
+  pointwise indexed-row equivalence of committed actions; the subsequent
+  twelve-port group bridge promotes those rows to a typed group isomorphism.
+- Twelve-port rotation group bridge
+  (`Screen/A5PortGroupBridge.lean`): sorry-free, standard axioms, no
+  `native_decide`.  Packages the sixty committed twelve-port rotations as the
+  subgroup `PortGroup` of `Equiv.Perm (Fin 12)` whose carrier is exactly
+  `Set.range portEl`.  Kernel `decide` checks multiplication and inversion on
+  the actual `Fin 12` permutations against the `rowEquiv`-transported
+  six-axis tables; `portEl` is injective, so the carrier has cardinality
+  sixty.  The resulting isomorphism `PortGroup ≃* SixAxisGroup` composes with
+  `psl_equiv_six_axis_group` to give `PSL2F5 ≃* PortGroup`.  This does not
+  prove an abstract `PSL(2,5) ≅ A5` classification, identify `SL(2,5)` with
+  `2I`, invoke McKay, transport the golden sectors as typed representations,
+  select `φ` or a mass law, or make a physical claim.
 - Universal cap coupling from icosahedral symmetry
   (`Screen/A5CouplingSymmetry.lean`, #576/#568): 9 / 9 declarations,
   sorry-free, standard axioms. Finite facts by kernel `decide` (caps map to
diff --git a/Lean/lakefile.lean b/Lean/lakefile.lean
index ee0948f3e..fe646de6a 100644
--- a/Lean/lakefile.lean
+++ b/Lean/lakefile.lean
@@ -126,4 +126,4 @@ lean_lib «OPHConstruction» where
     `QFT, `Variational]
 
 lean_exe «oph» where
-  root := `Main
\ No newline at end of file
+  root := `Main
diff --git a/claims/active_surface_inventory.json b/claims/active_surface_inventory.json
index 92a3c5d49..ccb942ef6 100644
--- a/claims/active_surface_inventory.json
+++ b/claims/active_surface_inventory.json
@@ -1,7 +1,7 @@
 {
   "schema": "oph.active_surface_inventory.v1",
   "generator": "tools/check_axiom_consistency.py --inventory",
-  "surface_count": 362,
+  "surface_count": 363,
   "entry_surfaces": [
     "README.md",
     "README_FR.md",
@@ -774,6 +774,11 @@
       "glob": "Lean/Screen/*.lean",
       "allowlisted": false
     },
+    {
+      "path": "Lean/Screen/A5PortGroupBridge.lean",
+      "glob": "Lean/Screen/*.lean",
+      "allowlisted": false
+    },
     {
       "path": "Lean/Screen/A5PortModule.lean",
       "glob": "Lean/Screen/*.lean",