diff --git a/docs/formal/evidence-verification.md b/docs/formal/evidence-verification.md new file mode 100644 index 0000000..7874c09 --- /dev/null +++ b/docs/formal/evidence-verification.md @@ -0,0 +1,104 @@ + +# Formal verification plan — evidence mode (issue #7) + +**Status: adopted 2026-09-26.** Companion to +[`verification-plan.md`](verification-plan.md) (issues #20, #21), same prover and +guardrails: Agda, `--safe --without-K`, no postulates, negative controls in +`proofs/agda/reject/`. This document fixes what the evidence library proves, +what it deliberately does not, and how it is tied to the code the server and +the Evidence Mode UI run. + +## 1. The gap being closed + +The standalone reference explorer (in `residual-evidence-types`) computes +presence verdicts for the signed finite model in separately tested JavaScript, +and its own footer admits there is **no proved extraction correspondence** +between that script and the Agda naturals example shipped beside it. Evidence +Mode (issue #7) turns those verdicts into first-class UI state — avec_fibre +edits, the fibre visualizer, the residual explorer's noise-bound slider — so +the correspondence can no longer be folklore: this library establishes the +signed finite model's decision procedures as *proved correct*, and the golden +vectors pin the same answers across every implementation. + +## 2. Layering + +| Layer | Content | Status | +|-------|---------|--------| +| **L0 abstract semantics** | `Candidate observe r E = Σ W ((observe w ≡ r) × E w)`; a `Case` carries one consistency witness while `Holds` quantifies over **all** candidates; `Identified` = unique query value across candidates; `actual-world-sound` (a warranted claim about candidates says nothing about reality until the actual world is shown admissible); `Echo`/`AvecFibre` (artefact carries semantic fibre ⇔ its echo fibre is inhabited) and the total-space factorisation; `Warrant`/`Epi`/`SoundWarrant` and `epi-does-not-give` — a warrant token is not truth. | Proved, generic (any `W`, `O`, `E`). | +| **L1 signed finite model** | `signed-integer-v1`: values in [−6, 6] as ℕ offsets, so every predicate is decidable on ℕ and the model is *executable inside Agda*; observation views (exact / sign / magnitude), admissibility (domain bound, noise bound, optional zero assumption); enumeration `candidates = filter cand? allWorlds`. | Proved: `candidates-sound` (listed ⇒ satisfies the specification) and `candidates-complete` (satisfies ∧ b ≤ 6 ⇒ listed). | +| **L2 decision procedures** | `decide`, `verdict₂`, `result` — the exact computation the server routes and the residual explorer run, with the four semantics theorems below. | Proved; plus `finitely-refute-identification` and the five reference presets as computed, proved terms. | +| **L3 implementation seam** | The Julia routes and the TypeScript UI. | Not proved. Pinned by the golden vectors (§4). | + +## 3. The four verdict theorems (Decision.agda) + +For `cs = candidates view r₀ b z` with `b ≤ 6`: + +| Computed verdict | Proved meaning | +|---|---| +| `entailed` | `FHolds … Present` — every admissible candidate has u ≠ 0 | +| `refuted` | `FHolds … Absent` — every admissible candidate has u = 0 | +| `unresolved` | `¬FHolds … Present` **and** `¬FHolds … Absent` (explicit witnesses of each kind) | +| `inconsistent` | `¬ FCase` — no admissible candidate exists. An empty candidate set does **not** make every claim vacuously true: there is no inhabited case at all, so no claim is issued. | + +Identification is *not* a verdict: presence without uniqueness is exactly the +"Present, value unknown" preset, and `present-without-identification` proves no +value is identified there. The negative control +`reject/IdentificationWithoutUniqueness.agda` is the UI bug Evidence Mode +exists to prevent — reporting an identified value from a mere presence verdict +— as a term that must fail to type-check. + +## 4. Golden vectors — the theorem-to-test map + +`proofs/vectors/evidence_vectors.json` (regenerate: +`python3 scripts/gen_evidence_vectors.py`) holds 546 cases: 13 residuals × +7 noise bounds × 3 views × 2 zero-assumptions, covering all four verdicts and +both identification outcomes. The durable encoding of the semantics is the +generator; Agda pins it as follows: + +| Vector field | Agda anchor | +|---|---| +| `candidate_count` | `length (candidates …)` | +| `presence` | `decide (candidates …)` + the four theorems | +| `identified_values` | `values (candidates …)`; singleton ⇔ identified | +| `first_candidates` | `candidates-sound` / `candidates-complete` | + +Follow-up stacks consume the same file from Julia (`test/unit`) and bun +(`frontend/tests`), so Agda, Julia and TypeScript are bound to one truth +rather than three agreeing-by-accident implementations. + +## 5. What is deliberately **not** proved + +- **The server and UI code** (L3): pinned by golden-vector tests, not proofs. +- **Beyond the grid**: the model is finite by design (|values| ≤ 6, bounds ≤ 6). + Infinity is not approximated here; it is out of scope. +- **Function extensionality**: `Echo.agda` states both fibre encodings and the + total-space factorisation without funext, keeping the suite's assumptions at + zero (the ILR plan's §1 guardrails). +- **A general extraction**: `epi-does-not-give` proves there *cannot* be one — + the reason warrant tokens must be checked against their receipts in code + rather than trusted. + +## 6. Module map + +``` +proofs/agda/MetaManifold/Evidence/ + Prelude.agda stdlib-free prelude (only Agda.Builtin.*): ⊥/¬_, ⊎, ×, + ∈ as a recursive proposition, subst/J, if/filter, _∸_, dist + Residual.agda L0: Candidate/Case/Holds/Identified, actual-world-sound, + different-candidates-refute-identification, no-free-weakening + Echo.agda L0: Echo fibres, AvecFibre, sans-fibre, total-space factorisation + Warrant.agda L0: Warrant/Epi/SoundWarrant, epi-does-not-give + Signed.agda L1: the signed finite model; enumeration sound + complete + Decision.agda L2: verdicts computed and proved; presets as proved terms +proofs/agda/reject/ + IdentificationWithoutUniqueness.agda must fail: presence ≠ identification +proofs/vectors/ + evidence_vectors.json the L3 pin (§4) +``` + +The `Evidence.*` modules import only `Agda.Builtin.*` — no stdlib — so the +whole evidence library type-checks under any Agda ≥ 2.6.4.3 even where the +standard library is unavailable; the estate pin (2.6.4.3 + stdlib 2.1) remains +the CI toolchain for the suite as a whole. diff --git a/proofs/agda/MetaManifold/All.agda b/proofs/agda/MetaManifold/All.agda index e45a897..139938f 100644 --- a/proofs/agda/MetaManifold/All.agda +++ b/proofs/agda/MetaManifold/All.agda @@ -20,3 +20,12 @@ import MetaManifold.ILR.Invariance import MetaManifold.ILR.Orthonormal import MetaManifold.ILR.Comb import MetaManifold.ILR.Integer + +-- Issue #7: Evidence Mode — candidate semantics, the signed finite model, +-- and the decision procedures the server routes and residual explorer run. +import MetaManifold.Evidence.Prelude +import MetaManifold.Evidence.Residual +import MetaManifold.Evidence.Echo +import MetaManifold.Evidence.Warrant +import MetaManifold.Evidence.Signed +import MetaManifold.Evidence.Decision diff --git a/proofs/agda/MetaManifold/Evidence/Decision.agda b/proofs/agda/MetaManifold/Evidence/Decision.agda new file mode 100644 index 0000000..6770f09 --- /dev/null +++ b/proofs/agda/MetaManifold/Evidence/Decision.agda @@ -0,0 +1,407 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: AGPL-3.0-only +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Decision procedures for the signed finite residual model, and the proofs +-- that they exactly decide the Candidate semantics of Residual.agda. +-- +-- These are the procedures the MetaManifold server routes (issue #7) and the +-- residual explorer UI run — here executed inside Agda itself and proved +-- correct, which closes the gap the standalone reference explorer honestly +-- flagged ("separately tested JavaScript, with no proved extraction +-- correspondence"). +-- +-- decide cs = entailed ⇔ Holds Present (every candidate has u ≠ 0) +-- decide cs = refuted ⇔ Holds Absent (every candidate has u = 0) +-- decide cs = unresolved ⇔ ¬Holds Present ∧ ¬Holds Absent +-- decide cs = inconsistent ⇔ no candidate exists (an empty candidate set +-- does NOT make every claim true — there is no +-- inhabited Case at all) + +module MetaManifold.Evidence.Decision where + +open import MetaManifold.Evidence.Prelude +open import MetaManifold.Evidence.Signed + +-- -------------------------------------------------------------------------- +-- The finite-case candidate set and claims over it +-- -------------------------------------------------------------------------- + +-- The evidence-refined preimage fibre for the finite model, as a type. +FCase : View → Nat → Nat → Bool → Set +FCase view r₀ b z = Σ World (λ w → (Obs view r₀ w) × (Adm b z w)) + +-- A claim holds when it holds of every admissible candidate's world. +FHolds : ∀ {p} (view : View) (r₀ b : Nat) (z : Bool) → + (World → Set p) → Set p +FHolds view r₀ b z P = (c : FCase view r₀ b z) → P (fst c) + +-- Presence: u ≠ 0, i.e. the u-offset is not the zero offset 6. +Present : World → Set +Present w = ¬ (fst w ≡ 6) + +-- Absence: u = 0. +Absent : World → Set +Absent w = fst w ≡ 6 + +-- A numeric query is identified when every admissible candidate agrees on it. +FIdentified : (view : View) (r₀ b : Nat) (z : Bool) → + (World → Nat) → Set +FIdentified view r₀ b z query = + Σ Nat (λ v → FHolds view r₀ b z (λ w → query w ≡ v)) + +-- Two admissible candidates that disagree on the query refute identification +-- (the finite-model shadow of different-candidates-refute-identification). +finitely-refute-identification : + ∀ (view : View) (r₀ b : Nat) (z : Bool) (query : World → Nat) + (x y : FCase view r₀ b z) → + ¬ (query (fst x) ≡ query (fst y)) → + ¬ (FIdentified view r₀ b z query) +finitely-refute-identification view r₀ b z query x y disagree (v , agrees) = + disagree (trans (agrees x) (sym (agrees y))) + +-- -------------------------------------------------------------------------- +-- Boolean any?-toolkit +-- -------------------------------------------------------------------------- + +not? : Bool → Bool +not? b = if b then false else true + +any? : ∀ {a} {A : Set a} (p : A → Bool) → List A → Bool +any? p [] = false +any? p (x ∷ xs) = (p x) or (any? p xs) + +contr-bool : (b : Bool) → (b ≡ true) → (b ≡ false) → ⊥ {lzero} +contr-bool true refl () +contr-bool false () refl + +true≢false→anything : ∀ {a} {A : Set a} → (true ≡ false) → A +true≢false→anything () + +any-true-tail : + ∀ {a} {A : Set a} (p : A → Bool) (x : A) (xs : List A) → + Σ A (λ y → (y ∈ xs) × ((p y) ≡ true)) → + Σ A (λ y → (y ∈ x ∷ xs) × ((p y) ≡ true)) +any-true-tail p x xs (y , m , pv) = y , inj₂ m , pv + +any-true : ∀ {a} {A : Set a} (p : A → Bool) (xs : List A) → + (any? p xs) ≡ true → Σ A (λ x → (x ∈ xs) × ((p x) ≡ true)) +any-true p [] () +any-true p (x ∷ xs) q with inspect (p x) +... | inspecting true peq = x , inj₁ refl , peq +... | inspecting false peq = + any-true-tail p x xs + (any-true p xs (subst (λ b → (b or any? p xs) ≡ true) peq q)) + +any-false : ∀ {a} {A : Set a} (p : A → Bool) (xs : List A) → + (any? p xs) ≡ false → (x : A) → x ∈ xs → (p x) ≡ false +any-false p [] q x () +any-false p (y ∷ xs) q x m with inspect (p y) +... | inspecting true peq = + true≢false→anything (subst (λ b → (b or any? p xs) ≡ false) peq q) +... | inspecting false peq with m +... | inj₁ eq = trans (cong p eq) peq +... | inj₂ m′ = + any-false p xs (subst (λ b → (b or any? p xs) ≡ false) peq q) x m′ + +-- -------------------------------------------------------------------------- +-- The decide computation (exactly what the server/UI compute) +-- -------------------------------------------------------------------------- + +data Verdict : Set where + entailed refuted unresolved inconsistent : Verdict + +is-zero : World → Bool +is-zero w = fst w == 6 + +is-nonzero : World → Bool +is-nonzero w = not? (is-zero w) + +has-zero? : List World → Bool +has-zero? cs = any? is-zero cs + +has-nonzero? : List World → Bool +has-nonzero? cs = any? is-nonzero cs + +verdict₂ : Bool → Bool → Verdict +verdict₂ false _ = entailed -- no zero-candidate: all present +verdict₂ true false = refuted -- only zero-candidates: all absent +verdict₂ true true = unresolved -- both kinds remain + +decide : List World → Verdict +decide [] = inconsistent +decide (w ∷ ws) = verdict₂ (has-zero? (w ∷ ws)) (has-nonzero? (w ∷ ws)) + +-- Full result record: what every endpoint returns for a residual case. +record Result : Set where + constructor mk-result + field + count : Nat + verdict : Verdict + identified-values : List Nat -- sorted unique u-offsets +open Result public + +result : View → Nat → Nat → Bool → Result +result view r₀ b z = + mk-result (length cs) (decide cs) (values cs) + where cs = candidates view r₀ b z + +-- -------------------------------------------------------------------------- +-- Bridging lemmas: boolean tests to propositions +-- -------------------------------------------------------------------------- + +zero-free→present : (w : World) → (is-zero w) ≡ false → Present w +zero-free→present w hz eq = contr-bool (fst w == 6) (≡-to-== eq) hz + +nonzero-step : (w : World) → (is-nonzero w) ≡ false → Inspect (is-zero w) → Absent w +nonzero-step w hn (inspecting true pz) = ==-to-≡ (fst w) 6 pz +nonzero-step w hn (inspecting false pz) = + ⊥-elim (contr-bool (not? (is-zero w)) + (subst (λ j → (not? j) ≡ true) (sym pz) refl) hn) + +nonzero-free→absent : (w : World) → (is-nonzero w) ≡ false → Absent w +nonzero-free→absent w hn = nonzero-step w hn (inspect (is-zero w)) + +-- Inversions of the decide computation. + +refuted≢entailed : verdict₂ true false ≡ entailed → ⊥ {lzero} +refuted≢entailed () + +unresolved≢entailed : verdict₂ true true ≡ entailed → ⊥ {lzero} +unresolved≢entailed () + +entailed≢refuted : ∀ j → verdict₂ false j ≡ refuted → ⊥ {lzero} +entailed≢refuted j () + +unresolved≢refuted : verdict₂ true true ≡ refuted → ⊥ {lzero} +unresolved≢refuted () + +entailed≢inconsistent : ∀ j → verdict₂ false j ≡ inconsistent → ⊥ {lzero} +entailed≢inconsistent j () + +refuted≢inconsistent : verdict₂ true false ≡ inconsistent → ⊥ {lzero} +refuted≢inconsistent () + +unresolved≢inconsistent : verdict₂ true true ≡ inconsistent → ⊥ {lzero} +unresolved≢inconsistent () + +decide-entailed⇒zero-free : ∀ cs → (decide cs ≡ entailed) → (has-zero? cs ≡ false) +decide-entailed⇒zero-free [] () +decide-entailed⇒zero-free (w ∷ ws) eq with inspect (has-zero? (w ∷ ws)) +... | inspecting false hz = hz +... | inspecting true hz = impossible hz eq + where + impossible : (has-zero? (w ∷ ws)) ≡ true → decide (w ∷ ws) ≡ entailed → + has-zero? (w ∷ ws) ≡ false + impossible hz′ eq′ with inspect (has-nonzero? (w ∷ ws)) + ... | inspecting false hn′ = + ⊥-elim (refuted≢entailed + (subst (λ j → verdict₂ true j ≡ entailed) hn′ + (subst (λ j → verdict₂ j (has-nonzero? (w ∷ ws)) ≡ entailed) hz′ eq′))) + ... | inspecting true hn′ = + ⊥-elim (unresolved≢entailed + (subst (λ j → verdict₂ true j ≡ entailed) hn′ + (subst (λ j → verdict₂ j (has-nonzero? (w ∷ ws)) ≡ entailed) hz′ eq′))) + +decide-refuted⇒nonzero-free : ∀ cs → (decide cs ≡ refuted) → (has-nonzero? cs ≡ false) +decide-refuted⇒nonzero-free [] () +decide-refuted⇒nonzero-free (w ∷ ws) eq with inspect (has-nonzero? (w ∷ ws)) +... | inspecting false hn = hn +... | inspecting true hn = impossible hn eq + where + impossible : (has-nonzero? (w ∷ ws)) ≡ true → decide (w ∷ ws) ≡ refuted → + has-nonzero? (w ∷ ws) ≡ false + impossible hn′ eq′ with inspect (has-zero? (w ∷ ws)) + ... | inspecting false hz′ = + ⊥-elim (entailed≢refuted (has-nonzero? (w ∷ ws)) + (subst (λ j → verdict₂ false j ≡ refuted) hn′ + (subst (λ j → verdict₂ j (has-nonzero? (w ∷ ws)) ≡ refuted) hz′ eq′))) + ... | inspecting true hz′ = + ⊥-elim (unresolved≢refuted + (subst (λ j → verdict₂ true j ≡ refuted) hn′ + (subst (λ j → verdict₂ j (has-nonzero? (w ∷ ws)) ≡ refuted) hz′ eq′))) + +unresolved⇒entailed-impossible : ∀ j → verdict₂ false j ≡ unresolved → ⊥ {lzero} +unresolved⇒entailed-impossible j () + +unresolved⇒refuted-impossible : verdict₂ true false ≡ unresolved → ⊥ {lzero} +unresolved⇒refuted-impossible () + +decide-unresolved⇒both : ∀ cs → (decide cs ≡ unresolved) → + (has-zero? cs ≡ true) × (has-nonzero? cs ≡ true) +decide-unresolved⇒both [] () +decide-unresolved⇒both (w ∷ ws) eq + with inspect (has-zero? (w ∷ ws)) | inspect (has-nonzero? (w ∷ ws)) +... | inspecting false hz | _ = + ⊥-elim (unresolved⇒entailed-impossible (has-nonzero? (w ∷ ws)) + (subst (λ j → verdict₂ j (has-nonzero? (w ∷ ws)) ≡ unresolved) hz eq)) +... | inspecting true hz′ | inspecting false hn = + ⊥-elim (unresolved⇒refuted-impossible + (subst (λ j → verdict₂ true j ≡ unresolved) hn + (subst (λ j → verdict₂ j (has-nonzero? (w ∷ ws)) ≡ unresolved) hz′ eq))) +... | inspecting true hz | inspecting true hn = hz , hn + +decide-inconsistent⇒empty : ∀ cs → (decide cs ≡ inconsistent) → (w : World) → ¬ (w ∈ cs) +decide-inconsistent⇒empty [] eq w () +decide-inconsistent⇒empty (y ∷ ws) eq w m + with inspect (has-zero? (y ∷ ws)) | inspect (has-nonzero? (y ∷ ws)) +... | inspecting false hz | _ = + ⊥-elim (entailed≢inconsistent (has-nonzero? (y ∷ ws)) + (subst (λ j → verdict₂ j (has-nonzero? (y ∷ ws)) ≡ inconsistent) hz eq)) +... | inspecting true hz′ | inspecting false hn = + ⊥-elim (refuted≢inconsistent + (subst (λ j → verdict₂ true j ≡ inconsistent) hn + (subst (λ j → verdict₂ j (has-nonzero? (y ∷ ws)) ≡ inconsistent) hz′ eq))) +... | inspecting true hz′ | inspecting true hn′ = + ⊥-elim (unresolved≢inconsistent + (subst (λ j → verdict₂ true j ≡ inconsistent) hn′ + (subst (λ j → verdict₂ j (has-nonzero? (y ∷ ws)) ≡ inconsistent) hz′ eq))) + +-- -------------------------------------------------------------------------- +-- Main correctness theorems +-- -------------------------------------------------------------------------- + +-- entailed ⇒ every admissible candidate is present. +entailed⇒holds : ∀ view r₀ b z → b ≤ 6 → + (decide (candidates view r₀ b z) ≡ entailed) → + FHolds view r₀ b z Present +entailed⇒holds view r₀ b z b≤6 v✓ c = + zero-free→present w hz + where + w = fst c + w∈ = candidates-complete view r₀ b z w b≤6 (snd c) + hz = any-false is-zero (candidates view r₀ b z) + (decide-entailed⇒zero-free (candidates view r₀ b z) v✓) w w∈ + +-- refuted ⇒ every admissible candidate is absent. +refuted⇒holds-absent : ∀ view r₀ b z → b ≤ 6 → + (decide (candidates view r₀ b z) ≡ refuted) → + FHolds view r₀ b z Absent +refuted⇒holds-absent view r₀ b z b≤6 v✓ c = + nonzero-free→absent w hn + where + w = fst c + w∈ = candidates-complete view r₀ b z w b≤6 (snd c) + hn = any-false is-nonzero (candidates view r₀ b z) + (decide-refuted⇒nonzero-free (candidates view r₀ b z) v✓) w w∈ + +-- unresolved ⇒ neither presence nor absence is warranted. +unresolved⇒¬holds : ∀ view r₀ b z → b ≤ 6 → + (decide (candidates view r₀ b z) ≡ unresolved) → + (¬ (FHolds view r₀ b z Present)) × (¬ (FHolds view r₀ b z Absent)) +unresolved⇒¬holds view r₀ b z b≤6 v✓ = + (λ holds → refutes-absent holds) , + (λ holds → refutes-present holds) + where + cs = candidates view r₀ b z + hz = fst (decide-unresolved⇒both cs v✓) + hn = snd (decide-unresolved⇒both cs v✓) + + zero-w = fst (any-true is-zero cs hz) + zero-m = fst (snd (any-true is-zero cs hz)) + zero-p = snd (snd (any-true is-zero cs hz)) + zero-cand : FCase view r₀ b z + zero-cand = zero-w , candidates-sound view r₀ b z zero-w zero-m + zero-absent : Absent (fst zero-cand) + zero-absent = ==-to-≡ (fst zero-w) 6 zero-p + + nonzero-w = fst (any-true is-nonzero cs hn) + nonzero-m = fst (snd (any-true is-nonzero cs hn)) + nonzero-p = snd (snd (any-true is-nonzero cs hn)) + nonzero-cand : FCase view r₀ b z + nonzero-cand = nonzero-w , candidates-sound view r₀ b z nonzero-w nonzero-m + nonzero-present : Present (fst nonzero-cand) + nonzero-present = zero-free→present nonzero-w + (contr-opposite (is-zero nonzero-w) nonzero-p) + where + contr-opposite : (b : Bool) → (not? b ≡ true) → (b ≡ false) + contr-opposite true () + contr-opposite false _ = refl + + refutes-absent : FHolds view r₀ b z Present → ⊥ + refutes-absent holds = holds zero-cand zero-absent + + refutes-present : FHolds view r₀ b z Absent → ⊥ + refutes-present holds = nonzero-present (holds nonzero-cand) + +-- inconsistent ⇒ NO candidate exists: an empty candidate set does not make +-- every claim true — there is no inhabited case at all. +inconsistent⇒no-candidate : ∀ view r₀ b z → b ≤ 6 → + (decide (candidates view r₀ b z) ≡ inconsistent) → + ¬ (FCase view r₀ b z) +inconsistent⇒no-candidate view r₀ b z b≤6 v✓ c = + decide-inconsistent⇒empty (candidates view r₀ b z) v✓ (fst c) + (candidates-complete view r₀ b z (fst c) b≤6 (snd c)) + +-- -------------------------------------------------------------------------- +-- The worked examples of the reference explorer, as computed and proved +-- terms. r = 2 means offset 8; the noise bound |n| ≤ b is a Nat. +-- -------------------------------------------------------------------------- + +-- Preset 2 "Present, value unknown": r = 2, |n| ≤ 1. +present-case : candidates exact 8 1 false ≡ (7 , 7) ∷ (8 , 6) ∷ (9 , 5) ∷ [] +present-case = refl + +present-entailed : decide (candidates exact 8 1 false) ≡ entailed +present-entailed = refl + +present-values : values (candidates exact 8 1 false) ≡ 7 ∷ 8 ∷ 9 ∷ [] +present-values = refl + +-- The witnesses, as members of the finite case. +seven-seven : FCase exact 8 1 false +seven-seven = (7 , 7) , refl , (≤7-12 , ≤1-1 , tt) + where + ≤7-12 : 7 ≤ 12 + ≤7-12 = s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))) + ≤1-1 : dist 7 6 ≤ 1 + ≤1-1 = s≤s z≤n + +eight-six : FCase exact 8 1 false +eight-six = (8 , 6) , refl , (≤8-12 , ≤0-1 , tt) + where + ≤8-12 : 8 ≤ 12 + ≤8-12 = s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))))) + ≤0-1 : dist 6 6 ≤ 1 + ≤0-1 = z≤n + +seven≢eight : ¬ (7 ≡ 8) +seven≢eight () + +-- Presence without identification: the canonical residual-evidence example. +present-without-identification : ¬ (FIdentified exact 8 1 false fst) +present-without-identification = + finitely-refute-identification exact 8 1 false fst seven-seven eight-six seven≢eight + +present-holds : FHolds exact 8 1 false Present +present-holds = entailed⇒holds exact 8 1 false ≤6 present-entailed + where + ≤6 : 1 ≤ 6 + ≤6 = s≤s z≤n + +-- Preset 1 "Residual alone": r = 2, unbounded noise. +ambiguous-unresolved : decide (candidates exact 8 6 false) ≡ unresolved +ambiguous-unresolved = refl + +-- Preset 3 "Value identified": r = 2, no noise. +exact-entailed : decide (candidates exact 8 0 false) ≡ entailed +exact-entailed = refl + +exact-identified-value : values (candidates exact 8 0 false) ≡ 8 ∷ [] +exact-identified-value = refl + +-- Preset 4 "Cancellation": r = 0, unbounded noise. +cancellation-unresolved : decide (candidates exact 6 6 false) ≡ unresolved +cancellation-unresolved = refl + +-- Preset 5 "Conflicting assumptions": r = 2, |n| ≤ 1, u = 0 — no candidate +-- exists, and no claim is issued. +conflict-inconsistent : decide (candidates exact 8 1 true) ≡ inconsistent +conflict-inconsistent = refl + +conflict-no-candidate : ¬ (FCase exact 8 1 true) +conflict-no-candidate = + inconsistent⇒no-candidate exact 8 1 true ≤6 conflict-inconsistent + where + ≤6 : 1 ≤ 6 + ≤6 = s≤s z≤n diff --git a/proofs/agda/MetaManifold/Evidence/Echo.agda b/proofs/agda/MetaManifold/Evidence/Echo.agda new file mode 100644 index 0000000..912ce64 --- /dev/null +++ b/proofs/agda/MetaManifold/Evidence/Echo.agda @@ -0,0 +1,83 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: AGPL-3.0-only +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Echo types — proof-relevant fibres as structured-loss witnesses, following +-- hyperpolymath/echo-types (MPL-2.0). +-- +-- Echo f y := Σ (x : A) , (f x ≡ y) +-- +-- In MetaManifold: f is the observation function (sequencing + denoising), +-- A the possible true worlds, B the observed table. The fibre over an +-- observed value is exactly "every true world compatible with the +-- observation, with its proof". `avec_fibre` records that this fibre is +-- inhabited; `sans_fibre` that it is not (the artefact retains no origin +-- structure). The total-space factorisation below is the standard fact that +-- nothing is gained or lost by grouping witnesses fibre-wise: it is the +-- licence for the server to store rows as (observed, witnesses) pairs. + +module MetaManifold.Evidence.Echo where + +open import MetaManifold.Evidence.Prelude +open import MetaManifold.Evidence.Residual + +Echo : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → B → Set (a ⊔ b) +Echo f y = Σ _ (λ x → f x ≡ y) + +-- An artefact over y carries semantic fibre exactly when its echo fibre is +-- inhabited. This mirrors Julia's avec_fibre(fiber) = !isempty(fiber.witnesses). +data AvecFibre {a b} {A : Set a} {B : Set b} (f : A → B) (y : B) : Set (a ⊔ b) where + carries : (x : A) (p : f x ≡ y) → AvecFibre f y + +sans-fibre : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (y : B) → Set (a ⊔ b) +sans-fibre {A = A} f y = (x : A) → ¬ (f x ≡ y) +-- (kept pointful so it reads as "no witness exists"; equivalent to ¬ Echo) + +sans-fibre-no-witness : + ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B} → + sans-fibre f y → (x : A) → ¬ (f x ≡ y) +sans-fibre-no-witness h x p = h x p + +-- Echo fibres are exactly Candidates with trivial (always-true) evidence. +Echo-as-Candidate : + ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B} → + Echo f y → Candidate f y (λ _ → ⊤) +Echo-as-Candidate (x , p) = x , p , tt + +Candidate-as-Echo : + ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B} → + Candidate f y (λ _ → ⊤) → Echo f y +Candidate-as-Echo (x , p , _) = x , p + +-- Total space of fibres: pairing each input with its fibre over its image. +Total : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Set (a ⊔ b) +Total {A = A} {B = B} f = Σ B (Echo f) + +encode : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (x : A) → Total f +encode f x = f x , x , refl + +-- The left leg of the factorisation is an equivalence (HoTT Book §4.8 +-- restated in Echo vocabulary): projecting a fibre down to its witness +-- recovers the input, and every point of the total space is the encoding of +-- its own witness. Both directions hold by eta-for-Sigma and J; no funext. +fib⁻¹ : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → Total f → A +fib⁻¹ f (_ , x , _) = x + +encode-fib⁻¹ : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (x : A) → + fib⁻¹ f (encode f x) ≡ x +encode-fib⁻¹ f x = refl + +fib⁻¹-encode : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (t : Total f) → + encode f (fib⁻¹ f t) ≡ t +fib⁻¹-encode f (y , x , p) = J (λ y′ q → encode f x ≡ (y′ , x , q)) refl p + +-- Residue: what the observation could not distinguish, made first-class. +-- The cloud-size heuristic in the UI (log(1 + count)) is a *presentation* +-- choice over this count; the fibre itself is the semantics. +fibre-count : ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B} → + List A → Nat +fibre-count xs = fibre-count′ xs + where + fibre-count′ : ∀ {a} {A : Set a} → List A → Nat + fibre-count′ [] = zero + fibre-count′ (_ ∷ xs) = suc (fibre-count′ xs) diff --git a/proofs/agda/MetaManifold/Evidence/Prelude.agda b/proofs/agda/MetaManifold/Evidence/Prelude.agda new file mode 100644 index 0000000..b2dc33e --- /dev/null +++ b/proofs/agda/MetaManifold/Evidence/Prelude.agda @@ -0,0 +1,142 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: AGPL-3.0-only +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Tiny standard-library-free prelude, in the style of +-- hyperpolymath/residual-evidence-types (MPL-2.0). Depending only on +-- Agda.Builtin modules keeps this library typecheckable by a bare Agda +-- install with no stdlib setup, which is how CI checks it. + +module MetaManifold.Evidence.Prelude where + +open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) public +open import Agda.Builtin.Equality using (_≡_; refl) public +open import Agda.Builtin.Sigma using (Σ; _,_; fst; snd) public +open import Agda.Builtin.Nat using (Nat; zero; suc; _+_; _*_; _==_; _<_) public + +-- Truncated subtraction, defined here rather than imported: the builtin +-- primitive only reduces when BOTH arguments are constructor-headed, while +-- this one reduces as soon as the first is, which the distance proofs need. +infixl 6 _∸_ +_∸_ : Nat → Nat → Nat +zero ∸ _ = zero +suc m ∸ zero = suc m +suc m ∸ suc n = m ∸ n +open import Agda.Builtin.Bool using (Bool; true; false) public +open import Agda.Builtin.Unit using (⊤; tt) public +open import Agda.Builtin.List using (List; []; _∷_) public + +-- Empty type and negation (level-polymorphic so it can appear in +-- level-polymorphic membership). +data ⊥ {a} : Set a where + +infix 3 ¬_ +¬_ : ∀ {a} → Set a → Set a +¬_ {a} A = A → ⊥ {a} + +⊥-elim : ∀ {a b} {A : Set b} → ⊥ {a} → A +⊥-elim () + +-- Products as nested Sigmas. +infixr 4 _×_ +_×_ : ∀ {a b} → Set a → Set b → Set (a ⊔ b) +A × B = Σ A (λ _ → B) + +-- Equality toolkit (intensional, no funext assumed anywhere). +sym : ∀ {a} {A : Set a} {x y : A} → x ≡ y → y ≡ x +sym refl = refl + +trans : ∀ {a} {A : Set a} {x y z : A} → x ≡ y → y ≡ z → x ≡ z +trans refl q = q + +cong : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y +cong f refl = refl + +subst : ∀ {a p} {A : Set a} (P : A → Set p) {x y : A} → x ≡ y → P x → P y +subst P refl p = p + +J : ∀ {a p} {A : Set a} {x : A} (P : (y : A) → x ≡ y → Set p) → + P x refl → {y : A} (eq : x ≡ y) → P y eq +J P p refl = p + +-- Booleans as propositions. +T : Bool → Set +T true = ⊤ +T false = ⊥ + +infixr 5 _and_ +_and_ : Bool → Bool → Bool +true and x = x +false and _ = false + +-- Natural-number order (from residual-evidence-types' prelude). +infix 4 _≤_ +data _≤_ : Nat → Nat → Set where + z≤n : ∀ {n} → zero ≤ n + s≤s : ∀ {m n} → m ≤ n → suc m ≤ suc n + +≤-refl : ∀ {n} → n ≤ n +≤-refl {zero} = z≤n +≤-refl {suc n} = s≤s ≤-refl + +≤-trans : ∀ {a b c} → a ≤ b → b ≤ c → a ≤ c +≤-trans z≤n _ = z≤n +≤-trans (s≤s p) (s≤s q) = s≤s (≤-trans p q) + +≤-suc : ∀ {m n} → m ≤ n → m ≤ suc n +≤-suc z≤n = z≤n +≤-suc (s≤s p) = s≤s (≤-suc p) + +-- Trichotomy of natural numbers, used for the sign view of the finite +-- residual model. +data Sign : Set where + neg zer pos : Sign + +signOf : (a mid : Nat) → Sign +signOf a mid with a < mid +... | true = neg +... | false with a == mid +... | true = zer +... | false = pos + +-- |a − b| on naturals (both truncated subtractions; exactly one is nonzero). +dist : (a b : Nat) → Nat +dist a b = (a ∸ b) + (b ∸ a) + +-- Absolute value of a signed offset value v = off − 6, as a natural. +absOff : (off : Nat) → Nat +absOff off = dist off 6 + +-- Minimal list toolkit. +infixr 5 _++_ +_++_ : ∀ {a} {A : Set a} → List A → List A → List A +[] ++ ys = ys +(x ∷ xs) ++ ys = x ∷ (xs ++ ys) + +map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List A → List B +map f [] = [] +map f (x ∷ xs) = f x ∷ map f xs + +concatMap : ∀ {a b} {A : Set a} {B : Set b} → (A → List B) → List A → List B +concatMap f [] = [] +concatMap f (x ∷ xs) = f x ++ concatMap f xs + +if_then_else_ : ∀ {a} {A : Set a} → Bool → A → A → A +if true then x else _ = x +if false then _ else y = y + +filter : ∀ {a} {A : Set a} → (A → Bool) → List A → List A +filter p [] = [] +filter p (x ∷ xs) = if p x then x ∷ filter p xs else filter p xs + +-- Coproducts. +data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where + inj₁ : A → A ⊎ B + inj₂ : B → A ⊎ B + +-- List membership, as a recursive proposition (not an indexed datatype): +-- index-free, so it never trips the --without-K unification restrictions. +infix 4 _∈_ +_∈_ : ∀ {a} {A : Set a} → A → List A → Set a +x ∈ [] = ⊥ +x ∈ (y ∷ xs) = (x ≡ y) ⊎ (x ∈ xs) diff --git a/proofs/agda/MetaManifold/Evidence/Residual.agda b/proofs/agda/MetaManifold/Evidence/Residual.agda new file mode 100644 index 0000000..6731f98 --- /dev/null +++ b/proofs/agda/MetaManifold/Evidence/Residual.agda @@ -0,0 +1,122 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: AGPL-3.0-only +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Residual evidence — the ordinary evidence-refined preimage fibre, following +-- hyperpolymath/residual-evidence-types (MPL-2.0), restated here so the +-- MetaManifold Evidence Mode has its semantics in one self-contained library. +-- +-- Candidate observe r E = Σ World (observe w ≡ r × E w) +-- +-- A claim warranted by a case must hold for EVERY admissible candidate, never +-- merely for a chosen inhabitant. Applying it to the actual world needs both +-- premises (observation match and evidence). Nothing here is MetaManifold- or +-- microbiome-specific: the finite signed model instantiating it lives in +-- Signed.agda, and the decision procedures the server runs are proved correct +-- against these definitions in Decision.agda. + +module MetaManifold.Evidence.Residual where + +open import MetaManifold.Evidence.Prelude + +-- The evidence-refined preimage fibre. +Candidate : ∀ {w o e} {W : Set w} {O : Set o} → + (W → O) → O → (W → Set e) → Set (w ⊔ o ⊔ e) +Candidate {W = W} observe r E = Σ W (λ world → (observe world ≡ r) × E world) + +-- A case must carry a witness of consistency (inhabitedness). Claims still +-- quantify over ALL candidates, not merely this chosen inhabitant. +record Case {w o e} {W : Set w} {O : Set o} + (observe : W → O) (r : O) (E : W → Set e) : Set (w ⊔ o ⊔ e) where + constructor inhabited + field + witness : Candidate observe r E + +-- A claim holds for a case when it holds of every admissible candidate's world. +Holds : ∀ {w o e p} {W : Set w} {O : Set o} + {observe : W → O} {r} {E : W → Set e} → + Case observe r E → (W → Set p) → Set (w ⊔ o ⊔ e ⊔ p) +Holds {observe = observe} {r} {E} c P = (x : Candidate observe r E) → P (fst x) + +-- A query is identified when every admissible candidate agrees on its value. +Identified : ∀ {w o e q} {W : Set w} {O : Set o} {Q : Set q} + {observe : W → O} {r} {E : W → Set e} → + Case observe r E → (W → Q) → Set (w ⊔ o ⊔ e ⊔ q) +Identified {Q = Q} c query = Σ Q (λ value → Holds c (λ world → query world ≡ value)) + +-- Applying a conditional claim to an actual world needs BOTH premises. This +-- is the honesty boundary of the whole Evidence Mode: a warranted claim about +-- candidate worlds says nothing about reality until the actual world is shown +-- to be one of those candidates. +actual-world-sound : ∀ {w o e p} {W : Set w} {O : Set o} + {observe : W → O} {r} {E : W → Set e} {P : W → Set p} + (c : Case observe r E) → Holds c P → + (actual : W) → observe actual ≡ r → E actual → P actual +actual-world-sound c claim actual observed evidence = claim (actual , observed , evidence) + +-- Two admissible worlds that disagree on a query refute identification. +different-candidates-refute-identification : + ∀ {w o e q} {W : Set w} {O : Set o} {Q : Set q} + {observe : W → O} {r} {E : W → Set e} + (c : Case observe r E) (query : W → Q) + (x y : Candidate observe r E) → + ¬ (query (fst x) ≡ query (fst y)) → ¬ Identified c query +different-candidates-refute-identification c query x y disagree (value , agrees) = + ⊥-elim (disagree (trans (agrees x) (sym (agrees y)))) + +-- Evidence strengthening alone does not promise a consistent new case, but it +-- does transport claims from the weaker case to the stronger one. +refine-candidate : ∀ {w o e f} {W : Set w} {O : Set o} + {observe : W → O} {r} {E : W → Set e} {F : W → Set f} → + ((world : W) → F world → E world) → Candidate observe r F → Candidate observe r E +refine-candidate entails (world , observed , evidence) = world , observed , entails world evidence + +refine-claim : ∀ {w o e f p} {W : Set w} {O : Set o} + {observe : W → O} {r} {E : W → Set e} {F : W → Set f} {P : W → Set p} → + (old : Case observe r E) (new : Case observe r F) → + ((world : W) → F world → E world) → Holds old P → Holds new P +refine-claim old new entails claim x = claim (refine-candidate entails x) + +-- Claims do NOT transfer from a stronger case to a weaker one for free +-- (dropping evidence constraints can invalidate a claim). Concrete +-- countermodel: two worlds, observation constant, strong evidence admits only +-- world `true`, weak evidence admits both. "w ≡ true" holds for the strong +-- case and fails for the weak one. This is the kernel anti-cherry-picking +-- fact: keeping a claim while discarding the evidence that supported it is +-- unsound, so the avec_fibre editor must never let a *label* edit bypass the +-- candidate set (see EvidenceMode.agda for the row-level statement). +module NoFreeWeakening where + obs-const : Bool → ⊤ + obs-const w = tt + + strong-E : Bool → Set + strong-E w = w ≡ true + + weak-E : Bool → Set + weak-E w = ⊤ + + strong-case : Case obs-const tt strong-E + strong-case = inhabited (true , refl , refl) + + weak-case : Case obs-const tt weak-E + weak-case = inhabited (true , refl , tt) + + strong-holds : Holds strong-case (λ w → w ≡ true) + strong-holds x = snd (snd x) + +no-free-weakening : + ¬ ( (P : Bool → Set) → + Holds NoFreeWeakening.strong-case P → + Holds NoFreeWeakening.weak-case P ) +no-free-weakening transfer = ⊥-elim (false≢true impossible-eq) + where + open NoFreeWeakening + + false≢true : ¬ (false ≡ true) + false≢true () + + weak-claim : Holds weak-case (λ w → w ≡ true) + weak-claim = transfer (λ w → w ≡ true) strong-holds + + impossible-eq : false ≡ true + impossible-eq = weak-claim (false , refl , tt) diff --git a/proofs/agda/MetaManifold/Evidence/Signed.agda b/proofs/agda/MetaManifold/Evidence/Signed.agda new file mode 100644 index 0000000..e77c3e1 --- /dev/null +++ b/proofs/agda/MetaManifold/Evidence/Signed.agda @@ -0,0 +1,433 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: AGPL-3.0-only +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- The signed finite residual model, 'signed-integer-v1' — the model used by +-- the reference explorer in hyperpolymath/residual-evidence-types, by the +-- MetaManifold server routes (issue #7), and pinned by the golden vectors in +-- proofs/vectors/evidence_vectors.json. +-- +-- world = (u , n) integers in [-6, 6], represented as OFFSETS: +-- a value v is stored as v + 6, so an offset is a Nat in [0, 12] +-- and "value zero" is offset 6. Offsets keep every observation +-- predicate decidable on Nat, which is what makes the model +-- executable inside Agda itself. +-- exact view : u + n = r (offsets: u₀ + n₀ = r₀ + 6) +-- sign view : sgn(u + n) = sgn(r) (offsets: signOf (u₀+n₀) 12 = signOf r₀ 6) +-- magnitude view : |u + n| = |r| (offsets: dist (u₀+n₀) 12 = dist r₀ 6) +-- admissibility : u in domain, |n| ≤ b, optionally u = 0. +-- +-- The correspondence "offset formula = signed view" is pinned across all 546 +-- golden-vector cases by the Julia and bun test suites against the reference +-- JavaScript; Decision.agda then proves the decision procedures correct +-- against these predicates, so the whole chain from server code to the +-- Candidate semantics of Residual.agda is validated. + +module MetaManifold.Evidence.Signed where + +open import MetaManifold.Evidence.Prelude + +-- -------------------------------------------------------------------------- +-- Model constants and shapes +-- -------------------------------------------------------------------------- + +LIMIT : Nat +LIMIT = 6 + +GRID : Nat +GRID = 12 -- 2 * LIMIT; offsets live in [0, GRID] + +World : Set +World = Nat × Nat -- (u-offset , n-offset) + +data View : Set where + exact sign magnitude : View + +-- -------------------------------------------------------------------------- +-- Decidable comparison toolkit on Nat +-- -------------------------------------------------------------------------- + +infix 4 _≤ᵇ_ +_≤ᵇ_ : Nat → Nat → Bool +zero ≤ᵇ _ = true +suc m ≤ᵇ zero = false +suc m ≤ᵇ suc n = m ≤ᵇ n + +≤ᵇ-to-≤ : ∀ m n → (m ≤ᵇ n) ≡ true → m ≤ n +≤ᵇ-to-≤ zero _ _ = z≤n +≤ᵇ-to-≤ (suc m) zero () +≤ᵇ-to-≤ (suc m) (suc n) p = s≤s (≤ᵇ-to-≤ m n p) + +≤-to-≤ᵇ : ∀ {m n} → m ≤ n → (m ≤ᵇ n) ≡ true +≤-to-≤ᵇ z≤n = refl +≤-to-≤ᵇ (s≤s p) = ≤-to-≤ᵇ p + +suc-not-≤ᵇ : ∀ {m n} → m ≤ n → (suc n ≤ᵇ m) ≡ false +suc-not-≤ᵇ z≤n = refl +suc-not-≤ᵇ (s≤s p) = suc-not-≤ᵇ p + +==-to-≡ : ∀ m n → (m == n) ≡ true → m ≡ n +==-to-≡ zero zero _ = refl +==-to-≡ zero (suc n) () +==-to-≡ (suc m) zero () +==-to-≡ (suc m) (suc n) p = cong suc (==-to-≡ m n p) + +==-refl : ∀ m → (m == m) ≡ true +==-refl zero = refl +==-refl (suc m) = ==-refl m + +≡-to-== : ∀ {m n} → m ≡ n → (m == n) ≡ true +≡-to-== {m} refl = ==-refl m + +signEq : Sign → Sign → Bool +signEq neg neg = true +signEq neg _ = false +signEq zer zer = true +signEq zer _ = false +signEq pos pos = true +signEq pos _ = false + +signEq-refl : ∀ s → (signEq s s) ≡ true +signEq-refl neg = refl +signEq-refl zer = refl +signEq-refl pos = refl + +signEq-to-≡ : ∀ s t → (signEq s t) ≡ true → s ≡ t +signEq-to-≡ neg neg _ = refl +signEq-to-≡ zer zer _ = refl +signEq-to-≡ pos pos _ = refl + +-- Arithmetic: a few standard Nat facts. +plus-zero : ∀ n → n + 0 ≡ n +plus-zero zero = refl +plus-zero (suc n) = cong suc (plus-zero n) + +plus-suc : ∀ m n → m + suc n ≡ suc (m + n) +plus-suc zero n = refl +plus-suc (suc m) n = cong suc (plus-suc m n) + +≤antisym : ∀ {m n} → m ≤ n → n ≤ m → m ≡ n +≤antisym z≤n z≤n = refl +≤antisym (s≤s p) (s≤s q) = cong suc (≤antisym p q) + +≤-split : ∀ {m n} → m ≤ n → (m ≡ n) ⊎ (suc m ≤ n) +≤-split {n = zero} z≤n = inj₁ refl +≤-split {n = suc n} z≤n = inj₂ (s≤s z≤n) +≤-split (s≤s p) with ≤-split p +... | inj₁ q = inj₁ (cong suc q) +... | inj₂ r = inj₂ (s≤s r) + +≤-mono-+ : ∀ k {m n} → m ≤ n → k + m ≤ k + n +≤-mono-+ zero p = p +≤-mono-+ (suc k) p = s≤s (≤-mono-+ k p) + +-- x ≤ x + y, by induction (all sums reduce on constructor heads). +x≤x+y : ∀ x y → x ≤ x + y +x≤x+y zero y = z≤n +x≤x+y (suc x) y = s≤s (x≤x+y x y) + +-- a ≤ b + (a ∸ b), by induction with both subtraction arguments split. +a≤b+∸ : ∀ a b → a ≤ b + (a ∸ b) +a≤b+∸ zero b = z≤n +a≤b+∸ (suc a) zero = ≤-refl +a≤b+∸ (suc a) (suc b) = s≤s (a≤b+∸ a b) + +-- a ≤ b + |a − b| (distance bounds the value from above). +a≤mid+dist : ∀ a b → a ≤ b + dist a b +a≤mid+dist a b = ≤-trans (a≤b+∸ a b) (≤-mono-+ b (x≤x+y (a ∸ b) (b ∸ a))) + +-- If |n| ≤ b and b ≤ 6 then the noise offset stays inside the grid. +offset-in-grid : ∀ n₀ b → dist n₀ 6 ≤ b → b ≤ 6 → n₀ ≤ 12 +offset-in-grid n₀ b p b≤6 = + ≤-trans (≤-trans (a≤mid+dist n₀ 6) (≤-mono-+ 6 p)) (bound-6 b b≤6) + where + bound-6 : ∀ b → b ≤ 6 → 6 + b ≤ 12 + bound-6 zero _ = s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))) + bound-6 (suc b) (s≤s p) = s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s p)))))) + +-- -------------------------------------------------------------------------- +-- Observation and admissibility: specification (Set) and decision (Bool) +-- -------------------------------------------------------------------------- + +-- Observation match. r₀ is the residual's offset. +Obs : View → Nat → World → Set +Obs exact r₀ w = (fst w + snd w) ≡ (r₀ + 6) +Obs sign r₀ w = signOf (fst w + snd w) 12 ≡ signOf r₀ 6 +Obs magnitude r₀ w = dist (fst w + snd w) 12 ≡ dist r₀ 6 + +obs? : View → Nat → World → Bool +obs? exact r₀ w = (fst w + snd w) == (r₀ + 6) +obs? sign r₀ w = signEq (signOf (fst w + snd w) 12) (signOf r₀ 6) +obs? magnitude r₀ w = dist (fst w + snd w) 12 == dist r₀ 6 + +obs?-sound : ∀ view r₀ w → (obs? view r₀ w) ≡ true → Obs view r₀ w +obs?-sound exact r₀ w p = ==-to-≡ (fst w + snd w) (r₀ + 6) p +obs?-sound sign r₀ w p = signEq-to-≡ (signOf (fst w + snd w) 12) (signOf r₀ 6) p +obs?-sound magnitude r₀ w p = ==-to-≡ (dist (fst w + snd w) 12) (dist r₀ 6) p + +obs?-complete : ∀ {view r₀ w} → Obs view r₀ w → (obs? view r₀ w) ≡ true +obs?-complete {exact} {r₀} {w} p = + subst (λ j → ((fst w + snd w) == j) ≡ true) p (==-refl (fst w + snd w)) +obs?-complete {sign} {r₀} {w} p = + subst (λ j → signEq (signOf (fst w + snd w) 12) j ≡ true) p + (signEq-refl (signOf (fst w + snd w) 12)) +obs?-complete {magnitude} {r₀} {w} p = + subst (λ j → (dist (fst w + snd w) 12 == j) ≡ true) p + (==-refl (dist (fst w + snd w) 12)) + +-- Evidence / admissibility: domain bound on u, noise bound on n, optional +-- zero assumption on u. +Adm : Nat → Bool → World → Set +Adm b z w = (fst w ≤ GRID) × (dist (snd w) 6 ≤ b) × + (if z then (fst w ≡ 6) else ⊤) + +adm? : Nat → Bool → World → Bool +adm? b z w = (fst w ≤ᵇ GRID) and ((dist (snd w) 6 ≤ᵇ b) and + (if z then (fst w == 6) else true)) + +and-split : ∀ {x y} → (x and y) ≡ true → (x ≡ true) × (y ≡ true) +and-split {true} {y} p = refl , p +and-split {false} {y} () + +and-join : ∀ {x y} → (x ≡ true) → (y ≡ true) → (x and y) ≡ true +and-join {true} {y} _ q = q +and-join {false} {y} () q + +adm?-sound : ∀ b z w → (adm? b z w) ≡ true → Adm b z w +adm?-sound b z w p + with and-split {fst w ≤ᵇ GRID} + {(dist (snd w) 6 ≤ᵇ b) and (if z then (fst w == 6) else true)} p +... | (u≤ , rest) + with and-split {dist (snd w) 6 ≤ᵇ b} {if z then (fst w == 6) else true} rest +... | (nb , zc) = ≤ᵇ-to-≤ (fst w) GRID u≤ , ≤ᵇ-to-≤ (dist (snd w) 6) b nb , + zero-cond z zc + where + zero-cond : (z : Bool) → (if z then (fst w == 6) else true) ≡ true → + (if z then (fst w ≡ 6) else ⊤) + zero-cond true q = ==-to-≡ (fst w) 6 q + zero-cond false _ = tt + +adm?-complete : ∀ {b z w} → Adm b z w → (adm? b z w) ≡ true +adm?-complete {b} {z} {w} (u≤ , nb , zc) = + and-join (≤-to-≤ᵇ u≤) (and-join (≤-to-≤ᵇ nb) (zero-cond z zc)) + where + zero-cond : (z : Bool) → (if z then (fst w ≡ 6) else ⊤) → + (if z then (fst w == 6) else true) ≡ true + zero-cond true eq = ≡-to-== eq + zero-cond false _ = refl + +adm-domain : ∀ {b z w} → Adm b z w → fst w ≤ GRID +adm-domain (u≤ , _ , _) = u≤ + +adm-noise : ∀ {b z w} → Adm b z w → dist (snd w) 6 ≤ b +adm-noise (_ , nb , _) = nb + +-- -------------------------------------------------------------------------- +-- Enumeration of the full model domain, and the candidate list +-- -------------------------------------------------------------------------- + +-- ascend n lo = [lo, lo+1, …, lo+n] +ascend : Nat → Nat → List Nat +ascend zero lo = lo ∷ [] +ascend (suc n) lo = lo ∷ ascend n (suc lo) + +suc≰ : ∀ m → ¬ (suc m ≤ m) +suc≰ zero () +suc≰ (suc m) (s≤s p) = suc≰ m p + +ascend∈ : ∀ n lo k → lo ≤ k → k ≤ lo + n → k ∈ ascend n lo +ascend∈ zero lo k lo≤k k≤ with ≤-split lo≤k +... | inj₁ lo≡k = inj₁ (sym lo≡k) +... | inj₂ suclo≤k = ⊥-elim (suc≰ lo (subst (λ j → suc lo ≤ j) (sym (≤antisym lo≤k (k≤lo+0 k≤))) suclo≤k)) + where + k≤lo+0 : k ≤ lo + zero → k ≤ lo + k≤lo+0 kt = subst (λ j → k ≤ j) (plus-zero lo) kt +ascend∈ (suc n) lo k lo≤k k≤ with ≤-split lo≤k +... | inj₁ lo≡k = inj₁ (sym lo≡k) +... | inj₂ suclo≤k = inj₂ (ascend∈ n (suc lo) k suclo≤k (k≤suclo+n k≤)) + where + k≤suclo+n : k ≤ lo + suc n → k ≤ suc lo + n + k≤suclo+n kt = subst (λ j → k ≤ j) (plus-suc lo n) kt + +offsets : List Nat +offsets = ascend GRID 0 + +allWorlds : List World -- u-offset outer, n-offset inner +allWorlds = concatMap (λ u₀ → map (λ n₀ → u₀ , n₀) offsets) offsets + +-- The admissible-candidate filter, exactly the reference explorer's loop. +cand? : View → Nat → Nat → Bool → World → Bool +cand? view r₀ b z w = obs? view r₀ w and adm? b z w + +candidates : View → Nat → Nat → Bool → List World +candidates view r₀ b z = filter (cand? view r₀ b z) allWorlds + +-- -------------------------------------------------------------------------- +-- Membership lemmas +-- -------------------------------------------------------------------------- + +++∈-head : ∀ {a} {A : Set a} {b : A} {ys zs : List A} → b ∈ ys → b ∈ ys ++ zs +++∈-head {ys = []} () +++∈-head {ys = y ∷ ys} (inj₁ eq) = inj₁ eq +++∈-head {ys = y ∷ ys} (inj₂ m) = inj₂ (++∈-head m) + +++∈-tail : ∀ {a} {A : Set a} {b : A} {ys zs : List A} → b ∈ zs → b ∈ ys ++ zs +++∈-tail {ys = []} m = m +++∈-tail {ys = _ ∷ ys} m = inj₂ (++∈-tail {ys = ys} m) + +map∈ : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x : A} {xs : List A} → + x ∈ xs → f x ∈ map f xs +map∈ f {xs = []} () +map∈ f {xs = x ∷ xs} (inj₁ eq) = inj₁ (cong f eq) +map∈ f {xs = x ∷ xs} (inj₂ p) = inj₂ (map∈ f p) + +∈-cong : ∀ {a b} {A : Set a} {B : Set b} (f : A → List B) {x y : A} {b : B} → + x ≡ y → b ∈ f x → b ∈ f y +∈-cong f {b = b} eq q = subst (λ j → b ∈ f j) eq q + +concatMap∈ : ∀ {a b} {A : Set a} {B : Set b} (f : A → List B) {a : A} {b : B} + {xs : List A} → a ∈ xs → b ∈ f a → b ∈ concatMap f xs +concatMap∈ f {xs = []} () +concatMap∈ f {xs = x ∷ xs} (inj₁ eq) q = ++∈-head (∈-cong f eq q) +concatMap∈ f {xs = x ∷ xs} (inj₂ p) q = ++∈-tail {ys = f x} (concatMap∈ f p q) + +-- The inspect idiom: pattern-match a boolean expression's value while +-- keeping the equation as data (no with-abstraction refinement needed). +data Inspect {a} {A : Set a} (x : A) : Set a where + inspecting : (y : A) → x ≡ y → Inspect x + +inspect : ∀ {a} {A : Set a} (x : A) → Inspect x +inspect x = inspecting x refl + +filter-true : ∀ {a} {A : Set a} (p : A → Bool) (x : A) (xs : List A) → + (p x) ≡ true → filter p (x ∷ xs) ≡ (x ∷ filter p xs) +filter-true p x xs eq = cong (λ b → if b then x ∷ filter p xs else filter p xs) eq + +filter-false : ∀ {a} {A : Set a} (p : A → Bool) (x : A) (xs : List A) → + (p x) ≡ false → filter p (x ∷ xs) ≡ filter p xs +filter-false p x xs eq = cong (λ b → if b then x ∷ filter p xs else filter p xs) eq + +∈-subst : ∀ {a} {A : Set a} {x : A} {l₁ l₂ : List A} → l₁ ≡ l₂ → x ∈ l₁ → x ∈ l₂ +∈-subst {x = x} eq m = subst (λ l → x ∈ l) eq m + +-- Filter-membership soundness and completeness. The element is an explicit +-- argument throughout (with it implicit, Agda promotes it to a rigid pattern +-- variable inside these clauses and cannot unify it with the cons head); +-- dispatch is by direct Inspect pattern-matching, which — unlike +-- with-abstraction — leaves the other arguments' types untouched. + +mutual + + -- Filter-membership soundness and completeness. The element x and the list + -- head y are both explicit (implicit pattern variables get rigidified here + -- and stop unifying); dispatch is by direct Inspect pattern-matching, which + -- — unlike with-abstraction — leaves the other arguments' types untouched. + + filter∈-dispatch : ∀ {a} {A : Set a} (p : A → Bool) (x y : A) (xs : List A) → + Inspect (p y) → x ∈ filter p (y ∷ xs) → + (x ∈ y ∷ xs) × ((p x) ≡ true) + filter∈-dispatch p x y xs (inspecting true peq) m + with ∈-subst {x = x} (filter-true p y xs peq) m + ... | inj₁ eq = inj₁ eq , trans (cong p eq) peq + ... | inj₂ m′ with filter∈-sound p x xs m′ + ... | (in-tail , pv) = inj₂ in-tail , pv + filter∈-dispatch p x y xs (inspecting false peq) m + with filter∈-sound p x xs (∈-subst {x = x} (filter-false p y xs peq) m) + ... | (in-tail , pv) = inj₂ in-tail , pv + + filter∈-sound : ∀ {a} {A : Set a} (p : A → Bool) (x : A) (xs : List A) → + x ∈ filter p xs → (x ∈ xs) × ((p x) ≡ true) + filter∈-sound p x [] () + filter∈-sound p x (y ∷ xs) m = filter∈-dispatch p x y xs (inspect (p y)) m + + filter∈-complete-false : ∀ {a} {A : Set a} (p : A → Bool) (x y : A) (xs : List A) → + (p y) ≡ false → x ∈ y ∷ xs → (p x) ≡ true → + x ∈ filter p (y ∷ xs) + filter∈-complete-false p x y xs peq m pv with m + ... | inj₁ eq = contradiction eq pv peq + where + contradiction : x ≡ y → (p x) ≡ true → (p y) ≡ false → x ∈ filter p (y ∷ xs) + contradiction eq′ pv′ peq′ = + nope (trans (sym pv′) (trans (cong p eq′) peq′)) + where + nope : true ≡ false → x ∈ filter p (y ∷ xs) + nope () + ... | inj₂ m′ = + ∈-subst {x = x} (sym (filter-false p y xs peq)) (filter∈-complete p x xs m′ pv) + + filter∈-complete : ∀ {a} {A : Set a} (p : A → Bool) (x : A) (xs : List A) → + x ∈ xs → (p x) ≡ true → x ∈ filter p xs + filter∈-complete p x [] () _ + filter∈-complete p x (y ∷ xs) m pv with inspect (p y) + ... | inspecting true peq = + ∈-subst {x = x} (sym (filter-true p y xs peq)) (build m) + where + build : x ∈ y ∷ xs → x ∈ y ∷ filter p xs + build (inj₁ eq) = inj₁ eq + build (inj₂ m′) = inj₂ (filter∈-complete p x xs m′ pv) + ... | inspecting false peq = filter∈-complete-false p x y xs peq m pv + +-- Every world with in-grid offsets is enumerated. +allWorlds∈ : ∀ w → fst w ≤ GRID → snd w ≤ GRID → w ∈ allWorlds +allWorlds∈ (u₀ , n₀) u≤ n≤ = + concatMap∈ (λ a → map (λ b → a , b) offsets) + (ascend∈ GRID 0 u₀ z≤n u≤) + (map∈ (λ b → u₀ , b) (ascend∈ GRID 0 n₀ z≤n n≤)) + +-- -------------------------------------------------------------------------- +-- Soundness and completeness of the enumeration +-- -------------------------------------------------------------------------- + +-- Splitting the candidate test into its observation and admissibility halves. +cand-split : ∀ view r₀ b z w → (cand? view r₀ b z w) ≡ true → + ((obs? view r₀ w) ≡ true) × ((adm? b z w) ≡ true) +cand-split view r₀ b z w pv = and-split {obs? view r₀ w} {adm? b z w} pv + +-- Every listed candidate satisfies the specification. +candidates-sound : ∀ view r₀ b z w → w ∈ candidates view r₀ b z → + (Obs view r₀ w) × Adm b z w +candidates-sound view r₀ b z w m = + sound-step (filter∈-sound (cand? view r₀ b z) w allWorlds m) + where + sound-step : ((w ∈ allWorlds) × ((cand? view r₀ b z w) ≡ true)) → + (Obs view r₀ w) × Adm b z w + sound-step (in-list , pv) = + obs?-sound view r₀ w (fst (cand-split view r₀ b z w pv)) , + adm?-sound b z w (snd (cand-split view r₀ b z w pv)) + +-- Every world satisfying the specification is listed, provided the bound is +-- within the model's validated range (b ≤ 6), which keeps noise offsets +-- inside the enumerated grid. +candidates-complete : ∀ view r₀ b z w → b ≤ 6 → + (Obs view r₀ w) × Adm b z w → + w ∈ candidates view r₀ b z +candidates-complete view r₀ b z w b≤6 (o , a) = + filter∈-complete (cand? view r₀ b z) w (allWorlds) + (allWorlds∈ w (adm-domain {w = w} a) + (offset-in-grid (snd w) b (adm-noise {w = w} a) b≤6)) + (and-join (obs?-complete o) (adm?-complete {w = w} a)) + +-- -------------------------------------------------------------------------- +-- Length and sorted unique u-values (for the golden-vector checks) +-- -------------------------------------------------------------------------- + +length : ∀ {a} {A : Set a} → List A → Nat +length [] = zero +length (_ ∷ xs) = suc (length xs) + +infixr 5 _or_ +_or_ : Bool → Bool → Bool +true or _ = true +false or b = b + +insert : Nat → List Nat → List Nat +insert k [] = k ∷ [] +insert k (x ∷ xs) = if k == x then x ∷ xs else + (if k ≤ᵇ x then k ∷ x ∷ xs else (x ∷ insert k xs)) + +usort : List Nat → List Nat +usort [] = [] +usort (x ∷ xs) = insert x (usort xs) + +values : List World → List Nat -- sorted unique u-offsets +values ws = usort (map fst ws) diff --git a/proofs/agda/MetaManifold/Evidence/Warrant.agda b/proofs/agda/MetaManifold/Evidence/Warrant.agda new file mode 100644 index 0000000..53b35da --- /dev/null +++ b/proofs/agda/MetaManifold/Evidence/Warrant.agda @@ -0,0 +1,70 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- SPDX-License-Identifier: AGPL-3.0-only +-- +-- Warrant without soundness, following hyperpolymath/epistemic-types +-- (MPL-2.0): a warrant is proof-relevant but NOT automatically sound. Having +-- a receipt for A is a different proposition from A being true; conflating +-- the two is precisely the "scientific misuse: cherry-picking" risk named in +-- MetaManifold-WebUI issue #7. The Julia `Epistemic.Warrant` / +-- `Epistemic.SoundWarrant` pair and the `epi_status` ladder +-- (:SansFibre → :Belief → :Warranted → :Factive) are finite shadows of the +-- definitions and separation results in this module. + +module MetaManifold.Evidence.Warrant where + +open import MetaManifold.Evidence.Prelude + +-- A warrant for A at standpoint κ exposes only a type of evidence tokens. +-- There is deliberately no field `Evidence → A`: that would make every +-- warrant factive. +record Warrant {kℓ ℓ wℓ : Level} (K : Set kℓ) (κ : K) (A : Set ℓ) + : Set (kℓ ⊔ ℓ ⊔ lsuc wℓ) where + constructor mkWarrant + field + Evidence : Set wℓ + +-- Epi packages a warrant object with a token of it. Sigma-like, but the +-- evidence type is read from the warrant, so a forged token of the wrong +-- type cannot be smuggled in. +record Epi {kℓ ℓ wℓ : Level} (K : Set kℓ) (κ : K) (A : Set ℓ) + : Set (kℓ ⊔ ℓ ⊔ lsuc wℓ) where + constructor epi + field + warrant : Warrant {kℓ = kℓ} {ℓ = ℓ} {wℓ = wℓ} K κ A + evidence : Warrant.Evidence warrant + +-- Soundness is a SEPARATE assumption. Only after adding it can a token be +-- exchanged for the claim. +record SoundWarrant {kℓ ℓ wℓ : Level} (K : Set kℓ) (κ : K) (A : Set ℓ) + : Set (kℓ ⊔ ℓ ⊔ lsuc wℓ) where + constructor soundWarrant + field + warrant : Warrant {kℓ = kℓ} {ℓ = ℓ} {wℓ = wℓ} K κ A + sound : Warrant.Evidence warrant → A + +sound-epi : + {kℓ ℓ wℓ : Level} {K : Set kℓ} {κ : K} {A : Set ℓ} → + (sw : SoundWarrant {wℓ = wℓ} K κ A) → + Warrant.Evidence (SoundWarrant.warrant sw) → A +sound-epi sw token = SoundWarrant.sound sw token + +-- Separation: Epi κ A does not give A. A concrete countermodel — a +-- standpoint with trivial evidence for an uninhabited claim — shows that no +-- general extraction function can exist. Any code path that treats a +-- warrant token as truth (e.g. an avec_fibre edit applied without checking +-- the receipt) is refuted by this term. +epi-does-not-give : + ¬ ( (K : Set) (κ : K) (A : Set) (e : Epi {wℓ = lzero} K κ A) → A ) +epi-does-not-give extract = ⊥-elim (extract ⊤ tt ⊥ trivial-epi) + where + trivial-warrant : Warrant {wℓ = lzero} ⊤ tt ⊥ + trivial-warrant = mkWarrant ⊤ + + trivial-epi : Epi {wℓ = lzero} ⊤ tt ⊥ + trivial-epi = epi trivial-warrant tt + +-- Forged acceptance stays forged: trivial evidence tokens can never be +-- exchanged for an uninhabited claim, no matter how the warrant is packaged. +no-sound-function-from-trivial-evidence : ¬ (⊤ → ⊥ {lzero}) +no-sound-function-from-trivial-evidence f = f tt diff --git a/proofs/agda/README.md b/proofs/agda/README.md index d105ee0..7219ca1 100644 --- a/proofs/agda/README.md +++ b/proofs/agda/README.md @@ -5,7 +5,9 @@ SPDX-License-Identifier: CC-BY-SA-4.0 Machine-checked statements about MetaManifold's compositional transforms. Scope, layering, the theorem-to-test map and what is deliberately **not** -proved: [`docs/formal/verification-plan.md`](../../docs/formal/verification-plan.md). +proved: [`docs/formal/verification-plan.md`](../../docs/formal/verification-plan.md); +for the evidence library (issue #7): +[`docs/formal/evidence-verification.md`](../../docs/formal/evidence-verification.md). ```sh just proofs # or: scripts/check-proofs.sh @@ -13,6 +15,11 @@ just proofs # or: scripts/check-proofs.sh AGDA=/path/to/agda AGDA_STDLIB_LIB=/path/to/standard-library.agda-lib scripts/check-proofs.sh ``` +The `Evidence.*` modules are deliberately **stdlib-free** (only `Agda.Builtin.*`), so they +check under any Agda ≥ 2.6.4.3 even where the stdlib is unavailable; the rest of the +suite uses the stdlib. Golden vectors pinning the signed model across implementations: +[`proofs/vectors/evidence_vectors.json`](../vectors/evidence_vectors.json). + Toolchain: Agda 2.6.4.3, agda-stdlib 2.1 (the estate pin). Every module is `--safe --without-K`; there are no postulates. Assumptions that cannot be proved in exact arithmetic (`log` turns products into sums; `1/sqrt` exists) are record @@ -31,4 +38,9 @@ its type. | `ILR.Orthonormal` | normalised basis orthonormal (via `Normaliser`) | | `ILR.Comb` | comb tree under uniform weights = MetaManifold's Helmert default | | `ILR.Integer` | ℤ instance; positive weights ⇒ `Cancellable`; counterexample for signed weights; philr known answer | +| `Evidence.Residual` | abstract evidence semantics: `Candidate` fibres, `Case`, `Holds`, `Identified`; actual-world honesty; no-free-weakening countermodel (issue #7) | +| `Evidence.Echo` | fibre semantics for artefacts: `Echo` = preimage fibre, `AvecFibre`, `sans-fibre`, total-space factorisation | +| `Evidence.Warrant` | warrant tokens: `Warrant`/`Epi`/`SoundWarrant`; `epi-does-not-give` (a token is not truth) | +| `Evidence.Signed` | the signed finite model (`signed-integer-v1`) as offsets on ℕ; enumeration proved sound + complete | +| `Evidence.Decision` | presence/identification verdicts computed **and** proved correct; the five reference presets as computed, proved terms | | `reject/` | must **fail** to type-check, each for the reason in its `-- EXPECT:` line | diff --git a/proofs/agda/reject/IdentificationWithoutUniqueness.agda b/proofs/agda/reject/IdentificationWithoutUniqueness.agda new file mode 100644 index 0000000..03f3eaa --- /dev/null +++ b/proofs/agda/reject/IdentificationWithoutUniqueness.agda @@ -0,0 +1,15 @@ +-- SPDX-License-Identifier: AGPL-3.0-only +-- MUST FAIL: the "Present, value unknown" preset (r = 2, |n| ≤ 1, exact view) +-- admits three admissible candidates with three different u-offsets, so +-- presence is entailed but no value is identified — this is Decision.agda's +-- present-without-identification. A UI that reports one identified value +-- from a mere presence verdict is exactly this term, and it must not check. +-- EXPECT: fst \(fst c\) != 8 +module reject.IdentificationWithoutUniqueness where + +open import MetaManifold.Evidence.Prelude +open import MetaManifold.Evidence.Signed +open import MetaManifold.Evidence.Decision + +present-but-unidentified : FIdentified exact 8 1 false fst +present-but-unidentified = 8 , λ c → refl diff --git a/proofs/vectors/evidence_vectors.json b/proofs/vectors/evidence_vectors.json new file mode 100644 index 0000000..0a7cac9 --- /dev/null +++ b/proofs/vectors/evidence_vectors.json @@ -0,0 +1,13135 @@ +{ + "model": "signed-integer-v1", + "limit": 6, + "source": "hyperpolymath/residual-evidence-types residual-evidence-explorer.html", + "licence": "MPL-2.0", + "case_count": 546, + "presets": { + "ambiguous": { + "residual": 2, + "noise_bound": 6, + "assume_zero": false, + "view": "exact" + }, + "present": { + "residual": 2, + "noise_bound": 1, + "assume_zero": false, + "view": "exact" + }, + "exact": { + "residual": 2, + "noise_bound": 0, + "assume_zero": false, + "view": "exact" + }, + "cancel": { + "residual": 0, + "noise_bound": 6, + "assume_zero": false, + "view": "exact" + }, + "conflict": { + "residual": 2, + "noise_bound": 1, + "assume_zero": true, + "view": "exact" + } + }, + "cases": [ + { + "residual": -6, + "noise_bound": 0, + "view": "exact", + "assume_zero": false, + "candidate_count": 1, + "presence": "entailed", + "identified_values": [ + -6 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + } + ] + }, + { + "residual": -6, + "noise_bound": 0, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -6, + "noise_bound": 0, + "view": "sign", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -6, + "noise_bound": 0, + "view": "sign", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -6, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 2, + "presence": "entailed", + "identified_values": [ + -6, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": 6, + "n": 0 + } + ] + }, + { + "residual": -6, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -6, + "noise_bound": 1, + "view": "exact", + "assume_zero": false, + "candidate_count": 2, + "presence": "entailed", + "identified_values": [ + -6, + -5 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + } + ] + }, + { + "residual": -6, + "noise_bound": 1, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -6, + "noise_bound": 1, + "view": "sign", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0 + ], + "first_candidates": [ + { + "u": -6, + "n": -1 + }, + { + "u": -6, + "n": 0 + }, + { + "u": -6, + "n": 1 + } + ] + }, + { + "residual": -6, + "noise_bound": 1, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -6, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 4, + "presence": "entailed", + "identified_values": [ + -6, + -5, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": 5, + "n": 1 + } + ] + }, + { + "residual": -6, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -6, + "noise_bound": 2, + "view": "exact", + "assume_zero": false, + "candidate_count": 3, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": -4, + "n": -2 + } + ] + }, + { + "residual": -6, + "noise_bound": 2, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -6, + "noise_bound": 2, + "view": "sign", + "assume_zero": false, + "candidate_count": 30, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1 + ], + "first_candidates": [ + { + "u": -6, + "n": -2 + }, + { + "u": -6, + "n": -1 + }, + { + "u": -6, + "n": 0 + } + ] + }, + { + "residual": -6, + "noise_bound": 2, + "view": "sign", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -6, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": -4, + "n": -2 + } + ] + }, + { + "residual": -6, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -6, + "noise_bound": 3, + "view": "exact", + "assume_zero": false, + "candidate_count": 4, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": -4, + "n": -2 + } + ] + }, + { + "residual": -6, + "noise_bound": 3, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -6, + "noise_bound": 3, + "view": "sign", + "assume_zero": false, + "candidate_count": 42, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2 + ], + "first_candidates": [ + { + "u": -6, + "n": -3 + }, + { + "u": -6, + "n": -2 + }, + { + "u": -6, + "n": -1 + } + ] + }, + { + "residual": -6, + "noise_bound": 3, + "view": "sign", + "assume_zero": true, + "candidate_count": 3, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -6, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 8, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": -4, + "n": -2 + } + ] + }, + { + "residual": -6, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -6, + "noise_bound": 4, + "view": "exact", + "assume_zero": false, + "candidate_count": 5, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": -4, + "n": -2 + } + ] + }, + { + "residual": -6, + "noise_bound": 4, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -6, + "noise_bound": 4, + "view": "sign", + "assume_zero": false, + "candidate_count": 54, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -6, + "n": -4 + }, + { + "u": -6, + "n": -3 + }, + { + "u": -6, + "n": -2 + } + ] + }, + { + "residual": -6, + "noise_bound": 4, + "view": "sign", + "assume_zero": true, + "candidate_count": 4, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": -2 + } + ] + }, + { + "residual": -6, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 10, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": -4, + "n": -2 + } + ] + }, + { + "residual": -6, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -6, + "noise_bound": 5, + "view": "exact", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": -4, + "n": -2 + } + ] + }, + { + "residual": -6, + "noise_bound": 5, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -6, + "noise_bound": 5, + "view": "sign", + "assume_zero": false, + "candidate_count": 66, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -6, + "n": -5 + }, + { + "u": -6, + "n": -4 + }, + { + "u": -6, + "n": -3 + } + ] + }, + { + "residual": -6, + "noise_bound": 5, + "view": "sign", + "assume_zero": true, + "candidate_count": 5, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -5 + }, + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": -3 + } + ] + }, + { + "residual": -6, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 12, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": -4, + "n": -2 + } + ] + }, + { + "residual": -6, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -6, + "noise_bound": 6, + "view": "exact", + "assume_zero": false, + "candidate_count": 7, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": -4, + "n": -2 + } + ] + }, + { + "residual": -6, + "noise_bound": 6, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -6 + } + ] + }, + { + "residual": -6, + "noise_bound": 6, + "view": "sign", + "assume_zero": false, + "candidate_count": 78, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -6, + "n": -6 + }, + { + "u": -6, + "n": -5 + }, + { + "u": -6, + "n": -4 + } + ] + }, + { + "residual": -6, + "noise_bound": 6, + "view": "sign", + "assume_zero": true, + "candidate_count": 6, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -6 + }, + { + "u": 0, + "n": -5 + }, + { + "u": 0, + "n": -4 + } + ] + }, + { + "residual": -6, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 14, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": -4, + "n": -2 + } + ] + }, + { + "residual": -6, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -6 + }, + { + "u": 0, + "n": 6 + } + ] + }, + { + "residual": -5, + "noise_bound": 0, + "view": "exact", + "assume_zero": false, + "candidate_count": 1, + "presence": "entailed", + "identified_values": [ + -5 + ], + "first_candidates": [ + { + "u": -5, + "n": 0 + } + ] + }, + { + "residual": -5, + "noise_bound": 0, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -5, + "noise_bound": 0, + "view": "sign", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -5, + "noise_bound": 0, + "view": "sign", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -5, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 2, + "presence": "entailed", + "identified_values": [ + -5, + 5 + ], + "first_candidates": [ + { + "u": -5, + "n": 0 + }, + { + "u": 5, + "n": 0 + } + ] + }, + { + "residual": -5, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -5, + "noise_bound": 1, + "view": "exact", + "assume_zero": false, + "candidate_count": 3, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": -5, + "noise_bound": 1, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -5, + "noise_bound": 1, + "view": "sign", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0 + ], + "first_candidates": [ + { + "u": -6, + "n": -1 + }, + { + "u": -6, + "n": 0 + }, + { + "u": -6, + "n": 1 + } + ] + }, + { + "residual": -5, + "noise_bound": 1, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -5, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": -5, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -5, + "noise_bound": 2, + "view": "exact", + "assume_zero": false, + "candidate_count": 4, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": -5, + "noise_bound": 2, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -5, + "noise_bound": 2, + "view": "sign", + "assume_zero": false, + "candidate_count": 30, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1 + ], + "first_candidates": [ + { + "u": -6, + "n": -2 + }, + { + "u": -6, + "n": -1 + }, + { + "u": -6, + "n": 0 + } + ] + }, + { + "residual": -5, + "noise_bound": 2, + "view": "sign", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -5, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 8, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": -5, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -5, + "noise_bound": 3, + "view": "exact", + "assume_zero": false, + "candidate_count": 5, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": -5, + "noise_bound": 3, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -5, + "noise_bound": 3, + "view": "sign", + "assume_zero": false, + "candidate_count": 42, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2 + ], + "first_candidates": [ + { + "u": -6, + "n": -3 + }, + { + "u": -6, + "n": -2 + }, + { + "u": -6, + "n": -1 + } + ] + }, + { + "residual": -5, + "noise_bound": 3, + "view": "sign", + "assume_zero": true, + "candidate_count": 3, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -5, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 10, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": -5, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -5, + "noise_bound": 4, + "view": "exact", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": -5, + "noise_bound": 4, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -5, + "noise_bound": 4, + "view": "sign", + "assume_zero": false, + "candidate_count": 54, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -6, + "n": -4 + }, + { + "u": -6, + "n": -3 + }, + { + "u": -6, + "n": -2 + } + ] + }, + { + "residual": -5, + "noise_bound": 4, + "view": "sign", + "assume_zero": true, + "candidate_count": 4, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": -2 + } + ] + }, + { + "residual": -5, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 12, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": -5, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -5, + "noise_bound": 5, + "view": "exact", + "assume_zero": false, + "candidate_count": 7, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": -5, + "noise_bound": 5, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -5 + } + ] + }, + { + "residual": -5, + "noise_bound": 5, + "view": "sign", + "assume_zero": false, + "candidate_count": 66, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -6, + "n": -5 + }, + { + "u": -6, + "n": -4 + }, + { + "u": -6, + "n": -3 + } + ] + }, + { + "residual": -5, + "noise_bound": 5, + "view": "sign", + "assume_zero": true, + "candidate_count": 5, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -5 + }, + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": -3 + } + ] + }, + { + "residual": -5, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 14, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": -5, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -5 + }, + { + "u": 0, + "n": 5 + } + ] + }, + { + "residual": -5, + "noise_bound": 6, + "view": "exact", + "assume_zero": false, + "candidate_count": 8, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": -5, + "noise_bound": 6, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -5 + } + ] + }, + { + "residual": -5, + "noise_bound": 6, + "view": "sign", + "assume_zero": false, + "candidate_count": 78, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -6, + "n": -6 + }, + { + "u": -6, + "n": -5 + }, + { + "u": -6, + "n": -4 + } + ] + }, + { + "residual": -5, + "noise_bound": 6, + "view": "sign", + "assume_zero": true, + "candidate_count": 6, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -6 + }, + { + "u": 0, + "n": -5 + }, + { + "u": 0, + "n": -4 + } + ] + }, + { + "residual": -5, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 16, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": -5, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -5 + }, + { + "u": 0, + "n": 5 + } + ] + }, + { + "residual": -4, + "noise_bound": 0, + "view": "exact", + "assume_zero": false, + "candidate_count": 1, + "presence": "entailed", + "identified_values": [ + -4 + ], + "first_candidates": [ + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -4, + "noise_bound": 0, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -4, + "noise_bound": 0, + "view": "sign", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -4, + "noise_bound": 0, + "view": "sign", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -4, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 2, + "presence": "entailed", + "identified_values": [ + -4, + 4 + ], + "first_candidates": [ + { + "u": -4, + "n": 0 + }, + { + "u": 4, + "n": 0 + } + ] + }, + { + "residual": -4, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -4, + "noise_bound": 1, + "view": "exact", + "assume_zero": false, + "candidate_count": 3, + "presence": "entailed", + "identified_values": [ + -5, + -4, + -3 + ], + "first_candidates": [ + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + }, + { + "u": -3, + "n": -1 + } + ] + }, + { + "residual": -4, + "noise_bound": 1, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -4, + "noise_bound": 1, + "view": "sign", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0 + ], + "first_candidates": [ + { + "u": -6, + "n": -1 + }, + { + "u": -6, + "n": 0 + }, + { + "u": -6, + "n": 1 + } + ] + }, + { + "residual": -4, + "noise_bound": 1, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -4, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -5, + -4, + -3, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + }, + { + "u": -3, + "n": -1 + } + ] + }, + { + "residual": -4, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -4, + "noise_bound": 2, + "view": "exact", + "assume_zero": false, + "candidate_count": 5, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2 + ], + "first_candidates": [ + { + "u": -6, + "n": 2 + }, + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -4, + "noise_bound": 2, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -4, + "noise_bound": 2, + "view": "sign", + "assume_zero": false, + "candidate_count": 30, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1 + ], + "first_candidates": [ + { + "u": -6, + "n": -2 + }, + { + "u": -6, + "n": -1 + }, + { + "u": -6, + "n": 0 + } + ] + }, + { + "residual": -4, + "noise_bound": 2, + "view": "sign", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -4, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 10, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 2 + }, + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -4, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -4, + "noise_bound": 3, + "view": "exact", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1 + ], + "first_candidates": [ + { + "u": -6, + "n": 2 + }, + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -4, + "noise_bound": 3, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -4, + "noise_bound": 3, + "view": "sign", + "assume_zero": false, + "candidate_count": 42, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2 + ], + "first_candidates": [ + { + "u": -6, + "n": -3 + }, + { + "u": -6, + "n": -2 + }, + { + "u": -6, + "n": -1 + } + ] + }, + { + "residual": -4, + "noise_bound": 3, + "view": "sign", + "assume_zero": true, + "candidate_count": 3, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -4, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 12, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 2 + }, + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -4, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -4, + "noise_bound": 4, + "view": "exact", + "assume_zero": false, + "candidate_count": 7, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0 + ], + "first_candidates": [ + { + "u": -6, + "n": 2 + }, + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -4, + "noise_bound": 4, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -4 + } + ] + }, + { + "residual": -4, + "noise_bound": 4, + "view": "sign", + "assume_zero": false, + "candidate_count": 54, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -6, + "n": -4 + }, + { + "u": -6, + "n": -3 + }, + { + "u": -6, + "n": -2 + } + ] + }, + { + "residual": -4, + "noise_bound": 4, + "view": "sign", + "assume_zero": true, + "candidate_count": 4, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": -2 + } + ] + }, + { + "residual": -4, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 14, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 2 + }, + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -4, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": 4 + } + ] + }, + { + "residual": -4, + "noise_bound": 5, + "view": "exact", + "assume_zero": false, + "candidate_count": 8, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1 + ], + "first_candidates": [ + { + "u": -6, + "n": 2 + }, + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -4, + "noise_bound": 5, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -4 + } + ] + }, + { + "residual": -4, + "noise_bound": 5, + "view": "sign", + "assume_zero": false, + "candidate_count": 66, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -6, + "n": -5 + }, + { + "u": -6, + "n": -4 + }, + { + "u": -6, + "n": -3 + } + ] + }, + { + "residual": -4, + "noise_bound": 5, + "view": "sign", + "assume_zero": true, + "candidate_count": 5, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -5 + }, + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": -3 + } + ] + }, + { + "residual": -4, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 16, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 2 + }, + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -4, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": 4 + } + ] + }, + { + "residual": -4, + "noise_bound": 6, + "view": "exact", + "assume_zero": false, + "candidate_count": 9, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2 + ], + "first_candidates": [ + { + "u": -6, + "n": 2 + }, + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -4, + "noise_bound": 6, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -4 + } + ] + }, + { + "residual": -4, + "noise_bound": 6, + "view": "sign", + "assume_zero": false, + "candidate_count": 78, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -6, + "n": -6 + }, + { + "u": -6, + "n": -5 + }, + { + "u": -6, + "n": -4 + } + ] + }, + { + "residual": -4, + "noise_bound": 6, + "view": "sign", + "assume_zero": true, + "candidate_count": 6, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -6 + }, + { + "u": 0, + "n": -5 + }, + { + "u": 0, + "n": -4 + } + ] + }, + { + "residual": -4, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 2 + }, + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -4, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": 4 + } + ] + }, + { + "residual": -3, + "noise_bound": 0, + "view": "exact", + "assume_zero": false, + "candidate_count": 1, + "presence": "entailed", + "identified_values": [ + -3 + ], + "first_candidates": [ + { + "u": -3, + "n": 0 + } + ] + }, + { + "residual": -3, + "noise_bound": 0, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -3, + "noise_bound": 0, + "view": "sign", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -3, + "noise_bound": 0, + "view": "sign", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -3, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 2, + "presence": "entailed", + "identified_values": [ + -3, + 3 + ], + "first_candidates": [ + { + "u": -3, + "n": 0 + }, + { + "u": 3, + "n": 0 + } + ] + }, + { + "residual": -3, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -3, + "noise_bound": 1, + "view": "exact", + "assume_zero": false, + "candidate_count": 3, + "presence": "entailed", + "identified_values": [ + -4, + -3, + -2 + ], + "first_candidates": [ + { + "u": -4, + "n": 1 + }, + { + "u": -3, + "n": 0 + }, + { + "u": -2, + "n": -1 + } + ] + }, + { + "residual": -3, + "noise_bound": 1, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -3, + "noise_bound": 1, + "view": "sign", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0 + ], + "first_candidates": [ + { + "u": -6, + "n": -1 + }, + { + "u": -6, + "n": 0 + }, + { + "u": -6, + "n": 1 + } + ] + }, + { + "residual": -3, + "noise_bound": 1, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -3, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -4, + -3, + -2, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -4, + "n": 1 + }, + { + "u": -3, + "n": 0 + }, + { + "u": -2, + "n": -1 + } + ] + }, + { + "residual": -3, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -3, + "noise_bound": 2, + "view": "exact", + "assume_zero": false, + "candidate_count": 5, + "presence": "entailed", + "identified_values": [ + -5, + -4, + -3, + -2, + -1 + ], + "first_candidates": [ + { + "u": -5, + "n": 2 + }, + { + "u": -4, + "n": 1 + }, + { + "u": -3, + "n": 0 + } + ] + }, + { + "residual": -3, + "noise_bound": 2, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -3, + "noise_bound": 2, + "view": "sign", + "assume_zero": false, + "candidate_count": 30, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1 + ], + "first_candidates": [ + { + "u": -6, + "n": -2 + }, + { + "u": -6, + "n": -1 + }, + { + "u": -6, + "n": 0 + } + ] + }, + { + "residual": -3, + "noise_bound": 2, + "view": "sign", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -3, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 10, + "presence": "entailed", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -5, + "n": 2 + }, + { + "u": -4, + "n": 1 + }, + { + "u": -3, + "n": 0 + } + ] + }, + { + "residual": -3, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -3, + "noise_bound": 3, + "view": "exact", + "assume_zero": false, + "candidate_count": 7, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0 + ], + "first_candidates": [ + { + "u": -6, + "n": 3 + }, + { + "u": -5, + "n": 2 + }, + { + "u": -4, + "n": 1 + } + ] + }, + { + "residual": -3, + "noise_bound": 3, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + } + ] + }, + { + "residual": -3, + "noise_bound": 3, + "view": "sign", + "assume_zero": false, + "candidate_count": 42, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2 + ], + "first_candidates": [ + { + "u": -6, + "n": -3 + }, + { + "u": -6, + "n": -2 + }, + { + "u": -6, + "n": -1 + } + ] + }, + { + "residual": -3, + "noise_bound": 3, + "view": "sign", + "assume_zero": true, + "candidate_count": 3, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -3, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 14, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 3 + }, + { + "u": -5, + "n": 2 + }, + { + "u": -4, + "n": 1 + } + ] + }, + { + "residual": -3, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": -3, + "noise_bound": 4, + "view": "exact", + "assume_zero": false, + "candidate_count": 8, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1 + ], + "first_candidates": [ + { + "u": -6, + "n": 3 + }, + { + "u": -5, + "n": 2 + }, + { + "u": -4, + "n": 1 + } + ] + }, + { + "residual": -3, + "noise_bound": 4, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + } + ] + }, + { + "residual": -3, + "noise_bound": 4, + "view": "sign", + "assume_zero": false, + "candidate_count": 54, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -6, + "n": -4 + }, + { + "u": -6, + "n": -3 + }, + { + "u": -6, + "n": -2 + } + ] + }, + { + "residual": -3, + "noise_bound": 4, + "view": "sign", + "assume_zero": true, + "candidate_count": 4, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": -2 + } + ] + }, + { + "residual": -3, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 16, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 3 + }, + { + "u": -5, + "n": 2 + }, + { + "u": -4, + "n": 1 + } + ] + }, + { + "residual": -3, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": -3, + "noise_bound": 5, + "view": "exact", + "assume_zero": false, + "candidate_count": 9, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2 + ], + "first_candidates": [ + { + "u": -6, + "n": 3 + }, + { + "u": -5, + "n": 2 + }, + { + "u": -4, + "n": 1 + } + ] + }, + { + "residual": -3, + "noise_bound": 5, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + } + ] + }, + { + "residual": -3, + "noise_bound": 5, + "view": "sign", + "assume_zero": false, + "candidate_count": 66, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -6, + "n": -5 + }, + { + "u": -6, + "n": -4 + }, + { + "u": -6, + "n": -3 + } + ] + }, + { + "residual": -3, + "noise_bound": 5, + "view": "sign", + "assume_zero": true, + "candidate_count": 5, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -5 + }, + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": -3 + } + ] + }, + { + "residual": -3, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 3 + }, + { + "u": -5, + "n": 2 + }, + { + "u": -4, + "n": 1 + } + ] + }, + { + "residual": -3, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": -3, + "noise_bound": 6, + "view": "exact", + "assume_zero": false, + "candidate_count": 10, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -6, + "n": 3 + }, + { + "u": -5, + "n": 2 + }, + { + "u": -4, + "n": 1 + } + ] + }, + { + "residual": -3, + "noise_bound": 6, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + } + ] + }, + { + "residual": -3, + "noise_bound": 6, + "view": "sign", + "assume_zero": false, + "candidate_count": 78, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -6, + "n": -6 + }, + { + "u": -6, + "n": -5 + }, + { + "u": -6, + "n": -4 + } + ] + }, + { + "residual": -3, + "noise_bound": 6, + "view": "sign", + "assume_zero": true, + "candidate_count": 6, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -6 + }, + { + "u": 0, + "n": -5 + }, + { + "u": 0, + "n": -4 + } + ] + }, + { + "residual": -3, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 20, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 3 + }, + { + "u": -5, + "n": 2 + }, + { + "u": -4, + "n": 1 + } + ] + }, + { + "residual": -3, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": -2, + "noise_bound": 0, + "view": "exact", + "assume_zero": false, + "candidate_count": 1, + "presence": "entailed", + "identified_values": [ + -2 + ], + "first_candidates": [ + { + "u": -2, + "n": 0 + } + ] + }, + { + "residual": -2, + "noise_bound": 0, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -2, + "noise_bound": 0, + "view": "sign", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -2, + "noise_bound": 0, + "view": "sign", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -2, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 2, + "presence": "entailed", + "identified_values": [ + -2, + 2 + ], + "first_candidates": [ + { + "u": -2, + "n": 0 + }, + { + "u": 2, + "n": 0 + } + ] + }, + { + "residual": -2, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -2, + "noise_bound": 1, + "view": "exact", + "assume_zero": false, + "candidate_count": 3, + "presence": "entailed", + "identified_values": [ + -3, + -2, + -1 + ], + "first_candidates": [ + { + "u": -3, + "n": 1 + }, + { + "u": -2, + "n": 0 + }, + { + "u": -1, + "n": -1 + } + ] + }, + { + "residual": -2, + "noise_bound": 1, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -2, + "noise_bound": 1, + "view": "sign", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0 + ], + "first_candidates": [ + { + "u": -6, + "n": -1 + }, + { + "u": -6, + "n": 0 + }, + { + "u": -6, + "n": 1 + } + ] + }, + { + "residual": -2, + "noise_bound": 1, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -2, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -3, + -2, + -1, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -3, + "n": 1 + }, + { + "u": -2, + "n": 0 + }, + { + "u": -1, + "n": -1 + } + ] + }, + { + "residual": -2, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -2, + "noise_bound": 2, + "view": "exact", + "assume_zero": false, + "candidate_count": 5, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0 + ], + "first_candidates": [ + { + "u": -4, + "n": 2 + }, + { + "u": -3, + "n": 1 + }, + { + "u": -2, + "n": 0 + } + ] + }, + { + "residual": -2, + "noise_bound": 2, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + } + ] + }, + { + "residual": -2, + "noise_bound": 2, + "view": "sign", + "assume_zero": false, + "candidate_count": 30, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1 + ], + "first_candidates": [ + { + "u": -6, + "n": -2 + }, + { + "u": -6, + "n": -1 + }, + { + "u": -6, + "n": 0 + } + ] + }, + { + "residual": -2, + "noise_bound": 2, + "view": "sign", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -2, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 10, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -4, + "n": 2 + }, + { + "u": -3, + "n": 1 + }, + { + "u": -2, + "n": 0 + } + ] + }, + { + "residual": -2, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": -2, + "noise_bound": 3, + "view": "exact", + "assume_zero": false, + "candidate_count": 7, + "presence": "unresolved", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 0, + 1 + ], + "first_candidates": [ + { + "u": -5, + "n": 3 + }, + { + "u": -4, + "n": 2 + }, + { + "u": -3, + "n": 1 + } + ] + }, + { + "residual": -2, + "noise_bound": 3, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + } + ] + }, + { + "residual": -2, + "noise_bound": 3, + "view": "sign", + "assume_zero": false, + "candidate_count": 42, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2 + ], + "first_candidates": [ + { + "u": -6, + "n": -3 + }, + { + "u": -6, + "n": -2 + }, + { + "u": -6, + "n": -1 + } + ] + }, + { + "residual": -2, + "noise_bound": 3, + "view": "sign", + "assume_zero": true, + "candidate_count": 3, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -2, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 14, + "presence": "unresolved", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -5, + "n": 3 + }, + { + "u": -4, + "n": 2 + }, + { + "u": -3, + "n": 1 + } + ] + }, + { + "residual": -2, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": -2, + "noise_bound": 4, + "view": "exact", + "assume_zero": false, + "candidate_count": 9, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2 + ], + "first_candidates": [ + { + "u": -6, + "n": 4 + }, + { + "u": -5, + "n": 3 + }, + { + "u": -4, + "n": 2 + } + ] + }, + { + "residual": -2, + "noise_bound": 4, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + } + ] + }, + { + "residual": -2, + "noise_bound": 4, + "view": "sign", + "assume_zero": false, + "candidate_count": 54, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -6, + "n": -4 + }, + { + "u": -6, + "n": -3 + }, + { + "u": -6, + "n": -2 + } + ] + }, + { + "residual": -2, + "noise_bound": 4, + "view": "sign", + "assume_zero": true, + "candidate_count": 4, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": -2 + } + ] + }, + { + "residual": -2, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 4 + }, + { + "u": -5, + "n": 3 + }, + { + "u": -4, + "n": 2 + } + ] + }, + { + "residual": -2, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": -2, + "noise_bound": 5, + "view": "exact", + "assume_zero": false, + "candidate_count": 10, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -6, + "n": 4 + }, + { + "u": -5, + "n": 3 + }, + { + "u": -4, + "n": 2 + } + ] + }, + { + "residual": -2, + "noise_bound": 5, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + } + ] + }, + { + "residual": -2, + "noise_bound": 5, + "view": "sign", + "assume_zero": false, + "candidate_count": 66, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -6, + "n": -5 + }, + { + "u": -6, + "n": -4 + }, + { + "u": -6, + "n": -3 + } + ] + }, + { + "residual": -2, + "noise_bound": 5, + "view": "sign", + "assume_zero": true, + "candidate_count": 5, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -5 + }, + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": -3 + } + ] + }, + { + "residual": -2, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 20, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 4 + }, + { + "u": -5, + "n": 3 + }, + { + "u": -4, + "n": 2 + } + ] + }, + { + "residual": -2, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": -2, + "noise_bound": 6, + "view": "exact", + "assume_zero": false, + "candidate_count": 11, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -6, + "n": 4 + }, + { + "u": -5, + "n": 3 + }, + { + "u": -4, + "n": 2 + } + ] + }, + { + "residual": -2, + "noise_bound": 6, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + } + ] + }, + { + "residual": -2, + "noise_bound": 6, + "view": "sign", + "assume_zero": false, + "candidate_count": 78, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -6, + "n": -6 + }, + { + "u": -6, + "n": -5 + }, + { + "u": -6, + "n": -4 + } + ] + }, + { + "residual": -2, + "noise_bound": 6, + "view": "sign", + "assume_zero": true, + "candidate_count": 6, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -6 + }, + { + "u": 0, + "n": -5 + }, + { + "u": 0, + "n": -4 + } + ] + }, + { + "residual": -2, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 22, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 4 + }, + { + "u": -5, + "n": 3 + }, + { + "u": -4, + "n": 2 + } + ] + }, + { + "residual": -2, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": -1, + "noise_bound": 0, + "view": "exact", + "assume_zero": false, + "candidate_count": 1, + "presence": "entailed", + "identified_values": [ + -1 + ], + "first_candidates": [ + { + "u": -1, + "n": 0 + } + ] + }, + { + "residual": -1, + "noise_bound": 0, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -1, + "noise_bound": 0, + "view": "sign", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": -1, + "noise_bound": 0, + "view": "sign", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -1, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 2, + "presence": "entailed", + "identified_values": [ + -1, + 1 + ], + "first_candidates": [ + { + "u": -1, + "n": 0 + }, + { + "u": 1, + "n": 0 + } + ] + }, + { + "residual": -1, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": -1, + "noise_bound": 1, + "view": "exact", + "assume_zero": false, + "candidate_count": 3, + "presence": "unresolved", + "identified_values": [ + -2, + -1, + 0 + ], + "first_candidates": [ + { + "u": -2, + "n": 1 + }, + { + "u": -1, + "n": 0 + }, + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -1, + "noise_bound": 1, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -1, + "noise_bound": 1, + "view": "sign", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0 + ], + "first_candidates": [ + { + "u": -6, + "n": -1 + }, + { + "u": -6, + "n": 0 + }, + { + "u": -6, + "n": 1 + } + ] + }, + { + "residual": -1, + "noise_bound": 1, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -1, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 6, + "presence": "unresolved", + "identified_values": [ + -2, + -1, + 0, + 1, + 2 + ], + "first_candidates": [ + { + "u": -2, + "n": 1 + }, + { + "u": -1, + "n": 0 + }, + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -1, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + }, + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": -1, + "noise_bound": 2, + "view": "exact", + "assume_zero": false, + "candidate_count": 5, + "presence": "unresolved", + "identified_values": [ + -3, + -2, + -1, + 0, + 1 + ], + "first_candidates": [ + { + "u": -3, + "n": 2 + }, + { + "u": -2, + "n": 1 + }, + { + "u": -1, + "n": 0 + } + ] + }, + { + "residual": -1, + "noise_bound": 2, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -1, + "noise_bound": 2, + "view": "sign", + "assume_zero": false, + "candidate_count": 30, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1 + ], + "first_candidates": [ + { + "u": -6, + "n": -2 + }, + { + "u": -6, + "n": -1 + }, + { + "u": -6, + "n": 0 + } + ] + }, + { + "residual": -1, + "noise_bound": 2, + "view": "sign", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -1, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 10, + "presence": "unresolved", + "identified_values": [ + -3, + -2, + -1, + 0, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -3, + "n": 2 + }, + { + "u": -2, + "n": 1 + }, + { + "u": -1, + "n": 0 + } + ] + }, + { + "residual": -1, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + }, + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": -1, + "noise_bound": 3, + "view": "exact", + "assume_zero": false, + "candidate_count": 7, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2 + ], + "first_candidates": [ + { + "u": -4, + "n": 3 + }, + { + "u": -3, + "n": 2 + }, + { + "u": -2, + "n": 1 + } + ] + }, + { + "residual": -1, + "noise_bound": 3, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -1, + "noise_bound": 3, + "view": "sign", + "assume_zero": false, + "candidate_count": 42, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2 + ], + "first_candidates": [ + { + "u": -6, + "n": -3 + }, + { + "u": -6, + "n": -2 + }, + { + "u": -6, + "n": -1 + } + ] + }, + { + "residual": -1, + "noise_bound": 3, + "view": "sign", + "assume_zero": true, + "candidate_count": 3, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -1, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 14, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -4, + "n": 3 + }, + { + "u": -3, + "n": 2 + }, + { + "u": -2, + "n": 1 + } + ] + }, + { + "residual": -1, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + }, + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": -1, + "noise_bound": 4, + "view": "exact", + "assume_zero": false, + "candidate_count": 9, + "presence": "unresolved", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -5, + "n": 4 + }, + { + "u": -4, + "n": 3 + }, + { + "u": -3, + "n": 2 + } + ] + }, + { + "residual": -1, + "noise_bound": 4, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -1, + "noise_bound": 4, + "view": "sign", + "assume_zero": false, + "candidate_count": 54, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -6, + "n": -4 + }, + { + "u": -6, + "n": -3 + }, + { + "u": -6, + "n": -2 + } + ] + }, + { + "residual": -1, + "noise_bound": 4, + "view": "sign", + "assume_zero": true, + "candidate_count": 4, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": -2 + } + ] + }, + { + "residual": -1, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -5, + "n": 4 + }, + { + "u": -4, + "n": 3 + }, + { + "u": -3, + "n": 2 + } + ] + }, + { + "residual": -1, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + }, + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": -1, + "noise_bound": 5, + "view": "exact", + "assume_zero": false, + "candidate_count": 11, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -6, + "n": 5 + }, + { + "u": -5, + "n": 4 + }, + { + "u": -4, + "n": 3 + } + ] + }, + { + "residual": -1, + "noise_bound": 5, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -1, + "noise_bound": 5, + "view": "sign", + "assume_zero": false, + "candidate_count": 66, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -6, + "n": -5 + }, + { + "u": -6, + "n": -4 + }, + { + "u": -6, + "n": -3 + } + ] + }, + { + "residual": -1, + "noise_bound": 5, + "view": "sign", + "assume_zero": true, + "candidate_count": 5, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -5 + }, + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": -3 + } + ] + }, + { + "residual": -1, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 22, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 5 + }, + { + "u": -5, + "n": 4 + }, + { + "u": -4, + "n": 3 + } + ] + }, + { + "residual": -1, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + }, + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": -1, + "noise_bound": 6, + "view": "exact", + "assume_zero": false, + "candidate_count": 12, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -6, + "n": 5 + }, + { + "u": -5, + "n": 4 + }, + { + "u": -4, + "n": 3 + } + ] + }, + { + "residual": -1, + "noise_bound": 6, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": -1, + "noise_bound": 6, + "view": "sign", + "assume_zero": false, + "candidate_count": 78, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -6, + "n": -6 + }, + { + "u": -6, + "n": -5 + }, + { + "u": -6, + "n": -4 + } + ] + }, + { + "residual": -1, + "noise_bound": 6, + "view": "sign", + "assume_zero": true, + "candidate_count": 6, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -6 + }, + { + "u": 0, + "n": -5 + }, + { + "u": 0, + "n": -4 + } + ] + }, + { + "residual": -1, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 24, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 5 + }, + { + "u": -5, + "n": 4 + }, + { + "u": -5, + "n": 6 + } + ] + }, + { + "residual": -1, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + }, + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 0, + "noise_bound": 0, + "view": "exact", + "assume_zero": false, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 0, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 0, + "view": "sign", + "assume_zero": false, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 0, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 1, + "view": "exact", + "assume_zero": false, + "candidate_count": 3, + "presence": "unresolved", + "identified_values": [ + -1, + 0, + 1 + ], + "first_candidates": [ + { + "u": -1, + "n": 1 + }, + { + "u": 0, + "n": 0 + }, + { + "u": 1, + "n": -1 + } + ] + }, + { + "residual": 0, + "noise_bound": 1, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 1, + "view": "sign", + "assume_zero": false, + "candidate_count": 3, + "presence": "unresolved", + "identified_values": [ + -1, + 0, + 1 + ], + "first_candidates": [ + { + "u": -1, + "n": 1 + }, + { + "u": 0, + "n": 0 + }, + { + "u": 1, + "n": -1 + } + ] + }, + { + "residual": 0, + "noise_bound": 1, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 3, + "presence": "unresolved", + "identified_values": [ + -1, + 0, + 1 + ], + "first_candidates": [ + { + "u": -1, + "n": 1 + }, + { + "u": 0, + "n": 0 + }, + { + "u": 1, + "n": -1 + } + ] + }, + { + "residual": 0, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 2, + "view": "exact", + "assume_zero": false, + "candidate_count": 5, + "presence": "unresolved", + "identified_values": [ + -2, + -1, + 0, + 1, + 2 + ], + "first_candidates": [ + { + "u": -2, + "n": 2 + }, + { + "u": -1, + "n": 1 + }, + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 2, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 2, + "view": "sign", + "assume_zero": false, + "candidate_count": 5, + "presence": "unresolved", + "identified_values": [ + -2, + -1, + 0, + 1, + 2 + ], + "first_candidates": [ + { + "u": -2, + "n": 2 + }, + { + "u": -1, + "n": 1 + }, + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 2, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 5, + "presence": "unresolved", + "identified_values": [ + -2, + -1, + 0, + 1, + 2 + ], + "first_candidates": [ + { + "u": -2, + "n": 2 + }, + { + "u": -1, + "n": 1 + }, + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 3, + "view": "exact", + "assume_zero": false, + "candidate_count": 7, + "presence": "unresolved", + "identified_values": [ + -3, + -2, + -1, + 0, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -3, + "n": 3 + }, + { + "u": -2, + "n": 2 + }, + { + "u": -1, + "n": 1 + } + ] + }, + { + "residual": 0, + "noise_bound": 3, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 3, + "view": "sign", + "assume_zero": false, + "candidate_count": 7, + "presence": "unresolved", + "identified_values": [ + -3, + -2, + -1, + 0, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -3, + "n": 3 + }, + { + "u": -2, + "n": 2 + }, + { + "u": -1, + "n": 1 + } + ] + }, + { + "residual": 0, + "noise_bound": 3, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 7, + "presence": "unresolved", + "identified_values": [ + -3, + -2, + -1, + 0, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -3, + "n": 3 + }, + { + "u": -2, + "n": 2 + }, + { + "u": -1, + "n": 1 + } + ] + }, + { + "residual": 0, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 4, + "view": "exact", + "assume_zero": false, + "candidate_count": 9, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -4, + "n": 4 + }, + { + "u": -3, + "n": 3 + }, + { + "u": -2, + "n": 2 + } + ] + }, + { + "residual": 0, + "noise_bound": 4, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 4, + "view": "sign", + "assume_zero": false, + "candidate_count": 9, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -4, + "n": 4 + }, + { + "u": -3, + "n": 3 + }, + { + "u": -2, + "n": 2 + } + ] + }, + { + "residual": 0, + "noise_bound": 4, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 9, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -4, + "n": 4 + }, + { + "u": -3, + "n": 3 + }, + { + "u": -2, + "n": 2 + } + ] + }, + { + "residual": 0, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 5, + "view": "exact", + "assume_zero": false, + "candidate_count": 11, + "presence": "unresolved", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -5, + "n": 5 + }, + { + "u": -4, + "n": 4 + }, + { + "u": -3, + "n": 3 + } + ] + }, + { + "residual": 0, + "noise_bound": 5, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 5, + "view": "sign", + "assume_zero": false, + "candidate_count": 11, + "presence": "unresolved", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -5, + "n": 5 + }, + { + "u": -4, + "n": 4 + }, + { + "u": -3, + "n": 3 + } + ] + }, + { + "residual": 0, + "noise_bound": 5, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 11, + "presence": "unresolved", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -5, + "n": 5 + }, + { + "u": -4, + "n": 4 + }, + { + "u": -3, + "n": 3 + } + ] + }, + { + "residual": 0, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 6, + "view": "exact", + "assume_zero": false, + "candidate_count": 13, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 6 + }, + { + "u": -5, + "n": 5 + }, + { + "u": -4, + "n": 4 + } + ] + }, + { + "residual": 0, + "noise_bound": 6, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 6, + "view": "sign", + "assume_zero": false, + "candidate_count": 13, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 6 + }, + { + "u": -5, + "n": 5 + }, + { + "u": -4, + "n": 4 + } + ] + }, + { + "residual": 0, + "noise_bound": 6, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 0, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 13, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 6 + }, + { + "u": -5, + "n": 5 + }, + { + "u": -4, + "n": 4 + } + ] + }, + { + "residual": 0, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 0 + } + ] + }, + { + "residual": 1, + "noise_bound": 0, + "view": "exact", + "assume_zero": false, + "candidate_count": 1, + "presence": "entailed", + "identified_values": [ + 1 + ], + "first_candidates": [ + { + "u": 1, + "n": 0 + } + ] + }, + { + "residual": 1, + "noise_bound": 0, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 1, + "noise_bound": 0, + "view": "sign", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 1, + "n": 0 + }, + { + "u": 2, + "n": 0 + }, + { + "u": 3, + "n": 0 + } + ] + }, + { + "residual": 1, + "noise_bound": 0, + "view": "sign", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 1, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 2, + "presence": "entailed", + "identified_values": [ + -1, + 1 + ], + "first_candidates": [ + { + "u": -1, + "n": 0 + }, + { + "u": 1, + "n": 0 + } + ] + }, + { + "residual": 1, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 1, + "noise_bound": 1, + "view": "exact", + "assume_zero": false, + "candidate_count": 3, + "presence": "unresolved", + "identified_values": [ + 0, + 1, + 2 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 1, + "n": 0 + }, + { + "u": 2, + "n": -1 + } + ] + }, + { + "residual": 1, + "noise_bound": 1, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 1, + "noise_bound": 1, + "view": "sign", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 1, + "n": 0 + }, + { + "u": 1, + "n": 1 + } + ] + }, + { + "residual": 1, + "noise_bound": 1, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 1, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 6, + "presence": "unresolved", + "identified_values": [ + -2, + -1, + 0, + 1, + 2 + ], + "first_candidates": [ + { + "u": -2, + "n": 1 + }, + { + "u": -1, + "n": 0 + }, + { + "u": 0, + "n": -1 + } + ] + }, + { + "residual": 1, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + }, + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 1, + "noise_bound": 2, + "view": "exact", + "assume_zero": false, + "candidate_count": 5, + "presence": "unresolved", + "identified_values": [ + -1, + 0, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -1, + "n": 2 + }, + { + "u": 0, + "n": 1 + }, + { + "u": 1, + "n": 0 + } + ] + }, + { + "residual": 1, + "noise_bound": 2, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 1, + "noise_bound": 2, + "view": "sign", + "assume_zero": false, + "candidate_count": 30, + "presence": "unresolved", + "identified_values": [ + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -1, + "n": 2 + }, + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 1, + "noise_bound": 2, + "view": "sign", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 1, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 10, + "presence": "unresolved", + "identified_values": [ + -3, + -2, + -1, + 0, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -3, + "n": 2 + }, + { + "u": -2, + "n": 1 + }, + { + "u": -1, + "n": 0 + } + ] + }, + { + "residual": 1, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + }, + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 1, + "noise_bound": 3, + "view": "exact", + "assume_zero": false, + "candidate_count": 7, + "presence": "unresolved", + "identified_values": [ + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -2, + "n": 3 + }, + { + "u": -1, + "n": 2 + }, + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 1, + "noise_bound": 3, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 1, + "noise_bound": 3, + "view": "sign", + "assume_zero": false, + "candidate_count": 42, + "presence": "unresolved", + "identified_values": [ + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -2, + "n": 3 + }, + { + "u": -1, + "n": 2 + }, + { + "u": -1, + "n": 3 + } + ] + }, + { + "residual": 1, + "noise_bound": 3, + "view": "sign", + "assume_zero": true, + "candidate_count": 3, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 1, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 14, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -4, + "n": 3 + }, + { + "u": -3, + "n": 2 + }, + { + "u": -2, + "n": 1 + } + ] + }, + { + "residual": 1, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + }, + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 1, + "noise_bound": 4, + "view": "exact", + "assume_zero": false, + "candidate_count": 9, + "presence": "unresolved", + "identified_values": [ + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -3, + "n": 4 + }, + { + "u": -2, + "n": 3 + }, + { + "u": -1, + "n": 2 + } + ] + }, + { + "residual": 1, + "noise_bound": 4, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 1, + "noise_bound": 4, + "view": "sign", + "assume_zero": false, + "candidate_count": 54, + "presence": "unresolved", + "identified_values": [ + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -3, + "n": 4 + }, + { + "u": -2, + "n": 3 + }, + { + "u": -2, + "n": 4 + } + ] + }, + { + "residual": 1, + "noise_bound": 4, + "view": "sign", + "assume_zero": true, + "candidate_count": 4, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 1, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -5, + "n": 4 + }, + { + "u": -4, + "n": 3 + }, + { + "u": -3, + "n": 2 + } + ] + }, + { + "residual": 1, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + }, + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 1, + "noise_bound": 5, + "view": "exact", + "assume_zero": false, + "candidate_count": 11, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -4, + "n": 5 + }, + { + "u": -3, + "n": 4 + }, + { + "u": -2, + "n": 3 + } + ] + }, + { + "residual": 1, + "noise_bound": 5, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 1, + "noise_bound": 5, + "view": "sign", + "assume_zero": false, + "candidate_count": 66, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -4, + "n": 5 + }, + { + "u": -3, + "n": 4 + }, + { + "u": -3, + "n": 5 + } + ] + }, + { + "residual": 1, + "noise_bound": 5, + "view": "sign", + "assume_zero": true, + "candidate_count": 5, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 1, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 22, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 5 + }, + { + "u": -5, + "n": 4 + }, + { + "u": -4, + "n": 3 + } + ] + }, + { + "residual": 1, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + }, + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 1, + "noise_bound": 6, + "view": "exact", + "assume_zero": false, + "candidate_count": 12, + "presence": "unresolved", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -5, + "n": 6 + }, + { + "u": -4, + "n": 5 + }, + { + "u": -3, + "n": 4 + } + ] + }, + { + "residual": 1, + "noise_bound": 6, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 1, + "noise_bound": 6, + "view": "sign", + "assume_zero": false, + "candidate_count": 78, + "presence": "unresolved", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -5, + "n": 6 + }, + { + "u": -4, + "n": 5 + }, + { + "u": -4, + "n": 6 + } + ] + }, + { + "residual": 1, + "noise_bound": 6, + "view": "sign", + "assume_zero": true, + "candidate_count": 6, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 1, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 24, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 5 + }, + { + "u": -5, + "n": 4 + }, + { + "u": -5, + "n": 6 + } + ] + }, + { + "residual": 1, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -1 + }, + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 2, + "noise_bound": 0, + "view": "exact", + "assume_zero": false, + "candidate_count": 1, + "presence": "entailed", + "identified_values": [ + 2 + ], + "first_candidates": [ + { + "u": 2, + "n": 0 + } + ] + }, + { + "residual": 2, + "noise_bound": 0, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 2, + "noise_bound": 0, + "view": "sign", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 1, + "n": 0 + }, + { + "u": 2, + "n": 0 + }, + { + "u": 3, + "n": 0 + } + ] + }, + { + "residual": 2, + "noise_bound": 0, + "view": "sign", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 2, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 2, + "presence": "entailed", + "identified_values": [ + -2, + 2 + ], + "first_candidates": [ + { + "u": -2, + "n": 0 + }, + { + "u": 2, + "n": 0 + } + ] + }, + { + "residual": 2, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 2, + "noise_bound": 1, + "view": "exact", + "assume_zero": false, + "candidate_count": 3, + "presence": "entailed", + "identified_values": [ + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": 1, + "n": 1 + }, + { + "u": 2, + "n": 0 + }, + { + "u": 3, + "n": -1 + } + ] + }, + { + "residual": 2, + "noise_bound": 1, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 2, + "noise_bound": 1, + "view": "sign", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 1, + "n": 0 + }, + { + "u": 1, + "n": 1 + } + ] + }, + { + "residual": 2, + "noise_bound": 1, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 2, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -3, + -2, + -1, + 1, + 2, + 3 + ], + "first_candidates": [ + { + "u": -3, + "n": 1 + }, + { + "u": -2, + "n": 0 + }, + { + "u": -1, + "n": -1 + } + ] + }, + { + "residual": 2, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 2, + "noise_bound": 2, + "view": "exact", + "assume_zero": false, + "candidate_count": 5, + "presence": "unresolved", + "identified_values": [ + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": 0, + "n": 2 + }, + { + "u": 1, + "n": 1 + }, + { + "u": 2, + "n": 0 + } + ] + }, + { + "residual": 2, + "noise_bound": 2, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 2, + "noise_bound": 2, + "view": "sign", + "assume_zero": false, + "candidate_count": 30, + "presence": "unresolved", + "identified_values": [ + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -1, + "n": 2 + }, + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 2, + "noise_bound": 2, + "view": "sign", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 2, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 10, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -4, + "n": 2 + }, + { + "u": -3, + "n": 1 + }, + { + "u": -2, + "n": 0 + } + ] + }, + { + "residual": 2, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 2, + "noise_bound": 3, + "view": "exact", + "assume_zero": false, + "candidate_count": 7, + "presence": "unresolved", + "identified_values": [ + -1, + 0, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -1, + "n": 3 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 1, + "n": 1 + } + ] + }, + { + "residual": 2, + "noise_bound": 3, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 2, + "noise_bound": 3, + "view": "sign", + "assume_zero": false, + "candidate_count": 42, + "presence": "unresolved", + "identified_values": [ + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -2, + "n": 3 + }, + { + "u": -1, + "n": 2 + }, + { + "u": -1, + "n": 3 + } + ] + }, + { + "residual": 2, + "noise_bound": 3, + "view": "sign", + "assume_zero": true, + "candidate_count": 3, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 2, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 14, + "presence": "unresolved", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -5, + "n": 3 + }, + { + "u": -4, + "n": 2 + }, + { + "u": -3, + "n": 1 + } + ] + }, + { + "residual": 2, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 2, + "noise_bound": 4, + "view": "exact", + "assume_zero": false, + "candidate_count": 9, + "presence": "unresolved", + "identified_values": [ + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -2, + "n": 4 + }, + { + "u": -1, + "n": 3 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 2, + "noise_bound": 4, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 2, + "noise_bound": 4, + "view": "sign", + "assume_zero": false, + "candidate_count": 54, + "presence": "unresolved", + "identified_values": [ + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -3, + "n": 4 + }, + { + "u": -2, + "n": 3 + }, + { + "u": -2, + "n": 4 + } + ] + }, + { + "residual": 2, + "noise_bound": 4, + "view": "sign", + "assume_zero": true, + "candidate_count": 4, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 2, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 4 + }, + { + "u": -5, + "n": 3 + }, + { + "u": -4, + "n": 2 + } + ] + }, + { + "residual": 2, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 2, + "noise_bound": 5, + "view": "exact", + "assume_zero": false, + "candidate_count": 10, + "presence": "unresolved", + "identified_values": [ + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -3, + "n": 5 + }, + { + "u": -2, + "n": 4 + }, + { + "u": -1, + "n": 3 + } + ] + }, + { + "residual": 2, + "noise_bound": 5, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 2, + "noise_bound": 5, + "view": "sign", + "assume_zero": false, + "candidate_count": 66, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -4, + "n": 5 + }, + { + "u": -3, + "n": 4 + }, + { + "u": -3, + "n": 5 + } + ] + }, + { + "residual": 2, + "noise_bound": 5, + "view": "sign", + "assume_zero": true, + "candidate_count": 5, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 2, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 20, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 4 + }, + { + "u": -5, + "n": 3 + }, + { + "u": -4, + "n": 2 + } + ] + }, + { + "residual": 2, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 2, + "noise_bound": 6, + "view": "exact", + "assume_zero": false, + "candidate_count": 11, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -4, + "n": 6 + }, + { + "u": -3, + "n": 5 + }, + { + "u": -2, + "n": 4 + } + ] + }, + { + "residual": 2, + "noise_bound": 6, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 2, + "noise_bound": 6, + "view": "sign", + "assume_zero": false, + "candidate_count": 78, + "presence": "unresolved", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -5, + "n": 6 + }, + { + "u": -4, + "n": 5 + }, + { + "u": -4, + "n": 6 + } + ] + }, + { + "residual": 2, + "noise_bound": 6, + "view": "sign", + "assume_zero": true, + "candidate_count": 6, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 2, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 22, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 4 + }, + { + "u": -5, + "n": 3 + }, + { + "u": -4, + "n": 2 + } + ] + }, + { + "residual": 2, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -2 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 3, + "noise_bound": 0, + "view": "exact", + "assume_zero": false, + "candidate_count": 1, + "presence": "entailed", + "identified_values": [ + 3 + ], + "first_candidates": [ + { + "u": 3, + "n": 0 + } + ] + }, + { + "residual": 3, + "noise_bound": 0, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 3, + "noise_bound": 0, + "view": "sign", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 1, + "n": 0 + }, + { + "u": 2, + "n": 0 + }, + { + "u": 3, + "n": 0 + } + ] + }, + { + "residual": 3, + "noise_bound": 0, + "view": "sign", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 3, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 2, + "presence": "entailed", + "identified_values": [ + -3, + 3 + ], + "first_candidates": [ + { + "u": -3, + "n": 0 + }, + { + "u": 3, + "n": 0 + } + ] + }, + { + "residual": 3, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 3, + "noise_bound": 1, + "view": "exact", + "assume_zero": false, + "candidate_count": 3, + "presence": "entailed", + "identified_values": [ + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": 2, + "n": 1 + }, + { + "u": 3, + "n": 0 + }, + { + "u": 4, + "n": -1 + } + ] + }, + { + "residual": 3, + "noise_bound": 1, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 3, + "noise_bound": 1, + "view": "sign", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 1, + "n": 0 + }, + { + "u": 1, + "n": 1 + } + ] + }, + { + "residual": 3, + "noise_bound": 1, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 3, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -4, + -3, + -2, + 2, + 3, + 4 + ], + "first_candidates": [ + { + "u": -4, + "n": 1 + }, + { + "u": -3, + "n": 0 + }, + { + "u": -2, + "n": -1 + } + ] + }, + { + "residual": 3, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 3, + "noise_bound": 2, + "view": "exact", + "assume_zero": false, + "candidate_count": 5, + "presence": "entailed", + "identified_values": [ + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": 1, + "n": 2 + }, + { + "u": 2, + "n": 1 + }, + { + "u": 3, + "n": 0 + } + ] + }, + { + "residual": 3, + "noise_bound": 2, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 3, + "noise_bound": 2, + "view": "sign", + "assume_zero": false, + "candidate_count": 30, + "presence": "unresolved", + "identified_values": [ + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -1, + "n": 2 + }, + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 3, + "noise_bound": 2, + "view": "sign", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 3, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 10, + "presence": "entailed", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 1, + 2, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -5, + "n": 2 + }, + { + "u": -4, + "n": 1 + }, + { + "u": -3, + "n": 0 + } + ] + }, + { + "residual": 3, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 3, + "noise_bound": 3, + "view": "exact", + "assume_zero": false, + "candidate_count": 7, + "presence": "unresolved", + "identified_values": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 0, + "n": 3 + }, + { + "u": 1, + "n": 2 + }, + { + "u": 2, + "n": 1 + } + ] + }, + { + "residual": 3, + "noise_bound": 3, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 3, + "noise_bound": 3, + "view": "sign", + "assume_zero": false, + "candidate_count": 42, + "presence": "unresolved", + "identified_values": [ + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -2, + "n": 3 + }, + { + "u": -1, + "n": 2 + }, + { + "u": -1, + "n": 3 + } + ] + }, + { + "residual": 3, + "noise_bound": 3, + "view": "sign", + "assume_zero": true, + "candidate_count": 3, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 3, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 14, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 3 + }, + { + "u": -5, + "n": 2 + }, + { + "u": -4, + "n": 1 + } + ] + }, + { + "residual": 3, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 3, + "noise_bound": 4, + "view": "exact", + "assume_zero": false, + "candidate_count": 8, + "presence": "unresolved", + "identified_values": [ + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -1, + "n": 4 + }, + { + "u": 0, + "n": 3 + }, + { + "u": 1, + "n": 2 + } + ] + }, + { + "residual": 3, + "noise_bound": 4, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 3, + "noise_bound": 4, + "view": "sign", + "assume_zero": false, + "candidate_count": 54, + "presence": "unresolved", + "identified_values": [ + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -3, + "n": 4 + }, + { + "u": -2, + "n": 3 + }, + { + "u": -2, + "n": 4 + } + ] + }, + { + "residual": 3, + "noise_bound": 4, + "view": "sign", + "assume_zero": true, + "candidate_count": 4, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 3, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 16, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 3 + }, + { + "u": -5, + "n": 2 + }, + { + "u": -4, + "n": 1 + } + ] + }, + { + "residual": 3, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 3, + "noise_bound": 5, + "view": "exact", + "assume_zero": false, + "candidate_count": 9, + "presence": "unresolved", + "identified_values": [ + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -2, + "n": 5 + }, + { + "u": -1, + "n": 4 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 3, + "noise_bound": 5, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 3, + "noise_bound": 5, + "view": "sign", + "assume_zero": false, + "candidate_count": 66, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -4, + "n": 5 + }, + { + "u": -3, + "n": 4 + }, + { + "u": -3, + "n": 5 + } + ] + }, + { + "residual": 3, + "noise_bound": 5, + "view": "sign", + "assume_zero": true, + "candidate_count": 5, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 3, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 3 + }, + { + "u": -5, + "n": 2 + }, + { + "u": -4, + "n": 1 + } + ] + }, + { + "residual": 3, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 3, + "noise_bound": 6, + "view": "exact", + "assume_zero": false, + "candidate_count": 10, + "presence": "unresolved", + "identified_values": [ + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -3, + "n": 6 + }, + { + "u": -2, + "n": 5 + }, + { + "u": -1, + "n": 4 + } + ] + }, + { + "residual": 3, + "noise_bound": 6, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 3, + "noise_bound": 6, + "view": "sign", + "assume_zero": false, + "candidate_count": 78, + "presence": "unresolved", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -5, + "n": 6 + }, + { + "u": -4, + "n": 5 + }, + { + "u": -4, + "n": 6 + } + ] + }, + { + "residual": 3, + "noise_bound": 6, + "view": "sign", + "assume_zero": true, + "candidate_count": 6, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 3, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 20, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 3 + }, + { + "u": -5, + "n": 2 + }, + { + "u": -4, + "n": 1 + } + ] + }, + { + "residual": 3, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -3 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 4, + "noise_bound": 0, + "view": "exact", + "assume_zero": false, + "candidate_count": 1, + "presence": "entailed", + "identified_values": [ + 4 + ], + "first_candidates": [ + { + "u": 4, + "n": 0 + } + ] + }, + { + "residual": 4, + "noise_bound": 0, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 4, + "noise_bound": 0, + "view": "sign", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 1, + "n": 0 + }, + { + "u": 2, + "n": 0 + }, + { + "u": 3, + "n": 0 + } + ] + }, + { + "residual": 4, + "noise_bound": 0, + "view": "sign", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 4, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 2, + "presence": "entailed", + "identified_values": [ + -4, + 4 + ], + "first_candidates": [ + { + "u": -4, + "n": 0 + }, + { + "u": 4, + "n": 0 + } + ] + }, + { + "residual": 4, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 4, + "noise_bound": 1, + "view": "exact", + "assume_zero": false, + "candidate_count": 3, + "presence": "entailed", + "identified_values": [ + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": 3, + "n": 1 + }, + { + "u": 4, + "n": 0 + }, + { + "u": 5, + "n": -1 + } + ] + }, + { + "residual": 4, + "noise_bound": 1, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 4, + "noise_bound": 1, + "view": "sign", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 1, + "n": 0 + }, + { + "u": 1, + "n": 1 + } + ] + }, + { + "residual": 4, + "noise_bound": 1, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 4, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -5, + -4, + -3, + 3, + 4, + 5 + ], + "first_candidates": [ + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + }, + { + "u": -3, + "n": -1 + } + ] + }, + { + "residual": 4, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 4, + "noise_bound": 2, + "view": "exact", + "assume_zero": false, + "candidate_count": 5, + "presence": "entailed", + "identified_values": [ + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 2, + "n": 2 + }, + { + "u": 3, + "n": 1 + }, + { + "u": 4, + "n": 0 + } + ] + }, + { + "residual": 4, + "noise_bound": 2, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 4, + "noise_bound": 2, + "view": "sign", + "assume_zero": false, + "candidate_count": 30, + "presence": "unresolved", + "identified_values": [ + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -1, + "n": 2 + }, + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 4, + "noise_bound": 2, + "view": "sign", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 4, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 10, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 2 + }, + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": 4, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 4, + "noise_bound": 3, + "view": "exact", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 1, + "n": 3 + }, + { + "u": 2, + "n": 2 + }, + { + "u": 3, + "n": 1 + } + ] + }, + { + "residual": 4, + "noise_bound": 3, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 4, + "noise_bound": 3, + "view": "sign", + "assume_zero": false, + "candidate_count": 42, + "presence": "unresolved", + "identified_values": [ + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -2, + "n": 3 + }, + { + "u": -1, + "n": 2 + }, + { + "u": -1, + "n": 3 + } + ] + }, + { + "residual": 4, + "noise_bound": 3, + "view": "sign", + "assume_zero": true, + "candidate_count": 3, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 4, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 12, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 2 + }, + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": 4, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 4, + "noise_bound": 4, + "view": "exact", + "assume_zero": false, + "candidate_count": 7, + "presence": "unresolved", + "identified_values": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 0, + "n": 4 + }, + { + "u": 1, + "n": 3 + }, + { + "u": 2, + "n": 2 + } + ] + }, + { + "residual": 4, + "noise_bound": 4, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 4 + } + ] + }, + { + "residual": 4, + "noise_bound": 4, + "view": "sign", + "assume_zero": false, + "candidate_count": 54, + "presence": "unresolved", + "identified_values": [ + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -3, + "n": 4 + }, + { + "u": -2, + "n": 3 + }, + { + "u": -2, + "n": 4 + } + ] + }, + { + "residual": 4, + "noise_bound": 4, + "view": "sign", + "assume_zero": true, + "candidate_count": 4, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 4, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 14, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 2 + }, + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": 4, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": 4 + } + ] + }, + { + "residual": 4, + "noise_bound": 5, + "view": "exact", + "assume_zero": false, + "candidate_count": 8, + "presence": "unresolved", + "identified_values": [ + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -1, + "n": 5 + }, + { + "u": 0, + "n": 4 + }, + { + "u": 1, + "n": 3 + } + ] + }, + { + "residual": 4, + "noise_bound": 5, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 4 + } + ] + }, + { + "residual": 4, + "noise_bound": 5, + "view": "sign", + "assume_zero": false, + "candidate_count": 66, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -4, + "n": 5 + }, + { + "u": -3, + "n": 4 + }, + { + "u": -3, + "n": 5 + } + ] + }, + { + "residual": 4, + "noise_bound": 5, + "view": "sign", + "assume_zero": true, + "candidate_count": 5, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 4, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 16, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 2 + }, + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": 4, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": 4 + } + ] + }, + { + "residual": 4, + "noise_bound": 6, + "view": "exact", + "assume_zero": false, + "candidate_count": 9, + "presence": "unresolved", + "identified_values": [ + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -2, + "n": 6 + }, + { + "u": -1, + "n": 5 + }, + { + "u": 0, + "n": 4 + } + ] + }, + { + "residual": 4, + "noise_bound": 6, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 4 + } + ] + }, + { + "residual": 4, + "noise_bound": 6, + "view": "sign", + "assume_zero": false, + "candidate_count": 78, + "presence": "unresolved", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -5, + "n": 6 + }, + { + "u": -4, + "n": 5 + }, + { + "u": -4, + "n": 6 + } + ] + }, + { + "residual": 4, + "noise_bound": 6, + "view": "sign", + "assume_zero": true, + "candidate_count": 6, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 4, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 2 + }, + { + "u": -5, + "n": 1 + }, + { + "u": -4, + "n": 0 + } + ] + }, + { + "residual": 4, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -4 + }, + { + "u": 0, + "n": 4 + } + ] + }, + { + "residual": 5, + "noise_bound": 0, + "view": "exact", + "assume_zero": false, + "candidate_count": 1, + "presence": "entailed", + "identified_values": [ + 5 + ], + "first_candidates": [ + { + "u": 5, + "n": 0 + } + ] + }, + { + "residual": 5, + "noise_bound": 0, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 5, + "noise_bound": 0, + "view": "sign", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 1, + "n": 0 + }, + { + "u": 2, + "n": 0 + }, + { + "u": 3, + "n": 0 + } + ] + }, + { + "residual": 5, + "noise_bound": 0, + "view": "sign", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 5, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 2, + "presence": "entailed", + "identified_values": [ + -5, + 5 + ], + "first_candidates": [ + { + "u": -5, + "n": 0 + }, + { + "u": 5, + "n": 0 + } + ] + }, + { + "residual": 5, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 5, + "noise_bound": 1, + "view": "exact", + "assume_zero": false, + "candidate_count": 3, + "presence": "entailed", + "identified_values": [ + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 4, + "n": 1 + }, + { + "u": 5, + "n": 0 + }, + { + "u": 6, + "n": -1 + } + ] + }, + { + "residual": 5, + "noise_bound": 1, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 5, + "noise_bound": 1, + "view": "sign", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 1, + "n": 0 + }, + { + "u": 1, + "n": 1 + } + ] + }, + { + "residual": 5, + "noise_bound": 1, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 5, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": 5, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 5, + "noise_bound": 2, + "view": "exact", + "assume_zero": false, + "candidate_count": 4, + "presence": "entailed", + "identified_values": [ + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 3, + "n": 2 + }, + { + "u": 4, + "n": 1 + }, + { + "u": 5, + "n": 0 + } + ] + }, + { + "residual": 5, + "noise_bound": 2, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 5, + "noise_bound": 2, + "view": "sign", + "assume_zero": false, + "candidate_count": 30, + "presence": "unresolved", + "identified_values": [ + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -1, + "n": 2 + }, + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 5, + "noise_bound": 2, + "view": "sign", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 5, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 8, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": 5, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 5, + "noise_bound": 3, + "view": "exact", + "assume_zero": false, + "candidate_count": 5, + "presence": "entailed", + "identified_values": [ + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 2, + "n": 3 + }, + { + "u": 3, + "n": 2 + }, + { + "u": 4, + "n": 1 + } + ] + }, + { + "residual": 5, + "noise_bound": 3, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 5, + "noise_bound": 3, + "view": "sign", + "assume_zero": false, + "candidate_count": 42, + "presence": "unresolved", + "identified_values": [ + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -2, + "n": 3 + }, + { + "u": -1, + "n": 2 + }, + { + "u": -1, + "n": 3 + } + ] + }, + { + "residual": 5, + "noise_bound": 3, + "view": "sign", + "assume_zero": true, + "candidate_count": 3, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 5, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 10, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": 5, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 5, + "noise_bound": 4, + "view": "exact", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 1, + "n": 4 + }, + { + "u": 2, + "n": 3 + }, + { + "u": 3, + "n": 2 + } + ] + }, + { + "residual": 5, + "noise_bound": 4, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 5, + "noise_bound": 4, + "view": "sign", + "assume_zero": false, + "candidate_count": 54, + "presence": "unresolved", + "identified_values": [ + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -3, + "n": 4 + }, + { + "u": -2, + "n": 3 + }, + { + "u": -2, + "n": 4 + } + ] + }, + { + "residual": 5, + "noise_bound": 4, + "view": "sign", + "assume_zero": true, + "candidate_count": 4, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 5, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 12, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": 5, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 5, + "noise_bound": 5, + "view": "exact", + "assume_zero": false, + "candidate_count": 7, + "presence": "unresolved", + "identified_values": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 0, + "n": 5 + }, + { + "u": 1, + "n": 4 + }, + { + "u": 2, + "n": 3 + } + ] + }, + { + "residual": 5, + "noise_bound": 5, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 5 + } + ] + }, + { + "residual": 5, + "noise_bound": 5, + "view": "sign", + "assume_zero": false, + "candidate_count": 66, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -4, + "n": 5 + }, + { + "u": -3, + "n": 4 + }, + { + "u": -3, + "n": 5 + } + ] + }, + { + "residual": 5, + "noise_bound": 5, + "view": "sign", + "assume_zero": true, + "candidate_count": 5, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 5, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 14, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": 5, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -5 + }, + { + "u": 0, + "n": 5 + } + ] + }, + { + "residual": 5, + "noise_bound": 6, + "view": "exact", + "assume_zero": false, + "candidate_count": 8, + "presence": "unresolved", + "identified_values": [ + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -1, + "n": 6 + }, + { + "u": 0, + "n": 5 + }, + { + "u": 1, + "n": 4 + } + ] + }, + { + "residual": 5, + "noise_bound": 6, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 5 + } + ] + }, + { + "residual": 5, + "noise_bound": 6, + "view": "sign", + "assume_zero": false, + "candidate_count": 78, + "presence": "unresolved", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -5, + "n": 6 + }, + { + "u": -4, + "n": 5 + }, + { + "u": -4, + "n": 6 + } + ] + }, + { + "residual": 5, + "noise_bound": 6, + "view": "sign", + "assume_zero": true, + "candidate_count": 6, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 5, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 16, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 1 + }, + { + "u": -5, + "n": 0 + }, + { + "u": -4, + "n": -1 + } + ] + }, + { + "residual": 5, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -5 + }, + { + "u": 0, + "n": 5 + } + ] + }, + { + "residual": 6, + "noise_bound": 0, + "view": "exact", + "assume_zero": false, + "candidate_count": 1, + "presence": "entailed", + "identified_values": [ + 6 + ], + "first_candidates": [ + { + "u": 6, + "n": 0 + } + ] + }, + { + "residual": 6, + "noise_bound": 0, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 6, + "noise_bound": 0, + "view": "sign", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 1, + "n": 0 + }, + { + "u": 2, + "n": 0 + }, + { + "u": 3, + "n": 0 + } + ] + }, + { + "residual": 6, + "noise_bound": 0, + "view": "sign", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 6, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 2, + "presence": "entailed", + "identified_values": [ + -6, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": 6, + "n": 0 + } + ] + }, + { + "residual": 6, + "noise_bound": 0, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 6, + "noise_bound": 1, + "view": "exact", + "assume_zero": false, + "candidate_count": 2, + "presence": "entailed", + "identified_values": [ + 5, + 6 + ], + "first_candidates": [ + { + "u": 5, + "n": 1 + }, + { + "u": 6, + "n": 0 + } + ] + }, + { + "residual": 6, + "noise_bound": 1, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 6, + "noise_bound": 1, + "view": "sign", + "assume_zero": false, + "candidate_count": 18, + "presence": "unresolved", + "identified_values": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 1, + "n": 0 + }, + { + "u": 1, + "n": 1 + } + ] + }, + { + "residual": 6, + "noise_bound": 1, + "view": "sign", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + } + ] + }, + { + "residual": 6, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 4, + "presence": "entailed", + "identified_values": [ + -6, + -5, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": 5, + "n": 1 + } + ] + }, + { + "residual": 6, + "noise_bound": 1, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 6, + "noise_bound": 2, + "view": "exact", + "assume_zero": false, + "candidate_count": 3, + "presence": "entailed", + "identified_values": [ + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 4, + "n": 2 + }, + { + "u": 5, + "n": 1 + }, + { + "u": 6, + "n": 0 + } + ] + }, + { + "residual": 6, + "noise_bound": 2, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 6, + "noise_bound": 2, + "view": "sign", + "assume_zero": false, + "candidate_count": 30, + "presence": "unresolved", + "identified_values": [ + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -1, + "n": 2 + }, + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 6, + "noise_bound": 2, + "view": "sign", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + } + ] + }, + { + "residual": 6, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": -4, + "n": -2 + } + ] + }, + { + "residual": 6, + "noise_bound": 2, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 6, + "noise_bound": 3, + "view": "exact", + "assume_zero": false, + "candidate_count": 4, + "presence": "entailed", + "identified_values": [ + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 3, + "n": 3 + }, + { + "u": 4, + "n": 2 + }, + { + "u": 5, + "n": 1 + } + ] + }, + { + "residual": 6, + "noise_bound": 3, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 6, + "noise_bound": 3, + "view": "sign", + "assume_zero": false, + "candidate_count": 42, + "presence": "unresolved", + "identified_values": [ + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -2, + "n": 3 + }, + { + "u": -1, + "n": 2 + }, + { + "u": -1, + "n": 3 + } + ] + }, + { + "residual": 6, + "noise_bound": 3, + "view": "sign", + "assume_zero": true, + "candidate_count": 3, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 6, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 8, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": -4, + "n": -2 + } + ] + }, + { + "residual": 6, + "noise_bound": 3, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 6, + "noise_bound": 4, + "view": "exact", + "assume_zero": false, + "candidate_count": 5, + "presence": "entailed", + "identified_values": [ + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 2, + "n": 4 + }, + { + "u": 3, + "n": 3 + }, + { + "u": 4, + "n": 2 + } + ] + }, + { + "residual": 6, + "noise_bound": 4, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 6, + "noise_bound": 4, + "view": "sign", + "assume_zero": false, + "candidate_count": 54, + "presence": "unresolved", + "identified_values": [ + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -3, + "n": 4 + }, + { + "u": -2, + "n": 3 + }, + { + "u": -2, + "n": 4 + } + ] + }, + { + "residual": 6, + "noise_bound": 4, + "view": "sign", + "assume_zero": true, + "candidate_count": 4, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 6, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 10, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": -4, + "n": -2 + } + ] + }, + { + "residual": 6, + "noise_bound": 4, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 6, + "noise_bound": 5, + "view": "exact", + "assume_zero": false, + "candidate_count": 6, + "presence": "entailed", + "identified_values": [ + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 1, + "n": 5 + }, + { + "u": 2, + "n": 4 + }, + { + "u": 3, + "n": 3 + } + ] + }, + { + "residual": 6, + "noise_bound": 5, + "view": "exact", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 6, + "noise_bound": 5, + "view": "sign", + "assume_zero": false, + "candidate_count": 66, + "presence": "unresolved", + "identified_values": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -4, + "n": 5 + }, + { + "u": -3, + "n": 4 + }, + { + "u": -3, + "n": 5 + } + ] + }, + { + "residual": 6, + "noise_bound": 5, + "view": "sign", + "assume_zero": true, + "candidate_count": 5, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 6, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 12, + "presence": "entailed", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": -4, + "n": -2 + } + ] + }, + { + "residual": 6, + "noise_bound": 5, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 0, + "presence": "inconsistent", + "identified_values": [], + "first_candidates": [] + }, + { + "residual": 6, + "noise_bound": 6, + "view": "exact", + "assume_zero": false, + "candidate_count": 7, + "presence": "unresolved", + "identified_values": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": 0, + "n": 6 + }, + { + "u": 1, + "n": 5 + }, + { + "u": 2, + "n": 4 + } + ] + }, + { + "residual": 6, + "noise_bound": 6, + "view": "exact", + "assume_zero": true, + "candidate_count": 1, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 6 + } + ] + }, + { + "residual": 6, + "noise_bound": 6, + "view": "sign", + "assume_zero": false, + "candidate_count": 78, + "presence": "unresolved", + "identified_values": [ + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -5, + "n": 6 + }, + { + "u": -4, + "n": 5 + }, + { + "u": -4, + "n": 6 + } + ] + }, + { + "residual": 6, + "noise_bound": 6, + "view": "sign", + "assume_zero": true, + "candidate_count": 6, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": 1 + }, + { + "u": 0, + "n": 2 + }, + { + "u": 0, + "n": 3 + } + ] + }, + { + "residual": 6, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": false, + "candidate_count": 14, + "presence": "unresolved", + "identified_values": [ + -6, + -5, + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "first_candidates": [ + { + "u": -6, + "n": 0 + }, + { + "u": -5, + "n": -1 + }, + { + "u": -4, + "n": -2 + } + ] + }, + { + "residual": 6, + "noise_bound": 6, + "view": "magnitude", + "assume_zero": true, + "candidate_count": 2, + "presence": "refuted", + "identified_values": [ + 0 + ], + "first_candidates": [ + { + "u": 0, + "n": -6 + }, + { + "u": 0, + "n": 6 + } + ] + } + ] +} diff --git a/scripts/gen_evidence_vectors.py b/scripts/gen_evidence_vectors.py new file mode 100644 index 0000000..7e04410 --- /dev/null +++ b/scripts/gen_evidence_vectors.py @@ -0,0 +1,129 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: AGPL-3.0-only +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# gen_evidence_vectors.py — regenerate the shared golden vectors for the +# Evidence Mode finite residual model (issue #7). +# +# The vectors are the single source of truth shared by three checkers: +# 1. the Agda proofs in proofs/ (decision procedures are *proved* correct +# against the Candidate semantics; representative vector cases are +# re-checked as executable Agda terms in MetaManifoldEvidence.Vectors) +# 2. the Julia backend tests (test/unit/test_evidence_mode.jl) +# 3. the frontend bun tests (frontend/tests/unit/evidence-model.test.ts) +# +# The semantics implemented here are copied EXACTLY from the reference +# finite explorer in hyperpolymath/residual-evidence-types +# (residual-evidence-explorer.html, model 'signed-integer-v1', MPL-2.0): +# +# LIMIT = 6; world = (u, n) with u, n integers in [-6, 6] +# views: exact = identity, sign = Math.sign, magnitude = Math.abs +# candidates = [(u, n) | |n| <= noise_bound, (not assume_zero or u == 0), +# observe(u + n) == observe(residual)] +# presence : entailed iff candidates nonempty and every candidate has u != 0 +# refuted iff candidates nonempty and every candidate has u == 0 +# unresolved iff both kinds remain +# inconsistent iff candidates empty +# identification: sorted unique u values over candidates; identified iff +# exactly one value, unidentified otherwise (inconsistent if empty) +# +# Output is deterministic (sorted keys, stable case order) so the committed +# JSON never churns: re-running this script must produce a byte-identical file. +# +# Usage: python3 scripts/gen_evidence_vectors.py [output-path] + +import json +import math +import sys +from pathlib import Path + +LIMIT = 6 + +VIEWS = { + "exact": lambda x: x, + "sign": lambda x: int(math.sign(x)) if False else (0 if x == 0 else (1 if x > 0 else -1)), + "magnitude": abs, +} + + +def make_case(residual, noise_bound, view, assume_zero): + """Reference semantics, ported line-for-line from the explorer.""" + if not (isinstance(residual, int) and abs(residual) <= LIMIT): + raise ValueError("residual must be an integer in [-6, 6]") + if not (isinstance(noise_bound, int) and 0 <= noise_bound <= LIMIT): + raise ValueError("noise_bound must be an integer in [0, 6]") + observe = VIEWS[view] + candidates = [] + for latent in range(-LIMIT, LIMIT + 1): + for noise in range(-LIMIT, LIMIT + 1): + if (abs(noise) <= noise_bound + and (not assume_zero or latent == 0) + and observe(latent + noise) == observe(residual)): + candidates.append({"u": latent, "n": noise}) + return candidates + + +def decide_presence(candidates): + """entailed / refuted / unresolved / inconsistent, with witnesses.""" + if not candidates: + return {"status": "inconsistent", "supporting": None, "counterexample": None} + supporting = next((w for w in candidates if w["u"] != 0), None) + counterexample = next((w for w in candidates if w["u"] == 0), None) + status = ("entailed" if counterexample is None + else "refuted" if supporting is None + else "unresolved") + return {"status": status, "supporting": supporting, "counterexample": counterexample} + + +def identify(candidates): + if not candidates: + return {"status": "inconsistent", "values": []} + values = sorted({w["u"] for w in candidates}) + return {"status": "identified" if len(values) == 1 else "unidentified", "values": values} + + +def main(): + out = Path(sys.argv[1] if len(sys.argv) > 1 else "proofs/vectors/evidence_vectors.json") + cases = [] + # Full factorial sweep: 13 residuals x 7 bounds x 3 views x 2 zero-assumptions. + for residual in range(-LIMIT, LIMIT + 1): + for bound in range(0, LIMIT + 1): + for view in ("exact", "sign", "magnitude"): + for assume_zero in (False, True): + cands = make_case(residual, bound, view, assume_zero) + case = { + "residual": residual, + "noise_bound": bound, + "view": view, + "assume_zero": assume_zero, + "candidate_count": len(cands), + "presence": decide_presence(cands)["status"], + "identified_values": identify(cands)["values"], + "first_candidates": cands[:3], + } + cases.append(case) + + doc = { + "model": "signed-integer-v1", + "limit": LIMIT, + "source": "hyperpolymath/residual-evidence-types residual-evidence-explorer.html", + "licence": "MPL-2.0", + "case_count": len(cases), + "presets": { + "ambiguous": {"residual": 2, "noise_bound": 6, "assume_zero": False, "view": "exact"}, + "present": {"residual": 2, "noise_bound": 1, "assume_zero": False, "view": "exact"}, + "exact": {"residual": 2, "noise_bound": 0, "assume_zero": False, "view": "exact"}, + "cancel": {"residual": 0, "noise_bound": 6, "assume_zero": False, "view": "exact"}, + "conflict": {"residual": 2, "noise_bound": 1, "assume_zero": True, "view": "exact"}, + }, + "cases": cases, + } + out.parent.mkdir(parents=True, exist_ok=True) + with open(out, "w", encoding="utf-8") as fh: + json.dump(doc, fh, indent=1, sort_keys=False) + fh.write("\n") + print(f"wrote {len(cases)} cases to {out}") + + +if __name__ == "__main__": + main()