ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A floor-division and multiplication adjunction between natural-number preorders

Example

Fix $m \in N$ with $m > 0$ . On the preorder $(N, \leq)$ define

$F (n) = m n, G (r) = ⌊ \frac{r}{m} ⌋ .$

Then $F ⊣ G$ . Its unit and counit are $n \leq G (F (n))$ and $F (G (r)) \leq r$ , and in fact $G (F (n)) = n$ , $F G F = F$ , and $G F G = G$ .

Facts & Assumptions

Given: Natural numbers $m, n, r$ with $m > 0$ .

[F1]

The natural numbers are the smallest inductive set, with $0 = \emptyset$ and successor $σ (n) = n \cup {n}$ (The natural numbers $N$ (von Neumann)).

[F2]

Natural order is defined by $a \leq b$ exactly when $a + d = b$ for some $d \in N$ (Order on the natural numbers).

[F3]

Natural multiplication is determined by $a \cdot 0 = 0$ and $a \cdot σ (b) = a \cdot b + a$ (Multiplication of natural numbers).

[F4]

For integers $a$ and $b > 0$ , there is a unique pair $(q, s)$ with $a = q b + s$ and $0 \leq s < b$ ; moreover $b$ divides $a$ exactly when $s = 0$ (Division with remainder in $Z$ : for $a \in Z$ and $b > 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < b$ ).

[F5]

A Galois connection between preorders satisfies $F (a) \leq b$ exactly when $a \leq G (b)$ , with unit $a \leq G F (a)$ and counit $F G (b) \leq b$ (Galois connection between preorders).

Verification

technique · direct

1.1

Apply [F4] to $r$ and $m$ , viewing naturals as nonnegative integers, and write uniquely $r = q m + s$ with $0 \leq s < m$ . Define $G (r) = q$ .

F1F4construct

2.1

If $m n \leq r$ , [F2] gives $r = m n + d$ . Divide $d$ by $m$ as $d = t m + s^{'}$ with $0 \leq s^{'} < m$ . Then $r = (n + t) m + s^{'}$ , so uniqueness in [F4] gives $q = n + t$ and $n \leq q$ .

step 1.1F2F3F4algebra

2.2

Conversely, if $n \leq q$ , write $q = n + t$ by [F2]. Then $r = q m + s = m n + (t m + s)$ , so [F2] gives $m n \leq r$ . Hence $F (n) \leq r$ exactly when $n \leq G (r)$ .

step 1.1F2F3algebra

3.1

The equivalence in steps 2.1 and 2.2 is the condition [F5], so $F ⊣ G$ . Taking $r = m n$ gives quotient $n$ and remainder $0$ , hence $G (F (n)) = n$ ; the counit is $m G (r) \leq r$ .

step 2.1step 2.2F4F5

4.1

The equality $G F = 1$ gives $F G F = F$ , while applying $G$ to the counit formula and using the quotient $q = G (r)$ gives $G F G = G$ . When $m = 1$ , every remainder is $0$ and both maps are the identity; the assumption $m > 0$ excludes division by zero.

step 3.1F4∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 51 results over 18 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Tom Leinster, Basic Category Theory, Section 2.1 (standard reference, not scraped)