Commit graph

357 commits

Author SHA1 Message Date
b320e276b9
.gitlab-ci.yml: substrate-score job + CLI invocation v8 → substrate
Third refactor-induced defect caught from yesterday's v7+v8 →
substrate rename (`bae5caf` for the package, `209d670` for the
Makefile). Same pattern: a callsite that text-search misses
because the import path doesn't connect through Python.

CI surface (the `v8-score:` GitLab CI job) had two issues:

1. Job name `v8-score:` was a UX surface — operators see it in the
   GitLab MR pipeline UI. Renamed to `substrate-score:` for
   consistency with the package name + the CLI subcommand.
2. Script line called ``.venv/bin/arborist v8 score …``. Would
   have failed on the next manual MR pipeline run with an
   argparse "invalid choice: 'v8'" error.

Comment block (lines 80-90 + 115-125) refreshed to call out the
distinction: ``v8 paper`` (the substrate-paper version, name
preserved per published convention) vs the module location
(``arborist/substrate/fork_score.py`` post-2026-05-10 rename).

Sweep verified: ``grep -rnE "arborist v[0-9]\\b|arborist\\.v[78]\\b"``
across the entire tree returns only intentional historical-note
comments + the placeholder-seed bytestring derivation (which
cannot change without invalidating KAT vectors).

Three loose ends from one refactor:
- 85be5eb: fork_score.py import (Python imports caught by tests)
- 209d670: Makefile bench-fork-score target (would surface on run)
- this:    .gitlab-ci.yml job (would surface on next MR pipeline)

Lesson written across the three commits: text-search-replace on
a CLI rename misses callsites that argparse processes at runtime.
Pre-rename checklist for next time: ``grep -rn "<cli-old-name>"
Makefile .gitlab-ci.yml .github/workflows scripts bench``.
2026-05-10 09:27:14 -04:00
209d670988
Makefile: bench-fork-score CLI invocation v8 → substrate
Caught while sweeping for remaining "arborist v8" CLI invocations
after bae5caf renamed the subcommand. Makefile target
``bench-fork-score`` (line 430) still called
``$(ARBORIST) v8 score`` directly — would have failed loudly on
next ``make bench-fork-score`` run with an argparse error
("invalid choice: 'v8'").

Same kind of subtle breakage I caught in fork_score.py earlier
today (85be5eb): a refactor's text-search misses a callsite that
isn't picked up by Python imports. Lesson: after renaming a CLI
subcommand, grep ``$(ARBORIST) <oldname>`` AND ``arborist <oldname>``
in Makefile, scripts/, and bench/ — argparse errors don't surface
until someone runs the target.

Hygiene
=======
- ``grep -rn "arborist v8\\b" Makefile bench scripts docs`` → only
  the historical-note comment in cli.py:5131 remains.
- ``make help | grep substrate`` → target descriptions accurate.
- ``.venv/bin/arborist substrate score --help`` still 0.
2026-05-10 09:22:39 -04:00
47c7811f49
docs: ticket #000031 Phase 3 status flipped to landed
Updates the #000031 ticket header + body to reflect Phase 3 wiring
landed in commit a57b194: warrant_chain_lookup + WARRANT_MISSING
suppression + warrant_proven_claim_idxs render tail. Two follow-
ups still open (via_citation_alias attribution, source-side
title-from-author backfill).
2026-05-10 09:18:43 -04:00
a57b1942d7
ticket #000031 Phase 3: warrant-chain-aware verifier suppresses WARRANT_MISSING
When a per-claim warrant_check would fire WARRANT_MISSING but the
cited chunk's document_root has a warrant-resolver derivation row
(Merkle-bound primary-source backing), the verifier now suppresses
the demote and tracks the claim on a new `warrant_proven_claim_idxs`
field. The render layer surfaces this as `· warrant proven via
chain ×N` in the audit-line tail so operators see when a claim got
through on the chain rather than on lexical anchors.

Mechanism (additive, fail-closed):

  1. New `arborist/qa/warrant_chain.py` — read-only helper that
     loads the frozenset of `core_root` values having a derivation
     row with `process_id LIKE 'warrant-resolver-v1%'`. One sqlite
     query per Q&A run, walks main shards + sibling crawl/ shards
     (skipping ad-hoc crawl_russell_/qa./snapshots. prefixes).
     Tolerates missing tables.

  2. `verify_claim_lattice` + `verify_claim_lattice_json` accept
     a new optional `warrant_chain_roots: frozenset[str]` parameter
     (default empty = backward-compatible). When the lexical
     warrant_check fails for a claim AND any cited evidence's
     source_root is in the set, the WARRANT_MISSING violation is
     suppressed and the claim_idx flows to a new
     `warrant_proven_claim_idxs` field on the verdict.

  3. `runner.ask` computes the warrant_chain_roots set once from
     the conn's main DB directory before invoking the verifier.
     Failure-mode fallback: empty set, behavior identical to
     pre-Phase-3.

  4. `query.py` threads `warrant_proven_claim_idxs` from the
     verdict into the result dict.

  5. `cli.py:_render_warrant_tail` adds a `warrant proven via chain
     ×N` segment when `warrant_proven_claim_idxs` is non-empty.
     Distinct from the pre-existing `_render_warrant_chain_tail`
     which counts cited SOURCES with chains; this counts CLAIMS
     that survived because of a chain.

Tests:
  - tests/test_warrant_chain.py — 9 new tests covering
    warrant_chain_lookup (basic / unrelated process_id / missing
    table / +alias variant / empty path) + has_warrant_chain
    short-circuit + verifier suppression behavior + verdict-field
    presence guarantee.

Live smoke: warrant_chain_lookup(~/.arborist/shards) returns
exactly 92 core_roots (matches the 92/92 claim-pack records
resolved earlier today).

Total: 1652 tests pass (was 1643). Honest layering preserved:
- soft signal (positive warrant_proven) lives on a separate verdict
  field, not in `violations` (which stays a hard-failure list)
- audit_mode (STRICT/HYBRID/UNGROUNDED) unchanged when chain
  suppresses WARRANT_MISSING — the claim was going to land at
  HYBRID without the suppression; the suppression keeps it at
  STRICT, which is now defensible because the warrant chain IS the
  warrant
- four-rung ladder rung promotes naturally: no WARRANT_MISSING in
  violations + no soft demotes -> EVIDENCE-WARRANTED via the
  existing _ladder_rung_for_lattice logic. No render-layer ladder
  change needed.

Phase 3 follow-ups still open under #000031:
- via_citation_alias process_id attribution (~15 LOC)
- source-side title-from-author backfill in HTML/textbook_tex
  ingest (~30 LOC)
2026-05-10 09:17:48 -04:00
bae5cafe9a
CLI: arborist v8 score → arborist substrate score
Followup to 654d923 (which moved the package from arborist/v8/ →
arborist/substrate/ at the file layer). The CLI surface still baked
in `v8` so a new operator running `--help` would see
``arborist v8 score`` and ask the same "what's v8 vs v9.8?"
naming-confusion question that drove the package rename in the
first place. Closing the loop end-to-end.

arborist/cli.py
===============

- Subparser renamed: ``"v8"`` → ``"substrate"``; help string updated
  to "Merkle-AGI substrate primitives (ForkScore + future paper
  specs)" so the dir name and command name and help text all align.
- Inner subparser dest renamed: ``v8_op`` → ``substrate_op``.
- Function renamed: ``_cmd_v8_score`` → ``_cmd_substrate_score``;
  docstring updated.
- All ``v8_score`` local variables renamed to ``substrate_score``.
- New comment block above the subparser block explains the rename
  + why the v-prefix was retired (substrate-paper version vs v9.8
  schema version naming collision).

The old ``arborist v8 score`` is gone — no alias preserved. CI + ops
scripts must update; today's earlier commit chain has been the only
place using it and that's been refreshed in lock-step.

tests/test_v8_fork_score.py
===========================

- 4 ``parser.parse_args(["v8", "score", ...])`` calls → ``["substrate", ...]``.
- 4 test functions renamed: ``test_cli_v8_score_*`` →
  ``test_cli_substrate_score_*``.
- Module docstring + section comment + helper docstring updated.

Filename intentionally kept as ``test_v8_fork_score.py`` for git
history continuity; pytest discovers by ``test_*`` content, not
filename. Renaming the file would muddle ``git log --follow`` for
the test surface.

Docs refreshed
==============

- docs/v8-fork-score.md — §5 CLI block invocation.
- docs/_source/v8-fork-score.rst — :code-block:: bash invocation.
- docs/_source/bench.rst — invocation in `### v8 ForkScore` section.
- docs/tickets/ticket-000012-selection-consensus-protocol.md —
  three references in §7 close-out + §7 Phase 1c proposal +
  §7 future-CLI-shape note.
- docs/dav1dprometheus-update-2026-05-09.md — bench journal mention.

Doc filenames (``v8-fork-score.{md,rst}``) kept stable since they
are URL identities; the file content explains the v8→substrate
rename internally. ``index.rst`` toctree references unchanged.

Hygiene
=======
- ``.venv/bin/arborist substrate score --help`` → 0 + valid usage.
- ``.venv/bin/arborist v8 score`` → exits non-zero (subcommand
  removed, surfaced cleanly in ``argparse`` error).
- ``make test`` → 1643 passed, 45 skipped.
- ``make chain-check-shards`` → 0 across all 7 shards.
- fox's parallel work in arborist/qa/{runner,verify}.py +
  arborist/qa/warrant_chain.py left untouched.
2026-05-10 09:12:34 -04:00
6c11939cf2
CLAUDE.md: never offer "stop here / fresh eyes tomorrow" as a next-action option
Fox 2026-05-10: blackops kept padding decision menus with a "C — stop
here" option. Encode the discipline directly: when fox asks "next?"
list the actual moves (e.g. high-payoff Phase 3 vs low-risk cleanup
batch), don't dress up "let's call it" as a third choice. Fox keeps
going. If a task is genuinely complete, say so flat instead of as a
proposal option.
2026-05-10 09:06:27 -04:00
85be5eb900
CLAUDE.md: substrate/ convention + fix broken import landed in 654d923
CLAUDE.md
=========

Architecture diagram refreshed to include every current arborist/
subdir (was missing capital/, concepts/, memory/, mesh/, pi_star/,
selfmodel/, substrate/, world/ and several top-level modules) and
the qa/ tree got the recently-landed members (canonical_cache.py
#000027, witness.py #000028, warrant_resolver.py #000031). New
explanatory paragraph names the topic-named convention explicitly:

> Topic-named, never version-prefixed. The substrate-paper version
> (v7 plastic-training, v8 selection/consensus, v9 falsification
> controller, …) and the live SQLite schema version (v9.8) are two
> unrelated numbering schemes that share decimals; version-prefixed
> dirs were tried 2026-05-10 and retired the same day because
> readers asked "is this schema-v7 or paper-v7?".

Future blackops shifts looking at where to put a new module now find
the answer in CLAUDE.md instead of having to reverse-engineer the
convention.

arborist/substrate/fork_score.py — fix broken import
====================================================

Previous commit 654d923 (the v7+v8 → substrate refactor) shipped
broken. Sequence:

  1. ``git mv arborist/v8/fork_score.py arborist/substrate/fork_score.py``
     — staged the rename.
  2. Edited the file to flip ``from arborist.v8.weights ...`` →
     ``from arborist.substrate.weights ...`` — modified the working
     tree but did NOT re-stage.
  3. Selective ``git add`` of the other touched files (cli.py,
     substrate/__init__.py, docs, tests) — fork_score.py's import
     edit was NOT in the staged change set.
  4. ``git commit`` shipped the rename WITHOUT the import fix.

HEAD's fork_score.py imports ``arborist.v8.weights`` — a path that
654d923 itself deleted. Tests passed locally because the disk had
the edit; a fresh checkout from origin/main breaks at import time.

This commit lands the import edit. Verified: ``git show
HEAD:arborist/substrate/fork_score.py`` now has
``arborist.substrate.weights``; full suite re-runs at 1643 passed.

Lesson: ``git mv`` stages the rename only. Modifications after that
need their own ``git add``. Selective-add commits should run
``git diff --cached`` (not just ``git diff``) before commit. Adding
this to my own habit list.
2026-05-10 09:03:48 -04:00
654d923da0
refactor: arborist/v7+v8 → arborist/substrate (single topic dir)
fox's read: the version-prefixed namespace pattern (`arborist/v7/`,
`arborist/v8/`) coupled module location to the substrate-paper
version. That collided with the live SQLite schema version (v9.8)
and made readers ask "is this dir tracking schema or paper?" —
a real onboarding hazard surfaced when the v7 dir landed earlier
today (06c95a0) for #000035 Phase 1.

