[randyxian08]

Submission type

• Mathematical solver information
• Lean proof or formalization author information

Problem

• Problem ID: JSP-000937; original source: Erdős problem 1130.
• Mathematical solution/review reference: The all-gap maximin interpolation problem, associated with de Boor and Pinkus (1978), plus the logarithmic request on the original Erdős 1130 page. Mathematical and formal-statement correspondence remain for maintainer review.
• Current catalog entry says Lean proof: No; this PR changes only this problem's Lean proof and Attribution basis rows to a scoped external proof reference. It leaves solver status, eligibility, and other records unchanged.
• Companion claim/evidence: #152. This reuses the existing single-problem PR JSP-000937: catalog Lean evidence and formalization attribution #765 after JSP-000936, JSP-000937, JSP-000958: migrate existing submission to catalog-only Lean references #144 was closed; it is not a new priority date.
• Priority/related work: Related JSP-000937: record existing Lean formalization (randyxian08/jsp000937-lean) #1566 cites our original repository and exact old SHA while disclaiming proof authorship; it is a catalog registration, not an independent competing proof. catalog: record Lean formalization for JSP-000937 #1680 addresses a stronger all-peaks-equal statement and catalog: record Lean formalization for JSP-000937 #2036 describes partial numerical scope. Please compare any independently earlier complete Target937 proof before assigning priority; we do not assert global firstness from the absence of one in this bounded comparison.

Formal statement

• Independent proposed statement; it has not been approved as an official benchmark statement.
• Exact target: JSPFreeNodes.jsp_000937 : JSPFreeNodes.Target937.
• Correspondence: Target937 is the conjunction of (i) existence and classification of maximizers of the minimum of all n+1 interval peaks, including both exterior intervals and the one-node case, and (ii) a single C>0 with allMinPeak(X)≤C log n for every n≥2 and every node family. The reference shape is normalized, but competitors are free-node; the exterior peaks are required to be at least the reference height, not all equal. The clause-by-clause mapping is in STATEMENT-CORRESPONDENCE.md.
• Low-cardinality check: for two nodes every placement has all-gap minimum 1; the pair (-1/2, 1/2) has exterior peaks 2 and internal peak 1. The literal maximization therefore cannot require all peaks to be equal in this case; see the calculation.

Proof submission

[
  {
    "repository": "https://github.com/randyxian08/jsp000937-lean",
    "branch": "main",
    "commit": "c6819617f4d8de6afcbf63da31544ce2902f7b6a"
  }
]

• Proof file and target above. The final theorem is the conjunction of jsp_000937_classification and jsp_000937_logarithmic; Audit937.lean checks the full target type, and AuditFull.lean checks the related entries and axioms.
• Historical public proof snapshot: 9f249379d6d96e9e70f91e2c22982f96a23de2da with submitter CI run 35125716929. Its 4.27.0 checks establish historical publication evidence, not verification of the new commit.

Reproduction

• lean-toolchain: Lean 4.33.0; pinned Mathlib db584cd6d46c92f209a44c0f1c829460d327499d in lakefile.toml and lake-manifest.json.
• From a clean checkout of the exact commit: bash verify.sh. The script builds the target, checks its declaration and statement bridge, reports transitive axioms, scans trust-sensitive source, and runs leanchecker.
• Direct target build: lake build Erdos1153.JSPInterpolation.Logarithmic. Axiom audit: lake env lean AuditFull.lean. Kernel replay: lake env leanchecker Erdos1153.JSPInterpolation.Logarithmic.
• The selected target's #print axioms output is [propext, Classical.choice, Quot.sound]. Local command/results record; Linux CI run 35849587676. These are submitter-run checks, not organizer verification. A separate FRO comparator self-check used the Lean 4.33.0-compatible comparator and Landrun in a network-disconnected Linux container. Both the Lean default kernel and the nanoda external kernel accepted the selected proof with only propext, Classical.choice, and Quot.sound. The challenge imports the submitted definition layer, so independent problem-to-statement review remains necessary. The evidence-only follow-up commit is 4d7493e7e730597877c38bd750bf02839863b68a; the proof submission remains c6819617f4d8de6afcbf63da31544ce2902f7b6a.

Attribution

• Mathematical solver(s): the historical publication authors cited above; this PR does not seek solver credit.
• Lean contribution claimed: randyxian08, with inherited work and AI assistance disclosed in the pinned source. The submitting account owns the original proof repository. PROVENANCE.md distinguishes the credited ethn-y/erdos-1153-lean base and AI assistance from the submitted all-gap and logarithmic extension. Repository control supports traceability but does not by itself settle independent identity verification.
• Independent verifier: none named. Identity, statement coverage, priority, and award eligibility remain for the organizers to determine.

Submission checklist

• Only the relevant catalog entry's permitted Lean proof and attribution text changes; the PR adds no Lean source or private contact data.
• The selected proof is submitted as a complete answer to the original problem, with no sorry, admit, or added unproved mathematical assumptions in the checked target; statement correspondence remains subject to review.
• The proof is from the submitting account's original repository, pinned to a 40-character SHA on main, with reproduction and axiom evidence above.

[randyxian08]

Superseded by #144, which now contains the compliant catalog-only reference for JSP-000937, the exact proof source and full chronology. Closing this temporary migration PR avoids duplicate proof submissions. Original Issue #152 and public verification evidence remain linked; no priority determination or withdrawal of the underlying contribution is implied.

[randyxian08]

The updated catalog entry and PR body now pin proof commit c6819617f4d8de6afcbf63da31544ce2902f7b6a. Its Lean 4.33.0 CI passed. The separate FRO comparator / nanoda evidence records submitter-run acceptance with the three standard axioms in a network-disconnected Linux container. That later evidence commit is documentation only; it does not change the selected proof SHA. The self-authored challenge imports the submitted definitions, so original-problem correspondence and formalization priority still require review. The older comment saying this PR was superseded by #144 is obsolete: #144 closed and this existing single-problem PR is the active submission.