JOURNAL.md

JOURNAL

Session journal for this repository. Newest entry on top. One section per session, headed by the date. Bullets state what changed and why — not what was considered, and not what is planned. Plans belong in PLAN.md.

This journal ships empty, with one example entry below to show the shape. Delete the example when you write your first real entry.

Conventions:

• Reverse chronological. A new session is inserted directly under this header.
• Heading format: ## YYYY-MM-DD — short title.
• Each bullet is a change, in the past tense, with its reason attached. A bullet with no reason is a bullet that will be useless in three months, when the only thing you want back is why you chose what you chose.
• A result promoted into NtLean/ gets a bullet naming the declaration and the module.
• A decision that will bind future sessions gets a bullet here and an entry in MEMORY.md: the journal records when and why, MEMORY.md records the standing rule.
• Failures are worth recording. An attempt that was abandoned earns a bullet, and the reason it failed is usually the most valuable line in the entry. It is what stops the next session from spending an afternoon rediscovering the same wall — and in Lean the reason is often specific and reusable ("omega treats n / m as an opaque atom, so the div/mod relation is invisible to it").
• Keep the whole entry short enough that you would actually read it later. Five to ten bullets is a full session.

---

2026-08-08 — Chebyshev analogue of Fermat, and a package-name bug

• Added cheb_fermat, cheb_fermat_int and the supporting chebT_char to NtLean/Chebyshev.lean: for p an odd prime and any x, either T_{p-1}(x) ≡ 1 or T_{p+1}(x) ≡ 1 mod p. The key lemma T_p = X^p in characteristic p comes from Frobenius on the conic, (c+is)^p = c^p + i^p s^p, compared against the expansion z^p = T_p + i s U_p and separated by repr_unique. Vault: vault/Theorems/Chebyshev Fermat little theorem.md.
• Fixed a bug that made this repository unbuildable: lakefile.toml declared name = "lean-interact", and a hyphen is not a valid Lean identifier, so Lake refused the manifest with name: expected a 'Name', got '"lean-interact"' before doing any work. Renamed the package to lean_interact in lakefile.toml and lake-manifest.json. The repository directory, the tmux session and the GitHub project keep the hyphenated name; only the Lake package identifier had to change.
• Why it was missed. The port verified the Lean by elaborating each module against an already-built environment, which never reads lakefile.toml. lake build had never been run in a fresh clone. The lesson is that "every module compiles" and "the package builds" are different claims, and only the second one is what a new user experiences.

---

2026-01-01 — EXAMPLE ENTRY (delete this section)

Names are omitted below rather than invented: this file ships without a Lean toolchain attached, and the repository rule is that no Mathlib name appears anywhere until it has been verified. Your own entries should name the lemmas, once you have run them.

• Promoted the divisibility rule by 9 into NtLean/Divisibility.lean as NtLean.dvd_nine_iff_digitSum. Stated over ℕ rather than ℤ, because the informal sentence was about natural numbers and the ℕ form is the one that will be quoted later; the ℤ version is a corollary if it is ever wanted.
• The proof works in ZMod 9, where every power of ten is 1, so the digit-sum statement becomes a computation instead of an induction. Found the reduction lemma with tools/mlq.py --about "digits" and verified it before use; the names are recorded in the vault note.
• Failed first, and this is the useful part: an hour went into induction on n itself. The induction hypothesis is about n / 10, and relating the digit list of n to that of n / 10 is the lemma being proved, so the argument was circular. The digit-list recursion is the right induction; the numeric one is not.
• Tactic lesson: decide closes the fixed-modulus base cases instantly but is useless once the statement quantifies over n — it is only honest when the search space is genuinely finite. omega was no help either: it treats n / 10 as an opaque atom, so the div/mod relation it needed was invisible to it.
• Wrote the vault note under vault/Theorems/, with the informal sentence, the LaTeX, the final Lean, and links to the two related notes.
• Recorded a preference in MEMORY.md: results enter the library in whichever number system the informal sentence used, with conversions done inside the proof rather than in the statement.