The iGEM Chronology Puzzle — Provenance & Handoff Document

Current version: v0.541. This document consolidates every prior provenance/changelog document in this project (igem-puzzle-v0.42-provenance.html, architecture-spec-multi-engine.md, clue-sets-B-and-C.md) plus everything learned since, into one place. It’s written to be read by a human or by a future Claude session picking this project back up cold — if you’re the latter, read §1 (current state) and §7 (engine implementation notes) first; those are the two sections most likely to save you from re-discovering bugs that have already been found and fixed.

1. Current state (read this first)

Executable page: igem-puzzle-v0.541.html. Single self-contained HTML file, no external dependencies, no build step. Opens directly in a browser or serves from any static host.

What works, fully verified (not just built): - Engine selection: Tau Prolog, ramo, or microKanren, chosen once per session before the main activity. - Clue-set selection: A, B, or C — all three clue-sets are available for all three engines (since v0.531); the setup screen doesn’t disable any (engine, clue-set) combination. - Every fact revealed comes from a genuine query against the selected engine — no clue’s readiness or result is decided by a JS conditional standing in for the engine. - A real Fitch-style proof (FitchFX, MIT) is driven automatically for 13 of Clue-set A’s 23 clues, when Tau Prolog is the engine (see §8) — still not wired to ramo or microKanren, and still not covering the remaining 10 clue types or clue-sets B/C. This is the one piece of the original plan still unfinished. As of v0.533, though, the interface now actually explains this coverage gap where it didn’t before (see below). - All nine (engine, clue-set) combinations converge on the identical real answer table (below), confirmed via jsdom end-to-end tests that click actual buttons and read the actual rendered DOM. - A dedicated provenance-tagging audit (v0.532, see §11) checked all 73 top-level declarations in the main script for attribution coverage and found/fixed three instances of stale “Clue-set A only” tag drift left over from the v0.531 port, plus one genuine tagging gap on the B/C clue-goal functions — see §11 for what was found and how. - Five interface/UX issues reported and diagnosed during v0.532 were fixed in v0.533 (§1a has the original diagnoses, §7e has how each was fixed): the broken FitchFX image, the missing Fitch-coverage and star-clue explanations, blocking Apply-button clicks, and a lack of local before/after feedback near each clue. Fixing the Apply-button responsiveness issue surfaced a genuine new concurrency bug (two clicks could launch overlapping queries against the same Tau Prolog session, confirmed to crash with an out-of-memory error) — also fixed, with an explicit lock, and documented in §7e as its own finding rather than folded silently into the original fix. - The Engine trace panel now serves a real purpose for all three engines, not just Tau Prolog (v0.534, see §7f) — it was reported as looking useless, and turned out to be useless permanently, not just for that one action: ramo and microKanren always returned trace: null, and the render function only ever checked that field, silently discarding a real query summary both functions were already computing. Fixed by building a genuine step-by-step log from data those functions already compute, rather than fabricating a resolution trace neither engine has any mechanism to produce. - A new Action-effect log (v0.541, see §7g) — a radical redesign, specified by the user: every clue application is now recorded, in order, along with every fact it revealed, including facts re-confirmed after already being known. The first-ever reveal of any fact is bolded; once all 24 facts are known, further actions are logged as wasted effort and the query is skipped entirely (a provable guarantee once that point is reached, not a heuristic). Required a real change to all three engines’ own fact-detection loops, not just a new display — see §7g for what changed and how it was verified not to alter any engine’s actual solving behavior.

The real answer (all nine (engine, clue-set) combinations solve to this):

Immediate next steps (in the order they were being tackled when this document was written): the big one queued and explicitly deferred out of v0.533’s scope is §1b’s proof-coherence requirement (tier 1 minimal-support-set computation, then tier 2 full proof construction) — not started. Smaller and still open: extending the FitchFX translation itself to ramo and microKanren, to Clue-sets B and C, and to the organism-year block and the other 10 not-yet-covered clue types within Clue-set A. A useful periodic check for any future session, independent of new features: re-run the kind of provenance-tagging audit done in v0.532 (§11) every few versions, since tag drift (a comment describing something that used to be true) accumulates silently otherwise — and, per v0.533’s own experience, re-running the full regression suite after any change to click-handling or async structure is worth treating as mandatory, not optional, since that’s exactly the kind of change whose failure mode is a crash rather than a wrong answer.

1a. Known issues, noted during v0.532, fixed in v0.533

Five issues were observed in practice and diagnosed (root cause found and confirmed) during v0.532, then all five were fixed in v0.533. Kept here as a historical record of the diagnosis (per this document’s own convention of preserving history rather than deleting resolved notes) — see §7e for how each was actually fixed, and what was found while fixing them.

1. Broken image in the Fitch display section. Confirmed cause: FitchFX’s own header markup includes <img src="img/github.png" style="height:25px;"> (a GitHub link icon), vendored byte-identical along with the rest of FitchFX’s HTML/CSS/JS (see §8’s provenance note on the <iframe srcdoc> embedding). The six FitchFX .js files and one .css file were mechanically inlined into that srcdoc string, matching this project’s single-file-no-external-dependencies convention — but FitchFX’s own img/ asset folder (just the one GitHub icon) was never brought along, since inlining code doesn’t inline image files the same way. The <img> tag is still there, pointing at a relative path with nothing behind it, so it renders as a broken image. This is the only <img> tag found anywhere in the page (confirmed via a full-file search) — not a wider pattern, just this one leftover reference. Fix options for v0.533: either remove the <img> tag from the vendored srcdoc string (a from-upstream-copy deviation, which would need its own explicit tag noting the modification, since the current comment says “byte-identical… no new Fitch code” — removing even a broken <img> tag breaks that literal claim and should be flagged, not done silently), or inline the actual icon as a data URI (keeps the markup closer to byte-identical while fixing the display; small enough image that this is practical), or replace it with a plain GitHub-icon-free link (simplest, changes the vendored appearance slightly). No decision made yet on which approach to take.

2. Unclear why some clues have a Fitch derivation available and others don’t. Confirmed cause: FITCH_SIMPLE_A (the lookup table driving which clues get an automatic Fitch translation) only has entries for the 13 of Clue-set A’s 23 clues that fit one exact shape — a single organism-anchored antecedent implying a single consequent value in another category ({ante:['organism', X], cons:[category, Y]}), i.e. clues of the form “if the organism is X, [country/award/project] is Y.” The other 10 clues don’t fit that template for three different, unrelated reasons, none of which are explained anywhere in the interface: clues 1 and 20 are absolute position-pins with no antecedent at all (not an implication, so there’s no “if” to translate); clues 2, 3, 4, 5, 9, and 22 are relative- order or chained-existential clues (righto/aftero/multi-hop offset), which are a fundamentally different logical shape than “single value implies single value”; and clues 12 and 16 are country-anchored rather than organism-anchored pairings (the template only ever built an organism-anchored antecedent). None of this is a bug in the sense of incorrect behavior — every clue that doesn’t fit still works correctly as a puzzle clue, it just doesn’t get an automatic proof-panel translation — but it is a real gap in that the interface never tells the person playing why only some clues light up a Fitch derivation, so from the outside it looks arbitrary rather than principled. It’s also worth noting this coverage is Clue-set-A-and-Tau-Prolog-only regardless: ramo and microKanren never get Fitch derivations for any clue, and clue-sets B and C never get them either (see §8) — the “why” question likely covers both the intra-clue-set-A gap and this broader engine/clue-set restriction, and any v0.533 fix should probably address the user-facing explanation for both rather than just the narrower 13-of-23 case. Fix options for v0.533: at minimum, add a short explanatory note near the Fitch panel (something like “Automatic proofs are available for the 13 of 23 clues that translate to a single if-then rule; clues with absolute position pins, relative ordering, or multi-step offsets aren’t yet translated”) rather than silence; more ambitious would be extending FITCH_SIMPLE_A’s template to cover country-anchored pairings (12, 16) and absolute pins (1, 20) as straightforward variations on the existing pattern, which would leave only the genuinely-different relative-order/chained clues (2, 3, 4, 5, 9, 22) uncovered and explainable on their own terms. No decision made yet on how far to take this for v0.533.

