[Lexovian]

Phase 3 Sprint 1: GAP-0190 (The Crown Jewel) Formal Verification

What is Formalized:

• GAP Source Anchor: lib/grpperm.gi:SizePermGroup (lines 350–480).
• IPLD Task CID: baguqeerabfmumkhx4awa3al6rthhculmjln7lhbwsw72b2elwll5rxyb2e5a.
• Lean 4 Module: RequestProject.Gap.Library.Grpperm.
• Data Structures:
  • PermGroup α: Concrete permutation group representation storing generators and Schreier-Sims stabilizer chain (StabChain α).
  • support: Support degree computation (LargestMovedPoint).
  • transversalInverses, transversalRepresentatives, transversalWords: Explicit transversal word factorization.

Proved Theorems (0 sorry, 0 admit):

1. sizeStabChain_nil: Empty chain order equals 1.
2. sizeStabChain_cons_eq: Prepending a level multiplies order by basic orbit length: $\text{size}(L :: \text{rest}) = |\Delta_L| \cdot \text{size}(\text{rest})$.
3. transversalInverses_length_eq: FilterMap preservation under full coverage.
4. transversalRepresentatives_length_eq: Inverses and representatives have equal length $|\Delta_L|$.
5. transversalWords_length_cons: Product length recursion across stabilizer levels.
6. transversalWords_length_eq_sizeStabChain: Exact cardinality equivalence $|\text{transversalWords}(S)| = \text{sizeStabChain}(S) = \prod_{i=1}^k |\Delta_i|$.
7. The Crown Jewel Theorem (permGroup_order_eq_prod_basicOrbits):

   theorem permGroup_order_eq_prod_basicOrbits (G : PermGroup α) (hCov : ChainFullCoverage G.chain) :
       (transversalWords G.chain).length = G.size

Verification & Environment:

• Cleanly compiled with lake build RequestProject (8,034 jobs) on Dual Intel Xeon E5-2630 v4 (40 cores).
• #print axioms audit: Strictly standard propositional extensionality ([propext, Quot.sound]), 0 unproven axioms.
• Fully updated docs/RUNG_LEDGER.md (promoted GAP-0190 to Rung 3 Proved) and tasks/merged_ledger.json.