One type, three semantics

The manifest answers with a threshold: consensus_disagreement > 0.25. But the rule does not say what the number measures. Rather than choose for the author, the specification fixes the metric’s type (a fact-by-checker answer matrix of nullable Booleans, mapped to a scalar in [0, 1] against the factored threshold; the codomain is a checked constraint, TYPE-01) and exhibits three type-satisfying metrics with different semantics, evaluated on the same matrix. All three satisfy the type; none is thereby correct. They do not agree on whether the gate fires, and, on the ensemble the recorded run used, two of them cannot fire it at all.

The answer’s base type is a nullable Bool, chosen for type-checking support as much as for clarity. The semantics: given a datum as context, and irrespective of which Cog produced it, each checker answers one question, “do you agree with the datum?”. True is agreement, False is disagreement, and null is cannot tell (the same outcome the Track records as earl:cantTell). Checkers are factored apart from generators on purpose: it is strictly possible for a Cog to produce a datum and still answer False when asked whether that datum is true. One could assume a producer always files True about its own output; the specification does not, and a Cog’s answer about its own datum is one column like any other (clarifications logged with GAP-04 in the open-questions chapter). The matrix is rectangular, and a run with no facts scores zero.

A correctly constructed policy is not the same as a fit-for-purpose policy. What is right for the job here is an open algorithmic policy design question, likely to have no unique correct answer but many viable answers with different implications on incentives, and the right answer is not limited to these three.

1The type, in the model¶

The abstract definition carries the type signature and five property attributes (what the value is a fraction of, how a null is treated, monotone in dissent, saturates at unanimous dissent, invariant under ensemble size). It splits along one axiom into two branches: a DisagreementMetric measures how much dissent a run carries and is monotone in it; an UndecodabilityMetric measures whether facts resolve and is not. Three concrete definitions specialize the branches, each documenting its semantics and its incentive implication and redefining the attributes its branch leaves open. The split names the under-specification the first version of this chapter only exhibited: the original single class could not distinguish two different quantities that both fit the type (a finding of the second external review, ruled on as a refinement of GAP-04). The table is parsed from the model: each row is one definition with its doc, verbatim.

The structural fact sits in the comparator oracle. Its metric slot is typed by the abstract definition and deliberately left unbound (part metric : ConsensusInadequacyMetric; with no concrete binding): the model states that a metric of this type is required and refuses to choose one (GAP-04 in the open-questions chapter). A deployment binds it, and in doing so picks a branch, which is a visible policy decision; the Track records which one a run used, and the matrix it ran on. The sharper punchline comes later in the chapter: two of the three type-satisfying bindings make the gate unreachable on the very ensemble the Track records.

2The three implementations¶

The same three semantics as running code, satisfying the declared type:

• dissent-fraction counts every answer that is not True, null included: honest abstention is punished, so checkers are pushed to affirm rather than say cannot tell. On the paper’s own section 5.5 example (three Cogs, two must agree) it FIRES the gate at 0.25, contradicting the example’s intent.

• strict-quorum-undecodable counts facts where no answer reaches a quorum of two matching non-null answers; null blocks quorum, so it escalates more, spending expert-review capacity. The quorum is the paper’s two-of-three, deliberately, and the metric is admissible for a three-checker ensemble only (with one checker, unanimous agreement scores 1; with nine, two agreements outvote seven dissents).

• erasure-aware-undecodable treats null as an erasure, not an error: a lone expressed voice among abstentions decodes, so abstention shifts power to whoever still answers.

Both undecodability metrics are “consistent with the section 5.5 example”, and the reason is not flattering: on three checkers with no abstention they are identically zero (shown below). Consistency with the example is a consequence of never firing, not evidence of fitness.

Could the signature live in the model as a calculation rather than as annotation? Partly. The pinned evaluator accepts a calc def with typed scalar parameters (probed, 2026-09-05); carrying a nullable-Boolean matrix and three alternative bodies through it was not attempted. So the signature is carried as declared attributes in the model and as Python here, and the test suite holds the two equal. That is the same honest division as the wiring rules in chapter 2: the model states, code checks.

