A Check That Tells Models Apart

In Part I we recorded two pieces of information about water and derived amphiproticity. Then we removed one piece, and the conclusion disappeared. These two cases check different sides of one promise: two premises suffice, and one does not.

Now imagine an error slipping into the rule — say, the proton-acceptance condition is dropped by accident. The two-premise scenario still gives the right answer. So one lucky example is not enough: we need a case where the right and the wrong rules behave differently.

First name the promise

Let us return to the familiar rule:

pub rule AmphiproticDonatesAndAccepts strict {
    label ru unofficial "способная и отдать, и принять протон частица амфипротна (14.1)";
    label en unofficial "a species capable of either donating or accepting protons is amphiprotic (14.1)";
    for s: Species;
    when donates_proton(s) and accepts_proton(s);
    then amphiprotic(s);
}

This rule carries at least three checkable requirements: both properties are needed; they must concern one particle; to test the inference, the conclusion must be derived from the inputs through this rule, rather than supplied in the case.

For each requirement we can pick a small change to the model that breaks it:

That states in advance what each check case is for. The expectation comes from the rule’s meaning and the source. The run then tests that expectation — the run’s own output must not become the expectation’s sole ground.

What the two-premise example notices

Scenario 14 of the chemical vocabulary reports both properties of water and expects TRUE_ONLY. If the rule AmphiproticDonatesAndAccepts is removed, the same information yields NEITHER. The scenario catches the lost conclusion.

Scenario 15 reports only proton donation and expects NEITHER. It passes both on the original model and on the model without the rule. The outcome matches, but the reasons differ: in one case a premise is missing; in the other, the very path to the conclusion is gone.

That does not make scenario 15 useless. It catches a different error: dropping the proton-acceptance condition. After that edit, a report of proton donation alone suffices, and TRUE_ONLY arrives instead of the expected NEITHER. One scenario may catch one error and miss another.

For experiments we can use the law engine mutate tool. It proposes changes to the program, for example remove_rule, drop_conjunct, and freshen_var_occurrence. The last replaces one occurrence of a variable with a fresh one. Such altered variants are usually called mutants[^chapter-17-mutation].

Here they serve as deliberately wrong models to compare against the original. If a change makes the model invalid, the language check catches it. The harder case is what matters here: the model stays valid, but the reasoning changes.

An error the earlier examples missed

Imagine that instead of one variable in two premises, the rule requires proton donation from a particle s and acceptance from some particle t. That is already a different statement: the properties may belong to different objects.

In the original water example the error stays invisible. Water both donates and accepts a proton, so either variable can bind to it. What is needed is a case that splits the properties.

Below is the author’s check based on scenario 15. One piece of information about another object is added. The header and context are kept so the example can be run as a separate .lawtest:

language "law.core" version "0.2";
package openstax.chemistry_acids version "0.1.0";
namespace "urn:openstax:clir:chemistry-acids";

test "urn:query:openstax-chem-acids-15-book-water-one-role-no-conclusion" {
    given {
        context {
            decision_time @2026-09-06T12:00:00Z;
            knowledge_time @2026-09-06T12:00:00Z;
            legal_time @2026-09-06;
            timezone "UTC";
        }
        assert donates_proton(entity_ref("urn:case:chem:h2o")) { id "k15-1"; origin case_input; }
        assert accepts_proton(entity_ref("urn:case:book:other")) { id "book-other-accepts"; origin case_input; }
    }
    evaluate truth(amphiprotic(entity_ref("urn:case:chem:h2o")));
    expect truth_status == NEITHER;
    expect evaluation_status == COMPUTED;
}

Donating belongs to h2o, accepting to other. We ask about h2o‘s amphiproticity. On the original model the answer is NEITHER: information about another object does not satisfy the premise about water.

On the altered model, where the acceptance premise carries a substituted variable, the answer becomes TRUE_ONLY and the test fails. That is exactly the difference we wanted to catch.

All 22 earlier scenarios still pass on that altered rule. The new case exposes a specific coverage gap: none of them splits the properties across objects in a way that fits this error. A count of passing checks alone does not reveal that gap.

For the symmetric error a mirror check is needed: water accepts a proton, and another object donates a proton. Then substituting the variable in the donation premise becomes visible too.

The same answer may come another way

Scenario 14 has one more expectation:

expect applied(AmphiproticDonatesAndAccepts);

It checks that the named rule took part. To see its use, take a temporary copy of the model. Give the original rule an extra condition that the case leaves unknown, and add a second rule deriving amphiproticity from the same two premises. Before running the changed model, predict the truth status and the rule-application check separately.

