Deducible ≠ known (the third ceiling)

Parent: recursive-harness

A trouble the clean CSP form hides: the constraints entail the answer, but deriving the entailed facts is intractable. Knowing all the axioms doesn't tell you which theorems are true.

Entailment vs derivation-within-budget

• The constraint set C entails (⊨) the solution set S — in principle every consistent assignment is pinned by C.
• But deriving an entailed fact (e.g. "x₃ = m₂ in every solution") may need full search: CSP satisfiability is NP-complete; detecting truly-forced values is exponential.
• Arc-consistency (AC-3) is sound but incomplete: it derives some entailed facts in polynomial time and misses the rest (deriving the rest = solving the CSP).

→ Exactly the math analogy: the axioms entail all theorems, but knowing theoremhood is undecidable / intractable. Once complexity is high enough, entailed ≫ derived.

This corrects the □/◇ read-off

• "□ = domain collapsed to singleton (by propagation)" is only propagation-visible forced-ness — a sound under-approximation of true forced-ness (entailment);
• "◇ = domain still has values" is an over-approximation of true openness (some surviving values are already deducibly dead, just not yet derived).
• True □/◇ = entailment = hard. The agent acts on incomplete knowledge of its own constraints' consequences.

Three consequences

1. A committed world can be deducibly-dead without the agent knowing — the contradiction is "derivable but not yet derived"; only deeper search hits it → backtrack. So backtracking is also "doing a deduction you'd skipped," not only "you chose wrong."
2. "Converged" = "consistent as far as bounded search checked," not "consistent in the full deductive closure." The gap = derivable-but-unchecked contradictions.
3. A third ceiling, beside the other two:
   • capability (recursion-is-a-phase-transition): can the model contract at all (k<1)?
   • observability (convergence-needs-an-observable-target): is the target identifiable?
   • deductive tractability (this): even determined and observable, finding the consequence is NP-hard / proof-search unbounded. The gap grows with complexity.

P×C does double duty: it also budgets the deduction search

Earlier P×C set decomposition depth; it also bounds how hard you search for contradictions:

$$\text{stop searching consequences when}\quad \Pr[\text{undeived contradiction}]\times\text{cost}\le\theta_{P\times C}.$$

i.e. satisfice on consequences too — don't compute the full closure, search only until the expected cost of a missed contradiction is acceptable. This is Simon's intelligence-is-satisficing-under-scarcity: under bounded compute you can't know all entailed truth, so you satisfice.

What the LLM actually does in propagation

Pure mechanical propagation (AC-3) is incomplete — it can't derive most entailments. The LLM is the heuristic for that intractable deduction: it guesses (well) which consequences hold instead of deriving them.

• its errors = heuristic vs true-entailment gap;
• "deducible ≠ known" is exactly the gap the LLM's heuristic (imperfectly) fills.
• That's why you need the LLM at decompose and constraint-eval: the entailments propagation can't afford, it guesses.

Revisited — under the theory layer

• "Satisfice on consequences" is now a row in the price list: how much closure a unit of P×C buys is the relaxation exchange-rate question, and "search until expected missed-contradiction cost ≤ θ" is its P×C instantiation.
• "The LLM guesses the entailments propagation can't afford" is coupling-to-the-learner's landscape: the guess is cheap and good on-manifold, and that non-uniformity is why the heuristic is usable at all.
• The third ceiling composes with the other machinery: bounded deduction is safe only because missed contradictions surface later as conflicts and are then learned / sent up as cuts — lazy deduction + monotone conflict knowledge together replace the closure you can't compute.

One line

The constraints entail the answer but don't hand it to you — deriving entailments is NP-hard / undecidable, so the agent's □/◇ is an approximation of true forced-ness, "convergence" is consistency-as-checked (not closure), and P×C doubles as the deduction-search budget. The LLM is the heuristic standing in for the deduction you can't afford.