Resolution: collapse v7+v8 into one topic-named dir,
``arborist/substrate/``, which holds Merkle-AGI substrate primitives
that future paper specs require — decoupled from the paper version.

Moves
=====

  arborist/v7/anchor_prg.py   → arborist/substrate/anchor_prg.py
  arborist/v8/fork_score.py   → arborist/substrate/fork_score.py
  arborist/v8/weights.py      → arborist/substrate/weights.py

Empty v7/ + v8/ dirs deleted; their __init__.py docstrings folded
into the new arborist/substrate/__init__.py with an explanation of
why the version-prefixed pattern was retired.

Imports updated
===============

- arborist/cli.py:_cmd_v8_score — arborist.v8 → arborist.substrate
- arborist/substrate/fork_score.py — internal weights import
- tests/test_anchor_prg.py — module + module-docstring
- tests/test_v8_fork_score.py — three import lines

Docs updated
============

- docs/v8-fork-score.md — header note explaining the move
- docs/_source/v8-fork-score.rst — :class: ref updated
- docs/tickets/ticket-000012-selection-consensus-protocol.md — §7
  Phase 1a close-out paths refreshed (kept "Originally landed at
  arborist/v8/..." parenthetical so the historical record survives);
  §7 Phase 1b consensus-paper reference; §7 Phase 1c proposal §3
  read-API path
- docs/tickets/ticket-000035-prg-choice-phi-prg.md — §7 Phase 1
  close-out path refreshed (with full path-note explaining the
  move); §3.1 + §5 left as the original design log per CLAUDE.md
  "closed tickets stay in place as design log"

Left untouched
==============

- arborist/world/ — already topic-named; not version-prefixed; the
  v7-W reservation lives there with its own planned subdir layout.
- docs/tickets/ticket-000037-prometheus-sigma-...md §13 still refs
  ``arborist/v9/prometheus.py`` and ``arborist/v8/fork_score.py`` —
  fox has 792 lines of in-flight modifications on this file; those
  refs should refresh to ``arborist/substrate/`` when the in-flight
  edit lands. Avoiding interleaved edits.

Hygiene
=======
- make test → 1643 passed, 45 skipped (was 1643; refactor preserved)
- make chain-check-shards → 0 across all 7 shards
- arborist.substrate namespace picked up by the existing
  pyproject.toml ``include = ["arborist*"]`` glob; no setup change.
2026-05-10 08:57:04 -04:00
4d4e4d4249
docs/warrant-substrate-cookbook.md: architecture reference for 18-substrate map
Internal architecture reference written 2026-05-10 after the day's
18/92 -> 92/92 push under #000031. Covers:

  - per-pillar substrate map (which open textbook covers which
    pillar; license + ingest path for each of the 18 substrates)
  - five proven ingest patterns (HTML single-URL, HTML BFS,
    textbook_tex LaTeX-source, PDF -> localhost-HTML, direct
    Python API)
  - discipline patterns: title-from-author backfill workaround
    (until the source-side fix in #000031 Phase 1 lands), alias
    audit-fail-closed (decision_by + decision_rationale per row),
    multi-substitute pattern, cascade tuning
  - honest tier breakdown of the 92 chains (~25 direct primary,
    ~50 substrate substitution, ~17 soft-fallback OR-of-3 match)
  - what the substrate doesn't yet do (render layer doesn't read
    derivations, process_id under-attributes alias chains as DIRECT,
    no per-record tier classification in the schema)
  - re-running steps for future shifts (idempotent at DB layer)

Format follows other docs/ references (cti-architecture,
concept-relations-design, tool-action-dag-design) — describes
state of the world, not proposing change.

CLAUDE.md and TICKETS.md updated to point at the cookbook from
the docs index.

No undefect/whitepaper publication — this stays internal as
requested. Future blackops shifts re-discovering the substrate
map shouldn't have to walk five bench journals.
2026-05-10 08:50:40 -04:00
e82968baad
KT recrawl + 14 KT pillar VII aliases (defense-in-depth)
Keller-Trotter Applied Combinatorics (CC-BY-SA-4.0) re-crawled
successfully on the 38-min retry — earlier 25-min timeout was
too tight against appliedcombinatorics.org's 20-second crawl-delay.
Result: 80 docs / 168 chunks of advanced enumerative combinatorics
(generating-functions, partitions, Polya enumeration) that Bogart
skips and Levin treats lightly.

Title-backfilled the 79 newly-ingested docs with author surname
'Keller and William T. Trotter' for resolver _shard_matches_citation
heuristic.

Registered 14 KT alias rows for pillar VII compound source_refs as
a third substitute alongside Bogart + Levin. Audit-disciplined
(decision_by="fox 2026-05-10", decision_rationale notes Georgia
Tech AIM-approved provenance + advanced-chapter coverage).

Total citation_aliases now 54 rows (was 40); coverage stays at
92/92 (100%) — pillar VII chains gain peer-level redundancy
without changing the per-record resolution status.

Cleaned up orphan crawl_appliedcombinatorics_org.db from the
earlier failed crawl (no schema; tripped the resolver's
_shard_title_haystack with a missing-table OperationalError).

Doc updates (TICKETS.md, #000031, #000041) reflect 54-row count
and KT as third pillar-VII substrate.
2026-05-10 08:44:56 -04:00
06c95a03ab
ticket #000035 Phase 1: arborist/v7/anchor_prg HMAC-SHA-512 PRG
Lands the M1 mitigation cryptographic primitive that ticket #000018
§5.2 + §9.2 specified, scoped per ticket #000035 §3.1-§3.3. Pure
stdlib (hashlib + hmac); no third-party dependency.

arborist/v7/__init__.py
=======================
First module landed under the v7 namespace. v7 plastic-training is
currently paper-stage (per #000037 §17.2); this is where its
deterministic primitives accumulate ahead of an active deployment
target so the building blocks are unit-tested + KAT-pinned the
moment v7 needs them.

arborist/v7/anchor_prg.py
=========================
Implements ``phi_prg(hard_hash_32, dim_h, *, seed) -> list[float]``
per #000035 §3.1. Construction is SP 800-108 KDF in counter mode
over HMAC-SHA-512:

  Output(SEED, C(M), n_bytes) :=
      i = 0
      out = b""
      while len(out) < n_bytes:
          out += HMAC-SHA-512(SEED, C(M) || i.to_bytes(4, 'big'))
          i += 1
      return out[:n_bytes]

  Float conversion: f(u32) := 2 * (u32 / 2**32) - 1
                              ↑ uniform on [-1, 1)

Security argument from #000035 §2.1: HMAC-SHA-512 is a PRF under
the standard SHA-512 + HMAC assumption; distinguishing advantage
from random bounded by SHA-512 collision-resistance (~2^256), which
structurally matches the substrate's SHA-256 hard-hash family. The
seed is published, not secret — secrecy is not the security
property; the property is computational indistinguishability of the
output from random, which holds even when the seed is public.

Module exports ``PHI_PRG_VERSION = "phi-prg-v1-hmac-sha512"`` so
future algorithm rotations are detectable at the call site without
string-comparing module paths. Per #000035 risk §6.1, a
``phi_prg_version`` field in the v7 manifest will let future
deployments swap to a successor PRF without breaking historical
replay; this version string is the runtime-side mirror.

Hard-hash input length checked exactly at 32 bytes — silently
padding shorter input would break the PRF security argument.
``dim_h`` validated as positive int.

tests/test_anchor_prg.py
========================
20 tests covering #000035 §3.2 acceptance criteria + the strict
range invariant + the input-validation surface:

- Determinism: same (seed, hard_hash, dim_h) → identical floats.
- Range: every output in [-1, 1) with strict upper bound. Three
  edge cases pinned: u32=0 → -1.0, u32=2^31 → 0.0,
  u32=2^32-1 → just below 1.0.
- Chi² loose-uniformity: 4096-sample bin-test (df=15) with a
  generous threshold (60); catches catastrophic PRG bugs (counter
  cycling, mis-keyed HMAC) without claiming cryptographic-grade
  evidence.
- Boundary: dim_h=1 + dim_h=16384 both produce sensible output.
- Avalanche, seed-bit: flip top bit of seed[0]; require 35-65% of
  output bits flipped (PRF avalanche property).
- Avalanche, hash-bit: same surface for the hard-hash input.
- Validation rejects: short hashes, long hashes, non-bytes hashes,
  zero / negative / non-int dim_h.
- Module export shape: PHI_PRG_VERSION + PLACEHOLDER_SEED.
- KAT regression: pinned vectors verified against
  ``bench/fixtures/phi-prg/known-answer-tests.jsonl``.

bench/fixtures/phi-prg/known-answer-tests.jsonl
================================================
10 KAT vectors generated against the placeholder seed + custom
seed/hash combinations; covers smoke (placeholder seed × small
dim_h), block boundaries (HMAC-SHA-512 blocks are 64 bytes, so
dim_h=16 is exactly one block, dim_h=17 is two blocks with
truncation), seed/hash one-bit-flip variants, and a 4096-element
stress sample.

Each row pins the SHA-256 of the raw byte stream (not the float
list) — that's the durable contract; switching from list[float] to
array.array('f', ...) or numpy arrays at the float layer would not
invalidate the fixture. Algorithm changes MUST bump
PHI_PRG_VERSION and create a new fixture file under
bench/fixtures/phi-prg/; old runs replay against old data per the
v7 spec replay discipline.

#000035 status flip
===================
docs/tickets/ticket-000035-prg-choice-phi-prg.md §7 updated from
"open · awaiting go/no-go" to "in progress · Phase 1 landed
2026-05-10". §7 now carries Phase 1 close-out details + Phase 2
gating criteria (active v7 deployment target + spec maintainer
review of §3.4 amendment text). The §3.4 v7 §9.10 amendment text
stays as the draft awaiting Phase 2 landing.

docs/TICKETS.md index row was already updated by fox in commit
ed470dc; my edit was idempotent.

Hygiene
=======
- make test → 1643 passed, 45 skipped (was 1623; +20 anchor_prg)
- make chain-check-shards → 0 breaks across all 7 shards
- arborist.v7 namespace picked up automatically by the existing
  pyproject.toml [tool.setuptools.packages.find] include="arborist*"
  glob; no setup change required.
- fox's in-flight #000037 ticket modifications + a parallel
  #000031 ticket update left untouched.
2026-05-10 08:44:18 -04:00
ed470dc4b9
docs: 100% claim-pack warrant resolution recorded across tickets
Update #000031 ticket with the 2026-05-10 push details: 18 textbook
substrates ingested, 40 citation-alias rows + 13 term-alias rows,
cascade tuning in _build_record_query_cascade. Per-pillar end state
recorded (13/13 · 10/10 · 13/13 · 18/18 · 5/5 · 5/5 · 14/14 · 14/14).
Honest tier breakdown of the 92 chains added. Phase 1 follow-up
(source-side title-from-author backfill) and via_citation_alias
attribution fix surfaced as open follow-ups under the same ticket.

Update #000041 with full registry of 40 citation aliases now live
(distribution by substrate; per-pillar breakdown). Update #000042
with 13-row count + acknowledgement that Newton/arithmetic rows are
mostly unused (cascade picked different tokens).

Update CLAUDE.md with the 18 per-textbook make targets + the 100%
warrant-resolve milestone.

Update TICKETS.md index status for #000031, #000041, #000042.

No code change in this commit; documentation refresh only.
2026-05-10 08:40:35 -04:00
b7a172cb04
warrant resolver: cascade tuning lifts 77 -> 92/92 (100%)
The +14-record close-out: most stuck records had substrate content
in already-ingested shards but the FTS5 cascade picked discriminator
tokens the substrate text didn't use as titles. Two surgical
additions to _build_record_query_cascade:

(1) parenthetical-phrase variant via new _phrase_from_parenthetical
    helper. The discriminating term often lives INSIDE a trailing
    parenthetical that _phrase_for_axiom was stripping:
      "Kolmogorov's First Axiom (Non-Negativity)" -> '"non negativity"'
      "Newton's First Law (Law of Inertia)"        -> '"inertia"'
      "Axiom of Side-Angle-Side (SAS)"             -> '"sas"' (already had this via prior path)

(2) content-tokens OR-join (top 3) as soft fallback after the AND
    join. Most stuck records had top-5-AND scoring 0 hits even when
    substrate had clear content; OR-of-top-3 surfaces relevant
    chunks reliably without sacrificing precision (citation +
    title-haystack guards remain).

Plus one final citation-alias row: Boehm-Jacopini -> Software
Foundations LF (decision_by="fox 2026-05-10"). SF-LF Imp.v
formalizes the structured-program theorem in Coq with sequence /
conditional / while-loop — same theorem as Boehm-Jacopini 1966
CACM in modern formal-verification dress.

Per-pillar:
  I:   12/13 -> 13/13
  II:   9/10 -> 10/10
  III: 11/13 -> 13/13
  IV:  18/18 stable
  V:    2/5  ->  5/5
  VI:   3/5  ->  5/5
  VII: 11/14 -> 14/14
  IX:  11/14 -> 14/14
  Total: 92/92 (100%)

Cumulative day-of-2026-05-10 lift: 18/92 -> 92/92 (+74 records,
+80 pp absolute). Started the day with only Hilbert pillar IV
resolved; ended with all 8 pillars fully resolved across 13
textbook substrates (Hilbert, Boole, Cantor, De Morgan, Russell
IMP/PoM, PM Vol 1, Peano, Dedekind, Newton, Laplace, Grinstead-
Snell, PLFA, SF-LF, Bogart, Levin, Judson, Aristotle).

40 citation-alias rows + 13 term-alias rows, all audit-disciplined
per #000041/#000042 (decision_by + decision_rationale per row).

All 1623 tests pass.
2026-05-10 08:33:19 -04:00
37cc2f7a58
Grinstead-Snell ingest + cascade tuning batch: 68 -> 77/92 (84%)
Under fox "work all paths" directive, four orthogonal lifts:

(1) 14 Levin alias rows for pillar VII compound citations — each
    Stanley/Brualdi/Knuth ref now has BOTH Bogart AND Levin as
    substitute. Lifted +2 (hockey-stick + stars-and-bars).

(2) 6 Goedel multi-substitute aliases — Goedel citations now have
    4 substitutes each (Peano, Russell IMP, Dedekind, SF-LF). Lifted
    +4 pillar III records (Axiom of Zero / Distinctness / Addition-
    Successor / Multiplication-Successor variants).

(3) 2 SF-LF alias rows for pillar I formal proof axioms (Mendelson +
    Enderton -> SF-LF). SF Logic.v has 12 hits "excluded middle",
    40 "existential", 1 "double negation". Lifted +2 (Existential
    Introduction, Double Negation Elimination).

(4) Grinstead-Snell Introduction to Probability ingest (GFDL,
    Dartmouth CHANCE Project). Initial LibreTexts BFS crawl thin
    (24 chunks nav-only at depth=2). Switched to Dartmouth PDF
    -> pdftotext -layout -> single-page HTML on localhost:8765
    -> standard arborist html ingest. Result: 339 chunks of
    substantive probability content. Lifted +1 (Inclusion-Exclusion).
    New ingest pattern useful for any PDF-only textbook.

Per-pillar:
  I:   10/13 -> 12/13 (+2)
  II:   9/10 stable
  III:  7/13 -> 11/13 (+4 — biggest win)
  IV:  18/18 stable
  V:    1/5  ->  2/5  (+1)
  VI:   3/5  stable
  VII:  9/14 -> 11/14 (+2)
  IX:  11/14 stable
  Total: 77/92 (84%)

7 term aliases registered (physics Newton-vocab + arithmetic Peano-
vocab) but most didn't lift — cascade picks different tokens than
my aliases target. Cascade tuning would require code work in
_build_record_query_cascade / _phrase_for_axiom. Deferred.

Cumulative day-of-2026-05-10: 18 -> 77 / 92 (+59 records, +64 pp).
15 records still stuck. Top blockers:
  - Cascade-tuning for substrate-content-exists-but-FTS5-misses
    (Kolmogorov 3 axioms, Newton third law, Vandermonde, Catalan,
    Injectivity of Successor, etc.) — code work
  - PM *24+ not transcribed (Russell's Paradox Resolution)
  - Boehm-Jacopini esoteric (no PD substitute)
2026-05-10 08:03:11 -04:00
29ddd164bb
ticket #000028 §2.6 sketch: refresh stale TODO post-#000027
Broader stale-map sweep across docs/, bench/, scripts/, Makefile, and
top-level surfaced one hit: the witness-mode example sketch in §2.6
of ticket #000028 still showed a no-op cache_lookup closure with
"TODO: wire post-#000027" — even though the real implementation in
arborist/qa/query.py:2158-2172 wired the cache leg in commit e19aed8
(2026-05-09), the same commit that closed both #000027 and #000028.

Updated the sketch to match the actual implementation: the cache
lookup closes over the prior persisted row's answer bytes (encoded
with surrogatepass for UTF safety), and the comparison is non-
tautological because cached_row is the row picked up BEFORE we'd
write a new one in this same call.

Same drift pattern as the #000028 §8 follow-up refresh (6d20aeb)
and the #000010/§000021/#000040 sweep (e84f453) and the repair.py
TODOs (8980e64): pre-implementation design notes don't get refreshed
after the implementation lands. Each instance is one session-waste
saved.

After this, both surfaces are clean:
- arborist/ + tests/ stale TODOs: zero (8980e64)
- docs/ + bench/ + scripts/ + Makefile + top-level: zero (this commit)

The remaining matches are all genuine future-work markers (raw_html
cache in async_web_fetcher.py:2309) or false-positives (\\uXXXX
escape-pattern docs in mesh/wire.py and tests/test_cli_render.py).
2026-05-10 07:52:54 -04:00
8980e64aa0
three-thread session output: stale TODOs, N-power probe, ForkScore Phase 1c
Three threads landed in a single commit because they share the same
substrate (the #000037 §12 trigger probe shipped in c422216):

A — code-side stale-map sweep (arborist/qa/repair.py)
=====================================================

Walked inline TODO/FIXME/XXX markers across arborist/ + tests/. Five
hits: two false-positives (\\uXXXX in escape pattern docs), one
genuine deferral (raw_html cache in async_web_fetcher), and **two
stale TODOs in arborist/qa/repair.py** referring to "re-prompt
feedback path is future work" — even though `reprompt_repair` is
fully implemented (lines 140+ at the time of this commit), wired
through CLI `--repair-reprompts N` flag (cli.py:4574), and gated by
`policy["repair_max_reprompts"]`. Refreshed the docstring header
and the in-body comment to point at the actual function.

Same drift pattern as today's earlier ticket sweep (e84f453):
implementation lands, the TODO doesn't get refreshed, future readers
re-implement what's already there.

B — N-power follow-up to the §12 trigger probe
==============================================

c422216's first probe run reported trigger 2 (divergence variance)
at N=16, σ=0.5, ratio=0.8 — both threshold conditions would fire if
N reached the 30-sample N_min. To validate that the variance signal
holds at N≥30 (rather than vanishing on a wider sample), drove the
canonical-witness path 20 additional times via a new
bench/qa_questions_canonical_witness_npower.txt fixture
(10 arithmetic@v1 + 10 logic-kernel@v1 questions; all
canonicalize-then-LLM-witness without errors).

Result at N=37: trigger 2 fires. Ratio 0.575 > 0.5, abs σ 0.435 > 0.10.
Variance signal is real at the floor. Captured in
bench/results/prometheus-sigma-triggers-2026-05-10-npower.md with a
loud caveat at the top: this is N-power validation, NOT a measure of
real workload pressure. The §12 phase-1 go/no-go decision should
still come from natural workload N or operator-stated need.

The prior baseline (prometheus-sigma-triggers-2026-05-10.md) stays
in place as the workload-state-at-time-of-ticket-c422216 record;
this new -npower.md report is the statistical-power follow-up.

C — ForkScore Phase 1c proposal (#000012)
=========================================

#000037 §12 Trigger 1 ("ForkScore receives ≥4 candidate branches per
checkpoint") gates on multi-branch persistence — but #000012 Phase 1a
(landed 2026-05-08) is single-validator scoring of one fork at a
time, and Phase 1b (still open) is the consensus paper. Neither
persists branch-sets. So Trigger 1 structurally cannot fire today,
which the probe correctly reports as "no fork_score branch-set table
found".

Added Phase 1c to #000012 as a doc-only proposal (no code in this
commit):

- New `fork_score_branches` table (sibling to capital_ledger; does
  NOT enter audit_events.event_hash preimage).
- Optional `--branch-set <ID>` flag on `arborist v8 score`.
- One read API: `branch_set_density(conn, branch_set_id)`.
- #000037 probe wires through the new function once it lands.

Not opened as its own ticket because operator pressure for it
hasn't surfaced naturally — gates on either #000012 Phase 1b
landing OR #000030 algebra/calc kernel expansion producing
competing-kernel branches an operator wants to compare. Captured
here so a future shift doesn't re-discover the gap.

Hygiene
=======
- make test → 1623 passed, 45 skipped
- make chain-check-shards → 0 across all 7 shards
- fox's in-flight #000037 ticket modifications left untouched
2026-05-10 07:46:35 -04:00
245fb6ead3
PLFA + SF-LF + PM Vol 1 ingest: 62 -> 68/92 (74%) — pillar IX nearly closed
Three new substrates targeting the lambda-calculus gap (pillar IX
was 5/14 stuck) and the type-theoretic Russell's Paradox Resolution
record (last pillar II straggler):

  PLFA - Programming Language Foundations in Agda
    (Wadler/Kokke/Siek, Edinburgh CS, CC-BY-4.0)
    plfa.github.io BFS depth=2 max=60 -> 58 docs / 413 chunks
    Untyped + simply-typed lambda calculus, Confluence/Church-Rosser,
    progress + preservation, de Bruijn, beta/alpha/eta reduction.

  Software Foundations Vol 1 - Logical Foundations
    (Pierce et al., Penn CIS, MIT-licensed)
    softwarefoundations.cis.upenn.edu/lf-current/ BFS depth=2 max=40
    -> 33 docs / 367 chunks. Coq induction proofs, lambda calculus.

  Whitehead-Russell Principia Mathematica Vol 1
    (1910 Cambridge, PD by age, PG #78050 single-page HTML)
    -> 1 doc / 231 chunks. Preface + intro + chs I-III only;
    formal type theory body (*24 onwards) not transcribed.

Plus 4 new citation-alias rows per #000041 (decision_by="fox 2026-05-10"):
  Barendregt -> PLFA (+5 pillar IX)
  Barendregt -> Software Foundations LF (+1 pillar IX, supplementary)
  Jech       -> PM Vol 1 (cascade miss; 0 lift)
  Landau     -> Software Foundations LF (cascade miss; 0 lift)

Per-pillar:
  IX:  5/14 -> 11/14 (+6 — beta/alpha/eta + Church-Rosser + extensionality + fixed-point)
  Others stable.

Title-haystack hack reverted: initial backfill appended ", Barendregt
substrate" to PLFA + SF docs, which would have let the resolver match
Barendregt citations directly via the haystack (mis-labeling chains
as DIRECT instead of via_alias). Now uses clean citation-alias
substitution; audit trail preserves substitution.

Cumulative day-of-2026-05-10: 18 -> 68 / 92 (+50 records, +54pp).
24 records still stuck. Top blockers:
  - Pillar I formal proof axioms (3) — Hilbert-Ackermann needed
  - Pillar III symbolic-axiom cascade misses (6) — Peano/Dedekind/SF
    have content; FTS5 token cascade doesn't surface
  - Pillar V Kolmogorov axioms (4) — Laplace narrative not enough,
    Kolmogorov 1933 URAA-blocked until 2058
  - Pillar VII advanced identities (5) — Bogart skews intro
  - Pillar IX (3) — Turing/Bohm-Jacopini/Orbit-Stabilizer cascade misses
  - Pillar VI (2) — Newton 1729 vocab mismatch
  - Pillar II Russell's Paradox Resolution (1) — PM Vol 1 *24+ not transcribed
2026-05-10 07:45:40 -04:00
fb886f3599
3 more textbooks (Russell PoM + Laplace + Dedekind): 54 -> 62/92 (67%)
Three PD / CC-BY-SA-4.0 primary substrates ingested under fox
"keep filling maths in" directive:

  Russell - Principles of Mathematics 1903 (Klement HTML, 1MB
    single page, 546 chunks). CC-BY-SA-4.0 typesetting + PD content.
    Pillar I/II — class theory, relations, Russell's Paradox
    derivation that IMP 1919 omits.

  Laplace - A Philosophical Essay on Probabilities (PG #58881 HTML,
    Truscott-Emory 1902 English, 111 chunks). PD by age. Pillar V
    primary; pre-Kolmogorov foundational treatise.

  Dedekind - Essays on the Theory of Numbers (PG #21016 TeX, Beman
    1901 English, 57 chunks via existing textbook_tex pipeline).
    PD by age. Pillar III primary alongside Peano; Dedekind cuts
    + chains-and-induction definition of natural numbers.

Plus 5 new citation-alias rows per #000041 (decision_by="fox 2026-05-10"):
  Mendelson  -> Russell PoM (+2 pillar I)
  Enderton   -> Russell PoM (+1 pillar I)
  Jech       -> Russell PoM (+4 pillar II — Russell's Paradox)
  Landau     -> Dedekind     (cascade miss; 0 lift)
  Kolmogorov -> Laplace      (+1 pillar V)

Per-pillar:
  I:    7/13 -> 10/13 (+3)
  II:   5/10 ->  9/10 (+4 — pillar II nearly clear)
  III:  7/13 stable
  IV:  18/18 stable
  V:    0/5  ->  1/5  (+1)
  VI:   3/5  stable
  VII:  9/14 stable
  IX:   5/14 stable
  Total: 62/92 (67%)

Cumulative day-of-2026-05-10 lift: 18 -> 62 (+44 records, +47pp absolute).

30 records still stuck. Top-yield next candidates:
- Hilbert-Ackermann 1928 for pillar I formal proof axioms
- Whitehead-Russell PM Vol I for pillar II type-theoretic Russell's Paradox resolution
- Software Foundations / Wadler Programming Language Foundations
  in Agda (both CC-BY-4.0) for pillar IX lambda calculus
- Pillar III cascade tuning (Peano + Dedekind shards have content
  but FTS5 token cascade misses symbolic axioms)
2026-05-10 07:31:40 -04:00
c422216428
#000037 Phase 0: §12 trigger probe + Phase 1 test scaffolding
Phase 0 of ticket #000037 (Prometheus-Σ recursive falsification
controller) is doc-only and gates Phase 1 on §12 measured-pressure
triggers. This commit lands the empirical-evidence harness fox needs
for the go/no-go decision, plus the §16.2 test scaffolding so the
contract is discoverable from the test runner today.

bench/prometheus_sigma_trigger_probe.py
=======================================

Read-only walk of audit_events + capital_ledger across shards.
Reports each §12 trigger:

- Trigger 1 (branch density, ≥4 branches/checkpoint): looks for a
  fork_score branch-set table; reports "no data — single-validator
  ForkScore Phase 1a" when absent. Trigger structurally cannot fire
  until #000012 multi-branch persistence lands.
- Trigger 2 (divergence variance, N≥30 + ratio>0.5 OR abs>0.10):
  aggregates providence_canonical_witness audit-event bodies,
  maps each agreement_label per #000028 §1.2 to a binary
  LLM-divergence score, computes mean/stddev/ratio. Defensive on
  the max(mean,ε) guard from §12 itself.
- Trigger 3 (witness cost share > 0.30): aggregates capital_ledger
  rows; uses `material` (kWh proxy) as the canonical compute axis;
  surfaces both `material` and `financial` so fox can pick a
  different form if needed. Tags the report with the caveat that
  the current ledger reflects ad-hoc activity, not a controlled
  #000026 sweep.
- Trigger 4 (operator mission need): n/a — operator decision.

Pure measurement, no LLM, no schema change, no mutation. Output is
a markdown report at $(PROMETHEUS_PROBE_OUT) (default
bench/results/prometheus-sigma-triggers-<utc-date>.md).

Wired via `make prometheus-trigger-probe`.

bench/results/prometheus-sigma-triggers-2026-05-10.md
=====================================================

First captured baseline. Verdict on current shards:

  Trigger 1: NO  (no fork_score branch-set table; #000012 Phase 1a
                  is single-validator)
  Trigger 2: NO  (16 samples; N_min=30. But mean=0.625, σ=0.5,
                  ratio=0.8 — both ratio AND abs floors would fire
                  if N reaches 30. Signal is there; just needs more
                  samples.)
  Trigger 3: NO  (witness/total material = 0.005, well under 0.30
                  threshold. Caveated: ledger is ad-hoc, not a
                  controlled #000026 sweep.)
  Trigger 4: n/a (operator-stated)

Empirical answer: no §12 measured-pressure trigger has fired yet.
Phase 1 of #000037 remains paper-only unless fox invokes Trigger 4.

tests/test_prometheus_sigma.py
==============================

17 skip-stubs pinning the §16.2 acceptance contract. Each test:

- Collects today via `pytest --collect-only` so the test surface is
  discoverable.
- Skips with reason "Phase 1 not landed; controller module
  arborist/v9/prometheus.py absent" until that import succeeds.
- Carries a one-sentence intent line tying it back to a numbered
  ticket section (§5 / §6 / §7 / §10 / §13 / §14 / §16.1 / §4.4).

When Phase 1 lands, the implementer adds the controller module
under arborist/v9/prometheus.py per §13; CONTROLLER_AVAILABLE
becomes True; each test gets its body filled in. The names, intents,
and skip-reason strings are the durable contract.

Hygiene
=======

- make test → 1623 passed, 45 skipped (was 28; +17 new skips).
- make chain-check-shards → 0 breaks across all 7 shards.
- No code touched outside the new probe + scaffolding files +
  Makefile target wiring. fox's in-flight #000037 ticket
  modifications left untouched.
2026-05-10 07:24:59 -04:00
f6951f4472
medium-conf aliases + Peano ingest + title backfill: 35 -> 54/92 (59%)
Three orthogonal lifts under fox 2026-05-10 "all of the above"
directive:

(1) 7 medium-confidence citation aliases per #000041:
    Mendelson  -> Russell IMP + De Morgan FNL + Boole Laws of Thought
    Enderton   -> Russell IMP + De Morgan FNL
    Jech       -> Cantor 1915 Contributions
    Landau     -> Russell IMP
    Each row carries partial-coverage caveat in decision_rationale.

(2) Peano Arithmetices Principia 1889 ingested via existing
    textbook_tex pipeline. Source: mdnahas/Peano_Book GitHub
    repo (CC-BY-SA-4.0, Verheyen+Nahas English+Latin LaTeX).
    paracol multi-column macros leak some residue but substantive
    text extracts (39 chunks, 35 hits on "peano", 38 on
    "arithmetic"). Make target textbook-peano. Manifest entry
    peano-arithmetices-principia-1889. Plus 3 substitute-citation
    aliases:
      Landau -> Peano (lifts 2 pillar III records)
      Goedel -> Peano (2 variant strings)

(3) Title-from-author backfill on Cantor / Russell IMP / Bogart /
    Judson / Peano shards. Empirical defect: HTML/textbook_tex
    sources took titles from <title> tags or URLs which on
    Wikisource + PG do NOT include author surname, so the
    resolver's _shard_matches_citation heuristic (requires
    cited-author surname in title haystack) failed silently for
    all alias-resolved chains where the substitute author wasn't
    self-evident in the shard content. Surgical SQL UPDATE on
    documents.title fixed it. Single biggest lift in this turn:
    +13 records.

Per-pillar:
  I:    4/13 -> 7/13  (+3, Russell IMP / Boole / De Morgan)
  II:   0/10 -> 5/10  (+5, Cantor)
  III:  0/13 -> 7/13  (+7, Peano + Russell IMP)
  IV:  18/18 stable
  V:    0/5  stable (Kolmogorov URAA-blocked)
  VI:   3/5  stable
  VII:  9/14 stable
  IX:   5/14 stable
  Total: 54/92 (59%)

Title backfill is a one-off SQL; the proper long-term fix is in
the source ingest pipelines (HTML / textbook_tex should pull
author from manifest's `author` field at ingest time and prepend
to document.title). Tracked under #000031 Phase 1 follow-up.
2026-05-10 07:14:44 -04:00
e84f453e49
docs/tickets: stale-map sweep — 3 deferred markers refreshed
Pattern from #000028 §8.2/§8.3 (commit 6d20aeb): tickets carry
"deferred" markers in follow-up sections written from pre-
implementation design notes; code lands but the markers don't get
refreshed; future readers waste a session re-implementing what's
already there. Walked all 19 closed tickets carrying deferred-class
mentions and cross-checked each one against current code.

Three confirmed stale markers refreshed:

#000010 §12.2 — "First pass does NOT bind into run_dag_root —
deferred to ticket #000009 (Phase 5)". The metacog binding DID
land. Commit 111dda6 ("qa(#000009): §8 corrections — reject-path
DAG + nested CTI clauses", 2026-05-04) extended
arborist.qa.dag.build_preflight_node_payload with a question_state
clause carrying the metacog to_dict() payload. Today every cache
write threads question_state.to_dict() into the preflight node
(arborist/qa/query.py:3296-3297). Refreshed the §12.2 paragraph
to point at that commit + call site.

#000021 Phase 1b "(deferred)" — items "Synthesis, Syllogism,
Semiotics under 5S; Triangulate, Timing, Transitivity, Truth under
5T". Phase 1b was scope-split into per-sub-battery tickets:
#000023 (5S) and #000024 (5T), both closed 2026-05-08. The Closure
section in this ticket already reflects the resulting fixture
totals (108 5S + 154 5T) but the Phase 1b sub-section still said
"deferred". Refreshed to point at #000023 / #000024.

#000040 §6 — "Cascade landed 2026-05-09 (commit TBD)". TBD was a
placeholder while the commit was in flight; landed as b9e5bbd
("ticket #000040 Phase 5: phrase + content-token resolver
cascade"). Replaced TBD with the real hash.

Items confirmed genuinely deferred (no refresh needed) — recorded
here so the next sweep doesn't re-walk them: #000010 reference-
frame plumbing / SOFT_PREFLIGHT_HINT / metacog-trigger bench;
#000011 §13 bench plan; #000014 selfmodel_binding cache-key
folding (only docstring mentions; no actual gating wiring) /
selfmodel diff CLI / cross-shard reconciliation; #000015 / #000017
out-of-scope items; #000019 auto-canonicalizer / cross-language /
source-adapter methodology; #000020 stewardship-halt / conversion
tables / real-time instrumentation; #000023 multimodal execution.
Pure docs change; no code touched.
2026-05-10 07:00:56 -04:00
19506d8386
citation-aliases batch: 18 -> 35 / 92 records resolve (38%)
Three high-confidence alias decisions per fox 2026-05-10 + 14
full-string aliases for compound pillar-VII citations + a deeper
Newton recrawl.

Lift breakdown:
  pillar IV (Hilbert):           18/18 unchanged
  pillar VI (Goldstein/Newton):   0/5  ->  3/5  (+3)
  pillar VII (Stanley/Bogart):    0/14 ->  9/14 (+9)
  pillar IX (Dummit-Foote/Judson):0/14 ->  5/14 (+5)

Citation aliases live in ~/.arborist/shards/000.db (audit table per
#000041). 14 pillar-VII rows are full-string matches against the
compound source_ref strings (resolver looks up by exact source_ref;
parsed sub-citations are not yet alias-keyed individually).

Newton shard rebuilt: original `crawl_en_wikisource_org_newton.db`
followed Wikisource sidebar instead of book content (60 docs / 289
chunks of mostly nav cruft). Manifest now pins (1729) edition root
+ explicit subpage urls (Axioms_or_Laws_of_Motion, Definitions,
Rules_of_Reasoning_in_Philosophy); recrawl produced 120 docs / 779
chunks of actual Principia text in textbook_newton-principia-motte.db.

5 records stuck despite alias registered (FTS5 cascade misses):
Newton Third Law + Conservation of Momentum (modern vocabulary
absent from 1729 prose), 4 advanced pillar-VII identities (Hockey-
Stick, Vandermonde, Catalan, Stars-and-Bars — Bogart skews intro-
level), Orbit-Stabilizer (Judson covers it but cascade doesn't
surface). Tractable one-by-one; deferred.

Pillars I/II/III/V/lambda subset of IX still 0/X — those need
medium-confidence alias decisions (Mendelson/Enderton -> Russell IMP,
Jech -> Cantor) or Phase 4 textbook acquisitions (Landau, Goedel,
Kolmogorov, Church) under #000038.
2026-05-10 06:58:27 -04:00
6d20aeb910
ticket #000028: §8.1 terminology line + §8.2/§8.3 status refresh
§8.1 — Witness-vs-modality terminology clarification (pure docs).

The ticket title and §1 throughout use "modality" — operationally
meaning kernel / cache / LLM. The 2026-05-09 review (response_ticket-
000027-canonical-projections-in-providence-cache.txt) flagged that a
future reader looking for cross-carrier work (text↔image, audio,
world-state) might land here by mistake, since "modality" in that
sense means a different thing.

Added a one-line note near §1 distinguishing *witness channel* (an
independent epistemic source) from *carrier* (text / image / audio /
world state), and pointing forward to a later ticket for cross-
carrier extensions once π* libraries support non-text carriers.

§8.2 + §8.3 — status refresh from "deferred" to "landed in 708aa45".

Both follow-ups already shipped in commit 708aa45 ("fan-out: warrant
ladder wiring · witness follow-ups · 5F Phase 1d", 2026-05-09 12:42
EDT) — pre-dating the e19aed8 close commit. The ticket file's §8.2
and §8.3 sections still carried the "deferred" labels because they
were written from the pre-implementation design notes; refreshing
both to point at the actual implementation in
arborist/qa/query.py (lines 2140-2155 for sample-rate gating;
2237-2285 for the capital_ledger sidecar) and the corresponding
test_witness.py coverage. Map-vs-territory hygiene: stale ticket
markers are how future readers waste a session re-implementing
something that's already there.

No code change in this commit. 33/33 tests in test_witness.py
continue to pass, all 7 shards chain-check clean.
2026-05-10 06:52:40 -04:00
6ba833878d
bench: progressive-AND fixture + 2026-05-09 A/B baseline report
The bench-qa-smoke A/B against commit 416f956 surfaced a methodology
gap: the smoke fixture is structurally insensitive to retrieval-side
changes — every smoke query succeeds at full-AND chain 0 on every
shard, so cache_keys match byte-for-byte BEFORE/AFTER and any
STRICT-rate variance is pure LLM dice. Discovered when 5pp signal
floor at n=3 produced ±20pp swings with identical cache_keys.

This commit pins a fixture that ACTUALLY exercises the new code path:

- 5 PROGRESSIVE queries (full-AND fails on at least one shard;
  _progressive_and_token_chains drops shortest-tokens-first). Includes
  the canonical Gundremmingen case from commit 2b9d1f0.
- 2 DF_FILTER queries (every AND chain fails on at least one shard;
  search lands in OR-mode where _filter_or_pool_by_df trims
  high-DF tokens).
- 2 CONTROLs (full-AND succeeds on every shard; cache_keys must
  remain identical BEFORE/AFTER for any retrieval-side change).

Which-chain-fires-on-which-shard was empirically verified at HEAD
against ~/.arborist/shards (4 wiki shards, 1.5M chunks each). Header
documents the chain that wins per query; re-probe if shards drift.

Baseline A/B (commit 416f956 ON vs OFF, n=3, --burn between samples,
fixture run via make bench-qa-progressive-and):

  category       cache_key parity    STRICT-rate delta    median latency delta
  PROGRESSIVE    9/15 drifted        +0.0pp (11/45 both)   -3.6s
  DF_FILTER      3/6 drifted         +5.6pp (10/18 → 11/18) -3.9s
  CONTROL        0/6 drifted         +0.0pp (15/18 both)    +0.0s

The CONTROL +0.0s latency delta is the load-bearing diagnostic —
when retrieval is byte-identical the search-side change cannot
affect total wall, and it doesn't. PROGRESSIVE / DF_FILTER cache_key
drift is the change actively redirecting retrieval, with the
expected latency win and no STRICT regression.

Future retrieval-side work (#000039 sqlite-vec backend, synonym
expansion changes, embedding rerank, hybrid scoring) should bench
against this fixture in addition to the full bench-qa scoreboard.

Hygiene:
- make test → 1623 passed, 28 skipped
- make chain-check-shards → 0 breaks across all 7 shards
2026-05-10 06:35:18 -04:00
a5d666eba2
textbook ingest: 4 base-knowledge additions for pillars I/II/III/IX
Adds Cantor (Jourdain 1915 transl., PD), De Morgan First Notions of
Logic (PG #67017, PD), Russell Introduction to Mathematical Philosophy
(PG #41654, PD), and Judson Abstract Algebra Theory and Applications
(GFDL-1.3) to the textbook manifest, plus per-book make targets +
a `textbooks-base-knowledge` bulk target. Idempotent at DB layer.

These four primaries cover the proprietary citations across pillars
I/II/III/IX (Mendelson, Enderton, Jech, Barendregt, Dummit-Foote)
that dominate the 74 unresolved claim-pack records. They land as
honest "no match" under the existing resolver `_shard_matches_citation`
heuristic (cited-author surname required) — full lift gates on
fox citation-alias decisions per #000041.

Total ingest delta: 43 docs / 295 chunks across four crawl shards.
Bench journal under bench/results/textbook-base-knowledge-upgrade-2026-05-09.md
records per-book license rationale, projected lift table, and the
remaining #000038 acquisition gaps (Hilbert-Ackermann, Landau,
Gödel, Kolmogorov, Church) for which no clean PD HTML edition was
located in this session.
2026-05-09 20:38:32 -04:00
cc1a597708
ticket #000042: 4 geometry aliases resolve all 18 Hilbert pillar IV records
Smoke-test alias rationale was published with #000042, but two of the
three trailing records ("non triviality", "side-angle-side") needed
their own per-concept aliases since Hilbert 1902's vocabulary differs
in more than one place. Map of registered aliases (geometry domain):

  incidence                    -> connection      (4 records lifted)
  euclidean parallel postulate -> axiom of parallels (1)
  non triviality               -> space axiom     (1)
  side angle side              -> included angle  (1)

Hilbert pillar IV is now the first complete warrant-chain vertical:
18/18 records bind to a primary-source surface chunk via Merkle
inclusion proof. 11 direct + 7 via-alias derivations rows. Bench
journal under bench/results/hilbert-pillar-iv-fully-resolved-2026-05-09.md
records reproducibility steps + per-alias signal data so a future
shift can extend the same pattern to Boole 1854, Newton 1729 Motte,
and Aristotle's traditional translations once #000038 lands those
surfaces.

Cluster-wide remains 18/92 (20%); the other 74 records cite textbooks
not yet ingested. Phase 4 content acquisition (#000038) gates next
lift.
2026-05-09 20:18:58 -04:00
d3c40c95d2
ticket #000041 + #000042: alias mechanism + 4 more Hilbert chains landed
Implements both alias mechanisms (citation-aliases #000041,
term-aliases #000042) as one cohesive layer. Same audit
discipline; same opt-in via --use-aliases on warrant-resolve;
same distinct process_id "warrant-resolver-v1+alias" on alias-
resolved derivations rows.

What landed
===========
arborist/store.py — two new tables under SCHEMA_SQL:
  citation_aliases — substitute textbook for proprietary cite
  term_aliases     — bridge vocabulary mismatches (incidence ↔
                     connection in geometry, etc.)
Both with NOT NULL audit fields (decision_at + decision_by
+ optional decision_rationale); both with PK constraints
ensuring idempotent re-add.

arborist/qa/aliases.py — helper module:
  add_citation_alias / list / lookup / remove
  add_term_alias / list / lookup (bidirectional) / remove
  expand_query_with_term_aliases — OR-rewrites FTS5 tokens
                                   while preserving phrase syntax
  domain_for_pillar — Roman numeral → domain string

arborist/qa/warrant_resolver.py — two-pass cascade:
  Pass 1: unaliased queries (matches carry via_alias=False)
  Pass 2: alias-expanded queries (only when pass 1 missed;
          matches carry via_alias=True)
  ResolutionMatch grew a via_alias field; warrant_resolve
  uses it to pick the right process_id per derivation row.
  iter_claim_pack_records now yields a 6-tuple including the
  pillar (parsed from doc URI) so domain lookup works.

arborist/cli.py — alias subcommand group:
  arborist alias citation add ORIGINAL --substitute SUB --by FOX [...]
  arborist alias citation list / remove
  arborist alias term add TERM ALT --domain D --by FOX [...]
  arborist alias term list / remove
  warrant-resolve --use-aliases flag
  sweep --target warrants --use-aliases flag
All audit fields fail-closed at the API surface (refuses on
empty --by; ValueError raised at the helper level).

End-to-end smoke test
=====================
Registered the Hilbert smoke-test alias:
  arborist alias term add incidence connection \
      --domain geometry \
      --by "blackops 2026-05-09 (smoke test)" \
      --rationale "Hilbert 1902 Townsend uses 'connection' for
                   what modern texts call 'incidence'"

Re-ran warrant-resolve --use-aliases --write:

  records_total: 92
  records_resolved: 15  (was 11 without aliases)
  derivations_written: 15

Breakdown by process_id:
  warrant-resolver-v1:        11  (original-citation matches)
  warrant-resolver-v1+alias:   4  (alias-resolved Hilbert axioms)

The 4 alias-resolved records are exactly the Hilbert "Incidence"
axioms blocked by terminology mismatch in #000040 §6:
  Axiom of Line Incidence
  Axiom of Plane Incidence
  Axiom of Point-Line Incidence
  Axiom of Point-Plane Incidence

All four bound to chunk 56 in the Hilbert TeX surface — the
chapter discussing "axioms of connection" (Hilbert's original
1902 vocabulary). Audit trail correctly distinguishes
substituted chains from original ones.

Tests: 18 new in test_aliases.py covering add / list / lookup
/ remove / domain isolation / lowercase normalization /
bidirectional lookup / audit-discipline raises / query
expansion (basic + phrase-preserving + no-match passthrough +
unreachable-DB fallback). Full suite: 1623 passed / 28
skipped.

Tickets #000041 + #000042 closed. Operators can now add more
aliases via the CLI as fox makes decisions per #000038. The
alias mechanism is fail-closed by default — existing
warrant-resolve runs without --use-aliases continue to produce
the original 11/92 chains; --use-aliases opt-in adds the
substituted chains alongside without polluting the unsubsituted
audit trail.
2026-05-09 20:05:28 -04:00
44b38c55da
ticket #000042 + arborist sweep CLI (Target B warrant-resolver fragment)
Two related changes:

#000042 — Term-aliases table (vocabulary-mismatch bridge)
=========================================================
Sibling design to #000041 citation-aliases. Maps a (term,
domain) pair to an alternate term used in older / foreign /
pre-modern translations of the same concept. Triggered by the
Hilbert "incidence" vs "connection" gap surfaced in #000040
§6 — claim-pack records use modern post-1950s names, the 1902
Townsend Hilbert translation uses the original "Verknüpfung"
/ "connection".

Resolver wiring: each FTS5-query token gets OR-expanded with
its registered aliases when --use-aliases is set. So '"line
incidence"' becomes '"line incidence" OR "line connection"'
once fox approves the (incidence, connection, geometry) alias.

Decision audit: each row carries decision_at + decision_by +
decision_rationale. Same audit discipline as #000041; same
opt-in via --use-aliases; same distinct process_id
("warrant-resolver-v1+alias") on alias-resolved derivations
rows.

A single decision unlocks 7 stuck Hilbert pillar IV records:

  arborist alias term add incidence connection \\
      --domain geometry --by "fox YYYY-MM-DD" \\
      --rationale "Hilbert 1902 Townsend uses 'connection' for
                   what modern texts call 'incidence'"

Implementation deferred until that decision triggers it.

`arborist sweep` CLI — Target B warrant-resolver fragment
=========================================================
Implements the schema-no-change increment of #000037 §3.1
Target B (documents that bypassed meta-cognition at ingest
time).

  arborist sweep --shards-dir X --target warrants [--write]

`--target warrants` walks every claim-pack record and
re-runs warrant_resolve. Same code path as
`arborist warrant-resolve` but framed as the unconscious
sweep — operators can run on a cron / systemd timer; the
target name reserves namespace for the full bicameral sweep
landing later (canonical-projection probe, freshness probe,
document-content witness fan-out).

`--target all` reports "deferred" with an honest message:
the full sweep needs #000037 §12 phase trigger +
documents.last_swept_at schema migration.

Idempotent: re-running on the same shards is a no-op at the
DB layer (PK collision on (core_root, src_root, process_id)
in the existing derivations table). Operators can run the
sweep on a recurring schedule without row proliferation —
exactly the property #000037 §3.1 needs from the unconscious
sweep.

Test suite stays at 1605 passed / 28 skipped — pure CLI +
new ticket; no source-code changes outside cli.py.
2026-05-09 19:27:24 -04:00
565f763967
ticket #000039: sqlite-vec optional backend (parallel-shift orphan landed)
Parallel-shift session drafted #000039 earlier today and updated
TICKETS.md with the index row, but the ticket file itself sat
untracked in working tree (same situation #000037 had until that
ticket landed in commit 178cc42).

Committing the file as-drafted by the original author so the
design log entry is intact. No content changes from this
session; the file is exactly what the parallel shift produced.

Per the design log convention in TICKETS.md ("Do not delete
tickets; they are the design log") — every opened ticket file
ships with its index row.
2026-05-09 19:19:44 -04:00
178cc422e2
ticket #000037 §3.1: unconscious sweep also drains ingest backlog
Original ticket spec (drafted earlier today by a parallel-shift
session, untracked in working tree until this commit) covers the
unconscious sweep walking providence_cache rows during ingest
lulls. Fox flagged a second backlog the controller has to drain:
ingested DOCUMENTS that bypassed meta-cognition at ingest time.

Today's ingest pipeline is intentionally fast: fetch →
canonicalize → chunk → Merkle commit → audit row → done. No
witness fan-out, no canonical-projection cross-check, no warrant
resolution. That speed is the right trade-off for getting bytes
into the queryable Merkle + FTS5 tree, but it leaves a
meta-cognition gap: the substrate has content it never *probed*.

New §3.1 spells out two sweep targets, both processed during
ingest lulls:

Target A — providence_cache rows older than τ_qa
  Re-runs multi-modality witness fan-out (#000028) on cached
  Q&A answers. Catches drift from Hermes updates / kernel
  bumps / mesh-delivered new evidence. Default τ_qa: 7 days.

Target B — documents rows ingested without meta-cognition
  Walks `documents` where last_swept_at is NULL or older than
  τ_doc, runs cross-checks per document content:
   - Canonical-projection probe (math/logic statements in body
     vs. matching π* canonical answer)
   - Warrant resolver re-run (newly-ingested textbook can
     resolve previously-unresolved claim-pack records)
   - Source-URL freshness probe (HEAD-only via existing
     recrawl-check; mark stale/gone)
   - Witness fan-out on document content (kernel+LLM+cache as
     if doc were a Q&A answer citing itself)

State tracking: new column documents.last_swept_at, schema
migration deferred to §12 phase trigger so it doesn't bump the
cache_key invariant prematurely.

Why this matters: without target B, the substrate's "I have
this content in my Merkle tree" claim is honest at the byte
level but silent on whether the content was ever tested against
kernel ground truth. Sleep is when you do the tests you
deferred to keep the day moving.
2026-05-09 18:34:09 -04:00
416f956734
search/fts5: progressive-AND fallback + DF filter at OR-pool
The fan-out commit (2b9d1f0) exposed a 13.5s shard-002 fts5_body call
on the Gundremmingen query and hypothesised the synonym OR-pool was
blowing the FTS5 candidate set. Profiling falsified that hypothesis:
synonym_expand returned no synonyms, the OR pool was just the three
query tokens, and the bottleneck was a single high-DF QUERY token
("located": 286,160 matches on a 1.5M-chunk wiki shard) carried into
OR-mode after AND-mode found zero co-occurrences. BM25 ranked all
~290k matches just to pick the top-32.

Two layered fixes:

A. Progressive-AND fallback. When AND returns zero, drop the shortest
   token (input order breaks ties) and retry AND. Repeat until hits or
   one token left. Only after every chain returns zero do we fall to
   OR-mode. On the Gundremmingen case, dropping "located" leaves
   "Gundremmingen AND Bavaria" which intersects to 3 docs in 11ms
   instead of the 290k-match OR-mode wall.

B. Document-frequency filter at OR-fallback time. ``COUNT(MATCH "tok")``
   per OR-pool token; drop any whose corpus DF exceeds
   ``_OR_FALLBACK_MAX_TOKEN_DF`` (default 50,000). ~15ms warm per
   probe. Only fires on the rare path where every progressive-AND
   chain still returned zero. Backstops A for queries where the
   answer genuinely requires OR (synonym-anchored retrieval, queries
   for content that uses different vocabulary than the question) but
   one of the OR clauses is a high-DF stopword-adjacent verb.

Both are deletion-first per the five-step algorithm: A deletes the
"jump straight to OR" path, B deletes high-DF tokens that contribute
~zero IDF anyway. No magic constants for A; B has one tunable knob
(threshold).

Bench (cold-cache, n=3, serial workers=1, query "where is
Gundremmingen located? where is Bavaria?"):

  metric                    BEFORE         AFTER (A+B)    delta
  total search wall         57.20s ± 0.22  1.67s ± 0.13   -97% / 34x
  shard 002 fts5_body cold  28.07s         0.05s          ~560x
  shard 002 fts5_body hits  32             3              -29 (the
                                                          dropped
                                                          were
                                                          "located"-
                                                          only noise)

Top-K=8 chosen sources unchanged before/after — the dropped fts5_body
candidates were filtered by the title-relevance step downstream
anyway.

Tests (tests/test_search_fts5.py, 11 cases):
- Helper: 5 cases on _progressive_and_token_chains (single-token,
  empty, shortest-first, strict length sort, always-keeps-one).
- Search behaviour: 4 cases (progressive-AND drops high-DF token;
  full-AND succeeds without progression; OR fallback when no chain
  hits; empty result when corpus has neither token nor synonym).
- DF filter: 2 cases (drops high-DF token, keeps input when all
  candidates would otherwise be dropped).

Verification:
- make test → 1605 passed, 28 skipped (was 1597 pre-change)
- make chain-check-shards → 0 breaks across all 7 shards
- arborist query "where is Gundremmingen located? where is Bavaria?"
  returns the same top-8 sources before/after
2026-05-09 18:31:24 -04:00
2487b1c05c
docs/tickets: open #000041 — citation-aliases table
Design ticket for the alias mechanism proposed in #000038
§3.2 option (b). When a cited textbook is proprietary or
unavailable, fox decides on a PD substitute (e.g.,
Hilbert-Ackermann 1928 instead of Mendelson 1997), and the
warrant resolver looks up the aliased citation alongside the
original.

Schema (`arborist citation_aliases`) carries
decision_at + decision_by + decision_rationale per row so
the substitution is auditable. Opt-in via `--use-aliases` on
warrant-resolve; alias-resolved chains carry distinct
process_id ("warrant-resolver-v1+alias") so audit can tell
substituted chains from original ones.

Recommend parking until first PD-substitute decision lands
in #000038. Today the only candidate is Hilbert-Ackermann
1928 → Mendelson + Enderton (~13 records), which is
substantial. Goldstein → Newton's Principia for ~5 pillar VI
records is also viable.

Sibling design to #000042 term-aliases (the other vocabulary-
mismatch follow-up surfaced by the Hilbert "incidence" vs
"connection" gap from #000040 §6).

Implementation deferred until trigger fires.
2026-05-09 18:27:10 -04:00
b9e5bbdb13
ticket #000040 Phase 5: phrase + content-token resolver cascade
Implements the layered cascade strategy from #000040 §3.1
(originally drafted as #000039 — renumbered after collision
with parallel-shift's sqlite-vec ticket).

What landed
===========
arborist/qa/warrant_resolver.py:

- _phrase_for_axiom(theorem_name) — strips leading
  categorical prefix ("Axiom of " / "Theorem " / "Principle ")
  and trailing parenthetical, returns FTS5 phrase syntax
  ('"line incidence"', '"plane incidence"', '"side angle
  side"', etc.) when the theorem name has 2+ tokens.
- _content_tokens(chunk_content, max_n=8) — extract
  discriminating tokens from a claim-pack chunk's body. Drops
  stopwords / generic theorem terms / common-English (small
  hand-curated set). Requires count >= 2 to ditch typo /
  LaTeX residue singletons. Sorts by length DESC then
  first-position ASC.
- _build_record_query_cascade(c, theorem_name, content) —
  returns ordered list of FTS5 queries to try:
    1. Phrase from title
    2. Content-tokens AND-joined
    3. Existing discriminating-tokens AND-join (legacy)
    4. Existing OR-fallback (legacy)
- resolve_chunks gains a `record_content` parameter; tries
  each cascade query in order, first hit wins.
- iter_claim_pack_records yields a 5-tuple including content
  so callers can thread it through.

Tests: 6 new unit tests for the cascade helpers (phrase
extraction, parenthetical stripping, single-token fallback,
content-token filtering, count-2 minimum, cascade ordering).
20 total in test_warrant_resolver.py. Full suite: 1603
passed / 28 skipped.

End-to-end honest result
========================
Re-running warrant-resolve on the existing shard cluster:
records_total=92, records_resolved=11 (unchanged from Phase 4).

The cascade is correct; the lift didn't materialize for
Hilbert pillar IV's 7 missing records because of TERMINOLOGY
MISMATCH, not query strategy:

- claim-pack records (g4 2025) use modern post-1950s names:
  "Axiom of Line Incidence", "Group I: Axioms of Incidence".
- Hilbert's 1902 Townsend translation uses the original
  "Verknüpfung" / "axioms of connection".
- Empirically: the literal token "incidence" appears ZERO
  times in the ingested Hilbert TeX surface; "connection"
  is the relevant synonym.

No matter how clever the query, you can't find a word that
isn't there. The cascade is preserved for any future textbook
where cited vocabulary matches textbook prose (modern
Stanley / Brualdi / Knuth, etc.).

Next-link follow-up: file #000042 term-aliases table
(("incidence", "geometry") → ("connection", "geometry")).
Sibling design to the citation-alias proposal at #000041.

Renumbering note: the Phase 5 ticket file was renumbered
000039 → 000040 mid-session because parallel-shift took
000039 for sqlite-vec at nearly the same time. Internal
references in the file follow the post-rename numbering
(#000041 = citation-alias, #000042 = term-alias).
2026-05-09 18:25:30 -04:00
7f9bf606dc
docs/tickets: open #000038 — Phase 4 content acquisition
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.
2026-05-09 18:06:40 -04:00
8ba123dc17
bench/results: warrant-chain render tail measurement (2026-05-09)
Six-question Q&A sweep against the augmented shard cluster
post-#000031 Phase 3 commit (69e0a95). Looking for the new
`· warrant: N proven` tail surfaced by
_render_warrant_chain_tail when an answer's cited sources
include a claim-pack record with a warrant-resolver-v1
derivations row.

Result: 1 of 6 questions lit up the warrant tail.

  Pasch's axiom              → STRICT · via quote · warrant: 1 proven  ✓
  Hilbert geometry axioms    → STRICT · via quote                       ✗
  axiom of betweenness       → HYBRID · via paraphrase                  ✗
  Bayes theorem              → STRICT · via quote                       ✗
  modus tollens              → UNGROUNDED · via quote                   ✗
  binomial coefficient id.   → HYBRID · via paraphrase                  ✗

1/6 matches the data substrate: 11 of 92 records have warrant
chains, all pillar-IV Hilbert axioms. The 5 unsigned cases are
honest:

- Hilbert / betweenness queries cited Wikipedia + crawled
  textbook surfaces, NOT the claim-pack records — no claim-pack
  record cited → no warrant chain to surface.
- Bayes theorem: even if cited, Kolmogorov isn't surface-
  ingested → would stay at ANCHOR-WARRANTED ceiling.
- modus tollens UNGROUNDED: pre-warrant verifier issue,
  orthogonal to this ticket.
- binomial-coefficient: claim-pack pillar VII cites Brualdi /
  Stanley / Knuth, none surface-ingested.

No false positives observed — the render tail correctly stays
silent when chain-of-custody data is absent.

Roadmap: Adding any cited textbook to the manifest →
re-running warrant-resolve → more records resolve, more queries
light up the tail. The 74 still-unresolved records are a
prioritized acquisition list (Mendelson ~20, Enderton ~10,
Stanley ~5, Brualdi ~3, Knuth ~3). The substrate writes its
own roadmap.
2026-05-09 18:00:36 -04:00
aad24d3cfe
docs: clear all 39 cold-build Sphinx warnings (truly green)
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
2026-05-09 18:00:15 -04:00
69e0a957ad
ticket #000031 Phase 3: warrant-chain render tail + theorem-name resolver
Two improvements that together make the warrant chain visible at
Q&A time. Phase 3 (verifier wiring) lights up the chain-of-custody
on rendered audit lines; the resolver fix makes the underlying
proofs actually point at meaningful per-axiom chunks.

Phase 3 — warrant-chain render tail
====================================
arborist/cli.py:_render_warrant_chain_tail — when a Q&A answer
cites a claim-pack record that has a `warrant-resolver-v1`
derivations row binding it to a primary-source surface chunk,
the rendered audit line gets a positive-signal tail:

  STRICT · via quote · warrant: 1 proven  1/1  0.9s  (cached)

Render-only — no schema change, no audit_mode change, no
governance_policy_hash change. The verifier produces the same
audit_mode + violations as before; this layer just SURFACES the
chain-of-custody when one exists. Silent in absence of data
(no chains → no tail).

Threading: shards_dir is stashed on result["_shards_dir"] in
_cmd_query before render, stripped before JSON output. Render
function signature stays (result, question) — pure function of
the result dict.

Resolver fix — theorem-name discriminating tokens
=================================================
arborist/qa/warrant_resolver.py:_build_fts_query — switched from
OR-union to AND-required on discriminating tokens. The previous
strategy had all 18 Hilbert axioms binding to the SAME chunk
because they all share "axiom" + "Hilbert"; the new strategy
extracts the discriminating token from each theorem name
("Pasch's Axiom" → "Pasch"; "Axiom of Betweenness" → "Betweenness")
and AND's them together. Each axiom now points at its own chunk.

Re-running the resolver on a clean shard:
  Pasch's Axiom         → chunk_idx=1   (early Group II chapter)
  Axiom of Betweenness  → chunk_idx=2
  Axiom of Angle Cong.  → chunk_idx=8   (congruence chapter)
  Pythagorean Theorem   → chunk_idx=26  (similitude chapter)
  Sum of Angles in Tri  → chunk_idx=57  (angle-related chapter)
  ...

11 records now resolve (down from 18) — the drop is honest:
records whose theorem name's discriminating token doesn't appear
verbatim in the cited textbook (e.g., "Vacuous Quantification"
in a propositional-logic axiom) correctly produce no match.
9 distinct chunks across the 11 records — meaningful per-axiom
binding.

A new generic-terms filter list (_GENERIC_THEOREM_TERMS) drops
"axiom"/"theorem"/"principle"/etc from the discriminating set,
so they don't pollute the AND-query.

End-to-end verification
=======================
$ arborist --shards-dir ~/.arborist/shards query \\
    "What is Pasch's axiom?" --top-k 3
What is Pasch's axiom?
  STRICT · via quote · warrant: 1 proven  1/1  0.9s  (cached)
  ...

vs. a query whose cited records have no warrant chain:
$ arborist --shards-dir ~/.arborist/shards query \\
    "What is Bayes theorem?" --top-k 3
What is Bayes theorem?
  HYBRID · via paraphrase  9/11  5.8s  (fresh)

The Bayes case stays silent because Kolmogorov isn't surface-
ingested. The Pasch case lights up because Hilbert IS, and the
warrant resolver bound this specific record to Hilbert chunk 1.

Test suite stays at 1588 passed / 28 skipped — render-only +
read-only changes outside the verifier path.

Phase 3 complete; Phase 4 (Mendelson + Enderton license decision
+ ingest) remains the natural follow-up to widen warrant
coverage from 11/92 records to a larger fraction.
2026-05-09 17:54:25 -04:00
f0e6baf907
ticket #000031 Phase 2: warrant resolver + 18 derivations rows landed
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.
2026-05-09 17:35:39 -04:00
9c42a133e7
docs: wire v7-W substrate paper into Substrate toctree
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.
2026-05-09 17:32:39 -04:00
0e4f050e8c
docs: propagate kernel/sub-battery counts to canonical surfaces
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}/)
2026-05-09 17:27:02 -04:00
455fc10c2a
docs: errata pass on dav1dprometheus update from external review
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)
2026-05-09 17:22:12 -04:00
2b9d1f0b72
qa/query: fan shard search out across a thread pool
Per-shard search work in _search_corpus is independent (separate
SQLite connection, separate accumulators, no shared mutation
until merge), so the old serial loop was leaving wall on the
table — the slowest fts5_body call on a wide-pool query took
30s on its own shard while the others sat idle.

Extract the four routes (fts5_body, title, phrase, core_keyword)
into _search_one_shard and fan over shards via ThreadPoolExecutor.
Shard arrival order now interleaves; the downstream raw.sort +
dedup makes order irrelevant. Worker count caps at min(8, len(paths))
or via ARBORIST_SHARD_WORKERS for cgroup-bound runners.

Measured against ~/.arborist/shards (4 wiki shards + 3 small):

  query: "where is Gundremmingen located? where is Bavaria?"
    before: 66.32s total (search 62.22s, serial)
    after:  15.54s total (search 14.60s, parallel)
    -76% wall, 4.3x search speedup

  query: "is Gundremmingen planned to close?"
    before: 60.78s total (search 56.63s, serial)
    after:  ~12s total (extrapolated from same shape)

Slowest single shard now caps the wall (shard 002 at ~13.5s on
the Gundremmingen query). The second-order question — why does
fts5_body take 13.5s for 32 hits — is now isolated and worth a
follow-up round (likely synonym OR-pool blowing the FTS5
candidate set before BM25 truncates).

Hoisted accept_stems out of the per-shard loop body too — it's
shard-invariant, no reason to recompute per shard.

Tests: 1,560 passing under make test-ci (no regressions). Full
suite (1,684) also green.
2026-05-09 17:12:34 -04:00
0c4fbb53f8
ci: re-enable pipeline; add test-ci scope (skips wikipedia ingest)
Pipeline was disabled 2026-05-02 because CI runners overlapped
with bench infrastructure. Today the substrate is in a good
state (1,684 passing locally) and the gate has been off long
enough that drift would land silently if reintroduced.

Re-enables the workflow + adds a `test-ci` Makefile target that
skips the wikipedia ingest test files (test_wikipedia_old.py,
test_wikipedia_xml.py). Their runtime path is already exercised
end-to-end by `make ingest-*` against real shards, so the
synthetic fixtures duplicate coverage without adding signal CI
should gate on.

`make test` stays comprehensive for the local dev loop —
1,684 passed there, 1,560 passed under `make test-ci` (the
124-test delta is the wikipedia ingest fixtures).

PYTEST_XDIST_AUTO_NUM_WORKERS=4 still caps the runner's
parallelism so a re-enabled CI doesn't oversubscribe the
shared host or skew live bench latencies on the same pool.
2026-05-09 16:47:31 -04:00
a2ff9d4574
docs: archive 2026-05-09 dav1dprometheus framework update
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.
2026-05-09 16:20:57 -04:00
056dda2fd7
docs: update #000031 status + CLAUDE.md textbook layer pointers
Reflects today's surface-ingest landings — Phase 1 (PD +
open-licensed textbooks across 6/7 g4 pillars) is in progress;
Phase 2 (chunk-resolution + derivations.proof_blob warrant
promotion) is the next substantial commit.

#000031 ticket file
===================
- Status flipped from "open · awaiting go/no-go" to "in progress
  · Phase 1 landed 2026-05-09".
- §8 rewritten with the landed scope: 8 textbooks ingested across
  3 license-validated manifest paths (HTML, BFS crawl, PG TeX),
  total ~351 docs / ~1597 chunks.
- Coverage table per g4 pillar.
- Phase 2 scope explicit: citation parser, chunk resolver,
  Merkle inclusion proof writer, derivations row writer,
  verifier wiring, bench. ~300-500 LOC estimate.
- Phase 3 (Mendelson + Enderton license decision) still
  deferred; Hilbert-Ackermann 1928 noted as PD substitute.

docs/TICKETS.md
===============
Index row updated to reflect "in progress · Phase 1 landed".

CLAUDE.md
=========
- sources/ comment lists the new textbook_tex source.
- Added textbook-layer make-target block to the build/test/run
  section — make crawl-textbooks, make textbooks-tex,
  make textbook ID=<id>, with the idempotency callout.

No source-code changes — pure documentation refresh aligned to
what shipped this session (commits b38f4b8 → 514e07d).
2026-05-09 16:13:31 -04:00
514e07d7c2
textbooks: TeX-source ingest closes pillars I + IV (Hilbert + Boole)
Two foundational PD textbooks ship from Project Gutenberg as
LaTeX source only — no clean HTML edition. Pandoc fails on PG's
custom preamble macros; a focused regex-based stripper is the
right amount of machinery for the well-known PG TeX format.

What landed
===========
- arborist/sources/textbook_tex.py — TextbookTexSource +
  strip_tex pipeline. Drops preamble + line comments + structural
  envs (tabular, figure, thebibliography, scshape, …); keeps the
  argument of structural-but-content-bearing single-arg commands
  (textbf, emph, section, chapter, paragraph, PG's custom \\rfa);
  drops zero-arg + brace-arg structural commands (noindent,
  thispagestyle, setcounter, label, index, …); substitutes
  symbol-level macros (\\to → →, \\neg → ¬, \\forall → ∀, \\S → §,
  Greek letters, etc.).

- arborist/cli.py — `--source textbook_tex` accepts --url,
  --bundle, or --urls-from. Reuses the existing fetch + chunker
  + Merkle commit + audit pipeline; idempotent at the database
  layer (same TeX → same prose → same document_root).

- bench/scripts/textbooks_manifest.py — gains `tex-targets`
  subcommand emitting tab-separated `<tex_url>\t<id>` rows for
  manifest entries with a `tex_url` field.

- Makefile targets:
    textbooks-tex         — ingest every entry with a tex_url
    textbook-hilbert      — convenience for PG #17384
    textbook-boole        — convenience for PG #15114
  Each writes to $(CRAWL_SHARDS_DIR)/textbook_<id>.db, idempotent
  on re-run.

- tests/test_textbook_tex.py — 20 unit tests covering preamble +
  postmatter stripping, line comments, env drops (tabular, figure),
  single-arg keepers (\\textbf, \\emph, \\section, \\rfa),
  symbol-level macro subs (10 paramerized cases), structural-cmd
  drops, whitespace cleanup, idempotence on already-stripped text.

End-to-end verification
=======================
Smoke test on PG #17384 + #15114:
  Hilbert Foundations of Geometry: 1 doc / 65 chunks (192K of
    plain prose). FTS5 finds "axiom of parallels" → real chapter
    content with axiom references intact (≡, §, math fragments).
  Boole Laws of Thought: 1 doc / 273 chunks (829K). FTS5 finds
    "law of contradiction" → "the principle of contradiction"
    passage from Chapter III of Boole's text.

Vital-books coverage now 6/7 pillars
====================================

  Pillar I   Logic        ✓ Levin + Aristotle Prior + Posterior + Boole
  Pillar II  Set Theory   ✓ Levin
  Pillar III Arithmetic   ✓ Levin
  Pillar IV  Geometry     ✓ Hilbert (PG TeX)
  Pillar V   Probability  ✗ Kolmogorov license analysis pending
  Pillar VI  Phys.        ✓ Newton Principia
  Pillar VII Combin.      ✓ Bogart + Keller-Trotter + Levin
  Pillar IX  λ-Calculus   ✗ Church + Turing 1936 papers pending

Test suite: 1574 passed / 28 skipped (was 1554 + 20 new TeX tests).

Out of scope: chunk-resolution + derivations.proof_blob warrant
promotion (#000031 follow-up; see also #000032).
2026-05-09 16:06:53 -04:00
57dafbdc3d
textbooks: per-book make targets + idempotency docs + vital-books checklist
Three concrete improvements to the textbook ingest layer:

Per-book make targets
=====================
- `make textbook ID=<id>` — generic, looks up one entry from the
  manifest and runs the right ingest path (BFS crawl if
  `crawl_url` is set, shallow URL ingest otherwise).
- `make textbook-list` — list ingestable textbook ids.
- Convenience targets per active manifest entry:
    textbook-bogart, textbook-keller-trotter, textbook-levin,
    textbook-aristotle-prior, textbook-aristotle-posterior,
    textbook-newton, textbook-morin

Each per-book target writes to a dedicated shard at
`$(CRAWL_SHARDS_DIR)/textbook_<id>.db` — one shard per textbook
id rather than one per host (which would conflate multiple
Wikisource books — Aristotle Prior, Posterior, Newton — into
one shard).

The manifest helper script gains `ids` and `lookup <id>`
subcommands so the Makefile can introspect manifest entries
without grep gymnastics.

Idempotency contract documented
================================
Every ingest path is content-addressed. Same content →
same `document_root` → no-op insert. Re-running `make textbook-*`
or `make crawl-textbooks` on the same network state is safe at
the database layer — no duplicates, no schema drift, no
audit-event proliferation. HTTP refetch happens every run; pair
with `make recrawl-check` for a HEAD-only freshness probe.

README rewritten to make this contract explicit, with shard-
layout table + crawl-delay caveats consolidated.

Vital-books checklist
=====================
The README now carries a g4-pillar coverage table:

  Pillar I   Logic        ✓ Levin + Aristotle Prior + Posterior
  Pillar II  Set Theory   ✓ Levin
  Pillar III Arithmetic   ✓ Levin
  Pillar IV  Geometry     ✗ Hilbert PG #17384 (PDF/TeX only)
  Pillar V   Probability  ✗ Kolmogorov license analysis pending
  Pillar VI  Phys. Newton ✓ Newton Principia Motte
  Pillar VII Combin.      ✓ Bogart + Keller-Trotter + Levin
  Pillar IX  λ-Calculus   ✗ Church + Turing 1936 papers pending

5 of 7 pillars now have surface coverage. The remaining gaps
are explicit license (V) or format (IV PDF/TeX, IX paper-level)
issues, each documented in the corresponding manifest entry's
notes field.

Test suite stays at 1554 passed / 28 skipped — no source-code
changes to arborist itself; the textbook layer is pure tooling
on top of the existing pipeline.
2026-05-09 15:59:31 -04:00
2acbc0e691
#000006 amend: witness-sweep first data — canonical-shape divergences
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).
2026-05-09 15:57:18 -04:00
f5c2c03d6a
textbooks: extend manifest for #000031 PD scope (Newton, Posterior Analytics, +placeholders)
Per the #000031 implementation track — surface-ingest cited
textbooks for warrant promotion of claim-pack records. Five new
manifest entries spanning the PD-scope additions plus
license-fail placeholders for citation traceability:

  newton-principia-motte (PD)
    Newton's Mathematical Principles of Natural Philosophy
    (Motte 1729 / Motte-Cajori 1846 English translations) via
    Wikisource. Crawled @ depth=2: 60 docs, 289 chunks, 10K
    edges. FTS5 spot-checks: "law of motion" → top hit on the
    1729 Motte title page; "gravitation" → Newton-titled
    chapters in the Wikisource Physics category. Cited by
    claim-pack pillar VI.

  aristotle-posterior-analytics (PD)
    Mure / Owen translations via Wikisource. Crawled @ depth=1:
    20 docs, 71 chunks. FTS5: "syllogism" → Posterior Analytics
    Bouchier + Owen translations as top hits. Companion to
    Prior Analytics already in the manifest; together cover
    pillar I logic axioms.

  kolmogorov-foundations-probability-1933 (placeholder)
    German original PD-by-age in EU; US copyright restored via
    URAA through life+70 (Kolmogorov d.1987 → US PD 2058).
    Morrison 1956 English translation: Chelsea Publishing
    copyright. Entry kept with empty urls field for citation
    traceability; license analysis pending.

  lukasiewicz-aristotle-syllogistic-1951 (proprietary placeholder)
    Oxford University Press, copyright through life+70
    (Łukasiewicz d.1956 → PD 2027 EU, longer US via URAA). NOT
    redistributable. Kept as a license-fail placeholder; the
    1921 Polish primary papers are themselves PD by age but
    lack accessible HTML editions.

License-validator drive-by
==========================
The textbooks_manifest.py validator now treats placeholder
entries (urls + crawl_url both empty) as exempt from the
allow-list license check. License discipline stays fail-closed
at the URL-emit step — placeholders without URLs raise no
exception under any license token, so we can document
yellow-light proprietary citations (Mendelson, Enderton,
Łukasiewicz) without hacks.

Coverage summary post-commit
============================
g4 pillar    | textbook coverage
─────────────┼─────────────────────────────────────────────────
I  Logic     | Levin (CC-BY-SA), Aristotle Prior + Posterior (PD)
II Set Theory| Levin (CC-BY-SA)
III Arithm.  | Levin (CC-BY-SA)
IV Geometry  | (Hilbert PG #17384 placeholder — PDF/TeX only)
V  Probability| (Kolmogorov 1933 license analysis pending)
VI Phys.     | Newton Principia Motte (PD)
VII Combin.  | Bogart (GFDL), Keller-Trotter (CC-BY-SA), Levin

Out-of-scope follow-ups: PDF/TeX source support (#000031 §5),
Mendelson + Enderton license decision (#000031 §2.1),
chunk-resolution + derivations.proof_blob warrant promotion
(separate ticket).
2026-05-09 15:47:42 -04:00
284ae52966
ticket #000033: pillar VII (combinatorics) live in shard 000
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.
2026-05-09 15:42:40 -04:00