Grammar hygiene: remove two redundant parse paths (ambiguity reduction)

[christiankissig]

Summary

Removes two genuine duplicate parse paths in the grammar, found while investigating the Earley timeout bucket. Both are safe structural cleanups that shrink the parse forest with zero regressions.

Change	Why it was redundant
Drop context as a direct theory alternative	context is already reachable via theory → statement → context, so every theory had ≥2 parses at the root
Drop the terminal by in proof_prove	by already appears as a repeated proof step, which covers the terminal position; the duplicate gave every by-terminated proof two parses

Effect on ambiguous-node counts (proof snippets): a nested proof drops from 6682 → 2707 (~60%); by simp from 10 → 3.

Honest scope: this is hygiene, not a speed fix

Profiling shows parse wall-clock is dominated by Earley chart breadth (millions of Item.__init__ / symbol __eq__ in predict_and_complete's set-dedup), which scales with grammar breadth × input length — not with the output ambiguity these changes remove. Accordingly, wall-clock is essentially unchanged (e.g. an 8 KB proof-heavy file stays ~11.6 s). These changes are worth keeping because they remove real redundancy and reduce the SPPF/memory, but they do not address the timeout bucket.

The actual speed levers (documented for follow-up): reduce per-proof-step prediction breadth (proof_prove/proof_state/method alternations), the keyword-vs-name and embedded terminal overlaps the dynamic lexer can't prune, or a different parse strategy. The opt-in --timeout from #5 remains the pragmatic guard meanwhile.

Testing

• Full unit suite: 135 passed, no regressions.
• Regression-checked against a real-file sample with a strict ok→fail criterion (timeout flakiness excluded): 0 real regressions; 2 sampled timeouts recovered.

🤖 Generated with Claude Code