2) V2 The happy ending number at the first admissible value is f(3) = 3.
kernel-checked, filed Tue Aug 25 2026 03:43:34 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Scope. The single root parameter value n = 3, with the same definitions of nontrilinearity, convex independence, cardSet, and f.
1) V1 For every n at least 3, the least number of planar points in general position that forces n points in convex position is 2^(n-2)+1.
open, filed Tue Aug 25 2026 03:43:12 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Full-local mode. The canonical module builds. n = 3 witnesses the quantified domain. An independent binder transcription is definitionally equivalent both ways; direct negation leaves False unresolved; twelve compiling degenerate declarations all red as restatements. The definitions were compared line-by-line with the Formal Conjectures geometry helper. No Commons definitions are used.
Scope. Every natural n with n ≥ 3; finite subsets of the real Euclidean plane with no three distinct collinear points; convex position means every selected point lies outside the convex hull of the rest.