ComparatorChallenges/IrrationalRotation.lean

GitHub source file

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

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

118 declarations, 2 contain sorry, 0 declared as axioms

  1. abbrev OAI.Invariant233.Circle line 12

    Also declared: OAI/Analysis/IrrationalRotation/Model/Analytic.lean:14 (same declaration text).

  2. def OAI.Invariant233.circleMeasure line 14

    Also declared: OAI/Analysis/IrrationalRotation/Model/Analytic.lean:16 (same declaration text).

  3. def OAI.Invariant233.negLogCost line 16

    Also declared: OAI/Analysis/IrrationalRotation/Model/Analytic.lean:18 (same declaration text).

  4. def OAI.Invariant233.HasNegInfiniteLogIntegral line 19

    Also declared: OAI/Analysis/IrrationalRotation/Model/Analytic.lean:21 (same declaration text).

  5. def OAI.Invariant233.scalarWeightDeterminant line 23

    Also declared: OAI/Analysis/IrrationalRotation/Model/Analytic.lean:25 (same declaration text).

  6. def OAI.Invariant233.NormQuasinilpotent line 27

    Also declared: OAI/Analysis/IrrationalRotation/Model/Analytic.lean:29 (same declaration text).

  7. def OAI.Invariant233.IsContinuousCircleWeight line 30

    Also declared: OAI/Analysis/IrrationalRotation/Model/Analytic.lean:32 (same declaration text).

  8. abbrev OAI.Invariant233.WeightedShift.Hilbert line 44

    Also declared: OAI/Analysis/IrrationalRotation/Model/WeightedShift.lean:13 (same declaration text).

  9. abbrev OAI.Invariant233.WeightedShift.Weight line 45

    Also declared: OAI/Analysis/IrrationalRotation/Model/WeightedShift.lean:14 (same declaration text).

  10. def OAI.Invariant233.WeightedShift.reindex line 47

    Also declared: OAI/Analysis/IrrationalRotation/Model/WeightedShift.lean:16 (same declaration text).

  11. def OAI.Invariant233.WeightedShift.shift line 61

    Also declared: OAI/Analysis/IrrationalRotation/Model/WeightedShift.lean:30 (same declaration text).

  12. def OAI.Invariant233.WeightedShift.diagonal line 63

    Also declared: OAI/Analysis/IrrationalRotation/Model/WeightedShift.lean:32 (same declaration text).

  13. def OAI.Invariant233.WeightedShift.diagonalAlgHom line 69

    Also declared: OAI/Analysis/IrrationalRotation/Model/WeightedShift.lean:38 (same declaration text).

  14. def OAI.Invariant233.WeightedShift.translate line 92

    Also declared: OAI/Analysis/IrrationalRotation/Model/WeightedShift.lean:61 (same declaration text).

  15. def OAI.Invariant233.WeightedShift.operator line 98

    Also declared: OAI/Analysis/IrrationalRotation/Model/WeightedShift.lean:67 (same declaration text).

  16. def OAI.Invariant233.WeightedShift.orbitProduct line 101

    Also declared: OAI/Analysis/IrrationalRotation/Model/WeightedShift.lean:70 (same declaration text).

  17. def OAI.Invariant233.WeightedShift.tailWeight line 114

    Also declared: OAI/Analysis/IrrationalRotation/Model/WeightedShift.lean:83 (same declaration text).

  18. def OAI.Invariant233.WeightedShift.tailProjection line 120

    Also declared: OAI/Analysis/IrrationalRotation/Model/WeightedShift.lean:89 (same declaration text).

  19. def OAI.Invariant233.vonNeumannGenerated line 138

    Also declared: OAI/Analysis/IrrationalRotation/Model/GeneratedVonNeumann.lean:15 (same declaration text).

  20. theorem OAI.Invariant233.WeightedShift.diagonal_value line 163

    Also declared: OAI/Analysis/IrrationalRotation/Model/FieldDiagonal.lean:14 (same declaration text).

  21. theorem OAI.Invariant233.WeightedShift.diagonal_bound line 166

    Also declared: OAI/Analysis/IrrationalRotation/Model/FieldDiagonal.lean:17 (same declaration text).

  22. theorem OAI.Invariant233.WeightedShift.diagonal_aestronglyMeasurable line 171

    Also declared: OAI/Analysis/IrrationalRotation/Model/FieldDiagonal.lean:22 (same declaration text).

  23. def OAI.Invariant233.WeightedShift.fieldDiagonalVec line 192

    Also declared: OAI/Analysis/IrrationalRotation/Model/FieldDiagonal.lean:43 (same declaration text).

  24. theorem OAI.Invariant233.WeightedShift.fieldDiagonalVec_ae line 200

    Also declared: OAI/Analysis/IrrationalRotation/Model/FieldDiagonal.lean:51 (same declaration text).

  25. def OAI.Invariant233.WeightedShift.fieldDiagonalLinear line 208

    Also declared: OAI/Analysis/IrrationalRotation/Model/FieldDiagonal.lean:59 (same declaration text).

  26. def OAI.Invariant233.WeightedShift.fieldDiagonal line 231

    Also declared: OAI/Analysis/IrrationalRotation/Model/FieldDiagonal.lean:82 (same declaration text).

  27. instance OAI.Invariant233.Rotation.circleMeasure_probability line 257

    Also declared: OAI/Analysis/IrrationalRotation/Model/Rotation.lean:17 (same declaration text).

  28. abbrev OAI.Invariant233.Rotation.Fiber line 262

    Also declared: OAI/Analysis/IrrationalRotation/Model/Rotation.lean:22 (same declaration text).

  29. abbrev OAI.Invariant233.Rotation.Hilbert line 263

    Also declared: OAI/Analysis/IrrationalRotation/Model/Rotation.lean:23 (same declaration text).

  30. def OAI.Invariant233.Rotation.action line 265

    Also declared: OAI/Analysis/IrrationalRotation/Model/Rotation.lean:25 (same declaration text).

  31. def OAI.Invariant233.Rotation.U line 268

    Also declared: OAI/Analysis/IrrationalRotation/Model/Rotation.lean:28 (same declaration text).

  32. def OAI.Invariant233.Rotation.orbitWeight line 271

    Also declared: OAI/Analysis/IrrationalRotation/Model/Rotation.lean:31 (same declaration text).

  33. def OAI.Invariant233.Rotation.character line 277

    Also declared: OAI/Analysis/IrrationalRotation/Model/Rotation.lean:37 (same declaration text).

  34. def OAI.Invariant233.Rotation.representation line 279

    Also declared: OAI/Analysis/IrrationalRotation/Model/Rotation.lean:39 (same declaration text).

  35. def OAI.Invariant233.Rotation.V line 288

    Also declared: OAI/Analysis/IrrationalRotation/Model/Rotation.lean:48 (same declaration text).

  36. def OAI.Invariant233.Rotation.algebra line 290

    Also declared: OAI/Analysis/IrrationalRotation/Model/Rotation.lean:50 (same declaration text).

  37. def OAI.Invariant233.Rotation.weighted line 293

    Also declared: OAI/Analysis/IrrationalRotation/Model/Rotation.lean:53 (same declaration text).

  38. def OAI.Invariant233.Rotation.complexWeight line 296

    Also declared: OAI/Analysis/IrrationalRotation/Model/Rotation.lean:56 (same declaration text).

  39. def OAI.Invariant233.Rotation.weightedReal line 299

    Also declared: OAI/Analysis/IrrationalRotation/Model/Rotation.lean:59 (same declaration text).

  40. def OAI.Invariant233.Rotation.vacuum line 302

    Also declared: OAI/Analysis/IrrationalRotation/Model/Rotation.lean:62 (same declaration text).

  41. def OAI.Invariant233.Rotation.vacuumFunctional line 304

    Also declared: OAI/Analysis/IrrationalRotation/Model/Rotation.lean:64 (same declaration text).

  42. def OAI.Invariant233.HasOnlyTrivialInvariantProjections line 322

    Also declared: OAI/Analysis/IrrationalRotation/Model/OperatorProperties.lean:15 (same declaration text).

  43. def OAI.Invariant233.IsProjectionAtom line 327

    Also declared: OAI/Analysis/IrrationalRotation/Model/OperatorProperties.lean:20 (same declaration text).

  44. def OAI.Invariant233.IsAtomicVonNeumannAlgebra line 332

    Also declared: OAI/Analysis/IrrationalRotation/Model/OperatorProperties.lean:25 (same declaration text).

  45. def OAI.Invariant233.IsAbelianVonNeumannAlgebra line 336

    Also declared: OAI/Analysis/IrrationalRotation/Model/OperatorProperties.lean:29 (same declaration text).

  46. def OAI.Invariant233.IsDiffuseVonNeumannAlgebra line 339

    Also declared: OAI/Analysis/IrrationalRotation/Model/OperatorProperties.lean:32 (same declaration text).

  47. def OAI.Invariant233.IsFactor line 342

    Also declared: OAI/Analysis/IrrationalRotation/Model/OperatorProperties.lean:35 (same declaration text).

  48. def OAI.Invariant233.vectorTrace line 347

    Also declared: OAI/Analysis/IrrationalRotation/Model/OperatorProperties.lean:40 (same declaration text).

  49. def OAI.Invariant233.IsFaithfulTracialVector line 350

    Also declared: OAI/Analysis/IrrationalRotation/Model/OperatorProperties.lean:43 (same declaration text).

  50. def OAI.Invariant233.IsTypeII1FactorWithVector line 357

    Also declared: OAI/Analysis/IrrationalRotation/Model/OperatorProperties.lean:50 (same declaration text).

  51. def OAI.Invariant233.HasSeparablePredual line 363

    Also declared: OAI/Analysis/IrrationalRotation/Model/OperatorProperties.lean:56 (same declaration text).

  52. structure OAI.Invariant233.TracialState line 383

    Also declared: OAI/Analysis/IrrationalRotation/Model/Spectral.lean:12 (same declaration text).

  53. instance OAI.Invariant233.TracialState.(instance at line 394) line 394
  54. def OAI.Invariant233.fugledeKadisonDeterminant line 399

    Also declared: OAI/Analysis/IrrationalRotation/Model/Spectral.lean:28 (same declaration text).

  55. def OAI.Invariant233.logarithmicPotentialDeterminant line 404

    Also declared: OAI/Analysis/IrrationalRotation/Model/Spectral.lean:33 (same declaration text).

  56. def OAI.Invariant233.IsBrownMeasure line 408

    Also declared: OAI/Analysis/IrrationalRotation/Model/Spectral.lean:37 (same declaration text).

  57. def OAI.Invariant233.vectorFugledeKadisonDeterminant line 428

    Also declared: OAI/Analysis/IrrationalRotation/Model/ConcreteSpectral.lean:13 (same declaration text).

  58. def OAI.Invariant233.IsVectorBrownMeasure line 432

    Also declared: OAI/Analysis/IrrationalRotation/Model/ConcreteSpectral.lean:17 (same declaration text).

  59. def OAI.Invariant233.operatorModulus line 437

    Also declared: OAI/Analysis/IrrationalRotation/Model/ConcreteSpectral.lean:22 (same declaration text).

  60. def OAI.Invariant233.HasCountablyAtomicSpectralType line 439

    Also declared: OAI/Analysis/IrrationalRotation/Model/ConcreteSpectral.lean:24 (same declaration text).

  61. def OAI.Invariant233.polarConjugate line 443

    Also declared: OAI/Analysis/IrrationalRotation/Model/ConcreteSpectral.lean:28 (same declaration text).

  62. def OAI.Invariant233.finitePolarAlgebra line 447

    Also declared: OAI/Analysis/IrrationalRotation/Model/ConcreteSpectral.lean:32 (same declaration text).

  63. def OAI.Invariant233.fullPolarAlgebra line 450

    Also declared: OAI/Analysis/IrrationalRotation/Model/ConcreteSpectral.lean:35 (same declaration text).

  64. def OAI.Invariant233.ProductPolarStructure line 453

    Also declared: OAI/Analysis/IrrationalRotation/Model/ConcreteSpectral.lean:38 (same declaration text).

  65. def OAI.Invariant233.circleRepresentative line 475

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductBase.lean:13 (same declaration text).

  66. instance OAI.Invariant233.circleMeasure_probability line 478

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductBase.lean:16 (same declaration text).

  67. abbrev OAI.Invariant233.ProductModel.Base line 484

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductBase.lean:22 (same declaration text).

  68. def OAI.Invariant233.ProductModel.baseMeasure line 486

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductBase.lean:24 (same declaration text).

  69. instance OAI.Invariant233.ProductModel.baseMeasure_probability line 488

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductBase.lean:26 (same declaration text).

  70. def OAI.Invariant233.ProductModel.Ordered line 492

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductBase.lean:30 (same declaration text).

  71. def OAI.Invariant233.ProductModel.rotation line 495

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductBase.lean:33 (same declaration text).

  72. def OAI.Invariant233.ProductModel.rotationIterate line 498

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductBase.lean:36 (same declaration text).

  73. def OAI.Invariant233.ProductModel.logarithmicCost line 501

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductBase.lean:39 (same declaration text).

  74. def OAI.Invariant233.ProductModel.weight line 504

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductBase.lean:42 (same declaration text).

  75. def OAI.Invariant233.ProductModel.JointlyRationallyIndependent line 507

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductBase.lean:45 (same declaration text).

  76. def OAI.Invariant233.ProductModel.AdmissibleAnglesAndCosts line 510

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductBase.lean:48 (same declaration text).

  77. abbrev OAI.Invariant233.ProductModel.Fiber line 514

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductBase.lean:52 (same declaration text).

  78. abbrev OAI.Invariant233.ProductModel.Hilbert line 515

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductBase.lean:53 (same declaration text).

  79. theorem OAI.Invariant233.ProductModel.measurable_rep line 535

    Also declared: OAI/Analysis/IrrationalRotation/Model/Product.lean:14 (same declaration text).

  80. theorem OAI.Invariant233.ProductModel.measurable_iterate line 538

    Also declared: OAI/Analysis/IrrationalRotation/Model/Product.lean:17 (same declaration text).

  81. theorem OAI.Invariant233.ProductModel.measurable_cost line 549

    Also declared: OAI/Analysis/IrrationalRotation/Model/Product.lean:28 (same declaration text).

  82. theorem OAI.Invariant233.ProductModel.weight_measurable line 558

    Also declared: OAI/Analysis/IrrationalRotation/Model/Product.lean:37 (same declaration text).

  83. theorem OAI.Invariant233.ProductModel.weight_nonneg line 561

    Also declared: OAI/Analysis/IrrationalRotation/Model/Product.lean:40 (same declaration text).

  84. theorem OAI.Invariant233.ProductModel.weight_le_one line 564

    Also declared: OAI/Analysis/IrrationalRotation/Model/Product.lean:43 (same declaration text).

  85. def OAI.Invariant233.ProductModel.shiftOperator line 571

    Also declared: OAI/Analysis/IrrationalRotation/Model/Product.lean:50 (same declaration text).

  86. def OAI.Invariant233.ProductModel.multiplierField line 574

    Also declared: OAI/Analysis/IrrationalRotation/Model/Product.lean:53 (same declaration text).

  87. def OAI.Invariant233.ProductModel.multiplier line 581

    Also declared: OAI/Analysis/IrrationalRotation/Model/Product.lean:60 (same declaration text).

  88. def OAI.Invariant233.ProductModel.multiplierGenerators line 587

    Also declared: OAI/Analysis/IrrationalRotation/Model/Product.lean:66 (same declaration text).

  89. def OAI.Invariant233.ProductModel.factor line 591

    Also declared: OAI/Analysis/IrrationalRotation/Model/Product.lean:70 (same declaration text).

  90. def OAI.Invariant233.ProductModel.traceVector line 594

    Also declared: OAI/Analysis/IrrationalRotation/Model/Product.lean:73 (same declaration text).

  91. theorem OAI.Invariant233.ProductModel.measurable_complexWeight line 596

    Also declared: OAI/Analysis/IrrationalRotation/Model/Product.lean:75 (same declaration text).

  92. theorem OAI.Invariant233.ProductModel.norm_complexWeight_le_one line 600

    Also declared: OAI/Analysis/IrrationalRotation/Model/Product.lean:79 (same declaration text).

  93. def OAI.Invariant233.ProductModel.weightedOperator line 639

    Also declared: OAI/Analysis/IrrationalRotation/Model/Product.lean:118 (same declaration text).

  94. abbrev OAI.Invariant233.ProductModel.EndpointPair line 667

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductSampling.lean:13 (same declaration text).

  95. def OAI.Invariant233.ProductModel.selectedEndpoint line 669

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductSampling.lean:15 (same declaration text).

  96. def OAI.Invariant233.ProductModel.triangularEvent line 672

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductSampling.lean:18 (same declaration text).

  97. def OAI.Invariant233.ProductModel.triangularLaw line 675

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductSampling.lean:21 (same declaration text).

  98. def OAI.Invariant233.ProductModel.triangularFirstDensity line 679

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductSampling.lean:25 (same declaration text).

  99. def OAI.Invariant233.ProductModel.triangularSecondDensity line 682

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductSampling.lean:28 (same declaration text).

  100. def OAI.Invariant233.ProductModel.TriangularLawProperties line 685

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductSampling.lean:31 (same declaration text).

  101. def OAI.Invariant233.ProductModel.WeaklyConverges line 696

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductSampling.lean:42 (same declaration text).

  102. def OAI.Invariant233.ProductModel.SupportedOnPositiveOrderedOrbitPairs line 700

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductSampling.lean:46 (same declaration text).

  103. def OAI.Invariant233.ProductModel.HasUniformL2Marginals line 705

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductSampling.lean:51 (same declaration text).

  104. def OAI.Invariant233.ProductModel.OrderedOrbitSampling line 712

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductSampling.lean:58 (same declaration text).

  105. def OAI.Invariant233.ProductModel.HasAllFiniteCoordinateSampling line 718

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductSampling.lean:64 (same declaration text).

  106. def OAI.Invariant233.ProductModel.IsCovariantFieldRepresentation line 731

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductFactorStructure.lean:10 (same declaration text).

  107. def OAI.Invariant233.ProductModel.centralDiagonalIntegral line 741

    Also declared: OAI/Analysis/IrrationalRotation/Model/ProductFactorStructure.lean:20 (same declaration text).

  108. def OAI.Invariant233.Rotation.IsContinuousCounterexample line 754

    Distinct definitions of this name: OAI/Analysis/IrrationalRotation/Model/ContinuousCounterexample.lean:10 (same statement text; different proof or body). Qualify references as OAI.Invariant233.Rotation.IsContinuousCounterexample@path.

  109. abbrev OAI.Invariant233.ProductModel.CounterexampleFiber line 769

    Also declared: OAI/Analysis/IrrationalRotation/Main.lean:603 (same declaration text).

  110. abbrev OAI.Invariant233.ProductModel.CounterexampleHilbert line 772

    Also declared: OAI/Analysis/IrrationalRotation/Main.lean:606 (same declaration text).

  111. instance OAI.Invariant233.ProductModel.instCompleteSpaceHilbertCounterexample line 778

    Also declared: OAI/Analysis/IrrationalRotation/Main.lean:612 (same declaration text).

  112. def OAI.Invariant233.ProductOperatorProperties line 781

    Also declared: OAI/Analysis/IrrationalRotation/Main.lean:615 (same declaration text).

  113. def OAI.Invariant233.ProductModel.counterexampleHilbertNormedAddCommGroup line 795

    Also declared: OAI/Analysis/IrrationalRotation/Main.lean:629 (same declaration text).

  114. def OAI.Invariant233.ProductModel.counterexampleHilbertInnerProductSpace line 804

    Also declared: OAI/Analysis/IrrationalRotation/Main.lean:638 (same declaration text).

  115. def OAI.Invariant233.ProductModel.HasCounterexampleOperator line 815

    Also declared: OAI/Analysis/IrrationalRotation/Main.lean:649 (same declaration text).

  116. def OAI.Invariant233.ProductModel.IsCounterexampleRealization line 822

    Also declared: OAI/Analysis/IrrationalRotation/Main.lean:656 (same declaration text).

  117. theorem OAI.Invariant233.Results.prescribed_irrational_counterexample Challenge statement: Invariant-projection counterexamples for every irrational rotation sorry line 838

    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 6 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    2. The repository's comparator configuration selects OAI.Analysis.IrrationalRotation.Main as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Analysis/IrrationalRotation/PrescribedAngle.lean:17 (different declaration text). Qualify references as OAI.Invariant233.Results.prescribed_irrational_counterexample@path.

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

    Gives

    • together with OAI.InternalCatalan.catalan_irrational, gives 0 < ∑' (j : ℕ), (-1) ^ j / ↑(2 * j + 1) ^ 2 → ∑' (j : ℕ), (-1) ^ j / ↑(2 * j + 1) ^ 2 < 1 → ∃ f, OAI.Invariant233.Rotation.IsContinuousCounterexample (∑' (j : ℕ), (-1) ^ j / ↑(2 * j + 1) ^ 2) f (short composition) checked derivation
    theorem prescribed_irrational_counterexample (θ : ℝ)
    (hθ0 : 0 < θ) (hθ1 : θ < 1) (hθ : Irrational θ) :
    ∃ f : C(Circle, ℝ), Rotation.IsContinuousCounterexample θ f := by
…

    Mentions: OAI.Invariant233.Circle

  118. theorem OAI.Invariant233.Results.product_realization Challenge statement: Invariant-projection counterexamples for every irrational rotation sorry line 843

    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 6 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    2. The repository's comparator configuration selects OAI.Analysis.IrrationalRotation.Main as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Analysis/IrrationalRotation/Main.lean:670 (same statement text; different proof or body). Qualify references as OAI.Invariant233.Results.product_realization@path.

    theorem product_realization :
    ∃ θ c : ℕ → ℝ, ProductModel.IsCounterexampleRealization θ c := by
…

    Mentions: OAI.Invariant233.ProductModel.IsCounterexampleRealization