3What each metric is, proved¶

The doc comments above make claims; the attributes make assertions; the cell below checks them. For each property the model declares, the implementation is enumerated over every answer matrix of up to two facts by three checkers (the test suite goes to three facts), and the declared value is compared with what the enumeration finds, with the minimal counterexample wherever a property fails to hold. Two results deserve a sentence each. Flipping one answer from agree to disagree can decrease both undecodability metrics: [T, F, null] scores 1.0 and [F, F, null] scores 0.0, because unanimous disagreement decodes. And a matrix of unanimous disagreement scores 0.0 under both, which is why they are not disagreement metrics and the class had to split.

4Two of three bindings cannot fire the gate on this ensemble¶

The recorded run names three Cogs. With three checkers over a two-valued answer domain, some value occurs at least twice, so the strict quorum is always met, and the majority strictly exceeds half, so the erasure-aware rule always decodes. Both undecodability metrics are identically zero on every answer matrix without an abstention. No threshold makes GATE-02 fire under them; only a null can. This is not “the bindings disagree at the margin”; it is a structural difference in what the gate is capable of doing under each binding, on the exact configuration the Track records. The cell reads the ensemble size from the Track and enumerates.

5The convention that binds model to code¶

The model cannot hold Python, and this walkthrough does not pretend it does. The binding between a part def and the function that implements its logic is a stated, mechanical convention, checked in both directions. A definition’s metric id is derived from its name (DissentFractionMetric becomes dissent-fraction); the same id keys the implementation mapping in exhibits.py and is the value a Track records in vfr:metric. The cell verifies the correspondence is one-to-one — every model definition has an implementation, every implementation has a definition — and that the metric run-001 cited resolves to a bound implementation. In a deployment, the same id is how the comparator oracle’s configuration names the metric it bound into the open slot.

6One matrix, three answers¶

The same answer matrix, the threshold read from the model’s single point of definition, and different gate decisions. The headline matrix is constructed so that no metric lands on the threshold. A second matrix is kept apart as the boundary case: under it one binding scores exactly 0.250, and the decision turns entirely on the comparator, which is the manifest’s own strict >, verbatim from the section 5.6 rule (so its strictness is source text, not a judgment call). The Track records which metric a run actually used; recording is not endorsing.

One more thing the single point of definition conceals: the three metrics do not share a denominator. dissent-fraction is a fraction of answers; both undecodability metrics are fractions of facts. The one number 0.25 therefore means different things under different bindings. The threshold stays where the manifest puts it, on the policy, and each metric now declares its denominator as a model attribute so the difference is a model fact rather than a reading of the code (GAP-11 in the open-questions chapter).

7The recorded run, under all three bindings¶

The Track records the consensus reading’s metric and its output. Since the second external review it also records its input: the answer matrix the comparator ran on (GAP-12 in the open-questions chapter). So the recorded value can be recomputed by anyone holding the record, and the question this chapter raises can be asked of the run rather than of fabricated data: what would the other two bindings have said about these answers? The matrix is fabricated like the rest of run-001, but it is the run’s, and the audit below is the one an auditor could perform.

8How often the choice matters¶

One matrix proves the bindings can disagree. It says nothing about how often, or where. The sweep below draws answer matrices from a stated generative model (independent cells; abstain with probability p_abstain, otherwise dissent with probability p_dissent), twelve facts by the recorded three checkers, and reports how often the three bindings fail to agree on the gate decision, and how often each fires. The marginal firing rates are the number a policy designer can budget against: the expert-review load each binding would impose on the same stream of runs. The heaviest binding fires about five times as often as the lightest. That is the incentive claim from the bullets above, as a quantity.

The caveat is stated in the cell’s docstring and repeated here: real checkers are correlated, and correlated dissent is exactly what a consensus gate exists to catch, so these numbers are a lower bound on how much the choice matters. A correlated-checker variant is logged as future work in the judgment record.