The water question still yields TRUE_ONLY, so the answer-only check passes. But the applied(AmphiproticDonatesAndAccepts) expectation fails: the conclusion came through a different rule. The explanation exposes the substitution.

At the same time, applied does not prove the named rule was the answer’s only ground, nor that its premises faithfully express the source. To assess that, we must read the rule itself and the matching branch of the explanation. The expectation has one particular job[^chapter-17-applied]; do not stretch its meaning further.

The same holds when no conclusion is established. On NEITHER, check what was missing: information, a reading choice as in Chapter 14, an applicable edition as in Chapter 13, or a rule. A matching status alone does not mean matching reasons.

Check the intermediate steps

The model on Gauss’s Disquisitiones Arithmeticae checks a supplied trace — a step-by-step record of a modular exponentiation calculation: raising a number to a power and finding its remainder after division by a fixed number. To follow the example, it is enough to know that a remainder is what is left after division.

The case reports base 2, divisor (or modulus) 341, and several “exponent — remainder” pairs. The model checks the links between them: when the exponent doubles, the remainder must match the square of the previous remainder taken modulo the same modulus.

In scenario 10, exponent 5 is recorded with remainder 33, and exponent 10 with remainder 1. Let us check the pair independently:

33² = 1089
1089 = 3 · 341 + 66

The independent calculation gives remainder 66, not 1.

(Author’s paraphrase of the reported engine result; the full output is not reproduced here.) The rule VestigiumFalsumInDuplicatione detects the inconsistency and derives vestigium_falsum. The query yields TRUE_ONLY, COMPUTED, and the explanation points to these two recorded steps.

The model also checks adjacent exponents: when the exponent increases by one, multiply the previous remainder by the base and take the remainder modulo the same divisor. This explains the second error, from remainder 16 at exponent 4 to remainder 33 at exponent 5: 16 · 2 = 32, already below 341, so the next remainder must be 32. The rule VestigiumFalsumInGradu checks that link.

Scenario 12 removes a link needed to build the checked chain. Here it is not enough to check equalities for the pairs at hand: we must also establish that the chain reached the declared final exponent 340.

(Author’s paraphrase of the reported engine result; the full output is not reproduced here.) A separate rule does this job. It reads the declared limit and not_known(catena(...)): no checked chain reaching it is established. The result is vestigium_ruptum: the trace breaks. Here 340 is the exponent the checked chain must reach.

That is how the check tells apart a wrong link and a missing path to the goal. Neither result on its own proves Fermat’s little theorem or that 341 is prime. The check’s subject is narrower: the consistency of the presented computation trace[^chapter-17-trace].

What repeating a calculation checks

So far we asked whether the model behaves as its stated rules require. One question remains: did the recipient repeat the calculation they were handed?

The calculation document holds the input manifest, the answers, and the explanation graph. The resultHash field serves as the fingerprint of its canonical contents. Comparing fingerprints catches a difference between documents even when both show TRUE_ONLY.

But a matching fingerprint does not check whether the author read the source rightly. It establishes which particular calculation was reproduced. Substantive checks and repetition checks solve different problems; the last chapter runs both.

Try picking the missing check

Work with a copy of the chemical package. First predict the outcome of scenarios 14 and 15 if accepts_proton(s) is removed from AmphiproticDonatesAndAccepts. Then make that edit and prepare the program with the law engine lower command and run the unchanged tests with law engine test --program. Scenario 14 must pass, and 15 must catch the error.

Then take the two-object check above and swap the relations: water accepts, another object donates. Confirm the explanation above by checking which of the two variable substitutions this case catches.

Finally, for one rule of your own, write down its promise and two examples: where it must produce a conclusion and where a nearby case must not yield that conclusion. If both examples pass after removing an essential condition, the check needs refining.

The final scenario set does not prove the model complete. It shows which differences we can detect. Hand over that knowledge with the model too: what was checked, by which case, and which boundary stays unchecked so far.

[^chapter-17-mutation]: The CLI’s mutation notes applies local changes to the CLIR program and checks that the result is valid. The original chemical set holds 22 scenarios. The count of passed cases concerns a particular mutation, not the model’s completeness. [^chapter-17-applied]: Scenario 14 separately checks truth_status and applied. The original rule links both premises with one variable; the alternative rule in the experiment is a study change to a temporary copy. [^chapter-17-trace]: The trace-check rules, scenario 10, and scenario 12. The first rule compares the presented remainders, the second checks the absence of an established catena up to the declared limit.