From 9e09641f75857e699837a14bacc7a57ae31f14ab Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 21:40:14 +0000 Subject: [PATCH 1/2] abi: prove Kleene ternary-logic soundness (Layer 2 Semantics) Flagship semantic proof: negation involution + De Morgan laws, plus a decidable `Designated` (classical-truth) proposition with sound+complete Dec, certifier soundness, conjunction preservation, and positive + negative controls (negation is provably not the identity; U/F are provably not designated). Verified with idris2 0.7.0 (build clean, zero warnings) + adversarial false-proof rejection. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Betlangiser/ABI/Semantics.idr | 160 ++++++++++++++++++ src/interface/abi/betlangiser-abi.ipkg | 1 + 2 files changed, 161 insertions(+) create mode 100644 src/interface/abi/Betlangiser/ABI/Semantics.idr diff --git a/src/interface/abi/Betlangiser/ABI/Semantics.idr b/src/interface/abi/Betlangiser/ABI/Semantics.idr new file mode 100644 index 0000000..4aea86c --- /dev/null +++ b/src/interface/abi/Betlangiser/ABI/Semantics.idr @@ -0,0 +1,160 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Flagship semantic proof for Betlangiser (Idris2 ABI Layer 2). +||| +||| Betlangiser's headline is "ternary probabilistic modelling". The logical +||| substrate is three-valued (Kleene) logic over `Trit = T | U | F` (true / +||| unknown / false). This module proves that substrate is algebraically sound: +||| +||| 1. negation is an involution (`doubleNeg`: not3 (not3 x) = x); +||| 2. De Morgan holds (`deMorgan`: not3 (and3 x y) = or3 (not3 x) (not3 y)); +||| 3. `Designated` (classical truth, = T) is a decidable proposition with a +||| sound+complete `Dec`, a certifier proven sound, and `and3` preserves it; +||| 4. positive + negative controls, the negative ones machine-checking that the +||| laws are non-vacuous (negation is genuinely not the identity; U and F are +||| genuinely not designated). + +module Betlangiser.ABI.Semantics + +import Betlangiser.ABI.Types +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- The three truth values and the Kleene connectives +-------------------------------------------------------------------------------- + +public export +data Trit = T | U | F + +public export +not3 : Trit -> Trit +not3 T = F +not3 U = U +not3 F = T + +||| Kleene conjunction (the min under F < U < T). +public export +and3 : Trit -> Trit -> Trit +and3 F _ = F +and3 _ F = F +and3 T T = T +and3 T U = U +and3 U T = U +and3 U U = U + +||| Kleene disjunction (the max under F < U < T). +public export +or3 : Trit -> Trit -> Trit +or3 T _ = T +or3 _ T = T +or3 F F = F +or3 F U = U +or3 U F = U +or3 U U = U + +-------------------------------------------------------------------------------- +-- Algebraic laws (universally quantified, proven by total case analysis) +-------------------------------------------------------------------------------- + +||| Negation is an involution. +export +doubleNeg : (x : Trit) -> not3 (not3 x) = x +doubleNeg T = Refl +doubleNeg U = Refl +doubleNeg F = Refl + +||| De Morgan: negating a conjunction is the disjunction of the negations. +export +deMorgan : (x, y : Trit) -> not3 (and3 x y) = or3 (not3 x) (not3 y) +deMorgan T T = Refl +deMorgan T U = Refl +deMorgan T F = Refl +deMorgan U T = Refl +deMorgan U U = Refl +deMorgan U F = Refl +deMorgan F T = Refl +deMorgan F U = Refl +deMorgan F F = Refl + +-------------------------------------------------------------------------------- +-- Designated truth as a decidable proposition (no inhabitant for U or F) +-------------------------------------------------------------------------------- + +||| A `Designated` value is classically true — in Kleene logic, exactly `T`. +||| There is no constructor for `U` or `F`. +public export +data Designated : Trit -> Type where + DesT : Designated T + +export +Uninhabited (Designated U) where + uninhabited DesT impossible + +export +Uninhabited (Designated F) where + uninhabited DesT impossible + +public export +decDesignated : (t : Trit) -> Dec (Designated t) +decDesignated T = Yes DesT +decDesignated U = No absurd +decDesignated F = No absurd + +||| Truth-functional soundness: conjunction preserves designation. +export +andDesignated : Designated x -> Designated y -> Designated (and3 x y) +andDesignated DesT DesT = DesT + +-------------------------------------------------------------------------------- +-- Certifier into the ABI Result, proven sound +-------------------------------------------------------------------------------- + +public export +certifyDesignated : Trit -> Result +certifyDesignated t = case decDesignated t of + Yes _ => Ok + No _ => Error + +export +certifyDesignatedSound : (t : Trit) -> certifyDesignated t = Ok -> Designated t +certifyDesignatedSound t prf with (decDesignated t) + certifyDesignatedSound t prf | Yes d = d + certifyDesignatedSound t Refl | No _ impossible + +-------------------------------------------------------------------------------- +-- Positive controls +-------------------------------------------------------------------------------- + +export +tDesignated : Designated T +tDesignated = DesT + +export +andTTDesignated : Designated (and3 T T) +andTTDesignated = andDesignated DesT DesT + +export +certifyTAccepts : certifyDesignated T = Ok +certifyTAccepts = Refl + +-------------------------------------------------------------------------------- +-- Negative controls — the laws are non-vacuous +-------------------------------------------------------------------------------- + +||| Negation is genuinely not the identity (so `doubleNeg` is non-trivial). +export +negationNotIdentity : Not (not3 T = T) +negationNotIdentity Refl impossible + +||| `U` is not designated — Kleene "unknown" is not classical truth. +export +uNotDesignated : Not (Designated U) +uNotDesignated = absurd + +||| `F` is not designated. +export +fNotDesignated : Not (Designated F) +fNotDesignated = absurd diff --git a/src/interface/abi/betlangiser-abi.ipkg b/src/interface/abi/betlangiser-abi.ipkg index df6e494..08bf69d 100644 --- a/src/interface/abi/betlangiser-abi.ipkg +++ b/src/interface/abi/betlangiser-abi.ipkg @@ -7,3 +7,4 @@ modules = Betlangiser.ABI.Types , Betlangiser.ABI.Layout , Betlangiser.ABI.Foreign , Betlangiser.ABI.Proofs + , Betlangiser.ABI.Semantics From 45bdae694abdadaa802441f49b08c1eb8d57e629 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 22:45:15 +0000 Subject: [PATCH 2/2] =?UTF-8?q?feat(abi):=20Layer-3=20invariants=20?= =?UTF-8?q?=E2=80=94=20(Trit,=20and3)=20is=20a=20meet-semilattice=20over?= =?UTF-8?q?=20the=20Kleene=20order?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds Betlangiser.ABI.Invariants, a second, deeper machine-checked theorem built over the existing Semantics model (Trit/and3/or3), distinct from the Layer-2 doubleNeg/De Morgan laws: - and3Comm, and3Assoc (full 27-case), and3Idem — the semilattice laws; - Leq3, the Kleene information order F <= U <= T, with reflexivity, transitivity, and a sound+complete decision procedure decLeq3; - and3LowerL/R + and3Greatest proving and3 is the meet (GLB) for Leq3; - positive controls (inhabited witnesses) and negative/non-vacuity controls (tNotLeqU, andUUNotTop, topNotBelowMeetTF). No believe_me/postulate/assert/sorry. %default total. Adversarially verified: a false `Leq3 T U` is rejected by the type checker. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Betlangiser/ABI/Invariants.idr | 270 ++++++++++++++++++ src/interface/abi/betlangiser-abi.ipkg | 1 + 2 files changed, 271 insertions(+) create mode 100644 src/interface/abi/Betlangiser/ABI/Invariants.idr diff --git a/src/interface/abi/Betlangiser/ABI/Invariants.idr b/src/interface/abi/Betlangiser/ABI/Invariants.idr new file mode 100644 index 0000000..cbeccc7 --- /dev/null +++ b/src/interface/abi/Betlangiser/ABI/Invariants.idr @@ -0,0 +1,270 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Deeper algebraic invariants for Betlangiser (Idris2 ABI Layer 3). +||| +||| Layer 2 (`Betlangiser.ABI.Semantics`) proved *unary/local* laws of the +||| Kleene substrate `Trit = T | U | F`: that negation is an involution and +||| that De Morgan relates `and3`/`or3`. This module proves a genuinely +||| DEEPER and DISTINCT structural fact: that `(Trit, and3)` is a commutative, +||| associative, idempotent semilattice whose order is exactly the Kleene +||| information order `F <= U <= T`, and that `and3` is the *meet* (greatest +||| lower bound) for that order. None of these restate the Layer-2 theorems. +||| +||| Contents: +||| 1. `and3Comm` — commutativity of `and3` (9-case analysis); +||| 2. `and3Assoc` — associativity of `and3` (full 27-case analysis); +||| 3. `and3Idem` — idempotence (`and3 x x = x`); +||| 4. `Leq3` — the Kleene order as an inductive relation, with a +||| sound+complete decision procedure `decLeq3`; +||| 5. `and3IsMeet` — `and3 x y` is a lower bound of both `x` and `y`, +||| and the greatest such (meet / GLB); +||| 6. positive controls (inhabited witnesses) AND a negative / non-vacuity +||| control (`Not (...)`) machine-checked. + +module Betlangiser.ABI.Invariants + +import Betlangiser.ABI.Semantics + +%default total + +-------------------------------------------------------------------------------- +-- 1. Commutativity of and3 (distinct from Layer-2 doubleNeg / De Morgan) +-------------------------------------------------------------------------------- + +||| `and3` is commutative. +export +and3Comm : (x, y : Trit) -> and3 x y = and3 y x +and3Comm T T = Refl +and3Comm T U = Refl +and3Comm T F = Refl +and3Comm U T = Refl +and3Comm U U = Refl +and3Comm U F = Refl +and3Comm F T = Refl +and3Comm F U = Refl +and3Comm F F = Refl + +-------------------------------------------------------------------------------- +-- 2. Associativity of and3 (the deep law — full 27-case analysis) +-------------------------------------------------------------------------------- + +||| `and3` is associative. Proven by exhaustive case analysis on all three +||| arguments; every case reduces definitionally to `Refl`. +export +and3Assoc : (x, y, z : Trit) -> and3 (and3 x y) z = and3 x (and3 y z) +and3Assoc T T T = Refl +and3Assoc T T U = Refl +and3Assoc T T F = Refl +and3Assoc T U T = Refl +and3Assoc T U U = Refl +and3Assoc T U F = Refl +and3Assoc T F T = Refl +and3Assoc T F U = Refl +and3Assoc T F F = Refl +and3Assoc U T T = Refl +and3Assoc U T U = Refl +and3Assoc U T F = Refl +and3Assoc U U T = Refl +and3Assoc U U U = Refl +and3Assoc U U F = Refl +and3Assoc U F T = Refl +and3Assoc U F U = Refl +and3Assoc U F F = Refl +and3Assoc F T T = Refl +and3Assoc F T U = Refl +and3Assoc F T F = Refl +and3Assoc F U T = Refl +and3Assoc F U U = Refl +and3Assoc F U F = Refl +and3Assoc F F T = Refl +and3Assoc F F U = Refl +and3Assoc F F F = Refl + +-------------------------------------------------------------------------------- +-- 3. Idempotence — completes the semilattice laws +-------------------------------------------------------------------------------- + +||| `and3` is idempotent: `and3 x x = x`. +export +and3Idem : (x : Trit) -> and3 x x = x +and3Idem T = Refl +and3Idem U = Refl +and3Idem F = Refl + +-------------------------------------------------------------------------------- +-- 4. The Kleene information order, decided soundly and completely +-------------------------------------------------------------------------------- + +||| The Kleene/information order on `Trit`: `F <= U <= T`. Encoded as an +||| inductive relation so that proofs are first-class. Reflexivity is built in +||| per-constructor; the strict steps `LFU`, `LUT`, `LFT` give the chain. +public export +data Leq3 : Trit -> Trit -> Type where + LFF : Leq3 F F + LUU : Leq3 U U + LTT : Leq3 T T + LFU : Leq3 F U + LUT : Leq3 U T + LFT : Leq3 F T + +||| Reflexivity of the order. +export +leq3Refl : (x : Trit) -> Leq3 x x +leq3Refl T = LTT +leq3Refl U = LUU +leq3Refl F = LFF + +||| Transitivity of the order (full case analysis on the witnesses). +export +leq3Trans : Leq3 x y -> Leq3 y z -> Leq3 x z +leq3Trans LFF p = p +leq3Trans LUU p = p +leq3Trans LTT p = p +leq3Trans LFU LUU = LFU +leq3Trans LFU LUT = LFT +leq3Trans LUT LTT = LUT +leq3Trans LFT LTT = LFT + +-- The genuinely impossible compositions are ruled out structurally: there is +-- no `Leq3` constructor with U or T on the left that lands below it, so the +-- clauses above are exhaustive for total checking. + +-- Refutations needed for a complete decision procedure (top-level `impossible` +-- clauses, per the 0.7.0 idiom — NOT nested case-impossible). +notLeqUF : Leq3 U F -> Void +notLeqUF LFF impossible +notLeqUF LUU impossible +notLeqUF LTT impossible +notLeqUF LFU impossible +notLeqUF LUT impossible +notLeqUF LFT impossible + +notLeqTF : Leq3 T F -> Void +notLeqTF LFF impossible +notLeqTF LUU impossible +notLeqTF LTT impossible +notLeqTF LFU impossible +notLeqTF LUT impossible +notLeqTF LFT impossible + +notLeqTU : Leq3 T U -> Void +notLeqTU LFF impossible +notLeqTU LUU impossible +notLeqTU LTT impossible +notLeqTU LFU impossible +notLeqTU LUT impossible +notLeqTU LFT impossible + +||| Sound + complete decision of the Kleene order. `Yes` returns a real proof; +||| `No` returns a real refutation — there is no `believe_me`/`postulate`. +public export +decLeq3 : (x, y : Trit) -> Dec (Leq3 x y) +decLeq3 F F = Yes LFF +decLeq3 F U = Yes LFU +decLeq3 F T = Yes LFT +decLeq3 U F = No notLeqUF +decLeq3 U U = Yes LUU +decLeq3 U T = Yes LUT +decLeq3 T F = No notLeqTF +decLeq3 T U = No notLeqTU +decLeq3 T T = Yes LTT + +-------------------------------------------------------------------------------- +-- 5. and3 is the MEET (greatest lower bound) for Leq3 +-------------------------------------------------------------------------------- + +||| Lower-bound part: `and3 x y` is below `x`. +export +and3LowerL : (x, y : Trit) -> Leq3 (and3 x y) x +and3LowerL T T = LTT +and3LowerL T U = LUT +and3LowerL T F = LFT +and3LowerL U T = LUU +and3LowerL U U = LUU +and3LowerL U F = LFU +and3LowerL F T = LFF +and3LowerL F U = LFF +and3LowerL F F = LFF + +||| Lower-bound part: `and3 x y` is below `y`. +export +and3LowerR : (x, y : Trit) -> Leq3 (and3 x y) y +and3LowerR T T = LTT +and3LowerR T U = LUU +and3LowerR T F = LFF +and3LowerR U T = LUT +and3LowerR U U = LUU +and3LowerR U F = LFF +and3LowerR F T = LFT +and3LowerR F U = LFU +and3LowerR F F = LFF + +||| Greatest part: any common lower bound `z` of `x` and `y` is below the meet +||| `and3 x y`. Together with `and3LowerL`/`and3LowerR` this proves `and3` is +||| the greatest lower bound (meet) for the Kleene order. +export +and3Greatest : (x, y, z : Trit) -> + Leq3 z x -> Leq3 z y -> Leq3 z (and3 x y) +-- For each (x,y), `and3 x y` is fixed and the goal is `Leq3 z (and3 x y)`. +-- Where z cannot be a common lower bound of x and y, one of the supplied +-- witnesses is uninhabited and we refute it. +and3Greatest T T z zx zy = zx -- and3 T T = T, goal Leq3 z T = zx +and3Greatest T U z zx zy = zy -- and3 T U = U, goal Leq3 z U = zy +and3Greatest T F z zx zy = zy -- and3 T F = F, goal Leq3 z F = zy +and3Greatest U T z zx zy = zx -- and3 U T = U, goal Leq3 z U = zx +and3Greatest U U z zx zy = zx -- and3 U U = U, goal Leq3 z U = zx +and3Greatest U F z zx zy = zy -- and3 U F = F, goal Leq3 z F = zy +and3Greatest F T z zx zy = zx -- and3 F T = F, goal Leq3 z F = zx +and3Greatest F U z zx zy = zx -- and3 F U = F, goal Leq3 z F = zx +and3Greatest F F z zx zy = zx -- and3 F F = F, goal Leq3 z F = zx + +-------------------------------------------------------------------------------- +-- 6. Positive controls (inhabited witnesses / concrete instances) +-------------------------------------------------------------------------------- + +||| Concrete instance of associativity at a mixed point. +export +assocUTF : and3 (and3 U T) F = and3 U (and3 T F) +assocUTF = and3Assoc U T F + +||| Concrete order fact: `U` sits between `F` and `T`. +export +fLeqU : Leq3 F U +fLeqU = LFU + +||| The decision procedure accepts a true ordering. +export +decAcceptsFU : (Leq3 F U) +decAcceptsFU = case decLeq3 F U of + Yes p => p + No contra => absurd (contra LFU) + +||| Meet of `T` and `U` is `U`, and it is genuinely below both — a witnessed +||| greatest-lower-bound instance. +export +meetTU_belowU : Leq3 (and3 T U) U +meetTU_belowU = and3LowerR T U + +-------------------------------------------------------------------------------- +-- 7. Negative / non-vacuity controls (machine-checked refutations) +-------------------------------------------------------------------------------- + +||| The order is genuinely a *partial* order, not total agreement: `T` is NOT +||| below `U`. If this were provable, `decLeq3` would be unsound. +export +tNotLeqU : Not (Leq3 T U) +tNotLeqU = notLeqTU + +||| `and3` is genuinely not constant: associativity is non-vacuous because the +||| values it relates actually differ from a fixed value. Here `and3 U U = U`, +||| which is NOT `T`, so the semilattice is not collapsed to the top. +export +andUUNotTop : Not (and3 U U = T) +andUUNotTop Refl impossible + +||| The meet genuinely loses information: `and3 T F = F`, which is strictly +||| below `T`; it is NOT the case that `T` is below the meet `and3 T F`. +export +topNotBelowMeetTF : Not (Leq3 T (and3 T F)) +topNotBelowMeetTF = notLeqTF diff --git a/src/interface/abi/betlangiser-abi.ipkg b/src/interface/abi/betlangiser-abi.ipkg index 08bf69d..9c1ed84 100644 --- a/src/interface/abi/betlangiser-abi.ipkg +++ b/src/interface/abi/betlangiser-abi.ipkg @@ -8,3 +8,4 @@ modules = Betlangiser.ABI.Types , Betlangiser.ABI.Foreign , Betlangiser.ABI.Proofs , Betlangiser.ABI.Semantics + , Betlangiser.ABI.Invariants