sre/track2i: Phase 4 — relation-aware join in distributive/SD checks

racket/prologos/sre-core.rkt

@@ -285,9 +285,13 @@
 (define axiom-untested 'axiom-untested)
 
 ;; Test commutativity of join: a ⊔ b = b ⊔ a
-(define (test-commutative-join domain samples)
+;;
+;; SRE Track 2I Phase 4 (2026-05-06): #:relation selects the join from
+;; merge-registry so axioms inferred under a non-equality relation stay
+;; in that relation's lattice. Default 'equality preserves prior callers.
+(define (test-commutative-join domain samples #:relation [relation 'equality])
   (define merge-fn (sre-domain-merge-registry domain))
-  (define join (merge-fn 'equality))  ;; equality merge = lattice join
+  (define join (merge-fn relation))  ;; merge under the requested relation
   (for/fold ([status (axiom-confirmed 0)])
             ([i (in-range (length samples))]
              [a (in-list samples)]
@@ -300,8 +304,8 @@
           (axiom-refuted (list a b))))))
 
 ;; Test associativity of join: (a ⊔ b) ⊔ c = a ⊔ (b ⊔ c)
-(define (test-associative-join domain samples)
-  (define join ((sre-domain-merge-registry domain) 'equality))
+(define (test-associative-join domain samples #:relation [relation 'equality])
+  (define join ((sre-domain-merge-registry domain) relation))
   (for/fold ([status (axiom-confirmed 0)])
             ([a (in-list samples)]
              #:break (axiom-refuted? status))
@@ -316,8 +320,8 @@
             (axiom-refuted (list a b c)))))))
 
 ;; Test idempotence of join: a ⊔ a = a
-(define (test-idempotent-join domain samples)
-  (define join ((sre-domain-merge-registry domain) 'equality))
+(define (test-idempotent-join domain samples #:relation [relation 'equality])
+  (define join ((sre-domain-merge-registry domain) relation))
   (for/fold ([status (axiom-confirmed 0)])
             ([a (in-list samples)]
              #:break (axiom-refuted? status))
@@ -327,10 +331,15 @@
 
 ;; Test distributivity: a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c)
 ;; Requires meet-fn. Returns axiom-untested if no meet available.
-(define (test-distributive domain samples meet-fn)
+;;
+;; SRE Track 2I Phase 4 (2026-05-06): the relation keyword selects the
+;; matching join from the merge-registry so the check stays inside ONE
+;; lattice. Without it, a subtype-meet was paired with the equality-join,
+;; mixing lattices and refuting distributivity for purely structural reasons.
+(define (test-distributive domain samples meet-fn #:relation [relation 'equality])
   (if (not meet-fn)
       axiom-untested
-      (let ([join ((sre-domain-merge-registry domain) 'equality)])
+      (let ([join ((sre-domain-merge-registry domain) relation)])
         (for/fold ([status (axiom-confirmed 0)])
                   ([a (in-list samples)]
                    #:break (axiom-refuted? status))
@@ -391,11 +400,14 @@
   #:transparent)
 
 ;; Detailed SD∨: a ⊔ b = a ⊔ c ⇒ a ⊔ b = a ⊔ (b ⊓ c)
-(define (test-sd-vee/detailed domain samples meet-fn)
+;;
+;; SRE Track 2I Phase 4 (2026-05-06): #:relation selects the matching join
+;; so the SD check stays inside one lattice. See test-distributive.
+(define (test-sd-vee/detailed domain samples meet-fn #:relation [relation 'equality])
   (cond
     [(not meet-fn) (sd-evidence 'untested 0 0 0 #f)]
     [else
-     (define join ((sre-domain-merge-registry domain) 'equality))
+     (define join ((sre-domain-merge-registry domain) relation))
      (let/ec return
        (define-values (total fired held)
          (for*/fold ([t 0] [f 0] [h 0])
@@ -421,11 +433,14 @@
        (sd-evidence 'confirmed total fired held #f))]))
 
 ;; Detailed SD∧ (dual): a ⊓ b = a ⊓ c ⇒ a ⊓ b = a ⊓ (b ⊔ c)
-(define (test-sd-wedge/detailed domain samples meet-fn)
+;;
+;; SRE Track 2I Phase 4 (2026-05-06): #:relation selects the matching join,
+;; mirroring test-sd-vee/detailed.
+(define (test-sd-wedge/detailed domain samples meet-fn #:relation [relation 'equality])
   (cond
     [(not meet-fn) (sd-evidence 'untested 0 0 0 #f)]
     [else
-     (define join ((sre-domain-merge-registry domain) 'equality))
+     (define join ((sre-domain-merge-registry domain) relation))
      (let/ec return
        (define-values (total fired held)
          (for*/fold ([t 0] [f 0] [h 0])
@@ -454,16 +469,16 @@
 ;; ------------------------------------------------------------------------
 
 ;; Test SD∨: a ⊔ b = a ⊔ c ⇒ a ⊔ b = a ⊔ (b ⊓ c)
-(define (test-sd-vee domain samples meet-fn)
-  (define ev (test-sd-vee/detailed domain samples meet-fn))
+(define (test-sd-vee domain samples meet-fn #:relation [relation 'equality])
+  (define ev (test-sd-vee/detailed domain samples meet-fn #:relation relation))
   (case (sd-evidence-status ev)
     [(confirmed) (axiom-confirmed (sd-evidence-total-checked ev))]
     [(refuted)   (axiom-refuted (sd-evidence-witness ev))]
     [(untested)  axiom-untested]))
 
 ;; Test SD∧ (dual of SD∨): a ⊓ b = a ⊓ c ⇒ a ⊓ b = a ⊓ (b ⊔ c)
-(define (test-sd-wedge domain samples meet-fn)
-  (define ev (test-sd-wedge/detailed domain samples meet-fn))
+(define (test-sd-wedge domain samples meet-fn #:relation [relation 'equality])
+  (define ev (test-sd-wedge/detailed domain samples meet-fn #:relation relation))
   (case (sd-evidence-status ev)
     [(confirmed) (axiom-confirmed (sd-evidence-total-checked ev))]
     [(refuted)   (axiom-refuted (sd-evidence-witness ev))]
@@ -491,28 +506,34 @@
 
   (define props-0
     (update-property declared 'commutative-join
-                     (test-commutative-join domain samples)))
+                     (test-commutative-join domain samples
+                                            #:relation relation-name)))
   (define props-1
     (update-property props-0 'associative-join
-                     (test-associative-join domain samples)))
+                     (test-associative-join domain samples
+                                            #:relation relation-name)))
   (define props-2
     (update-property props-1 'idempotent-join
-                     (test-idempotent-join domain samples)))
+                     (test-idempotent-join domain samples
+                                           #:relation relation-name)))
   (define props-3
     (if meet-fn
         (update-property props-2 'distributive
-                         (test-distributive domain samples meet-fn))
+                         (test-distributive domain samples meet-fn
+                                            #:relation relation-name))
         props-2))
   ;; Track 2I: SD∨ and SD∧ (require meet-fn; otherwise untested)
   (define props-4
     (if meet-fn
         (update-property props-3 'sd-vee
-                         (test-sd-vee domain samples meet-fn))
+                         (test-sd-vee domain samples meet-fn
+                                      #:relation relation-name))
         props-3))
   (define props-5
     (if meet-fn
         (update-property props-4 'sd-wedge
-                         (test-sd-wedge domain samples meet-fn))
+                         (test-sd-wedge domain samples meet-fn
+                                        #:relation relation-name))
         props-4))
   props-5)
 

racket/prologos/sre-property-sweep.rkt

@@ -91,11 +91,11 @@
            (define meet-fn (sre-domain-meet domain rel))
            (list
              (sd-finding domain-name rel 'distributive sample-count
-                         (test-distributive domain samples meet-fn))
+                         (test-distributive domain samples meet-fn #:relation rel))
              (sd-finding domain-name rel 'sd-vee sample-count
-                         (test-sd-vee/detailed domain samples meet-fn))
+                         (test-sd-vee/detailed domain samples meet-fn #:relation rel))
              (sd-finding domain-name rel 'sd-wedge sample-count
-                         (test-sd-wedge/detailed domain samples meet-fn))))))
+                         (test-sd-wedge/detailed domain samples meet-fn #:relation rel))))))
 
 ;; ========================================================================
 ;; format-sd-findings

racket/prologos/tests/test-sre-algebraic.rkt

@@ -127,6 +127,35 @@
   (define result (test-idempotent-join td type-samples))
   (check-true (axiom-confirmed? result)))
 
+;; ----------------------------------------------------------------------
+;; Phase 4 (2026-05-06): join-axiom tests under #:relation 'subtype.
+;;
+;; The three join-axiom tests gained a #:relation keyword so that a caller
+;; like `infer-domain-properties` can compute axioms in the relation's own
+;; lattice. These tests lock in the contract that the keyword routes to the
+;; subtype-merge from the domain's merge-registry; a regression that
+;; reintroduced hardcoded 'equality would still pass for these samples
+;; because the subtype merge happens to also be commutative/associative/
+;; idempotent on this set, but the explicit subtype assertion documents
+;; the behavior the review surfaced.
+;; ----------------------------------------------------------------------
+
+(test-case "inference: commutative-join confirmed for type domain under #:relation 'subtype"
+  (define td (lookup-domain 'type))
+  (define result (test-commutative-join td type-samples #:relation 'subtype))
+  (check-true (axiom-confirmed? result))
+  (check-true (> (axiom-confirmed-count result) 0)))
+
+(test-case "inference: associative-join confirmed for type domain under #:relation 'subtype"
+  (define td (lookup-domain 'type))
+  (define result (test-associative-join td type-samples #:relation 'subtype))
+  (check-true (axiom-confirmed? result)))
+
+(test-case "inference: idempotent-join confirmed for type domain under #:relation 'subtype"
+  (define td (lookup-domain 'type))
+  (define result (test-idempotent-join td type-samples #:relation 'subtype))
+  (check-true (axiom-confirmed? result)))
+
 (test-case "inference: distributive CONFIRMED for type domain (post-Phase-3c)"
   ;; HISTORY: Pre-Phase-3c (Track 2I, 2026-04-30) this test asserted REFUTED.
   ;; That finding was an artifact of `current-lattice-subtype-fn` being installed

racket/prologos/tests/test-sre-sd-properties.rkt

@@ -91,8 +91,8 @@
   (for ([f (in-list phase3-findings)])
     (check-true (sd-finding? f))
     (check-eq? (sd-finding-domain-name f) 'type)
-    (check-true (memq (sd-finding-relation f) '(equality subtype)))
-    (check-true (memq (sd-finding-property f) '(distributive sd-vee sd-wedge)))
+    (check-not-false (memq (sd-finding-relation f) '(equality subtype)))
+    (check-not-false (memq (sd-finding-property f) '(distributive sd-vee sd-wedge)))
     (check-true (positive? (sd-finding-sample-count f)))))
 
 (test-case "Phase 3: distributive findings carry axiom-*; SD findings carry sd-evidence"
@@ -168,3 +168,31 @@
       (check-true (positive? total))
       (check-true (<= 0 fired total))
       (check-true (<= 0 held fired)))))
+
+;; ============================================================================
+;; Phase 4 (2026-05-06): infer-domain-properties end-to-end under 'subtype
+;; ============================================================================
+;; Integration regression for the lattice-mixing bug PR #59 review surfaced.
+;; `infer-domain-properties` is parametrised on #:relation; after Phase 4 it
+;; threads that through to all six axiom tests. With #:relation 'subtype +
+;; the subtype-aware meet, every axiom should resolve to prop-confirmed for
+;; the type domain (Track 2H declared subtype distributive +
+;; has-pseudo-complement → distributive ⇒ SD∨ ∧ SD∧).
+;;
+;; If a future change reintroduces a hardcoded 'equality join lookup in any
+;; of the eight functions involved, this test will refute the corresponding
+;; property under subtype while leaving the equality-only suites green.
+
+(define subtype-meet-fn
+  (sre-domain-meet type-domain-for-sweep 'subtype))
+
+(test-case "Phase 4: infer-domain-properties under #:relation 'subtype confirms all axioms"
+  (define props
+    (infer-domain-properties type-domain-for-sweep
+                             realistic-type-atoms
+                             #:meet-fn subtype-meet-fn
+                             #:relation 'subtype))
+  (for ([axiom (in-list '(commutative-join associative-join idempotent-join
+                          distributive sd-vee sd-wedge))])
+    (check-eq? (hash-ref props axiom) prop-confirmed
+               (format "type domain × subtype: ~a should be prop-confirmed" axiom))))