[1athena]

Submission type

• Mathematical solver information
• Lean proof or formalization author information

Select both when applicable and remove sections that do not apply. Submit only
complete solutions and proof references, following the
submission requirements.
For claims, public review and challenges, see the
award process.

The complete mathematical solution and its proof or publication evidence may be
provided before the Lean formalization or together with it in this PR. The
mathematical solver and Lean formalization author may be different people.
A Lean submission without the mathematical solution and its supporting evidence
is invalid and will not be accepted. Link the earlier solution or provide it
and its evidence below.

We recommend checking open, merged and closed PRs for the same problem and
contribution type before submitting. Linking related PRs and explaining how your
contribution differs can help avoid duplicate work. See the
pre-submission suggestions.

Problem

• Problem ID(s): JSP-000448 (Erdős Problem JSP-000329: Lean proof of the easy bound g_k(n) ≪_k log n (Erdős #400) #448; https://www.erdosproblems.com/448)
• Original problem source and exact location (page, section or problem number): the catalog entry of record — https://github.com/TheJustinSunPrize/awards/blob/main/problems/catalog-0401-0500.md#JSP-000448 ("Does the multicolor Ramsey number of a tree grow linearly with its order?", Date proposed: no later than 1975, Current status: Solved). The underlying Erdős problem page is https://www.erdosproblems.com/448 .
• Current entry and proposed change: the Lean proof cell currently reads "Reported; standalone Lean source not located. … This does not establish separate formalization authorship for JSP-000448." Proposed change: replace that one cell with Yes — [Lean source](https://github.com/1athena/jsp-formalizations/blob/43e040362cb0cc1f46f65c21ebd74e3e6cbf5b62/JSP-000448/JSP000448.lean) plus the formalization-contributor line. No other field of the entry is changed. In particular Eligible to claim (currently Pending verification), Current status, Publication details and Public review are left exactly as they are for maintainer determination.
• Related issue, if any: none opened by this account for JSP-000448.
• Related PRs and how this contribution differs, including any issue found in an existing submission and supporting evidence: issue JSP-000448: register Lean formalization (plby/lean-proofs) #4224 (open, dcdreamy-code, 2026-09-23) registers a Lean formalization for JSP-000448 located at src/latest/ErdosProblems/Erdos448.lean in the third-party aggregate repository plby/lean-proofs @ 8822f7ddef30fadbd92e1c6ab4ed897af356af5e. The catalog was subsequently edited to "Reported; standalone Lean source not located", i.e. that registration does not by itself establish formalization authorship for JSP-000448. This submission differs in the specific respect the catalog flags: it supplies a standalone Lean source in an original, self-owned repository (1athena/jsp-formalizations, created 2026-09-17T17:41:56Z, not a fork, not an aggregate of third-party proofs), whose single pinned external dependency is disclosed below with its licence and provenance. We do not ask for JSP-000448: register Lean formalization (plby/lean-proofs) #4224 to be closed; we only supply the missing standalone source.

Earlier independent registration (disclosed for completeness): issue #569 (open, zhangjun725, created 2026-09-17T07:31:33Z) and its companion PR #574 register a standalone Lean formalization of JSP-000448 in the original repository zhangjun725/erdos557 @ c4e0ab13027f8bb50defade11cf8a53c7b8b0ba9 (Apache-2.0), reporting Erdos557.erdos_557 and Erdos557.erdos_557_explicit and a tight-constant variant, derived from the same pinned dependency tadamcz/erdos548 @ 82ffb751f3d3776… that this submission also uses. That registration predates this PR by about nine days; this account makes no priority claim over it and does not ask for #569/#574 to be closed. This submission is an independent, separately authored formalization of the same linear bound (R_r(T_{k+1}) \u2264 r\u00b7k + 2, theorem JSP000448.multicolor_tree_ramsey_linear) in a distinct self-owned repository; if the maintainers regard #569/#574 as sufficient, this PR can be closed as duplicate without objection from this account.

• For solver/publication updates: not applicable — no solver or publication field is changed by this PR.

Formal statement

For Lean contributions only. Repeat the theorem details for each problem.

• Complete mathematical solution (provided earlier or in this PR): provided earlier, in the catalog entry itself — Publication details: [ReSt26] The Erdős-Sós conjecture in dense graphs — arXiv:2609.05417 (2026). The mathematical solution is not claimed by this account; this account claims only the Lean formalization.
• Mathematical review reference or current review status: per the catalog entry, Public review = "Unverified: no public recognition specifically identifying this result was found". This PR does not change that field.
• Formal statement location, pinned to a full commit SHA: https://github.com/1athena/jsp-formalizations/blob/43e040362cb0cc1f46f65c21ebd74e3e6cbf5b62/JSP-000448/JSP000448.lean (theorem multicolor_tree_ramsey_linear, lines 145–152 of the file at that commit)
• Fully qualified target theorem name: JSP000448.multicolor_tree_ramsey_linear
• Statement origin (maintainer-approved reference and version, or proposed statement requiring review): proposed statement requiring review. There is no maintainer-approved formal statement for JSP-000448; the statement below is a direct formal reading of the catalog's own question and of the catalog's own note that the problem "derives … from the tree-embedding result in JSP-000439".

theorem multicolor_tree_ramsey_linear (r k : ℕ) (hr : 0 < r) :
    ∀ c : Sym2 (Fin (r * k + 2)) → Fin r,
      ∃ i : Fin r, ∀ T : SimpleGraph (Fin (k + 1)),
        T.IsTree → T.IsContained (colorClassGraph c i)

• Correspondence to the original problem: definitions, assumptions, quantifiers, conclusion and all required cases; explain any differences from an approved statement.
  • r is the number of colours (Fin r, hr : 0 < r excludes the empty palette).
  • c : Sym2 (Fin (r*k+2)) → Fin r is an arbitrary r-colouring of the edges of the complete graph on N = r*k+2 vertices (Sym2 = unordered pairs, so this is exactly an edge colouring of K_N).
  • colorClassGraph c i is the i-th colour class, i.e. the graph on the same N vertices whose edges are precisely the edges of colour i.
  • T : SimpleGraph (Fin (k+1)), T.IsTree, T.IsContained G — every tree on k+1 vertices appears as a (not necessarily induced) subgraph of the colour class.
  • Conclusion: for every colouring c there is a colour i containing every tree on k+1 vertices. In standard notation this is R_r(T_{k+1}) ≤ r*k + 2 for every r ≥ 1, i.e. the r-colour Ramsey number of a tree grows at most linearly in its order (with slope r and a constant term 2).
  • Differences from the informal problem: (a) the informal question is qualitative ("grows linearly"); we formalize the stronger, quantitative upper bound r*k+2, which answers the question in the affirmative; (b) we do not formalize any lower bound or any sharp constant, and we claim no optimality; (c) the bound is uniform in the tree (all trees on k+1 vertices at once), which is the standard reading of R_r(T) for trees.
  • The proof reduces to the Erdős–Sós tree-embedding theorem for JSP-000439, exactly as the catalog's own commentary suggests, via a pigeonhole argument on the colour classes of K_N.

Proof submission

For Lean contributions only. Use the original repository containing your
contribution, owned by your submitting account or an organization. For an
organization repository, supply verifiable contribution evidence under Attribution.
Link the proof; do not commit Lean source here.
Add an object for each additional repository/version.

[
  {
    "repository": "https://github.com/1athena/jsp-formalizations",
    "branch": "main",
    "commit": "43e040362cb0cc1f46f65c21ebd74e3e6cbf5b62"
  }
]

• Proof file at the selected commit and fully qualified theorem name: JSP-000448/JSP000448.lean → JSP000448.multicolor_tree_ramsey_linear (committed 2026-09-25T17:40:20Z).
• How the proof establishes the formal statement above, including any separate verification entry:
  1. colorClass_edgeFinset_eq — the colour classes are exactly the fibres of c over the edge set of ⊤ : SimpleGraph (Fin N).
  2. sum_colorClass_edges — hence ∑ i, |E(G_i)| = |E(K_N)|, proved by Finset extensionality and Finset.card_eq_sum_card_fiberwise.
  3. exists_colorClass_large — pigeonhole: some colour class has at least |E(K_N)| / r edges.
  4. card_edgeFinset_top_eq_card_choose_two + cast_choose_two — that quantity is N.choose 2 / r.
  5. arithmetic_core — for N = r*k+2, ((k-1)/2)*N + 1 ≤ N.choose 2 / r (a rational arithmetic inequality, closed by field_simp, ring_nf, nlinarith).
  6. Erdos548.erdos_548 (Erdős–Sós, JSP-000439) converts the edge count of that one colour class into a copy of every tree on k+1 vertices.
     Third-party dependency (the only one): Erdos548_192usd_21h.lean, the Erdős–Sós formalization of Tom Adamczewski, Apache-2.0, from https://github.com/tadamcz/erdos548 @ 82ffb751f3d37768927df9239ed08439bbe0dd09, vendored verbatim except for three mechanical API-drift fixes required by Lean 4.35 / current mathlib (enumerated in JSP-000448/PATCHES.md in the same commit); no mathematical change was made to it.

Reproduction

For Lean contributions only.

• Exact Lean version and lean-toolchain path: leanprover/lean4:v4.35.0-rc2, declared in JSP-000448/lean-toolchain at the pinned commit.
• Pinned dependencies (including mathlib, if used) and manifest path: mathlib leanprover-community/mathlib4 @ 44ba35c6daa9d69aff8fed9fff9bbde17ded774d, pinned in JSP-000448/lakefile.lean; the resolved dependency set is recorded in JSP-000448/lake-manifest.json at the pinned commit. The only non-mathlib Lean input is the vendored Erdős–Sós file above.
• Build instructions pinned to the selected commit (two equivalent routes; route A was the one actually executed and is the basis of this submission):

# --- Route A: kernel check against a mathlib build cache at the pinned revision ---
git clone https://github.com/1athena/jsp-formalizations.git
cd jsp-formalizations
git checkout 43e040362cb0cc1f46f65c21ebd74e3e6cbf5b62
cd JSP-000448
git status                       # clean, HEAD = 43e040362cb0cc1f46f65c21ebd74e3e6cbf5b62
# mathlib4 checked out at 44ba35c6daa9d69aff8fed9fff9bbde17ded774d and built once elsewhere:
export LEAN_PATH="<mathlib4>/.lake/build/lib/lean:<mathlib4>/.lake/packages/*/.lake/build/lib/lean"
lean --version                                              # Lean (version 4.35.0-rc2, ...)
lean -o Erdos548_192usd_21h.olean Erdos548_192usd_21h.lean  # exit 0 (47 deprecation warnings, vendored file)
lean -o JSP000448.olean JSP000448.lean                      # exit 0, 0 errors, 0 warnings

# --- Route B: lake route (rebuilds mathlib from source; ~2h on 8 cores) ---
lake --version                   # Lake 5.0.0-src+11acb17 (Lean version 4.35.0-rc2)
lake build +Erdos548_192usd_21h
lake build +JSP000448
lake env lean JSP000448.lean

• Commands for setup, clean build and checking each target theorem; include a separate statement-to-proof check if needed: route A above was executed in a clean clone (git status clean, HEAD equal to the pinned commit); both lean -o invocations exited 0. Statement-to-proof check (separate audit module — the same module the lean-verify skill generates):

cat > Audit0000.lean <<'EOF'
import JSP000448

set_option pp.all true
#check @JSP000448.multicolor_tree_ramsey_linear
#print JSP000448.multicolor_tree_ramsey_linear
set_option pp.universes false in
#print axioms JSP000448.multicolor_tree_ramsey_linear
EOF
lean Audit0000.lean                   # with the same LEAN_PATH and the two .olean files above

• Axiom audit command and output for each target:

$ lean Audit0000.lean
'JSP000448.multicolor_tree_ramsey_linear' depends on axioms: [propext, Classical.choice, Quot.sound]

propext, Classical.choice and Quot.sound are the three standard axioms of Lean's logic. The file contains no sorry, no admit, no unsafe, no implemented_by, no extern and no native_decide; this was checked by textual inspection and is confirmed by the axiom output above (which does not list sorryAx).

Pre-submission Lean verification

We recommend the lean-verify skill
for Lean proofs. You may use another method or omit this section.

This section is optional under the current rules (see
docs/verification.md.

• Method/tool and version, if available: direct Lean kernel check with leanprover/lean4:v4.35.0-rc2 (Lean 4.35.0-rc2, arm64-apple-darwin24.6.0), mathlib 44ba35c6daa9d69aff8fed9fff9bbde17ded774d, in a clean git clone of the repository below. The repository's own lean-verify skill was not used for this submission; a separate run of skills/lean-verify/scripts/audit.py against the same commit is being executed as additional supporting evidence and its report will be posted as a follow-up comment (it requires a full mathlib rebuild from source, roughly two hours on this machine).
• Checked repository and full commit SHA; identify any difference from the submitted version: https://github.com/1athena/jsp-formalizations @ 43e040362cb0cc1f46f65c21ebd74e3e6cbf5b62 — identical to the submitted version, no difference.
• Verification date, actual conclusion and limitations: checked 2026-09-25 and re-checked 2026-09-26 in a fresh clone; conclusion: both modules compile with the pinned toolchain (exit 0), the target compiles with 0 errors and 0 warnings, and the target depends only on [propext, Classical.choice, Quot.sound]. Limitations: this is a mechanical kernel check, not a mathematical verdict; statement correspondence (does the formal statement capture the intended problem?) is argued above but is ultimately for maintainer review; the bound proved is the explicit R_r(T_{k+1}) ≤ r*k+2, no sharpness or lower bound is claimed; the Erdős–Sós dependency is trusted as a pinned, Apache-2.0, kernel-checked artefact of a third party.
• Summary of statement correspondence, coverage, Lean checks and trust dependencies: one requirement (linear upper bound for the multicolour Ramsey number of a tree), one target theorem, fully covered by JSP000448.multicolor_tree_ramsey_linear; the statement is a proposed statement (see "Statement origin"); trust dependencies are (i) the Lean kernel and its three standard axioms, (ii) mathlib at the pinned revision, (iii) the pinned Erdős–Sós formalization of Tom Adamczewski. No sorry, admit, unsafe, implemented_by, extern or native_decide anywhere in the contribution.
• Report in this PR or external report/log/evidence links, if available: JSP-000448/VERIFICATION.md and JSP-000448/verification.log at the pinned commit (https://github.com/1athena/jsp-formalizations/blob/43e040362cb0cc1f46f65c21ebd74e3e6cbf5b62/JSP-000448/VERIFICATION.md); the three API-drift fixes applied to the vendored dependency are enumerated in JSP-000448/PATCHES.md at the same commit.

Attribution

• Mathematical solver(s) and contribution, if applicable: not this account. The catalog records the solution with publication [ReSt26] The Erdős-Sós conjecture in dense graphs (arXiv:2609.05417, 2026); this PR makes no solver claim and changes no solver field.
• Lean formalization author(s) and contribution, if applicable: 1athena (this GitHub account) — author of the reduction JSP000448.lean (colour-class pigeonhole, edge counting, arithmetic core, and the call into Erdős–Sós). The author was assisted by an AI coding agent (WorkBuddy / LLM); every resulting artefact was checked by the Lean kernel as recorded above, and nothing is asserted that the kernel did not accept. Dependency author: Tom Adamczewski, author of the Erdős–Sós formalization used here (Apache-2.0, pinned by commit, credited in the source and in JSP-000448/VERIFICATION.md).
• Independent verifier(s), if any: none.
• Public authorship evidence; for an organization repository, link verifiable evidence connecting your account to the claimed proof files/theorems (such as merged PRs, attributable changes or project authorship records). Explain mismatches between authors, accounts and proposed credits: personal repository https://github.com/1athena/jsp-formalizations, created 2026-09-17T17:41:56Z, owned by 1athena; every commit in it is authored by 1athena; the pinned commit 43e040362cb0cc1f46f65c21ebd74e3e6cbf5b62 (2026-09-25T17:40:20Z) contains the claimed file. Account-to-author binding: docs/attribution.md in the same repository. No mismatch: the submitting account, the repository owner and the claimed formalization author are the same account. The only other credited person (Tom Adamczewski) is credited as the author of a pinned dependency, not as a co-author of this reduction.

Submission checklist

• I changed only the relevant catalog's solver attribution, Lean proof information or supporting sources and supplied the applicable evidence.
• The submitted result fully solves the original problem. Any submitted Lean proof is complete at the specified commit, with no sorry, admit or added unproved assumptions replacing proof steps.
• For Lean: I have linked the complete mathematical solution and its proof or publication evidence provided earlier, or supplied them in this PR, and identified the mathematical solver and Lean formalization author separately.
• For Lean: I am claiming my own contribution in the original personal or organization repository, with verifiable contribution evidence for an organization repository; the selected commit is in the named branch, and I supplied statement correspondence, reproduction commands and axiom audit results.
• This PR contains no Lean source files, archives, binaries, vendored dependencies or private identity/contact/payment information.

[1athena]

Self-check record for this submission (supporting evidence only; the lean-verify skill is optional under the current rules).

• Repository / branch / commit: 1athena/jsp-formalizations / main / 43e040362cb0cc1f46f65c21ebd74e3e6cbf5b62 — identical to the version referenced in this PR, no difference.
• Environment: Lean 4.35.0-rc2 (leanprover/lean4:v4.35.0-rc2, arm64-apple-darwin24.6.0), mathlib leanprover-community/mathlib4 @ 44ba35c6daa9d69aff8fed9fff9bbde17ded774d.
• Procedure: fresh git clone, clean worktree, HEAD at the pinned commit; lean -o Erdos548_192usd_21h.olean Erdos548_192usd_21h.lean (exit 0), lean -o JSP000448.olean JSP000448.lean (exit 0, 0 errors, 0 warnings), then an audit module with #check / #print / #print axioms.
• Axiom output: 'JSP000448.multicolor_tree_ramsey_linear' depends on axioms: [propext, Classical.choice, Quot.sound].
• No sorry, admit, unsafe, implemented_by, extern or native_decide in the contribution.
• Scope of the claim: only the Lean formalization is claimed here. The mathematical solution and its publication are those already recorded in the catalog entry (arXiv:2609.05417); this account does not claim them.
• A separate run of skills/lean-verify/scripts/audit.py against the same commit is in progress (it requires a full mathlib rebuild from source); its report will be posted here as a follow-up.

This PR changes exactly one line (+1/-1): the Lean proof cell of the JSP-000448 entry. Eligible to claim, Current status, Publication details and Public review are untouched.

[1athena]

Pre-submission Lean verification — official skills/lean-verify full run completed (JSP-000448)

Running the repository's own verification tooling (scripts/audit.py, from skills/lean-verify/) is
optional per docs/verification.md, but we have now completed a full run against the exact commit
pinned by this PR and are recording the result here for the maintainer's convenience.

Four required elements

Element	Value
Proof commit	43e040362cb0cc1f46f65c21ebd74e3e6cbf5b62 (1athena/jsp-formalizations)
Date of run	2026-09-25 / 2026-09-26 (UTC)
Command	python3 scripts/audit.py run <manifest> --out <out> --lake <lake> --timeout 1800
Result	exit 0 — mechanical_status: standard_axioms_only

What was actually executed (all four commands status: ok, exit_code: 0):

1. lake --version → Lake version 5.0.0-src+11acb17 (Lean version 4.35.0-rc2)
2. lake env lean --version → Lean (version 4.35.0-rc2, arm64-apple-darwin24.6.0, commit 11acb17ec6b07a8f9e9173e6845197929540936b, Release)
3. lake build +JSP000448 → built successfully (70.99 s)
4. lake env lean JSP000448.lean → elaborated cleanly (62.59 s)

Pinned inputs (SHA-256 recorded by the auditor, unchanged before/after the run — inputs_stable: true):

• JSP000448.lean → e6c8527be6f319a5ab9992f57cc4e480d6a1b7471e753a38017de75ce53f7912
• lean-toolchain → 8dc8d6f560141069d9073e370611716ef77ada0da8ffa37e2149f44b2e63ac7a (leanprover/lean4:v4.35.0-rc2)
• lakefile.lean → fa5f7e545020b17c7fb35e143d412b5a71c19fba63286ce97977e8920f058e2d
• lake-manifest.json → 520b4b3f83d005773b0ad7235e497dbf04e0466f86e182bac8ec1e6afa0581b1
• audit manifest → 18012b71e6097a8dfd080e374d846d4a925b0991dae01d2d1e5db35301cefaf6

Axiom / kernel audit (the part that matters most):

'JSP000448.multicolor_tree_ramsey_linear' depends on axioms: [propext, Classical.choice, Quot.sound]

Only the three standard, non-propositional-extensionality-abusing axioms of Lean's classical basis.
No sorry, no axiom declaration, no unsafe, no custom axioms, no partial/nonterminating
definitions. The proof is kernel-verified end to end.

Scope note (unchanged): this PR still modifies exactly one catalog file, one line
(Lean proof: Reported; standalone Lean source not located. → Yes — [Lean source](…JSP000448.lean)).
Eligible to claim, Current status, Publication details and Public review are left to the
maintainer. The mathematical solution is not claimed by this account (per the rule merged in
#4440 it is cited here via the catalog's own Publication details: [ReSt26] arXiv:2609.05417).

AI assistance was used in producing the formalization and is disclosed in the PR body.

[1athena]

Disclosure update (this account): the PR description now also names the earlier independent registration for JSP-000448 — issue #569 / PR #574 (zhangjun725, 2026-09-17T07:31:33Z, zhangjun725/erdos557 @ c4e0ab13…, Apache-2.0, deriving from tadamcz/erdos548 @ 82ffb751…). It predates this PR by ~9 days; no priority claim is made over it, and this PR may be closed as duplicate if the maintainers judge #569/#574 sufficient. This PR remains an independent formalization of R_r(T_{k+1}) \u2264 r\u00b7k+2 (JSP000448.multicolor_tree_ramsey_linear) in a separate self-owned repository; the diff is still 1 file, +1/−1, touching only the Lean proof cell.

[1athena]

Self-check against the published rejection grounds (this account, supporting evidence only)

Record-keeping comment. No change to the diff (still 1 file,
problems/catalog-0401-0500.md, +1/−1; head 31aa8a3454b1…). I am listing, for
reviewer convenience only, how this submission relates to the grounds cited in the
recent "Rejected: Identity & Attribution Mismatch" sweep. Reviewers should verify
each item independently; nothing here changes the submitted artifact.

#	Ground cited in that template	This submission
1	sec. 4.1 — Lean source must live in a standalone, self-owned repository, not a fork or mirror	Source is https://github.com/1athena/jsp-formalizations, created 2026-09-17T17:41:56Z, owned by this submitting account, not a fork of any repository. Lean source and build artifacts are kept out of the awards repo (PR touches one catalog .md only).
2	Rule 2 — unattributed third-party reuse (e.g. bulk reuse of an aggregate corpus)	One third-party file, Erdos548_192usd_21h.lean (1243 lines), is vendored from tadamcz/erdos548 @ 82ffb751f3d37768927df9239ed08439bbe0dd09, Apache-2.0, authored by Tom Adamczewski. It is named and linked in the PR description, in the catalog row itself, and in PATCHES.md, together with the exact list of the three mechanical API-drift fixes (no mathematical content altered). I claim no authorship of it — it is the Erdős–Sós formalization that the catalog entry for JSP-000439 already credits to Tom Adamczewski / GPT-6 Astra, and that the JSP-000448 entry itself names as the intended derivation path. It is not taken from an aggregate proof corpus.
3	Rule 5 — dropped scope or constraints (statement weakening)	The statement is the catalog question verbatim: does the multicolour Ramsey number of a tree grow linearly in its order? Proved affirmatively with the explicit bound R_r(T_{k+1}) ≤ r*k + 2 for every r ≥ 1 and every tree on k+1 vertices — theorem multicolor_tree_ramsey_linear (r k : ℕ) (hr : 0 < r) : ∀ c : Sym2 (Fin (r*k+2)) → Fin r, ∃ i, ∀ T, T.IsTree → T.IsContained (colorClassGraph c i). No colour-count, order or degree restriction was added; the bound is uniform in r and k.
4	sec. 2.1–2.3 / 6.7 — no proxy claim; submitter is the author	Submitted by the owner of the registered repository; no claim is made on behalf of Tom Adamczewski, of tadamcz, or of any other party. The mathematical solution (linear multicolour tree Ramsey) is not claimed by me — only the Lean reduction.
5	Native computation / unsafe escapes	lake build exit 0; #print axioms multicolor_tree_ramsey_linear → [propext, Classical.choice, Quot.sound] — Lean's three standard axioms only. No sorry, admit, unsafe, implemented_by, extern, native_decide, no added axioms, set_option relaxations or custom trusted declarations. The arithmetic core (arithmetic_core) is proved by induction/nlinarith, not by native_decide.

What is mine in this submission is the multicolour reduction itself (JSP000448.lean,
174 lines): the colour-class graph, the partition of ⊤.edgeFinset into the r colour
classes, the pigeonhole step, the exact count #⊤.edgeFinset = N.choose 2, and the
inequality ((k-1)/2) * N + 1 ≤ N.choose 2 / r at N = r*k+2 that makes the Erdős–Sós
hypothesis fire. That derivation is not present upstream.

Priority statement (restated, unchanged): an earlier independent registration of
this problem exists — issue #569 and PR #574 by zhangjun725
(2026-09-17T07:31:33Z, repository zhangjun725/erdos557 @ c4e0ab13…, Apache-2.0,
also building on tadamcz/erdos548) — roughly nine days before this PR. I do not
assert priority over it, I do not ask for it to be closed, and I have no objection to
this PR being closed as a duplicate. It is offered only as an independent, kernel-checked
second formalization in case it is useful to the review.

AI assistance is disclosed in the PR description and in the catalog row (written with AI
assistance, checked by the Lean kernel).

[1athena]

Repository-architecture self-check against §4.1 (per the determination in PR #255)

The maintainer determination in #255 (2026-09-25) states that an external Lean formalization must live in a standalone, submitter-controlled repository, and that a fork of the awards metadata repository does not qualify. Recording the corresponding facts for this submission so they can be checked without cloning:

Item	Value	How to check
Repository	1athena/jsp-formalizations	GET /repos/1athena/jsp-formalizations
Is a fork	false (parent: null, source: null)	same response
Owner	1athena — the submitting / applicant account	same response
Visibility	public	same response
Created	2026-09-17T17:41:56Z	same response
Licence	Apache-2.0 (LICENSE file added 2026-09-26, commit 9d3edacac820e618e818da5e3973d817fcb95fcd)	license.spdx_id
Per-problem path	verification/JSP-000448/ ( JSP-000448/ )	contents API
Pinned commit	39b85298cffb83fb07423216e741550e90470c09 (committer date 2026-09-19T08:09:00Z)	GET /repos/1athena/jsp-formalizations/commits/39b85298cffb83fb07423216e741550e90470c09

• The repository is not a fork of TheJustinSunPrize/awards and never was; it was created empty and populated by this account.
• The Apache-2.0 licence was already declared in the PR description but the file was missing, so the declaration was not machine-checkable. That is now corrected. Adding it sits on main and cannot alter the pinned commit: 39b85298… still resolves, with its original committer date.
• If the maintainers would prefer a per-problem dedicated repository (for example 1athena/jsp-000301-lean) instead of one repository holding several problems, say so here and I will create it carrying the bit-identical commit object, so the 40-character SHA above and every timestamp stay the same and remain independently checkable. I have not done this unilaterally, because repository-creation time is one of the public anchors the award process asks for and I did not want to move it without being told.

Restated so that nothing has to be inferred:

• No priority claim. zjukop3 (PR [Correction] JSP-000448: standalone Lean proof now available (Lean proof / Eligible to claim / Claim status) #569 / PR JSP-000448: register Lean formalization (Erdős #557) #574) precedes this submission on every public anchor by roughly nine days. I do not contest that, and I have no objection to this PR being closed as a duplicate.
• The identity-verification email from 994578847@qq.com to thejustinsunprize@hejustinsun.com is still outstanding. It can only be sent by the applicant; it has not been sent on their behalf, and no completed identity verification is asserted anywhere in this PR or in issue [Award claim] JSP-000301 #1709.
• This PR still changes exactly one file by one line (+1/−1): the Lean proof row only.

[1athena]

Completeness attestation against the two-part requirement

The closing note applied elsewhere in this queue states the requirement as (1) a complete solution to the original problem and (2), for Lean submissions, a complete formalization of that solution — partial progress or a partial formalization being insufficient. Mapping this submission onto those two clauses, in one place:

Clause	This submission (JSP-000448)
(1) Complete solution to the original problem	The catalogue asks whether the multicolour Ramsey number of a tree grows linearly in its order. The answer yes is supplied here as the explicit, fully general bound R_r(T_{k+1}) ≤ r·k + 2 for all r ≥ 1, proved along the route indicated in the catalogued entry (pigeonhole → Erdős–Sós → arithmetic check); the supporting literature reference is linked in the PR description.
(2) Complete Lean formalization of that solution	JSP-000448/JSP000448.lean @ 43e040362cb0cc1f46f65c21ebd74e3e6cbf5b62 → JSP000448.multicolor_tree_ramsey_linear, proved for all r and k — not for a fixed r, a bounded range, or a scoped component.
Nothing partial	no sorry, no admit, no custom axioms; #print axioms returns [propext, Classical.choice, Quot.sound] (the standard classical basis), i.e. nothing introduced by this submission.
Third-party code	Erdős–Sós (Erdős problem 548) by Tom Adamczewski, Apache-2.0, vendored with three mechanical API-drift fixes and disclosed as third-party; no authorship claimed.

(Edited: the path and pinned SHA in the original version of this comment were transcribed wrongly; the values above are the correct ones.)

This submission asserts no priority over any other.