openpr_K_v3_gemini.txt

====================================================================================================
CASE K  PR #33664  (open-pr, v3 prompt, Gemini)
file: Mathlib/Geometry/Convex/Cone/Pointed/Face/Basic.lean  line: 44.0
reviewer: @eric-wieser  on 2026-01-06T13:06:18Z
advice_kind: docstring suggestion
model: gemini-2.5-flash  prompt_tokens: 7853  completion_tokens: 1086
HUMAN reviewer (ground truth):
  > ```suggestion
  > for all `x, y` in `C` and positive scalars `a`, then `x` is also in `F`. -/
  > ```
====================================================================================================

[SYSTEM]
----------------------------------------------------------------------------------------------------
You are an expert reviewer for the Lean 4 / mathlib4 mathematical library. Given a NEW code hunk from an open pull request and a set of historically retrieved (past_hunk, past_comment) pairs, your job is to identify which past reviewer feedback would also apply to the new hunk.

Your single most important task is to AVOID "axis-miss" false positives: cases where a past comment and the new code LOOK similar on the surface, but the past reviewer was raising a different KIND of concern than anything the new hunk actually has. A correct silent output is far more valuable than a confident wrong-axis answer.

Read carefully before producing JSON. Follow the four steps below in order.

STEP 1 — STRUCTURAL + SEMANTIC READING OF THE NEW HUNK.
  1a. Parse the code shape: tactic-mode vs term-mode, declaration kind (`def` / `theorem` / `lemma` / `instance` / `class` / `structure` / `abbrev` / `syntax` / `notation`), attributes (`@[simp]`, `@[to_additive]`, `@[deprecated]`, `@[ext]`, `@[fun_prop]`, `@[reassoc]`, …), universe parameters, implicit/explicit binders, docstring style, proof tactics used.
  1b. Inventory what *could* be criticized about THIS specific hunk. Pick as many as apply from this list of "concern axes":
     - correctness-bug        (code doesn't typecheck / is logically wrong)
     - naming                  (lemma/def name doesn't follow conventions)
     - docstring               (missing, unclear, typo, wrong phrasing)
     - attribute               (missing/wrong `@[simp]` / `@[to_additive]` …)
     - style-syntax            (`fun x ↦` vs `fun x =>`, `by use _; exact _` vs `⟨_, _⟩`, whitespace/`ppSpace`, notation preference)
     - proof-golf              (the proof tactics could be shorter/nicer)
     - refactor-simplify       (same statement provable with less machinery)
     - generalize-signature    (hypotheses too strong; remove/weaken a typeclass)
     - design-smell-architectural (this API shape is wrong; returning a string, unnecessary instance, redundant definition, etc.)
     - imports-module          (superfluous imports, module structure)
     - namespace-organization  (`_root_`, namespace boundary, file placement)
     - automation-tactic       (should use / should teach `aesop_cat`, `gcongr`, `positivity`, etc.)
     - instance-diamond        (this instance creates an ambiguity / defeq diamond with another)
     - unify-with-existing     (a similar definition/lemma already exists)
     - junk-value              (docstring should note behavior at the "undefined" input; handled via `0`/`⊥`/`⊤`)
  List the concerns that PLAUSIBLY apply to the new hunk. If none are obviously present, say so — don't invent them.

STEP 2 — PER-CANDIDATE CONCERN CLASSIFICATION.
  For EACH candidate, identify which concern axis (from the same list) the past reviewer's comment was about. Read the past comment carefully: the reviewer's *words* (not the past code) tell you the concern axis. If a past comment ships a `suggestion` code block, that block is evidence for what the reviewer wanted changed — but the axis of concern comes from the prose around it. Ignore candidates whose past comment is pure bikeshed or where you cannot identify a clear concern.

STEP 3 — AXIS MATCH + APPLICABILITY CHECK.
  A candidate is eligible for `strong_matches` ONLY if BOTH:
    (a) Its axis (from step 2) is among the new hunk's plausible concerns (from step 1b).
    (b) You can write a concrete adaptation that a Lean/mathlib reviewer would plausibly post on the new hunk *today*, given what is visible in the hunk.
  Before promoting, write — in the JSON output, per match — a `why_might_not_apply` field giving the strongest counter-argument against promotion (one short sentence). If this counter-argument is actually compelling (e.g. "the new code does not have that pattern", "the new code *does* have an ext lemma, so this doesn't apply"), DO NOT promote; demote to `weak_observations` or drop.
  Cross-candidate synthesis is allowed: if candidate X establishes that an identifier in the new hunk is a `class`, and candidate Y shows the preferred term-mode `instance := ⟨...⟩` template, they jointly support a promotion. List both in `supporting_past_prs` and still produce one `why_might_not_apply`.

STEP 4 — CONFIDENCE AND OUTPUT.
  Confidence scale:
    - "high"   — ≥1 strong match survives step 3 AND the adaptation is a near-verbatim application of a past comment; the counter-argument is weak.
    - "medium" — ≥1 strong match survives step 3 BUT needs adaptation or synthesis; counter-argument is plausible but not decisive.
    - "low"    — no candidate survives step 3; only stylistic patterns worth mentioning as `weak_observations`.
    - "none"   — retrieved pool's axes don't match anything plausible about the new hunk; state this and stop.
  When in doubt between "medium" and "low" on a single uncertain candidate, prefer "low" and put that candidate in `weak_observations`. "Confident but wrong-axis" is the #1 failure we are trying to eliminate.

Output JSON ONLY, matching this exact schema:

{
  "new_hunk_plausible_concerns": [<one or more axis labels from Step 1b, or []>],
  "summary": "<one sentence describing what we found>",
  "confidence": "high"|"medium"|"low"|"none",
  "strong_matches": [
    {
      "past_pr": <int>,
      "past_file": "<string>",
      "past_concern_axis": "<axis label from the list>",
      "past_comment_excerpt": "<verbatim short quote from the past comment OR the relevant snippet from its suggestion block>",
      "applies_because": "<one or two sentences linking past code/comment to the new hunk's structure AND explaining why the concern axis matches>",
      "suggested_adaptation": "<one sentence on what the reviewer might say on the new hunk>",
      "why_might_not_apply": "<one short sentence — strongest counter-argument against this promotion>",
      "supporting_past_prs": [<int>, ...]
    }
  ],
  "weak_observations": [
    {
      "observation": "<short string>",
      "axis": "<axis label>",
      "supporting_past_prs": [<int>, ...]
    }
  ]
}

Quote short — under 40 words per excerpt. Do not invent axis labels outside the list. Do not promote a candidate whose axis is not in `new_hunk_plausible_concerns`.

[USER]
----------------------------------------------------------------------------------------------------
NEW HUNK from open PR #33664 (file: Mathlib/Geometry/Convex/Cone/Pointed/Face/Basic.lean):
```
@@ -0,0 +1,276 @@
... [4 lines above hidden]
+Authors: Olivia Röhrig
+-/
+module
+
+public import Mathlib.Analysis.Convex.Extreme
+public import Mathlib.Geometry.Convex.Cone.Pointed.Basic
+
+/-!
+# Faces of pointed cones
+
+This file defines what it means for a pointed cone to be a face of another pointed cone and
+establishes basic properties of this relation.
+A subcone `F` of a cone `C` is a face if any two points in `C` that have a positive combination
+in `F` are also in `F`.
+
+## Main declarations
+
+* `IsFaceOf F C`: States that the pointed cone `F` is a face of the pointed cone `C`.
+
+## Implementation notes
+
+* We prove that every face is an extreme set of its cone. We do not use `IsExtreme` as a
+  definition because this is an affine notion and does not allow the flexibility necessary to
+  deal wth cones over general rings. E.g. the cone of positive integers has no proper subset that
+  are extreme.
+* Most results proven over a field hold more generally over an Archimedean ring. In particular,
+  `iff_mem_of_add_mem` holds whenever for every `x ∈ R` there is a `y ∈ R` with `1 ≤ x * y`.
+
+-/
+
+open Submodule
+
+@[expose] public section
+
+namespace PointedCone
+
+variable {R M N : Type*}
+
+variable [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M] in
+/-- A pointed cone `F` is a face of another pointed cone `C` if `F ≤ C` and if `a • x + y` is in `F`
+for all `x, y` in `C` and positive scalars `a`, then `x` ist also in `F`. -/
```

RETRIEVED CANDIDATES (top-20 by hunk-embedding similarity, sorted by sim desc):

--- candidate 1 (sim=0.773, past_pr=#6437, file=Mathlib/Analysis/Convex/Cone/Pointed.lean) ---
PAST HUNK:
```
@@ -0,0 +1,265 @@
... [2 lines above hidden]
+Copyright (c) 2022 Apurva Nakade All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Apurva Nakade
+-/
+import Mathlib.Analysis.Convex.Cone.Dual
+import Mathlib.Algebra.Order.Nonneg.Ring
+import Mathlib.Algebra.Module.Submodule.Basic
+
+
+/-!
+# Pointed cones
+
+We define pointed cone as a convex cone which contains `0`. This is a bundled version of
```
PAST COMMENT (from reviewer):
```suggestion
A *pointed cone* is defined to be a convex cone which contains `0`. This is a bundled version of
```

--- candidate 2 (sim=0.771, past_pr=#6437, file=Mathlib/Analysis/Convex/Cone/Pointed.lean) ---
PAST HUNK:
```
@@ -0,0 +1,260 @@
... [2 lines above hidden]
+Copyright (c) 2022 Apurva Nakade All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Apurva Nakade
+-/
+import Mathlib.Analysis.Convex.Cone.Dual
+import Mathlib.Algebra.Order.Nonneg.Ring
+import Mathlib.Algebra.Module.Submodule.Basic
+
+
+/-!
+# Pointed cones
+
+We define a pointed cones as convex cones which contain `0`. This is a bundled version of
```
PAST COMMENT (from reviewer):
That still doesn't read right 🤔

--- candidate 3 (sim=0.765, past_pr=#28140, file=Mathlib/Geometry/Convex/Cone/Pointed.lean) ---
PAST HUNK:
```
@@ -34,7 +34,7 @@ open Function
 section Definitions
 
 variable [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E]
-  {C C₁ C₂ : PointedCone R E} {x : E} {r : R}
+  {C C₁ C₂ : PointedCone R E} {S : Set E} {x : E} {r : R}
```
PAST COMMENT (from reviewer):
I think the variable name `S` is quite confusing here because you have `R` as well, which has a very different meaning! What do you think about `s` (as used in Cone/Dual)?

--- candidate 4 (sim=0.741, past_pr=#33780, file=Mathlib/Geometry/Convex/Cone/Pointed.lean) ---
PAST HUNK:
```
@@ -287,6 +290,44 @@ lemma to_isOrderedModule (C : PointedCone R E) (h : ∀ x y : E, x ≤ y ↔ y -
 
 end OrderedAddCommGroup
 
+section Lineal
+
+open Pointwise
+
+variable [Ring R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup E] [Module R E]
+
+/-- The lineality space of a cone `C` is the submodule given by `C ⊓ -C`. -/
+def lineal (C : PointedCone R E) : Submodule R E where
+  __ := C.toAddSubmonoid.support
```
PAST COMMENT (from reviewer):
```suggestion
  __ := C.support
```

--- candidate 5 (sim=0.741, past_pr=#33780, file=Mathlib/Geometry/Convex/Cone/Pointed.lean) ---
PAST HUNK:
```
@@ -287,6 +290,45 @@ lemma to_isOrderedModule (C : PointedCone R E) (h : ∀ x y : E, x ≤ y ↔ y -
... [7 lines above hidden]
+
+variable [Ring R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup E] [Module R E]
+
+/-- The lineality space of a cone `C` is the submodule given by `C ⊓ -C`. -/
+@[simps!]
+def lineal (C : PointedCone R E) : Submodule R E where
+  __ := C.support
+  smul_mem' r _ hx := by
+    by_cases hr : 0 ≤ r
+    · simpa using And.intro (C.smul_mem hr hx.1) (C.smul_mem hr hx.2)
+    · have hr := le_of_lt <| neg_pos_of_neg <| lt_of_not_ge hr
+      simpa using And.intro (C.smul_mem hr hx.2) (C.smul_mem hr hx.1)
+@[simp]
```
PAST COMMENT (from reviewer):
```suggestion

@[simp]
```

--- candidate 6 (sim=0.741, past_pr=#27578, file=Mathlib/Geometry/Convex/Cone/Pointed.lean) ---
PAST HUNK:
```
@@ -105,6 +112,16 @@ abbrev span (s : Set E) : PointedCone R E := Submodule.span R≥0 s
 
 lemma subset_span {s : Set E} : s ⊆ PointedCone.span R s := Submodule.subset_span
 
+/-- Elements of PointedCone.span R s are expressible as conical combination of elements from s. -/
```
PAST COMMENT (from reviewer):
```suggestion
/-- Elements of the cone hull are expressible as conical combination of elements from s. -/
```


--- candidate 7 (sim=0.734, past_pr=#25204, file=Mathlib/Analysis/Convex/Cone/Proper.lean) ---
PAST HUNK:
```
@@ -30,77 +32,107 @@ The next steps are:
... [42 lines above hidden]
 
-instance : Coe (ProperCone 𝕜 E) (PointedCone 𝕜 E) :=
-  ⟨toPointedCone⟩
+-- TODO: add `ConvexConeClass` that extends `SetLike` and replace the below instance
+instance : SetLike (ProperCone R E) E where
+  coe C := C.carrier
+  coe_injective' _ _ h := ProperCone.toPointedCone_injective <| SetLike.coe_injective h
 
-theorem toPointedCone_injective : Function.Injective ((↑) : ProperCone 𝕜 E → PointedCone 𝕜 E) :=
-  fun S T h => by cases S; cases T; congr
+@[ext] lemma ext (h : ∀ x, x ∈ C₁ ↔ x ∈ C₂) : C₁ = C₂ := SetLike.ext h
 
--- TODO: add `ConvexConeClass` that extends `SetLike` and replace the below instance
-instance : SetLike (ProperCone 𝕜 E) E where
-  coe K := K.carrier
-  coe_injective' _ _ h := ProperCone.toPointedCone_injective (SetLike.coe_injective h)
+@[simp] lemma mem_toPointedCone : x ∈ C.toPointedCone ↔ x ∈ C := .rfl
```
PAST COMMENT (from reviewer):
`mem_coe` makes more sense as the name for this, since in the infoview it'll get printed as a coercion (this is also consistent with the old way)

--- candidate 8 (sim=0.734, past_pr=#25204, file=Mathlib/Analysis/Convex/Cone/Proper.lean) ---
PAST HUNK:
```
@@ -30,77 +32,107 @@ The next steps are:
... [42 lines above hidden]
 
-instance : Coe (ProperCone 𝕜 E) (PointedCone 𝕜 E) :=
-  ⟨toPointedCone⟩
+-- TODO: add `ConvexConeClass` that extends `SetLike` and replace the below instance
+instance : SetLike (ProperCone R E) E where
+  coe C := C.carrier
+  coe_injective' _ _ h := ProperCone.toPointedCone_injective <| SetLike.coe_injective h
 
-theorem toPointedCone_injective : Function.Injective ((↑) : ProperCone 𝕜 E → PointedCone 𝕜 E) :=
-  fun S T h => by cases S; cases T; congr
+@[ext] lemma ext (h : ∀ x, x ∈ C₁ ↔ x ∈ C₂) : C₁ = C₂ := SetLike.ext h
 
--- TODO: add `ConvexConeClass` that extends `SetLike` and replace the below instance
-instance : SetLike (ProperCone 𝕜 E) E where
-  coe K := K.carrier
-  coe_injective' _ _ h := ProperCone.toPointedCone_injective (SetLike.coe_injective h)
+@[simp] lemma mem_toPointedCone : x ∈ C.toPointedCone ↔ x ∈ C := .rfl
```
PAST COMMENT (from reviewer):
that's a good enough reason. don't forget to deprecate though

--- candidate 9 (sim=0.733, past_pr=#29950, file=Mathlib/Analysis/Convex/Extreme.lean) ---
PAST HUNK:
```
@@ -49,32 +49,37 @@ variable (𝕜) [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜
 
 /-- A set `B` is an extreme subset of `A` if `B ⊆ A` and all points of `B` only belong to open
 segments whose ends are in `B`. -/
```
PAST COMMENT (from reviewer):
```suggestion
/-- A set `B` is an extreme subset of `A` if `B ⊆ A` and all points of `B` only belong to open
segments whose ends are in `B`.

Our definition only requires that the left endpoint of the segment lies in `B`,
but by symmetry of open segments, the right endpoint must also lie in `B`.
See `IsExtreme.right_mem_of_mem_openSegment`. -/
```

--- candidate 10 (sim=0.728, past_pr=#31648, file=Mathlib/Geometry/Convex/Cone/Pointed.lean) ---
PAST HUNK:
```
@@ -221,4 +222,22 @@ lemma to_isOrderedModule (C : PointedCone R E) (h : ∀ x y : E, x ≤ y ↔ y -
     IsOrderedModule R E := .of_smul_nonneg <| by simp +contextual [h, C.smul_mem]
 
 end OrderedAddCommGroup
+
+section Salient
+variable [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup E] [Module R E]
+open Pointwise
+
+/-- A pointed cone is salient iff an element `x` being a member of both the cone and its negative
+is equivalent to `x = 0`. -/
+lemma salient_iff_mem_neg_eq_zero (C : PointedCone R E) :
+    (C : ConvexCone R E).Salient ↔ ∀ x, (x ∈ C ∧ x ∈ -C) ↔ x = 0 := by
```
PAST COMMENT (from reviewer):
Okay, sure, remove the version I suggested.

--- candidate 11 (sim=0.728, past_pr=#31648, file=Mathlib/Geometry/Convex/Cone/Pointed.lean) ---
PAST HUNK:
```
@@ -221,4 +222,22 @@ lemma to_isOrderedModule (C : PointedCone R E) (h : ∀ x y : E, x ≤ y ↔ y -
     IsOrderedModule R E := .of_smul_nonneg <| by simp +contextual [h, C.smul_mem]
 
 end OrderedAddCommGroup
+
+section Salient
+variable [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup E] [Module R E]
+open Pointwise
+
+/-- A pointed cone is salient iff an element `x` being a member of both the cone and its negative
+is equivalent to `x = 0`. -/
+lemma salient_iff_mem_neg_eq_zero (C : PointedCone R E) :
+    (C : ConvexCone R E).Salient ↔ ∀ x, (x ∈ C ∧ x ∈ -C) ↔ x = 0 := by
```
PAST COMMENT (from reviewer):
Probably this is more useful in practice, no? As otherwise you end up constantly needing to prove the trivial fact that `0 ∈ C ∧ 0 ∈ -C`.
```suggestion
    (C : ConvexCone R E).Salient ↔ ∀ x, (x ∈ C ∧ x ∈ -C) → x = 0 := by
```
Do you also want to have an `alias` for the reverse direction?

--- candidate 12 (sim=0.725, past_pr=#29241, file=Mathlib/Analysis/Convex/Cone/Basic.lean) ---
PAST HUNK:
```
@@ -80,8 +80,6 @@ instance : SetLike (ProperCone R E) E where
 
 @[ext] lemma ext (h : ∀ x, x ∈ C₁ ↔ x ∈ C₂) : C₁ = C₂ := SetLike.ext h
 
-@[simp] lemma mem_toPointedCone : x ∈ C.toPointedCone ↔ x ∈ C := .rfl
```
PAST COMMENT (from reviewer):
I'd keep the lemma (because it's more easily discoverable than something on closed submodules) but remove the simp attribute.

--- candidate 13 (sim=0.725, past_pr=#29241, file=Mathlib/Analysis/Convex/Cone/Basic.lean) ---
PAST HUNK:
```
@@ -80,8 +80,6 @@ instance : SetLike (ProperCone R E) E where
 
 @[ext] lemma ext (h : ∀ x, x ∈ C₁ ↔ x ∈ C₂) : C₁ = C₂ := SetLike.ext h
 
-@[simp] lemma mem_toPointedCone : x ∈ C.toPointedCone ↔ x ∈ C := .rfl
```
PAST COMMENT (from reviewer):
I'm not sure it is the role of this PR to do this change and the next one. Remove the changes?

--- candidate 14 (sim=0.719, past_pr=#27578, file=Mathlib/Geometry/Convex/Cone/Pointed.lean) ---
PAST HUNK:
```
@@ -105,6 +112,15 @@ abbrev span (s : Set E) : PointedCone R E := Submodule.span R≥0 s
 
 lemma subset_span {s : Set E} : s ⊆ PointedCone.span R s := Submodule.subset_span
 
+/-- Elements of PointedCone.span R s are expressible as conical combination of elements from s. -/
+lemma mem_span_set {s : Set E} : x ∈ span R s ↔
+      ∃ c : E →₀ R, ↑c.support ⊆ s ∧ (∀ y, 0 ≤ c y) ∧ c.sum (fun m r => r • m) = x := by
+  rw [Submodule.mem_span_set]
+  constructor
+  · rintro ⟨c, hc, rfl⟩
+    exact ⟨⟨c.support, Subtype.val ∘ c, by simp [← Subtype.val_inj]⟩, hc, fun y ↦ (c y).2, rfl⟩
+  · rintro ⟨c, hc, hc₀, rfl⟩
+    exact ⟨⟨c.support, fun y ↦ ⟨c y, hc₀ _⟩, by simp⟩, hc, rfl⟩
```
PAST COMMENT (from reviewer):
```suggestion
    exact ⟨⟨c.support, fun y ↦ ⟨c y, hc₀ _⟩, by simp⟩, hc, rfl⟩

```

--- candidate 15 (sim=0.718, past_pr=#20595, file=Mathlib/Analysis/Convex/Cone/Basic.lean) ---
PAST HUNK:
```
@@ -48,11 +48,12 @@ variable {𝕜 E F G : Type*}
 section Definitions
 
 variable (𝕜 E)
-variable [OrderedSemiring 𝕜]
+variable [Semiring 𝕜] [PartialOrder 𝕜]
 
 /-- A convex cone is a subset `s` of a `𝕜`-module such that `a • x + b • y ∈ s` whenever `a, b > 0`
 and `x, y ∈ s`. -/
-structure ConvexCone [AddCommMonoid E] [SMul 𝕜 E] where
+@[nolint unusedArguments]
```
PAST COMMENT (from reviewer):
```suggestion
```
I don't think this is needed?

--- candidate 16 (sim=0.715, past_pr=#35308, file=Mathlib/Geometry/Convex/Cone/Pointed.lean) ---
PAST HUNK:
```
@@ -35,10 +35,55 @@ namespace PointedCone
... [4 lines above hidden]
-section Definitions
+section Submodule
 
 variable [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E]
-  {C C₁ C₂ : PointedCone R E} {x : E} {r : R}
+variable {C : PointedCone R E}
+
+/-- A submodule is a pointed cone. -/
+@[coe] abbrev ofSubmodule (S : Submodule R E) : PointedCone R E := S.restrictScalars _
+
+instance : Coe (Submodule R E) (PointedCone R E) := ⟨ofSubmodule⟩
+
+@[simp] lemma ofSubmodule_coe (S : Submodule R E) : (ofSubmodule S : Set E) = S := by rfl
```
PAST COMMENT (from reviewer):
```suggestion
@[simp] lemma coe_ofSubmodule (S : Submodule R E) : (ofSubmodule S : Set E) = S := rfl
```

--- candidate 17 (sim=0.712, past_pr=#36953, file=Mathlib/Geometry/Convex/Cone/Pointed.lean) ---
PAST HUNK:
```
@@ -170,18 +170,18 @@ def ofConeComb (C : Set E) (nonempty : C.Nonempty)
... [3 lines above hidden]
 variable (R) in
-/-- The span of a set `s` is the smallest pointed cone that contains `s`.
+/-- The cone hull of a set `s` is the smallest pointed cone that contains `s`.
 
-Pointed cones being defined as submodules over nonnegative scalars, this is exactly the
-submodule span of `s` w.r.t. nonnegative scalars. -/
-abbrev span (s : Set E) : PointedCone R E := Submodule.span R≥0 s
+Pointed cones being defined as submodules over nonnegative scalars, this is implemented as
+the submodule span of `s` w.r.t. nonnegative scalars. -/
+abbrev hull (s : Set E) : PointedCone R E := span R≥0 s
 
-lemma subset_span {s : Set E} : s ⊆ PointedCone.span R s := Submodule.subset_span
+lemma subset_hull {s : Set E} : s ⊆ PointedCone.hull R s := subset_span
```
PAST COMMENT (from reviewer):
It's OK to not deprecated `span`.

--- candidate 18 (sim=0.712, past_pr=#36953, file=Mathlib/Geometry/Convex/Cone/Pointed.lean) ---
PAST HUNK:
```
@@ -170,18 +170,18 @@ def ofConeComb (C : Set E) (nonempty : C.Nonempty)
... [3 lines above hidden]
 variable (R) in
-/-- The span of a set `s` is the smallest pointed cone that contains `s`.
+/-- The cone hull of a set `s` is the smallest pointed cone that contains `s`.
 
-Pointed cones being defined as submodules over nonnegative scalars, this is exactly the
-submodule span of `s` w.r.t. nonnegative scalars. -/
-abbrev span (s : Set E) : PointedCone R E := Submodule.span R≥0 s
+Pointed cones being defined as submodules over nonnegative scalars, this is implemented as
+the submodule span of `s` w.r.t. nonnegative scalars. -/
+abbrev hull (s : Set E) : PointedCone R E := span R≥0 s
 
-lemma subset_span {s : Set E} : s ⊆ PointedCone.span R s := Submodule.subset_span
+lemma subset_hull {s : Set E} : s ⊆ PointedCone.hull R s := subset_span
```
PAST COMMENT (from reviewer):
Same here. We want deprecations for all declarations that changed the name

--- candidate 19 (sim=0.710, past_pr=#32355, file=Mathlib/Geometry/Convex/Cone/Simplicial.lean) ---
PAST HUNK:
```
@@ -0,0 +1,117 @@
... [41 lines above hidden]
+## References
+
+* [de Bruyn *Tensor products of convex cones*][https://arxiv.org/abs/2009.11843v2]
+
+-/
+
+@[expose] public section
+
+variable {R M : Type*}
+variable [Semiring R] [PartialOrder R] [IsOrderedRing R]
+variable [AddCommMonoid M] [Module R M]
+
+local notation3 "R≥0" => {c : R // 0 ≤ c}
```
PAST COMMENT (from reviewer):
hmm yeah not sure what to do either but the current approach doesn't scale
I suppose we can leave it for a future PR

--- candidate 20 (sim=0.710, past_pr=#32355, file=Mathlib/Geometry/Convex/Cone/Simplicial.lean) ---
PAST HUNK:
```
@@ -0,0 +1,117 @@
... [41 lines above hidden]
+## References
+
+* [de Bruyn *Tensor products of convex cones*][https://arxiv.org/abs/2009.11843v2]
+
+-/
+
+@[expose] public section
+
+variable {R M : Type*}
+variable [Semiring R] [PartialOrder R] [IsOrderedRing R]
+variable [AddCommMonoid M] [Module R M]
+
+local notation3 "R≥0" => {c : R // 0 ≤ c}
```
PAST COMMENT (from reviewer):
This notation line appears already in several files - could you consider refactoring it into scoped notation in the `PointedCone` namespace?


Decide which candidates' comments genuinely apply to the NEW hunk. If none, say so. Output JSON only.

[ASSISTANT]
----------------------------------------------------------------------------------------------------
{
  "new_hunk_plausible_concerns": [
    "docstring",
    "naming",
    "style-syntax",
    "imports-module",
    "design-smell-architectural"
  ],
  "summary": "The new hunk's docstrings and variable declarations could be refined, and its architectural choices like `@[expose] public section` might warrant discussion.",
  "confidence": "medium",
  "strong_matches": [
    {
      "past_pr": 6437,
      "past_file": "Mathlib/Analysis/Convex/Cone/Pointed.lean",
      "past_concern_axis": "docstring",
      "past_comment_excerpt": "A *pointed cone* is defined to be a convex cone which contains `0`. This is a bundled version of",
      "applies_because": "The new hunk defines `IsFaceOf` with a docstring that could be made more precise or formal, similar to the suggested rephrasing for 'Pointed cone'. The specific definition of a face given in the docstring could be expanded for clarity.",
      "suggested_adaptation": "Consider refining the docstring for `IsFaceOf` to explicitly state 'A face of a pointed cone `F` is defined to be...' and elaborate slightly on the conditions, possibly noting the asymmetry if relevant.",
      "why_might_not_apply": "The existing docstring for `IsFaceOf` is already quite clear and provides sufficient information for a definition."
    },
    {
      "past_pr": 28140,
      "past_file": "Mathlib/Geometry/Convex/Cone/Pointed.lean",
      "past_concern_axis": "naming",
      "past_comment_excerpt": "I think the variable name `S` is quite confusing here because you have `R` as well, which has a very different meaning! What do you think about `s` (as used in Cone/Dual)?",
      "applies_because": "The new hunk's `variable` declaration includes `N : Type*` which is not used in the `IsFaceOf` definition, potentially introducing an unused or confusing variable, mirroring the concern about 'S' in the past comment.",
      "suggested_adaptation": "Consider if the `N : Type*` variable is strictly necessary in this `variable` block, or if it could be moved to a more specific scope where it is actually used.",
      "why_might_not_apply": "The `N` variable might be used in other definitions within the same `public section` not visible in the hunk, making its declaration appropriate for the broader scope."
    },
    {
      "past_pr": 29950,
      "past_file": "Mathlib/Analysis/Convex/Extreme.lean",
      "past_concern_axis": "docstring",
      "past_comment_excerpt": "Our definition only requires that the left endpoint of the segment lies in `B`, but by symmetry of open segments, the right endpoint must also lie in `B`.",
      "applies_because": "The definition of `IsFaceOf` in the new hunk involves an asymmetric condition on `x` and `y` (`a • x + y` in `F` implies `x` in `F`), and the past comment suggests adding clarification about implicit properties or symmetry to a related definition (`IsExtreme`). This suggests the new docstring could also benefit from similar detail or a note on this asymmetry.",
      "suggested_adaptation": "Given the asymmetric condition on `x` and `y` in the definition of `IsFaceOf`, consider adding a note to the docstring or implementation notes discussing its implications or if `y` is also implicitly included.",
      "why_might_not_apply": "The implementation notes already touch upon the relation to `IsExtreme` and the choice of definition, which might implicitly address some of these concerns."
    }
  ],
  "weak_observations": [
    {
      "observation": "The note about `iff_mem_of_add_mem` holding more generally over an Archimedean ring in the implementation notes suggests future lemmas might need careful consideration of typeclass generalization, similar to a past comment on simplifying lemma statements by weakening assumptions.",
      "axis": "generalize-signature",
      "supporting_past_prs": [
        31648
      ]
    },
    {
      "observation": "The use of `@[expose] public section` and `public import` are specific stylistic choices that might lead to discussions about design patterns or refactoring, similar to past comments regarding the scalability of `local notation3 R≥0`.",
      "axis": "style-syntax",
      "supporting_past_prs": [
        32355
      ]
    }
  ]
}