`ComparatorChallenges/SpinAngle.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 120 curated AI-written annotations and 1273 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 9 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. Those 9 annotations were revised on 2026-10-14 to bind all of them to exact page-one quotations from 6 pinned OpenAI manuscripts, the matching pinned formalization notes, and named historical primary sources; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. The 3 manuscript-grounded matrix-multiplication annotations were composed from pinned OpenAI manuscripts and named historical sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Six additional target-specific annotations for Catalan's constant, the irrationality exponent of pi, dyadic Erdos similarity, Unique Games, quintic Lienard systems, and Yau nodal growth were composed from pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for Seymour's second-neighborhood conjecture, Cannon's conjecture, Koebe circle-domain uniformization, and circle-domain rigidity were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical primary sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for simple Lebesgue spectrum on the three-torus, Rokhlin multiple mixing, the nine-dimensional Borsuk counterexample, and Tingley's sphere-isometry problem were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical primary sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for the Abhyankar-Sathaye counterexample, the circulant Hadamard conjecture, the Eilenberg-Ganea counterexample, and short Egyptian fractions were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and quotations from Sathaye, Turyn with Storer, Eilenberg with Ganea, and Erdos in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for the complete Crouzeix inequality, unrestricted Euclidean five-coloring, the general Mahler conjecture, and Thompson F nonamenability were composed on 2026-10-14 from exact Lean statements, 4 pinned OpenAI manuscripts, the matching formalization notes, and linked historical sources by Crouzeix, de Grey, Mahler, Cannon, Floyd, and Parry; no human review is claimed. Four additional target-specific annotations for algorithmic strong thin trees, Barnette's Hamiltonian-cycle conjecture, the explicit Artin CAT(0) counterexample, and generalized amplitude-damping capacity were composed on 2026-10-14 from exact Lean statements, 4 pinned OpenAI manuscripts, matching formalization notes, and linked historical sources by Anari with Goddyn, Arts with Hopman and Timmermans, Charney, and Khatri with Sharma and Wilde; no human review is claimed. Fourteen solution-level annotations for Seymour's second-neighborhood theorem were added on 2026-10-14 from the pinned 15-page manuscript, covering the exact-neighborhood model, minimal-counterexample reduction, subset deficit, transitive blowup, pruning, extremal contradiction, and proof-bearing final theorem. The subset and blowup annotations also bind exact quotations from Tyler Seacrest (2019) and Brantner, Brockman, Kay, and Snively (2009); no human review is claimed. Thirty-seven declaration-level annotations were added on 2026-10-14 for the rest of ComparatorChallenges/AlgorithmicThinTrees.lean, covering its multigraph semantics, stack-machine cost model, explicit and binary-multiplicity encodings, output certificate, and complete algorithmic proposition. They are bound to the pinned OpenAI manuscript and linked earlier thin-tree sources by Luis Goddyn, Nima Anari, and Shayan Oveis Gharan; the annotation explicitly preserves that the concluding comparator theorem still has body by sorry, and no human review is claimed. Thirty-one supporting declarations in ComparatorChallenges/UniqueGamesTheorem.lean were upgraded or added on 2026-10-14, completing curated coverage of all thirty-two declarations in that file. The annotations cover the finite game model, Boolean formula and parser, binary-vector translations, explicit output serialization, finite-alphabet machine contract, and gap theorem; they distinguish manuscript-backed mathematics from Lean-specific canonical parsing and unary game output encoding, bind exact OpenAI manuscript quotations, and credit Subhash Khot through his 2010 survey. The comparator theorem remains explicitly labeled as having body by sorry; no human review is claimed. The source-derived generator was hardened on 2026-10-14 so a formalization note covering multiple comparator results no longer copies its combined Scope prose onto each declaration; those targets now use declaration-specific source comments when available and otherwise remain explicitly bounded to the exact Lean statement. The remaining source-derived annotations were generated mechanically from pinned formalization notes and source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the source prose.

Credit: OpenAI's pinned repository says an unreleased internal model produced the manuscripts and supporting proof artifacts. The collection builds on the mathematics community's accumulated problems, results, language, and formal libraries; each manuscript's BibTeX and bibliography are the authority for individual scholarly credit.

Project sources: Pinned openai/math documentation, Pinned formalization catalogue

73 declarations, 1 contain sorry, 0 declared as axioms

def OAI.SpinAngle.Specht.cyclic line 16
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:16 (same declaration text).
def OAI.SpinAngle.TensorRep.tensor line 35
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:140 (same declaration text).
lemma OAI.SpinAngle.TensorRep.tensor_mul line 38
Distinct definitions of this name: OAI/RepresentationTheory/SpinAngle/Core.lean:153 (different declaration text). Qualify references as OAI.SpinAngle.TensorRep.tensor_mul@path.
lemma OAI.SpinAngle.TensorRep.tensor_one line 51
Distinct definitions of this name: OAI/RepresentationTheory/SpinAngle/Core.lean:166 (different declaration text). Qualify references as OAI.SpinAngle.TensorRep.tensor_one@path.
lemma OAI.SpinAngle.TensorRep.toEuclideanLin_mul line 67
Distinct definitions of this name: OAI/RepresentationTheory/SpinAngle/Core.lean:199 (different declaration text). Qualify references as OAI.SpinAngle.TensorRep.toEuclideanLin_mul@path.
lemma OAI.SpinAngle.TensorRep.toEuclideanLin_one line 79
Distinct definitions of this name: OAI/RepresentationTheory/SpinAngle/Core.lean:211 (different declaration text). Qualify references as OAI.SpinAngle.TensorRep.toEuclideanLin_one@path.
def OAI.SpinAngle.TensorRep.action line 89
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:222 (same declaration text).
def OAI.SpinAngle.TensorRep.rep line 94
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:229 (same declaration text).
lemma OAI.SpinAngle.TensorRep.tensor_reindex line 97
Distinct definitions of this name: OAI/RepresentationTheory/SpinAngle/Core.lean:254 (different declaration text). Qualify references as OAI.SpinAngle.TensorRep.tensor_reindex@path.
def OAI.SpinAngle.Specht.PermutationSpace.rep line 116
Distinct definitions of this name: OAI/RepresentationTheory/SpinAngle/Core.lean:282 (same statement text; different proof or body). Qualify references as OAI.SpinAngle.Specht.PermutationSpace.rep@path.
def OAI.SpinAngle.Specht.PermutationSpace.alternator line 130
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:314 (same declaration text).
lemma OAI.SpinAngle.Specht.PermutationSpace.alternator_apply line 134
Distinct definitions of this name: OAI/RepresentationTheory/SpinAngle/Core.lean:318 (same statement text; different proof or body). Qualify references as OAI.SpinAngle.Specht.PermutationSpace.alternator_apply@path.
lemma OAI.SpinAngle.Specht.PermutationSpace.rep_alternator line 138
Distinct definitions of this name: OAI/RepresentationTheory/SpinAngle/Core.lean:676 (different declaration text). Qualify references as OAI.SpinAngle.Specht.PermutationSpace.rep_alternator@path.
def OAI.SpinAngle.Specht.complexSign line 162
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:423 (same declaration text).
lemma OAI.SpinAngle.Specht.complexSign_inv line 167
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:431 (same declaration text).
abbrev OAI.SpinAngle.Young.Cells line 174
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:442 (same declaration text).
instance OAI.SpinAngle.PolynomialCarrier.coloringAction line 183
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:567 (same declaration text).
def OAI.SpinAngle.PolynomialCarrier.reindex line 188
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:580 (same declaration text).
lemma OAI.SpinAngle.PolynomialCarrier.action_site_commute line 194
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:586 (same declaration text).
def OAI.SpinAngle.PolynomialCarrier.columnGroup line 208
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:601 (same declaration text).
abbrev OAI.SpinAngle.PolynomialCarrier.TensorSpace line 217
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:610 (same declaration text).
def OAI.SpinAngle.PolynomialCarrier.alternating line 219
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:614 (same declaration text).
def OAI.SpinAngle.PolynomialCarrier.rowColor line 234
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:629 (same declaration text).
def OAI.SpinAngle.PolynomialCarrier.highest line 239
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:634 (same declaration text).
lemma OAI.SpinAngle.PolynomialCarrier.highest_mem line 245
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:702 (same declaration text).
def OAI.SpinAngle.PolynomialCarrier.ordinary line 255
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:891 (same declaration text).
abbrev OAI.SpinAngle.PolynomialCarrier.Carrier line 259
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:1162 (same declaration text).
instance OAI.SpinAngle.PolynomialCarrier.carrierInner line 261
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:1164 (same declaration text).
def OAI.SpinAngle.ExternalTensor.rep line 274
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:1257 (same declaration text).
abbrev OAI.SpinAngle.SignedTensor.Spin line 284
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:1590 (same declaration text).
abbrev OAI.SpinAngle.SignedTensor.Mat line 285
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:1591 (same declaration text).
abbrev OAI.SpinAngle.SignedTensor.Group line 286
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:1592 (same declaration text).
def OAI.SpinAngle.SignedTensor.block line 288
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:1594 (same declaration text).
lemma OAI.SpinAngle.SignedTensor.block_star line 301
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:1607 (same declaration text).
def OAI.SpinAngle.SignedTensor.blockGroup line 308
Distinct definitions of this name: OAI/RepresentationTheory/SpinAngle/Core.lean:1614 (same statement text; different proof or body). Qualify references as OAI.SpinAngle.SignedTensor.blockGroup@path.
abbrev OAI.SpinAngle.SignedTensor.Raw line 327
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:1633 (same declaration text).
def OAI.SpinAngle.SignedTensor.rep line 329
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:1636 (same declaration text).
def OAI.SpinAngle.EntropyMonomial.entropy line 337
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:2119 (same declaration text).
def OAI.SpinAngle.Isotypic.space line 349
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:2253 (same declaration text).
def OAI.SpinAngle.Isotypic.projection line 363
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:2267 (same declaration text).
abbrev OAI.SpinAngle.SignedCarrier.Carrier line 372
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:1797 (same declaration text).
instance OAI.SpinAngle.SignedCarrier.carrierNormed line 374
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:1799 (same declaration text).
instance OAI.SpinAngle.SignedCarrier.carrierInner line 378
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:1803 (same declaration text).
instance OAI.SpinAngle.SignedCarrier.carrierFinite line 382
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:1807 (same declaration text).
abbrev OAI.SpinAngle.SignedCarrier.rep line 385
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:1810 (same declaration text).
def OAI.SpinAngle.SignedCarrier.parts line 390
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:2487 (same declaration text).
def OAI.SpinAngle.SignedCarrier.entropy line 391
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:2488 (same declaration text).
def OAI.SpinAngle.SignedCarrier.dimension line 392
Distinct definitions of this name: OAI/RepresentationTheory/SpinAngle/Core.lean:2489 (same statement text; different proof or body). Qualify references as OAI.SpinAngle.SignedCarrier.dimension@path.
abbrev OAI.SpinAngle.SignedCarrier.typeProjection line 396
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:2567 (same declaration text).
def OAI.SpinAngle.SignedCarrier.matrixProjection line 399
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:3643 (same declaration text).
def OAI.SpinAngle.missingCellFactor line 406
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4065 (same declaration text).
def OAI.SpinAngle.missingCellProductFactor line 409
Distinct definitions of this name: OAI/RepresentationTheory/SpinAngle/Core.lean:4068 (same statement text; different proof or body). Qualify references as OAI.SpinAngle.missingCellProductFactor@path.
def OAI.SpinAngle.occupiedRow line 414
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4150 (same declaration text).
def OAI.SpinAngle.missingInRow line 417
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4153 (same declaration text).
abbrev OAI.SpinAngle.DependentTensor.Mat line 426
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4309 (same declaration text).
def OAI.SpinAngle.DependentTensor.tensor line 428
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4311 (same declaration text).
abbrev OAI.SpinAngle.BlockTensor.Fiber line 438
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4430 (same declaration text).
def OAI.SpinAngle.BlockTensor.splitEquiv line 440
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4432 (same declaration text).
def OAI.SpinAngle.BlockTensor.tensor line 450
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4443 (same declaration text).
abbrev OAI.SpinAngle.MatrixAnalysis.Mat line 458
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:3771 (same declaration text).
structure OAI.SpinAngle.TypeLabel line 466
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4631 (same declaration text).
def OAI.SpinAngle.TypeLabel.size line 474
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4639 (same declaration text).
def OAI.SpinAngle.TypeLabel.entropy line 475
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4640 (same declaration text).
def OAI.SpinAngle.TypeLabel.dimension line 476
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4641 (same declaration text).
def OAI.SpinAngle.TypeLabel.projection line 478
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4643 (same declaration text).
abbrev OAI.SpinAngle.TypeBlocks.Fiber line 490
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4723 (same declaration text).
def OAI.SpinAngle.TypeBlocks.projection line 492
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4725 (same declaration text).
def OAI.SpinAngle.TypeBlocks.entropy line 495
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4728 (same declaration text).
def OAI.SpinAngle.TypeBlocks.dimension line 496
Also declared: OAI/RepresentationTheory/SpinAngle/Core.lean:4729 (same declaration text).
def OAI.SpinAngle.TypeAngle.row Challenge statement: One-sided angle bound for signed spin types line 511
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.SpinAngle.TypeAngle as the released solution module checked against this declaration.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/RepresentationTheory/SpinAngle/TypeAngle.lean:35 (same declaration text).
```
def row (W : Finset (R × C)) (w : W) : R := w.val.1
```
def OAI.SpinAngle.TypeAngle.column Challenge statement: One-sided angle bound for signed spin types line 513
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.SpinAngle.TypeAngle as the released solution module checked against this declaration.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/RepresentationTheory/SpinAngle/TypeAngle.lean:36 (same declaration text).
```
def column (W : Finset (R × C)) (w : W) : C := w.val.2
```
def OAI.SpinAngle.TypeAngle.phi Challenge statement: One-sided angle bound for signed spin types line 515
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.SpinAngle.TypeAngle as the released solution module checked against this declaration.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/RepresentationTheory/SpinAngle/TypeAngle.lean:38 (same declaration text).
```
def phi (W : Finset (R × C)) : ℝ :=
…
```
theorem OAI.SpinAngle.TypeAngle.one_sided_type_angle Challenge statement: One-sided angle bound for signed spin types sorry line 518
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.SpinAngle.TypeAngle as the released solution module checked against this declaration.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Distinct definitions of this name: OAI/RepresentationTheory/SpinAngle/TypeAngle.lean:189 (different declaration text). Qualify references as OAI.SpinAngle.TypeAngle.one_sided_type_angle@path.
```
theorem one_sided_type_angle (W : Finset (R × C))
    (D : TypeLabel q) (H : C → TypeLabel q) (K : R → TypeLabel q)
    (hD : D.size = W.card)
    (hH : ∀ j, (H j).size = Fintype.card (TypeBlocks.Fiber (column W) j))
    (hK : ∀ i, (K i).size = Fintype.card (TypeBlocks.Fiber (row W) i)) :
    (‖TypeBlocks.projection (column W) H * TypeBlocks.projection (row W) K * D.projection W‖ ^ 2 ≤
      min 1 (Real.exp (TypeBlocks.entropy H + TypeBlocks.entropy K - D.entropy) *
        (TypeBlocks.dimension H : ℝ) * (TypeBlocks.dimension K : ℝ) * phi W)) ∧
    (min 1 (Real.exp (TypeBlocks.entropy H + TypeBlocks.entropy K - D.entropy) *
        (TypeBlocks.dimension H : ℝ) * (TypeBlocks.dimension K : ℝ) * phi W) ≤
      min 1 (Real.exp (TypeBlocks.entropy H + TypeBlocks.entropy K - D.entropy +
        (Fintype.card R * Fintype.card C - W.card : ℕ)) *
…
```
Mentions: OAI.SpinAngle.TypeLabel, OAI.SpinAngle.TypeBlocks.Fiber, OAI.SpinAngle.TypeAngle.column, OAI.SpinAngle.TypeAngle.row, OAI.SpinAngle.TypeBlocks.projection, OAI.SpinAngle.TypeBlocks.entropy, OAI.SpinAngle.TypeBlocks.dimension, OAI.SpinAngle.TypeAngle.phi