Skip to content

Disposition doc for eigentrust pitfalls #8/#9/#10/#16 (observations)#7

Closed
kumavis wants to merge 2 commits into
mainfrom
claude/fix-eigentrust-observations-doc
Closed

Disposition doc for eigentrust pitfalls #8/#9/#10/#16 (observations)#7
kumavis wants to merge 2 commits into
mainfrom
claude/fix-eigentrust-observations-doc

Conversation

@kumavis
Copy link
Copy Markdown
Contributor

@kumavis kumavis commented Apr 25, 2026

Companion to the 2026-04-23 eigentrust pitfalls memo. The four items in this PR are observations (not Prologos defects) that should be tracked separately from the bug-fix PRs so a future reader does not double-count them as open work.

Coverage

Test plan

  • No code changes — pure docs PR
  • After this lands and the 2026-04-23 pitfalls memo lands, link this disposition doc from the memo's "Status" section

PR map across the pitfalls

Item PR Branch
#1 TBD TBD
#2 TBD TBD
#3 in flight claude/fix-eigentrust-pitfall-3-rl3z
#4 TBD TBD
#5 in flight claude/fix-eigentrust-pitfall-5-letm
#6 #4 (already landed-equivalent) claude/fix-eigentrust-pitfall-6-m5bE8
#7 TBD TBD
#8 this PR claude/fix-eigentrust-observations-doc
#9 this PR claude/fix-eigentrust-observations-doc
#10 this PR (subsumed by #3) claude/fix-eigentrust-observations-doc
#11 TBD TBD
#12 in flight claude/fix-eigentrust-pitfall-12-pv12
#13 #5 claude/fix-eigentrust-pitfall-13-pv13
#14 #6 claude/fix-eigentrust-pitfall-14-pp01
#15 in flight claude/fix-eigentrust-pitfall-15-mldef
#16 this PR claude/fix-eigentrust-observations-doc

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x


Generated by Claude Code

claude and others added 2 commits April 25, 2026 08:43
The 2026-04-23 eigentrust pitfalls memo (forthcoming branch) enumerated 16
items hit during the EigenTrust implementation. Items #1-7 and #11-15 are
language/elaboration defects with their own PRs. Items #8, #9, #10, and #16
are observations rather than Prologos defects; no compiler change is needed
for them but the memo deserves a parallel disposition note so a future reader
does not double-count them as open work.

#8 (exact-Rat slow on deep iter): intrinsic to exact rational arithmetic;
benchmark-scope guidance, not a fix.

#9 (Posit32 literals work): positive observation; `~` literal prefix is
unambiguous unlike `0/1`. No action.

#10 (PVec preserves where List does not): subsumed by pitfall #3 fix. After
#3 lands, both literal forms preserve element type uniformly. Close as
duplicate.

#16 (column-stochastic vs row-stochastic): algorithm/spec clarification, not
a Prologos defect. The eigentrust implementation branch already takes
column-stochastic M directly and validates via col-stochastic?.

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
Cherry-picked from PR #2 (commit f3a3ca3). The benchmark file references
the pre-D.5b TMS API (`tms-write`, `tms-cell-value`, `tms-read`,
`tms-commit`) which was removed when the TMS was refactored into the
`tms-cell` struct + `atms-write-cell` interface. The file is a
historical baseline-measurement artifact (Pre-0 micro-benchmark) that
does not run in CI or the regression suite, but `raco pkg install
--auto` compiles every .rkt in the collection, so its unbound-identifier
error fails the build.