3. No explanation for the star/orange-highlighted clues. Three of Clue-set A’s clues (9, 22, 23) render in orange with a ★, via wrap.className = 'clueRow' + (curData().text[num].includes('\u2605') ? ' star' : '') in renderClueRows() — the star is a literal character embedded directly in those three clues’ own text strings, not a separate flag. All three are independent ways to pin Hong Kong’s year (matching Clue-set A’s own top-level description: “23 clues, chained arithmetic + three independent routes to Hong Kong’s year”), but nothing in the interface says so — a person playing sees the color/star with no explanation of what it means or why those three specifically. Fix for v0.533: add a hint (tooltip, legend entry, or a line near the clue list) telling the person that clues marked with the orange/star styling are likely to be particularly load-bearing for finishing the puzzle, since each is an independent route to the same conclusion. Purely a UI-text addition — no logic changes needed, since the styling and the underlying three-independent-routes design are already correct and intentional, just unexplained.

4. Apply buttons feel unresponsive for ramo and microKanren (main-thread blocking, not background work). Confirmed root cause, not just perceived slowness: applyClueRamo and applyClueMK contain zero await statements in their bodies (verified directly by grepping each function’s body) — applyClueRamo is labeled async, but that alone does not create a yield point; a function only actually yields to the browser at a real await on a still-pending promise. Since neither function ever awaits anything, each runs its entire search (permutation generation, goal solving, diffing against known facts) as one uninterrupted synchronous block on the main thread. The click handler sets the button to “Querying…” before calling applyClue(), but the browser can’t paint that change until the current call stack returns — so for however long the query takes (measured up to ~2–3s for some ramo/microKanren B/C cases, see §7d), the button just looks frozen/unresponsive, then everything updates at once. This is the opposite of “background work”: the engine is blocking the only thread the browser has, foreground included. Tau Prolog doesn’t have this problem — runQuery() wraps Tau’s own callback-based session.answer() in a genuine Promise, which is a real yield point, so the browser gets to repaint before Tau’s heavy work runs. Fix options for v0.533: the simplest is inserting a real yield (e.g. await new Promise(r => setTimeout(r, 0))) between setting the “Querying…” state and calling into ramoLib.run(...)/the microKanren solve, so the browser paints the intermediate state first — this won’t make the query itself faster, but it will make the button visibly respond immediately rather than appearing stuck. A more thorough (and more involved) fix would move the actual search off the main thread entirely (a Web Worker), which would also stop the query from blocking any other UI interaction while it runs, not just this button’s own label.

5. No local feedback near the Apply button itself — the person has to look at a distant table to tell if a click did anything. Raised from a user’s perspective: the Known-So-Far grid is a different part of the page from the clue list, so after clicking Apply, there’s no way to tell from the button’s own area whether that click actually revealed something, without scrolling/glancing away and back. There’s a partial version of this already: when newFacts.length === 0, a .hint div gets appended right under the clue row explaining why nothing happened (see renderClueRows()’s click handler, and the noProgress entries in HINTS). But when a click does reveal something, nothing comparable appears locally — the person only finds out by checking the grid. Fix for v0.533: generalize that existing mechanism so it always shows local feedback, not just on the zero-progress case. Concretely: count total filled cells in KNOWN right before applyClue() is called (call it x) and again right after newFacts are folded in (call it y), and render a short message in the clue row’s own area either way — something like “Facts known before: x → after: y.” If y = x, that reads as “this click didn’t move anything forward” (subsuming the existing noProgress hint, which can stay as the more specific explanation when one exists); if y > x, it reads as immediate positive confirmation that the click was productive, without needing to look anywhere else on the page. Straightforward to build on top of what’s already there — the counting logic itself is trivial (Object.values(KNOWN).reduce((n,row) => n+Object.keys(row).length, 0), already used in exactly this form by the project’s own test scripts), the only new work is capturing that count before the query as well as after, and rendering it unconditionally rather than only in the zero-progress branch.

1b. Design requirement raised after v0.532: the reveal sequence should correspond to a coherent proof

The requirement, as stated by the user: when all facts are known, the sequence in which facts get revealed should correspond to at least one valid proof. Applying a clue should be a reasoning step (or a small number of them) expressible as logical statements — not an opaque result. This substantially broadens §1a issue #2 above: extending FITCH_SIMPLE_A’s template to more clue shapes would explain more individual clues, but it would not, by itself, guarantee the sequence of reveals forms a coherent proof. This needs its own analysis before v0.533 work starts, since it’s a genuinely different (larger) problem than the display-gap issue it grew out of.

Why the current architecture doesn’t satisfy this, mechanically: every engine’s applyClue* reveals facts the same way — query all currently-active clues plus already- known facts together, then check which category/row cells agree across every solution the engine returns, and report those as new facts. This is a diff against exhaustive search, not a step-by-step derivation. Nothing about it currently records why a cell became forced — only that it did. Three concrete gaps this creates: 1. Multi-clue combination. Several clues often only force a fact together, not individually — e.g. clue-set A’s clues 1–5 reveal nothing on their own but resolve the entire organism ordering once all five are active. A correct proof for that reveal needs to cite all five clues (and however the reasoning actually combines them), not just whichever one happened to be clicked last. 2. Order-dependence. Because clues can be clicked in any order, which facts are already “known” (and thus available as premises) at the moment a given clue is applied depends on the person’s own click order. A valid proof has to be built from what was actually known at that moment, not from some idealized canonical order — there’s no single fixed proof for the puzzle as a whole; there’s a different valid proof for each possible click order, and the code would need to construct whichever one actually happened. 3. Different clue shapes need different inference rules. The existing FITCH_SIMPLE_A template is a single-step modus-ponens shape (“if organism is X, category is Y”). That doesn’t cover: absolute position pins (which aren’t an implication at all — more like a direct premise); relative-order clues (righto/ aftero, needing something like transitivity chains over multiple known positions); chained-existential offset clues (clue 9/22-style, needing existential instantiation chained through intermediate positions); and — hardest — elimination-style reveals, where a fact becomes known only because it’s the one remaining possibility once every other value has been placed elsewhere (a disjunctive-syllogism/case-elimination argument, not a forward chain — in Fitch terms this typically needs nested subproofs with case splits, not a flat four-line derivation).

