pith. sign in

arxiv: 2511.20724 · v2 · pith:YQMV6HY7new · submitted 2025-11-25 · 🧮 math.CO · math.LO

Hall's Harem Theorem with controlled sizes of cycles

Pith reviewed 2026-05-21 18:40 UTC · model grok-4.3

classification 🧮 math.CO math.LO
keywords Hall's Harem Theorembipartite graphsmatchingsunary functionscyclescombinatoricsset systems
0
0 comments X

The pith

Hall's Harem Theorem holds when the matching is realized by a unary function with controlled cycle sizes.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper proves a variant of Hall's Harem Theorem in which the harem matching in a bipartite graph is represented by a unary function. The function comes with restrictions on the sizes of cycles that appear in its functional graph. The standard Hall condition on the graph guarantees the existence of such a representation. This version is independent of a prior computable version of the same theorem. It matters because it gives a different structural way to view and perhaps construct the required matchings with explicit cycle bounds.

Core claim

If a set system or bipartite graph satisfies the generalized Hall condition for prescribed matching sizes, then there exists a unary function that realizes the matching and whose cycles satisfy additional size conditions derived from the matching.

What carries the argument

Unary function that realizes the harem matching while enforcing cycle size restrictions in its graph.

If this is right

  • The theorem applies directly to any collection of sets meeting the Hall condition.
  • Matchings can be chosen so that their functional representation has cycles of controlled lengths.
  • The result provides an alternative to computable constructions without relying on them.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Combining this structural version with computational methods might yield new algorithms for finding such matchings.
  • Similar cycle controls could apply to other matching theorems in graph theory.
  • The independence from the computable version suggests multiple proof techniques exist for the same extension.

Load-bearing premise

The input bipartite graph or set system must satisfy the standard generalized Hall condition for the desired harem sizes.

What would settle it

A specific bipartite graph that obeys the Hall condition yet has no unary function realization of the matching with the stated cycle size restrictions would disprove the theorem.

Figures

Figures reproduced from arXiv: 2511.20724 by Karol Duda.

