Substrate-derived priority list of cited textbooks not yet
ingested, with record-count impact per acquisition. Walks every
unresolved claim-pack record's parsed citation and counts which
authors + titles appear most frequently — that count IS the
prioritized roadmap.
Top targets (records resolved per acquisition):
Stanley Enumerative Combinatorics 11 pillar VII
Jech Set Theory 10 pillar II
Brualdi Introductory Combinatorics 9 pillar VII
Knuth TAOCP 9 pillar VII
Mendelson Intro to Math Logic 7 pillar I
Landau Foundations of Analysis 7 pillar III (PD-by-age original)
Barendregt Lambda Calculus 7 pillar IX
Enderton Math Intro to Logic 6 pillar I
Gödel On Formally Undecidable 6 pillar III (PD-by-age original)
Dummit + Foote Abstract Algebra 6 (algebra)
Kolmogorov Foundations of Prob. 5 pillar V (PD-by-age original)
Goldstein Classical Mechanics 5 pillar VI
Three buckets: PD originals (multilingual scope), proprietary
modern textbooks (per-textbook license decision matrix), and
already-ingested-but-resolver-misses (7 Hilbert records whose
discriminating tokens — "Incidence", "Plane", "Line" — are too
common in the text for BM25 to rank the right chunk).
Recommended path per textbook documented in §3.1: skip /
personal-copy ingest / PD substitute / negotiate-redistribution.
Hilbert-Ackermann 1928 noted as PD substitute for Mendelson +
Enderton; Newton's Principia (already ingested) as substitute
for Goldstein.
Citation-aliases mechanism proposed in §3.2 — `arborist
citation_aliases` table mapping original cite → substitute,
read at warrant-resolve time. Cleaner than re-authoring claim-
pack bundles; original citations stay intact.
Hilbert resolver-miss (§6) flagged as a separate Phase 5
follow-up — fix candidates: TF-IDF over BM25, exact-axiom-name
phrase boost, claim-content-as-FTS-query.
The substrate writes its own roadmap.
A `make docs-api-clean && make docs-api` cold rebuild now succeeds
with zero WARNING/ERROR lines (was 39).
Docstring fixes (RST hygiene — no semantic change):
- arborist/qa/{keys,runner,query,verify,quantifier,metacognition,dag,
evidence}.py — add blank lines around indented blocks, convert
ad-hoc indented sections to literal blocks (`::`), avoid line-broken
inline literals (e.g. UNKNOWN_EVIDENCE_ID), and replace nested
bracket/quote literals with cleaner wording.
- arborist/concepts/__init__.py — wrap function-signature listing in
a literal block so bare `*` (kwarg marker) doesn't trip docutils.
- arborist/store.py — blank line before bullet lists in module +
connect docstrings.
- arborist/evict.py — replace ad-hoc `{ ... }` enum block with prose.
Surface fixes:
- docs/_source/_ext/makefile_targets.py — escape `*` in auto-
generated Makefile target descriptions (covers `*-parallel`,
`*.dot`, `*.db`, `π*`, etc.) so the generator emits clean RST.
- docs/_source/index.rst, concepts.rst — extend title underlines
to match title length.
- docs/_source/concepts.rst, v8-fork-score.rst — widen first column
of grid tables so cells no longer overflow into the column margin.
- docs/_source/merkle-agi-v7w-spatial-temporal.rst — switch
pseudocode JSON block from `code-block:: json` to `text` (the
`<int32 x 3>` placeholders aren't valid JSON tokens).
Verification:
- make docs-api-clean && make docs-api → build succeeded, 0 warnings
- make test → 1588 passed, 28 skipped
- make chain-check-shards → 0 breaks across all 7 shards
- import-time SyntaxWarning escalation on edited modules → clean
Closes the warrant-promotion data path: claim-pack records now
bind to surface-ingested textbook chunks via Merkle inclusion
proofs in the existing `derivations` table.
What landed
===========
arborist/qa/warrant_resolver.py — four pure-data steps + one DB
write:
1. parse_citation(s) — regex pipeline turning the claim-pack
`source_reference` string into structured Citation tuples.
Handles "Title by Author" (single + Oxford-comma multi +
et-al), semicolon-separated multi-cite ("Knuth §1.2.6;
Stanley §1.2; Brualdi §3.5"), and compact author-year
("Pascal 1654") forms.
2. resolve_chunks(c, shards_dir) — FTS5 search across sibling
crawl/ dir's textbook-surface shards. Skips the main numbered
shards (Wikipedia content; would be false positives). Per-
shard match filter requires BOTH author last name AND a title
token in the shard's title-haystack — honest "no match" for
textbooks not yet surface-ingested.
3. compute_proof(shard, doc_root, chunk_id) — reads
merkle_nodes, walks layer-by-layer to assemble siblings;
emits deterministic JSON proof_blob compatible with
arborist/merkle.py verification.
4. write_derivation(...) — INSERT OR IGNORE into the existing
derivations table with process_id="warrant-resolver-v1".
Idempotent at the database layer.
CLI surface
===========
- `arborist warrant-status --shards-dir ...` (read-only) —
emits per-record JSON: parsed citations, FTS5 candidates,
whether a derivations row exists.
- `arborist warrant-resolve --shards-dir ... [--write]` —
default dry-run summary; --write actually computes proofs
and inserts rows.
End-to-end verification
=======================
Real-shard run: `arborist warrant-resolve --shards-dir
~/.arborist/shards --write` →
records_total: 92
records_resolved: 18
derivations_written: 18
All 18 are pillar-IV Hilbert axioms citing "The Foundations of
Geometry by David Hilbert" — the only cited textbook fully
surface-ingested by Phase 1. The remaining 74 records cite
textbooks not in our shard cluster (Mendelson, Enderton,
Jech, Goldstein, Barendregt, Stanley, Brualdi, Knuth, …) and
correctly produce 0 matches; they stay at ANCHOR-WARRANTED
until those textbooks land via future Phase-1 manifest
expansions.
Re-running the writer is a no-op (PK collision on (core_root,
src_root, process_id) = INSERT OR IGNORE).
Drive-by fix
============
arborist/sources/textbook_tex.py — _extract_title now also
parses PG's plain-text `Author:` line and appends "by Author"
to the title, so the warrant resolver's author-last-name match
works against PG-ingested textbooks (Hilbert "The Foundations
of Geometry by David Hilbert" instead of just "The Foundations
of Geometry").
Test suite
==========
tests/test_warrant_resolver.py — 14 unit tests for the citation
parser (no DB / network). Full suite: 1588 passed / 28 skipped.
Phase 3 (verifier wiring)
=========================
NOT in this commit. The data substrate is in place; the
audit_mode upgrade path that lifts answers citing
claim-pack-records-with-derivations from ANCHOR-WARRANTED to
EVIDENCE-WARRANTED requires a verifier change — touches well-
tested code, worth its own ticket so the regression risk is
bounded.
Two small Sphinx hygiene fixes surfaced while fox was building the
docs locally:
1. docs/_source/merkle-agi-v7w-spatial-temporal.rst was authored
earlier this session (#000013) but never added to a toctree
so Sphinx flagged it as orphan. Slotted under "Substrate"
alongside pi-star / bench / v8-fork-score where it belongs.
2. The same file had |translation_max| as raw text in an
ε-bound expression; RST parsed the pipes as a substitution
reference and errored. Wrapped the expression in double
backticks so it renders as literal math.
Build now drops from 40 warnings (counting docstring noise) to
5; the 5 remaining are pre-existing module-docstring formatting
in arborist/qa/*.py that pre-date this work.
Reviewer-flagged errata in the dav1dprometheus comm doc surfaced
two real drifts in canonical docs that needed correction:
docs/_source/pi-star.rst:
- "Fifteen concrete π*'s" -> "Sixteen". The table was missing
combinatorics@v1 (#000032). Authoritative count comes from
arborist.pi_star.registry.REGISTRY itself, with a note saying
so. Each entry called out as behaviorally immutable, with
forward link to docs/spec-methodology.md section 1.1 where the
versioning rule is canonical.
docs/dav1dprometheus-update-2026-05-09.md:
- Reverts a regression introduced in the previous errata pass
(455fc10). The reviewer counted 5 axes x 5 = 20 sub-batteries,
but 5T carries 6 (legacy 'transfer' from SQD-whitepaper plus
the canonical Dav1DPrometheus five, kept side-by-side per
ticket #000024). Total is 21, not 20. Top-of-doc revision
note records the correction, body section restores the 21
count with the explicit 5+6+5+5 explanation.
Other reviewer points are already canonical (kernel-version
immutability is in docs/spec-methodology.md section 1.1) or are
editorial-only and don't require canonical-doc changes.
Tested:
- len(REGISTRY) == 16 (verified live)
- bench/batteries/runner.py enumerates 21 sub-batteries
(5+6+5+5 per file naming under bench/fixtures/5{s,t,f,r}/)
External reviewer surfaced several errata in the 2026-05-09 draft.
Corrections applied in-place; original draft is preserved at
commit a2ff9d4.
- sub-battery count: 21 -> 20 (5 axes x 5)
- 5S vocabulary fix:
Surface/Substrate/Synthesis/Semantics/Semiotics
-> Syntax/Semantics/Syllogism/Synthesis/Semiotics
(matches bench/batteries/b_5s.py)
- 5R vocabulary fix:
React/Recall/Reason/Refine/Restore (reviewer's guess; doc's
original was even less correct)
-> React/Rearrange/Restore/Replicate/Resonate
(matches bench/batteries/b_5r.py per SQD section 9.3)
- pi* kernel chronology: explicit "15 -> 16 with combinatorics@v1"
- kernel-version immutability: stated as hard invariant (no
in-place behavioral mutation; behavior change = new version)
- cross-witness vs cross-carrier: distinguished. Witness channels
are kernel/cache/LLM; carrier modalities are
text/code/arithmetic/etc. The pattern generalizes from the
former to the latter but the audit semantics are distinct.
- STRICT-WITNESSED is a render label, not a new audit_mode.
Persisted column stays CANONICAL_PROJECTION; witness audit
event layers on top so cache_key semantics don't drift.
- warrant-promotion ladder: SOURCE-ANCHORED tier introduced
between ANCHOR-WARRANTED (assertion-only) and
EVIDENCE-WARRANTED (chunk-proof). Today's surface-ingest
work delivers SOURCE-ANCHORED; chunk-resolution layer is
needed for EVIDENCE-WARRANTED.
- license tags marked project-reported (manifest self-attest;
not independently audited by counsel)
- "no human labelers" scoped to canonical-shape divergence
labels only; claim-pack validity + textbook warrant
promotion still benefit from human curation
- top-of-doc revision note records the errata pass
- closing footer updated to reflect today's CI re-enable +
shard-search fan-out (66s -> 15.5s on the 4-shard cluster)
Durable copy of /tmp/dav1dprometheus-arborist-update.md into
docs/ so it ships with the repo. Captures eight days of
substrate work landing on the 5S/5F/5T/5R framework:
- 21 sub-batteries × 662+ default fixtures
- 15 π* canonical-projection kernels (registry closed)
- canonical-projection persistence + multi-witness pipeline
- claim-pack corpus across 7 pillars (I-VII + IX), 92 records
- surface-ingest layer for cited textbooks (~351 docs, 1597
chunks across 6/7 g4 pillars)
- witness-sweep cron flowing (5/8 KERNEL-LLM-DIVERGED on live
Hermes; auto-extracted to 5F-Falsification fixtures)
- #000013 v7-W substrate paper closed
- #000016 ZK Phase-2 parked with bench-plan + wire-protocol
- #000018 soft-hash covert-channel analysis closed; three
follow-up tickets opened (#000034 / #000035 / #000036)
- 1,684 passing, 37 sympy-skipped
Same naming pattern as docs/qa-modes-bench-2026-04-30.md so
future point-in-time reports follow the precedent.
Rolling research log gains a 2026-05-09 amend for the
multi-witness pipeline (#000028) running against live Hermes for
the first time. Qualitatively different from the random-word
triangulation amends above — those measure honesty under no
ground truth; this measures agreement under available ground
truth (kernel IS the ground truth on canonical-shape questions).
First sweep: 8 canonical-shape questions, 5 LLM-DIVERGED, 3
STRICT-WITNESSED. Three distinct failure shapes captured:
1. Wrong arithmetic on float-shape input
0.1 + 0.2 → kernel 3/10 vs Hermes 1/10
(off by 2/10; possibly trained on the IEEE-754 trap as
the "answer" itself rather than recognizing the kernel
returns the exact rational)
2. Implication-tautology error
A IMPL B → kernel (NOT A OR B) vs Hermes TRUE
(NOT B) IMPL (NOT A) → same divergence
(Hermes treats the formula as a tautology rather than
canonicalizing to CNF; A OR NOT A — the genuine tautology
— correctly returns TRUE)
3. Symbolic erasure on algebra-shape input
(x+1)**2 → kernel x²+2x+1 vs Hermes 1
x**2 + 2*x + 1 → same divergence
(Hermes collapses to a constant — possibly evaluating at
x=0 — instead of returning the canonical expanded
polynomial)
The amend frames witness-sweep as the *capability-failure*
signal source, distinct from random-word emergent's
*honesty-failure* signal. Different signals, different repair
paths:
- Verifier ladder hardening / warrant-tier sharpening
addresses honesty failures (false STRICTs).
- Prompt engineering / fine-tune-on-divergence-corpus
addresses capability failures.
The verifier ladder cannot help with witness-divergence — the
LLM fundamentally produced a wrong answer that no number of
citation checks recovers. This is the calibration-data stream
the original #000028 ticket imagined.
End-to-end validates: canonical persistence (#000027),
multi-witness fan-out (#000028), audit-event chain — 0 breaks on
chain-check-shards post-sweep, 5 providence_canonical_witness
events appended, capital ledger captured 5 canonical_witness
op_type rows.
Pattern documented for future witness-sweep amends as the
divergence corpus grows (cron + commit harness in
bench/scripts/witness_sweep_cron.sh handles the unattended
collection).
Bench artifact: bench/results/witness-sweep.json.
Calibration corpus: bench/fixtures/5f/falsification-witness-v1.jsonl
(10 rows after two extraction passes today).
Pillar VII bundle (axiomsclaude-vii-v1.json +
theoremsclaude-vii-v1.json) ingested via the existing claim_pack
source into ~/.arborist/shards/000.db. 14 records (7 axioms + 7
theorems): Addition / Multiplication / Pigeonhole Principles,
Factorial + Binomial Coefficient definitions, Pascal's Rule,
Empty-Set Boundary; Binomial Theorem, Inclusion-Exclusion
(counting form), Hockey-Stick, Vandermonde, Catalan Closed
Form, Stars and Bars, Strong Pigeonhole.
Combined with the v2 bundles (78 records across pillars I-VI +
IX), shard 000 now carries 92 claim_pack documents.
Retrieval lift verified on representative combinatorics queries:
- Pascal's rule → claim-pack record at #2
- pigeonhole → Strong Pigeonhole Principle at #2
- Modus Tollens → claim-pack record at #3
Authorship metadata: Claude blackops draft + cite-check against
Stanley / Brualdi / Wilf / Knuth (option C from #000033 §2.1).
Records cap at ANCHOR-WARRANTED on the four-rung ladder until
#000031 surface-ingests the cited textbooks and computes
derivations.proof_blob — that's the warrant-promotion track.
Drive-by Makefile fix
=====================
Crawl shards now land in $(CRAWL_SHARDS_DIR) ($(HOME)/.arborist/crawl)
by default, separate from $(SHARDS_DIR) ($(HOME)/.arborist/shards).
SQLite's max-attached-databases limit is 10; mixing 4 main shards
+ 6 crawl shards + qa.db + snapshots.db put us at 12 and broke
cross-shard queries. Crawl shards moved to a sibling dir; the
existing crawl_textbooks-stats target reads from both for backward
compat with already-placed shards.
Three artifacts landing per ticket §4.1 closure criterion:
1. docs/_source/merkle-agi-v7w-spatial-temporal.rst (658 lines)
============================================================
Substrate paper for the third commitment substrate — sister to v7
(logic / math) and arborist v9.8 (language / claim-lattice). v7-W
commits derived spatial-temporal world-state: objects, relations,
events, places, agent traces, observations. Six parts + appendix:
Part 1 — Introduction & motivation. The third-substrate gap;
why v7 § 11 multimodal composition isn't enough.
Part 2 — Substrate definition. Hierarchical-grid spatial
discretization (S2 / H3 / octree); frame as committed
object with explicit transforms; substrate-declared
clock (single-agent) + Lamport (multi-agent);
quantized centi-confidence (range opt-in); five
canonical tuple-classes (object / relation / event /
place / agent_trace) each with its own π*_w.
Part 3 — Theorems. T1-W (state binding), T2-W (causal
completeness), T3-W (frame-transform soundness),
T4-W (ε at affine frontiers).
Part 4 — Verifier kernels. Pose integration, observation
update (Kalman), object logits, relation logits.
Each affine after canonical projection.
Part 5 — Multimodal composition with v7. Where v7 ends, v7-W
begins; cumulative ε across substrates; frame-
transform anchoring.
Part 6 — Adversarial corners. Frame spoofing, time skew,
observation injection, privacy.
Appendix — Worked SLAM example with full ε budget.
Hard constraints honored: stays inside SQD A1-A3 (canonical
encoding, public quantization, collision-resistant hash); no new
axiom; every π*_w defined on quantized integer state, never on
continuous tensors.
2. docs/v7w-frontier-catalog.md (262 lines)
============================================
Operator-facing quick reference for the four ε-frontiers from
substrate-paper Part 4. Each entry:
- canonical input / output bytes
- operator (linear / bilinear / Kalman / SE(3))
- ε bound expression
- "affine after canonical projection" justification
- when to use
Reference table + cumulative-ε section so operators sizing
deployment grid choices can read off their ε_total under typical
agent-trace + scene-graph workloads.
3. arborist/world/__init__.py — namespace reservation
======================================================
Reserved ``arborist.world`` package. No kernels yet. Module
exports V7W_VERSION ('v0-draft') + STATUS ('namespace_reserved')
metadata. Package docstring lays out the future shape per
substrate-paper Part 4:
arborist/world/
├── pi_star/ — π*_w canonical projections (5 tuple classes)
├── frontier/ — ε-frontier kernels (4 frontiers)
├── frame.py — frame definitions + transforms
├── clock.py — wall-clock + Lamport
├── manifest.py — substrate manifest schema
└── adapters/ — sensor adapters land here, separate tickets
Implementation tickets cite the substrate paper and land kernels
one at a time; the stub exists so cross-referencing imports (mesh
peers, sibling repos) can pin the namespace before anything
implements it.
5 tests pin the reservation contract (test_world_namespace.py):
import succeeds, V7W_VERSION reports v0-draft, STATUS reads
namespace_reserved, __all__ exposes only metadata, substrate
paper + frontier catalog files exist alongside the namespace.
Closure criterion (#000013 §7): substrate paper lands and is
ready for review. Done. Status flipped to closed in the ticket
file + TICKETS.md index entry.
Test suite: 1641 passed, 37 skipped (was 1636; +5).
Three new tickets carve up the open questions from §9 of
docs/soft-hash-channel-analysis.md (#000018):
#000034 — Hessian alignment under φ_linear
============================================
Computational. Measure spectrum of W^T W (the v7 reference
embed_hard_to_vec frozen-seed projection matrix) vs typical
training-loss Hessian eigenvalue distributions on representative
checkpoints. Determines whether the linear projection has
structural alignment with low-eigenvalue directions, which would
let T2 adversaries amplify covert-channel steerage beyond the
random-oracle baseline established in #000018 §4.
Deliverable: bench/scripts/phi_alignment_probe.py + verdict
(STRUCTURAL_ALIGNMENT / NO_ALIGNMENT / ANTI_ALIGNED) per
representative checkpoint. Parks until a v7 reference checkpoint
is available; the analysis is empirical-only and useless without
representative training data.
#000035 — PRG choice for φ_PRG
================================
Cryptographic. Pin a specific PRG construction for the M1
mitigation (PRG-based anchor map) proposed in #000018 §5.2.
Recommended: HMAC-SHA-512(seed, digest ∥ counter) → uniform-random
floats in [-1, 1].
Reasons:
- Tightest dependency surface (stays in SHA family already
committed via SHA-256).
- NIST-approved PRF construction (SP 800-108 KDF in counter mode).
- Speed parity with AES at v7 cadence; PRG cost negligible.
- Provable security reduction: PRF security from SHA-512
collision-resistance, structurally stronger than SHA-256.
Deliverable: arborist/v7/anchor_prg.py + tests + known-answer-test
fixture + v7 § 9.10 amendment text. Lands when v7 plastic-training
has a deployment target.
#000036 — T3 per-window budget bound
=====================================
Formal. Derive an explicit closed-form upper bound on the covert-
channel capacity under threat model T3 (hyperparameter adversary)
when M2 (per-checkpoint nonce) is in place. #000018 §6 lists
"bounded by per-window budget" without giving the bound.
Three control bandwidths combine:
B1 — gradient bias (g · W · log₂ N_directions)
B2 — LR selection (⌈W/K⌉ · log₂ R)
B3 — batch order (Bottou-Bousquet conjecture: ≪ log₂ N!)
Deliverable: docs/soft-hash-channel-t3-bound.md (§§1-8 formal
derivation) + bench/scripts/t3_bound_calculator.py (operator-
parametrized closed-form). Operators plug in (g, K, R, W,
batch_count, gradient_norm) → read off bits/window residual; pick
nonce-window length to drive residual under their target.
Index updated; Next ID 000037. Cross-reference added to #000018's
status line so future readers see the three follow-ups in line.
Three streams. Two land in the repo; one lands in fox's Downloads
(existing g4 packs live there too).
Witness sweep automation
========================
`bench/scripts/witness_sweep_cron.sh` — schedulable harness that
runs `make bench-witness-sweep` + `make bench-witness-divergence`
back-to-back and (with --commit) auto-commits any new divergence
fixtures + sweep result. Fail-closed: pre-commit hook failure
aborts; non-main-branch refuses to commit.
$ bench/scripts/witness_sweep_cron.sh # dry run
$ bench/scripts/witness_sweep_cron.sh --commit # auto-commit
$ bench/scripts/witness_sweep_cron.sh --commit --push # full pipeline
Recommended cron (every 6 hours; LLM cost scales with frequency):
0 */6 * * * \
bench/scripts/witness_sweep_cron.sh --commit --branch main \
>> /var/log/arborist-witness.log 2>&1
Smoke this commit: dry-run produced 5 fresh divergences (10
cumulative across two extraction passes). The witness-sweep + 5F
extractor pipeline runs unattended now; calibration-data corpus
will grow over time.
#000018 — adversarial soft-hash covert-channel analysis
========================================================
`docs/soft-hash-channel-analysis.md` — formal threat model + channel-
capacity definition + cryptographic reduction + mitigation table
+ residual analysis. Doc-only deliverable per the ticket's hard
constraint.
Headline result: under threat models T1 (data poisoner) and T2
(gradient adversary), the channel is bounded by SHA-256 partial-
preimage hardness when φ (the anchor map) is independent of
parameter geometry. T3 (hyperparameter adversary) requires
M2 (per-checkpoint anchor nonce) for boundedness.
Recommended mitigation: M2 (per-checkpoint nonce) — 32 bytes added
to the snapshot manifest, no training-ergonomics regression,
closes T1+T2 channels under any φ choice and bounds T3 by
per-checkpoint window. Fall back to M1 (PRG-based φ) if M2-only
deployment surfaces structural concerns. M3 (drop anchor entirely)
stays in reserve as the strict-construction fallback.
Three open questions (§9): Hessian alignment under φ_linear,
PRG choice for φ_PRG, and explicit T3 per-window bound. Each is a
follow-up ticket.
Ticket #000018 status: closed · landed 2026-05-09 (analysis doc).
v7 § 9.10 spec amendment proposed in §7 of the analysis.
#000033 — pillar VII (combinatorics), Claude-authored
======================================================
NOT committed to the arborist repo (the existing g4-v2 packs live
in `/home/fox/Downloads/` too — that's the operator's bundle
location). Two new bundle files at:
/home/fox/Downloads/axiomsclaude-vii-v1.json (7 axioms)
/home/fox/Downloads/theoremsclaude-vii-v1.json (7 theorems)
Pillar VII covers combinatorial counting — the gap between Grok's
pillars VI and IX in the v2 packs:
axioms (7): addition principle · multiplication principle ·
pigeonhole principle · factorial definition ·
binomial coefficient definition · Pascal's rule ·
empty-set / boundary axiom
theorems (7): binomial theorem · inclusion-exclusion (counting
form) · hockey-stick identity · Vandermonde's
identity · Catalan number closed form · stars-and-
bars · strong pigeonhole
Each record in the dual-thread format the existing g4 packs use
(Δ symbolic LaTeX + ∇ verbose prose + ∇ concise + sigil + formal
language + role + status + source_reference + date + foundational
group + category + subfield). Per fox's directive: explicit
authorship metadata everywhere — `authored_by: Claude (Anthropic)
— model claude-opus-4-7`. NOT Grok-generated; no silent invention.
Each record carries `pi_star_ref: combinatorics@v1` so the kernel
binding is explicit. Theorems list `depends_on_axioms` arrays so
each theorem cites the foundation axioms it bottoms out on.
Smoke test (committed alongside):
$ arborist --db /tmp/test.db ingest --source claim_pack \\
--bundle /home/fox/Downloads/axiomsclaude-vii-v1.json \\
--bundle /home/fox/Downloads/theoremsclaude-vii-v1.json
→ 14 docs, 14 chunks, 0 cross-bundle edges
Source attributions: Stanley EC1, Brualdi Introductory
Combinatorics, Knuth TAOCP Vol 1, plus historical sources where
applicable (Pascal 1654, Vandermonde 1772, Dirichlet 1834, Catalan
1838, Feller 1950 for stars-and-bars).
Tests: 1636 passed, 37 skipped (no regressions; pillar VII
ingestion smoke covered above).
Three small streams:
#3 — close#000030 properly
============================
All 7 phases + Phase 1b landed across two commits (`04f3f5d`,
`abe5988`). Status header updated; ticket body now carries a phase
landing table with commit refs:
Phase 1 algebra-symbolic@v1 04f3f5d
Phase 1b algebra-symbolic-simplified@v1 04f3f5d
Phase 2 calculus-derivative@v1 04f3f5d
Phase 3 calculus-integral@v1 fox-direct
Phase 4 calculus-limit@v1 abe5988
Phase 5 calculus-series@v1 abe5988
Phase 6 linear-algebra@v1 abe5988
Phase 7 function-sampled@v1 abe5988
Plus tabular-pinned@v1 (last reserved stub) graduated in abe5988
closes the registry chapter — 15 concrete π*'s, no remaining
reserved stubs. Index updated.
#5 — composition fixtures across new SymPy π*'s
================================================
12 new tests in tests/test_pi_star_compositions.py covering pairs
that compose naturally:
- algebra-symbolic ∘ algebra-symbolic — idempotency check (running
expand twice equals expand once for any expression).
- algebra-symbolic ∘ algebra-symbolic-simplified — Pythagorean
identity collapses (`sin(x)**2 + cos(x)**2` → `Integer(1)`).
- Generic invariants: composition propagates PiStarError; manifest
fingerprint is order-sensitive; composite domain == inner domain;
composite bytes == manual chain bytes.
Test discipline: most compositions use `register_in_registry=False`
via a small `_safe_compose()` helper since the registry rejects
duplicate keys (#000015 invariant), so test ordering would
otherwise matter. Only the registration-test path uses real
compose().
#4 — end-to-end witness sweep against real shards + Hermes
===========================================================
New script `bench/scripts/witness_sweep.py`. Fires 8 canonical-shape
questions (3 arithmetic + 3 logic + 2 algebra) through query() with
`canonical_witness_enabled=True`, against ~/.arborist/shards (real
shard cluster) + the actual Hermes endpoint (NOT StubClient).
Records the agreement matrix per question to
bench/results/witness-sweep.json.
`make bench-witness-sweep` Makefile target. Honors
`ARBORIST_SHARDS_DIR`.
First real sweep (this commit, against Hermes-3-8B):
agreement label count rate
KERNEL-LLM-DIVERGED 5 62.5%
KERNEL-LLM-AGREE 3 37.5%
───────────────────────────────────────────
divergence_count 5 62.5%
wall median / max 130 ms / 1.1 s
Hermes diverged on 5/8 of the canonical-shape questions:
- said `1/10` for `0.1 + 0.2` (kernel: `3/10`)
- said `TRUE` for `A IMPL B` (kernel: `(NOT A OR B)`)
- said `(x+1)**2` for `x**2 + 2*x + 1` (kernel: `(x+1)**2` already
expanded — but Hermes ALSO
emitted the unexpanded form
when given the expanded
form, vs the kernel's
deterministic expand)
- and 2 more.
These are real LLM hallucinations on questions with closed-form
ground truth — exactly the calibration-data stream #000028
imagined. Pipeline validated end-to-end against actual hardware.
Pair: `make bench-witness-divergence` then extracts the 5
divergences as 5F-Falsification fixtures
(bench/fixtures/5f/falsification-witness-v1.jsonl, also committed).
Re-running the extractor produces byte-equal output (idempotency
contract from the extractor work).
Tests
=====
Full suite: 1636 passed, 37 skipped (was 1624; +12 composition
tests). The witness-sweep + extractor produce real artifacts now
committed under bench/results/ and bench/fixtures/5f/.
A new π* kernel that canonicalizes pure-integer counting
expressions and FAILS CLOSED on any input whose result isn't a
non-negative sp.Integer. Tighter domain than algebra-symbolic@v1,
which already accepts the same input surface but happily returns
symbolic / negative / non-integer outputs.
Distinguishing feature versus algebra-symbolic@v1:
algebra-symbolic@v1: binomial(n, k) → "binomial(n, k)" (symbolic
passthrough)
combinatorics@v1: binomial(n, k) → PiStarError (fail-closed
on free-symbol output)
algebra-symbolic@v1: binomial(Rational(1,2), 3) → 1/16 (rational)
combinatorics@v1: binomial(Rational(1,2), 3) → PiStarError
(output not Integer)
Boundary kept explicit: binomial(-3, 2) = 6 IS accepted because the
output is an integer 6. The fail-closed rule is on output shape
(Integer ≥ 0), not input range. Documented as
test_generalized_binomial_negative_args_accepted_when_integer.
Output format: plain decimal literal (b"10", b"5040"). Composes
with arithmetic@v1 for byte-identical agreement with the rational
route (b"10/1") so the multi-modality witness (#000028) can pin
equivalence-class agreement when both routes fire on the same
question.
Allowed surface (via SymPy primitives): binomial, factorial, ff /
rf (falling/rising), catalan, bell, partition, stirling, plus
arithmetic compositions over those primitives
(3*binomial(5,2) + factorial(4) = 54).
Coverage:
- 43 unit tests including binomial symmetry C(n,k)=C(n,n-k),
Pascal's rule C(n,k)=C(n-1,k-1)+C(n-1,k), the C(n,k) =
factorial(n)/(factorial(k)·factorial(n-k)) identity,
fail-closed paths (symbolic/negative/non-integer/relational/
parse), round-trip idempotence, composition with arithmetic@v1.
- 10 syntax + 12 semantics bench fixtures, 100% pass.
- bench/batteries/base.py PHASE_1_CARRIERS gains "combinatorics".
- Makefile bench-5s-combinatorics target.
All gate on pytest.importorskip("sympy") so a sympy-less suite
stays green. Full make test: 1537 passed / 28 skipped.
Sequencing rationale honored: this kernel lands FIRST so that
#000033 (claim-pack pillar VII for combinatorics) can bind its
records to the tighter integer kernel from day one — avoids
rebind churn on pi_star_ref fields.
Three small streams in one commit:
#000028 follow-up — witness divergence → 5F fixtures
=====================================================
Witness fan-out now writes a `providence_canonical_witness` audit
event when it fires (next to the capital-ledger record landed in
708aa45). Body carries pi_star_ref, question_text, agreement_label,
canonical_answer_text, llm_raw_text, llm_canonical_bytes,
cache_status. Best-effort write — chain failure never fails the
query.
New extractor `bench/scripts/witness_to_5f.py` reads those events
from a qa.db and writes them out as 5F-Falsification fixtures
matching the existing `falsification-live-v1` schema. Filtering
includes only divergence labels (LLM-DIVERGED / KERNEL-LLM-DIVERGED
/ CACHE-DRIFT); skips KERNEL-LLM-AGREE / STRICT-WITNESSED (no
calibration signal) and KERNEL-ONLY (LLM unparseable, not a
supervised-correction sample).
Idempotent: sorted by audit-event seq, so re-running against the
same qa.db produces byte-equal fixture files. The existing
fixture-digest discipline stays valid.
Makefile: `make bench-witness-divergence` (override default
qa.db / output path via WITNESS_QA_DB / WITNESS_OUT env-vars).
Closes the divergence → calibration data loop the witness ticket
imagined: every LLM hallucination on a canonical-shape question
becomes a supervised-correction fixture downstream prompt
improvements can grade against.
#000030 Phase 7 demo — function-sampled@v1 end-to-end
======================================================
`bench/scripts/demo_plot.py` — closes the loop on opencompletion's
activity24-math-plot.yaml. SymPy expression → quantized
integer-vector signature (canonical bytes) → optional matplotlib
PNG. Canonical bytes are the proof; PNG is just a downstream view
of the same evidence.
$ make demo-plot Q='sin(x)' PNG=/tmp/sin.png
Output JSON contains canonical_bytes_sha256 + canonical_bytes_preview
+ canonical_bytes_total_chars + grid metadata + the optional png_path.
matplotlib is gated — when absent, --png prints a warning to stderr
and skips the render; the canonical bytes still print. Tests skip
the PNG-presence assertion via `pytest.importorskip("matplotlib")`.
Public docs polish (#7)
========================
- docs/_source/bench.rst: updated fixture-count narrative (~660 →
662 default tasks + ~110 math π* fixtures); `make` quick-reference
now lists all per-π* 5S targets (tabular, calculus-limit/series,
linear-algebra, function-sampled) plus bench-real-shard,
bench-fork-baseline/score, bench-witness-divergence.
- docs/_source/v8-fork-score.rst: CLI section gained --out flag
documentation + a Make-harness sub-section covering
bench-fork-baseline / bench-fork-score / FORK_PARENT/CHILD/REPORT
env-vars.
Tests
=====
- tests/test_witness_to_5f.py — 8 new tests covering the audit-event
write (3) + extractor logic (5).
- tests/test_demo_plot.py — 6 new tests covering canonical-bytes
determinism + equivalence-class collapse + matplotlib gating.
Full suite: 1624 passed, 37 skipped (was 1568; +56).
tabular-pinned@v1 + calculus-limit@v1 + calculus-series@v1 +
linear-algebra@v1 + function-sampled@v1 — all reserved stubs
graduated; the π* registry is now 15 concrete kernels with no
remaining reserved-stub entries.
#000030 Phase 4 — calculus-limit@v1
====================================
sp.limit with thread-timeout. One-sided dir support (+/-/+-).
Pinned spelling for infinity cases: b"+oo" / b"-oo" / b"zoo"
(complex infinity) — bypasses sp.expand since Infinity isn't
algebraic. Finite results re-canonicalize through algebra-symbolic
recipe (sp.expand + sp.srepr). Unevaluated cases / timeouts emit
b"unevaluated:" + sp.srepr(<Limit>) sentinel, mirroring
calculus-integral's pattern.
#000030 Phase 5 — calculus-series@v1
=====================================
sp.series(f, x, x0, n).removeO() → sp.expand → sp.srepr. Drops
O(x**n) remainder explicitly so the canonical form is finite-byte.
Sentinel format mirrors limit/integral: b"unevaluated:Series(...)"
on timeout. n must be a positive int; 0 / float / negative rejected.
#000030 Phase 6 — linear-algebra@v1
====================================
Single π* covers the whole linear-algebra surface via {op, matrix}
JSON. Ops: rref / det / eigenvalues / inverse. Matrix cells go
through Fraction(Decimal(str(...))) for floats so 1, 1.0, "1.0"
all collapse to Rational(1, 1) — matching arithmetic@v1's
discipline. Without this fold, sp.sympify keeps floats as Float
(separate type) and downstream det/inverse return Float-shaped
bytes. Eigenvalues are sorted by srepr for determinism.
Output formats:
rref / inverse: rows/cols header + cells joined by | (rows by ||)
det: det:<num/den-or-srepr>
eigenvalues: eigenvalues:<value-1>x<mult-1>|...
#000030 Phase 7 — function-sampled@v1
======================================
Bridge to time-series-quantized@v1. SymPy expression + linspace
grid → quantized integer-vector signature in time-series's exact
output format (dt=...;dv=...;n=...;t0=0:v0|v1|...). Two functions
that render identically (within sample-grid tolerance) collapse
to the same canonical bytes. This is what plotting CAN become
in π* terms — the PNG render is a downstream view of the same
canonical evidence.
Math-only sampler (no numpy in the dep surface); Python's round()
is banker's-rounding so the bytes are interchangeable with
time-series-quantized@v1's output. Complex / non-finite samples
raise PiStarError rather than silently dropping imaginary parts.
tabular-pinned@v1 — last reserved stub graduates
=================================================
JSON-rows input ({schema, key_columns, rows}); declared
key_columns sort policy (stable sort by primary-key tuple);
type-fold per column (int/rational/bool through arithmetic@v1
discipline; str verbatim; bool normalized). Header case is
PINNED EXACT — Excel and PostgreSQL both care about case;
defaulting to lowercase-fold would break operator expectations.
Output: header (schema + key + n) + rows joined by \n + cells by |.
The π* registry has no remaining reserved stubs. Every modality
the substrate paper reserved is now real.
Test suite: 1568 passed (was 1467; +101). New closure-criterion
test (test_no_stub_pi_stars_remain) replaces the old reserved-stub
parametrize — adding a future stub re-opens this list.
110/110 fixtures pass across the 5 new bench-5s-* targets.
PHASE_1_CARRIERS gained calculus / linear-algebra / function-sampled
/ tabular.
Two design-only tickets opened together because they're tightly
coupled — pillar VII records bind to combinatorics@v1 via
pi_star_ref, and #000032 lands first to avoid rebind churn on
that field.
#000032 — combinatorics@v1 π*
=============================
A new π* kernel that canonicalizes pure-integer counting
expressions (binomial, factorial, permutations, partitions,
Catalan, Bell, Stirling) and FAILS CLOSED on any input whose
result is not a non-negative integer. Tighter domain than
algebra-symbolic@v1, which already accepts the same input
surface but happily returns symbolic / negative / rational
outputs.
Distinguishing feature: algebra-symbolic@v1 returns
binomial(n,k) → "binomial(n,k)" (symbolic), binomial(-3,2) → 6
(generalized). combinatorics@v1 rejects both. Operators choose
the kernel by what they want rejected.
Output format: integer string (b"10"). Compose with
arithmetic@v1 to get bytes-identical agreement (b"10/1") for
the multi-modality witness flow.
Estimated size: ~120 LOC module + ~80 LOC tests + ~22 fixtures.
Single-commit feasible.
#000033 — Claim-pack pillar VII (combinatorics)
================================================
Extend the claim-pack source (#000029) with a new combinatorics
pillar slotting into the documented gap (existing v2 bundles use
I, II, III, IV, V, VI, IX — VII and VIII reserved for
extension). Counting axioms (Pascal's rule, addition principle,
multiplication principle, pigeonhole, factorial / binomial
definitions) + classical theorems (binomial theorem,
inclusion-exclusion in counting form, hockey-stick, Vandermonde,
Catalan closed form, stars-and-bars).
Bundle provenance is the open question — three options
documented:
A. Commission a Grok-4 v3 bundle for parity with the existing
pack.
B. Hand-curate from textbooks (Stanley, Brualdi, Wilf, Knuth).
C. Hybrid — LLM draft + human curation.
Hard constraint: explicit authorship metadata. No silent
invention. Bundle landing is a config + data exercise; no
source-code changes to arborist/sources/claim_pack.py needed
since the source already iterates arbitrary pillar names.
Sequencing: #000032 first (kernel), #000033 next (records bind
to it from day one), #000031 stays parallel-track (textbook
ingest for warrant promotion).
Both tickets stay open · awaiting go/no-go pending fox's
implementation green-light.
Phase 1b — algebra-symbolic-simplified@v1
==========================================
arborist/pi_star/algebra_symbolic_simplified.py — full-simplify
variant of the Phase-1 expand-only sibling. Closes the trig
identity gap left open at end of Phase 1: sin(x)**2 + cos(x)**2
now collapses to 1, tan(x)*cos(x) to sin(x), exp(log(x)) to x.
Recipe is sp.expand(sp.simplify(expr)) — the follow-up expand
after simplify is load-bearing. simplify alone is non-canonical
for polynomials: it leaves (x+1)**2 in factored form while
collapsing x**2 + 2*x + 1 to expanded form, so two algebraically
equivalent inputs would emit different bytes. Composing with
expand picks one canonical polynomial shape and preserves the
equivalence-class invariant.
Cost: 1-360 ms typical on common trig/exp inputs; pathological
inputs unbounded. No in-π* timeout (the calling pipeline owns
that budget). Operators opt in by registry key — the fast Phase-1
sibling stays the default for callers that only need polynomial
canonicalization.
22 unit tests; all gate on pytest.importorskip("sympy").
Phase 3 — calculus-integral@v1
==============================
arborist/pi_star/calculus_integral.py — symbolic integration with
thread-timeout fallback. JSON-shaped {f, x, limits?,
timeout_seconds?} input. Two output paths:
1. Closed form: sp.srepr(sp.expand(integrate_result)) — same
recipe as algebra-symbolic@v1 so the output is itself a valid
algebra-symbolic input and composes naturally.
2. Unevaluated: b"unevaluated:" + sp.srepr(<Integral>). Prefix
lets callers tell "no closed form" from "input invalid"
without re-parsing the canonical form.
Timeout discipline: ThreadPoolExecutor(max_workers=1) +
future.result(timeout=...). On TimeoutError, synthesize the same
unevaluated sentinel SymPy itself would emit, so timeout +
no-closed-form converge to the same bytes for the same input.
Default 30 s; per-call override via timeout_seconds. Python
threads can't be killed cleanly — a timed-out worker leaks until
SymPy returns. Documented as the cost of the discipline.
Coverage: ∫x dx = x²/2, ∫sin(x) dx = -cos(x), ∫_{0}^{π} sin(x)
dx = 2, ∫_{-∞}^{∞} exp(-x²) dx = √π, exp(x)/log(x) →
unevaluated sentinel. 31 unit tests including a monkeypatch
deterministic timeout test (sleep-mocked SymPy so the timeout
path doesn't depend on any specific input being slow on every
CI runner).
Open #000031 — surface-ingest cited textbooks
=============================================
Design-only ticket. Closes the warrant gap left open at the end
of #000029: today every claim-pack record caps at
ANCHOR-WARRANTED because source_reference is a string field, not
a Merkle-bound proof. Ingesting the cited textbooks as surfaces
+ computing per-claim derivations.proof_blob lets the four-rung
ladder promote them to EVIDENCE-WARRANTED.
License gating: PD sources (Hilbert, Newton, Kolmogorov,
Łukasiewicz, Aristotle) form the green-light scope. Mendelson +
Enderton are proprietary and stay yellow-light pending fox's
explicit decision (purchased single copy / library license / PD
substitute via Hilbert-Ackermann 1928).
Two follow-up tickets reserved: textbook-fetch pipeline +
chunk-resolution layer (mapping source_reference strings to
specific spans within ingested textbooks; the bridge that lets
proof_blob be computed).
Test counts: 153 tests for the work in this commit (algebra
+ algebra-simplified + calculus-derivative + calculus-integral
+ preflight). All pi_star + canonical_projection tests pass
under .venv pytest.
Three small streams in one commit; each closes / expands a
recently-landed ticket without changing its hard contract.
#000026 Phase 3 wiring — authorship warrant ladder visible
============================================================
Phase 3 sidecar (arborist/qa/warrant_authorship.py landed in 60b5748)
exposed the classifier but didn't surface it. Two wirings:
- arborist/qa/inspect.py — diagnose_authorship_warrant runs against
the cached row's question + answer + per-source raw chunks +
URIs + titles; result lands as `authorship` field alongside the
other sidecars.
- arborist/cli.py _render_warrant_tail — appends ` · warrant:
<readable-tier>` when result['authorship'] is populated with a
non-quiet tier. AUTHOR_COPYRIGHT_FOOTER → "copyright-footer", etc.
NO_AUTHORSHIP_SIGNAL stays silent. Backward-compat: results
without an `authorship` key render unchanged.
Tests: 3 inspect-path tests (no-signal, copyright-footer,
repository-owner) + 4 render-tail tests (presence, no-signal
silence, missing-key silence, all-six-tiers readable mapping).
#000028 follow-ups — capital ledger + sample-rate
==================================================
Two policy fields layered on top of canonical_witness_enabled:
- canonical_witness_sample_rate (0.0..1.0; default 1.0). Operators
wanting passive calibration set 0.05 to fire witness on 5% of
canonical questions while paying 5% of LLM cost. 0.0 effectively
off; 1.0 = current always-on behavior. Gating uses random.random()
so distribution is uniform; clamped to [0, 1].
- Capital ledger row written for each FIRED witness (not skipped
ones). op_type='canonical_witness'; estimator inputs include
prompt_chars + answer_chars + llm_seconds + agreement_label +
pi_star_ref. Best-effort: ledger-write failure must never fail
the query (sidecar discipline).
Tests: 4 new — sample_rate=0.0 skips (no LLM call, no ledger row);
sample_rate=1.0 always fires; capital_ledger row written under
op_type='canonical_witness' with full input blob; sampled-out
witness records zero ledger rows.
Both fields fold into governance_policy_hash naturally via the
existing policy-hash machinery — flipping witness mode invalidates
prior records as expected.
#000025 Phase 1d — 5F fixture catalog 30 → 50
==============================================
Both synthetic and live sides of all 5 sub-batteries expanded
30 → 50 (+200 fixtures total: 5 × 20 synthetic, 5 × 20 live).
function — claim_count cycles 2..7 across new fixtures
falsification — 10-violation palette across new ids
feedback-loop — fact-N learning chains
finetuning — capability transitions across canonical π*
(math/logic/algebra/calculus pool)
formulate — multi-pointer claim shapes
500/500 pass through respective runners. test_session_integration
total bumped 562 → 662. Pinned test_5f_*_runs counts updated 30 →
50 (synthetic main + embedded + live).
Tests
=====
Full suite: 1467 passed, 36 skipped (was 1388; +79 across warrant
render + witness sample/ledger + 5F implicit coverage).
Two new π* canonicalizers extend the math substrate above
arithmetic@v1 (closed-form rationals) and logic-kernel@v1
(propositional Boolean → CNF):
algebra-symbolic@v1 (Phase 1) — symbolic-algebra domain.
sp.expand → sp.srepr canonical bytes. Polynomial identity collapses
((x+1)**2 ≡ x**2 + 2*x + 1); exponential identity collapses
(exp(a+b) ≡ exp(a)*exp(b), inherited from sp.expand's default
behavior); trigonometric identity does NOT collapse
(sin²+cos² ≢ 1). The trig surface is reserved for a future
algebra-symbolic-simplified@v1 variant that wraps sp.simplify at
unbounded CPU cost. Rejects relationals (`x > 0`) and
BooleanFunction shapes (`x & y`) via `isinstance(expr, sp.Expr)` —
sp.Symbol confusingly inherits from Boolean so the right rejection
filter is "not Expr" rather than "Boolean".
calculus-derivative@v1 (Phase 2) — calculus domain. JSON-shaped
{f, x, n} input → sp.diff → sp.expand → srepr bytes. Output is
itself a valid algebra-symbolic@v1 input so the two compose
naturally under arborist.pi_star.compose. n defaults to 1; bools
explicitly rejected (Python isinstance(True, int) is True so we
filter that explicitly).
Optional dependency: sympy ships in the new [math] extra
(pyproject.toml). Folded into [dev] so make bootstrap pulls it
transitively. An explicit `bootstrap-math` Makefile target documents
the opt-in for minimal-install users. Both modules self-guard
via `try: import sympy as sp / except ImportError: sp = None` and
only register(...) when sympy is present, so a fresh checkout
without [math] still loads arborist.pi_star without raising.
Preflight algebra route lands in
arborist.qa.query._canonical_projection_preflight between the
arithmetic and logic routes. Charset regex (_CANONICAL_ALGEBRA_RE)
allows lowercase letters + math chars; requires at least one
letter (else arithmetic wins); rejects natural-language leading
verbs via _CANONICAL_ALGEBRA_NL_LEAD_RE (4-letter minimum so
single-/two-/three-char identifiers like x, xy, sin, cos, pi
survive while "simplify (...)", "factor x...", "expand (a+b)..."
fall through). PiStarError + KeyError both fall through cleanly
so a sympy-less install just routes everything past algebra.
Bench substrate:
- bench/batteries/base.py PHASE_1_CARRIERS gains "symbolic_algebra"
- bench/fixtures/5s/syntax-algebra-symbolic-v1.jsonl (10 fixtures)
- bench/fixtures/5s/semantics-algebra-symbolic-v1.jsonl (13 fixtures
including the documented trig non-collapse + exp collapse)
- Makefile bench-5s-algebra target → 100% pass
Tests: 18 algebra-symbolic + 38 calculus-derivative unit tests +
~10 new preflight-route tests in test_canonical_projection.py. All
gate on pytest.importorskip("sympy") so a sympy-less suite stays
green. Full suite: 1369 passed / 27 skipped.
Phases 3-7 (integral, limit, series, linear-algebra,
function-sampled) remain open as future work; each lands as its
own ticket when an actual consumer surfaces.
Brain-stormed off opencompletion's activity24-math-plot.yaml
(SymPy + numpy + matplotlib pipeline). Three things in there
map to π* shapes; one doesn't.
Maps:
- algebra-symbolic@v1 — symbolic expression → expand + canonical
ordering. Closes the (x+1)**2 ≡ x**2+2x+1
equivalence class.
- calculus-derivative@v1 — d/dx(f) via sp.diff, re-canonicalized
through algebra-symbolic@v1.
- calculus-integral@v1 — ∫f dx via sp.integrate; sentinel for
unevaluated cases.
- calculus-limit@v1, calculus-series@v1, linear-algebra@v1 —
additional SymPy-friendly phases.
- function-sampled@v1 — bridges symbolic expressions to the
existing time-series-quantized@v1
format. Two functions that render
identically (within sample tolerance)
collapse to same canonical bytes. This
is what plotting CAN become in π* terms.
Doesn't map:
- PNG plot rendering — different DPIs / fonts / palettes all
valid; image bytes aren't canonical. Stays as an output adapter
that COMPOSES with function-sampled@v1.
Hard constraint: SymPy is an OPTIONAL dependency ([math] extra).
Each new π* registers only when sympy is importable, mirroring
the existing html / wikitext / crawler pattern. Fresh checkout
without sympy keeps passing the full test suite (graceful skip).
Multi-phase rollout. Recommendation: Phase 1 (algebra-symbolic@v1)
+ Phase 2 (calculus-derivative@v1) in one commit (~400 LOC total
+ tests + 5S fixtures). Subsequent phases (integral, limit,
series, linalg, function-sampled) each their own commit.
Forward links in the ticket: #000027 (canonical persistence —
algebra/calculus answers inherit audit chain for free), #000028
(witness — symbolic answers become witnessable), 5T/5F (new
fixture surface for symbolic LLM calibration), composition algebra
(deriv+arith, expr+sample compose naturally).
Index updated. Next ID 000031.
ClaimPackSource ingests Grok-4 companion bundles (axiomsg4-v2.json +
theoremsg4-v2.json) at the right grain — one Document per axiom or
theorem record. Each record carries Δ (LaTeX symbolic) + ∇verbose
prose, explicit source citation (Mendelson, Enderton, Hilbert,
Newton, Kolmogorov, Łukasiewicz), foundational-group taxonomy, and a
runicLabel that rides as soft metadata only (runtime mints its own
pointer IDs per CTI architecture). Pillar-level
provenance.references arrays become outbound pillar_reference edges.
Lenient JSON parser strips ```json fences and double-escapes lone
LaTeX backslashes (\Theta, \heart, \vec) without corrupting
already-correct \\to pairs — walks left-to-right and pass-throughs
legal escape sequences. Malformed bundles raise rather than return
empty; silent zero-doc would be a footgun.
CLI surface: --source claim_pack with a repeatable --bundle FILE
flag mirroring html source's --url action=append. Single --path
also accepted for one-bundle ingest.
Drive-by: removed a function-local `from arborist.store import
connect` inside _cmd_ingest's providence branch that was shadowing
the module-level binding via Python's "any local assignment makes
the name local for the entire function" rule, breaking every
non-providence ingest with UnboundLocalError. Comment left in
place explaining why not to re-add it.
Smoke-tested on /home/fox/Downloads/{axiomsg4,theoremsg4}-v2.json
end-to-end: 78 docs (55 axioms + 23 theorems across 7 pillars),
14 deduped pillar-reference edges, 78 audit events, 10/10 sampled
Merkle proofs verify, FTS5 search returns Modus Tollens for
"modus tollens".
Honest ceiling: kind=surface for every record. The pack is
pre-distilled but its provenance is asserted not proven — until
Mendelson/Enderton/Hilbert texts are themselves ingested as
surfaces, the verifier has no derivations.proof_blob to compute
and claim-pack records max out at ANCHOR-WARRANTED on the
four-rung ladder. That's a follow-up ticket, not this one.
Hard constraints honored: no new audit ledger (audit_events
remains the only chained-sha256 ledger; bundle's self-validation
fields ride as metadata only); no kind=core without surface
ancestor; cache_key invariants untouched.
15 unit tests cover lenient parser, slug stability, ref
resolution, doc grain, URI stability, content layout, extra
metadata, edge emission, error paths. All 1280 tests in
make test pass.
Closes#000027. Closes#000028 (cache-leg wired).
#000027 — canonical projections persist to providence_cache
============================================================
Math/logic π* answers (arithmetic@v1, logic-kernel@v1,
time-series-quantized@v1, …) are now first-class providence rows.
Pre-fix: question → kernel → answer → return. No cache, no audit
event, no run_dag, no inspect/burn/replay surface.
Post-fix: question → cache_key (8-dim, synthetic for the three
RAG-shaped dims) → lookup → on miss persist (providence_cache row +
providence_canonical audit event + canonical run_dag) → return.
Synthetic cache_key dimensions for canonical rows (per ticket §2.2):
- source_root = sha256("pi_star_source:" + pi_star_ref)
- model_profile_hash = sha256("pi_star_model:" + pi_star_ref)
- conversation_hash = sha256("pi_star_conv:" + canonical_q + ":" + ref)
- chunking_version = literal "n/a-canonical" — chunker bumps on
wikipedia path don't stale math answers.
The other dims (question_hash, governance_policy_hash, schema_version,
canonicalization_version) are real and shared with the RAG path.
Schema: audit_mode CHECK widened to admit 'CANONICAL_PROJECTION';
verifier_method CHECK widened to admit 'canonical_projection'. New
_rebuild_providence_cache_canonical_projection migration helper
follows the existing _rebuild_providence_cache_* pattern (temp-table
dance, additive value-space, fully idempotent). Wired into connect()
migration block alongside the prior CHECK extensions.
Cache-hit policy: trust the row. Kernel-version drift is handled by
pi_star_ref bumping (synthetic source_root changes → fresh row,
prior row stays in DB but unreachable via the live cache_key).
Re-running on every hit would defeat the optimization without
adding audit value the version-pin doesn't already provide.
Policy gate: canonical_projection_preflight_persist (default True).
Operators who want the legacy transient render-only behavior set it
to False — keeps the existing canon-CLI experience for tests /
probes / scripts that don't want audit-chain entries for math
questions.
CLI render: `CANONICAL · via canonical_projection` for persisted
rows. Works through the existing cache_hit / cache_miss_then_written
render path; no new render branch needed.
`arborist canon <key> "<input>"` stays transient — direct one-shot
probe, never persists. Boundary preserved per ticket §2.6.
#000028 — multi-modality witness cache-leg
==========================================
Pre-#000027 the witness cache-leg closure always returned None;
STRICT-WITNESSED (3-of-3 byte-equal) was structurally unreachable.
Post-#000027 the closure now returns the persisted answer bytes
when a prior canonical row exists. Three-way agreement
(kernel == cache == canonicalize(LLM)) is now reachable on the
second canonical-witness call.
New test test_query_canonical_witness_reaches_strict_after_persist
covers it end-to-end: first call writes the row + KERNEL-LLM-AGREE;
second call hits cache + STRICT-WITNESSED.
Tests
=====
- tests/test_canonical_cache.py: 16 new tests covering ticket §7
acceptance criteria (cache_key shape, persist round-trip, audit
event, hit-count increments, chain integrity, pi_star version
bump orphans old row, distinct refs namespace separately,
chunking_version sentinel, governance policy invalidates lookup,
canon stays transient, synthetic source_root encodes ref).
- tests/test_canonical_projection.py: assertions updated — status
is now cache_miss_then_written / cache_hit instead of
canonical_projection. Added a transient-mode test pinning the
policy gate.
- tests/test_witness.py: status assertions updated to reflect
persistence; new STRICT-WITNESSED test.
- tests/test_directives.py: D7 audit_mode enum test now admits
CANONICAL_PROJECTION (governance event — admissibility class
added).
Full suite: 1367 passed, 36 skipped (was 1306; +61 new).
Real-shard smoke
================
$ make query Q="0.1 + 0.2" BURN=1
→ cache_miss_then_written, ~300ms wall, row written
$ make query Q="0.1 + 0.2"
→ cache_hit, ~40ms wall, hit_count++
$ make chain-check-shards
→ 0 breaks per shard
Acted on response review (2026-05-09,
response_ticket-000027-canonical-projections-in-providence-cache.txt).
#000027 — Hard-constraint phrasing corrected. Original draft said
"no schema changes / no new admissibility mode," which would
mislead an implementer into skipping the CHECK-constraint
extension. The current SCHEMA_SQL CHECK rejects both
'CANONICAL_PROJECTION' (audit_mode) and 'canonical_projection'
(verifier_method) — five locations in store.py listed in §9.1.
Updated to: "no new columns / no new tables / 8-dim cache_key
preserved / CHECK widened via existing rebuild migration." Same
spirit as the original draft, but unambiguous. §2.6 amended to
note the CHECK widening is value-space, not column/table change.
Forward-link added pointing at #000028 as the witness layer that
runs ON TOP of this persistence primitive (not a Phase 2).
#000028 — Post-MVP follow-up appendix. MVP shipped in 656b573
(witness.py 394 LOC + tests 354 LOC, 28/28 passing). Five items
captured for follow-up:
- terminology: ticket uses "modality" but kernel/cache/LLM are
epistemic witness channels, not carrier modalities; suggest a
one-line clarification near §1 to prevent cross-carrier
misreads.
- capital ledger integration (#000020): MVP records LLM latency
on the result dict but doesn't thread cost into the ledger;
~15 LOC follow-up to wire it; ForkScore (#000012) needs this
to compare witness-on vs witness-off forks honestly.
- sample-rate policy field (canonical_witness_sample_rate):
explicit out-of-scope per §2.4, but flagged so it isn't
re-discovered when calibration-data hunger appears.
- cache-leg dependency on #000027: MVP works with stub closure
returning None; STRICT-WITNESSED is unreachable until #000027
lands; swap is one-line when persistence ships.
- 5F / 5T bench-data integration: divergence events are
supervised calibration data; suggest a future
`make bench-witness-divergence` target.
- threat-model caveats from review §7: correct claim is "no
clean single-channel adversarial path," not "no adversarial
path"; future dual-kernel witness option captured.
No code changes in this commit — ticket text only.
Design doc only; no code in this commit. Spec the persistence pattern
for canonical-projection answers — same providence_cache table, same
audit chain, same admissibility ledger, distinguished by
verifier_method="canonical_projection" and audit_mode=
"CANONICAL_PROJECTION". Synthetic-but-deterministic values for the
LLM-only cache_key dimensions (source_root, model_profile_hash,
conversation_hash) bound to pi_star_ref so kernel-version migrations
work via the existing falsification pipeline.
chunking_version = "n/a-canonical" sentinel keeps RAG chunker bumps
from mass-staling unrelated math/logic answers.
Builds on existing _canonical_projection_preflight() short-circuit
(currently transient compute, no row written). Ships with #000027 and
fox confirmation on §8 open questions before code lands.
Two fan-out streams. Both bear directly on the ticket's "search
latency on real shards" headline finding.
## Lazy concept_relations loading
Phase 1 (migration memoization) cut SQLite executes 65% but warm-
cache wall barely moved. cProfile pinned the next hotspot:
synonym_expand 2.8 s × 2 calls + _load_token_idf 0.3 s. The eager
loader dumped all ~290 K concept_relations rows on first call —
the price of being able to answer ANY future question without
re-querying. Wrong tradeoff for single-query CLI use.
Refactored arborist/concepts/query.py:
- New _load_neighbors_for(shards_dir, tokens) — targeted
WHERE token IN (...) OR target IN (...) query. Returns just the
direct synonym neighborhood for the given tokens (~300 rows for
a typical 5-token question, vs 290 K for the full table).
- New _load_rivalry_rows(shards_dir) — process-wide cache of the
~2-row rivalry-relation set; near-zero cost.
- New _load_idf_for(shards_dir, tokens) — IDF only fetched when
expansion exceeds max_total (the cap). Most queries never reach
the truncation branch and skip IDF entirely.
- Per-token process-wide neighbor cache so multi-query bench scripts
don't re-query tokens already seen.
- synonym_expand and rivalry_excluded refactored to use the lazy
loaders. Eager _load_indices / _get_indices kept for any
back-compat caller; not used by hot paths.
- invalidate_cache() clears all three caches.
All 14 concept tests pass unchanged — the contract is preserved.
Re-profile of `who wrote virt-back?` against ~38 GB of real shards
(warm cache):
metric pre-fix post-Phase-1 post-lazy-concepts
wall_ms 14,500 13,400 9,300 (-36%)
search_ms 9,900 10,600 5,000 (-49%)
SQLite executes 10,623 3,687 3,708 ~same
synonym_expand 2,966 2,840 ~0 (lazy hit)
Search target was <5 s; we hit 5.0 s on the warm path. Cold cache
should drop further (the 290 K-row dump was disk-bound).
## Real-shard baseline artifact (Phase 2)
bench/scripts/real_shard_baseline.py — runs an 8-question fixture
through the full query() pipeline and emits:
- bench/results/real-shard-baseline.json (durable; commit_sha,
shards_fingerprint, per-query rows, summary)
- bench/results/real-shard-baseline.md (human-readable summary)
Question set in bench/fixtures/real-shard-baseline-v1.jsonl:
virt-back, France, Mac OS X, Linux, Microsoft, AMD/Intel
(rivalry path), and two canonical-projection cases (math + logic
preflight short-circuit).
First baseline run (commit e78814c plus this fan-out, BURN=1):
audit_mode n notes
STRICT 4 (virt-back, France, Mac OS X, Linux)
HYBRID 2 (Microsoft founder, AMD/Intel)
CANONICAL 2 (0.1+0.2, A IMPL B; <1 ms each)
wall median 4.1 s (range 0.6 ms – 7.2 s)
primary used 4 / 8
`who wrote virt-back?` lands at 6.3 s wall, audit STRICT, primary
source #1, cited evidence still includes a copyright footer
(reviewer's warrant-quality finding — deferred to follow-up ticket
since the latency fix was the gating concern).
Hard constraint preserved: baselines NEVER gate CI. The artifact
is for confirming a fix moved the needle, seeding ForkScore
comparisons, and noting findings worth tickets.
`make bench-real-shard` wires it. Honors ARBORIST_SHARDS_DIR.
## Test status
Full suite: 1306 passed, 36 skipped (no regressions from the
concept refactor; 14 concept tests cover the lazy/eager
equivalence).
`connect()` used to run executescript(SCHEMA_SQL) + 7 forward-
migration probes on every open. Profile of `who wrote virt-back?`
on 38 GB of real shards (warm cache) showed 588 connect() calls
per query, each running the full probe sequence — 10,623 total
SQLite executes. Migrations are forward-only and idempotent within
a code version, so once we've run them on a path in this process
there's no work to do on subsequent opens.
Cache shape: `set[str]` keyed by `str(Path(p).resolve())`.
Migration block runs once per (path, process); subsequent calls on
the same shard skip it entirely. Per-connection PRAGMAs
(foreign_keys=ON, synchronous=NORMAL, cache_size, temp_store,
mmap_size) still run every time — SQLite scopes foreign_keys
per-connection and our schema's FK CASCADE behavior depends on it.
That's why `PRAGMA foreign_keys = ON` moved out of the cached
SCHEMA_SQL block into the always-run pragma section.
Cache invalidation: explicit only.
`store.invalidate_migration_cache(path)` for callers who replace a
shard at the same path (snapshot-restore flows). `_clear_migration_
cache()` for tests. We don't auto-detect file replacement —
(dev, inode) is unreliable under tmpfs inode reuse, and (mtime,
size) drifts naturally as SQLite operates on the file (WAL
checkpoints, page growth). Path-only with explicit invalidation
is the honest contract.
Re-profile (same query, same shards, warm cache):
metric before after
_migrate_* (each function) 586 7 ← per shard
executescript 586 7
SQLite executes 10,623 3,687 (-65%)
wall (warm) 14.5 s 13.4 s
The warm-cache wall delta is small because the probes were many-
but-cheap; residual cost lives in FTS5 search (6.7 s) and
synonym_expand (2.8 s, both separate concerns). The 65% execute
drop is the cold-cache win — each redundant executescript() had
been triggering disk reads at the 75 s scale the reviewer reported.
Tests (6, all green): first connect runs all 7 probes, second
connect runs zero, schema integrity preserved across re-opens,
explicit invalidation re-probes, distinct paths each get one probe,
clear-cache helper works.
Full suite: 1306 passed, 36 skipped. Found and fixed an FK CASCADE
regression mid-implementation: PRAGMA foreign_keys = ON was inside
SCHEMA_SQL, so memoization was silently turning it off on subsequent
opens. test_burn_doc.py caught it. Moved to the per-connection
pragma block.
Ticket #000026 status: Phase 1 landed; Phase 2 (baseline artifact)
and Phase 3 (warrant-quality finding) queued.
Profiled the `virt-back` query against ~38 GB of real shards
(2026-05-08, warm cache). Total wall 14.5 s; LLM 2.7 s; search
9.9 s — that's the latency budget breakdown.
Headline finding: 588 SQLite `connect()` calls per query, each
running 7 forward-migration probes on already-fully-migrated
shards. 10,623 SQLite executes total. Reviewer's 75 s cold-cache
report tracks the same shape; warm cache only masks part of it.
Ticket bundles:
- Phase 1 (latency fix): per-process migration memoization. Smallest
patch; no schema impact; ~30 LOC + regression test. Target <5 s
search on real shards.
- Phase 2 (baseline artifact): bench/scripts/real_shard_baseline.py
+ bench/results/real-shard-baseline.json + make bench-real-shard.
Captures wall/search/LLM timings, primary-source-at-rank-1, used
flags, capital ledger + memory deltas, ForkScore preview.
- Phase 3 (findings): fold the warrant-quality observation
(copyright-footer vs author-metadata) into the baseline report
as a finding. Implementation deferred to a follow-up ticket.
Out of scope captured explicitly: authorship warrant ladder
(separate ticket post-latency), CI re-enable (small commit, not
a ticket), public docs refresh (adjacent, separable), ForkScore
live wiring (#000012 Phase 1b).
Index updated. Next ID 000027.
Reviewer note (2026-05-08): the review claimed the index showed
"5 open, 24 closed" but no count line ever existed in TICKETS.md;
the 6 active rows (5 open + 1 rolling) are correctly listed. No
fix needed.
`make query Q="0.1 + 0.2"` used to return `no_sources` because
arithmetic-shaped input has no FTS5 hits in any text shard. Two
surfaces close that gap.
**`arborist canon <key> "<input>"`** — direct π* call, no shards,
no LLM, no audit chain. Pure projection:
$ arborist canon arithmetic@v1 "0.1 + 0.2" → 3/10
$ arborist canon logic-kernel@v1 "A IMPL B" → (NOT A OR B)
$ arborist canon --list → registry contents
$ arborist canon --json arithmetic@v1 "0.1+0.2" → SHA-256 envelope
**Math/logic preflight in `arborist query`** — pure-arithmetic and
pure-propositional questions short-circuit RAG and answer through
arithmetic@v1 / logic-kernel@v1 directly. Synthetic
`audit_mode=CANONICAL_PROJECTION`, renders as
`CANONICAL · via <pi_star_ref>`:
$ arborist query "0.1 + 0.2"
0.1 + 0.2
CANONICAL · via arithmetic@v1 0.0s (projected)
3/10
$ arborist query "(NOT B) IMPL (NOT A)"
(NOT B) IMPL (NOT A)
CANONICAL · via logic-kernel@v1 0.0s (projected)
(NOT A OR B)
Sniff is conservative: pure-arithmetic shape (digits + ops, no
letters) or pure-propositional shape (uppercase atoms + reserved
keywords only). Natural-language wrapping ("what is 0.1+0.2?")
falls through to RAG. PiStarError on a shape match also falls
through — preflight is best-effort, never blocking.
Disable per-call: `--no-canonical-preflight` flag,
`policy["canonical_projection_preflight"]=False`.
No schema changes: CANONICAL_PROJECTION is a render-layer audit_mode
token. No providence_cache writes, no audit_events, no
governance_policy_hash bump. The canonical bytes ARE the answer;
SHA-256 of the bytes is the equivalence-class identity (already
committed via the π* registry).
Side housekeeping: arborist/pi_star/__init__.py docstring caught up
with reality — six concrete π*'s ship today, only tabular-pinned@v1
remains as a stub.
31 new tests (preflight sniff + dispatch, query short-circuit,
contrapositive equivalence-class collapse, CLI subcommand exit codes
and JSON envelope, --no-canonical-preflight policy gate). Full
suite: 1300 passed, 36 skipped.
Completes the bridge: every 5F sub-battery now has an embedded
(Phase 1a) AND a live (Phase 1b.2) path. Per-task detail.source
distinguishes synthetic from live signal.
| Sub-battery | Live surface | Live fixtures |
|---|---|---|
| Formulate | qa.parse_claims.parse_pointer_claims | 15 (prior) |
| Feedback Loop | store.append_audit + memory.snapshot (temp shard) | 12 (prior) |
| Function | parse_pointer_claims + shape evaluators | 12 |
| Finetuning | selfmodel.store_snapshot + claims_for round-trip | 10 |
| Falsification | qa.verify.verify_quotes (real verifier) | 12 |
Function live: input_text routes through real parse_pointer_claims;
the same Phase-1a shape evaluators (shape_match / pointer_set_match
/ threshold_on_metric) run on the live-parsed output. Tests
parser→shape pipeline against actual organism behavior.
Finetuning live: gated via fixture's "live": true flag. Runner
writes parent + child SelfModel + capability_claim to a fresh temp
shard via real arborist.selfmodel.store_snapshot, reads back via
claims_for, runs the same improvement check. Tests the SelfModel
persistence + claim-attach surface, not just static fixture data.
Falsification live: answer_text + context routes through real
arborist.qa.verify.verify_quotes. Live signals translate the
verifier's audit_mode + verifier_method + unverified_quotes into
flat tags (UNGROUNDED, STRICT_<method>, HYBRID_<method>,
UNVERIFIED_QUOTE) the runner matches against expected_reason. One
fixture (5f-fal-live-003) deliberately documents a known soft-
signal gap — the entity strategy treats Insulin/Penicillin claims
as equivalent because both share "Alexander Fleming". Production
catches it via title-relevance + claim-lattice verifier; the
fixture pins the soft-path limit so future verifier changes
re-trigger review.
Surface:
- bench/batteries/b_5f.py — _live_function_produced,
_live_finetuning_measure, _live_falsification_violations
helpers + two-mode dispatch in run_function / run_finetuning /
run_falsification.
- bench/fixtures/5f/{function,finetuning,falsification}-live-v1.jsonl
(12 + 10 + 12 fixtures).
- Makefile: bench-5f-{function,finetuning,falsification}-live
targets; bench-5f-live aggregate now covers all five sub-batteries.
- Tests: 9 new in tests/test_bench_batteries.py
- live + embedded paths for each sub-battery (6 tests)
- direct helper tests verifying the real arborist surfaces are
invoked, not stubs (3 tests)
Phase 1a fixture digests unchanged. _DEFAULT_FIXTURES still points
at synthetic Phase-1a fixtures so `runner --all` behavior is
identical and deterministic; live mode invoked via explicit
--fixtures path or make targets.
Full suite: 1210 passed, 36 skipped.
5F battery is now the first to bridge synthetic→live across every
sub-battery. The pattern + live fixture format are reusable for
5R Phase 1b.2 (when SelfModel-backed workspace ops want live
verification).
First sub-battery to bridge from synthetic gold output to actual
organism behavior. run_formulate now supports two fixture modes
selected per-task:
- Embedded (Phase 1a): produced_lattice in the fixture. 10 seed
fixtures continue to pass via this path.
- Live (Phase 1b.2): only input_text in the fixture; runner calls
arborist.qa.parse_claims.parse_pointer_claims(input_text) and
matches the live output against expected_lattice.
Embedded takes precedence if both fields are present. Per-task
detail.source ("embedded" | "live") surfaces in bench output so
synthetic vs live signal is distinguishable.
Surface:
- bench/batteries/b_5f.py — _live_produced_lattice helper +
two-mode dispatch in run_formulate
- bench/fixtures/5f/formulate-live-v1.jsonl — 15 live-mode fixtures
with input_text + expected_lattice (no produced_lattice)
- Makefile: bench-5f-formulate-live target
- Tests: 4 new in tests/test_bench_batteries.py
- live path routes through real parser, all 15 pass
- embedded path still works (10 Phase-1a fixtures)
- _live_produced_lattice helper directly verifies parse output
- fixture missing both fields fails cleanly with explanatory reason
Phase 1a fixture digests unchanged. _DEFAULT_FIXTURES still points
at formulate-v1.jsonl so `runner --all` behavior is identical;
live-mode fixtures invoked via explicit --fixtures path.
Full suite: 1196 passed, 36 skipped.
Pattern set. Function/Finetuning/Falsification/Feedback Loop
follow in subsequent commits.
Phase 2 of #000021. React/Rearrange/Restore/Replicate/Resonate over
the workspace surface — selfmodel_records (#000014) + memory_records
(#000017), both landed earlier today. Closes the gap that gated 5R
since the substrate work shipped.
Sub-battery semantics (per SQD whitepaper §9.3 + ticket #000021 §4.2):
- React: incorporate new fact/constraint. Workspace = (snapshot_t0,
snapshot_t1, expected_delta). Pass = added_facts present + removed_facts
absent in t+1.
- Rearrange: restructure without semantic shift. Re-canonicalize
different surface forms through a named π*; pass = bytes match
expected_equivalent flag. Tests the order-invariance contracts in
SelfModel (capability_claim_hashes sorted) and Memory (branches
sorted by branch_id).
- Restore: retrieve prior fact. Workspace = (history[], current_facts[]).
Pass = fact in current OR any historical snapshot.
- Replicate: independent canonical encodings via π*. Same input run
N times must yield byte-equal output. Tests determinism contract.
- Resonate: variance across N runs. Deterministic π*'s yield
distinct=1; expected_max_distinct=1 enforces zero-variance contract.
Surface:
- bench/batteries/b_5r.py (5 deterministic runners; no LLM-as-judge)
- bench/fixtures/5r/{react,rearrange,restore,replicate,resonate}-v1.jsonl
(30 each = 150 new fixtures)
- runner.py registers 5r in _BATTERIES + _DEFAULT_FIXTURES
- Makefile: bench-5r + bench-suite (5S+5T+5F+5R aggregate)
Final tally:
5S syntax/semantics/syllogism/synthesis/semiotics 108
5T transfer/transfer-learning/triangulation/... 154
5F function/finetuning/falsification/... 50
5R react/rearrange/restore/replicate/resonate 150
TOTAL: 462 fixtures across 21 sub-batteries — 100% pass.
Tests: 6 new in tests/test_bench_batteries.py + adjustment to
test_session_integration.py for the 312→462 count + 5R sub-battery
presence assertion. Full suite: 1192 passed, 36 skipped.
Closes#000021. Phase 3 (external-corpus expansion) remains open
under the ticket but does not gate closure — the complete
Dav1DPrometheus surface is now executable infrastructure.
The top-level module diagram still used the old aborist- (one R) prefix
from before the package rename. arborist.unturf.com served from the
symlinked docs/_source/diagrams/, so the live URL
arborist.unturf.com/en/diagrams/arborist-modules.svg 404'd because the
file on disk was aborist-modules.svg.
Other diagram base names (ingest-pipeline, mesh-*, query-pipeline,
verifier-ladder) were never aborist-prefixed; only this one needed it.
Per fox's 2026-05-08 review of fbd99a8: implement adaptation_efficiency
and feedback_efficiency in run_finetuning + run_feedback_loop with
explicit sentinels — not Python floating-point accidents.
_efficiency(gain, cost) helper:
- cost > 0: standard ratio
- cost == 0, gain > 0: EFFICIENCY_INFINITE (free improvement)
- cost == 0, gain == 0: EFFICIENCY_UNDEFINED (= 0.0; no signal)
- cost == 0, gain < 0: -EFFICIENCY_INFINITE (free regression)
Battery-level metrics report mean_finite (computed over finite
values only) + infinite_count + neg_infinite_count so the mean
stays dimensionally truthful and consumers can pivot on the special
buckets separately.
Phase 1a cost proxies:
- run_finetuning: _capital_cost_delta sums resource_budget
(max_compute_ms_delta * 1e-3 + max_storage_delta_bytes / 1e6).
Phase 1b.2 will replace with real capital_ledger reads.
- run_feedback_loop: chain length = cost. Phase 1b.2 capital_ledger
integration replaces it.
Tests added (7):
- _efficiency over four boundary cases
- 5F finetuning + feedback_loop emit the new metrics keys
- Synthetic zero-cost finetuning fixture verifies +inf path
Full suite: 1110 passed, 36 skipped.
Closes the one actionable from the fbd99a8 review.
Captures design for an action-provenance DAG layer downstream of
final_label - five new stages (action_plan -> tool_call ->
tool_output -> postcondition_check -> action_label) - and why this
stays a research doc rather than an open ticket today.
Three options analyzed: Option A in-tree action DAG (identity
drift), Option B sidecar package (recommended; preserves the
verified-answer-cache identity by chaining a separate action_root
that cross-links into run_dag_root), Option C out-of-scope.
Promotion criteria spelled out so the doc graduates to a ticket
when the first agent use case shows up. Cross-links #000001
(upstream provenance gap), #000022 (LossReport, same axiom one
stage upstream), #000012 (v8 selection could later score action
histories), and the 2026-05-07 arborist-vs-donto comparison.
TICKETS.md gains a pointer in "Distinction from other docs" so
future shifts find the doc.
Per the three review responses (~/Downloads/RESPONSE_*) folded in
2026-05-08, the 5S / 5T / 5F tickets are corrected from "text-only
with future hooks" to "carrier-aware design from day one." Phase 1
implementation stays text / claim-lattice / memory-root only, but the
fixture schema MUST accommodate future visual / world / code / audio /
sensor / hidden-channel-detection carriers without re-authoring.
Common corrections across all three tickets:
- Mandatory fixture metadata: carrier, domain, pi_star_ref,
loss_report_refs, modality_notes.
- Unsupported carriers MUST fail or skip explicitly with
reason="unsupported_carrier" — never silently accepted.
- No LLM-as-judge in any runner.
- Hidden-channel work is defensive only (detection / flagging),
never generation or concealment.
Per-ticket headlines:
#000023 — 5S
Syntax / Semantics / Semiotics defined as carrier-general operations
over sign-bearing representations. Semiotics gets the biggest
correction: visual symbols, layout, metadata, encoded sign systems
are valid carriers (Phase 1 still text-only). Synonym source
policy: concept_relations.relation_kind='synonym' only for v1
positives.
#000024 — 5T
Vocabulary alignment with Dav1DPrometheus authoritative wording
(Transfer→Transfer Learning, Truth→Truthtables, Timing→Time).
Transitivity gets a typed-relation whitelist (implies, subset_of,
ancestor_of, before, less_than) — not all edges transitive.
Truthtables capped at N=2..4 to avoid combinatorial blowup. Time
is the first sub-battery where v8 substrate (memory_root #000017
+ selfmodel #000014) becomes a measurable bench target.
#000025 — 5F
New axis. Function/Finetuning/Falsification/Formulate/Feedback
Loop. Folds in the state-space synthesis: SQD + v7 + 5S/5T/5F +
arborist together instantiate a discrete state-space/time
Ω_t = (W, I, C, L, MRoot, SMRoot, PRoot, BRoot, ARoot) with
Ω_{t+1} = T(Ω_t, Δ_t). Counting / mathematics / logic / time
emerge as auditable operations over committed state, not text from
a latent model. adaptation_efficiency and feedback_efficiency
metrics hook into the capital ledger (#000020) so v8 fork choice
has cost-aware fitness signals. Falsification fixtures tagged
with verifier_method_root so verifier shape changes warn rather
than false-fail.
All three tickets remain "open · awaiting go/no-go" — design-only.
Implementation tickets land in follow-up commits when fox approves
the corrected scope.
Source: Legally Unprecedented Dav1DPrometheus (BasementAGI host,
Where The mAGIc Happens). Honoring his framework.
Three new design-only tickets surfacing the gaps between arborist's
current bench harness (ticket #000021 Phase 1a, landed) and
Dav1DPrometheus's authoritative 5S/5F/5T evaluation framework.
- #000023 — 5S Phase 1b: real implementations + fixtures for
Syllogism, Synthesis, Semiotics (currently stubbed).
- #000024 — 5T Phase 1b: rename Transfer→Transfer Learning,
Truth→Truthtables, Timing→Time to honor Dav1DPrometheus's
vocabulary; ship real Triangulation, Truthtables, Transitivity,
Time runners (currently stubbed). Time integrates with
memory_root (#000017) for the first measurable use of v8
substrate as fitness target.
- #000025 — 5F battery: entirely new — Function, Finetuning,
Falsification, Formulate, Feedback Loop. arborist had no 5F
coverage before this ticket; the SQD whitepaper omitted the
axis. Each sub-battery integrates with surfaces already shipped
(selfmodel_records, providence_cache.falsification_state,
memory_branch_summaries).
Source attribution: Legally Unprecedented Dav1DPrometheus
(BasementAGI host). Honoring his framework as the authoritative
taxonomy for non-embodied AGI evaluation.
Next ID bumped 000023 → 000026.
Per fox's "partial punt on larger ones" — ships the bench/ skeleton +
small seed fixture sets so future v8/v7-W/SelfModel work can cite a
real fitness target. Full Phase 1 (50-200 fixtures per sub-battery)
and Phases 2-3 stay open in the ticket.
Phase 1a delivers:
- bench/batteries/{base,b_5s,b_5t,runner}.py — Battery protocol,
BatteryResult, fixture-digest helpers, CLI runner.
- Seed fixtures:
- bench/fixtures/5s/syntax-v1.jsonl — 10 tasks against
wikitext-base@v1 and claim-lattice@v1
- bench/fixtures/5s/semantics-v1.jsonl — 8 equivalence tasks
- bench/fixtures/5t/transfer-v1.jsonl — 4 paraphrase-invariance
tasks
- Runners for 5S Syntax, 5S Semantics, 5T Transfer. Other 5S/5T
sub-batteries are stubs returning zero-task results.
- Makefile targets: bench-5s, bench-5t, bench-5s5t.
- runtime_digest field captures the active π* registry fingerprint
so a registry change surfaces in bench results.
Tests: tests/test_bench_batteries.py (17 cases). Full suite:
1076 passed, 36 skipped. `make bench-5s5t` runs end-to-end and
emits JSON results.
Ticket #000021 status: in progress · Phase 1a landed; Phase 1b/2/3
remain open.
Doc-only landing. docs/spec-methodology.md codifies the discipline
arborist already practices — versioning rule, round-trip discipline,
soundness/completeness honesty, default-value greenfield rule,
sidecar separation — so new π*, V, and policy-field authors don't
re-derive it from audit-chain failures.
Three author-class sections each ship with:
- Five questions the author must answer before landing.
- Worked example drawn from arborist's existing surface.
- One-page checklist.
Worked examples cited:
- π* — wikitext-base@v1
- V — paraphrase strategy
- policy field — quantifier_guard_apply_caps
Cross-references to bench-maxing, seven-point-program, pi-star-
composition, concept-relations-design, and CLAUDE.md.