Skip to content

Commit 4ba51c1

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 3: (Trit, and3) is a commutative idempotent meet-semilattice (#40)
## Summary Layer 3 (second, deeper invariant): proves `(Trit, and3)` is a **commutative, associative, idempotent meet-semilattice** whose induced order matches the Kleene truth order. Distinct from and deeper than the Layer-2 double-negation/De Morgan laws. New module `Betlangiser.ABI.Invariants` (imports the Layer-2 `Semantics` model). Positive + non-vacuity controls. ## Testing Idris2 0.7.0 `--build` → exit 0, zero warnings. Adversarial rejection confirmed. `build/` removed. No `believe_me`/`postulate`/`sorry`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- _Generated by [Claude Code](https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx)_ --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com>
1 parent 1f72b7e commit 4ba51c1

2 files changed

Lines changed: 271 additions & 0 deletions

File tree

‎src/interface/abi/Betlangiser/ABI/Invariants.idr‎

Lines changed: 270 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,270 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
--
4+
||| Deeper algebraic invariants for Betlangiser (Idris2 ABI Layer 3).
5+
|||
6+
||| Layer 2 (`Betlangiser.ABI.Semantics`) proved *unary/local* laws of the
7+
||| Kleene substrate `Trit = T | U | F`: that negation is an involution and
8+
||| that De Morgan relates `and3`/`or3`. This module proves a genuinely
9+
||| DEEPER and DISTINCT structural fact: that `(Trit, and3)` is a commutative,
10+
||| associative, idempotent semilattice whose order is exactly the Kleene
11+
||| information order `F <= U <= T`, and that `and3` is the *meet* (greatest
12+
||| lower bound) for that order. None of these restate the Layer-2 theorems.
13+
|||
14+
||| Contents:
15+
||| 1. `and3Comm` — commutativity of `and3` (9-case analysis);
16+
||| 2. `and3Assoc` — associativity of `and3` (full 27-case analysis);
17+
||| 3. `and3Idem` — idempotence (`and3 x x = x`);
18+
||| 4. `Leq3` — the Kleene order as an inductive relation, with a
19+
||| sound+complete decision procedure `decLeq3`;
20+
||| 5. `and3IsMeet` — `and3 x y` is a lower bound of both `x` and `y`,
21+
||| and the greatest such (meet / GLB);
22+
||| 6. positive controls (inhabited witnesses) AND a negative / non-vacuity
23+
||| control (`Not (...)`) machine-checked.
24+
25+
module Betlangiser.ABI.Invariants
26+
27+
import Betlangiser.ABI.Semantics
28+
29+
%default total
30+
31+
--------------------------------------------------------------------------------
32+
-- 1. Commutativity of and3 (distinct from Layer-2 doubleNeg / De Morgan)
33+
--------------------------------------------------------------------------------
34+
35+
||| `and3` is commutative.
36+
export
37+
and3Comm : (x, y : Trit) -> and3 x y = and3 y x
38+
and3Comm T T = Refl
39+
and3Comm T U = Refl
40+
and3Comm T F = Refl
41+
and3Comm U T = Refl
42+
and3Comm U U = Refl
43+
and3Comm U F = Refl
44+
and3Comm F T = Refl
45+
and3Comm F U = Refl
46+
and3Comm F F = Refl
47+
48+
--------------------------------------------------------------------------------
49+
-- 2. Associativity of and3 (the deep law — full 27-case analysis)
50+
--------------------------------------------------------------------------------
51+
52+
||| `and3` is associative. Proven by exhaustive case analysis on all three
53+
||| arguments; every case reduces definitionally to `Refl`.
54+
export
55+
and3Assoc : (x, y, z : Trit) -> and3 (and3 x y) z = and3 x (and3 y z)
56+
and3Assoc T T T = Refl
57+
and3Assoc T T U = Refl
58+
and3Assoc T T F = Refl
59+
and3Assoc T U T = Refl
60+
and3Assoc T U U = Refl
61+
and3Assoc T U F = Refl
62+
and3Assoc T F T = Refl
63+
and3Assoc T F U = Refl
64+
and3Assoc T F F = Refl
65+
and3Assoc U T T = Refl
66+
and3Assoc U T U = Refl
67+
and3Assoc U T F = Refl
68+
and3Assoc U U T = Refl
69+
and3Assoc U U U = Refl
70+
and3Assoc U U F = Refl
71+
and3Assoc U F T = Refl
72+
and3Assoc U F U = Refl
73+
and3Assoc U F F = Refl
74+
and3Assoc F T T = Refl
75+
and3Assoc F T U = Refl
76+
and3Assoc F T F = Refl
77+
and3Assoc F U T = Refl
78+
and3Assoc F U U = Refl
79+
and3Assoc F U F = Refl
80+
and3Assoc F F T = Refl
81+
and3Assoc F F U = Refl
82+
and3Assoc F F F = Refl
83+
84+
--------------------------------------------------------------------------------
85+
-- 3. Idempotence — completes the semilattice laws
86+
--------------------------------------------------------------------------------
87+
88+
||| `and3` is idempotent: `and3 x x = x`.
89+
export
90+
and3Idem : (x : Trit) -> and3 x x = x
91+
and3Idem T = Refl
92+
and3Idem U = Refl
93+
and3Idem F = Refl
94+
95+
--------------------------------------------------------------------------------
96+
-- 4. The Kleene information order, decided soundly and completely
97+
--------------------------------------------------------------------------------
98+
99+
||| The Kleene/information order on `Trit`: `F <= U <= T`. Encoded as an
100+
||| inductive relation so that proofs are first-class. Reflexivity is built in
101+
||| per-constructor; the strict steps `LFU`, `LUT`, `LFT` give the chain.
102+
public export
103+
data Leq3 : Trit -> Trit -> Type where
104+
LFF : Leq3 F F
105+
LUU : Leq3 U U
106+
LTT : Leq3 T T
107+
LFU : Leq3 F U
108+
LUT : Leq3 U T
109+
LFT : Leq3 F T
110+
111+
||| Reflexivity of the order.
112+
export
113+
leq3Refl : (x : Trit) -> Leq3 x x
114+
leq3Refl T = LTT
115+
leq3Refl U = LUU
116+
leq3Refl F = LFF
117+
118+
||| Transitivity of the order (full case analysis on the witnesses).
119+
export
120+
leq3Trans : Leq3 x y -> Leq3 y z -> Leq3 x z
121+
leq3Trans LFF p = p
122+
leq3Trans LUU p = p
123+
leq3Trans LTT p = p
124+
leq3Trans LFU LUU = LFU
125+
leq3Trans LFU LUT = LFT
126+
leq3Trans LUT LTT = LUT
127+
leq3Trans LFT LTT = LFT
128+
129+
-- The genuinely impossible compositions are ruled out structurally: there is
130+
-- no `Leq3` constructor with U or T on the left that lands below it, so the
131+
-- clauses above are exhaustive for total checking.
132+
133+
-- Refutations needed for a complete decision procedure (top-level `impossible`
134+
-- clauses, per the 0.7.0 idiom — NOT nested case-impossible).
135+
notLeqUF : Leq3 U F -> Void
136+
notLeqUF LFF impossible
137+
notLeqUF LUU impossible
138+
notLeqUF LTT impossible
139+
notLeqUF LFU impossible
140+
notLeqUF LUT impossible
141+
notLeqUF LFT impossible
142+
143+
notLeqTF : Leq3 T F -> Void
144+
notLeqTF LFF impossible
145+
notLeqTF LUU impossible
146+
notLeqTF LTT impossible
147+
notLeqTF LFU impossible
148+
notLeqTF LUT impossible
149+
notLeqTF LFT impossible
150+
151+
notLeqTU : Leq3 T U -> Void
152+
notLeqTU LFF impossible
153+
notLeqTU LUU impossible
154+
notLeqTU LTT impossible
155+
notLeqTU LFU impossible
156+
notLeqTU LUT impossible
157+
notLeqTU LFT impossible
158+
159+
||| Sound + complete decision of the Kleene order. `Yes` returns a real proof;
160+
||| `No` returns a real refutation — there is no `believe_me`/`postulate`.
161+
public export
162+
decLeq3 : (x, y : Trit) -> Dec (Leq3 x y)
163+
decLeq3 F F = Yes LFF
164+
decLeq3 F U = Yes LFU
165+
decLeq3 F T = Yes LFT
166+
decLeq3 U F = No notLeqUF
167+
decLeq3 U U = Yes LUU
168+
decLeq3 U T = Yes LUT
169+
decLeq3 T F = No notLeqTF
170+
decLeq3 T U = No notLeqTU
171+
decLeq3 T T = Yes LTT
172+
173+
--------------------------------------------------------------------------------
174+
-- 5. and3 is the MEET (greatest lower bound) for Leq3
175+
--------------------------------------------------------------------------------
176+
177+
||| Lower-bound part: `and3 x y` is below `x`.
178+
export
179+
and3LowerL : (x, y : Trit) -> Leq3 (and3 x y) x
180+
and3LowerL T T = LTT
181+
and3LowerL T U = LUT
182+
and3LowerL T F = LFT
183+
and3LowerL U T = LUU
184+
and3LowerL U U = LUU
185+
and3LowerL U F = LFU
186+
and3LowerL F T = LFF
187+
and3LowerL F U = LFF
188+
and3LowerL F F = LFF
189+
190+
||| Lower-bound part: `and3 x y` is below `y`.
191+
export
192+
and3LowerR : (x, y : Trit) -> Leq3 (and3 x y) y
193+
and3LowerR T T = LTT
194+
and3LowerR T U = LUU
195+
and3LowerR T F = LFF
196+
and3LowerR U T = LUT
197+
and3LowerR U U = LUU
198+
and3LowerR U F = LFF
199+
and3LowerR F T = LFT
200+
and3LowerR F U = LFU
201+
and3LowerR F F = LFF
202+
203+
||| Greatest part: any common lower bound `z` of `x` and `y` is below the meet
204+
||| `and3 x y`. Together with `and3LowerL`/`and3LowerR` this proves `and3` is
205+
||| the greatest lower bound (meet) for the Kleene order.
206+
export
207+
and3Greatest : (x, y, z : Trit) ->
208+
Leq3 z x -> Leq3 z y -> Leq3 z (and3 x y)
209+
-- For each (x,y), `and3 x y` is fixed and the goal is `Leq3 z (and3 x y)`.
210+
-- Where z cannot be a common lower bound of x and y, one of the supplied
211+
-- witnesses is uninhabited and we refute it.
212+
and3Greatest T T z zx zy = zx -- and3 T T = T, goal Leq3 z T = zx
213+
and3Greatest T U z zx zy = zy -- and3 T U = U, goal Leq3 z U = zy
214+
and3Greatest T F z zx zy = zy -- and3 T F = F, goal Leq3 z F = zy
215+
and3Greatest U T z zx zy = zx -- and3 U T = U, goal Leq3 z U = zx
216+
and3Greatest U U z zx zy = zx -- and3 U U = U, goal Leq3 z U = zx
217+
and3Greatest U F z zx zy = zy -- and3 U F = F, goal Leq3 z F = zy
218+
and3Greatest F T z zx zy = zx -- and3 F T = F, goal Leq3 z F = zx
219+
and3Greatest F U z zx zy = zx -- and3 F U = F, goal Leq3 z F = zx
220+
and3Greatest F F z zx zy = zx -- and3 F F = F, goal Leq3 z F = zx
221+
222+
--------------------------------------------------------------------------------
223+
-- 6. Positive controls (inhabited witnesses / concrete instances)
224+
--------------------------------------------------------------------------------
225+
226+
||| Concrete instance of associativity at a mixed point.
227+
export
228+
assocUTF : and3 (and3 U T) F = and3 U (and3 T F)
229+
assocUTF = and3Assoc U T F
230+
231+
||| Concrete order fact: `U` sits between `F` and `T`.
232+
export
233+
fLeqU : Leq3 F U
234+
fLeqU = LFU
235+
236+
||| The decision procedure accepts a true ordering.
237+
export
238+
decAcceptsFU : (Leq3 F U)
239+
decAcceptsFU = case decLeq3 F U of
240+
Yes p => p
241+
No contra => absurd (contra LFU)
242+
243+
||| Meet of `T` and `U` is `U`, and it is genuinely below both — a witnessed
244+
||| greatest-lower-bound instance.
245+
export
246+
meetTU_belowU : Leq3 (and3 T U) U
247+
meetTU_belowU = and3LowerR T U
248+
249+
--------------------------------------------------------------------------------
250+
-- 7. Negative / non-vacuity controls (machine-checked refutations)
251+
--------------------------------------------------------------------------------
252+
253+
||| The order is genuinely a *partial* order, not total agreement: `T` is NOT
254+
||| below `U`. If this were provable, `decLeq3` would be unsound.
255+
export
256+
tNotLeqU : Not (Leq3 T U)
257+
tNotLeqU = notLeqTU
258+
259+
||| `and3` is genuinely not constant: associativity is non-vacuous because the
260+
||| values it relates actually differ from a fixed value. Here `and3 U U = U`,
261+
||| which is NOT `T`, so the semilattice is not collapsed to the top.
262+
export
263+
andUUNotTop : Not (and3 U U = T)
264+
andUUNotTop Refl impossible
265+
266+
||| The meet genuinely loses information: `and3 T F = F`, which is strictly
267+
||| below `T`; it is NOT the case that `T` is below the meet `and3 T F`.
268+
export
269+
topNotBelowMeetTF : Not (Leq3 T (and3 T F))
270+
topNotBelowMeetTF = notLeqTF

‎src/interface/abi/betlangiser-abi.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,4 @@ modules = Betlangiser.ABI.Types
88
, Betlangiser.ABI.Foreign
99
, Betlangiser.ABI.Proofs
1010
, Betlangiser.ABI.Semantics
11+
, Betlangiser.ABI.Invariants

0 commit comments

Comments
 (0)