A two-tier plan, not yet started, for whoever picks this up: - Tier 1 (tractable, worth doing first): minimal-support-set computation. For each newly revealed fact, determine the smallest subset of currently-active clues (plus already-known facts) that still forces it — by re-querying with each active clue dropped one at a time and checking whether the fact still comes out forced; whichever clues can’t be dropped without losing the fact are the ones actually load-bearing for that reveal. This doesn’t construct a full natural-deduction proof, but it directly answers “which clues, combined, are actually responsible for this fact becoming known” — which is most of what’s needed for issue #2’s transparency problem, and a necessary input to tier 2 regardless. Feasible with the existing engines as-is (just more queries per reveal), and worth verifying its cost doesn’t reintroduce the kind of performance problems §7c/§7d already found and fixed for microKanren specifically. - Tier 2 (substantially harder): actual proof construction. Given a minimal support set from tier 1, construct a valid Fitch-style (or other natural-deduction) proof whose premises are exactly those clues/facts and whose conclusion is the revealed fact — this needs a distinct inference-rule template per clue shape (at least four: direct pin, single implication, order/transitivity, chained existential) plus a genuinely different template for elimination-style multi-clue combinations (nested case-split subproofs). Mining Tau Prolog’s own resolution trace (already partially read elsewhere in this project, per §7a’s debugger-trace note) is one possible source of structure for this, but SLD resolution and Fitch natural deduction are different proof formalisms — that translation is itself nontrivial, and wouldn’t help ramo or microKanren at all, which have no comparable trace to mine. Building tier 2 as an engine-agnostic layer on top of tier 1’s support sets (rather than trying to extract it from each engine’s internals differently) is probably the more robust path, but this is genuinely new proof-search code, not a lookup-table extension like FITCH_SIMPLE_A.

Scoping note: this is larger than a single v0.533 session’s worth of “extra code,” on the order of the original three-engine or three-clue-set efforts (§6/§7d) rather than a bug fix. Worth explicitly scoping/estimating tier 1 alone before committing to tier 2 in the same version, rather than assuming both fit together.

2. File inventory

Note on the jump from v0.534 to v0.541: earlier versions incremented by exactly 0.001 per round of changes; v0.541 is a user-specified version number for this particular (substantial, “radical redesign”) change, not a sign that versions 0.535–0.540 exist somewhere and were skipped over in this document. There is no gap to account for.

Executable pages (all preserved, never overwritten)

Documents

Standalone test/module files (project sandbox, not shipped in the HTML)

3. What this project actually is

An interactive puzzle tool built around a 6×4 Einstein/zebra-style logic puzzle (6 iGEM synthetic-biology teams, 2020–2025, each with a unique country/organism/project/award). The puzzle itself was supplied by the user at the very start of the project (real, sourced iGEM team data) — this is user-supplied content, not something Claude invented.

The project’s guiding constraint, stated explicitly partway through and driving every architectural decision since: maximize genuinely open-source or textbook-derived code, minimize bespoke Claude-authored logic, for presentation to judges as evidence of responsible AI use. This is why the architecture pivoted hard partway through (see §4) — an earlier, more pedagogically elaborate design (v0.4–v0.42) was almost entirely bespoke JavaScript, which directly conflicts with that goal even though it was a reasonable design on its own terms.

4. The architectural pivot (why v0.5 looks nothing like v0.42)

v0.1–v0.32: mostly open-source-dependent (Tau Prolog / ramo / microKanren doing the actual solving) but passive — click “solve,” watch a trace.

v0.4–v0.42: maximally forcing (nothing revealed until the student clicks for it — including a real hand-authored Fitch natural-deduction engine with genuine reductio boxes) but almost entirely bespoke Claude logic. None of the readiness-checking, case-exhaustion analysis, or Fitch-proof construction in these versions came from Tau Prolog, ramo, or microKanren — it was Claude re-implementing what those engines could have done, defeating the “minimize bespoke code” goal even while nailing the pedagogy.

v0.5 onward: the resolution. Keep the forcing function (nothing revealed until genuinely derivable), but make the engine the thing doing the deriving — “is this clue ready” becomes a real query against whichever backend is selected, using that engine’s actual unification/search, not a hand-written JS conditional. This is a genuinely different codebase from v0.42’s, not an incremental evolution of it; the two lineages share almost no logic (only the FOL notation scheme carries forward).

5. The three clue-sets

All three use the identical vocabulary (6 years, 6 countries, 6 organisms, 6 projects, 6 awards) and the identical organism↔︎project pairing (real project names tied to organisms: RootPatch↔︎nematodes, Helo↔︎yeast, ReneWool↔︎spider silk, Ecoplaster↔︎Black Soldier Fly, SPROUT↔︎peptide-sensor bacteria, the unnamed algae project↔︎cyanobacteria — fixed across all three, not re-derived per clue-set). All three converge on the identical real answer (§1). They differ in reasoning style:

• Clue-set A (23 clues): successor-chain arithmetic for organism-years (cyanobacteria = nematodes + 1, etc.), organism-anchored co-occurrence for the rest, plus three independent, verified routes to Hong Kong’s year (clues 9, 22, 23 — each checked by removing the other two entirely and confirming the puzzle still solves uniquely via each alone).
• Clue-set B (22 clues): direct year-pins and loose (non-fixed-distance) inequalities for organism-years; country facts chained by arithmetic offset from the Dutch team; award/project facts anchored to country and award respectively (not organism, unlike A).
• Clue-set C (21 clues): pure negation/exclusion throughout — organism-years, awards, and projects are all pinned by ruling out five of six alternatives; country facts chained by offset before the German team (reverse direction from B).

Pairwise clue overlap (literal text comparison against A’s exact wording, not estimated): A∩B = 3 clues (share the same natural, singular wording for “the nematode team was Dutch,” “the American team was nominated for Best Therapeutics,” and “the German team won the Safety and Security Prize” — deliberately not forced apart into awkward alternate phrasing). A∩C = 0. B∩C = 0. All well within the requested ≤8-per-pair budget.

Four real bugs caught building B and C, all found by running the actual solver, not by re-reading the hand-written clues more carefully: 1. Clue-set C’s project-exclusion clues originally excluded only 4 of 5 wrong answers (forgot the unnamed algae project as a candidate), leaving every project ambiguous. 2. A leftover dead-code line (nth1(Anem, Awards, XX0), true) nondeterministically enumerated award positions, producing 6 spurious duplicate “solutions.” 3. An unbound-variable typo (Nnem referenced but never bound to the right quantity) silently misapplied one constraint. 4. Clue-set B and C’s cyanobacteria-year clues were accidentally worded identically before this was caught and fixed (would have been an unintended overlap).

Full clue text and FOL notation for all three sets are embedded in igem-puzzle-v0.525.html itself (CLUESET_DATA.A/B/C.text and .fol), and the original verification notes are also in clue-sets-B-and-C.md.

6. Architecture: the multi-engine design

Core idea: one UI shell (clue list, known-so-far grid, trace panel) that contains no solving logic itself. All solving logic lives behind a shared informal interface, implemented once per engine. The student picks engine + clue-set once per session; everything downstream is identical regardless of which combination they picked (subject to the combination actually being supported — see §1).

UI Shell (clue text, grid, trace panel, buttons)
        |
        v
  per-engine dispatch (isReady / applyClue, see §7)
        |
   -----+---------+-------------
   |               |            |
Tau Prolog        ramo      microKanren
 (built, A/B/C)  (built, A/B/C) (built, A/B/C)

Why session-level, not per-action: switching backends mid-derivation would require translating partial state between fundamentally different internal representations (a Prolog substitution vs. a relational substitution map) — real complexity for no real benefit. Session-level choice keeps each backend self-contained and independently testable, which mattered a great deal in practice (see §7).

Shared puzzle data (used by all backends, never used to decide correctness — only for display and for cross-checking test results): the clue text, display labels, and the answer key.

The trace panel is deliberately not normalized across engines. Tau Prolog’s trace is its own debugger_states (real WAM resolution steps); ramo’s is a textual description of the query run (no per-step hook exists — see §7b); FitchFX’s proof panel is a third, different kind of “trace” entirely. Forcing these into one common shape would hide real information about how each engine actually works, which cuts against the whole point of showing genuine internals.