Figure 1
Figure 1. Figure 1: The first part of the first step, M1 0 -fan of u0 in red and green, M0 0 in green. 3.2. Remarks before part 2. Before the second part of step 1 let us discuss our local goals. Let f0 be the partial function which correspond to M0 and let Γ(1) be the graph obtained after step 1, i.e. the part of Γ after removal M0. We want to force that: (1) for all n ∈ Dom(f0) there exists i such that f i 0 (n) is a period… view at source ↗
Figure 2
Figure 2. Figure 2: Step 1, part 2. M2 0 is red. We want the edge (u 1 0 , vu0 ) to be in M0. Force the situation from [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: M1 0 is green. It is possible that the purple fan consisting of edges ( ˙u ⊥ 0 , v˙ ⊥ 0,1 ),( ˙u ⊥ 0 , v˙ ⊥ 0,2 ) will be added to Γ(1)⊥. Put M0 = M0 0 ∪ M1 0 . We obtain Γ(1) by removal of M0 from Γ. Since u0, vu0 , v0 0,1 and u 1 0 = uv 0 0,1 have been removed, Γ(1) is U (1)-reflected. It might turn out that it does not satisfy Hall’s d-harem condition. Let Γ′ 0 = (U (1) \ {u˙ ⊥ 0 }, V (1) \ {v˙ ⊥ 0,1 , … view at source ↗
Figure 4
Figure 4. Figure 4: Γ (n)⋆ is black, Γ(n)⊥ is purple. un vun v 0 n,1 v 0 n,2 v 0 n,3 u ⊥ j0 v ⊥ j0,1 vu ⊥ j0 v ⊥ j=0,2 [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Mn 1 is red and green, M0 n is green. We have vun = v ⊥ j0,2 [PITH_FULL_IMAGE:figures/full_fig_p008_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: M1 n is green. We have vu⊥ j1 = v ⊥ j2,2 . Moreover vu⊥ j1 = v 0 n,2 . To demonstrate the cycle in a single picture, we take 4 copies of N as rows. The first and the second ones correspond to V and U after part 1 of the step. The second and the third rows correspond to the sets V and U after the first iteration step. The third and the fourth rows correspond to U and V after the second step of the iteration… view at source ↗
Figure 7
Figure 7. Figure 7: The final Mn with the obtained cycle of length 3 marked in blue. The red edge is the edge from Mn 1 that was not added to M0 n . 3.12. Case (3) and the end. Since the edge (u l n , vl n,1 ) is in Γ(n) and vul n is not in Γ(n) (−un, −u 1 n , . . . , −u l n ), applying U (n) -reflectedness of Γ(n) we see (u l+1 n , vul n ) ∈ Γ (n) (−un, −u 1 n , . . . , −u l n ). Observe that since u ⊥ j1 , . . . , u⊥ jl are… view at source ↗
Figure 8
Figure 8. Figure 8: x is accessible from y by matching M (red), the elements of X are blue and the elements of NΓ(X) are green • X is a minimal connected subset in V ⋆ ∪ {vb} with |NΓ(X)| < 1 d |X|; • ub ∈ NΓ(X) \ U ⋆ . • (u, b vb) ∈/ E. Then u , b M,X −−−→→ vb. Proof. It is clear that vb ∈ X. Let X′ denote the subset of all elements of X that are either adjacent to ub or accessible from ub through X by the matching M. Since … view at source ↗
Figure 9
Figure 9. Figure 9: Application of Lemma 4.2; red letters correspond to the notation of Lemma 4.2. Indeed, let S denote the fan from the matching M containing vun and S′ denote S with vun removed. The conditions of Lemma 4.2 are satisfied if we consider Γ(n) (−un) as Γ in that lemma, vun as v, and Γ(n)⊥ ∪ {v} ∪ S′ as Γ⊥. Indeed, Γ(n) (−un, −vun ) is U (n) (−un, −vun )- reflected. Moreover, the corresponding graph Γ⋆ from Lemm… view at source ↗
Figure 10
Figure 10. Figure 10: We replace the red fans in the matching M1 n by the blue fans to obtain the matching M′ in Γ(n)⋆ (−un, +u ⊥ j ). We remind the reader that M1 n is a perfect (1, d)-matching in the graph Γ(n)⋆ . We have obtained M′ by removing d edges adjacent to un, adding d edges incident to u ⊥ j , and the following replacement: for each of u ′ i we replace one edge incident to it by another incident edge (then v become… view at source ↗
read the original abstract

We prove a new version of Hall's Harem Theorem, where the final matching is realized by a unary function with additional conditions on behavior of cycles. The present paper can be considered as a helpful companion of the paper of the author: arXiv:2105.06304, where a computable version of Hall's Harem Theorem with controlled sizes of cycles is proved. These two versions of Hall's Harem Theorem are independent: none of them follows from the other one.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper proves a new version of Hall's Harem Theorem in which the final matching is realized by a unary function with additional conditions on the behavior of cycles. It is presented as an independent companion to the author's earlier computable version in arXiv:2105.06304, with neither result following from the other.

Significance. If the proof holds, the result supplies a non-constructive existence theorem for Hall-type harem matchings with controlled cycle sizes, realized via a unary function and non-computable selection. This complements the computable version by establishing independence through distinct methodological choices, adding structural insight into set systems satisfying Hall-type conditions.

minor comments (2)
  1. The abstract states the independence from arXiv:2105.06304 but does not briefly indicate the methodological distinction (non-computable selection versus computable construction); adding one sentence would improve reader orientation.
  2. Notation for the unary function and the precise cycle-size restrictions should be introduced with a short definition or example in the introduction rather than deferred to the main construction.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our manuscript, the accurate summary of its contribution as an independent companion result to arXiv:2105.06304, and the recommendation of minor revision. No specific major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The manuscript is a direct existence proof in combinatorics that starts from the standard Hall-type matching condition on a set system (or bipartite graph) and explicitly constructs a unary function representation while enforcing the required cycle-size restrictions via the matching properties. The derivation relies on non-computable selection to maintain independence from the author's prior arXiv:2105.06304, which is cited only as a companion paper with the explicit statement that neither version follows from the other. No load-bearing step reduces by definition, by fitting, or by self-citation chain to the target result; the argument is self-contained against the external Hall condition and does not invoke any of the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the standard combinatorial assumptions of Hall's Harem Theorem and the existence of a matching under those assumptions; no new free parameters, invented entities, or ad-hoc axioms are introduced in the abstract.

axioms (1)
  • domain assumption Standard Hall-type condition for the existence of a harem matching
    The proof begins from the usual hypothesis that a matching exists and then constructs the unary-function representation with cycle controls.

pith-pipeline@v0.9.0 · 5589 in / 1181 out tokens · 65262 ms · 2026-05-21T18:40:28.311330+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

3 extracted references · 3 canonical work pages

  1. [1]

    Matchings in infinite graphs

    [Aha88] Ron Aharoni. “Matchings in infinite graphs”. In:Journal of Combinatorial Theory, Series B44.1 (1988), pp. 87–125.issn: 0095-8956.doi:https : / / doi . org / 10 . 1016/0095- 8956(88)90098- 6.url:https://www.sciencedirect.com/science/ article/pii/0095895688900986. [Bol79] B´ ela Bollob´ as.Graph theory, an introductory course. Graduate Texts in Math...

  2. [2]

    Computability of Følner sets

    Springer, 1979.doi:10.1007/978-1-4612-9967-7. [Cav17] M. Cavaleri. “Computability of Følner sets”. In:Intern. Journ. Algebra and Comput. 27 (2017), pp. 819–830. [Cav18] M. Cavaleri. “Følner functions and the generic Word Problem for finitely generated amenable groups”. In:J. Algebra511 (2018), pp. 388–404. [CC10] Tullio Ceccherini-Silberstein and Michel C...

  3. [3]

    Computable paradoxical decompositions

    arXiv:2105.06304v3 [math.GR]. [DI22a] Karol Duda and Aleksander Ivanov. “Computable paradoxical decompositions”. In: International Journal of Algebra and Computation32 (2022), pp. 953–967.doi:https: //doi.org/10.1142/S0218196722500400. [DI22b] Karol Duda and Aleksander Ivanov. “On Decidability of Amenability in Computable Groups”. In:Arch. Math. Log.61.7–...