[Essoz]

An independent precondition solve could remove a clause from all later solves in the same process: _pruned_clauses=set() was allocated once at function definition and updated in place.

Use a None default and initialize a fresh set only when none is supplied. Recursive children continue sharing the explicit set, and caller-supplied sets retain their existing update/reuse behavior.

Concrete reproduction with real trace/clause inference: solve A has phase train in both positive and negative examples and distinguishes them by signal=True versus False. A learns the signal clause and prunes the phase clause. Independent solve B needs phase=train to distinguish positive train from negative eval:

Fresh-process sequence	Preconditions before	After
B	1	1
A, B	1, 0	1, 1
B, A	1, 1	1, 1
B, B	1, 1	1, 1

Python RNG state is unchanged in every sequence. This exposes dependence on prior process history, including which earlier tasks ran in a reused worker, independently of RNG.

Validation: six focused tests had five failures before the fix and all pass afterward. Coverage includes independent/reversed/repeated solves, fresh-process versus warm-process histories, explicit set reuse, recursive sibling sharing, and separate root sets. Repository-pinned Ruff/Mypy/Black/isort hooks pass. Compact reproduction evidence and a test command are in docs/measurements/precondition-state-isolation.md.

A complete configured replay on the same 573,494-row trace also finished: 835 → 836 emitted invariants; 105 → 104 failed hypotheses. All 940 non-precondition hypothesis identities match. One Linear.forward → checkpoint._internal_assert hypothesis moved from failed to emitted; 833 previous emitted records are structurally identical. Two others gain substantive constraints: RMSNorm.forward → checkpoint._internal_assert goes from one to seven clauses, and get_rng_state → current_device from two to three. These are not clause-order differences.

That replay applied only the two production hunks to the cache candidate, preserving its existing RNG isolation; this PR's standalone source/base remains unchanged. All 17 combined tests passed. The single-worker replay disabled FunctionLeadRelation and FunctionCoverRelation; source/input hashes and context states were unchanged. Compact source and output evidence is in docs/measurements/precondition-state-isolation-replay-20261025.json.

All three changed/new predicates contain concrete trace-specific thread IDs. Their applicability to future checking runs is unvalidated. The output changes are not ground-truth correctness labels or a speed/memory comparison. This PR does not claim global order/scheduling determinism, unchanged large-trace outputs, or a multi-worker-count matrix.

Engineering hardening

Signed commit aec748e gives the regression records, solve fixtures, and recursion observer explicit types. The observer requires the actual recursive call fields, and fresh-process tests compare the complete expected serialized precondition. Production behavior is unchanged. Pinned Mypy 1.9 reports 14 → 0 errors for the test module with --check-untyped-defs --disallow-untyped-defs --disallow-any-generics --follow-imports=silent --ignore-missing-imports; this scoped result does not certify strict typing of imported legacy modules. All six tests pass, the repository hooks pass, and explicit pinned Ruff/Black/isort checks pass for the test file. The earlier full-replay results remain tied to their recorded source revisions; this hardening adds no performance claim.