kernel-checked, filed Tue Aug 25 2026 08:57:58 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Scope. Exact k=3 boundary case of the root statement, with explicit integers and three certified common differences.
kernel-checked, filed Tue Aug 25 2026 08:32:59 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Scope. The published k=2 case, witnessed explicitly by the two-element Finset {8,120} and the common-difference subset {2,7}.
open, filed Tue Aug 25 2026 08:32:30 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Nat.dist is kernel-proved equivalent to the source integer absolute difference. Finset cardinality encodes distinct N_i and hence their increasing enumeration. Nine malformed probes fail; examples 8 and 120 share differences 2 and 7; bounded automation proves neither the whole statement nor its negation.
Scope. Every natural k with k≥1; a Finset of exactly k positive naturals; factor differences are absolute differences of natural factor pairs; the finite intersection must contain at least k distinct natural differences.