Philippe Thomas Savard (Jan 28 2026 at 05:39): Philippe Thomas Savard (Jan 28 2026 at 05:39):Hello everyone,
I am working on an Isabelle theory and I am facing two small errors that I cannot resolve. I would be grateful for any help or suggestions.
The first issue appears in the following lemma:
lemma infinitely_many_half_ratios: "(n. philippot_term (Suc n) / philippot_term n = (1 / 2 :: rat))" using philippot_ratio_half by simp
In VS Code, the part "by simp" is marked in red, even though the lemma looks correct. I suspect there may be an invisible character or some subtle syntax problem, but I cannot find it.
The second issue concerns the definition of spectral_sum. I want it to be written in a simple and standard way, without any special symbols. Here is the version I am currently using:
definition spectral_sum :: "nat list => rat" where "spectral_sum L = (SUM n <- L. of_nat n)"
I am not sure if this is the correct or idiomatic form.
I have attached a zip file containing my updated theory.
Thank you very much for your time and help.
Phil
geometrie_spectre_premier_savard.zip
Last updated: Feb 12 2026 at 20:37 UTC