# Verification report — OPG-57403 and OPG-751 (two problems of Porton on reloids)

Verification date: 2026-10-08.

**Verdict.**
- OPG-57403: the conjecture is **true**. Every metamonovalued reloid is monovalued; already every weakly
  metamonovalued reloid is monovalued, and one fixed pair of principal reloids decides it (Theorem 1.1).
- OPG-751: the answer is **no**. There is an endoreloid f on a countable set with S(f)∘S(f) ≠ S(f) and
  S(S(f)) ≠ S(f) (Theorem 1.2). The identities hold for principal reloids, in particular on finite sets, and for
  Porton's operator S*.
- By-product: the corresponding two conjectures for funcoids fail as well (Theorem 1.3). These funcoid statements
  are not corpus records. The proof of Theorem 1.3 was written for the note and was then checked by the third
  independent verification run (see "Independent verification runs" below).

The note is unrefereed. All results are elementary.

## Statement checked
- **Primary source.** V. Porton, *General Topology as Ordered Semigroup Actions. Book 1* (earlier title:
  *Algebraic General Topology. Volume 1*), self-published and regularly rebuilt. Two copies were used.
  - Copy A, built 2026-08-16: 455 pages, sha256 `2f339b490e70f13483357b20fabd6120299dee4437a404d622a3ec96fa55cecf`.
    The note uses its item and page numbers.
  - Copy B, built 2026-10-01: 463 pages, 2,182,877 bytes, sha256
    `286f7913ef6ca8a03b842fff66416fe670120f51814fa18171b014f6c384722a`. It was fetched from
    https://math.portonvictor.org/binaries/volume-1.pdf on 2026-10-08 at 14:19 UTC. HEAD requests at 15:10 UTC and
    at 16:14 UTC returned the same ETag, Last-Modified (2026-10-01 14:47:59 GMT) and length, so this was still the
    online copy when the note was written and when it was checked.
  - Numbering. For the cited items the two copies have the same wording. Items of Chapters 2–5 keep their numbers
    and appear one page later in copy B. Items of Chapters 25–32 of copy A have numbers larger by 6 in copy B,
    appear four pages later, and their chapters are numbered one higher. This was confirmed for 104 items (62 of
    them cited in the note) and 6 section headings by `reproducibility/sources/crosscheck_numbering.py`, and again
    for the 62 cited items and 5 section headings by `reproducibility/independent_run_2/run2_D_sources.py`, on a
    second text extraction.
  - The conjectures. Copy A: Conjecture 1363 (p. 282); Conjecture 1253 parts 1° and 2°, Conjecture 1254 and
    Conjecture 1256 (p. 261). Copy B: Conjecture 1369 (p. 286); Conjectures 1259, 1260 and 1262 (p. 265). In copy B
    they are **still stated as conjectures** (pages read on 2026-10-08).
  - All items cited in the note were read on rendered pages of copy A, when the note was written and again in the
    third run. In copy B the following pages were read: 2, 49, 214, 215, 222, 260, 262, 265, 286 (writing), and
    176, 215, 260, 262, 265, 286 (third run).
- **Open Problem Garden** (pages read on 2026-10-08, by the verification runs and at the writing; last at
  16:15 UTC).
  - "Every metamonovalued reloid is monovalued" (posted 2013-09-17 by V. Porton): the one-sentence conjecture, no
    comments, no solution. It refers to the book for the notions.
  - "S(S(f)) = S(f) for reloids" (posted 2008-04-10 by V. Porton): the question for every endo-reloid f. One
    comment of 2008 by the poster about a corrected article; no solution. For definitions the page refers to the
    draft "Connected funcoids and reloids"; in its version of 2008-05-08 (Internet Archive capture of 2008-05-15),
    S(μ) = μ⁰ ∪ S₁(μ) contains the identity term, as in the book, and its Conjecture 30 is S(S(f)) = S(f) for
    reloids and for funcoids.
  - "S(S(f)) = S(f) for funcoids" (posted 2008-04-10): the same question for any funcoid; no solution.
- **Corpus records.** ulamai/UnsolvedMath, OPG-57403 and OPG-751 (upstream status `open`). Their statements are the
  Open Problem Garden statements. The funcoid question is not a corpus record.

