ComparatorChallenges/OccupiedOverlap.lean

GitHub source file

43 declarations, 2 contain sorry, 0 declared as axioms

1. abbrev OAI.CubeShuffle.Specht.Cell line 9

   Also declared: ComparatorChallenges/WeightedSweepMoments.lean:9 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:10 (same declaration text).

2. def OAI.CubeShuffle.Specht.row line 10

   Also declared: ComparatorChallenges/WeightedSweepMoments.lean:10 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:15 (same declaration text).

3. def OAI.CubeShuffle.Specht.col line 11

   Also declared: ComparatorChallenges/WeightedSweepMoments.lean:11 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:16 (same declaration text).

4. lemma OAI.CubeShuffle.Specht.row_lt_colLen line 13

   Also declared: ComparatorChallenges/WeightedSweepMoments.lean:13 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:18 (same declaration text).

5. def OAI.CubeShuffle.Specht.rowIndex line 15

   Also declared: ComparatorChallenges/WeightedSweepMoments.lean:15 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:122 (same declaration text).

6. abbrev OAI.CubeShuffle.Specht.Tabloid line 18

   Also declared: ComparatorChallenges/WeightedSweepMoments.lean:18 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:125 (same declaration text).

7. instance OAI.CubeShuffle.Specht.(instance at line 21) line 21
8. def OAI.CubeShuffle.Specht.baseTabloid line 23

   Also declared: ComparatorChallenges/WeightedSweepMoments.lean:23 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:130 (same declaration text).

9. def OAI.CubeShuffle.Specht.tabloidAct line 25

   Also declared: ComparatorChallenges/WeightedSweepMoments.lean:25 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:132 (same declaration text).

10. lemma OAI.CubeShuffle.Specht.tabloidAct_apply line 40

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:40 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:147 (same declaration text).

11. lemma OAI.CubeShuffle.Specht.tabloidAct_one line 43

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:43 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:150 (same declaration text).

12. lemma OAI.CubeShuffle.Specht.tabloidAct_mul line 47

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:47 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:154 (same declaration text).

13. lemma OAI.CubeShuffle.Specht.tabloidAct_inv line 52

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:52 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:159 (same declaration text).

14. def OAI.CubeShuffle.Specht.tabloidRep line 57

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:57 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:164 (same declaration text).

15. lemma OAI.CubeShuffle.Specht.tabloidRep_apply line 69

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:69 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:176 (same declaration text).

16. def OAI.CubeShuffle.Specht.delta line 72

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:72 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:179 (same declaration text).

17. def OAI.CubeShuffle.Specht.colGroup line 75

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:75 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:190 (same declaration text).

18. def OAI.CubeShuffle.Specht.permSign line 81

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:81 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:229 (same declaration text).

19. def OAI.CubeShuffle.Specht.alternator line 86

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:86 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:251 (same declaration text).

20. def OAI.CubeShuffle.Specht.polytabloid line 93

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:93 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:336 (same declaration text).

21. def OAI.CubeShuffle.Specht.space line 96

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:96 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:472 (same declaration text).

22. lemma OAI.CubeShuffle.Specht.orbit_mem_space line 99

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:99 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:475 (same declaration text).

23. lemma OAI.CubeShuffle.Specht.action_mem_space line 102

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:102 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:481 (same declaration text).

24. def OAI.CubeShuffle.Specht.subrepresentation line 114

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:114 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:543 (same declaration text).

25. def OAI.CubeShuffle.Specht.representation line 117

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:117 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean:546 (same declaration text).

26. abbrev OAI.CubeShuffle.PermutationHilbert.H line 130

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:130 (same declaration text), OAI/RepresentationTheory/FiniteUnitary/Uncertainty.lean:10 (same declaration text).

27. def OAI.CubeShuffle.Specht.hilbertEquiv line 138

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:138 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Dimensions.lean:9 (same declaration text).

28. def OAI.CubeShuffle.Specht.hilbertSpace Challenge statement: Row–column overlap on occupied boards line 142

    L4DEL explanation

    This declaration is an exact comparator-selected statement. Read the Lean statement below for its mathematical content.

    1. The linked formalization note covers 13 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    2. The repository's comparator configuration selects OAI.RepresentationTheory.RowColumn.Occupied as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:142 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/Dimensions.lean:13 (same declaration text).

    noncomputable def hilbertSpace (μ : YoungDiagram) :
        Submodule ℂ (PermutationHilbert.H (Tabloid μ)) := (space μ).map (hilbertEquiv μ).toLinearMap

    Mentions: OAI.CubeShuffle.PermutationHilbert.H, OAI.CubeShuffle.Specht.Tabloid, OAI.CubeShuffle.Specht.space, OAI.CubeShuffle.Specht.hilbertEquiv