microKanren, built in v0.53. Per the original plan, this is a from-scratch, from-the-paper core (Hemann & Friedman), not a port of any existing JS package — see §7c for the implementation notes and §9 for why its provenance category is distinct from Tau Prolog’s and ramo’s (transcribed technique vs. vendored dependency).

7. Engine implementation notes — read before touching either backend

7a. Tau Prolog (built: Clue-sets A, B, C)

• Encoding: per-clue-predicate Prolog, one predicate per clue number (clue1/1 … clue23/2 for A; similarly for B/C), each fully self-contained — no clue’s predicate requires another clue’s variable pre-bound. This self-containment is what makes “any clue independently clickable” possible at all; it required rewriting the original sequential-threading encoding from earlier versions.
• Readiness/query mechanism: findall over the currently-active clue set (the ones the student has actually clicked), never over all 23 at once (that would just solve the whole puzzle immediately on the first click, defeating the incremental reveal). A cell is “newly forced” if its value is identical across every solution in the findall result — genuinely exhaustive, not sampled (contrast with ramo, §7b).
• Two severe bugs found and fixed, both matter if this encoding is touched again:
  1. Goal ordering. A fixed category order (organism→country→project→award) caused Tau to exhaustively search an unconstrained category before ever checking the constraint that would prune it — measured at 45+ seconds, and in one case an actual out-of-memory crash. Fixed by dynamically ordering categories by how constrained they currently are (most-known first) rather than a fixed sequence.
  2. Trace size. Capturing debugger_states from the exhaustive findall itself produced 24,000–42,000 steps per single click — rendering that into the DOM repeatedly is what caused the crash above, not the query cost itself (which is ~1 second either way). Fixed by running the findall without the debugger for correctness, and a separate, cheap single-answer query with the debugger purely for the trace display (129 steps instead of 31,815).
  3. Readiness rule, arrived at empirically, not derived on paper: a multi-category clue is fast once at least one of its categories is ≥5/6 known (not necessarily all of them) — verified this is both necessary (true cold-start, both categories open, is still genuinely slow: 15+ seconds) and sufficient (combined with the dynamic ordering fix) across every case tried.
• Tau’s own consult/query/answer async callback pattern is documented usage, not something invented for this project — the promisification wrapper around it is the only new code there.

7b. ramo (originally built for Clue-set A only in v0.525; ported to B and C in v0.531, see §7d)

• Encoding: membero, righto, aftero copied essentially verbatim from ramo’s own README tutorial (its worked zebra-puzzle example) — same as v0.1. Two small custom relations were needed and written in the same recursive shape as ramo’s own combinators: nthValo (indexed access, the ramo analogue of Tau’s nth1/3) and pairedAto (correlates positions across two parallel lists — e.g. organism-list position i and country-list position i both representing “year i’s team”).
• The central discovery, worth understanding before extending this backend: ramo has no native disequality/distinctness primitive — confirmed by checking its complete exported API (Rel, conde, cons/conso, eq, exist, failo, first/firsto, nilo, rest/resto, run, succeedo — nothing else). Without one, an unconstrained “house” can spuriously claim any organism via membero, not just its real one (verified directly: a naive query produced china/usa/hongkong alongside the correct netherlands for what should have been a single-answer query). Fix: precompute all 720 permutations of each category in plain JavaScript (not relationally — ramo can’t derive distinctness on its own without a disequality constraint it doesn’t have), and constrain each category list via membero(list, PRECOMPUTED_PERMS). This plays the exact role Tau Prolog’s permutation/2 played, just computed outside the relational engine instead of inside it.
• Ramo’s search did NOT reproduce Tau’s catastrophic goal-ordering blowup — a pleasant, verified surprise. The exact query shape that took 45+ seconds (and once crashed) for Tau — two categories fully unconstrained, queried jointly — completed in ~100ms for ramo. Ramo’s fair/interleaved relational search appears to be naturally more robust to goal ordering than Tau’s depth-first WAM backtracking. No analogous dynamic ordering fix was needed, and readiness gating was set to “always ready” for every clue (isReadyRamo unconditionally returns true) since no case anywhere near as bad as Tau’s was found (worst measured: a few seconds, not 45+ or a crash).
• Honest reduction in rigor vs. Tau: ramo’s run() needs an explicit sample size — there is no cheap, always-fast equivalent of Tau’s genuinely-exhaustive findall for this backend (unlimited run() for even a lightly-constrained query took ~1.35 seconds for just 120 results). The “newly forced” check here uses a bounded sample (40 results) rather than true exhaustive enumeration: “same value across 40 samples” is strong practical evidence, not the mathematical certainty exhaustive findall gave for Tau. State this plainly if asked about it — it’s a real, documented gap, not hidden.
• A real integration bug, found only by testing the actual assembled page (the standalone Node module worked perfectly in isolation): the browser integration accidentally reused Tau’s VARNAME mapping ({organism:'Organisms', ...}, capitalized, matching Prolog variable-naming convention) inside the ramo query construction, where the actual local variable names are lowercase (organisms, matching the exist((organisms, countries, projects, awards) => ...) parameter names). v[VARNAME[cat]] therefore looked up v['Organisms'] on an object whose only keys were lowercase, silently returning undefined, which broke every ramo query (0 results for every clue, including clue 1 alone, which should give 120). This is exactly the kind of bug that a standalone-module test cannot catch, because the bug is in the wiring, not the logic — a reminder that “verified as a module” and “verified integrated” are genuinely different claims, and both need actually doing. Fixed with a separate RAMO_VARNAME mapping using the correct lowercase keys.
• Some individual ramo queries do measurably slow down (~1.2–1.5 seconds, occasionally 3–4 seconds) as the active clue set grows large late in a playthrough — flagged directly during testing rather than hidden, but this is a different, non-catastrophic kind of slowdown from Tau’s issue, and hasn’t needed a fix.
• Vendored as ramo/dist/bundle.umd.js (the package’s own published UMD build, exposing window.ramo), inlined verbatim, MIT license (Copyright 2019 William Lewis) reproduced in the page.

7c. microKanren (originally built for Clue-set A only in v0.53; ported to B and C in v0.531, see §7d)

• Encoding: a from-scratch microKanren core (MK namespace in the HTML, mirrored by mk-backend.js in the sandbox) transcribed directly from Hemann & Friedman’s paper (“A Minimal Functional Core for Relational Programming,” Scheme Workshop 2013) — call/fresh, disj, conj, ===, and cons-pair list terms, following the paper’s own structure. Correction to this document’s own earlier expectation: §6 originally assumed this would reuse memberoFixed/rightoFixed/afteroFixed relations “from v0.1” — but v0.1’s actual source wasn’t in hand when this was built (only this document’s own description of it was), so rather than guess at an old implementation’s exact shape, the relations (mk_membero, mk_righto, mk_aftero, plus mk_nthValo/mk_pairedAto, the ramo-analogue relations this puzzle also needs) were written fresh against the new core, following the same conceptual definitions as the ramo backend’s versions (themselves transcribed from ramo’s own README). If v0.1 is ever consulted directly, it’s worth diffing against these rather than assuming they match.
• Two deliberate, flagged departures from strict fidelity to the paper:
  1. Streams are eager arrays, not the paper’s lazy thunks. The paper’s laziness exists for potentially-infinite search; this puzzle’s search space is always finite (bounded by the precomputed permutation lists, same fix as ramo’s — see below), so eager arrays were verified sufficient. Consequence: unlike ramo’s genuinely bounded run(N), this backend’s internal search is always fully exhaustive — closer in spirit to Tau’s findall than to ramo’s honest sampling gap. That’s more rigorous than ramo, but it’s also exactly why goal ordering and the readiness gate below matter so much: there’s no early-exit valve to fall back on.
  2. List terms are cons pairs built fresh in JS for this project, not copied from any existing JS microKanren port (none was used or needed).
