`ComparatorChallenges/ThorpRouting.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

409 declarations, 1 contain sorry, 0 declared as axioms

abbrev OAI.ThorpNine.Adaptive.Thorp.Card line 11
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:11 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.switchFun line 13
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:13 (same declaration text).
theorem OAI.ThorpNine.Adaptive.Thorp.switchFun_involutive line 16
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:16 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.pairSwitch line 25
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:25 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Butterfly line 31
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:31 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.childLift line 35
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:35 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.butterflyPerm line 41
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:41 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.SwitchIndex line 45
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:45 (same declaration text).
instance OAI.ThorpNine.Adaptive.Thorp.(instance at line 49) line 49
instance OAI.ThorpNine.Adaptive.Thorp.(instance at line 54) line 54
def OAI.ThorpNine.Adaptive.Thorp.decodeButterfly line 59
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:59 (same declaration text).
abbrev OAI.ThorpNine.Adaptive.Thorp.Specht.Cell line 69
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:69 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.row line 71
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:71 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.col line 73
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:73 (same declaration text).
lemma OAI.ThorpNine.Adaptive.Thorp.Specht.row_lt_colLen line 75
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:75 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.rowIndex line 78
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:78 (same declaration text).
abbrev OAI.ThorpNine.Adaptive.Thorp.Specht.Tabloid line 81
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:81 (same declaration text).
instance OAI.ThorpNine.Adaptive.Thorp.Specht.(instance at line 84) line 84
def OAI.ThorpNine.Adaptive.Thorp.Specht.baseTabloid line 86
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:86 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.tabloidAct line 88
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:88 (same declaration text).
lemma OAI.ThorpNine.Adaptive.Thorp.Specht.tabloidAct_apply line 103
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:103 (same declaration text).
lemma OAI.ThorpNine.Adaptive.Thorp.Specht.tabloidAct_one line 106
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:106 (same declaration text).
lemma OAI.ThorpNine.Adaptive.Thorp.Specht.tabloidAct_mul line 110
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:110 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.tabloidRep line 115
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:115 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.delta line 127
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:127 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.colGroup line 130
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:130 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.permSign line 136
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:136 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.alternator line 143
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:143 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.polytabloid line 150
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:150 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.space line 153
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:153 (same declaration text).
lemma OAI.ThorpNine.Adaptive.Thorp.Specht.orbit_mem_space line 156
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:156 (same declaration text).
lemma OAI.ThorpNine.Adaptive.Thorp.Specht.action_mem_space line 159
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:159 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.subrepresentation line 171
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:171 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.representation line 174
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:174 (same declaration text).
abbrev OAI.ThorpNine.Adaptive.Thorp.PermutationHilbert.H line 185
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:185 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.hilbertEquiv line 192
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:192 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.hilbertSpace line 196
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:196 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.continuousRepresentation line 208
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:208 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.sampleOperator line 219
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:219 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.spaceHilbertEquiv line 227
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:227 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.unitaryRepresentation line 230
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:230 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Specht.relabelledUnitary line 236
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:236 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.SparseContact.sweepOperator line 245
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:245 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.Casimir.levelScale line 258
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:258 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.positiveSquare line 267
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:267 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.F line 271
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:271 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.fourthTrace line 275
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:275 (same declaration text).
def OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.MainStatement line 279
Also declared: OAI/Probability/ThorpRouting/Adaptive/Model.lean:279 (same declaration text).
abbrev OAI.ThorpNine.Casimir.Thorp.Card line 305
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:11 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Coins line 307
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:13 (same declaration text).
instance OAI.ThorpNine.Casimir.Thorp.(instance at line 311) line 311
def OAI.ThorpNine.Casimir.Thorp.switchFun line 314
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:20 (same declaration text).
theorem OAI.ThorpNine.Casimir.Thorp.switchFun_involutive line 317
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:23 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.pairSwitch line 326
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:32 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.rotate line 332
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:38 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.step line 338
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:44 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.run line 342
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:48 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.law line 346
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:52 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Butterfly line 350
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:56 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.childLift line 354
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:60 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.butterflyPerm line 360
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:66 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.finiteMean line 364
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:70 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.SwitchIndex line 367
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:73 (same declaration text).
instance OAI.ThorpNine.Casimir.Thorp.(instance at line 371) line 371
instance OAI.ThorpNine.Casimir.Thorp.(instance at line 376) line 376
def OAI.ThorpNine.Casimir.Thorp.decodeButterfly line 381
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:87 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.PairRouting.tupleProbability line 393
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:99 (same declaration text).
abbrev OAI.ThorpNine.Casimir.Thorp.BenesCoins line 404
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:110 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.palindromePerm line 406
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:112 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.palindromeRowMoment line 409
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:115 (same declaration text).
abbrev OAI.ThorpNine.Casimir.Thorp.Specht.Cell line 419
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:125 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.row line 421
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:127 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.col line 423
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:129 (same declaration text).
lemma OAI.ThorpNine.Casimir.Thorp.Specht.row_lt_colLen line 425
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:131 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.rowIndex line 428
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:134 (same declaration text).
abbrev OAI.ThorpNine.Casimir.Thorp.Specht.Tabloid line 431
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:137 (same declaration text).
instance OAI.ThorpNine.Casimir.Thorp.Specht.(instance at line 434) line 434
def OAI.ThorpNine.Casimir.Thorp.Specht.baseTabloid line 436
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:142 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.tabloidAct line 438
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:144 (same declaration text).
lemma OAI.ThorpNine.Casimir.Thorp.Specht.tabloidAct_apply line 453
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:159 (same declaration text).
lemma OAI.ThorpNine.Casimir.Thorp.Specht.tabloidAct_one line 456
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:162 (same declaration text).
lemma OAI.ThorpNine.Casimir.Thorp.Specht.tabloidAct_mul line 460
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:166 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.tabloidRep line 465
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:171 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.delta line 477
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:183 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.colGroup line 480
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:186 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.permSign line 486
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:192 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.alternator line 493
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:199 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.polytabloid line 500
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:206 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.space line 503
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:209 (same declaration text).
lemma OAI.ThorpNine.Casimir.Thorp.Specht.orbit_mem_space line 506
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:212 (same declaration text).
lemma OAI.ThorpNine.Casimir.Thorp.Specht.action_mem_space line 509
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:215 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.subrepresentation line 521
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:227 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.representation line 524
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:230 (same declaration text).
abbrev OAI.ThorpNine.Casimir.Thorp.PermutationHilbert.H line 535
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:241 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.hilbertEquiv line 542
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:248 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.hilbertSpace line 546
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:252 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.continuousRepresentation line 558
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:264 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.sampleOperator line 569
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:275 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.spaceHilbertEquiv line 577
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:283 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.unitaryRepresentation line 580
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:286 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.Specht.relabelledUnitary line 586
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:292 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.CasimirBounds.levelScale line 596
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:302 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.CasimirBounds.K line 599
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:305 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.CasimirBounds.traceMoment line 604
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:310 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.CasimirBounds.fromDistance line 608
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:314 (same declaration text).
def OAI.ThorpNine.Casimir.Thorp.CasimirBounds.MainStatement line 612
Also declared: OAI/Probability/ThorpRouting/Casimir/Model.lean:318 (same declaration text).
abbrev OAI.ThorpNine.Dense.Thorp.Card line 642
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:11 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.switchFun line 644
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:13 (same declaration text).
theorem OAI.ThorpNine.Dense.Thorp.switchFun_involutive line 647
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:16 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.pairSwitch line 656
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:25 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.Butterfly line 662
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:31 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.childLift line 666
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:35 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.butterflyPerm line 672
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:41 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.finiteMean line 676
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:45 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.SwitchIndex line 679
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:48 (same declaration text).
instance OAI.ThorpNine.Dense.Thorp.(instance at line 683) line 683
instance OAI.ThorpNine.Dense.Thorp.(instance at line 688) line 688
def OAI.ThorpNine.Dense.Thorp.decodeButterfly line 693
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:62 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.orbitSet line 700
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:69 (same declaration text).
abbrev OAI.ThorpNine.Dense.Thorp.RoutingNetwork.SelectedCycle line 711
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:80 (same declaration text).
instance OAI.ThorpNine.Dense.Thorp.RoutingNetwork.(instance at line 714) line 714
def OAI.ThorpNine.Dense.Thorp.pairLayer line 726
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:95 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.coinStepEquiv line 740
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:109 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.headTailEquiv line 754
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:123 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.CycleColoring.alternatingPerm line 764
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:133 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.PairRouting.required line 777
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:146 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.PairRouting.Compatible line 779
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:148 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.PairRouting.colors line 782
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:151 (same declaration text).
lemma OAI.ThorpNine.Dense.Thorp.PairRouting.required_colors line 786
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:155 (same declaration text).
lemma OAI.ThorpNine.Dense.Thorp.PairRouting.colors_compatible line 792
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:161 (same declaration text).
lemma OAI.ThorpNine.Dense.Thorp.PairRouting.Compatible.tail_injective line 797
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:166 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.PairRouting.childEmbedding line 808
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:177 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.PairRouting.labelSet line 811
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:180 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.PairRouting.alternatingProjection line 813
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:182 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.PairRouting.alternatingCycles line 815
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:184 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.PairRouting.switchedEmbedding line 819
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:188 (same declaration text).
abbrev OAI.ThorpNine.Dense.Thorp.BenesCoins line 828
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:197 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.palindromePerm line 830
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:199 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.sandwichShuffle line 833
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:202 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.benesStepEquiv line 840
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:209 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.palindromeCost line 844
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:213 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.DenseTruncation.AdmissibleCycleLaw line 862
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:231 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.DenseTruncation.h line 866
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:235 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.DenseTruncation.AdmissibleAllocation line 870
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:239 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.DenseTruncation.H line 874
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:243 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.DenseTruncation.entropyCorrection line 878
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:247 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.DenseTruncation.densityExponent line 881
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:250 (same declaration text).
def OAI.ThorpNine.Dense.Thorp.DenseTruncation.MainStatement line 886
Also declared: OAI/Probability/ThorpRouting/Dense/Model.lean:255 (same declaration text).
abbrev OAI.ThorpNine.Contact.Thorp.Card line 911
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:11 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.switchFun line 913
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:13 (same declaration text).
theorem OAI.ThorpNine.Contact.Thorp.switchFun_involutive line 916
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:16 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.pairSwitch line 925
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:25 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Butterfly line 931
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:31 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.childLift line 935
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:35 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.butterflyPerm line 941
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:41 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.SwitchIndex line 945
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:45 (same declaration text).
instance OAI.ThorpNine.Contact.Thorp.(instance at line 949) line 949
instance OAI.ThorpNine.Contact.Thorp.(instance at line 954) line 954
def OAI.ThorpNine.Contact.Thorp.decodeButterfly line 959
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:59 (same declaration text).
abbrev OAI.ThorpNine.Contact.Thorp.Specht.Cell line 969
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:69 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.row line 971
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:71 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.col line 973
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:73 (same declaration text).
lemma OAI.ThorpNine.Contact.Thorp.Specht.row_lt_colLen line 975
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:75 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.rowIndex line 978
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:78 (same declaration text).
abbrev OAI.ThorpNine.Contact.Thorp.Specht.Tabloid line 981
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:81 (same declaration text).
instance OAI.ThorpNine.Contact.Thorp.Specht.(instance at line 984) line 984
def OAI.ThorpNine.Contact.Thorp.Specht.baseTabloid line 986
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:86 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.tabloidAct line 988
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:88 (same declaration text).
lemma OAI.ThorpNine.Contact.Thorp.Specht.tabloidAct_apply line 1003
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:103 (same declaration text).
lemma OAI.ThorpNine.Contact.Thorp.Specht.tabloidAct_one line 1006
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:106 (same declaration text).
lemma OAI.ThorpNine.Contact.Thorp.Specht.tabloidAct_mul line 1010
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:110 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.tabloidRep line 1015
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:115 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.delta line 1027
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:127 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.colGroup line 1030
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:130 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.permSign line 1036
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:136 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.alternator line 1043
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:143 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.polytabloid line 1050
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:150 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.space line 1053
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:153 (same declaration text).
lemma OAI.ThorpNine.Contact.Thorp.Specht.orbit_mem_space line 1056
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:156 (same declaration text).
lemma OAI.ThorpNine.Contact.Thorp.Specht.action_mem_space line 1059
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:159 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.subrepresentation line 1071
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:171 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.representation line 1074
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:174 (same declaration text).
abbrev OAI.ThorpNine.Contact.Thorp.PermutationHilbert.H line 1085
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:185 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.hilbertEquiv line 1092
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:192 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.hilbertSpace line 1096
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:196 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.UnitaryFinite.continuousRepresentation line 1108
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:208 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.UnitaryFinite.sampleOperator line 1119
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:219 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.spaceHilbertEquiv line 1127
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:227 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.unitaryRepresentation line 1130
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:230 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.Specht.relabelledUnitary line 1136
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:236 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.SparseContact.sweepOperator line 1145
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:245 (same declaration text).
def OAI.ThorpNine.Contact.Thorp.SparseContact.MainStatement line 1152
Also declared: OAI/Probability/ThorpRouting/Contact/Model.lean:252 (same declaration text).
abbrev OAI.ThorpNine.Harmonic.Thorp.Card line 1180
Also declared: ComparatorChallenges/CoordinateTrace.lean:11 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:89 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:11 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.switchFun line 1182
Also declared: ComparatorChallenges/CoordinateTrace.lean:13 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:91 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:13 (same declaration text).
theorem OAI.ThorpNine.Harmonic.Thorp.switchFun_involutive line 1185
Also declared: ComparatorChallenges/CoordinateTrace.lean:16 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:94 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:16 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.pairSwitch line 1194
Also declared: ComparatorChallenges/CoordinateTrace.lean:25 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:103 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:25 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Butterfly line 1200
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:31 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.childLift line 1204
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:35 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.butterflyPerm line 1210
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:41 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.finiteMean line 1214
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:45 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.SwitchIndex line 1217
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:48 (same declaration text).
instance OAI.ThorpNine.Harmonic.Thorp.(instance at line 1221) line 1221
instance OAI.ThorpNine.Harmonic.Thorp.(instance at line 1226) line 1226
def OAI.ThorpNine.Harmonic.Thorp.decodeButterfly line 1231
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:62 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.PairRouting.tupleProbability line 1243
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:74 (same declaration text).
abbrev OAI.ThorpNine.Harmonic.Thorp.BenesCoins line 1254
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:85 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.palindromePerm line 1256
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:87 (same declaration text).
abbrev OAI.ThorpNine.Harmonic.Thorp.Specht.Cell line 1264
Also declared: ComparatorChallenges/CoordinateTrace.lean:67 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:155 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:95 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.row line 1266
Also declared: ComparatorChallenges/CoordinateTrace.lean:69 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:157 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:97 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.col line 1268
Also declared: ComparatorChallenges/CoordinateTrace.lean:71 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:159 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:99 (same declaration text).
lemma OAI.ThorpNine.Harmonic.Thorp.Specht.row_lt_colLen line 1270
Also declared: ComparatorChallenges/CoordinateTrace.lean:73 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:161 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:101 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.rowIndex line 1273
Also declared: ComparatorChallenges/CoordinateTrace.lean:76 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:164 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:104 (same declaration text).
abbrev OAI.ThorpNine.Harmonic.Thorp.Specht.Tabloid line 1276
Also declared: ComparatorChallenges/CoordinateTrace.lean:79 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:167 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:107 (same declaration text).
instance OAI.ThorpNine.Harmonic.Thorp.Specht.(instance at line 1279) line 1279
def OAI.ThorpNine.Harmonic.Thorp.Specht.baseTabloid line 1281
Also declared: ComparatorChallenges/CoordinateTrace.lean:84 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:172 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:112 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct line 1283
Also declared: ComparatorChallenges/CoordinateTrace.lean:86 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:174 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:114 (same declaration text).
lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct_apply line 1298
Also declared: ComparatorChallenges/CoordinateTrace.lean:101 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:189 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:129 (same declaration text).
lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct_one line 1301
Also declared: ComparatorChallenges/CoordinateTrace.lean:104 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:192 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:132 (same declaration text).
lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct_mul line 1305
Also declared: ComparatorChallenges/CoordinateTrace.lean:108 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:196 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:136 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidRep line 1310
Also declared: ComparatorChallenges/CoordinateTrace.lean:113 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:201 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:141 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.delta line 1322
Also declared: ComparatorChallenges/CoordinateTrace.lean:125 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:213 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:153 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.colGroup line 1325
Also declared: ComparatorChallenges/CoordinateTrace.lean:128 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:216 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:156 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.permSign line 1331
Also declared: ComparatorChallenges/CoordinateTrace.lean:134 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:222 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:162 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.alternator line 1338
Also declared: ComparatorChallenges/CoordinateTrace.lean:143 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:228 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:169 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.polytabloid line 1345
Also declared: ComparatorChallenges/CoordinateTrace.lean:153 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:235 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:176 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.space line 1348
Also declared: ComparatorChallenges/CoordinateTrace.lean:156 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:238 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:179 (same declaration text).
lemma OAI.ThorpNine.Harmonic.Thorp.Specht.orbit_mem_space line 1351
Also declared: ComparatorChallenges/CoordinateTrace.lean:159 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:241 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:182 (same declaration text).
lemma OAI.ThorpNine.Harmonic.Thorp.Specht.action_mem_space line 1354
Also declared: ComparatorChallenges/CoordinateTrace.lean:162 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:244 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:185 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.subrepresentation line 1366
Also declared: ComparatorChallenges/CoordinateTrace.lean:174 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:256 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:197 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.representation line 1369
Also declared: ComparatorChallenges/CoordinateTrace.lean:177 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:259 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:200 (same declaration text).
abbrev OAI.ThorpNine.Harmonic.Thorp.PermutationHilbert.H line 1380
Also declared: ComparatorChallenges/CoordinateTrace.lean:188 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:270 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:211 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.hilbertEquiv line 1387
Also declared: ComparatorChallenges/CoordinateTrace.lean:195 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:277 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:218 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.hilbertSpace line 1391
Also declared: ComparatorChallenges/CoordinateTrace.lean:199 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:281 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:222 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.continuousRepresentation line 1403
Also declared: ComparatorChallenges/CoordinateTrace.lean:209 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:293 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:234 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator line 1414
Also declared: ComparatorChallenges/CoordinateTrace.lean:222 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:304 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:245 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.spaceHilbertEquiv line 1422
Also declared: ComparatorChallenges/CoordinateTrace.lean:230 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:312 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:253 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Specht.unitaryRepresentation line 1425
Distinct definitions of this name: ComparatorChallenges/CoordinateTrace.lean:233 (same statement text; different proof or body), ComparatorChallenges/ThorpRemaining.lean:315 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:256 (same declaration text). Qualify references as OAI.ThorpNine.Harmonic.Thorp.Specht.unitaryRepresentation@path.
def OAI.ThorpNine.Harmonic.Thorp.Specht.relabelledUnitary line 1431
Also declared: ComparatorChallenges/CoordinateTrace.lean:243 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:321 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:262 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.SparseContact.sweepOperator line 1440
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:271 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.coordinateRelabel line 1451
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:282 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.sweep line 1457
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:288 (same declaration text).
abbrev OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.Tuples line 1462
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:293 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.sweepKernel line 1464
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:295 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.reflectedKernel line 1468
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:299 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.StrongTail.tailDiagram line 1479
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:310 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Casimir.levelScale line 1488
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:319 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.Casimir.K line 1491
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:322 (same declaration text).
abbrev OAI.ThorpNine.Harmonic.Thorp.HarmonicBounds.tail line 1502
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:333 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.HarmonicBounds.W line 1504
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:335 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.HarmonicBounds.tupleTrace line 1506
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:337 (same declaration text).
def OAI.ThorpNine.Harmonic.Thorp.HarmonicBounds.MainStatement line 1509
Also declared: OAI/Probability/ThorpRouting/Harmonic/Model.lean:340 (same declaration text).
abbrev OAI.ThorpNine.Smoothing.Thorp.Card line 1546
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:11 (same declaration text).
def OAI.ThorpNine.Smoothing.Thorp.switchFun line 1548
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:13 (same declaration text).
theorem OAI.ThorpNine.Smoothing.Thorp.switchFun_involutive line 1551
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:16 (same declaration text).
def OAI.ThorpNine.Smoothing.Thorp.pairSwitch line 1560
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:25 (same declaration text).
def OAI.ThorpNine.Smoothing.Thorp.Butterfly line 1566
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:31 (same declaration text).
def OAI.ThorpNine.Smoothing.Thorp.childLift line 1570
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:35 (same declaration text).
def OAI.ThorpNine.Smoothing.Thorp.butterflyPerm line 1576
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:41 (same declaration text).
def OAI.ThorpNine.Smoothing.Thorp.finiteMean line 1580
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:45 (same declaration text).
def OAI.ThorpNine.Smoothing.Thorp.SwitchIndex line 1583
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:48 (same declaration text).
instance OAI.ThorpNine.Smoothing.Thorp.(instance at line 1587) line 1587
instance OAI.ThorpNine.Smoothing.Thorp.(instance at line 1592) line 1592
def OAI.ThorpNine.Smoothing.Thorp.decodeButterfly line 1597
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:62 (same declaration text).
def OAI.ThorpNine.Smoothing.Thorp.PairRouting.tupleProbability line 1609
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:74 (same declaration text).
def OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.coordinateRelabel line 1618
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:83 (same declaration text).
def OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.sweep line 1624
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:89 (same declaration text).
abbrev OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.Tuples line 1629
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:94 (same declaration text).
def OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.sweepKernel line 1631
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:96 (same declaration text).
def OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.reflectedKernel line 1635
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:100 (same declaration text).
def OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.regularAbsoluteEvenTrace line 1640
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:105 (same declaration text).
def OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.MainStatement line 1643
Also declared: OAI/Probability/ThorpRouting/Smoothing/Model.lean:108 (same declaration text).
abbrev OAI.ThorpNine.Tail.Thorp.Card line 1669
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:11 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.switchFun line 1671
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:13 (same declaration text).
theorem OAI.ThorpNine.Tail.Thorp.switchFun_involutive line 1674
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:16 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.pairSwitch line 1683
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:25 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Butterfly line 1689
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:31 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.childLift line 1693
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:35 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.butterflyPerm line 1699
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:41 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.finiteMean line 1703
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:45 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.SwitchIndex line 1706
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:48 (same declaration text).
instance OAI.ThorpNine.Tail.Thorp.(instance at line 1710) line 1710
instance OAI.ThorpNine.Tail.Thorp.(instance at line 1715) line 1715
def OAI.ThorpNine.Tail.Thorp.decodeButterfly line 1720
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:62 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.PairRouting.tupleProbability line 1732
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:74 (same declaration text).
abbrev OAI.ThorpNine.Tail.Thorp.Specht.Cell line 1742
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:84 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.row line 1744
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:86 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.col line 1746
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:88 (same declaration text).
lemma OAI.ThorpNine.Tail.Thorp.Specht.row_lt_colLen line 1748
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:90 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.rowIndex line 1751
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:93 (same declaration text).
abbrev OAI.ThorpNine.Tail.Thorp.Specht.Tabloid line 1754
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:96 (same declaration text).
instance OAI.ThorpNine.Tail.Thorp.Specht.(instance at line 1757) line 1757
def OAI.ThorpNine.Tail.Thorp.Specht.baseTabloid line 1759
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:101 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.tabloidAct line 1761
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:103 (same declaration text).
lemma OAI.ThorpNine.Tail.Thorp.Specht.tabloidAct_apply line 1776
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:118 (same declaration text).
lemma OAI.ThorpNine.Tail.Thorp.Specht.tabloidAct_one line 1779
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:121 (same declaration text).
lemma OAI.ThorpNine.Tail.Thorp.Specht.tabloidAct_mul line 1783
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:125 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.tabloidRep line 1788
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:130 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.delta line 1800
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:142 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.colGroup line 1803
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:145 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.permSign line 1809
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:151 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.alternator line 1816
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:158 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.polytabloid line 1823
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:165 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.space line 1826
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:168 (same declaration text).
lemma OAI.ThorpNine.Tail.Thorp.Specht.orbit_mem_space line 1829
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:171 (same declaration text).
lemma OAI.ThorpNine.Tail.Thorp.Specht.action_mem_space line 1832
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:174 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.subrepresentation line 1844
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:186 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.representation line 1847
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:189 (same declaration text).
abbrev OAI.ThorpNine.Tail.Thorp.PermutationHilbert.H line 1858
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:200 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.hilbertEquiv line 1865
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:207 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.hilbertSpace line 1869
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:211 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.UnitaryFinite.continuousRepresentation line 1881
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:223 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.UnitaryFinite.sampleOperator line 1892
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:234 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.spaceHilbertEquiv line 1900
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:242 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.unitaryRepresentation line 1903
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:245 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.Specht.relabelledUnitary line 1909
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:251 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.SparseContact.sweepOperator line 1918
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:260 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.StrongSmoothing.coordinateRelabel line 1929
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:271 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.StrongSmoothing.sweep line 1935
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:277 (same declaration text).
abbrev OAI.ThorpNine.Tail.Thorp.StrongSmoothing.Tuples line 1940
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:282 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.StrongSmoothing.sweepKernel line 1942
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:284 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.StrongSmoothing.reflectedKernel line 1946
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:288 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.StrongTail.tailDiagram line 1957
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:301 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.StrongTail.DensityAt line 1966
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:307 (same declaration text).
def OAI.ThorpNine.Tail.Thorp.StrongTail.MainStatement line 1983
Also declared: OAI/Probability/ThorpRouting/Tail/Model.lean:324 (same declaration text).
abbrev OAI.ThorpNine.HighTail.Thorp.Card line 2007
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:11 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.switchFun line 2009
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:13 (same declaration text).
theorem OAI.ThorpNine.HighTail.Thorp.switchFun_involutive line 2012
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:16 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.pairSwitch line 2021
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:25 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.Butterfly line 2027
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:31 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.childLift line 2031
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:35 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.butterflyPerm line 2037
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:41 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.finiteMean line 2041
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:45 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.SwitchIndex line 2044
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:48 (same declaration text).
instance OAI.ThorpNine.HighTail.Thorp.(instance at line 2048) line 2048
instance OAI.ThorpNine.HighTail.Thorp.(instance at line 2053) line 2053
def OAI.ThorpNine.HighTail.Thorp.decodeButterfly line 2058
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:62 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.orbitSet line 2065
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:69 (same declaration text).
abbrev OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.SelectedCycle line 2076
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:80 (same declaration text).
instance OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.(instance at line 2079) line 2079
def OAI.ThorpNine.HighTail.Thorp.cardSplit line 2088
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:92 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.assembleBits line 2108
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:112 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.pairLayer line 2119
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:123 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.coinStepEquiv line 2133
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:137 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.headTailEquiv line 2147
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:151 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.CycleColoring.alternatingPerm line 2157
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:161 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.PairRouting.required line 2170
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:174 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.PairRouting.Compatible line 2172
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:176 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.PairRouting.colors line 2175
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:179 (same declaration text).
lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.required_colors line 2179
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:183 (same declaration text).
lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.colors_compatible line 2185
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:189 (same declaration text).
lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.Compatible.tail_injective line 2190
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:194 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.PairRouting.childEmbedding line 2201
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:205 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.PairRouting.labelSet line 2204
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:208 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.PairRouting.alternatingProjection line 2206
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:210 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.PairRouting.alternatingCycles line 2208
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:212 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.PairRouting.switchedEmbedding line 2212
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:216 (same declaration text).
abbrev OAI.ThorpNine.HighTail.Thorp.BenesCoins line 2223
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:227 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.palindromePerm line 2225
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:229 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.sandwichShuffle line 2228
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:232 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.benesStepEquiv line 2235
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:239 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.palindromeCost line 2239
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:243 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.palindromeLowCost line 2254
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:258 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.HighHeight.highCost line 2272
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:276 (same declaration text).
def OAI.ThorpNine.HighTail.Thorp.HighHeight.MainStatement line 2276
Also declared: OAI/Probability/ThorpRouting/HighTail/Model.lean:280 (same declaration text).
abbrev OAI.ThorpNine.SparseSaving.Thorp.Card line 2307
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:11 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.switchFun line 2309
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:13 (same declaration text).
theorem OAI.ThorpNine.SparseSaving.Thorp.switchFun_involutive line 2312
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:16 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.pairSwitch line 2321
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:25 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Butterfly line 2327
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:31 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.childLift line 2331
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:35 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.butterflyPerm line 2337
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:41 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.SwitchIndex line 2341
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:45 (same declaration text).
instance OAI.ThorpNine.SparseSaving.Thorp.(instance at line 2345) line 2345
instance OAI.ThorpNine.SparseSaving.Thorp.(instance at line 2350) line 2350
def OAI.ThorpNine.SparseSaving.Thorp.decodeButterfly line 2355
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:59 (same declaration text).
abbrev OAI.ThorpNine.SparseSaving.Thorp.Specht.Cell line 2365
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:69 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.row line 2367
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:71 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.col line 2369
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:73 (same declaration text).
lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.row_lt_colLen line 2371
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:75 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.rowIndex line 2374
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:78 (same declaration text).
abbrev OAI.ThorpNine.SparseSaving.Thorp.Specht.Tabloid line 2377
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:81 (same declaration text).
instance OAI.ThorpNine.SparseSaving.Thorp.Specht.(instance at line 2380) line 2380
def OAI.ThorpNine.SparseSaving.Thorp.Specht.baseTabloid line 2382
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:86 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.tabloidAct line 2384
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:88 (same declaration text).
lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.tabloidAct_apply line 2399
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:103 (same declaration text).
lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.tabloidAct_one line 2402
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:106 (same declaration text).
lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.tabloidAct_mul line 2406
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:110 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.tabloidRep line 2411
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:115 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.delta line 2423
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:127 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.colGroup line 2426
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:130 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.permSign line 2432
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:136 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.alternator line 2439
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:143 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.polytabloid line 2446
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:150 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.space line 2449
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:153 (same declaration text).
lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.orbit_mem_space line 2452
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:156 (same declaration text).
lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.action_mem_space line 2455
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:159 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.subrepresentation line 2467
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:171 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.representation line 2470
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:174 (same declaration text).
abbrev OAI.ThorpNine.SparseSaving.Thorp.PermutationHilbert.H line 2481
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:185 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.hilbertEquiv line 2488
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:192 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.hilbertSpace line 2492
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:196 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.continuousRepresentation line 2504
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:208 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.sampleOperator line 2515
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:219 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.spaceHilbertEquiv line 2523
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:227 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.unitaryRepresentation line 2526
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:230 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.Specht.relabelledUnitary line 2532
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:236 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.sweepOperator line 2541
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:245 (same declaration text).
def OAI.ThorpNine.SparseSaving.Thorp.SparseRegime.MainStatement line 2552
Also declared: OAI/Probability/ThorpRouting/SparseSaving/Model.lean:256 (same declaration text).
theorem OAI.ThorpNine.main Challenge statement: Nine routing-density and representation estimates sorry line 2567
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.Probability.ThorpRouting.Main as the released solution module checked against this declaration.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Distinct definitions of this name: OAI/Probability/ThorpRouting/Main.lean:13 (same statement text; different proof or body). Qualify references as OAI.ThorpNine.main@path.
```
theorem ThorpNine.main :
    ThorpNine.Adaptive.Thorp.AdaptiveBounds.MainStatement ∧
    ThorpNine.Casimir.Thorp.CasimirBounds.MainStatement ∧
    ThorpNine.Dense.Thorp.DenseTruncation.MainStatement ∧
    ThorpNine.Contact.Thorp.SparseContact.MainStatement ∧
    ThorpNine.Harmonic.Thorp.HarmonicBounds.MainStatement ∧
    ThorpNine.Smoothing.Thorp.StrongSmoothing.MainStatement ∧
    ThorpNine.Tail.Thorp.StrongTail.MainStatement ∧
    ThorpNine.HighTail.Thorp.HighHeight.MainStatement ∧
    ThorpNine.SparseSaving.Thorp.SparseRegime.MainStatement := by
…
```
Mentions: OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.MainStatement, OAI.ThorpNine.Casimir.Thorp.CasimirBounds.MainStatement, OAI.ThorpNine.Dense.Thorp.DenseTruncation.MainStatement, OAI.ThorpNine.Contact.Thorp.SparseContact.MainStatement, OAI.ThorpNine.Harmonic.Thorp.HarmonicBounds.MainStatement, OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.MainStatement, OAI.ThorpNine.Tail.Thorp.StrongTail.MainStatement, OAI.ThorpNine.HighTail.Thorp.HighHeight.MainStatement, OAI.ThorpNine.SparseSaving.Thorp.SparseRegime.MainStatement