ExampleConstruction: AI-generatedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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 split coequalizer on a two-element set

Example

Let $X = Y = {0, 1}$ and $Z = {*}$ . Define $g = t = 1_{Y}$ , let $f : X \to Y$ be constant at $0$ , let $h : Y \to Z$ be the unique map, and put $s (*) = 0$ . Then

$X \begin{array}{c} \overset{f}{\to} \\ \to_{g}^{} \end{array} Y \overset{h}{\to} Z$

with $t$ and $s$ is a split coequalizer in $S e t$ .

Facts & Assumptions

Given: The displayed finite sets and functions.

[L1]

A split coequalizer satisfies $h f = h g$ , $h s = 1_{Z}$ , $g t = 1_{Y}$ , and $f t = s h$ (Split coequalizer diagrams).

[L2]

Every split coequalizer is a coequalizer and an absolute colimit (Every split coequalizer is a coequalizer and an absolute colimit).

Verification

technique · direct

1.1

The maps are $f (0) = f (1) = 0$ , $g (0) = 0$ , $g (1) = 1$ , $t = g$ , $h (0) = h (1) = *$ , and $s (*) = 0$ .

construct

2.1

Both $h f$ and $h g$ are the unique map to $Z$ ; $h s (*) = *$ ; $g t$ is the identity on $0$ and $1$ ; and both $f t$ and $s h$ are constant at $0$ . Thus all four equations in [L1] hold on both elements.

step 1.1L1algebra

3.1

By [L2], the displayed fork is a coequalizer.

step 2.1L2

4.1

Directly, if $k : Y \to W$ satisfies $k f = k g$ , then $k (0) = k (y)$ for both $y = 0, 1$ , so $k$ is constant and factors uniquely through $h : Y \to {*}$ . This independently checks the universal property.

step 1.1construct∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.