Add `racket/prologos/benchmarks/micro/info.rkt` with
`compile-omit-paths '("bench-bsp-le-track2.rkt")` so `raco setup`
skips it. This is a minimal CI-unblock; the full migration to the
current TMS API is out of scope for this PR (same as f3a3ca3's scope).

Without this, PR #4 (and the other pitfall PRs branched from main) all
fail CI in the `raco pkg install` step.

https://claude.ai/code/session_01MbncYJnrvjzhbVWw4xGi5x

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
@kumavis
Copy link
Copy Markdown
Contributor Author

kumavis commented Apr 25, 2026

you can skip this one

@kumavis kumavis closed this Apr 25, 2026
kumavis added a commit that referenced this pull request Apr 26, 2026
…defn

Pre-fix: `defn f | cons r nil -> r | cons r rest -> ...` parsed each
bare token after `|` as a separate arg pattern, splitting the function
into clauses with mismatched arities (1 nil clause + 2 cons-3-arg
clauses). This produced a per-clause helper (`f::1`, `f::3`) and the
recursive call site `[f rest]` failed with `Unbound variable f::1`
because the arity-1 helper only knew the nil clause and any non-empty
list hit __match-fail.

Fix shape (a) — implement general pattern matrices by auto-packing
when the leading bare token names a known constructor whose field
count matches the remaining tokens. `cons r nil` → one compound
pattern `pat-compound 'cons (var-r, var-nil)` (then normalize-pattern
converts var-nil to compound-nil since nil is a known nullary ctor).

Fallback preserved for genuinely multi-arg defns:
  defn add | x y -> [+ x y]
The leading `x` is a variable (lookup-ctor returns #f), so falls
through to the old N-arg interpretation.

Trade-off vs (b) (raise an error): (a) makes the syntax do what
ML/Haskell users expect — `defn` IS the primary dispatch mechanism
per .claude/rules/prologos-syntax.md, so making `cons r nil` mean
"compound pattern" is the natural reading. The detection is local and
does not change semantics for any pattern that didn't have a known
ctor as its leading token.

Scope: 23 lines in parser.rkt's parse-defn-clause + 11 new tests in
test-defn-multiarg-patterns.rkt. No changes elsewhere.

Test results: 11/11 new tests pass. 43/43 related tests pass
(test-pattern-defn-01, test-pattern-defn-02, test-multi-body-defn).
Full affected-suite: 4646 tests in 255 files, 1 unrelated pre-existing
failure (stale tracking entry for non-existent
test-constraint-retry-propagator.rkt).

Latent issue exposed (NOT introduced by this fix): compile-match-tree
binds variable patterns to outer-param names when those params get
destructured by a later dispatch column. E.g., `cons r rest` after
outer-cons specialization tries `let rest := __cons_1` while `__cons_1`
is being destructured into `__cons_1_0` and `__cons_1_1`. This affects
the recursive bodies of the eigentrust example with multi-element
inputs, but is a pre-existing bug in compile-match-tree —
reproducible on main with the bracketed `[cons r rest]` form, which
parses to the same internal representation. The new tests cover the
slices unaffected by this bug (empty + singleton inputs, wildcard
patterns, all-var multi-arg) and explicitly call out the latent issue.

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
kumavis added a commit that referenced this pull request Apr 26, 2026
…defn

Pre-fix: `defn f | cons r nil -> r | cons r rest -> ...` parsed each
bare token after `|` as a separate arg pattern, splitting the function
into clauses with mismatched arities (1 nil clause + 2 cons-3-arg
clauses). This produced a per-clause helper (`f::1`, `f::3`) and the
recursive call site `[f rest]` failed with `Unbound variable f::1`
because the arity-1 helper only knew the nil clause and any non-empty
list hit __match-fail.

Fix shape (a) — implement general pattern matrices by auto-packing
when the leading bare token names a known constructor whose field
count matches the remaining tokens. `cons r nil` → one compound
pattern `pat-compound 'cons (var-r, var-nil)` (then normalize-pattern
converts var-nil to compound-nil since nil is a known nullary ctor).

Fallback preserved for genuinely multi-arg defns:
  defn add | x y -> [+ x y]
The leading `x` is a variable (lookup-ctor returns #f), so falls
through to the old N-arg interpretation.

Trade-off vs (b) (raise an error): (a) makes the syntax do what
ML/Haskell users expect — `defn` IS the primary dispatch mechanism
per .claude/rules/prologos-syntax.md, so making `cons r nil` mean
"compound pattern" is the natural reading. The detection is local and
does not change semantics for any pattern that didn't have a known
ctor as its leading token.

Scope: 23 lines in parser.rkt's parse-defn-clause + 11 new tests in
test-defn-multiarg-patterns.rkt. No changes elsewhere.

Test results: 11/11 new tests pass. 43/43 related tests pass
(test-pattern-defn-01, test-pattern-defn-02, test-multi-body-defn).
Full affected-suite: 4646 tests in 255 files, 1 unrelated pre-existing
failure (stale tracking entry for non-existent
test-constraint-retry-propagator.rkt).

Latent issue exposed (NOT introduced by this fix): compile-match-tree
binds variable patterns to outer-param names when those params get
destructured by a later dispatch column. E.g., `cons r rest` after
outer-cons specialization tries `let rest := __cons_1` while `__cons_1`
is being destructured into `__cons_1_0` and `__cons_1_1`. This affects
the recursive bodies of the eigentrust example with multi-element
inputs, but is a pre-existing bug in compile-match-tree —
reproducible on main with the bracketed `[cons r rest]` form, which
parses to the same internal representation. The new tests cover the
slices unaffected by this bug (empty + singleton inputs, wildcard
patterns, all-var multi-arg) and explicitly call out the latent issue.

Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com>
hierophantos added a commit that referenced this pull request Apr 27, 2026
…-marg

parser: disambiguate bare-token compound patterns in defn (eigentrust pitfall #7)
kumavis pushed a commit that referenced this pull request Apr 27, 2026
Per user review of #0-#10: many entries were either out-of-scope
(env limitations, not Prologos issues) or wrong (claims I never
actually tested). Re-tested every claim against a real Racket and
revised the doc.

Numbers are reserved per the user's instruction — entries marked
DELETED keep their slot so cross-refs don't drift.

Detail:

  #0  DELETED — out-of-scope (Racket toolchain not in sandbox).
                Environment limitation, not a Prologos issue.

  #1  REFRAMED — was "capability subtype + promise resolution
                composition." Re-titled to honestly reflect what
                this actually is: an OCapN-side Phase 0
                deferred-implementation note (eventual cross-vat
                receive isn't wired up yet). NOT a Prologos bug.

  #2  DELETED — false claim. Tested with a real Racket: WS-mode
                wildcard match `match | _ -> body` on user data
                types elaborates AND evaluates correctly when the
                function carries a proper `spec`. The
                `prologos::data::datum` comment I cited applies to
                a narrower polymorphic-context case, not a blanket
                wildcard ban as I asserted.
                Cleanup of behavior.prologos (~250 -> ~70 LOC)
                follows.

  #3  DELETED — false claim. Tested: `data Step step : [Nat -> Nat]`
                (with bracketed function type per the lseq-cell
                convention) accepts a function value, including
                closures with captured state. Open-world actor
                behaviour storage IS supported. The closed-enum
                BehaviorTag in our implementation was a needless
                workaround driven by this incorrect pitfall.
                Cleanup tracked separately.

  #4  KEPT, REFRAMED — real, narrowed claim. grammar.ebnf §6
                lines 1153/1187/1199 promise `Mu` (sexp) and `rec`
                (WS) for recursive sessions. Both elaborate to
                `Unknown session type: rec` / `Mu`. So pitfall #4
                is now: "rec/Mu in grammar but not in elaborator."
                CapTP's stream-level well-typedness is therefore
                the documented ceiling; per-exchange sub-protocols
                remain the workaround.

  #5  KEPT — `none`/`some` need explicit type args in some inference
            contexts. Real ergonomics tension, accurately
            documented.

  #6  DELETED — out-of-scope. WS-mode `let p := body` and sexp-mode
                `(let (p v) body)` are TWO surface forms by design
                (grammar.ebnf §7 line 1236). User-error, not a
                Prologos bug.

  #7  DELETED — was a quantitative restatement of #2. With #2
                recanted, #7 evaporates: behavior modules can be
                wildcard-collapsed, dropping ~180 LOC.

  #8  DELETED — false claim. Tested: `data Box1 box1 : [Sigma [_ <Nat>] Bool]`
                and `data Table table : Nat -> [List [Sigma [_ <Nat>] Bool]]`
                both elaborate cleanly. The named-struct
                ActorEntry/PromiseEntry workaround in vat.prologos
                was unnecessary; can be simplified back.

  #9  DELETED — user error. `def` for value bindings vs `defn` for
                functions is documented (grammar.ebnf §3
                lines 189-190, prologos-syntax rules). Mis-using
                `defn` for a 0-ary constant isn't a Prologos bug.

  #10 DELETED — out-of-scope. Network sandbox blocking external
                docs is an environment limitation.

#11-#20 were not in scope of this review and remain as-is for the
user to review next.
kumavis pushed a commit that referenced this pull request May 4, 2026
Original PIR text claimed runtime/core/ contains the BSP scheduler.
Wrong — actual runtime/core/ has only data structures (cell store +
profile counters + format buffer). The BSP scheduler stayed in each
kernel file (hybrid kernel's worklist + fire_against_snapshot +
merge_pending_writes + swap_worklists are inlined in
prologos-runtime-hybrid.zig).

Stage 3 design called for core/bsp.zig (~150 LOC) + core/worklist.zig
(~60 LOC) as Phase 1 deliverables. Actual Phase 1 extracted only
cells.zig + profile.zig + format.zig. The factoring scope shrank
silently — neither the implementing commit nor any subsequent commit
acknowledged the gap. Surfaced when the user asked "what's in the
hybrid core zig side?" during PIR review.

Corrections:
- §1 (What Was Built): explicit "data structures only" + cross-ref
  to wrong-assumption #9
- §2 (Stated Objectives): added "reality check on the design quote"
  flagging the drift
- §3 delivered table: Phase 1 status changed to "✅ partial"
- §4 timeline: Phase 1+3+4 line clarifies scheduler not extracted
- §5 deferred: new row for BSP scheduler factoring
- §8 D1 + anti-decision: caveat added; "BSP scheduler abstraction"
  claim corrected to "cell-store comptime-parameterization
  abstraction"
- §9 #2: factoring narrative softened to "data structures only"
- §11 #3: original kernel template + factoring made explicit at
  data-structure layer only
- §12 #2 + #8: kernel-LOC framing corrected; "factored core LOC was
  bigger than expected" reframed to "smaller than expected — and
  the gap is the BSP scheduler"
- §13 architecture: "consuming runtime/core/" framing softened to
  "consumes for cell store + profile + format helpers; the BSP
  scheduler is inlined"
- §14 #3, #7, #8: "future kernels instantiate the same scheduler"
  claim corrected to "instantiate CellStore + reuse profile
  counters; each kernel still writes its own scheduler"
- §15 technical debt: new row for "BSP scheduler not factored"
- §17 wrong assumptions: new #9 "Phase 1 will factor the BSP
  scheduler into core" — Wrong; codifies the silent scope shrinkage
- §18 #4: "factoring at second-instance" pattern reinforced with
  "complete vs minimum-viable shared surface" caveat
- §21 lessons: new entry for "phase-close should compare delivered
  scope against design plan"
- §24 open Q #4: kernel-PU consumption clarified — needs scheduler
  reuse in-place or triggers the extraction debt

Errata block added at the top of the PIR documenting which sections
were corrected and why.

https://claude.ai/code/session_01Tycs6BWKG58Wo99YVPg6DF
kumavis pushed a commit that referenced this pull request May 4, 2026
Plan to factor preduce.rkt + preduce-hybrid.rkt into a backend-agnostic
core (preduce-core.rkt) parameterized by a small backend interface.
Two concrete backends — backend-racket (current preduce.rkt internals)
and backend-hybrid (current preduce-hybrid.rkt FFI bridging) — wrap
their respective primitives. preduce.rkt and preduce-hybrid.rkt
become thin wrappers (~100 LOC each).

Why now:
- Phase 10/10b on hybrid is currently a port-not-wire-up because the
  two reducers have parallel compile-expr implementations
- ~80 sites of (define-values (cid net) ...) threading in preduce.rkt
  vs side-effecting kernel-state in preduce-hybrid is the structural
  divergence to reconcile
- After the refactor, OCapN-on-hybrid works for free via Racket
  callback fire-fns; profile-driven migration replaces hot callbacks
  with native individually
- Pattern parallel to runtime/core/ factoring at the Zig layer (the
  BSP scheduler debt from hybrid PIR §15); same shape one layer up

Plan structure:
- §1 motivation + cost of duplication today
- §2 audit — what's shared, what's specific (the threading-style
  divergence is the load-bearing decision)
- §3 design — preduce-backend struct, two concrete backends,
  fire-fn-as-pure-value-fn signature inversion
- §4 8-phase rollout (~9-11h total work; Phases 1-4 land the
  refactor, 5-8 validate + first migration on real workload)
- §5 6 risks + mitigations (threading flip, bot-handling, tag
  exhaustion, test-suite churn, hybrid-backend bugs, perf regression)
- §6 9 acceptance criteria
- §7 what this doesn't solve (Zig-kernel unification, FFI economics
  unchanged, Phase 11+ still callback)
- §8 connection to existing debt + the "factor at second-instance"
  pattern with three Racket-reducer consumers in mind
- §9 progress tracker

Acceptance criterion #7 is the user's stated goal: OCapN-syrup
running end-to-end through the hybrid kernel with --profile showing
where time is spent. Phase 6+7 deliver this.

https://claude.ai/code/session_01Tycs6BWKG58Wo99YVPg6DF
kumavis pushed a commit that referenced this pull request May 4, 2026
…throughout)

User challenged: "which threading model is appropriate to use both in
and out of native?" The answer is functional — preserve preduce.rkt's
(values cid net) discipline, have the hybrid backend wrap with a unit
sentinel.

Why functional, in-and-out-of-native:
- SH Track 1 deliverable is ".pnet network-as-value" — networks become
  first-class cell values that round-trip
- SH Track 9 (compiler-in-Prologos): compile-expr itself runs natively
  on propagators, with AST-cell input + network-cell output
- Native fire-fns can't side-effect networks they don't hold; they
  must take net as input and produce net' as output
- Side-effecting via current-prop-net is a bring-up convenience that
  becomes a dead-end at the SH endpoint
- The current-bsp-fire-round? #f hack retires when the parameter
  becomes the threaded net itself (in native)

Cost trade-off favors functional too:
- Functional: preduce.rkt unchanged; backend-hybrid wraps with sentinel
- Side-effecting: ~80-call-site flip in preduce.rkt
- Both backends pass through fire-fn closures unchanged (still
  net-threaded)

Plan revisions:
- §2.3 reconciliation: flipped from "side-effecting under the hood"
  to "functional throughout"; added comparison table showing why
  functional fits native + cost is lower today
- §3.1 interface: every primitive accepts and returns net; fire-fns
  unchanged from today (still net → net')
- §3.2 backends: backend-racket uses prop-network struct; backend-
  hybrid uses 'hybrid sentinel; future backend-native uses cell-id
  as net (native dataflow)
- §3.3 compile-expr sketch: structurally identical to today's
  preduce.rkt; only primitive-rename to b-alloc / b-install-fire-once
- §4 rollout: simplified — Phase 2 (interface inversion) eliminated;
  total dropped from 9-11h to 8-10h
- §5 risks: dropped #1 (threading-flip), refined #2 (bot-handling
  via b-read normalization), added #7 (current-bsp-fire-round?
  through FFI verification)
- §9 tracker: 8 phases, this design doc done

Critical implication for the hybrid backend: fire-fns stay net-
threaded, which means make-reduce-fire's compile-and-bridge recursive
compilation (which itself installs more propagators) just works
through the abstract backend without modification.

https://claude.ai/code/session_01Tycs6BWKG58Wo99YVPg6DF
kumavis pushed a commit that referenced this pull request May 4, 2026
Per user review of #0-#10: many entries were either out-of-scope
(env limitations, not Prologos issues) or wrong (claims I never
actually tested). Re-tested every claim against a real Racket and
revised the doc.

Numbers are reserved per the user's instruction — entries marked
DELETED keep their slot so cross-refs don't drift.

Detail:

  #0  DELETED — out-of-scope (Racket toolchain not in sandbox).
                Environment limitation, not a Prologos issue.

  #1  REFRAMED — was "capability subtype + promise resolution
                composition." Re-titled to honestly reflect what
                this actually is: an OCapN-side Phase 0
                deferred-implementation note (eventual cross-vat
                receive isn't wired up yet). NOT a Prologos bug.

  #2  DELETED — false claim. Tested with a real Racket: WS-mode
                wildcard match `match | _ -> body` on user data
                types elaborates AND evaluates correctly when the
                function carries a proper `spec`. The
                `prologos::data::datum` comment I cited applies to
                a narrower polymorphic-context case, not a blanket
                wildcard ban as I asserted.
                Cleanup of behavior.prologos (~250 -> ~70 LOC)
                follows.

  #3  DELETED — false claim. Tested: `data Step step : [Nat -> Nat]`
                (with bracketed function type per the lseq-cell
                convention) accepts a function value, including
                closures with captured state. Open-world actor
                behaviour storage IS supported. The closed-enum
                BehaviorTag in our implementation was a needless
                workaround driven by this incorrect pitfall.
                Cleanup tracked separately.

  #4  KEPT, REFRAMED — real, narrowed claim. grammar.ebnf §6
                lines 1153/1187/1199 promise `Mu` (sexp) and `rec`
                (WS) for recursive sessions. Both elaborate to
                `Unknown session type: rec` / `Mu`. So pitfall #4
                is now: "rec/Mu in grammar but not in elaborator."
                CapTP's stream-level well-typedness is therefore
                the documented ceiling; per-exchange sub-protocols
                remain the workaround.

  #5  KEPT — `none`/`some` need explicit type args in some inference
            contexts. Real ergonomics tension, accurately
            documented.

  #6  DELETED — out-of-scope. WS-mode `let p := body` and sexp-mode
                `(let (p v) body)` are TWO surface forms by design
                (grammar.ebnf §7 line 1236). User-error, not a
                Prologos bug.

  #7  DELETED — was a quantitative restatement of #2. With #2
                recanted, #7 evaporates: behavior modules can be
                wildcard-collapsed, dropping ~180 LOC.

  #8  DELETED — false claim. Tested: `data Box1 box1 : [Sigma [_ <Nat>] Bool]`
                and `data Table table : Nat -> [List [Sigma [_ <Nat>] Bool]]`
                both elaborate cleanly. The named-struct
                ActorEntry/PromiseEntry workaround in vat.prologos
                was unnecessary; can be simplified back.

  #9  DELETED — user error. `def` for value bindings vs `defn` for
                functions is documented (grammar.ebnf §3
                lines 189-190, prologos-syntax rules). Mis-using
                `defn` for a 0-ary constant isn't a Prologos bug.

  #10 DELETED — out-of-scope. Network sandbox blocking external
                docs is an environment limitation.

#11-#20 were not in scope of this review and remain as-is for the
user to review next.
kumavis pushed a commit that referenced this pull request May 6, 2026
Per-track LOC contribution estimates for the remaining Phase 7
migration targets, with rationale + risk weighting + prerequisite
ordering. Grounded against current code-size baselines:
  Zig kernel: 913 LOC
  Racket reducer + backends + bridge: 2347 LOC

Summary (track / Zig delta / Racket delta / cb-time absorbed):
  #5 boolrec -> kernel_select         +0    +30    ~4%   (free; just routing)
  #4 ctor-N native ABI                +400  +200/-100  ~5% workload, ~50% OCapN
  #3 expr-reduce match dispatch       +200  +200/-150  ~10%
  #2 expr-natrec step                 +150  +50/-30    ~5% effective, ~17% theoretical
  #1 recursive expr-fvar + expr-app   +1000 +400/-200  ~60%
  #7 CHAMP collection ops             +5000+ +500/-200 ~4% (synthetic; defer)

Net if #1-#5 land: Zig +1750 LOC (~3x growth); Racket -50 LOC net.
Surface complexity migrates from Racket compile-expr to Zig kernel.

Three suggested orderings (A: biggest payoff first; B: incremental;
C: value-engineering minimum). All start with #5 (free), all
prerequisite #4 before #3.

Doc identifies 5 open design questions: ctor-N ABI choice
(heap-backed vs bit-packed), closure representation, tail-call
semantics, eager arm compilation interaction with recursion,
bot-guard convention formalization.

Three things this analysis does NOT settle:
- Whether #1 is feasible without losing static-beta benefits
  (B1/B2/H1/J1/J2 do zero runtime fires today; native apply costs
  more rounds).
- Per-fire cost of native call apparatus (somewhere between 115ns
  native and 4100ns callback; not measured).
- Whether #1+#2+#3 land as one track or three (architecturally
  coupled; landing them independently means a stub-laden middle
  state).

https://claude.ai/code/session_01Tycs6BWKG58Wo99YVPg6DF
hierophantos added a commit that referenced this pull request May 9, 2026
…sisted

Phase 15 (Day's doubling / inflation detection per Adaricheva-Nation
2017) opens with full Stage 4 mini-design + mini-audit + adversarial
CRITIQUE_METHODOLOGY pass.

Background research (mempalace): Day's doubling lineage 1970-2017+.
Day 1970 original interval-doubling (used to prove (W) for FL); 1979
bounded-homomorphic-image characterization; Adaricheva-Nation 2017
generalizes to all-or-nothing set inflation.

Q1=B: Algorithm = Option B (Adaricheva-Nation 2017 all-or-nothing
pair detection). Option A (Day covering-pair) subsumed.
Q2=pair-only: extended-set search (Tier 4) deferred.
Q3=no implication rule (sample-unsound either direction per Phase 12+13).
Q4=full sweep scope (10 tuples; 4 domains × relations × depths).
Q5=honest framing: sample-bounded admittance claim, not inflation
history.

Confirmation/refutation semantics differ from Phase 12+13: existence-
claim shape — one witness = confirmed, none = refuted-on-sample.

Adversarial pass: P/R/M/S two-column. 4 honest scope-acknowledgments;
no drift requiring corrective. 7 drift risks named.

Phase 15 = final reopened-arc phase. Track 2I closes after Phase 15.
Adversarial VAG at close extends to whole reopened arc (Phases 11-15)
per drift-risk #7.
hierophantos added a commit that referenced this pull request May 9, 2026
Sub-phase pattern not needed: single-commit implementation per Phase 11+
in-phase pattern. Algorithm: Option B (Adaricheva-Nation 2017
all-or-nothing pair detection).

New code in sre-core.rkt:
- dd-evidence 5-field struct (status × total-pairs × hypothesis-fired
  × conclusion-held × witness)
- dd-classify-side helper: classifies external x w.r.t. (s1, s2) as
  'above | 'below | 'incomparable | 'split
- test-admits-day-doubling/detailed + wrapper. For each incomparable
  pair (s1, s2), check that no external x is 'split. First witness =
  confirmed; no witness = refuted-on-sample.
- Wrapper coerces symbol-witness to list for axiom-refuted contract
  (refuted-on-sample uses 'no-incomparable-pairs / 'no-all-or-nothing-
  pair-on-sample markers).

Wired into all 7 sites: provides + props-22 + evidence map +
all-sweep-properties (now 20) + sweep dispatch + extract-detailed-fields
(both sre-property-sweep and run-phase9-sweep per Phase 11 lesson).
7 new test-cases. Targeted suite GREEN: 196 tests / 4.5s.

Sweep run via 4 concurrent processes (~1s wall total — much faster
than estimated):

| Tuple | Status | Non-vacuity | Witness highlight |
|---|---|---|---|
| type × eq × ground | refuted-on-sample | n/a | hash-code anomaly |
| type × eq × wider | confirmed | 33% | (Int, pair(Bool, Bool)) |
| type × sub × ground | refuted-on-sample | n/a | hash-code anomaly |
| type × sub × wider | confirmed | 92% | (Bool, pair(Bool, Bool)) |
| session × eq × ground | confirmed | 100% | (sess-end, sess-svar 0) |
| session × eq × wider | confirmed | 100% | same |
| form-cell × eq × ground/wider | confirmed | 40% | tag-set differing |
| spec-cell × eq × ground/wider | confirmed | 33% | name differing |

8/10 tuples confirm Day-doubling admittance with concrete witnesses.
Heterogeneous Prologos lattices universally admit Day-style inflation.

Type × ground anomaly: nullary constructor instances (expr-Int,
expr-Bool, etc.) have colliding equal-hash-codes, causing canonical-
pair filter (< hash s1 hash s2) to skip same-hash pairs in BOTH
directions. Atomic-pair incomparable-detection bypassed at ground
sublattice. Wider sample provides substantive answer; documented as
sample-set quirk in design doc tracker + Nation report § What we did
not measure (already committed in f23ed5e).

No forward implication rule (sample-unsound, Phase 12+13 precedent).

test-sre-sd-properties.rkt:413 count: 19 → 20 (Phase 15 +1
admits-day-doubling).

Adversarial VAG passed at phase close. Reopened-arc VAG (Phases 11-15
as unit) deferred to Track 2I close commit per drift-risk #7.

Phase 15 — final reopened-arc phase. Track 2I close commit next.
hierophantos added a commit that referenced this pull request May 9, 2026
Track 2I substantively closed at Phase 10 (first close, 2026-05-08).
Reopened for Phases 11-15 gap-closure (commit 6aab87c, same day).
Phase 15 lands as the final reopened-arc phase.

Reopened-arc adversarial VAG (Phases 11-15 as unit) per drift-risk #7:
- (a) On-network: 5 new property checks extend Track 2G off-network
  scaffolding lineage; honestly labeled.
- (b) Complete: 196 tests GREEN; substantive Q7 added to Nation report;
  honest scope-bounds (type×wider anti-exchange CPU timeout, type×ground
  all-or-nothing hash-collision artifact).
- (c) Vision-advancing: empirical breadth across 5 algebraic axes;
  Adaricheva-Nation 2017 direct relevance secured for meeting.
- (d) Drift-risks-cleared: each phase's named risks materialized as
  expected, didn't fire, or resolved in-flight.

VAG passes adversarially across the reopened arc.

Two cross-phase patterns surfaced for promotion candidate (next
session's lessons-distillation pass):
1. No-forward-implication-rule discipline (sample-unsound) — 4-phase
   pattern across Phases 12, 13, 14, 15.
2. Single-commit code+sweep+report rhythm (Phase 11+ in-phase pattern)
   — 4 data points across Phases 11, 12, 13/14, 15.

Track 2I final status:
- 14 phases complete (1-15 minus Phase 9b sub-phasing)
- 20 algebraic properties in all-sweep-properties
- 4 SRE-registered domains × {ground, wider} sweep matrix populated
- Lattice Variety Report ready for Nation meeting
- 196 tests GREEN

Open follow-ups (post-meeting): type×wider anti-exchange k=1 rerun;
Phase 14 type-domain wider-sample congruence empirical content;
Phase 15 extended-set search (Tier 4); property-cells migration
(sister track); hash-code-stable canonicalization for atomic-struct
samples.

Track 2I CLOSED (substantively + comprehensively).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants