F-Identity: name the two identity predicates and say which is normative (#59)

[lex00]

Closes #59.

The specification stated two identity tests for captures and never reconciled them. F-Import's is typeof object or function; F-Val-Live's recurses through plain objects and arrays and rejects a plain { a: 1 }. A reader implementing from the text could use either for both uses and be wrong in one of two directions — the narrow one everywhere loses capture edges, the broad one everywhere makes every parameter helper a taint source.

F-Identity lands in J3's definitions and resolves it:

• the entity test (F-Val-Live) is normative, because the proposition is about entities the build names and serializes, and two structurally equal plain objects that no AttrRef points at cannot be told apart in the output
• the reference test (F-Import) is a deliberate over-approximation: an imported binding is nearly always an entity, and one typeof is cheaper than a recursive walk of every resolved import
• the cost is coverage rather than correctness, which is F-Direction
• whether to narrow F-Import is left as a question for measurement, since it changes which files fold

Also in this change:

• F-Capture and F-CallLeak say which test each uses
• values.md's claim that liveness is what F-Capture tests was wrong and is corrected
• packages/reference's comments cite F-Identity rather than pointing at CAVEATS.md for an open question; that section of CAVEATS.md becomes a pointer
• F-Succ/backward-along-captures cites F-Identity, since the value it captures is plain and the edge exists only because F-Capture over-approximates
• the prose baseline ratchets 212 to 211

🤖 Generated with Claude Code

https://claude.ai/code/session_01RfnRhfdYHLFAZJKHwZhBYc