## Readings
| Statement and reading | Answer | Where |
|---|---|---|
| Every metamonovalued reloid is monovalued; families in the definition nonempty | true; then metamonovalued ⇔ monovalued ⇔ weakly metamonovalued | Theorem 1.1, Proposition 4.2, Corollary 4.3 |
| The same; definition read literally (empty family admitted) | true; metamonovalued reloids are then exactly the principal reloids of maps A → B | Theorem 1.1, Remark 4.4 |
| Every weakly metamonovalued reloid is monovalued | true | Theorem 1.1 |
| S(S(f)) = S(f) and S(f)∘S(f) = S(f) for every endoreloid f; S with the identity term | false; the two equations are equivalent for each f | Theorem 1.2, Lemma 3.3(d) |
| S₁(f)∘S₁(f) ⊑ S₁(f) for every endoreloid f (S₁: no identity term) | false | Remark 5.3 |
| The same for principal reloids, in particular on finite sets | true | Proposition 5.2(a) |
| The same with S* in place of S | true (theorems of the book) | Proposition 5.2(b); book, Theorems 1251 and 1255 |
| S(S(f)) = S(f) and S(f)∘S(f) = S(f) for every endofuncoid f | false | Theorem 1.3 |

## Results in the paper
- **Conventions.** A reloid from A to B is a filter on A × B. The order is reverse inclusion of filters, the
  improper filter is the least reloid, composition is generated by the compositions of members with the first
  factor acting first, and S contains the identity term.
- **Lemmas 3.1–3.4.** Bases of meets, of compositions and of powers; a description of the filter of S(f);
  S(f) ⊑ S(f)∘S(f) ⊑ S(S(f)); a reloid is monovalued if and only if its filter has a single valued member.
- **Theorem 1.1.** With g the identity reloid of B and h the principal reloid of {(y, z) : y ≠ z}:
  (g ⊓ h)∘f = (g∘f) ⊓ (h∘f) if and only if f is monovalued. The left side is the least reloid. The right side
  has the base {F ∩ (N∘F) : F ∈ up f}, and F ∩ (N∘F) is empty exactly when F is single valued.
