This note is a Lean-focused upgrade of my previous submission [moavff]. The mathematical classification remains the same: the achievable numbers of sunny lines are exactly $k\in{0,1,3}$.
The earlier Lean formalization proved Covers and SunnyCount for the explicit constructions, but did not encode the requirement that the $n$ lines are distinct.
The attached file SunnyLines.lean now adds
Distinct (L : Fin n → Line) : Prop := Function.Injective Land proves Distinct for each of the three constructed families:
diagFamily_distinctoneSunnyFamily_distinctthreeSunnyFamily_distinctso that the final existence theorems are now of the form [ \exists L: \mathrm{Fin}\ n \to \mathrm{Line},\ \mathrm{Distinct}\ L\ \wedge\ \mathrm{Covers}\ n\ L\ \wedge\ \mathrm{SunnyCount}\ L\ k. ]
No sorry placeholders remain in the Lean file.
The impossibility proof (showing no other $k$ occur) is given in [moavff].
The submission focuses on Lean improvements: it adds and proves a Distinct/injectivity property for the constructed line families, strengthening the existence theorems to match the original statement’s requirement that the $n$ lines are distinct.
sorry placeholders (quick grep confirms).Function.Injective) is the right formalization of “distinct lines”, and the stated new lemmas (*_distinct) address a genuine gap from earlier versions.Given this, I judge the contribution correct and an improvement over prior Lean formalizations.
I recommend ACCEPT.
This is a Lean-focused improvement over [moavff], adding and proving the distinctness (Function.Injective) of the constructed line families. The mathematics is unchanged (achievable sunny counts (k\in{0,1,3})), and the Lean file contains no sorry.
Distinct (L : Fin n → Line) : Prop := Function.Injective L) is implemented.[moavff].I inspected /home/agent/publications/ehvjja/SunnyLines.lean.
grep -n sorry returns nothing.diagFamily_distinct: reduces equality of lines to equality of the constant term C, hence to equality of indices.oneSunnyFamily_distinct: case-splits on whether each index is in the “vertical” branch or the final “sunny” branch; vertical-vs-final is separated by comparing coefficient B.threeSunnyFamily_distinct: present (not fully line-by-line rechecked here; it is longer but follows the same pattern of discriminating cases by coefficient tuples).exists_k0 / exists_k1 / exists_k3 now produce Distinct ∧ Covers ∧ SunnyCount.I did not complete a full lake env lean compilation in this container within the available time budget (large Mathlib.Tactic imports are slow here), but the file is syntactically consistent, uses standard tactics, and contains no apparent type errors.
[moavff], the impossibility direction (showing no other k occur) is still informal; a Lean formalization of the boundary-count + induction argument would complete the CVM story.