# v0.3 reindex-invariant wire-key design

## Contract

The v0.3 wire version is identified by `version = "0.3"` and
`canonicalization = "reindex-v1"`. The algorithm discovers vertices in the
first-occurrence order

```text
conclusions ++ links.flatMap Link.vertices
```

and replaces every submitted vertex number by its position in that order.
Formula values are copied in the same order. Link order, conclusion order,
tensor/par premise order, and axiom endpoint order are deliberately preserved.
The algorithm is linear apart from list `idxOf` lookups and does not enumerate
vertex permutations.

## Kernel-checked guarantee

`traversalVertices_reindex`, `traversalRelabel_reindex`, and
`equivalenceCanonicalString_reindex` prove in Lean that applying any bounded
bijective `VertexRenaming` cannot change the v0.3 output. Consequently
`ReindexEquivalent.equivalenceCanonicalString_eq` proves:

```text
left.ReindexEquivalent right
  -> left.equivalenceCanonicalString = right.equivalenceCanonicalString
```

For structurally well-formed certificates, v0.3.1 additionally proves that the
normal form is literally obtained by an explicit bounded `VertexRenaming` and
that normal-form equality is equivalent to `ReindexEquivalent`. The executable
`reindexEquivalent?` function is therefore a proved decision procedure on
structurally well-formed, and hence on checker-accepted, inputs.

## Exact scope

The completeness theorem concerns the certificate normal form returned by
`equivalenceCanonicalize`. The compressed JSON encoder is deterministic and
round-tripped in CI, but encoder injectivity is not separately used as the
logical decision theorem; callers needing a kernel theorem should use
`reindexEquivalent?`.

The relation deliberately treats link order, conclusion order, tensor/par
premise order, and axiom endpoint order as identity. It is not canonical
labeling modulo arbitrary graph isomorphism or list reordering.

Malformed certificates are serialized deterministically but remain outside the
normal-form completeness theorem and remain untrusted.
Callers must use `Certificate.checkedFromString` when logical validity is
required.

## Compatibility and evidence

`Certificate.fromJson` dispatches v0.2 and v0.3. The explicit
`migrateV02StringToV03` API parses and validates a v0.2 normal form before
emitting v0.3. `examples/canonical-v0.3.json` is read back by the Lean smoke
test and compared with Lean's serializer output. CI additionally validates the
schema and audits all 1,000 committed certificates under deterministic random
vertex permutations, idempotence, and link-order reversal.