Metadata
slug: kumar-2026-rectangular-weak-two-metric-dimension
bibkey: kumar2026weakmetric
doi: 10.48550/arXiv.2609.32161
url: https://arxiv.org/abs/2609.32161v1
triage: theorem
motivation_gids:
- D5/S3/Combinatorics/Graph/HammingWeakTwoMetricDimension.result
Kumar’s remaining rectangular weak two-metric dimensions
Problem
Aryan Kumar, arXiv:2609.32161v1, §7:
The rectangular k = 2 values below the threshold m = 2n − 2 remain to be determined.
The vertices of are pairs in , with . For a landmark set , put . A weak -resolving set has for every distinct pair; is its least cardinality.
The exact rectangular answer is
For natural-number division, the ceiling is .
The Lean claim retains all three size conditions and both upper-bound terms.
Motivation
The source’s Theorem 2.10 gives dimension when and the lower bound when . The formula determines the remaining strictly rectangular values, including the transition between the two optimal landmark constructions.
Gap
Kumar (arXiv:2609.32161v1, 2026) proves for and for , and lists the values for as undetermined in §7. Fernández, Klavžar, Kuziak, Muñoz-Márquez and Yero (arXiv:2505.19642) leave the rectangular case for further investigation and report integer-programming values for ; all fourteen of their values with agree with the formula proved here. arXiv lists only version 1 of 2609.32161 and no citing work; an arXiv search for “weak k-metric” returns only 2505.19642, 2605.22307 and 2609.32161; the MathDB entry #368568 concerns .
Route
Write and for the landmark counts in row and column . Pairs in one row have separation ; pairs in one column have separation . For and ,
Consequently the row and column degree sums must be at least two. Two vertex-disjoint landmark edges must have total endpoint degree at least six. These three conditions also suffice: when both cross corners are landmarks, the third condition applies; with zero or one cross landmark, the first two conditions suffice. This includes empty rows and columns.
For the lower bound, an empty row forces every other row to have degree at least two, giving . An empty column similarly gives . Otherwise all degrees are positive and the exact incidence count is
If there is no edge with both endpoint degrees one, each summand is at most , so . If an edge has both degrees one, every other edge is disjoint from it and has endpoint-degree sum at least four. Its charge is therefore at most . Thus , or . For this again implies . Taking the integer ceiling proves the lower bound.
For the upper bound , leave row zero empty. Index landmarks by and place landmark in row and column . Every occupied row has degree two, and every column is occupied because . Every two disjoint landmark edges therefore have endpoint-degree total at least six, and the degree conditions hold.
For the ceiling upper bound, construct an incidence forest for positive with , and . For totals at most five, use a three-vertex star, a four-vertex path, or a five-vertex path. For larger totals, if , remove one row and two columns, construct the smaller forest, and adjoin a disjoint three-vertex star centered in the new row. If , use the symmetric construction. The reduced sizes retain the balance conditions. Each step adds three vertices and two edges, so the total edge count is at most . Every row and column has positive degree, and every edge has endpoint-degree sum at least three. The resolving conditions follow.
Falsifier
The formula would fail if the distance identities were incorrect, an empty row or column evaded the degree lower bound, the reciprocal charges exceeded their stated bounds, or either construction violated its cardinality or separation conditions. The distance identities count both cross corners, and the constructions retain every row and column condition needed for all distinct vertex pairs.
Evidence
The designated statement is
D5/S3/Combinatorics/Graph/HammingWeakTwoMetricDimension.result : claim.
The core definitions use Fin n × Fin m, finite landmark sums and the
infimum of achievable natural cardinalities. The complete vertex set is
weak two-resolving for every pair of natural sizes, so the minimum at
is attained even for empty or singleton vertex products.
The lower estimate uses exact rational arithmetic and finite incidence
counts. The upper estimates use symbolic finite embeddings and natural
arithmetic. No approximate optimization or floating-point premise is needed.
The axiom closure of result is propext, Classical.choice, and
Quot.sound; no sorry, new axiom or native_decide is used.
Triage
- [proved:
HammingWeakTwoMetricDimension.result] The formula determines every strictly rectangular value below the source threshold. The two competing mechanisms are a sparse incidence forest covering all vertices and a configuration with one empty row. The smaller of their landmark counts is optimal. - [proved:
HammingWeakTwoMetricDimensionLower.bipartite_degree_charging] The nonisolated-vertex incidence estimate only needs at least six total vertices and the disjoint-edge endpoint-degree condition; connected components need not be classified. - [open] The source’s questions for and the square case are separate boundaries. The rectangular formula alone supplies no general solution for those parameters.
ASSUMED-UNVERIFIED
Forward citations were screened through arXiv, Semantic Scholar, MathDB and web search only; no citation index was read exhaustively.