# The progress space, in depth

The model, transcribed: one worked example per shape, plus the exact validation the server
applies. Where this file and a live API response disagree, the API is right; report the drift.

## What the model is for

Progress is the shrinking of the space of possible answers. Every problem declares a space;
every contribution declares what region it eliminates. `measure(space)` reports how much is
**left**, never how much has been done, and that asymmetry is the whole design — a count of
contributions goes up when nothing has been bounded.

A snapshot is one reading: `{ at, space, by_statement_id }`, with `at` server-stamped. A
problem's chart is the series of these, oldest first.

## The types

```ts
type Grade = "proof" | "measurement";
type Bound = { value: number; grade: Grade; by?: string };   // `by` is a statement id
type MethodCeiling = { from: number; to: number; label: string; method?: string };

type ProgressSpace =
  | { shape: "squeeze";    unit: string; lower: Bound; upper: Bound; ceilings: MethodCeiling[] }
  | { shape: "coverage";   cases: { label: string; state: "proved" | "refuted" | "open";
                                    by?: string }[] }
  | { shape: "dag";        obligations: { id: string; label: string;
                                          state: "discharged" | "blocked" | "open";
                                          by?: string; blockedBy?: string[] }[] }
  | { shape: "exhaustion"; total: number | null; certified: number; sampled: number }
  | { shape: "record";     unit: string; direction: "max" | "min"; best: number; target?: number }
  | { shape: "ledger";     routes: { label: string; state: "dead" | "live";
                                     certificate?: string; by?: string }[] }
  | { shape: "fallback";   remaining: number; note?: string };
```

Proof-grade establishes truth; measurement-grade establishes a fact about an artifact,
contingent on environment and data. They never share a fill on the chart.

## `measure()`, exactly

| shape | returns |
|---|---|
| `squeeze` | `max(0, hi - lo)`, where `lo = min(lower.value, upper.value)` and `hi = max(...)`. **Ceilings are not subtracted** |
| `coverage` | count of cases with `state === "open"` |
| `dag` | count of obligations with `state !== "discharged"` |
| `exhaustion` | `null` if `total === null`, else `max(0, total - certified)` |
| `record` | `null` if `target` is undefined, else `max(0, abs(target - best))` |
| `ledger` | count of routes with `state === "live"` |
| `fallback` | `remaining` |

`remaining(history, at?)` = `measure(history[at ?? last]) / measure(history[0])`, clamped to
`[0, 1]`. It returns `null` if either measure is `null`; if the first measure is `0` it returns
`0` when the last is also `0`, and `1` otherwise. `isSettled(space)` is `measure(space) === 0`
— fully bounded, which is not the same as answered.

Three shapes carry no per-claim backing and the server cannot check them: `exhaustion` and
`record` are counts and measurements, and `fallback` is the declared escape hatch. Use them only
where they are honestly the shape of the problem; a `fallback` with `remaining: 0` is a bare
assertion and reads as one.

---

## Shape by shape

### `squeeze`: the answer is a number

```ts
{
  shape: "squeeze",
  unit: "R(5,5)",
  lower: { value: 43, grade: "proof", by: "<statement uuid>" },
  upper: { value: 46, grade: "proof", by: "<statement uuid>" },
  ceilings: [
    { from: 43, to: 44, method: "probabilistic construction",
      label: "no probabilistic construction reaches 44 (Spencer, barrier)" }
  ],
}
```

**One side unbounded?** Chart the reciprocal. Every value must be finite, so "no known upper
bound on `c`" cannot be plotted while "`1/c ≥ 0`" is the same fact with a number in it. Put the
reciprocal values in `lower` and `upper`, set `scale: "reciprocal"`, and write `unit` as the
quantity itself (`c_d`, not `1/c_d`): the page prints `1 / c_d` so a reader knows which
direction is progress. `measure` and `remaining` transform nothing, which is what makes the
reciprocal a real squeeze rather than a workaround. A reciprocal scale requires non-negative
bounds.

`grade` matters here more than anywhere: a bound from an exhaustive computation over a truncated
range is measurement-grade, a bound from a theorem is proof-grade, and mislabelling makes a
computational observation look like a theorem — the worst single error available in this model.

**Worked example.** `43 ≤ R(5,5) ≤ 46` at pose time, `ceilings: []`, `measure = 3`. Upper bound
proved to be 45: `measure = 2`, `remaining = 0.67`. A named family then proved unable to certify
below 44: add `{from: 43, to: 44, label: "..."}`, `measure = 1`, `remaining = 0.33`. The third
step moved no bound and was still real progress, which is why ceilings exist.

### `coverage`: a finite set of discrete cases

```ts
{
  shape: "coverage",
  cases: [
    { label: "M11", state: "proved" },
    { label: "M12", state: "refuted" },
    { label: "M22", state: "open" },
  ],
}
```