29. def OAI.CubeShuffle.Specht.spaceHilbertEquiv line 145

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:145 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/UnitaryModel.lean:10 (same declaration text).

30. def OAI.CubeShuffle.Specht.unitaryRepresentation Challenge statement: Row–column overlap on occupied boards line 148

    L4DEL explanation

    This declaration is an exact comparator-selected statement. Read the Lean statement below for its mathematical content.

    1. The linked formalization note covers 13 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    2. The repository's comparator configuration selects OAI.RepresentationTheory.RowColumn.Occupied as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: ComparatorChallenges/WeightedSweepMoments.lean:148 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/UnitaryModel.lean:13 (same statement text; different proof or body). Qualify references as OAI.CubeShuffle.Specht.unitaryRepresentation@path.

    noncomputable def unitaryRepresentation (μ : YoungDiagram) :
        Representation ℂ (Equiv.Perm (Cell μ)) (hilbertSpace μ) :=
    …

    Mentions: OAI.CubeShuffle.Specht.Cell, OAI.CubeShuffle.Specht.hilbertSpace

31. def OAI.CubeShuffle.Specht.relabelledUnitary Challenge statement: Row–column overlap on occupied boards line 154

    L4DEL explanation

    This declaration is an exact comparator-selected statement. Read the Lean statement below for its mathematical content.

    1. The linked formalization note covers 13 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    2. The repository's comparator configuration selects OAI.RepresentationTheory.RowColumn.Occupied as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: ComparatorChallenges/WeightedSweepMoments.lean:154 (same declaration text), OAI/RepresentationTheory/YoungSymmetry/UnitaryModel.lean:87 (same statement text; different proof or body). Qualify references as OAI.CubeShuffle.Specht.relabelledUnitary@path.

    noncomputable def relabelledUnitary (μ : YoungDiagram) (e : α ≃ Cell μ) :
        Representation ℂ (Equiv.Perm α) (hilbertSpace μ) :=
    …

    Mentions: OAI.CubeShuffle.Specht.Cell, OAI.CubeShuffle.Specht.hilbertSpace

32. def OAI.CubeShuffle.UnitaryFinite.IsUnitary Challenge statement: Row–column overlap on occupied boards line 169

    L4DEL explanation

    This declaration is an exact comparator-selected statement. Read the Lean statement below for its mathematical content.

    1. The linked formalization note covers 13 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    2. The repository's comparator configuration selects OAI.RepresentationTheory.RowColumn.Occupied as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/RepresentationTheory/FiniteUnitary/Coefficients.lean:12 (same statement text; different proof or body). Qualify references as OAI.CubeShuffle.UnitaryFinite.IsUnitary@path.

    def IsUnitary (ρ : Representation ℂ G V) : Prop :=
    …

33. def OAI.RowColumn.lineGroup Permutations preserving each fibre of a given line map line 182

    Source documentation

    Permutations preserving each fibre of a given line map.

    L4DEL explanation

    Permutations preserving each fibre of a given line map.

    1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Also declared: OAI/RepresentationTheory/RowColumn/Basic.lean:13 (same declaration text).

    def lineGroup {α β : Type*} (f : α → β) : Subgroup (Equiv.Perm α) where
    …

34. abbrev OAI.RowColumn.Board line 192

    Also declared: OAI/RepresentationTheory/RowColumn/Basic.lean:23 (same declaration text).

35. abbrev OAI.RowColumn.rowGroup line 193

    Also declared: OAI/RepresentationTheory/RowColumn/Basic.lean:24 (same declaration text).

36. abbrev OAI.RowColumn.columnGroup line 195

    Also declared: OAI/RepresentationTheory/RowColumn/Basic.lean:26 (same declaration text).

37. def OAI.RowColumn.InHook Zero-based form of the manuscript's (h,h)-hook line 199

    Source documentation

    Zero-based form of the manuscript's (h,h)-hook.

    L4DEL explanation

    Zero-based form of the manuscript's (h,h)-hook.

    1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Also declared: OAI/RepresentationTheory/RowColumn/Basic.lean:30 (same declaration text).

    def InHook (a : YoungDiagram) (h : ℕ) : Prop :=
    …

38. def OAI.RowColumn.Intertwines An actual equivariant inclusion, not an unspecified overlap matrix line 208

    Source documentation

    An actual equivariant inclusion, not an unspecified overlap matrix.

    L4DEL explanation

    An actual equivariant inclusion, not an unspecified overlap matrix.

    1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Also declared: OAI/RepresentationTheory/RowColumn/Basic.lean:39 (same declaration text).

    def Intertwines (ρ : Representation ℂ G V) (τ : Representation ℂ G W)
        (I : V →ₗ[ℂ] W) : Prop :=
    …

