# Style and proof-engineering guide

The accumulated lore of this library: how to state a reduction, how to build a
gadget, how to write a certificate annex, and the tactic failures that recur
here often enough to be worth naming. `CLAUDE.md` holds what is true of every
session — build, architecture, file layout, the handful of conventions that
shape every file. This holds what is true of a *particular* job.

Read the relevant section before starting:

| Doing this | Read |
| --- | --- |
| Adding a catalog entry (a new problem) | [Stating a problem](#stating-a-problem) |
| Writing a reduction's correctness proof | [Stating a reduction](#stating-a-reduction) |
| Building a gadget (a new graph/set/formula from an old one) | [Building a gadget](#building-a-gadget) |
| Writing a `Code.lean` / `Adequacy.lean` / `Certified.lean` | [Certificate annexes](#certificate-annexes) |
| Connecting a domain's bundled problems to their concrete encodings | [Representation theorems](#representation-theorems) |
| Anything, when a tactic misbehaves | [Tactic failure modes](#tactic-failure-modes) |
| Adding a `Code` constructor | [Adding a `Code` primitive](#adding-a-code-primitive) |
| Updating `README.md` or writing a file's top docstring | [Prose: timeless and even](#prose-timeless-and-even) |

New lessons land here, not in `CLAUDE.md`, and land at the same time as the
work that taught them. The bar: a lesson is worth writing down when it cost
more than a few minutes, would cost that again, and is expected to *recur* —
a pattern of the library, not the internals of one reduction (those belong in
that file's docstring). State the rule, one sentence of why, and cite the
precedent, so the next reader can go look at working code.

## Stating a problem

A catalog entry owes its *future* gadgets two lemmas. Both get crossed twice by
every reduction into the problem, so stating them once at the entry is what
keeps them out of the annexes. What it does *not* owe them is a third one on
spec: a transport lemma with no client is not infrastructure but a claim about
what the next gadget will want, and the claim is usually wrong. Three entries
of the packing–scheduling axis each carried an `exists_…_ofFn_iff` that nothing
ever called, while what their reductions actually needed was the enumeration
form (`sequencing_iff_of_enum`). Add the lemma with the reduction that consumes
it, as the engine adds a combinator with the certificate that needs it.

- **A renaming-invariance lemma**, whenever a gadget will *tag* the problem's
  elements (`matching3D_iff_of_equiv`, `colorable_iff_of_equiv`). This is what
  lets a certificate transport a tagged construction onto positions, and every
  later reduction into the problem reuses it. State it with the
  adjacency/membership correspondence as a *hypothesis*, not a bundled iso —
  that is the form certificates produce, and the representation layer consumes
  the same form.
- **An unbundling lemma**, whenever mathlib offers only a bundled form
  (`colorable_iff_exists_fun` turns `Colorable` into the bare separating
  function both directions of every proof actually use).

Further rules for the statement:

- **An indexed witness costs one extra transport lemma.** If the witness type
  mentions `Fin (Fintype.card x.V)` (TSP's tour), renaming the elements renames
  the witness's *index type* too: the invariance lemma transports along
  `finCongr (Fintype.card_congr e)`, and whatever index operation the statement
  uses must be shown to commute with a cast (`cast_finRotate`).
- **An arrangement problem is stated over positions and *built* in a
  convenient order.** A gadget knows relative placement, not absolute
  positions, so an entry whose witness is an arrangement owes an unbundling
  lemma saying an injection into *any* `LinearOrder` suffices
  (`exists_btw_of_key`: positions are recovered by counting predecessors). The
  gadget then keys into `ℕ ×ₗ ℕ`, the second coordinate reserving room *inside*
  a slot, and every comparison is `omega` on two coordinates — where a
  `gap * slot + offset` layout is nonlinear and `omega` cannot see it.
- **Cyclic successors are `finRotate`, not `· + 1`** — `(1 : Fin n)` needs a
  `NeZero n` instance, which a statement quantifying over a possibly-empty
  carrier cannot supply. `Cycle.lean` converts `finRotate` to the `if`-form a
  certificate computes.
- **State the sharpest restriction your construction actually delivers**, even
  when a sibling entry states a weaker one (3SAT: width `≤ 3`; NAE3SAT: width
  `= 3`). A restriction is a *theorem about the reduction into it*; weakening
  it to match a neighbour throws away hardness already proved, which a
  descendant would have to win back. Say in the docstring why the two differ.
- **A counting predicate needs a counting twin of every transport lemma the
  entry family already has.** A count is invariant only under maps preserving
  the counted objects one for one, so none of the satisfiability lemmas
  transfer (the `numSat_…` lemmas of `Logic/MaxSat.lean`). The twins are
  short, but there is one per transport lemma and the representation pair
  needs them all.
- **Two functions on one index set: carry one list of pairs, not two parallel
  lists.** Parallel lists mean a length-agreement side condition, and the
  decoding discipline admits none; pairing puts the agreement in the type,
  the certificate needs no branch, and the round trips are `rfl` (KNAPSACK's
  `(size, value)` pairs).
- **Define the problem as the literature defines it, never as the thing the
  reduction into it proves.** CLIQUE COVER is a partition into cliques,
  *equivalent* to `Gᶜ.Colorable k`; the second definition would have made the
  reduction from K-COLORABILITY true by `rfl` and proved nothing. The tell: a
  reduction whose correctness proof is `Iff.rfl` has a definition that
  absorbed the theorem. MULTIPROCESSOR SCHEDULING is the same choice made
  again: start times with a load bound, as Garey–Johnson state it, and *not* a
  partition of the tasks into `m` groups — which would have been BIN PACKING
  under another name, and would have thrown away the interval-colouring
  argument that is the entry's whole content.
- When several entries ask *different questions of the same Garey–Johnson
  instance*, they share one instance type and one encoding
  (`SetSystemInstance`; `GraphThresholdInstance`), and each entry file holds
  only its question.
- **Share the encoding, not the abstract instance type: an abstract instance
  carries no field its problem never reads.** When an entry asks a question of
  *almost* the shared instance — the same data minus the threshold, because
  Garey–Johnson give it no bound `K` — it gets its own instance type, joined to
  the shared one by a forgetful map and a junk-supplying one
  (`GraphThresholdInstance.forgetThreshold` / `GraphInstance.withThreshold`,
  and the same pair for `SetSystemInstance` / `SetFamilyInstance`). The saving
  that tempts the other choice — one encoding, one decoder, one round trip — is
  had anyway: the `Ty` encoding stays shared, the decoder composes with the
  forgetful map, and the representation pair supplies `0` on the way in and
  forgets it on the way back. That pair is then the *theorem* that the junk is
  junk, where an unread field on the abstract instance is only a hope. The tell
  that the line was drawn in the wrong place: an abstract reduction *into* the
  entry has to invent a threshold nobody reads.
- **Dot notation does not see the `Hardness` namespace.** An operation on a
  mathlib type declared inside it is `Hardness.Digraph.Acyclic`, and
  `D.Acyclic` fails to elaborate — generalized field notation resolves against
  the type's root name only. Dot notation on a *hypothesis* still works
  (`h.mono`, for `h : Digraph.Acyclic D`), so pick names that read prefix-style
  and spell them out in statements. Declaring into mathlib's own namespace buys
  the notation at the price of a collision with whatever mathlib adds there
  later, which for an API their TODOs already ask for is not a remote risk.

## Stating a reduction

State the mathematical content as a standalone lemma over **unbundled data**
(`exists_indepSet_iff_exists_vertexCover`), then define the `Reduction` with a
trivial glue proof. This avoids fighting structure projections and keeps the
interesting mathematics reusable.

- **Reducing *from* a restricted problem: collapse the out-of-range case, do
  not truncate it.** A gadget reading a bounded-size object must still be
  total, and the tempting reading — take the first three literals of a wide
  clause — produces a spurious yes-instance. Send the out-of-range input to
  something the target rejects instead (`pad3`); the restriction is then
  *reflected* rather than assumed — the backward direction derives the bound
  (precedent: `naeSatisfiable_naeSplit_iff`).
- **When the instance map builds a canonical object out of a *number*, state
  the lemma about a hypothesis characterizing that object, never about the
  canonical representative.** CLIQUE → SUBGRAPH ISOMORPHISM sends `(G, k)` to
  `(G, K_k)`, but the certificate cannot build `K_k` from a binary `k` — the
  size model forbids a list whose length is an input number — so it cuts the
  pattern out of the host's own vertex list and its pattern is neither `⊤` nor
  on `Fin k`. A lemma stated for `⊤` on `Fin k` would have been unusable, with
  an isomorphism to prove in its place; stated with "adjacency is disequality"
  and `Fintype.card W = k` as hypotheses, it serves both layers. This is the
  unbundled-data rule sharpened by the size model, and it recurs for any
  Garey–Johnson problem whose instance mentions a *structure of size k*.
- **A restriction a gadget cannot weaken away is reflected by an unsatisfiable
  *emitted object*, not by a branch.** A width-blind gadget composes
  `ofRestrict` in front (`naeSatToSetSplitting`, which reads clauses of any
  width). One that reads exactly `w` slots per clause cannot, and the fix is
  not a branch: emit one degenerate object per off-width clause — BETWEENNESS's
  triple `(centre, centre, centre)`, which no arrangement satisfies — so the
  program stays branch-free and the restriction is *derived* in the backward
  direction. This is "guard junk with the threshold, not with the
  construction", carried to problems that have no threshold.
- **A data-preserving reduction still has to be checked on the degenerate
  instances, and the `ℕ`-for-`Z⁺` convention is where they bite.** Bin packing
  and multiprocessor scheduling ask the same question of the same data — but an
  item of size *zero* still has to be put in some bin, while a task of length
  zero is invisible to every load count, so at `bins = 0` the "identity"
  reduction sends a no-instance to a yes-instance. Two habits follow: enumerate
  the instances where a *count* field is zero before believing a map is the
  identity, and fix the divergence by emitting different data in that branch
  (here, unit lengths, which no processor can run) rather than by restricting
  the source problem — a restriction would have to be justified, and this one
  could not be.
- The *direction* of a threshold decides what must be proved about the naming
  maps: minimization (`s.card ≤ k`) needs only `Finset.card_image_le`;
  maximization (`k ≤ s.card`) needs **injectivity**. One construction can
  serve both (the vertex-star system covers and packs), so state the
  injectivity next to the construction, not inside one reduction.

## Building a gadget

Fresh names are *tagged tuples of input objects*, realized as dependent pairs
or sum types (`CNF.Occ φ` = clause index × position), never generated counters.
Beyond that:

- **A problem with no symmetry to exploit pays for it in clauses, once.**
  NAE3SAT pins a variable to `false` for free, by complementing the assignment
  (`CNF.exists_naeSat_eq_false`); exactly-one satisfaction has no such
  symmetry, so ONE-IN-THREE 3SAT buys the same convenience with a three-clause
  block over four fresh variables (`falseBlock`). Being input-independent, such
  a block is a *constant* on the certificate side and belongs at domain level,
  shared by every reduction that needs it — not rebuilt per annex.
- **Present a gadget's edges (or sets, or triples) as an explicit list with a
  `mem_…` characterization** (`colorEdges` / `mem_colorEdges`), not as a
  `Prop`-valued relation: the list is the shape the certificate must
  reproduce, and a relation hits instance-search failures on its first family.
  But a structure that is only ever a *witness inside a correctness proof* —
  never emitted, never counted, never certified — should be a relation, or the
  list obligations (`Nodup`, faithfulness, size) are proved for nothing
  (precedent: `chosenGraph`, HAMILTONIAN CIRCUIT). The test: "list" exactly
  when the certificate will reproduce it.
- **Prefer local characterizations to global objects.** When the target theory
  has one (`IsCycles`: every node has exactly two neighbours), prove the
  per-node statement and let the packaging lemma produce the walk. And when a
  count would need "each edge has exactly one end of such-and-such kind"
  before it could be fibred, count *incident pairs* instead of edges.
- **Route each family's counting obligations through
  `Graph/EdgeFamily.lean`.** Every family flattens to an index list plus one
  emitted edge per index, and the kit supplies length, `countP` transport,
  looplessness, and `Nodup`-of-`edgeSyms` once and for all. Apply it as a
  *view* — keep the flat definition canonical and prove one
  `family = fam.list` equation per family. The one real obligation per family
  is `SymInjOn`, discharged by `symInjOn_of_rank` under a single gadget-wide
  rank, *except* for a family joining two vertices of the same shape — no
  rank can orient an input-derived pair, and such a family spends the input's
  `Nodup` there instead. Cross-family obligations are
  `EdgeFamily.disjoint_edgeSyms` + `nodup_edgeSyms_append`, closed by
  constructor discrimination.
- Build each family with `flatMap` of a list literal, never `List.map`:
  `List.mem_map` produces the *reversed* orientation (`f a = p`) while
  `List.mem_cons` produces `p = a`. One orientation everywhere and the
  characterization closes by `simp only […, exists_or, or_assoc]`; a mismatch
  forces `tauto`, which times out on a wide disjunction.
- **Name the `Fintype` and `DecidableEq` instances of a structured gadget
  type** (`instDecidableEqColVtx`): search finds `DecidableEq X` and then
  fails on `DecidableEq (X × X)`. List membership is decided through
  `LawfulBEq`, which is *not* reachable for such types — decide the bounded
  existential instead (`decidable_of_iff (∃ p ∈ l, p = a) …`).
- **Seed a chain at a fresh vertex forced to the constant, not at the constant
  itself.** The degenerate case becomes a genuine edge rather than an
  inexpressible self-loop, and the construction stays uniform — it is what
  lets SAT → 3-COLORABILITY handle the empty clause with no width restriction
  and no case split.
- **Describe a chain positionally, not recursively** (`chainAt i j`): the
  construction stays flat — so the `Code` program is a straight-line
  enumeration — and the induction lives only in the correctness proof. When
  the mathematical layer *does* recurse (`chainSplit`), add a closed form over
  positions to the reduction file (`splitClause_eq`) and have the certificate
  match that; programs enumerate, they do not recurse.
- **Absorb a source's "we may assume" into the *index type*, not into a
  preprocessing pass.** Give every clause `w` *slots* and let an out-of-range
  slot re-read the clause's first literal: the padding stage (with its own
  correctness proof and certificate) becomes a definition, and the index type
  stays a **rectangle** (`Fin p × Fin w`), which numbers by mixed radix where
  a sigma type needs `finSigmaFinEquiv`. The apparatus is shared
  (`Logic/Slots.lean` + `Logic/Slots/Code.lean`); a client needs only
  `sat_of_slotHolds` and `exists_slotHolds_of_sat`.
- **When generalizing a shared gadget, make the new parameter explicit only
  where it cannot be inferred** from an argument's type; most client lines
  then stay untouched. The residue is a *numeral* at the parameterized type
  (`OfNat (Fin ?w) 0` is stuck) — annotate the numeral (`(0 : Fin 3)`), not
  the whole term.
- **Guard junk with the threshold, not with the construction.** If the
  objective has a *hypothesis-free* bound that ignores the input — a lower
  bound for minimization (`le_card_of_isVertexCover`), an upper bound for
  maximization (`numSat_le_seven_mul`) — then one `if` in the threshold
  absorbs every ill-formed input as a no-instance for a reason the proof can
  state, and there is no preprocessing pass to certify. Pick the unreachable
  value by arithmetic over the shape parameters, never as
  `(constructed list).length + 1` — hitting the true length would force the
  certificate to match the list entry for entry, which membership-level
  adequacy never otherwise needs.
- **Abstract a fixed-size gadget to `Bool`, once, and then `by decide`.** When
  a gadget's behaviour depends on the input only through the truth values of
  a few literals, transfer the count to a `Bool^k` function in one `simp`;
  every fact about the gadget is then a finite check `decide` closes in a
  line, and the paper's on-trust case analysis becomes machine-checked
  exhaustion. Name the winning assignment as a function rather than
  existentially, so `decide` proves an equation, not an `∃` (precedent:
  `boolCount`, MAX 2SAT).
- **Count a `flatMap` block by block** (`Counting.lean`). To reject junk:
  bound each block by the maximum (`sum_map_le_mul_length`). To extract a
  witness: `eq_of_sum_map_ge` forces every block to the maximum, and the
  per-block characterization hands back the local data; the other direction
  is `sum_map_const`. Stated over an arbitrary `g : α → ℕ`, and any counting
  reduction wants all four.
- **Relabel first when a construction needs a `Fintype` variable index.**
  Threading a slot map through the construction makes its injectivity
  load-bearing inside the graph correctness; interpose an explicit
  `CNF.relabel` instead and spend injectivity exactly once, in the entry's
  relabeling lemma. The gadget then lives over honest `Fin m` and its
  families are full rectangles (a non-occurring variable's component is free
  and nothing touches it). Choose the relabeling's *list* so the certificate
  gets positions by arithmetic — source variables `++` fresh block
  (precedent: `cutVarList`).
- **A counting objective transfers through the edge bijection, not a witness
  set** (`cutSize_eq_of_equiv`, via `Sym2.map e` and `Finset.card_nbij'`) —
  same statement shape as the set versions, so the representation pair stays
  one line.
- **A property of a *global* object is refuted locally and established by a
  rank.** Before building the theory of an object a predicate quantifies over
  (a cycle, a path), check which way each direction of the reduction crosses
  it. Acyclicity of a digraph is the model case: refuting it means exhibiting
  one short closed chain, which a gadget always knows explicitly, and
  establishing it means exhibiting a function to `ℕ` that every arc increases
  (`Digraph.acyclic_of_rank`) — so neither direction ever takes a cycle apart,
  and the walk API that looked like a prerequisite is never built. The tell
  that this applies: no proof needs to *quantify over* the objects, only to
  produce one or to rule them all out at once.
- **A witness with a carrier of its own transports along `SimpleGraph.Iso.map`.**
  When a predicate quantifies over a graph on a *subset* of the vertices — a
  subtree spanning only the required vertices — the entry's renaming-invariance
  lemma has to move the carrier too: send `W` to `W.image e`, the graph to
  `T.map (e.subtypeEquiv …).toEmbedding`, and read `IsTree` off
  `Iso.isTree_iff` and the edge sum off `Finset.sum_nbij'` through
  `Sym2.map`. Nothing about trees is reproved (precedent:
  `steinerTree_of_equiv`). The companion decision at the entry: state weight
  agreement only *on edges of the graph*, since that is where a weight is read
  — a gadget with a constant weight function disagrees with a decoder's junk
  default everywhere else, and requiring agreement there would make the
  invariance lemma unusable.
- **Carry the position data the certificate will need.** The language has no
  prefix-sum scan, so anything a chained gadget needs to know about an
  occurrence — its position within its clause, its clause's width — must ride
  *in the enumerated list*. Decide this when designing the gadget, not when
  writing the certificate (precedent: `occPos`, `Logic/Sat/Encoding.lean`).

## Certificate annexes

### Structure and naming

- Spec lemma names: `foo_eval_true` for `foo.eval x = true ↔ …` boolean specs,
  `mem_foo_eval` for `_ ∈ foo.eval x ↔ …` membership specs.
- Wrap helper programs, their specs, and proof apparatus in a namespace named
  after the program (`ComplementCode`, `VcToDomSetCode`); only
  program-qualified names live at `Hardness.Cert` level, which is what
  prevents clashes under parallel authoring. **A domain's `Ty` abbrevs are the
  exception that bites**: they must sit at `Hardness.Cert` level, the namespace
  is flat across domains, and two domains that both want the obvious name for
  the obvious shape collide — `TripleTy` for `.pair .nat (.pair .nat .nat)`
  was written independently in `Sets/Matching3D/Encoding.lean` and
  `Ordering/Encoding.lean`. Neither file imports the other, so nothing fails
  until the root aggregate imports both, and the error names the *import*, not
  the declaration. Grep the existing abbrevs before naming one, and qualify by
  what the shape *means* here (`OrderedTripleTy`) rather than by its shape.
  The same rule governs
  `Adequacy.lean`: only the final correctness theorem, the
  `CertifiedReduction`, and the closing `example` sit at top level.
- Annex template: module docstring citing the generic theorem for the free
  bounds, `rfl` examples exercising the program (junk input included where
  instructive), spec lemmas, correctness, the `CertifiedReduction`, and a
  closing sanity `example` projecting to `⟶ᵣ`.
- **Look for it before you write it.** Annexes accumulate material that later
  turns out to be shared, so the first move on a new certificate is to grep
  the existing ones for what it needs, and promote rather than rewrite.
- **Generic material must not hide in annexes**: derived combinators go in
  `Cert/Language.lean`, encodings/decoders/accessors/`Concrete.*` problems in
  the domain's `Encoding.lean`, and any decoded-instance lemma needed twice
  gets promoted to the toolkit (`decodeGraph_adj`).

### Naming the gadget's objects in the concrete world

Concrete instances carry only `ℕ` labels, so a gadget's tagged fresh names have
to be realized as numbers. Only *injectivity* of the realization is ever
needed, so prove that and nothing more.

- For **formula** gadgets: `Code.natPair` for the tuple, plus a parity split
  to keep gadget labels off the input's (`splitVar`); state the adequacy
  lemma "up to relabelling" and let `CNF.satisfiable_relabel` /
  `CNF.width_relabel` transport the rest. A gadget whose output is another
  formula is the cheapest kind of certificate — no positions to number, no
  coordinate bijection, only variables — and can be stated as a single `map`
  image (`MaxSat/FromSat3/Adequacy.lean`).
- For **structured element types** (sums and products of `Fin`/`Bool`): a
  positional numbering, never hand-rolled — compose the layout from
  `Cert/Numbering.lean` (`fin`/`bool` digits, `prod` rectangles, `sum`
  blocks), and its bound, injectivity, and bijection onto the positions are
  read off. Two ways to wire it: define the numbering as the layout's own
  `num` with `@[simp]` face lemmas (when nothing matches program output
  definitionally; precedent `zNum`), or keep an arithmetic definition plus
  one bridge lemma "the arithmetic is the layout" (`extIdx_eq_num` — a
  constructor case split, `simp only` on the faces, then `ring`). Either way
  state the layout's `_size` lemma once and `rw` with it.
- A gadget with a distinguished **root** vertex has tag type `Option _`, and
  `Numbering.option` is its block: the root takes position `0` and the rest
  shifts by one. Order the *program's* output to match the numbering's blocks
  rather than the other way round — the layout is then read off the
  combinators, and the face lemmas are `rfl` (precedent: the Steiner annex,
  laid out root, elements, 3-sets).
- **State a numbering's face lemmas in the type the tag actually has.** When
  the tag type is a projection (`(decode x).Z`, definitionally `Fin n`), a face
  lemma stated over `Fin n` will not `rw` against a goal built from the
  projection: the two are defeq but not syntactic, and `rw` matches
  syntactically. Bind the projection.
- For **occurrence-indexed** tag types (a sigma of `Fin`s, clauses differing
  in width), the bijection is mathlib's `finSigmaFinEquiv`, wrapped as a
  block via `Numbering.ofEquiv`; the residue is one indexing lemma matching
  the program's flattened list against it.
- **A one-dimensional tag space needs no pairing function**: doubled original
  labels plus fixed odd labels separate `Option (Fin n)` by arithmetic,
  injectivity is one `omega` per case, and the labels stay small enough to
  read in the annex's `rfl` examples (precedent: `naeVar`).
- Define a certificate's naming map as the program's own evaluation
  (`occName := Code.natPair.eval …`): the bridging proofs then match
  syntactically, and only the map's injectivity is ever proved about it.
- Pipeline stages can be certified independently "up to injective
  relabelling" and composed freely, provided every property transported
  between stages is relabel-invariant; no stage needs to know how the
  previous one named its variables (precedent: `occ3Code`).

### Matching the edge list

The correspondence between the program's edge list and the gadget's is the
bulk of a graph annex. Three shapes, in order of preference:

1. **Equality of lists** — `edgesCode.eval x = (vcEdges φ).map (idxPair φ)`,
   each family the image of its mathematical family under the numbering.
   Membership transfers in one step from injectivity alone; no disjunction is
   ever assembled. Available exactly when both layers iterate the *same list
   in the same order* — worth engineering for: key the construction off data
   the certificate computes anyway (circuits indexed by `slotKeys`, not
   `cnfVars` — the two lists would be equal, and proving that would cost an
   enumeration lemma and buy nothing). When the two layers iterate at
   different granularities (per source clause vs per descendant), the
   regrouping is a clean list identity — land such lemmas generically in
   `Counting.lean` (`finRange_two_mul`, `zipIdx_eq_finRange`,
   `finRange_flatMap_cast`), not in the annex.
2. **Membership at the level of numbered nodes** —
   `(num a, num b) ∈ famCode.eval y ↔ (a, b) ∈ fam`, quantified over *nodes*,
   when the lists agree only up to permutation. The forward direction ends in
   `num_inj`, which does the number-to-node inversion for free. Under
   `ofEdgeList` the program may emit families in any order and duplicates
   cost nothing — but watch for the one ingredient whose order *is*
   load-bearing (a chain's occurrence list builds a different graph if
   permuted); find it before writing the specs and state that one as a list
   equality.
3. **The raw disjunction**, when a `filter` or `branch` in the program has no
   gadget counterpart. Keep the bookkeeping mechanical: emit the program's
   families in the order the mathematical layer lists them; build the
   `Or.inr` chain with `<|`; on the concrete side keep the `++` tree and use
   nested `List.mem_append_left/right` (depth = number of families, not
   disjuncts); come out of either side with an explicit `rcases` pattern —
   `simp`/`tauto` on the whole disjunction is what times out.

**Define the adequacy's shape parameters to be *definitionally* the abstract
construction's own indices** (`cutQ x := (cutPairs (decodeCNF x.1)).length`,
not `2 * x.1.length`), so the two layers' vertex types are literally equal and
no dependent rewriting is needed; expose the arithmetic face as a separate
`_eq` lemma. The price is a defeq that is definitional but not syntactic:
`rw`/`simp` match at keyed transparency and report "pattern not found" on
list-shape goals manifestly of that shape. The escapes, both using full defeq:
state the step as a `have` closed by `exact` (term elaboration unifies at
default transparency), or `change` the goal to the syntactic form wanted. And
prefer `refine congrArg₂ (· ++ ·) ?_ ?_` to `congr 1` when splitting an append
of two large terms — `congr` triggers an expensive defeq descent into them.

### Branching certificates

An instance map that branches becomes a program that branches, and the
adequacy proof splits the same way.

- **Give each branch its own `eval` lemma**, with the branch condition as a
  hypothesis, proved by `rw [show … from rfl, if_pos/if_neg]`. The main
  correctness proof is then per-branch rewrites and appeals, and no `if` —
  and none of `.branch`'s `Bool`-vs-`Prop` juggling — appears in it.
- **Recompute the branch condition, do not reproduce it.** The program may
  branch on an equivalent quantity that is cheap under the decoding (positions
  incident to a sanitized edge, where the mathematical layer counts a
  deduplicated vertex list). The agreement of the two is a real lemma
  (`numTouched_eval`), to be stated and proved *before* the program that
  branches on it — left implicit inside a transport, it is exactly where a
  certificate silently stops certifying the reduction it claims to.
- **The degenerate branches carry the hypotheses the gadget needs.** Check
  that the assumptions the short branches buy (`1 ≤ k < n₁`) are the ones the
  gadget's two directions actually take, and that the short branches' own
  correctness is provable — a fixed yes-instance needs the *source* to be a
  yes on that branch.

### Lookup tables, and making their defaults unreachable

A weighted problem's concrete instance carries a *table* — an association list
keyed by an index pair — and decoding must be total, so an absent key needs a
default. Three rules keep the default from becoming a proof obligation
(precedent: `weightOf` and the TSP annex).

- **Emit the whole table.** A program that emits every key never consults the
  default, so no lemma downstream mentions it; a full `n²` matrix is charged
  honestly and costs nothing new.
- **Make the emitted value a function of the key.** "The lookup returns `v`"
  then needs only *a* membership plus "every entry under this key carries
  `v`" (`weightOf_eq_of_mem`); proving the key occurs *once* is the expensive
  way to the same conclusion.
- **Let the key normalize the symmetry.** Reading the key
  `(min i j, max i j)` makes the decoded table symmetric by construction,
  discharging the instance-type field with no well-formedness predicate — and
  the emitter may list a pair in either orientation.

### Sanitizing

**Sanitize when the tag space is smaller than the position space.** Junk input
that names nothing in the *source* instance can still name something in the
target (an out-of-range 3DM index is still a position of the concatenated
element list). Whenever the certificate's numbering is not onto the target's
positions from raw input alone, the program must filter first (`goodEdges`).
The tell: the transport lemma's `↔` fails in the backward direction.

**Sanitize when the two decoders disagree about junk**, even where the tag
spaces match. Two problems may share a `Ty` and read it differently:
`decodeGraph` ignores a diagonal index pair, `decodeDigraph` reads one as a
self-loop. A program copying raw pairs across then invents structure — here a
loop, hence a cycle — that the decoded input does not have, so it is *wrong*
on junk inputs rather than untidy. Whenever a program forwards raw data
between domains, compare the two decoders' junk rules first, and filter to the
intersection.

### Transporting a tagged index type to list positions

A gadget indexed by a tagged type (`↥T × Fin 4`, one block of numbers per
surviving object) meets a target problem indexed by *positions* of the emitted
list. Two moves keep the passage cheap (precedent: the 4-PARTITION annex).

- **Introduce the bijection together with its defining formula**, not as a
  bare term:
  `obtain ⟨E, hE⟩ : ∃ e : Tagged ≃ Fin L.length, ∀ p, (e p).val = <formula> := ⟨…, fun _ ↦ rfl⟩`.
  Every later step rewrites with `hE`; the numbering combinators
  (`Numbering.prod`, `equivFin`) never appear again, and nothing downstream
  can get stuck unfolding them.
- **Prove the pointwise reading with `getElem?`, then convert once.**
  `L[(E p).val]? = some (size p)` is motive-free — the index is a plain `ℕ`
  and the block lemmas (`getElem?_flatMap_four`) speak `getElem?` anyway.
  Convert to `L[i] = size (E.symm i)` at the end via
  `List.getElem?_eq_getElem` and `Option.some_inj`; the sum and the
  membership arguments both want that form.
- **A `getElem` index cannot be rewritten — so state the enumeration at the
  coerced index, and reindex with the entry's transport lemma.** `L[↑(e a)]`
  carries a bound proof mentioning the index, so `rw` on `e (e.symm i) = i`
  fails the motive check and `simp only` unfolding the *list* rebuilds a
  differently-typed equiv around it. The phrasing that works is an enumeration
  hypothesis `∀ a, L[↑(e a)] = <the triple of families at a>` (no rewriting
  needed to *use* it) plus the entry's `exists_…_iff_map e.symm` to move the
  question from positions to tagged names (`sequencing_iff_of_enum`). Two
  supporting habits: reach the append form with `change`, which is defeq and
  leaves the surrounding types alone, and note that
  `List.getElem_append_left/right` take the bound as an *irrelevant implicit*,
  so they rewrite freely once the index is a plain numeral.
- **A pool of pairs is a filtered `Code.cross` of `listEnum` with itself, and
  it needs no dedup.** Crossing the *enumerated* list rather than
  `Code.indices` makes each entry carry its payload beside its index, so a
  value read off the pair costs no lookup; and the cross of two
  repetition-free lists is repetition-free (`List.nodup_flatMap`), which is
  what `idxOf` needs to be a bijection onto positions. Membership, an
  injectivity and a lift are then all `Equiv.ofBijective` wants
  (`poolList` and `srcPair_idx_bijective`, the 3-PARTITION annex; the same
  three feed the dedup'd survivor list of the 4-PARTITION one).

### Combinators to reach for

- Environment-dependent filtering is `Code.filterMapEnv` / `Code.filterEnv` —
  do not hand-roll `listMapEnv`-of-`branch`-then-`listJoin` again. Applied
  forms exist for the common point-free noise (`Code.add`, `Code.mul`,
  `Code.lt`, `Code.and`, `Code.append`). The *combinators* live in
  `namespace Code`, their *spec lemmas* do not. A few older annexes still
  hand-roll the idiom — leftovers, not the pattern to copy.
- **`getD` is `listNth` with a default appended.** `Code.listNth` returns a
  one-element list, empty out of range; appending the default and reading
  position `0` is exactly `List.getD`, which is how a program pads a short
  list to fixed width (`padLit`). Reuse the one-element shape rather than
  unwrapping it — when the output is a formula, `listNth`'s result already
  *is* a clause.
- **Consecutive pairs are `listNth` at the next position.** Enumerate, put
  the element in the environment, look up `i + 1`; the empty out-of-range
  result makes it a *chain*, not a cycle (`consecCode`), and `finRotate`
  closes the cyclic cousin (`linkPass`). No primitive is needed for either.
- **`listSum` is the missing `head`.** For a numeric field, a singleton list
  is its own sum and the empty one sums to `0`, so `listSum` reads the
  element and supplies the default in one step (`slotEntry`). Carry a
  separate found-bit when `0` must be distinguishable from "absent".
- When only a *length* matters, build the list with `Code.cross` from lists
  already in hand (`length_cross_eval`); the language has no `range`, and
  `Code.indices` gets the positions when the numbers themselves are wanted.
- **Division and remainder are not primitives, and do not need to be.** A
  gadget that wants `len / k` wants a *list* of that length, and the
  enumerated input filtered by `k * i < len` has length exactly `⌈len / k⌉` —
  `length_filter_zipIdx_lt` closes it after a `List.filter_congr` restating
  the test as `i < (len + k - 1) / k` (`quarterList`, the 3-PARTITION annex).
  The same list decides `k ∣ len`, as `len = k * (its length)`. Adding a
  division primitive to charge a bit-length would be the wrong trade: the
  list is what the construction consumes anyway. Two riders. The *floor*
  `⌊len / k⌋` is the same idiom with the test `k * i + (k - 1) < len`
  (`thirdList`, the bin-packing annex) — pick the rounding the construction
  needs and let `List.filter_congr` restate the test. And when the quotient is
  to be *emitted* in unary, the filtered list already **is** the numeral: map
  its entries away with `unaryOfList` and no crossing happens at all.

## Representation theorems

The once-per-domain layer (`Graph/Representation.lean` is the precedent) that
makes each concrete problem a *faithful representation* of its bundled one:
`P ⟶ᵣ Concrete.P` (encode) and `Concrete.P ⟶ᵣ P` (decode). Composing through
a pair turns a certified reduction between concrete problems into the
reduction between the bundled ones — which is what rules out a degenerate
decoder by theorem rather than by inspection.

- **The decode direction is `Iff.rfl`** — the concrete problem is *defined*
  as `P.comap decode` — so all content is in the encode direction: one encode
  function and one round-trip lemma serve every problem of the domain.
- **Encode is noncomputable, and deliberately not a `Code` program.** A
  bundled instance holds an arbitrary `Fintype`, which is not `Ty`-data; cost
  is charged on the concrete side only. Use `Fintype.equivFin` and do not
  fight for computability.
- **State the round trip as the invariance hypothesis.** One lemma
  (`encodeGraph_adj`) in exactly the `e : V ≃ W` + correspondence form the
  entries' renaming-invariance lemmas consume; each representation pair is
  then a one-line application of one existing lemma.
- **Compose the vertex bijection with `finCongr`** — the two lengths are
  propositionally, not definitionally, equal — and expose the `rfl` lemma for
  its `val` so membership proofs downstream match definitionally.
- **Thresholds ride definitionally**, so a restriction's side condition
  (`k = 3`) transfers by `and_congr Iff.rfl …` with no extra lemma.
- The missing invariance lemmas are the real work, and they belong at their
  entries (see [Stating a problem](#stating-a-problem)), not in the
  representation file; deriving one from a sibling by complementation
  (`exists_indepSet_iff_of_equiv`) is cheaper than mirroring the proof.
- **If the bundled carrier has no `Fintype`, ask for injectivity only where
  the instance can see it**: generalize the domain's transport lemmas to
  `Set.InjOn f φ.vars` and keep the globally-injective versions as one-line
  corollaries — gadget certificates then need no changes. The reflection
  direction gets genuinely harder: both "an unused label is counted zero
  times" and "an absent variable is" are needed, so neither side can hide an
  excess (`CNF.forall_varOccs_relabel_le`).
- **If the encoding cannot express every bundled instance, weaken the
  invariance lemma — never add a well-formedness predicate.** X3C's encoding
  drops sets of size other than three, so the entry's invariance lemma
  requires correspondence only on the sets the question can use
  (`exactCover3_iff_of_equiv_card3`). Because the side condition sits in the
  question rather than on the instance type, the gap closes by a theorem.
- The degenerate domains are worth writing anyway: `Numbers/` has no carrier
  to name, encode is a repackaging, and the round trips are `rfl` — state
  them as named theorems.
- **A second notion of satisfaction on an existing instance type costs one
  lemma, if the first was factored**: isolate the single step where the
  labelling's injectivity is spent (`CNF.exists_relabel_assignment`) when the
  *second* client appears — not speculatively, but in the same commit, so
  nothing is proved twice.
- **The best closing example is cross-domain**: two domains' pairs composed
  around a certificate (`VERTEX_COVER ⟶ᵣ SET_COVER`, abstract source to
  abstract target), which is the claim the layer exists to support.

## Tactic failure modes

The recurring ones, with the fix that works. Most are the same underlying
story: `rw` fails its motive check when the rewrite would move something a
dependent proof mentions, and the fix is term mode.

### `rw` motive-check failures

- `rw` with `decodeGraph`/`Ty.denote`-flavored iff lemmas can fail at instance
  transparency; fall back to term-mode `Iff.trans` chains, `change`, or a
  closing `exact Iff.rfl`. The same failure on `Finset` lemmas about a
  decoded family (`Finset.disjoint_left`) — use `.mp`/`.mpr` instead.
- Lemmas of the shape `(∀ i : Fin l.length, p l[i]) ↔ ∀ a ∈ l, p a` are
  higher-order and `rw` will not match them — apply them with the predicate
  given explicitly. Likewise `rw` with any lemma quantifying over a
  *predicate* fails higher-order unification ("did not find an occurrence");
  reach for the specialized form when there is one (`CNF.width_relabel`).
- `rw` fails the motive check on `l[i]` when it would move the *list* or the
  *index* (the bound proof depends on both). Rewrite with lemmas that
  eliminate the `getElem` first (`List.getElem_append_left`, `getElem_map`,
  `getElem_zipIdx`), then fix up the index arithmetic — by then the goal is
  non-dependent and `rw`/`omega` work.
- When a decoder-lemma rewrite leaves a goal ill-typed at instance
  transparency (a `Membership` mismatch between `(decode x).U` and the `Fin`
  it definitionally is): pull the step out as
  `have … : _ ↔ _ := by rw [decoder lemma]; exact (membership lemma) _ _` —
  the `exact` closes at default transparency — then `rw` with that.
- A decoded instance's type fields are only *definitionally* `Fin _`, so
  terms mentioning them can fail to elaborate; ascribe the binder type in the
  statement (`∃ t : Fin x.1.length × …, …`) and close with term-mode
  `Eq.trans`/`Iff.trans`.
- A plain `def` has no equation lemma to `rw` with; ship a `foo_eq` proved by
  `rfl` when proofs must see through it. Local `Ty` synonyms used as `Code`
  indices must be `abbrev`, not `def` — at `def` transparency `rw` fails to
  match across the synonym.
- `rw [decide_eq_true_iff]` **inside an `ite`** fails the motive check (the
  `Decidable` instance mentions the term being rewritten). Split instead:
  `by_cases h : c` then `rw [if_pos (decide_eq_true h), if_pos h]` and the
  `if_neg` mirror. The same applies to relating `Code.branch`'s
  Bool-conditioned `ite` to a `Prop` `ite`.
- `rw` of a *list length* fails whenever a dependent `Fin` in the goal is
  bounded by it. When the function being applied is non-dependent in the
  argument to change, `congrArg` in term mode does the rewrite with no motive
  at all.

### `omega`, and where its hypotheses go missing

- **`omega` silently drops a goal whose equality does not live in `ℕ`
  syntactically.** An arithmetic goal `a = b` at `Ty.nat.denote` — which is
  `ℕ`, but not spelled so — is discarded, and `omega` then tries to derive a
  contradiction from the hypotheses alone and reports a counterexample with
  the goal's atoms missing. That missing-atom report *is* the diagnosis. The
  fix belongs in the statement: bind plain `ℕ`s in the membership lemma
  (`∃ c d : ℕ, (c, d) ∈ …`) rather than one element of a list whose element
  type is `Ty`-flavored.
- **A *hypothesis* is dropped too, and which one depends on the order of its
  operands.** From a visibly contradictory context `h : x.1.length < x.2`,
  `hk : x.2 ≤ c`, `hs : c ≤ x.1.length` (all at `ℕ`, with `x.2` at
  `Ty.nat.denote`), `omega` reports a counterexample with `hk` simply absent —
  while `h`, which mixes the same two flavours, is read. Writing the *same
  fact* as `hk : c ≥ x.2` makes it visible and the call succeeds: the left
  operand fixes which `LE` instance is elaborated, and only the `Ty`-flavoured
  spelling is one `omega` does not recognize. Type-ascribing the offending side
  (`(x.2 : ℕ) ≤ c`) does nothing, the ascription being a no-op on a defeq
  alias. So: put the plain-`ℕ` side on the left, or drop to term mode
  (`absurd (hk.trans hs) (Nat.not_le.mpr h)`). The missing-constraint report is
  again the diagnosis — do not hunt for a missing atom.
- **Reduce `Bool.toNat` after the case split, not before.** A `simp only` on
  the tag bits placed ahead of `cases b` fires on nothing, and `omega`
  afterwards sees `Bool.toNat false` as an opaque atom with no value. Case
  first, then reduce — `cases b <;> simp only [Bool.toNat_false, …]`.
- Projections left unreduced (`(c, d).1`) are likewise separate atoms from
  `c`; `dsimp only at h` before the arithmetic, or destructure the pair in the
  `rintro` pattern.
- **So is a beta-redex.** A predicate whose argument is a *family* —
  `IsPacking (fun i ↦ 2 * l[i.1]) cap k a` — unfolds to a goal containing
  `∑ i ∈ …, (fun i ↦ 2 * l[i.1]) i`, and the same predicate *instantiated*
  (`ha 0`) keeps the redex while a `have` stated by hand does not. The two
  spellings are one atom to `exact` and two to `omega` and `rw`. Normalize with
  `simp only [h]` rather than `rw [h]` — simp beta-reduces before matching,
  which is exactly the step `rw` skips — and state the bridging lemma
  (`∀ t, ∑ i ∈ t, 2 * l[i.1] = 2 * ∑ i ∈ t, l[i.1]`) redex-free, so it can
  serve as a simp lemma in both directions of the proof.

### Instance mismatches, not term mismatches

A tactic can fail on two terms that *print identically*. The mismatch is then
in an implicit type or a `Decidable` instance, and no amount of rewriting the
visible structure helps.

- **`classical` at the top of a long proof is not free.** It installs
  `Classical.propDecidable` locally, and any later `change`/`exact` that must
  reproduce a `Decidable` argument already present in the goal (an `if` from
  an unfolded gadget size) synthesizes the classical instance instead —
  "synthesized type class instance is not definitionally equal". Add
  `classical` where a proof needs it, not by reflex.
- **Rewriting an `if`'s condition:** `if_congr` needs its second `Decidable`
  argument *synthesized*, before unification can supply the one from the
  goal, and fails outright. `simp only [h.symm]` with the condition
  equivalence rewrites the condition and rebuilds the instance; feed it a
  rfl-`show` for whatever projection defeq blocks the match
  (`show (pval th).1 = ↑(↑th).1 from rfl`) and close with `rfl`, which
  absorbs the two instances' difference.
- **A `rw` whose pattern is displayed identically to the goal's subterm** is a
  re-elaboration mismatch: spelling the lemma's arguments out again picks up
  different implicit types than the goal carries (`Fin.val` at `(decode x).W`
  versus at the `Fin` it definitionally is). Take the arguments *from the
  goal* — `refine Iff.trans ?_ (lemma e _ 4 _).symm` leaves them to
  unification — and rewrite only with hypotheses whose statement the same
  elaboration produced.
- **A defeq-but-not-syntactic type argument poisons `rw` and `omega`.** When
  one index type reaches a proof by two routes — from destructuring the
  problem, and from the gadget's own spelling of it — a term like
  `parts.card` elaborates with two different implicit arguments, and the
  tactics see two atoms however identical the display. Re-type the problem
  *once*, at the boundary, with an `Iff.rfl` lemma over the gadget's spelling
  and destructure through it (`fourPartition_decode_iff`, the 3-PARTITION
  annex); every hypothesis downstream then carries one elaboration.
- `set_option maxHeartbeats N in` goes **before** the docstring (the same
  placement trap as `omit`), and the mathlib linter wants the explanatory
  comment *after* the `set_option` line.

### Stating things so `rw` does not have to

- State a decoded family's shape as a **quantifier translation**
  (`forall_mem_family : (∀ S ∈ (decodeX …).family, P S) ↔ ∀ q ∈ …, P (…)`),
  not as a list equality to be rewritten with: rewriting a decoded list
  equation *in place* unfolds `Ty.denote` and leaves the goal ill-typed for
  every later tactic.
- Closed forms with *computed* element indices (`(p + 1) % k`) should read
  elements with `getD`, not `getElem`: the index is then a plain `ℕ`
  argument, `rw`/`omega` work without motive trouble, and
  `List.getElem_eq_getD` converts at the end (precedent: `cycleOf_eq`).

### `decide` and `Decidable`

- Never rewrite selectively inside `decide`'s Prop argument: simp skips the
  `Decidable` *instance* argument, the term desyncs internally, and
  afterwards nothing matches it. Resolve a Bool `ite` by rewriting the whole
  `decide …` atom via `decide_eq_true`/`decide_eq_false`, and let the closing
  `rfl` absorb the defeq projections.
- `decide` of a bounded `∀ _ ∈ l.zipIdx …` can fail `Decidable` synthesis
  outright; state list predicates Bool-natively with `List.all` and reason
  via `List.all_eq_true`.
- `∀ a b c d : Fin 3, …` overruns `Decidable` synthesis — do `Fin` pigeonhole
  through `.isLt` and `omega`. `∀ A B C D : Bool, …` is sixteen cases and
  `decide` closes it instantly; that asymmetry is the reason to abstract a
  gadget to `Bool` rather than to `Fin`.
- `fin_cases` is *not available* (not on this library's import surface). To
  case on a `Fin 3` variable, prove `∀ u : Fin 3, u = 0 ∨ u = 1 ∨ u = 2` by
  `decide` and `rcases … with rfl | rfl | rfl`.
- When a goal mixes `decide` with Boolean connectives, do not hunt for
  projection lemmas — give `simp` the unfolding lemmas for the definitions
  involved. The lemma `decide_congr` would be is `decide_eq_decide.mpr`.
- **A `simp` that must unfold a dependent recursor is a performance trap even
  on tiny data** — evaluating a concrete walk through
  `Walk.support`/`Walk.edges` equation lemmas takes a minute where splitting
  the goal into its fields (`isCycle_def`) and `decide`-ing each takes
  seconds (precedent: `hamiltonianCircuit_triangleInstance`).

### `cases h : f x` under a `decide`

`cases h : σ v` fails with "motive is not type correct" whenever the goal
contains `decide` of a proposition mentioning `σ v`: the `Decidable` instance
depends on the term being generalized. Case on the *proposition* instead —
`by_cases h : l.Holds σ`, then `decide_eq_true h` / `decide_eq_false h` — which
rewrites the whole `decide` atom at once. Same rule as never rewriting
selectively inside `decide`'s `Prop` argument.

### Eliminating an inductive family

- **`cases` on an indexed family whose indices are already instantiated
  substitutes them unpredictably** — binder lists drift per alternative,
  impossible clauses vanish, and `rintro` fails with "dependent elimination
  failed". The robust form is a **flat inversion lemma**, stated once: a
  disjunction with one explicit `∃ …, u = … ∧ x = …` per constructor, proved
  by `cases` on the *uninstantiated* hypothesis. Every use site goes through
  it and lets the constructor-injectivity simp lemma do the work (precedent:
  `chosenAdj_inv`).
- **A vertex type built from `Sum` and `Fin k` with named shapes needs its
  own eliminator**: `rcases` leaves raw `Sum.inr ⟨2, _⟩` values the face
  lemmas do not match. Declare it once —
  `@[elab_as_elim] theorem hpVtx_cases …` — and `induction u using hpVtx_cases`
  hands back goals already phrased in the names.

## Adding a `Code` primitive

Rare, and deliberately expensive. A new constructor needs: the constructor with
a docstring saying *why it cannot break the blanket theorem*, an `eval` case, a
`cost` case charging at least the naive interpreter's work, a private
`..._case` lemma stated over plain `ℕ` (so the induction case closes by
`exact`, as for `natAdd_case`), and its case in `cost_size_le_polyBound`.

Prefer deriving: `Code.powEnum` is a derived combinator precisely so that only
`natPowLen` (`b ^ l.length`) had to be trusted. The rule an aggregate must
satisfy is that its output size is bounded by the input's bit content — which
is why there is no general fold and no value-indexed exponentiation.

## Prose: timeless and even

`README.md` entries and top-of-file docstrings are read long after they are
written, by a reader who does not know — and should not need to know — the
order in which the catalog grew. Two rules.

**Timeless.** Never state a fact whose truth depends on when it was written:
"the catalog's first counting predicate", "the cheapest certificate in the
library", "until now", "the previous restrictions", "with X landed, …". These
are progress-report sentences, and the next entry falsifies them silently —
at one point two files each claimed to be the cheapest certificate in the
catalog. If the observation has real content, restate it as a comparison that
stays true: not "the catalog's first counting predicate" but "a counting
predicate: where a subset problem asks whether a set exists, this one asks
how many …". The library's chronology lives in git, and its work queue in
`ROADMAP.md`; those are the only documents allowed a "now".

**Even, and informational.** A catalog entry in `README.md` gets the same
treatment as its neighbours: its sources, a one-sentence gist of the
construction in parentheses, and at most one genuinely mathematical or
design remark. It does not get superlatives, narration of the proof strategy,
or links to its certificate annex (the annex convention is stated once, above
the list). The recurring failure mode is the implementing session writing its
own entry: the agent that lands a big construction is the one most tempted to
write it a big entry, with the emphasis on what was hard to *do* rather than
what is useful to *know*. Entry length should track what a reader needs, not
what the construction cost. Program mechanics are the reliable tell — "takes
the count as the length of the enumerated positions with `3i + 2 < n`" is a
sentence about the annex, and each of BIN PACKING and 3-PARTITION once carried
its own copy of it.

**One thing an entry docstring must carry.** The `Hardness proof (in …)` line
names each reduction *and* its certificate annex, because that line is where a
reader checks the standing milestone — correctness catalog equals certified
catalog — one problem at a time. An entry naming the reduction but not the
certificate reads as an uncertified entry, and the line goes stale silently:
seven of them said less than the library had proved, and the Bin Packing entry
still listed one source after a second had landed. Update it in the batch that
lands the reduction, not later.

The same standard governs *this* file: a lesson lands here only when it is a
pattern of the library, stated as rule + why + precedent, not as the story of
the session that learned it. One reduction's internals belong in that
reduction's docstring.

Docstrings follow the same line: a file may say what is unusual about itself
when that routes the reader ("a branching certificate", so see the branching
section; "a counting predicate", so transport lemmas need counting twins) —
but it does not rank itself against the rest of the library.