Primary domain: convex geometry of cone hulls in ℝ².

Relevant owner declarations sampled for this item:

• Metric.closedBall
• convex_closedBall
• ConvexCone.hull
• ConvexCone.subset_hull
• ConvexCone.mem_hull_of_convex

Best owner abstraction:

• the source-facing disk owner Q₁ from Definition_2_29
• the generated cone, expressed directly as hull ℝ Q₁

Primitive data:

• the imported disk owner Q₁
• the center e₁ = EuclideanSpace.single (0 : Fin 2) (1 : ℝ)

Derived API:

• mem_Q₁_iff for the defining disk inequality
• convex_closedBall for convexity of Q₁
• ConvexCone.mem_hull_of_convex for cone-hull membership over a convex source set

Source/core/bridge triage:

• source-facing: the proposition identifying the cone generated by Q₁
• core/canonical: the imported owner Q₁, EuclideanSpace.single, PointedCone.hull, ConvexCone.hull
• bridge/view: mem_Q₁_iff and the private equivalence between the pointed and convex cone hulls of Q₁

This refinement therefore reuses the owner file Definition_2_29 for the disk itself and keeps only the cone-hull geometry local to this proposition.

theorem cone_generated_by_Q1_eq_positive_first_coordinate_or_origin : ↑(PointedCone.hull ℝ Q₁) = {x : EuclideanSpace ℝ (Fin 2) | 0 < x.ofLp 0} ∪ {0}

Proposition 2.16: the cone generated by the closed unit disk centered at (1, 0) is exactly the set of points in ℝ² with strictly positive first coordinate together with the origin.