Coherence score range

The HaltMonitor model in HaltMonitor.Core reasons about an abstract Score flowing through the streaming-halt loop. This file gives that score a concrete model at the level of CoherenceScorer.calculate_coherence in src/director_ai/core/scoring/scorer.py, and proves the property the rest of the pipeline (thresholding, halting, monotonicity) silently assumes:

The composite coherence score always lies in the unit interval [0,1].

The Python computation modelled here is the core path of _score_and_evidence:

total_divergence = self.W_LOGIC * h_logic + self.W_FACT * h_fact
coherence = 1.0 - total_divergence

with W_LOGIC + W_FACT == 1, both weights non-negative, and each divergence component already clamped to [0,1] upstream (max(0.0, min(1.0, …))). That makes total_divergence a convex combination of two unit-interval values, hence itself in [0,1], so coherence = 1 − total_divergence ∈ [0,1].

The rescaling branch in the Python code applies an explicit max(0.0, min(1.0, …)); clampUnit models that clamp and is proved to land in [0,1] unconditionally, and to be the identity on scores that are already in range (so clamping never perturbs a valid score).

This is FVGK programme phase 1: the abstract Score of the halt model is now backed by a scorer-level model whose output range is machine-checked, not assumed. All proofs are core Lean 4 (no Mathlib).

structure HaltMonitor.UnitValue : Type

A value constrained to the closed unit interval [0,1].

Mirrors a divergence/probability component after the upstream max(0.0, min(1.0, …)) clamp in the Python scorer: it cannot be negative and cannot exceed one. Rational so the model stays decidable and executable.

• val : Rat

  The underlying rational value.

• lo : 0 ≤ self.val

  The value is non-negative.

• hi : self.val ≤ 1

  The value does not exceed one.

structure HaltMonitor.CoherenceScore : Type

The two-component coherence model.

hLogical and hFactual are the logical- and factual-divergence components (h_logic, h_fact in the Python scorer), each a UnitValue. wLogical and wFactual are the mixing weights (W_LOGIC, W_FACT): non-negative and summing to one, i.e. a convex combination.

• hLogical : UnitValue

  Logical-divergence component (NLI contradiction probability).

• hFactual : UnitValue

  Factual-divergence component (ground-truth deviation).

• wLogical : Rat

  Weight on the logical-divergence component.

• wFactual : Rat

  Weight on the factual-divergence component.

• wLogical_nonneg : 0 ≤ self.wLogical

  The logical weight is non-negative.

• wFactual_nonneg : 0 ≤ self.wFactual

  The factual weight is non-negative.

• weights_sum_one : self.wLogical + self.wFactual = 1

  The weights form a convex combination (sum to one).

def HaltMonitor.CoherenceScore.totalDivergence (c : CoherenceScore) : Rat

Total divergence: the convex combination of the two component divergences. Mirrors total_divergence = W_LOGIC * h_logic + W_FACT * h_fact.

def HaltMonitor.CoherenceScore.score (c : CoherenceScore) : Rat

The composite coherence score. Mirrors coherence = 1.0 - total_divergence.

theorem HaltMonitor.CoherenceScore.totalDivergence_nonneg (c : CoherenceScore) : 0 ≤ c.totalDivergence

Total divergence is non-negative: each weighted component is a product of two non-negatives.

theorem HaltMonitor.CoherenceScore.totalDivergence_le_one (c : CoherenceScore) : c.totalDivergence ≤ 1

Total divergence does not exceed one: bounding each component by its weight (w * h ≤ w * 1 = w) and summing gives wLogical + wFactual = 1.

theorem HaltMonitor.CoherenceScore.score_nonneg (c : CoherenceScore) : 0 ≤ c.score

Lower bound. The composite coherence score is non-negative — a token can never be assigned a negative coherence. Follows from totalDivergence ≤ 1.

theorem HaltMonitor.CoherenceScore.score_le_one (c : CoherenceScore) : c.score ≤ 1

Upper bound. The composite coherence score never exceeds one. Follows from 0 ≤ totalDivergence.

theorem HaltMonitor.CoherenceScore.score_mem_unit (c : CoherenceScore) : 0 ≤ c.score ∧ c.score ≤ 1

score() ∈ [0,1]. The composite coherence score always lies in the unit interval — the range invariant the halt monitor, thresholding, and monotonicity proofs assume of the abstract Score, now machine-checked for the scorer model.

def HaltMonitor.clampUnit (x : Rat) : Rat

Clamp a rational into [0,1], modelling the Python max(0.0, min(1.0, x)) applied on the rescaling branch of the scorer.

theorem HaltMonitor.clampUnit_nonneg (x : Rat) : 0 ≤ clampUnit x

The clamp output is non-negative, regardless of input.

theorem HaltMonitor.clampUnit_le_one (x : Rat) : clampUnit x ≤ 1

The clamp output does not exceed one, regardless of input.

theorem HaltMonitor.clampUnit_mem_unit (x : Rat) : 0 ≤ clampUnit x ∧ clampUnit x ≤ 1

clampUnit x ∈ [0,1]. The explicit clamp guarantees the unit interval for any input — so the rescaling path cannot produce an out-of-range score.

theorem HaltMonitor.clampUnit_id_of_mem {x : Rat} (h0 : 0 ≤ x) (h1 : x ≤ 1) : clampUnit x = x

The clamp is the identity on values already in [0,1]: it never perturbs a score that is already valid, only reins in out-of-range ones.

theorem HaltMonitor.CoherenceScore.clamp_score_eq (c : CoherenceScore) : clampUnit c.score = c.score

Clamping a coherence score is therefore a no-op: the model already proves the score is in range, so the production clamp is a defensive belt-and-braces, never a correction.