Tiger documentation: newcomer explainer and full rule reference - #13

Replace docs/Tiger Explainer.html with docs/Tiger Explainer.md so the
newcomer doc lives in the same format as the rule reference and renders
on GitHub without a download. README links the new path, and the docs
meta-test reads the .md file so the removed-vocabulary check keeps
covering it.

…s, bug classes

The explainer now states at the top that it describes tiger as it is meant to be
when finished, and names the surface checks (TS-I01, I03, I05, I06, I07) as the part
that is specified but not enforced. New sections: "Invariants have names", "One pin
holds the whole subtree" (replacing the transitive-pins TODO), and "Whole bug classes
are excluded, not caught". "Effects are the fourth oracle" is rewritten with tests
restored as the third oracle. Every transcript is live tiger check output; the footer
says which runs use the ledger and which use a scratch module.

The spec now matches the code: unpinned effect sets and synthesized variants print
only under --show-facts and never block; TS-A08 and the five surface rules carry an
Unimplemented status, and the analyzer table marks invariantsymmetry (ENG-182),
surfaces, and adapters as not built. TS-V01 records that //tiger:batched waives
TS-S02 but not the variant check (ENG-183).

…eview fixes

Adds "A frame is where a function writes" after the subtree-pin section, built on a
live run where a method pinned to one field calls a helper that writes another.

The mechanism sections now speak in the team's voice: "we" for what was chosen,
required, shipped, or found in trials; "tiger" for what the tool does when it runs.

"What adoption looks like" is removed as incomplete, along with the plugin caveat
box it carried; "Try it" no longer points at adoption steps and now states the
1,023-finding first run directly. The opening narrows "security holes" to denial of
service, the one such bug the trials found.

Final review fixes: the top note uses plain words instead of surface vocabulary the
page has not yet defined; the nondeterminism section opens with the concept before
rule codes; the footer attributes the Drain transcripts to scratch packages rather
than the ledger and notes the pinned Drain excerpt omits a second TS-C05 finding.

The explainer is now the authority on what tiger promises. It requires every
nondeterministic dependency to be injectable and proves that per pinned
function through effect sets; it does not require a fake, mock, or test
double, and whether a test substitutes one is the coder's call per test.
The spec follows: TS-I01 retitled and enforced through effects pins, TS-I03,
TS-I05 and TS-I07 marked review-only, TS-I06 deleted (tiger cannot classify
a wrapper), TS-X01 notes the coming test-double exemption (ENG-185), and the
surfaces and adapters analyzers are marked not planned and deleted.

The tagline now leads with what tiger does for AI-written Go and credits
Power of Ten and TigerStyle; README, spec, and CONTEXT.md open the same way.
"Dialect" is retired from every live document and Go comment in favour of
"the rules" or "the rule set"; ADRs and dated feature reports keep it as
history.

Also: grammar pass and a four-slice reviewed edit of the explainer (pin
walkthrough now names Drain, map order no longer listed as injectable,
"variant" named in prose, escape hatch -> escape directive, rule codes out
of prose), TS-A08 marked unimplemented (ENG-182), TS-V01 batched gap noted
(ENG-183).

The "Tiger is not a linter" section described golangci-lint as advisory
output tiger runs alongside. That is not how tiger uses it: half the rule
set is enforced by golangci-lint linters that tiger configures with
`tiger golangci --init` and audits with `tiger golangci`, and every issue
fails the run. The section now explains both engines, shows a real audit
transcript from a config drifted to 80 lines, and covers package
restrictions with the transitive-bound mechanism from the spec. The
unsourced claim that the analysis is "cheap" is dropped.

The "Run the check" opening now states what the command does instead of
narrating a day with tiger. Three Benefits bullets are written from
verified behaviour: a pin fails in either direction, and a failing test
that supplies the clock and store reproduces.

…bsidian

Overview and Benefits rewritten for grammar and continuity; nolint is
disallowed outright per the intended design. Adds 30 inline citations and
a 16-entry References section (Power of Ten, Mars Code, Holzmann's Systems
Distributed '26 talk, Kudrjavets/Nagappan/Ball on assertion density,
McCabe, Campbell, Floyd, TigerStyle, VOPR, FoundationDB, Bernhardt,
Cockburn). Removes every mention of //tiger:restrict, restores the spawn
sentence tying the goroutine rule to pins, renames the illustrative
surface function to Prune, and fixes the inverted correctness/liveness
sentence in the assertions paragraph.