[CatarinaGamboa]

Renames the C4.2 error category from UNPROVABLE to UNKNOWN. Every refinement error means the verifier could not prove something, so "unprovable" does not set this case apart. What does is that nothing is known about the value or state.

• ErrorCategory: UNPROVABLE → UNKNOWN, title now starts with "Unknown:"
• RefinementError, StateErrorCategories and StateHints use the new name
• Test case ErrorUnprovableArgument.java → ErrorUnknownArgument.java, test methods in TestErrorCategories renamed

No behaviour change in verification. The codebook ID (C4.2) is unchanged.

API break: ErrorCategory is public and returned by LJDiagnostic.getCategory(), so clients that reference ErrorCategory.UNPROVABLE no longer compile, and serialized enum names change from UNPROVABLE to UNKNOWN. No client in the organisation (vscode-liquidjava, liquidjava-mcp) uses the old name. Releases after 0.0.36 carry this change.

Tests: mvn -pl liquidjava-verifier -am test passes (496 tests, 0 failures).

🤖 Generated with Claude Code

[CatarinaGamboa]

[Codex review] The internal rename is consistent: the category ID stays C4.2, the diagnostic and hint branches use UNKNOWN, and the full verifier suite passes locally at this head (./mvnw -q -pl liquidjava-verifier -am test). One compatibility detail missing from “No behaviour change”: ErrorCategory is public and returned by LJDiagnostic.getCategory(). External clients that reference ErrorCategory.UNPROVABLE will fail to compile against this version (and enum-name serialization changes). Please document this as an API break, or retain a compatibility path if consumers rely on that constant.

[CatarinaGamboa]

[Claude] Good point. The PR description now documents this as an API break: ErrorCategory.UNPROVABLE no longer compiles and serialized names change to UNKNOWN. I did not add a compatibility alias. No client in the organisation (vscode-liquidjava, liquidjava-mcp) references the old constant, 0.0.36 does not include the rename, and a deprecated duplicate constant would be a second category rather than an alias.