The proper repair dimension on a fixed domain: a sharp bound, its equality cases, and a domain-minimal separation from the Littlestone dimension
Abstract
For a finite binary concept class H ⊆ {0,1}^X on a finite domain X, Li [Li] defines the proper repair dimension PRD(H) by a recursion on version spaces — a live hypothesis is eliminated by a label it does not predict, and PRD is the worst case, over the adversary's choices, of the best case over the learner's — and proves Ldim(H) ≤ PRD(H) ≤ |H|-1, both bounds tight. Every bound in that paper is in terms of |H|; nothing there constrains PRD in terms of the domain. We prove that PRD(V) ≤ |free(V)|, where free(V) is the set of coordinates on which V is not constant, so that PRD(H) ≤ n for every class on n points, against the 2ⁿ-1 that |H|-1 gives at H={0,1}^([n]). We then determine the equality cases exactly: PRD(V)=|free(V)| holds if and only if V is a subcube, so max{PRD(H): emptyset ≠ H ⊆ {0,1}^([n])}=n with the full class as the unique maximiser. It follows that a class of size m ≥ 3 attaining Li's bound PRD(H)=|H|-1 needs a domain of at least m points. That bound is attained: the one-hot class {e₁,…,eₙ} ⊆ {0,1}^([n]) has |H|=n, Ldim(H)=1 and PRD(H)=n-1=|H|-1. This class is Li's own separating example Uₙ with its domain cut from 2^([n]) down to the n singletons, and it improves that example on two axes at once — domain size 2ⁿ → n and Littlestone dimension ⌊log₂ n⌋ → 1 — at the same |H| and the same PRD; by the previous sentence the domain cannot be cut further. We also record the complete joint distribution of (Ldim,PRD) over all nonempty classes on at most three points, and, as computations outside the formal development, over all 65 535 classes on four points and, as a count of orbits under the automorphism group of the cube, over the 4 294 967 295 on five. All the general statements are proved uniformly in n and machine-checked in Lean 4.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-09-07 03:53 UTC
File fingerprint
7b9159eaef3bc3fb6a7648a31f31922dc0d9b7a74d10010967ef840a630ed9d4
Claim ledger
Stated results
RD1known2026-09-02
The source's own two bounds, formalised from its own definitions for every finite binary class on a finite domain: Ldim(V) <= PRD(V) and PRD(V) <= |V| - 1 (Theorem thm:ldim-prd), and PRD(0,1^[n]) = n (Theorem thm:full-class at C_d)
RD2candidate2026-09-02
A domain-minimal separating class: the one-hot class e₁,...,eₙ in 0,1^[n] has |H| = n, Ldim(H) = 1 and PRD(H) = n - 1 = |H| - 1, for every n >= 2; the same holds for its bit-flip translate Hₙ = 0ⁿ u e_c + eⱼ: j!= c. Against the source's own separating class Uₙ (|Uₙ| = n, PRD = n-1, Ldim = floor(log2 n), domain of size 2ⁿ) this improves the domain from 2ⁿ to n AND the Littlestone dimension from floor(log2 n) to 1, at the same |H| and the same PRD
RD3candidate2026-09-02
PRD(V) <= |free(V)| <= n for every nonempty V in 0,1^[n], where free(V) is the set of coordinates on which V is not constant. The source's only upper bound is PRD(H) <= |H| - 1, which is 2ⁿ - 1 at |H| = 2ⁿ
RD4candidate2026-09-02
PRD(V) = |free(V)| holds exactly on the subcubes: for nonempty V in 0,1^[n], PRD(V) = |free(V)| if and only if V contains every concept that agrees with V at each coordinate where V is constant. Both directions proved uniformly in n; the census confirms the count 3, 9, 27 = 3ⁿ at n = 1, 2, 3
RD5routine2026-09-02
Ldim and PRD are invariant under the bit-flip translations g |-> g XOR v of the cube (2ⁿ of the 2ⁿ n! automorphisms of 0,1^[n])
RD6candidate2026-09-02
maxPRD(H): H a nonempty subset of 0,1^[n] = n, attained ONLY by the full class H = 0,1^[n]; consequently a class with |H| = m >= 3 attaining the source's bound PRD(H) = |H| - 1 needs a domain of size at least m, so the one-hot class of RD2 is domain-minimal (the source's own witness Uₘ uses a domain of size 2ᵐ)
RD7routine2026-09-02
The complete (Ldim, PRD) census of every nonempty concept class on a domain of size n <= 3, kernel-bound: n=1 -> (0,0):2, (1,1):1; n=2 -> (0,0):4, (1,1):10, (2,2):1; n=3 -> (0,0):8, (1,1):84, (1,2):8, (2,2):154, (3,3):1, with the five cells proved to exhaust all 255 classes
RD8routine2026-09-02
The (Ldim, PRD) census at n = 4 (65535 classes: (0,0):16, (1,1):696, (1,2):160, (1,3):16, (2,2):23052, (2,3):8088, (3,3):33506, (4,4):1) and at n = 5 (4294967295 classes: (0,0):32, (1,1):5968, (1,2):2080, (1,3):480, (1,4):32, (2,2):3823000, (2,3):6236384, (2,4):442672, (3,3):1315856404, (3,4):1205986440, (4,4):1762613802, (5,5):1), from families/repair-dim/tools/census.c; not kernel-bound
This ledger entry is reported in prose and is not bound to a Lean theorem.RD9routine2026-09-02
Negative controls: PRD <= n cannot be improved to n-1 (the full class attains n); the source's PRD <= |H|-1 cannot be improved to |H|-2 (the one-hot class attains it); Ldim = PRD is false (Ldim 1 < PRD 2 on three points); the subcube hypothesis of RD4 is not vacuous (0³, 1³ has three free coordinates and PRD 1); the 2 <= |J| hypothesis of Ldim(oneHot J) = 1 is needed; the |H| >= 3 hypothesis of the minimal-domain theorem is needed (on a one-point domain the full class has |H| = 2 = PRD + 1 > n)
Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- Fix a finite domain X and a finite binary concept class H ⊆ 0,1^X. For a version space V ⊆ H, a point x ∈ X and a label b ∈ 0,1, write V_(x,b) = g ∈ V: g(x) = b.
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7