39. def OAI.RowColumn.CompleteCopies All orthogonal multiplicity copies of one irreducible type line 215

    Source documentation

    All orthogonal multiplicity copies of one irreducible type. The completeness condition quantifies over genuine intertwiners, i.e. it is exactly the isotypic space condition.

    L4DEL explanation

    All orthogonal multiplicity copies of one irreducible type. The completeness condition quantifies over genuine intertwiners, i.e. it is exactly the isotypic space condition.

    1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Also declared: OAI/RepresentationTheory/RowColumn/Basic.lean:46 (same declaration text).

    def CompleteCopies (ρ : Representation ℂ G V) (τ : Representation ℂ G W)
        {u : ℕ} (I : Fin u → V →ₗᵢ[ℂ] W) : Prop :=
    …

40. def OAI.RowColumn.allCopyOverlap The all-copy operator-overlap sum, with each squared operator norm line 225

    Source documentation

    The all-copy operator-overlap sum, with each squared operator norm.

    L4DEL explanation

    The all-copy operator-overlap sum, with each squared operator norm.

    1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Also declared: OAI/RepresentationTheory/RowColumn/Basic.lean:56 (same declaration text).

    def allCopyOverlap {V W X : Type*}
        [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]
        [NormedAddCommGroup W] [InnerProductSpace ℂ W] [FiniteDimensional ℂ W]
        [NormedAddCommGroup X] [InnerProductSpace ℂ X] [FiniteDimensional ℂ X]
        {u v : ℕ} (I : Fin u → V →ₗᵢ[ℂ] X) (J : Fin v → W →ₗᵢ[ℂ] X) : ℝ :=
    …

41. abbrev OAI.RowColumn.OccupiedOverlapEndpoint Challenge statement: Row–column overlap on occupied boards line 237

    Source documentation

    Exact occupied-board main. Carriers are in orthonormal coordinates; arbitrary unitary irreducibles of the two actual line groups are quantified over (equivalently, the tuples of line partitions in the manuscript). Labelling e chooses the action of the Specht module on the occupied cells and forces |a| = |Ω|.

    L4DEL explanation

    Exact occupied-board main. Carriers are in orthonormal coordinates; arbitrary unitary irreducibles of the two actual line groups are quantified over (equivalently, the tuples of line partitions in the manuscript). Labelling e chooses the action of the Specht module on the occupied cells and forces |a| = |Ω|.

    1. This explanation is a condensed rendering of this declaration's own doc comment at the pinned source commit.
    2. The linked formalization note covers 13 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    3. The repository's comparator configuration selects OAI.RepresentationTheory.RowColumn.Occupied as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Also declared: OAI/RepresentationTheory/RowColumn/Basic.lean:68 (same declaration text).

    abbrev OccupiedOverlapEndpoint : Prop :=
    …

42. theorem OAI.RowColumn.occupied_overlap_endpoint Challenge statement: Row–column overlap on occupied boards sorry line 260

    L4DEL explanation

    This declaration is an exact comparator-selected statement. Read the Lean statement below for its mathematical content.

    1. The linked formalization note covers 13 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    2. The repository's comparator configuration selects OAI.RepresentationTheory.RowColumn.Occupied as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/RepresentationTheory/RowColumn/Occupied.lean:203 (different declaration text). Qualify references as OAI.RowColumn.occupied_overlap_endpoint@path.

    Checked implications (found by the pipeline and checked by Lean's kernel when it ran; a recorded result, not checked again in this build: what these are)

    2 more checked entries are routine (the same statement, a restatement, a generated lemma, one challenge file, a field of a structure, a route the released proof already takes, a duplicate): in the catalogue.

    theorem RowColumn.occupied_overlap_endpoint : RowColumn.OccupiedOverlapEndpoint := by
    …

    Mentions: OAI.RowColumn.OccupiedOverlapEndpoint

43. theorem OAI.RowColumn.occupied_overlap Challenge statement: Row–column overlap on occupied boards sorry line 263

    L4DEL explanation

    This declaration is an exact comparator-selected statement. Read the Lean statement below for its mathematical content.

    1. The linked formalization note covers 13 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    2. The repository's comparator configuration selects OAI.RepresentationTheory.RowColumn.Occupied as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/RepresentationTheory/RowColumn/Occupied.lean:274 (same statement text; different proof or body). Qualify references as OAI.RowColumn.occupied_overlap@path.

    Checked implications (found by the pipeline and checked by Lean's kernel when it ran; a recorded result, not checked again in this build: what these are)

    2 more checked entries are routine (the same statement, a restatement, a generated lemma, one challenge file, a field of a structure, a route the released proof already takes, a duplicate): in the catalogue.

    theorem RowColumn.occupied_overlap : RowColumn.OccupiedOverlapEndpoint := by
    …

    Mentions: OAI.RowColumn.OccupiedOverlapEndpoint