- **Proposition 4.2** (Porton's theorem, with a short direct proof): monovalued reloids satisfy the identity of
  metamonovaluedness for all nonempty families.
- **Remark 4.4.** The empty family: the condition becomes ⊤∘f = ⊤, which says that every member of the filter has
  full domain, that is, that f is entirely defined.
- **Remark 4.5.** Pairs of points, as used in the book for relations, do not detect all non-monovalued reloids.
  The pair of the first proof is recorded there.
- **Theorem 1.2.** U = ℕ ∪ {c₁, c₂, …}, P = {(i, i+1)}, F_j = P ∪ {(n, c_n) : n ≥ j}, f the reloid with the base
  {F_j}. The relation K = id ∪ ⋃_m (F_m)^m belongs to the filter of S(f) and not to the filter of S(f)∘S(f),
  because every member of the latter contains a pair (0, c_j).
- **Proposition 5.2.** What remains true: principal reloids; S*∘S* = S* and S(S*) = S*;
  S(f) ⊑ S(f)∘S(f) ⊑ S(S(f)) ⊑ S*(f).
- **Remarks 5.3 and 5.4.** In the example, S(f)∘S(f) = S(S(f)) = S*(f) (with the argument printed), and
  S₁(f)∘S₁(f) ⋢ S₁(f). Two further examples: on ℕ × ℝ (the first one found), and the translation by 1
  composed with the uniformity of ℝ.
- **Theorem 1.3.** For the funcoid φ defined by the same sets F_j: {0} [S(φ)∘S(φ)]* C holds and {0} [S(φ)]* C does
  not, where C = {c_n}. The proof uses only the definitions of the book (Definitions 29, 831, 834, 835, 839, 847,
  853, 877, 885 and 1220); the two facts on funcoids that it needs (Lemmas 6.1 and 6.2, which are Theorem 856 2°
  and Theorem 880 of the book for nonempty families) are proved in the note.

## Computations (sanity checks; scripts and outputs in reproducibility/)
No proof depends on a computation. On a finite set every filter is principal, so the programs test the
combinatorial steps of the proofs, not the statements about non-principal reloids and funcoids. All programs were
re-run on 2026-10-08 (Python 3.13.5, standard library); all checks passed.
- `verification_run_2/check_A.py`. All relations F ⊆ A × B with |A|, |B| ≤ 3 and all pairs of relations from B to
  C with |C| ≤ 3 (11,956,242 equality tests): the identity of weak metamonovaluedness holds for all pairs if and
  only if F is single valued (for C ≠ ∅). The single pair of Theorem 1.1. All nonempty families when
  |B|·|C| ≤ 4. The empty family.
- `verification_run_2/check_first_pair.py` and `verification_run_1/check_A_finite.py`. The pair of the first proof
  (Remark 4.5), on all 689 relations between sets with at most 3 elements.
- `verification_run_2/check_B.py`. All relations on at most 4 points satisfy S(S(F)) = S(F) = S(F)∘S(F). The
  path arguments of Theorem 1.2 and Remark 5.3 on a window of the example (indices up to 40).
- `verification_run_1/check_B_models.py`. Exact rational checks for the example of Remark 5.4(a), and a
  truncation of one further discrete example that is not printed in the note.
- `author/check_note.py`. The statements as printed in the note: Theorem 1.1 and Remarks 4.4, 4.5; the key step
  of Proposition 4.2; the closed formulas of Theorem 1.2 and Remark 5.3; Proposition 5.2(a) on at most 3 points;
  the band argument of Remark 5.4(b); the sets F_j[X] used in the proof of Theorem 1.3.
- `independent_run_2/` (third run; separate programs written from the statements of the note before the other
  scripts were read).
  - `run2_A_metamonovalued.py`: the checks of Section 4 again (689 relations; 12,014,204 pairs; 2,654,781
    nonempty families; the empty family; both test pairs; the example of Remark 4.5).
  - `run2_B_series.py`: 66,067 relations on at most 4 points; on the window 0..30 of the example the closed
    forms of (F_j)^m, of K and of S(F_j), Step 2, and Step 3 for all 65,536 pairs of members of a base of the
    filter of S(f) built from maps on {1..4}; exact rational checks for Remark 5.4.
  - `run2_C_funcoids.py`: all 66,077 pairs of maps between the power sets of sets with at most 2 elements; the
    funcoids among them are exactly those given by binary relations; Lemmas 6.1 and 6.2 hold on them; the sets
    F_j[X] of Theorem 1.3 on windows.
- The archive `source.zip` was extracted and `run_all.sh` was run from the extracted copy; the outputs agree with
  the packaged ones up to the lines that report running times.

## Independent verification runs
The two answers were first obtained with the test pair of Remark 4.5 and the example of Remark 5.4(a). Three
independent verification runs, all AI-assisted, followed on 2026-10-08: two before the note was written, and one
on the finished note.

| Item | First run (line-by-line check of the first proofs) | Second run (derivation before seeing the first proofs) |
|---|---|---|
| Definitions and item numbers against the book | CONFIRMED | CONFIRMED |
| Every (weakly) metamonovalued reloid is monovalued | CONFIRMED | CONFIRMED, with the test pair of Theorem 1.1 |
| S(f)∘S(f) ≠ S(f) and S(S(f)) ≠ S(f) for some endoreloid | CONFIRMED; added the example of Remark 5.4(b) | CONFIRMED, with the example of Theorem 1.2 |
| The statements answer the records and the book as posed | CONFIRMED | CONFIRMED |
| Earlier solution found | none | none |

Both runs found no mathematical gap in the first proofs. Their required corrections were all applied in the note:
1. Both numberings of the book are given, and the online copy was checked on the day of writing.
2. The series without the identity term is called S₁. S* is the book's different operator; its identities are
   theorems of the book and are consistent with the examples (Proposition 5.2, Remark 5.3).
3. The note says explicitly that Theorem 1.2 refutes part 1° of Conjecture 1253 and Conjecture 1254, and that
   these two are equivalent for each f. The funcoid statements are treated separately (Theorem 1.3).
4. The empty-family convention is stated. Theorem 1.1 holds under both readings; the converse and the three-way
   equivalence hold for nonempty families (Remark 4.4).
5. The converse is proved (Proposition 4.2) and cited precisely.
6. "Single valued relation (partial function)" is used instead of "function"; the equivalence of the two
   formulations of "monovalued" in the book is proved (Remark 3.5).
7. The base of the powers fⁿ is proved (Lemma 3.3(a)); the book leaves it as an exercise.
8. "Has the base" is used, with the directedness argument, wherever a filter base is needed.
9. The remark on finite sets is strengthened: no principal reloid on any set is a counterexample.

Both runs also concluded that the funcoid conjectures fail. Their arguments differ from each other and from the
note, and they rest on Theorems 856, 859 and 880 of the book, whose proofs the runs did not re-check. The proof of
Theorem 1.3 in Section 6 was therefore written from the definitions of the book alone.

**Third run (on the finished note).** It read the whole note line by line, read every cited item again on
rendered pages of the book, wrote its own programs before reading the packaged ones, and repeated the literature
search. Verdicts:

| Item | Verdict |
|---|---|
| Statement fidelity (book in both copies, Open Problem Garden, corpus records) | CONFIRMED |
| Proofs of Sections 2–5 (Theorems 1.1 and 1.2 and all lemmas, propositions and corollaries) | CONFIRMED (every proof checked line by line; no mathematical error) |
| Section 6: the equivalences (4), Lemmas 6.1 and 6.2, Theorem 1.3, Corollary 6.3 | CONFIRMED (no gap) |
| Cited items of the book (62 items, both numberings) and the credit to Mathematics Stack Exchange | CONFIRMED |
| Computations | CONFIRMED |
| Answers as posed (OPG-57403: yes; OPG-751: no) | CONFIRMED |
| Novelty | CONFIRMED as far as can be checked (no priority claim) |
| Presentation | CONFIRMED_WITH_FIXES |

For Section 6 the run compared the text with the book on rendered pages: intersecting elements (Def. 29, p. 19);
funcoids, ⟨f⟩, the reverse and [f] (Def. 831, 834, 835, 839, p. 172); composition and [f]* (Def. 847, 853,
p. 174); the order f ⊑ g ⇔ [f] ⊆ [g] (Def. 877, p. 180); joins of funcoids as least upper bounds in that order
(Thm. 880, p. 181); the identity funcoid (Def. 885, p. 184); the category of funcoids (Section 25.8, p. 186);
and the series S for endomorphisms of a category with countable joins of morphisms (Def. 1220, p. 256). All are
used in the note as they are defined in the book. The run also derived the two key facts a second time through
the relation [·]* alone: {0} [φⁿ]* Y holds if and only if n ∈ Y, and ℕ [φ]* C holds.

All required fixes of the third run were applied:
1. The Verification paragraph of the note states the final state of the checks.
2. Remark 5.3: the argument is printed in place of "One checks that" (the closed form of S(F_j) from the shape of
   the paths of F_j, and the reason for the S₁ statement).
3. Remark 4.5: the statement that the book's test pairs do not suffice is restricted to pairs of points, which is
   what the example shows. For two different non-principal ultrafilters the analogous product pair does detect
   that the reloid of the example is not monovalued, so the earlier wording claimed too much.
4. Remark 4.4: the credit to the Stack Exchange answer is made exact (accepted answer; it states without an
   example that counterexamples exist in the category of relations, and proves the implication for monovalued,
   entirely defined morphisms), and the agreement with the remark is stated (Def. 257 of the book).
5. Scope paragraph: the literature search is described as it was made (OpenAlex added; SciLag groups; web
   searches).
6. Section 6: one clause on how Def. 1220 applies to funcoids, and one clause in the proof of Lemma 6.2.
7. Page numbers added to five citations of the book.
8. This report, the reproducibility folder and the metadata were updated.

In addition the bibliography was set ragged right, which removed three loose lines.

## Relation to the literature, novelty and scope
- **Searches (2026-10-08; all requests anonymous).**
  - The online copy of the book: the four statements are still conjectures.
  - The author's site: the list of 554 posts (latest of 2026-02-09) and searches for "metamonovalued",
    "endoreloid" and "connectedness". The posts of 2013 introduce the notion and announce the converse theorem.
    A post of 2018-06-30 announces S*(μ)∘S*(μ) = S*(μ), which is a different statement. No post announces a
    solution of the statements treated here.
  - Open Problem Garden: the three pages above, without solutions.
  - SciLag: groups G-181201.1 (metamonovalued morphisms) and G-181201.3 (the four identities for S, for funcoids
    and for reloids), posted 2018-12-01; all member problems are listed as open, with no solutions. The entries
    P-181201.18 and P-181201.20 were also read.
  - arXiv API: no record for reloid, reloids, endoreloid, metamonovalued, funcoid, funcoids, endofuncoid.
  - zbMATH Open API: no record for reloid, reloids, endoreloid, metamonovalued, funcoid, funcoids, endofuncoid;
    two documents by the author of the book, on filters on posets.
  - Crossref: no record for the book under either title, for "reloid funcoid" or for "metamonovalued".
  - OpenAlex: for "reloid" and "funcoid" only texts of the author of the book (without DOI) and unrelated
    records; nothing for "metamonovalued".
  - Mathematics Stack Exchange, question 495672 (2013) with its accepted answer by the user Berci: about ordered
    categories in general. The answer states that counterexamples to "monovalued implies metamonovalued" exist in
    the category of relations and proves the implication for monovalued, entirely defined morphisms. This agrees
    with Remark 4.4 and is cited there. Nothing on reloids.
  - Web searches (six in all, by the three runs and at the writing): only the Open Problem Garden and SciLag
    listings and pages of the author.
- **Result.** No earlier proof of the conjecture and no earlier counterexample was found.
- **Caveats.** The theory has been developed essentially by one author, in a self-published book and on a blog.
  Not every post of the blog was read. Unindexed or private communications cannot be excluded. This negative
  search is not a proof of priority.
- **Scope.** The notions, the conjectures and the theorems quoted from the book are due to V. Porton. The note
  answers the two records as posed. It does not study how often S has to be iterated before it stabilises, and
  it does not discuss products of ultrafilters as test pairs for reloids.

## Public release and license
This paper, its source files, and this verification report are licensed under the Creative Commons Attribution
4.0 International License (CC BY 4.0): https://creativecommons.org/licenses/by/4.0/