From 3e7ef84088860581e77a30be5045869d15155cf0 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 26 Sep 2026 15:30:55 +0000 Subject: [PATCH 1/3] =?UTF-8?q?feat(proofs):=20evidence=20library=20?= =?UTF-8?q?=E2=80=94=20semantics,=20signed=20model,=20proved=20verdicts=20?= =?UTF-8?q?(#7)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary Lands the formal-foundations layer of Evidence Mode: what a residual, an evidence-refined candidate set, a warrant token and a presence verdict *are*, and a proof that the verdict computation the server routes and the residual explorer run decides exactly the candidate semantics. Closes the gap the reference explorer's own footer admits ("separately tested JavaScript, no proved extraction correspondence"). ## Changes - `MetaManifold/Evidence/{Prelude,Residual,Echo,Warrant,Signed,Decision}.agda` — L0 abstract semantics (Candidate fibres; Holds quantifies over ALL candidates; actual-world honesty; epi-does-not-give), L1 the signed finite model 'signed-integer-v1' as ℕ offsets with enumeration proved sound + complete, L2 verdicts computed and proved correct (entailed/refuted/unresolved/inconsistent), the five reference presets as computed proved terms. - `All.agda` imports the six new modules (CI reachability gate). - `reject/IdentificationWithoutUniqueness.agda` — negative control: reporting an identified value from a mere presence verdict must not type-check. - `README.md` — module table rows + stdlib-free note (Evidence.* uses only Agda.Builtin.*, so it checks under any Agda ≥ 2.6.4.3). ## Verification - All six modules type-check clean (Agda 2.7.0.1, --safe --without-K, exit 0, no output). - check-proofs.sh guard logic replicated on all 17 modules: no postulates/holes/escape flags; --safe --without-K pragma present. - reject control fails with `fst (fst c) != 8` as its EXPECT line states. - `scripts/check-spdx.sh`: OK. - Full All.agda run needs the estate toolchain (Agda 2.6.4.3 + stdlib 2.1); the Evidence half is stdlib-free by construction. Issue tracking: See also: #7 Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- proofs/agda/MetaManifold/All.agda | 9 + .../agda/MetaManifold/Evidence/Decision.agda | 407 ++++++++++++++++ proofs/agda/MetaManifold/Evidence/Echo.agda | 83 ++++ .../agda/MetaManifold/Evidence/Prelude.agda | 142 ++++++ .../agda/MetaManifold/Evidence/Residual.agda | 122 +++++ proofs/agda/MetaManifold/Evidence/Signed.agda | 433 ++++++++++++++++++ .../agda/MetaManifold/Evidence/Warrant.agda | 70 +++ proofs/agda/README.md | 14 +- .../IdentificationWithoutUniqueness.agda | 15 + 9 files changed, 1294 insertions(+), 1 deletion(-) create mode 100644 proofs/agda/MetaManifold/Evidence/Decision.agda create mode 100644 proofs/agda/MetaManifold/Evidence/Echo.agda create mode 100644 proofs/agda/MetaManifold/Evidence/Prelude.agda create mode 100644 proofs/agda/MetaManifold/Evidence/Residual.agda create mode 100644 proofs/agda/MetaManifold/Evidence/Signed.agda create mode 100644 proofs/agda/MetaManifold/Evidence/Warrant.agda create mode 100644 proofs/agda/reject/IdentificationWithoutUniqueness.agda 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 From 27396b3696b868b16fe60a4e480be75454a51957 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 26 Sep 2026 15:31:01 +0000 Subject: [PATCH 2/3] feat(evidence): golden vectors pinning the signed model (#7) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary 546 golden cases (13 residuals × 7 noise bounds × 3 views × 2 zero-assumptions) that pin the signed finite model's answers — candidate counts, presence verdicts, identified values — as data, so Agda, Julia and TypeScript can be bound to one truth instead of three agreeing-by-accident implementations. ## Changes - `scripts/gen_evidence_vectors.py` — the durable encoding of the explorer semantics (validation, candidate enumeration, decide, identify); regenerates the JSON byte-identically. - `proofs/vectors/evidence_vectors.json` — the generated pin; all four verdicts and both identification outcomes covered, plus the five reference presets. ## Verification - Regeneration diff: identical (546 cases). - Fields anchored in Decision.agda: candidate_count ↔ length, presence ↔ decide + the four theorems, identified_values ↔ values. Issue tracking: See also: #7 Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- proofs/vectors/evidence_vectors.json | 13135 +++++++++++++++++++++++++ scripts/gen_evidence_vectors.py | 129 + 2 files changed, 13264 insertions(+) create mode 100644 proofs/vectors/evidence_vectors.json create mode 100644 scripts/gen_evidence_vectors.py 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() From 99e5abb3123b5d886f92c0eb34564000604dbdc2 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 26 Sep 2026 15:31:01 +0000 Subject: [PATCH 3/3] docs(formal): evidence verification plan (#7) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Companion to verification-plan.md for the evidence library: the layer table (abstract semantics → signed finite model → decision procedures → implementation seam), the four verdict theorems, the golden-vector theorem-to-test map, and what is deliberately not proved (server/UI code, beyond-the-grid, funext, general extraction). Issue tracking: See also: #7 Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- docs/formal/evidence-verification.md | 104 +++++++++++++++++++++++++++ 1 file changed, 104 insertions(+) create mode 100644 docs/formal/evidence-verification.md 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.