• Distinctness gap, verified directly (test-mk-distinctness-gap.js): bare microKanren, like bare ramo, has no native disequality/distinctness primitive — two positions of an unconstrained list can be unified to the same value with nothing above forbidding it (confirmed: a 3-slot list with positions 0 and 1 both constrained to 'nematodes' simply succeeds). Fix: the same precomputed-permutation approach as ramo’s, and in fact reusing ramo’s own ramoPermutations() helper directly rather than writing a second generator — it already produces exactly the plain-JS-array permutations needed.
• A real bug in the core itself, found by test-mk-core.js before any puzzle logic was layered on: Array.prototype.reduce called with no initial value on a single- element array returns that element directly, without ever invoking the reducer. Since fresh()’s implementation combined its goals via goals.reduce(conj), any fresh() call wrapping exactly one goal silently returned an un-invoked composed goal (a function) instead of a stream — surfaced immediately as run() receiving a function instead of an iterable and throwing “results is not iterable.” Fixed by explicitly invoking the reduced goal against the current state.
• A real performance bug, found by test-mk-puzzle.js’s per-clue timing probe: under the naive goal order (all category-membership constraints first, every active clue’s own constraint appended only at the very end), a full 23-clue sequential playthrough took 20.2 seconds total, with individual clue queries as slow as 8.3s (clue 10) and 6.1s (clue 17) — the same flavor of blowup Tau Prolog hit before its own dynamic-ordering fix (§7a), for an analogous reason: an unconstrained ~720-permutation category, joined to another before anything filters it, gets fully cross-multiplied by eager bind. Fix, re-derived for this engine’s own dispatch shape rather than copied from Tau’s raw-Prolog-goal reordering: (a) sort categories most-known-first, so a still-open category gets cross-multiplied against an already-narrow prefix instead of a full 720; (b) splice each active clue’s own goal into the chain as soon as every category it touches has been introduced, instead of waiting until every category goal has run. This brought the same 23-clue playthrough down to ~3.1–3.3 seconds total, worst individual query ~750ms.
• A more severe bug that survived the reordering fix, found by test-mk-stress.js: reordering alone doesn’t help a genuinely cold query — e.g. clue 10 (organism + award) applied first, with both categories still fully open. This didn’t just run slowly; it crashed Node with an out-of-memory error, materializing the full 720×720 cross product with nothing yet available to prune it. This is the identical shape of problem §7a documents for Tau (which needed an explicit readiness gate, not just goal reordering, to stay safe), independently re-derived here rather than reused verbatim (Tau’s gate reasons about raw Prolog goal order; this one reasons about which JS category-vars are still fully open). Fix: isReadyMK, gating any clue that touches more than one category until at least one of those categories has >=5/6 rows already known — empirically, the exact same threshold Tau independently settled on generalizes here too. Verified both necessary (4/6 known measured slow/risky in test-mk-readiness.js) and sufficient (5/6 known resolves in well under a second, and the natural 1→23 clue order never actually triggers the gate, since organism reaches full knowledge early and every later two-category clue rides on that).
• No name-mapping table, by design — unlike Tau’s VARNAME (capitalized) vs. ramo’s separate RAMO_VARNAME (lowercase, added only after the capitalization mismatch broke every ramo query, §7b), this backend’s clue-goal variable keys (organisms/countries/projects/awards) are used directly as the object keys passed into clueGoalMK, with no separate mapping table to fall out of sync in the first place. A deliberate design choice to avoid re-introducing that exact class of bug, not a claim that the underlying risk doesn’t exist in other forms.
• Verified integrated, not just as a standalone module — same testing-discipline point §7b makes about ramo’s VARNAME bug: run-mk-integration-test.js clicks real buttons against the real, assembled igem-puzzle-v0.53.html (not just the standalone mk-puzzle.js module) and confirms the rendered grid matches the real answer exactly. run-full-regression.js then re-ran every other supported (engine, clue-set) combination in the same integrated file to confirm nothing else broke.

7d. Porting ramo and microKanren to Clue-sets B and C (v0.531)

Goal: all three engines support all three clue-sets. Built and verified in standalone modules first (ramo-shared.js/ramo-puzzle-bc.js and the B/C additions to mk-puzzle.js, plus test-ramo-bc.js/test-ramo-bc-stress.js and test-mk-bc.js/test-mk-bc-stress.js), same discipline as every other engine addition, before touching the HTML.

• Two new relations needed, shared by both engines’ ports (built once conceptually, implemented separately per engine’s own primitives, same pattern as membero/righto/ aftero/nthValo/pairedAto already being independently re-derived per engine rather than shared as literal code):
  • offsetK(r, l, xs, k): r’s position is exactly k positions after l’s, for a fixed positive integer k. This generalizes a pattern clue-set A’s own clue 9 already used (two chained rightos through one intermediate existential, for a fixed offset of 3) to an arbitrary k — clue-sets B and C between them need offsets of 1 through 5 (B chains forward from the Dutch team’s year; C chains backward from the German team’s, i.e. the same relation with the “later” and “earlier” arguments swapped). Implemented recursively: offsetK(r,l,xs,1) = righto(r,l,xs); offsetK(r,l,xs,k) = exists m: righto(m,l,xs) AND offsetK(r,m,xs,k-1).
  • pairedAtoAmong(listA, valA, listB, candidates): listB’s value at valA’s position is SOME member of candidates, not one fixed value. This is the relation clue-set C’s award/project clues need — Tau’s Prolog source encodes those clues as genuine negation-as-failure (\+ member(A, blacklist)), but neither ramo nor bare microKanren has a negation-as-failure primitive (checked directly against both engines’ complete primitive sets — see §7b and §7c). Over a finite, fixed 6-value domain, though, “value NOT IN blacklist” and “value IN (fullDomain MINUS blacklist)” are logically identical, so the complement set — computed once, by hand, from the exact blacklist already hardcoded in CLUESET_DATA.C.prolog — is a faithful translation of the negation, not a shortcut around it. Verified this collapses to exactly the single correct candidate for every one of C’s actual award/project clues (12–21), though the relation itself is implemented as a genuine disjunction over the whole complement set (via conde over the candidates array), not a hardcoded singleton, so it would behave correctly even if a future clue-set had a multi-candidate complement.
• Clue-set B’s relative-order clue (its clue 3: “the yeast team’s year was earlier than Black Soldier Fly’s and later than cyanobacteria’s”) needed no new relation — it’s just two aftero conjuncts (yeast after cyanobacteria AND Black Soldier Fly after yeast), the same relation clue-set A already needed.
• Performance, verified per engine, not assumed to generalize from clue-set A:
  • ramo: worst-case query time for B and C landed around 2–3 seconds (a full 22/21-clue sequential playthrough took ~23–26 seconds total, vs. clue-set A’s ~few hundred ms per clue) — slower than A but still squarely in the “a few seconds, not a crash” territory that led to isReadyRamo returning true unconditionally for A; directly stress-tested cold two/three/four-category B/C queries (test-ramo-bc-stress.js) and confirmed none exceeded ~500ms even fully unconstrained, so no readiness gate was added for ramo on B or C either — this was verified freshly for the new clue-sets, not inherited on the assumption that “ramo was fine before.”
  • microKanren: the existing >=5/6-known readiness gate (§7c) was reused as-is (isReadyMK/isReadyMKGeneric already read the per-clue-set category map generically via curData().cats, needing no clue-set-specific change) — but this was verified, not assumed: test-mk-bc-stress.js deliberately forced a cold two-category B/C query (bypassing the gate) and confirmed it does OOM, exactly like clue-set A’s cold query did. This confirms the gate is genuinely necessary for the new clue-sets too, not just carried over defensively.
• A design decision, not a bug: rather than have applyClueRamo/applyClueMK branch internally on SELECTED_CLUESET, each engine’s clue-goal function was split into three separate functions (ramoClueGoalA/B/C, clueGoalMK_A/B/C) with a thin dispatcher on top (ramoClueGoal, clueGoalMK) selecting by SELECTED_CLUESET — mirroring how CLUESET_DATA itself already separates A/B/C content, rather than interleaving three clue-sets’ switch cases into one function.
• A stale-documentation bug caught while making this change, unrelated to the port itself: the page’s own footer (<footer>Version 0.525 (ramo engine added, Clue-set A only...)</footer>) had not been updated when microKanren was added in v0.53 — it still said “0.525… Clue-set A only” even in the v0.53 file. Fixed as part of this change (now correctly describes v0.531’s state); worth checking this footer specifically whenever future versions ship, since nothing else in the codebase enforces it stays in sync with the actual version number.
• Full regression, not just the new pieces: run-full-regression.js was extended from checking “ramo/microKanren + B/C should be correctly disabled” to actually playing through all nine (engine, clue-set) combinations against the real, integrated igem-puzzle-v0.531.html and checking the rendered grid — all nine converge on the real answer.
• A test-harness quirk, not a product bug, worth knowing if this happens again: running all nine combinations back-to-back in one node process occasionally hit Node’s default heap ceiling and crashed with an out-of-memory error — but re-running with node --max-old-space-size=4096 passed cleanly every time, and the crash’s location (accumulated JSDOM window instances across nine sequential combinations in a single process) has nothing to do with the puzzle logic itself: a real user’s browser only ever has one such window open, not nine in a row. Distinct from the genuine product-level OOM bugs documented in §7c/§7d above (those reproduce inside a single, isolated query and are about the puzzle’s own relational search, not test-harness accumulation) — don’t conflate the two if this surfaces again.

7e. Fixing the five §1a issues (v0.533), and a real concurrency bug found along the way

All five issues noted during v0.532 (§1a) were fixed in v0.533. Four were small and self-contained; the fifth (the Apply-button responsiveness fix) surfaced a genuine new bug that needed its own fix on top of the original one.

• Broken FitchFX image (issue #1): fetched the actual icon from FitchFX’s own upstream repo (raw.githubusercontent.com/mrieppel/FitchFX/master/img/github.png, same MIT-licensed source everything else here comes from) and inlined it as a base64 data URI in place of the dead relative path. This is the one deliberate departure from “byte-identical to upstream,” flagged directly in the vendoring comment itself rather than left for the claim to quietly go stale (see §9’s general point on flagging departures explicitly).
• Fitch coverage / star-clue explanations (issues #2 and #3): added renderFitchCoverageNote(), rendered once per session start into a new #fitchCoverageNote div placed right above the clue list. Fixing this surfaced an extra find: the static text above the Fitch panel already said “see the note above the clue list for which [clue types aren’t translated]” — but no such note had ever actually existed. That sentence had been a dangling promise since whenever it was first written; renderFitchCoverageNote() is what makes it true now, not a new invention on top of an already-accurate claim.
• Blocking Apply clicks (issue #4): added a real yield point (await new Promise(r => setTimeout(r, 0))) between setting the “Querying…” button state and calling into applyClue(), so the browser actually gets to paint that state before the heavy synchronous computation runs (confirmed necessary: ramo’s and microKanren’s applyClue* functions have zero internal await points, so nothing else would have yielded control).
• Local before/after feedback (issue #5): added totalKnownCount() (same counting expression already used by this project’s own test scripts, just promoted into the shipped page) and a “Facts known before this click: x → after: y” message rendered unconditionally in each clue’s row, generalizing the pre-existing zero-progress .hint mechanism rather than replacing it — the more specific noProgress hint (when one exists) still renders right underneath the new general message.

A real regression found while testing issue #4’s fix, not a separate pre-existing bug: before this fix, every engine’s applyClue* ran as one uninterrupted synchronous block — which, entirely by accident, meant only one query could ever be in flight at a time, since nothing yielded control back to the event loop mid-query. Adding a genuine yield point removes that accidental mutex: two Apply clicks close enough together can now both reach their query call before either resolves, launching two overlapping queries against the same shared Tau Prolog SESSION object. Confirmed directly, not just suspected: a from-scratch sequential-clicking test crashed with an out-of-memory error at exactly the point two queries would have overlapped (specifically, Tau Prolog + Clue-set A, clue 10, when country and award were both still fully open) — the identical test without the yield-point fix never crashed there. Tau’s session isn’t designed for concurrent queries, so the yield-point fix on its own was actually unsafe to ship without a second fix alongside it: a QUERY_IN_FLIGHT lock, checked and set at the top of the click handler, that disables every Apply button (not just the one clicked) for the duration of a query, and is read by renderClueRows()’s own disabled-state logic so any render respects it. Verified this actually fixes the crash (the same from-scratch test that crashed before no longer does), and re-ran the full 9-combination regression suite afterward to confirm no other combination regressed.

Two of the project’s own test scripts needed the same kind of fix, for the same reason: run-full-regression.js and test-click-count.js both originally waited a short fixed delay after dispatching a click before assuming it had fully resolved (30ms and 150ms respectively) — safe under the old fully-synchronous behavior (a click was guaranteed complete by the time any fixed delay elapsed), not safe anymore now that there’s a genuine yield point and an explicit lock gating completion. Both were rewritten to poll for the button set actually re-enabling (doc.querySelector('#clueRows button:not([disabled])')) rather than guessing a sleep duration — this is also the more correct way to write a test like this regardless of which engine is being exercised, since Tau’s exhaustive findall on Clue-set B/C’s later clues can genuinely take longer than ramo’s or microKanren’s equivalent queries, and a fixed guess that happens to work for one engine isn’t guaranteed to work for another.

7f. The Engine trace panel was dead UI for two of three engines (v0.534)

Reported directly (screenshot showing “No trace recorded for this action” after applying a clue on Clue-set C): the “Engine trace (last action)” panel appeared useless. Confirmed it wasn’t just that particular action — it was every action, for two of the three engines, permanently:

• renderTrace(res) only ever checked res.trace. If falsy, it always rendered the generic “No trace recorded for this action.” message and returned, discarding everything else on res.
• applyClueRamo and applyClueMK both unconditionally set trace: null — neither engine has anything resembling Tau’s debugger_states, so there was never a plan for this to be populated any other way.
• But both functions were already computing a real, accurate one-line summary (res.query) describing the actual query just run — categories involved, active clues, result count, elapsed time — and renderTrace never looked at it. That data existed and was thrown away, not merely absent.

Fix: rather than fabricate step-by-step resolution the way Tau’s debugger produces (neither engine has any mechanism that could genuinely produce that), both applyClueRamo and applyClueMK now also build res.steps — a real, accurate, numbered log constructed from data they already compute during goal construction: one line per category (whether it was pinned outright from already-known facts, or searched over its 720 permutations and how many positions constrained it), one line per active clue that fired (its number, its text, and which categories it touches), and a final line with the result count and elapsed time. renderTrace was updated to check res.trace first (Tau’s real resolution steps, unchanged), then fall back to res.steps (the new per-engine goal-construction log) before finally falling back to the generic message — so that generic message is now reachable only when neither exists, rather than being the default outcome for two-thirds of the engine options.

Verified directly (test-trace-panel.js): clicking a clue on ramo and on microKanren now shows genuine, non-fabricated content in both the header and body of the trace panel, where before both always showed the same static fallback text regardless of which clue was clicked. Confirmed the numbers in that content are real by cross-checking them against each engine’s own already-established behavior (e.g. microKanren’s step count matching its genuinely-exhaustive solution count, not a sampled one, consistent with §7c’s documented distinction from ramo’s bounded run()). Full 9-combination regression suite re-run afterward, still all-pass.

7g. The Action-effect log (v0.541, radical redesign, user-specified version number)

The requirement, as specified by the user, nearly verbatim: track which rule applications reveal facts, even facts already revealed before — present this as a log where the first-ever reveal of any fact is emphasized (bold), and once every fact is known, further actions are logged as wasted effort.

Why this needed real changes, not just a new display: every engine’s fact-detection loop (applyClueTau/applyClueRamo/applyClueMK) had always skipped already-known cells outright — if (KNOWN[r][cat]) continue; — because the only thing that mattered before was newFacts (genuinely new information to merge into KNOWN). That skip meant there was no way to tell whether a query had re-confirmed an already-known fact or simply never touched that cell at all; the information the new feature needs didn’t exist anywhere to log. Fixed by removing the skip in all three loops: every forced cell is now recorded into a new revealed array (a superset of newFacts), and newFacts is derived from it by filtering to cells not already in KNOWN — same final behavior for everything that already depended on newFacts (verified via the full regression suite, unchanged), with the strictly-additional revealed array carried alongside it in each function’s return value.

New session-level state (same never-reset-mid-session lifetime as KNOWN/ACTIVE/ CLUE_CLICK_COUNTS — no “back to setup” control exists on this page): - ACTION_LOG: one entry per Apply click, in the single global order they happened, each listing every fact that click’s query forced (or a wasted: true marker). - ACTION_COUNTER: a 1-indexed action number across the whole session — distinct from CLUE_CLICK_COUNTS, which counts clicks per individual clue; this counts actions in the single sequence the log presents. - FACT_REVEAL_COUNT: keyed by "row-field", incremented every time that fact is revealed by any action. A fact’s first-ever reveal is exactly when this reads 1 after incrementing — the same event KNOWN newly acquiring that fact marks, tracked by a separate counter because the feature needs an actual count (“revealed 2nd time”), not just a yes/no.

The wasted-effort check lives in the shared applyClue() dispatcher, not duplicated per engine: once every one of the 24 knowable facts (6 rows × 4 categories — the same ceiling renderKnownGrid’s own comment already establishes) is in KNOWN, no further query against any engine could possibly reveal anything else. This is a mathematical guarantee, not a heuristic, so it was implemented as an early return in applyClue() itself — before any engine-specific function is even called — which has the added benefit of skipping a pointless query entirely once the puzzle is solved, rather than running (and paying for) a full search that’s provably going to find nothing new. This matters more for ramo’s and microKanren’s heavier searches than Tau’s, but applies to all three uniformly since the check is engine-agnostic.

Rendering: a new panel (“Action-effect log”) was added to the main layout, below the existing Engine trace panel, with its own render function (renderActionLog()) called after every click and once at session start. Unlike the plain-text trace panel, this one uses innerHTML (not textContent), since the whole point is bolding first reveals — each action’s entry is either a “Wasted effort” line, or one line per revealed fact, phrased as “First reveal of row R (year), Category = value.” (bold) or “Re-revealed row R (year), Category = value (revealed Nth time).” (plain), using a small hand-written ordinal-number formatter for the “Nth” phrasing.

Verified directly (test-action-log.js), not just by inspection: clicking a clue for the first time produces a bolded first-reveal entry; clicking the same clue again (after that fact is already known) produces a plain “re-revealed… 2nd time” entry, not another bolded first-reveal; playing through an entire clue-set to all 24 facts known and then clicking once more produces a “Wasted effort” entry. Full 9-combination regression suite re-run afterward, still all-pass, confirming the fact-detection loop change didn’t alter any engine’s actual solving behavior — only what gets recorded about it.

Relationship to §1b’s proof-coherence requirement: this is a genuinely different, smaller piece of work than §1b’s tier 1/tier 2 plan — the action-effect log records what was revealed and when, across the literal sequence of clicks, but doesn’t construct or verify that the sequence forms a valid proof (no inference rules, no minimal-support-set computation, no case-split reasoning). It’s a useful complementary piece of infrastructure for that future work (a per-action list of exactly what changed is a natural input to a support-set computation), but doesn’t substitute for it — §1b remains open and out of scope for this version.

8. The Fitch proof panel (FitchFX integration)

History: two candidates were researched and one was abandoned mid-integration once a better match was found — worth knowing both, since the abandoned one (ndt93/Proof-Editor) is still sitting in the outputs directory as a working two-file fallback (v0.522/523).

• ndt93/Proof-Editor (MIT, github.com/ndt93/Proof-Editor): a real, working, MIT-licensed Fitch editor — but propositional logic only (no native quantifiers/predicate-argument structure). Verified working end-to-end (real Modus Ponens applied via its actual UI, correct result). Used in v0.522/523, superseded once a better match was found.
• mrieppel/FitchFX (MIT, github.com/mrieppel/FitchFX, actively maintained through 2025 by the same author as the earlier mrieppel/fitchjs): genuine first-order logic support, including real quantifier rules (AE/∀-Elim, AI/∀-Intro, EE/∃-Elim, EI/∃-Intro) with proper name-flagging and subproof handling — not a toy. Adopted in v0.524 and current.
• Syntax discovered empirically, not from documentation alone: FitchFX requires single-letter names (a–t) and single-letter variables (u–z) — classic forallx/Barwise-Etchemendy convention. Multi-character constants are flatly rejected (“unrecognized character,” confirmed directly). Multi-argument predicates use direct letter concatenation with no parens/commas (Rab = R(a,b), confirmed from FitchFX’s own on-page reference table).
• The translation scheme (Claude-authored, but pure data-formatting — the actual proof validation, quantifier-rule checking, and rendering are entirely FitchFX’s own unmodified code, invoked via its real import_proof() function): each translated clue application is its own independent FitchFX “Problem” — no global naming registry is needed, since each is a separate context. A small fixed local scheme is reused for every one: x = the universally-quantified variable, a = the specific year being instantiated, b = the antecedent’s value, c = the consequent’s value (d if a second consequent value is ever needed) — with a plain-English legend shown alongside each (“a = 2020, b = Nematodes, c = Netherlands”).
• Verified with a fully closed loop, not just “looks right”: the actual generated output of the real translation function (from a genuine Tau Prolog-derived fact) was fed into a fresh, separately-loaded FitchFX instance, and it returned “Proof successfully imported. Proof is complete!” — confirming the whole pipeline, not a hand-typed lookalike.
• Scope, stated honestly: only 13 of Clue-set A’s 23 clues are auto-translated — the ones of the shape “single universal premise + one already-known fact → ∀-Elimination + Modus Ponens” (clues 6, 7, 8, 10, 11, 13, 14, 15, 17, 18, 19, 21, 23). Not yet translated: the organism-year block (clues 1–5 — this would need a genuine reductio/case-exhaustion translation, since the engine solves this block as one atomic query with no natural step-by-step structure to translate), the Hong Kong-offset clues (9, 22), the award-injectivity move (11+12’s interaction) and clue 16 (joint country+award derivation), and clue 20 (fixed fact, no real inference to show). Not wired to ramo at all — only active when Tau Prolog is the selected engine. Not extended to Clue-sets B or C.
• One real bug found during this integration: after replacing the ndt93 section with the new FitchFX one, the notation-legend and full-FOL-clue-list reference elements (#notationLegend, #folClueList) were accidentally dropped from the HTML while renderFitchReference() still referenced them — a null-reference crash on session start. Caught immediately by the regression suite, fixed by restoring the elements.
• A genuine, documented testing limitation, not a functional bug: jsdom does not reliably render <iframe srcdoc="..."> content (confirmed with both the full vendored app and a trivial one-button test case — both produce an empty body in jsdom despite readyState: 'complete' and no load event firing). This means the live iframe click-through specifically could not be verified via the automated test suite; what was verified independently and directly is (a) the translation function’s exact output, and (b) that exact output validating correctly in a fresh, separately-loaded FitchFX instance outside the iframe. Both pieces are proven; the live iframe wiring itself should be spot-checked in an actual browser if this area is touched again. Separately, FitchFX’s own SVG drawing needs SVGElement.prototype.getBBox, which jsdom also doesn’t implement — worked around in tests with a stub (getBBox: () => ({x:0,y:0,width:100,height:20})); real browsers don’t need this.

9. Open-source dependencies (complete list, with license and role)

Researched but explicitly rejected, for future reference (don’t re-research these): - OpenLogicProject/fitch-checker and its successor LogicPenguin (Kevin Klement) — both GPL-3.0, ruled out by the permissive-license-only constraint. - Carnap (carnap/carnap) — GPL-3.0, same reason. - dramala/prolog-Natural-Deduction — no license file at all (defaults to all-rights-reserved), ruled out regardless of content. - A dedicated “translate a Prolog resolution trace into a Fitch proof” open-source tool was searched for directly and not found with a permissive license — the closest match (a 2021 bachelor’s thesis, “Towards Automated Natural Deduction in Prolog”) does something adjacent but different (searches for proofs from scratch, doesn’t translate an existing trace), and its code availability/license is unconfirmed. This is why the FitchFX translation layer (§8) is Claude-authored data-formatting rather than a found open-source translator — there wasn’t one to find. - shimmer (BSD-2-Clause) and cowboy/javascript-hooker (MIT) were identified as good candidates for instrumenting ramo/microKanren with real open-source function-wrapping code (see the original architecture spec §8), intended for adding a trace/logging capability to those backends. Not yet actually vendored or used — ramo’s current trace (§7b) is just a descriptive string, not instrumented via either of these. Worth revisiting if a richer ramo trace is wanted later.

10. In-code provenance tagging convention

Established in igem-puzzle-v0.521.html and maintained since. Every block of original code/content in the final (non-vendored) <script> section is tagged with one of:

• [USER INSTRUCTION] — the human operator explicitly directed this change or requirement. Quoted or paraphrased where practical.
• [CLAUDE INITIATIVE] — Claude Sonnet 5 designed this without being told the specific approach (a bug found and fixed during testing, an implementation detail chosen to satisfy a broader requirement, or puzzle content authored to satisfy a user-stated constraint without the user specifying the actual content).
• [USER CONTENT] — content originating from the user, not a coding instruction (specifically, the original iGEM puzzle and Clue-set A, supplied directly by the user).
• [OPEN SOURCE] — code imported from a permissively-licensed project, unmodified, or written to directly follow that project’s own documented API.

As of v0.532 (current), the exact tag count in the main script (not a rough estimate — counted directly during the v0.532 audit) is: 25 [USER INSTRUCTION], 68 [CLAUDE INITIATIVE], 8 [USER CONTENT], 11 [OPEN SOURCE]. When extending the code, keep tagging as you go, in the same pass as writing the code — two audit passes now (v0.521 and v0.532) have each found real gaps or drift that accumulated silently between them, which is more error-prone than tagging immediately and checking periodically.

11. Testing discipline (the pattern to keep using)

Every version in this project has been verified by actually running it — clicking real buttons in a real (simulated) DOM via jsdom, reading the actual rendered output — not by code review alone. This discipline is why so many real bugs got caught before shipping rather than after:

• The original 20-clue puzzle had two solutions (caught before any UI code existed, by running an actual solver).
• Tau Prolog’s goal-ordering blowup, and the 31,815-step trace problem (§7a).
• FitchFX’s exact plain-text syntax, determined by actually running it and reading its own export output, not guessed from documentation.
• Two of clue-set C’s four bugs (§5), plus the accidental B/C wording duplicate.
• ramo’s distinctness gap, and the VARNAME capitalization bug (§7b) — the latter specifically was invisible in standalone-module testing and only surfaced once the actual integrated page was tested.
• microKanren’s own single-goal Array.reduce bug in the core (§7c), its goal-ordering performance blowup (20.2s down to ~3.3s for a full playthrough), and — most severely — a genuinely cold two-category query that didn’t just run slowly but crashed with an out-of-memory error, caught by a dedicated stress test (test-mk-stress.js) written specifically to probe the worst-case shape before trusting the reordering fix alone, the same way Tau’s own worst case was hunted down rather than assumed fixed.
• The B/C port (v0.531) re-verified rather than assumed its predecessors’ findings still applied: test-ramo-bc-stress.js confirmed ramo’s B/C clues stay fast even cold (not inherited from clue-set A’s finding without re-checking), and test-mk-bc-stress.js confirmed microKanren’s B/C clues do OOM cold, exactly like clue-set A’s did — both results could have gone the other way and weren’t assumed.
• A stale-documentation bug: the page’s own version footer still read “Version 0.525… Clue-set A only” inside the v0.53 file, missed when microKanren was added — caught and fixed while making the v0.531 change, not before.
• A dedicated provenance-tagging audit (v0.532), not just incidental testing: every top-level function/const/let declaration in the main script (73 of them) was checked for a preceding attribution tag, distinguishing genuine gaps from declarations correctly covered by a shared block-level tag above a group of related functions. Found and fixed three real instances of the exact “tag drift” problem the v0.521 audit first identified (a comment describing something that used to be true, silently left behind by a later change): the comments above ENGINES, and above the ramo and microKanren backend blocks’ own headers, all still asserted “Clue-set A only… B and C have not been ported” — accurate when first written, false since the v0.531 port, never updated at the time. Also found a smaller, genuine gap (not drift): ramoClueGoalB/ ramoClueGoalC and clueGoalMK_B/clueGoalMK_C had no explicit tag restating the ordinary user-content-vs-Claude-encoding split that ramoClueGoalA/clueGoalMK_A each have directly above them — the B/C port’s own tag explained the two new relations needed, but never separately re-stated that split for the clue-goal functions themselves. All four fixes were verified not to have broken anything (full 9-combination regression suite re-run afterward, still all-pass) — a tag is documentation, but editing the comments immediately next to live dispatch code is exactly the kind of change worth re-testing rather than assuming is inert.
• Two provenance-adjacent bugs: a \u2013 escape leaking into plain HTML (§2, v0.521), and dropped notation-legend elements during the FitchFX section rewrite (§8).

When extending this project: write a standalone test script, run it, read the actual output before believing it, and re-run the full existing regression suite (not just the new piece) after every change. The test files (run-v52*-test.js and similar) in the project sandbox show the established pattern — reuse and extend them rather than starting from scratch each time.