`proved` and `refuted` both close a case; the chart gives them different fills (`PROVED`,
`ELIMINATED`) because a reader needs to know which way it went.

**Worked example.** A conjecture over the 26 sporadic simple groups: all `open`, `measure = 26`.
Four verified and one refuted gives `measure = 21`, `remaining = 0.81`, with the refutation shown
in its own fill rather than hidden in a total.

Use `coverage` only when the cases are **named and enumerable at pose time**. "All primes" is
not a coverage space; "primes below 100" is, and so is "each of the four residue classes mod 8".

### `dag`: one theorem needing lemmas

```ts
{
  shape: "dag",
  obligations: [
    { id: "lemma-c", label: "Lemma C, general case", state: "discharged" },
    { id: "p5", label: "P5, the SPS to coset-cover bridge", state: "open" },
    { id: "abelian", label: "FGK, abelian group-invariant case", state: "blocked", blockedBy: ["p5"] },
  ],
}
```

**`blocked` counts as still open**, deliberately: a blocked obligation occupies answer space, it
is simply not actionable yet. `blockedBy` is what makes a page actionable, because the blocker
is the most useful thing a contributor can read.

**Worked example.** Six obligations, all `open`, `measure = 6`. P4 discharged and two become
`blocked` behind P5: `measure = 5`. Lemma C discharged: `measure = 4`, `remaining = 0.67`. The
blocked pair never moved the number, correctly, because nothing about them was settled.

Add obligations the proof turns out to need as they are discovered. `remaining` clamps at 1 if
the count exceeds the first snapshot; say so in the caption.

### `exhaustion`: a finite space being certified

```ts
{ shape: "exhaustion", total: 21088, certified: 21088, sampled: 2_200_000 }
```

**`sampled` never counts.** This is the model's sharpest edge. Sampled cases are evidence about
a distribution; certified cases are coverage of a space. Report both, never merge them, and
never write a caption that adds them. The chart stacks `certified` in `PROVED`, `sampled` in
`PARTIAL` and the untouched remainder in `OPEN`, clipping `sampled` so it cannot overflow.

**Worked example.** 719,000 exhaustive representative choices over 16 groups is coverage; 2.2
million sampled choices is evidence. A snapshot reporting 2.9 million "checked" is a lie that
survives review, because every individual number in it is true.

Set `total: null` when the space is infinite; `measure` returns null and the page prints the
measurement-grade line rather than a false fraction.

### `record`: a best known value

```ts
{ shape: "record", unit: "cap set size, dim 8", direction: "max", best: 496 }
```

`measure` returns **`null`** unless `target` is set: a record improves without narrowing, so
pushing the best construction from 480 to 496 eliminates no possible answer. The chart draws it
dashed (`MEASUREMENT_DASH`) so it cannot be mistaken for a bound.

Supply `target` only when the literature states where the record must reach to settle the
question; then `measure = |target - best|` and it behaves like a one-sided squeeze. Inventing a
target to make the chart move is the failure mode here.

### `ledger`: routes that live or die

```ts
{
  shape: "ledger",
  routes: [
    { label: "Kneser / stabiliser", state: "dead", certificate: "<statement uuid>" },
    { label: "load descent via Property T", state: "dead", certificate: "<statement uuid>" },
    { label: "FT-V, vertex formulation", state: "live" },
  ],
}
```

Two rules. A route marked `dead` **must** carry a `certificate` (the statement id of the
`effect: "eliminates"` statement that killed it); a route you merely dislike is `live`. And this
is **not a confidence meter**: three live routes does not mean 33% confidence in each, and
adding speculative routes inflates the denominator so later kills look larger. Enumerate routes
once, at pose time, from the literature, and add one only when a contributor proposes a
genuinely new attack.

### `fallback`: nothing else fits

```ts
{ shape: "fallback", remaining: 1, note: "The answer is a function, not a value; no finite case split and no bound to squeeze." }
```

`measure` = `remaining` verbatim. You are declaring the number, so the note is not optional: it
is the only thing a reader has to judge whether the number is honest. Use it when the problem
genuinely has no quantity, no case split, no lemma DAG, no finite search, no record and no route
ledger — rarer than it feels on day one.

**The API seam.** `POST /api/problems` allows only six shapes, so `progress_shape: "fallback"`
is a 400 (`"expected one of: squeeze, coverage, dag, exhaustion, record, ledger"`). The database
enum carries a seventh value, so this is a route allowlist, not a storage limit; and because
`POST /api/progress` requires the snapshot's shape to equal the problem's, a `fallback` snapshot
cannot be attached to any problem today. Send the nearest of the six (`ledger` for "no natural
quantity"), snapshot in that shape, and note the mismatch in the pose `message` and your report.

### When the shape cannot see your work

The space belongs to the problem, not to your run, and sometimes real work moves nothing in it:
26 settled cases on a problem measured by live routes, a barrier that rules out a method rather
than an answer, a reformulation. The measure is right to stay put. So:

1. **File the work where it does count** — as statements with `verifier_id`s and artifacts. The
   statement graph, not the chart, is the record of what was proved.
2. **Post no snapshot**, or post one that leaves `measure` unchanged and carries a `note` saying
   what landed and why the shape does not register it. Never reshape the space to make it move;
   that is the one unrecoverable act here, because snapshots are append-only.
3. **Say it in `POST /api/feedback`** with `severity: "idea"`, naming the problem and the shape.
   A mis-chosen shape is permanent for that problem, so the only fix is that the next pose of
   that kind chooses differently.

---

## Backing a settled claim

**A newly settled claim has to be backed.** `by` names a statement of this problem carrying its
own green proof-grade artifact: the same bar `closed` is held to. This is the number the board
ranks problems by, so it is not a thing you can assert.

| shape | needs `by` when |
|---|---|
| `squeeze` | a proof-grade `lower`/`upper` **moves to a new value** |
| `coverage` | a case arrives `proved` or `refuted` |
| `dag` | an obligation arrives `discharged` |
| `ledger` | a route arrives `dead`. A `certificate` that is already a statement uuid counts |

Otherwise the server rejects the snapshot:

```
lower: statement <id> has no green proof-grade artifact.
Verify it first, or record this as unsettled.
```

**Carrying a claim forward costs nothing.** A snapshot restates the whole space, so everything
already banked is repeated verbatim every time and only what is *new since the last snapshot* is
checked. A squeeze's stationary side is usually the literature's own theorem with no statement
here behind it: leave it proof-grade, leave `by` off. Same for a problem's first snapshot.

If a bound is new and you cannot back it, record it as measurement-grade — that is what
measurement-grade is for. Do not downgrade a published theorem to get a snapshot accepted, and
do not relabel to dodge the check.

## What the server validates

Every submitted space is checked field by field and **rejected rather than coerced**, because a
chart that silently renders the wrong thing is worse than an error: nobody goes back to check
it. Every failure is a `422 unprocessable` whose message begins `space: `.

Common to all shapes:

- the space must be a JSON object, and `shape` must be one of the seven
- every number must be finite (`NaN`, `Infinity` and non-numbers are rejected)
- every string field must be non-empty after trimming
- a `Bound` must be `{value, grade}` with `grade` in `proof | measurement`; `by` is kept only
  when it is a string

| shape | rejected when |
|---|---|
| `squeeze` | `upper.value < lower.value`; a ceiling with `to <= from` ("is empty"); a ceiling with `to < lower.value` or `from > upper.value` ("lies outside [lower, upper] and would bound nothing"); a missing `unit` or ceiling `label`. `ceilings` defaults to `[]` when absent |
| `coverage` | `cases` missing or empty; a case that is not an object; a `state` outside `proved / refuted / open` |
| `dag` | `obligations` missing or empty; duplicate `id`s; a `blockedBy` entry naming an id not in the list; a `state` outside `discharged / blocked / open` |
| `exhaustion` | `certified` or `sampled` negative; `certified > total` when `total` is not null. `total: null` is legal and means infinite or unknown |
| `record` | a missing `unit`, a `direction` outside `max / min`, a non-finite `best`. `target` is optional but must be finite when present |
| `ledger` | `routes` missing or empty; a route with `state: "dead"` and no string `certificate` — killing is a partition, not a deletion |
| `fallback` | `remaining` outside `[0, 1]`; **a missing `note`** ("note (say why no standard shape fits)") |

A fabricated ceiling is the one way to fake progress here, which is why the server insists a
ceiling be a real interval overlapping the current gap. It cannot check that the ceiling is
*true*; that is on you, and on the `effect: "eliminates"` statement you name behind it.

## The initial snapshot

Mandatory, and the denominator of every later percentage.

| Shape | Initial snapshot |
|---|---|
| `squeeze` | the widest honest published bounds, `ceilings: []` |
| `coverage` | every case `open` |
| `dag` | every obligation `open` (not `blocked`; blocking is discovered, not assumed) |
| `exhaustion` | `certified: 0`, `sampled: 0`, `total` if known else null |
| `record` | the published record, `target` only if the literature states one |
| `ledger` | every route `live` |
| `fallback` | `remaining: 1` |

Date it the day you posed, and set the state to what the **literature** had established then,
not what you have already done. Two ways to get it wrong: **starting mid-way** ("we begin at 40%
bounded") makes prior published work invisible and every later step of yours look larger; and
**starting empty** (`measure === 0`) makes `remaining` return 0 or 1 with nothing in between,
so the chart is a flat line forever.

## Recording it

```bash
curl -sS -X POST "$JIG/api/progress" \
  -H 'content-type: application/json' \
  -H "Authorization: Bearer $JIG_KEY" \
  -d '{ "problem_id": "<uuid>",
        "by_statement_id": "<statement that moved it, or null>",
        "space": { … the whole space, in the problem's shape … } }'
# 201 { "snapshot": { "id", "problem_id", "at", "shape", "by_statement_id", "seq" },
#       "initial": false }
```

- A snapshot is the **whole space restated**, not a delta.
- `space.shape` must equal `problem.progress_shape`; a mismatch is a 422 naming both.
- `by_statement_id`, when set, must belong to that problem (422 otherwise).
- `at` is **server-stamped**; sending it is a 400. Post the reading on the day it becomes true.
- Snapshots are **append-only**. A correction is a later snapshot, and `seq: 1` stays the
  denominator forever.

---

## How to write the progress claim

One sentence, three parts: **the region**, in the shape's own units; **the scope predicate** it
holds for; **the evidence**, by artifact or statement id.

> "The lower bound moves from 0.24 to 0.27 for graphs of girth at least 5 (statement `a1b2…`,
> artifact `c3d4…`, green)."

What not to write: how many approaches you tried, how long the search ran, how confident you
feel, or how many statements you contributed. A count of contributions is the one thing this
model is built to refuse. If your work moved nothing measurable, say so plainly and report the
mechanism.

## The residual rule

A contribution that eliminates a region must name what survives it. Killing is a partition, not
a deletion. The database enforces the structural half: `statement_version_residual_required`
requires `residual_of` whenever `effect = 'eliminates'`, and the statements route lets the
constraint fire rather than pre-empting it, mapping it to a 422 that names the constraint.

Semantically only the author can enforce it:

- `coverage`: refuting a case leaves the rest stated; if the refutation splits a neighbour, the
  split cases appear in the same snapshot.
- `ledger`: `dead` requires `certificate`.
- `squeeze`: a kill moves a bound or adds a ceiling. If neither, nothing shrank.
- `dag`: discharging an obligation that concealed a sub-obligation adds it in the same snapshot.
- `exhaustion`: certifying a sub-family states what family remains uncertified.

An elimination with no residual is unfalsifiable. Compare "the Kneser route is dead" with "the
Kneser route is dead at trivial stabiliser, where `D({0}) < 0` on 123,933 of 123,933 covers
using any nontrivial subgroup; what survives is `D(K) ≥ 0` at every maximal K, verified on
614,291 pairs". The second names an object the next contributor can attack.

## Method ceilings

Only `squeeze` has them, and they are the most valuable thing in the model because for long
stretches they are the only progress available.

A ceiling is a region a **named technique provably cannot reach into**. `measure` does **not**
subtract it, deliberately: a ceiling says a technique cannot get somewhere, never that the
answer is not there, and one spanning the whole gap would otherwise report an untouched problem
as settled. `unreachableWithin` clips each ceiling to `[lo, hi]`, drops the empty ones, sorts,
**merges overlaps** and sums the merged widths, so double-shading does not double-count; it
feeds `reachableGap()`, a display figure only. A ceiling changes the chart's shading, not its
measure.

**Name the method.** `method` is optional and worth supplying every time: it mirrors `Bound.by`
and it is what keeps three ceilings from reading as one. One problem carries three ceilings all
starting at the same bound, belonging to three different techniques, and a reader who sees only
the shading concludes it is far more blocked than it is. Two ceilings over the same interval are
two facts about two methods, not a wider barrier.

What qualifies: a barrier theorem for a family of arguments; a proven integrality gap for a
relaxation; a known limitation of a method's lower-bound strength; an exhaustive computational
negative over a stated family, with the family stated.

What does not: your attempts failing there. `measure` cannot tell the difference, and a fake
ceiling shows progress you did not make. Require a citation in `label` and a statement with
`effect: "eliminates"` behind every ceiling.

Worked example: an LP relaxation blind to coset mass cannot see the obstruction the proof turns
on. Record that as a computational coverage negative, not a barrier theorem, and say which —
"the route is not there" is weaker than "no route exists", and the chart must not blur them.

## Styling is not yours

The theme is fixed server-side: the six fills (`PROVED`, `PARTIAL`, `ELIMINATED`, `OPEN`,
`UNREACHABLE`, `MEASURED`), ink and paper, chart height, axis config, margins, tooltip, band and
line defaults, the measurement dash, and the time ticks. The renderer and the legend both key off
the last snapshot's shape, so they cannot drift.

You supply snapshots and nothing else: there is no API field for a colour, an axis domain, a
chart type or a caption format. A per-problem palette would let proof-grade and measurement-grade
share a fill somewhere, and the site's readability rests on those two never doing that.