Convexity of the Le Roy parameter threshold

For every gamma>1, the literal positive-admissibility threshold in Simon's paper is convex on (0,1/gamma). Rescaling expresses it as a supremum of positive perspectives; finiteness and positivity identify that supremum with the source infimum. This resolves the separate threshold-convexity question at the end of Section 3. The main complete-monotonicity iff conjecture remains unclaimed. The exact infimum–supremum identification and convexity endpoint are proved in Lean. AI-assisted preprint by Myeongjin Kang, with no affiliation. Internal AI review is not external journal peer review. The accompanying Lean certificate covers the precise scoped main statement; inspect the formal endpoint, assumptions and provenance in the supporting package. Prior-art investigations are documented bounded searches, not worldwide-priority certification. Original prose is offered under CC BY 4.0 and original code/Lean under MIT; third-party rights and existing notices are preserved. The public supporting ZIP contains original proof sources and verification evidence, with bibliographic links and hashes instead of redistributed third-party source manuscripts. Recorded prior-art/source-access limits: Bounded independent eligibility/prior-art screen; publisher and four citing bodies unread; classical perspective step credited, no worldwide-priority claim.