…ertion (#97)

The false assertion corrected in #95 was **not an isolated slip**.
Auditing whether the conformance corpus actually *runs* — the gate only
ever checked that it *parsed* — turned up a second mathematically false
claim of exactly the same kind, plus one genuine unimplemented feature.

## The second false assertion

`conformance/valid/v16_close_mirror_reverse.tangle`:

```tangle
assert reverse(braid[s1, s2]) == braid[s2, s1]
```

`reverse` reverses the word **and** negates every exponent — it yields
the *inverse* braid, so `reverse(s1 s2) = s2⁻¹ s1⁻¹`.

Disproved by invariant: `writhe(reverse(braid[s1,s2])) = -2` while
`writhe(braid[s2,s1]) = +2`, and writhe is invariant under the braid
relations, so they cannot be the same element.

## Two authors, same mistake → a documentation failure

`examples/trefoil.tangle` and this file made the *identical* wrong
assumption. That is not carelessness. `FORMAL-SEMANTICS.md` described
the operation as:

```
|  reverse(e)     -- reverse word
```

which reads as order-only. Now stated as an identity:

```
reverse(g₁ g₂ … gₙ)  =  gₙ⁻¹ … g₂⁻¹ g₁⁻¹        i.e.  reverse(w) = w⁻¹
```

with the contrast against `mirror` (which negates **in place**) spelled
out, and the writhe argument recorded so the next reader can check it
rather than trust it.

## The systemic fix

`scripts/check-corpus.sh` now **evaluates** `conformance/valid`, not
just parses it. Parsing was never enough — a program can parse perfectly
and assert something false. Both bad assertions survived precisely
because nothing ran them.

**Verified in both directions:** reintroducing the exact false assertion
makes the gate fail (`exit 1`, *"parses but does not evaluate"*);
restoring it returns `exit 0`.

## The genuine gap

`v09_twist.tangle` uses `(~a)` to twist a named strand inside a weave.
`spec/grammar.ebnf` says *"In weave context: (~a) twists named strand
a"*, but `infer_expr` rejects any strand name used as an expression —
specified and unimplemented. Recorded in the new
`CONFORMANCE_KNOWN_UNRUNNABLE` list rather than papered over, and raised
as **#96**.

Worth noting *why* it was invisible: until #93 a weave block could not
be bound to anything, so its body was never evaluated. The construct has
literally never run.

## Regression tests

Four pinning `reverse`, chosen so they cannot pass vacuously:

| Test | Why it can't be faked |
|---|---|
| reverse is **not** order-reversal | asserts inequality with the wrong
answer |
| `reverse(reverse(w)) = w` | only holds if it genuinely inverts |
| reverse negates writhe | the invariant that disproved both false
claims |
| `mirror` negates *in place* | pins the contrast that caused the
confusion |

Suites 112 → 116, all green; TG-3 still 1008/0.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

…ent-order bug (#99)

TG-11 (#98) landed the type former, typing, evaluation and six proofs —
but there was **no way to write one**. Zero occurrences of the
constructors in `lexer.mll` or `parser.mly`, against 4 for echo. Fully
implemented and unreachable.

## Surface syntax

```tangle
def w     = warrant[0](42, braid[s1, s2])   -- at standpoint 0
def token = evidence(w)                      -- the ONLY elimination
```

The standpoint is bracketed because it's an *index*, not an operand —
the same reading as a braid generator's subscript. No grammar conflicts.

**Non-factivity reaches the syntax.** There is deliberately no keyword
extracting the claim: `claim(w)` parses as an ordinary call to an
undefined function, never as a language form. A test pins that
distinction — if a `Claim` form ever appears, it contradicts
`epi_only_yields_evidence`.

## A *second* copy of the statement-order bug

Writing the first epistemic program surfaced it immediately:

```
def w   = warrant[0](42, braid[s1])
def tok = evidence(w)
→ In definition 'tok': evidence requires an Epi[k, rho, tau], got Word[0]
```

That `Word[0]` is the pass-1a **placeholder** — `tok` was being checked
*before* `w` was refined. Same root cause as #95 (`stmts := prog @
!stmts` then `List.rev` on the flattened list), but in a **second
copy**, in `lib/check.ml`.

**That copy feeds `tanglec --check` and the LSP.** Both have been
analysing programs with their statements reversed.

And it was never epistemic-specific:

```
def e = echoClose(braid[s1])
def r = residue(e)
→ residue requires Echo[_, _], got Word[0]
```

**Any cross-definition reference to a non-`Word` type was mis-typed.**
Echo has been broken this way for as long as the recovering path has
existed.

The test suites missed *both* copies for the same reason: they call
`Parser.program` directly and never exercise the recovering path.

## Tests

**Parser** — warrant with bracketed standpoint; evidence; TG-4
round-trip; the no-claim-form guard.
**Check** — three cross-definition cases (plain, echo, epistemic), all
of which would have failed before this.

## Example

`examples/epistemic.tangle`, wired into the corpus gate's must-run set —
warrants at three standpoints, evidence recovery, and the echo
composition `residue(evidence(we))`. All assertions pass.

It also documents *why* the claim is unreachable: if it were
extractable, anything anyone attested would become true by fiat —
precisely the bug you don't want in a provenance system.

All gates green: Lean 0 errors, full suite, corpus, RSR.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>