ZTL Judge

Check an algebra derivation step by step: does each step keep exactly the same solutions? Args: request: {"equations": ["x^2 = x", "x = 1"], "var": "x", "domain": [lo, hi] or null, "domain_verified": true}. Each equation is the next step; one unknown; + - * / ^ with whole powers. Returns: The chain's verdict (its weakest step) and each step's: EARNED = same solutions on the domain; ON CREDIT = the same, on an unverified domain; REFUTED = a solution is lost (e.g. cancelling a factor that can be 0) or gained (e.g. clearing a denominator where the original was undefined), with the witness and the cause; E = the step divides by an expression that is 0 for every value. A request above the public limits is refused with the reason (ok: false, refused).

Ready requests for check_steps and judge_naive (the kernels' own examples).

Worked examples: questions already written as ZFL documents, ready to judge.

Judge a ZFL document with ZTL, a zero-trust logic: three values, two-valued connectives. Args: document: The ZFL document, as an object or as JSON text: {"rows": [{"name": ..., "means": ..., "status": ..., "ground": ...}], "claim": ...}. Returns: The verdict with its disposition and grade, the receipt, the instruments that applied, the issues found, and what the core read. Read the verdict WITH its disposition: T EARNED = established; F REFUTED = false; F OPEN or Z OPEN = NOT ESTABLISHED, it could still turn either way (do not report it as false) — `why` and `unverified` say what to check; ON CREDIT = holds only on an unverified ground. A compound claim gets T or F; a claim that is a single name gets that name's own value, Z while unverified. The full report is returned whatever `ask` says.

Judge sets defined by a property, self-reference allowed (Russell's set, a web of trust, a policy rule). Args: universe: {"sets": {name: {"list": [...]} | {"data": {name: "T"|"F"|"Z"}} | {"abs": formula}}, "claims": [formula, ...]}. Formulas: ["in", a, S], ["not", f], ["and"|"or"|"imp"|"iff", f, g], ["all"|"ex", "y", f], ["eq", S, T]; an abs set's own variable is "x". Every name is also an object. Returns: Per set: the members and non-members the definitions ground, and a passport for each membership they leave undecided — PARADOX (no stipulation can repair it), UNDERDETERMINED (consistent; a decision is owed), INTRINSIC, INPUT (verify the given cell), DOWNSTREAM (inherits a quarantine). Per claim: EARNED / REFUTED / EARNED IF STABLE / REFUTED IF STABLE / OPEN, the cells it rests on with their passports, and for a universal claim the instances left undecided. Oversized requests are refused with the reason.

The ZFL language: the columns of a row, the document fields, their meaning and rules.