What was already known
Kanoria’s earlier theorem gave a lower bound of order log(m)/m and an upper bound of order (log m)²/m in this model.
AI involvement
Kanoria directed and explained the project. The manuscript and repository credit ChatGPT/Codex agents with developing the retained hierarchical deletion policy and proof.
Agents developed the retained policy and proof under Kanoria's mathematical direction; exact model versions are not fully recorded.
- Supporting source (github.com) — cost clauses, policy quantifiers and omitted resource-accounting claim
Importance
Matches the known lower-bound order for the specified fully dynamic one-dimensional matching model.
Limitations
The reported formal theorem covers the two upper-bound cost clauses. It does not certify an executable time or memory bound, and the earlier lower bound remains prior human work. No independent human line-by-line proof check is documented.
Technical verification
The source reports a Lean kernel-checked proof of the two upper-bound clauses and Comparator/NanoDa replay. Operational complexity and the lower-bound corollary are outside the checked statement.
Formal checking
Repository reports Lean verification, statement comparison, axiom audit and replay of the two upper-bound clauses.
- Checker
- Lean kernel, Comparator and NanoDa
- Scope
- FD1D.V5.Palomar.optimalDynamicMatchingUpperBound: RMS and finite-horizon expected-cost clauses
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Kanoria's manuscript explains the central policy and analysis in Sections 1–4 and its detailed Bellman proof; this is human-facing explanation of the assessed upper bound, separate from proof checking.
Correction and publication history
The compared Lean theorem covers two upper-bound cost clauses for the specified policy.
Read this published revision