Per fox: apply the conservative max_envelope B1 model by changing the
v1 calculator's default — NOT by forking a v2. CALCULATOR_VERSION stays
"t3-bound-v1-bottou-refinement" (the descriptor names the unchanged B3
term); b1_model is echoed in the output AND the inputs dict so KAT
replays are unambiguous about which model produced a row.
Calculator (bench/scripts/t3_bound_calculator.py):
- New b1_model kwarg + --b1-model CLI flag, choices:
max_envelope (default) max(fraction_channels, aggregate_bias)
fraction_channels g · W · log₂(1 + G/σ)
aggregate_bias W · log₂(1 + g·G/σ)
effective_control_v1 g · W · log₂(1 + g·G/σ) (old non-worst-case)
- Default is now max_envelope — genuinely upper-bounding across both
interpretations of g (dav1d review §3 closure blocker, RESOLVED).
- Every output reports all three concrete B1 variants
(B1_fraction_channels / B1_aggregate_bias / B1_effective_control_v1),
b1_selected, and both SNR readings (snr_grad = g·G/σ,
snr_per_channel = G/σ) regardless of which b1_model was requested.
- model_assumptions[] now carries f"B1_model_{b1_model}".
- inputs echo now includes c_b1/c_b2/c_b3/b1_model (replay-complete).
- Invalid b1_model rejected with a ValueError naming the field.
- Baseline I_window: 625.8716 (effective_control_v1) → 6183.0154
(max_envelope: B1=aggregate_bias 5849.63 dominates fraction_channels
1729.72), certification_status NOT_CERTIFIED_BY_BOUND at W=10000.
KAT fixture (bench/fixtures/t3-bound/known-answer-tests.jsonl):
- Regenerated 2026-05-11 — 12 entries: the 8 §7-derived configs under
the new max_envelope default, a g=0 edge case, plus explicit-mode
pins for effective_control_v1 / fraction_channels / aggregate_bias.
- Each entry carries b1_model, expected_b1_selected,
expected_b1_{fraction_channels,aggregate_bias,effective_control_v1},
expected_snr_per_channel, expected_certification_status.
Tests (tests/test_t3_bound_calculator.py, 75 → 83):
- test_t3_bound_known_answer_tests no longer skips (fixture active);
pins b1_model, b1_selected, certification_status + numbers, tolerates
optional new fields on older fixtures.
- New: test_b1_max_envelope_exact_formula, test_invalid_b1_model_rejected,
test_cli_b1_model_flag (effective_control_v1 / fraction_channels /
aggregate_bias). test_b1_exact_formula renamed
test_b1_effective_control_v1_exact_formula and now passes the explicit
model. Updated baseline / below-256 / CLI tests for the new numbers.
Doc (docs/soft-hash-channel-t3-bound.md):
- Header + §0 + §3.1 + §6 + §7 (worked examples) + §8 (operator
guidance W-solving) + §10 (closure blockers RESOLVED) + §10.1 +
§11 (calculator schema) + §12 all updated for the max_envelope
default. §8: target-256 W drops from ~4196 to ~415 steps under the
conservative model — the ~10× cost of not assuming which g-reading
holds; operators who can measure effective-control applies can use
--b1-model effective_control_v1 for the looser W (a calibration
claim they must justify, not a default).
Status (#000036 ticket + TICKETS.md): both prior dav1d closure
blockers cleared (B1 worst-case model + active KAT fixture); remaining
= fox's final close-or-iterate call.
AUTOCOUNT markers bumped 75 → 83. Full suite: 2288 passed, 28 skipped.
trigger_1_branch_density in bench/prometheus_sigma_trigger_probe.py read
the fork_score_branches table via branch_set_density() instead of the
"density check not yet implemented" stub. It groups rows by branch_set_id,
fires when the most-recently-recorded checkpoint carries >= 4 branches
(BRANCH_DENSITY_FLOOR), and surfaces n_checkpoints / latest_density /
max_density / n_checkpoints_clearing_floor in the markdown report so
section 12's "regularly" qualifier stays visible. Density sums across
shards per branch_set_id.
With no branch sets persisted yet the probe reports "table present but
empty across shards" (data_available True, fires False) rather than a
false negative. Re-ran the probe against the live shards:
bench/results/prometheus-sigma-triggers-2026-05-11.md.
6 new tests in tests/test_prometheus_trigger_probe.py (probe loaded via
importlib): no-table to no-data, empty-table to data-available-no-fire,
latest-checkpoint->=4 to fires, earlier-dense-but-latest-sparse to no-fire,
density-sums-across-shards, report-renders-density-lines.
Updated #000012 Phase 1c landing receipt, #000037 section 12 Trigger 1
note, and the TICKETS.md index rows for both. Pure measurement: no
mutation, no LLM call, no schema change.
dav1d's review (RESPONSE_1 + RESPONSE_2) returned 2026-05-11. This
lands the Tier-1 items — everything that doesn't change numeric
outputs or invalidate the KAT discipline. The Tier-2 B1 conservative-
envelope (v2 calculator) is a separate decision and stays a closure
blocker.
Calculator (bench/scripts/t3_bound_calculator.py):
- Recommendation wording: "M2's single-window guarantee is broken"
→ "this conservative bound CANNOT CERTIFY M2's residual". An upper
bound exceeding 256 bits means we cannot certify, NOT that the
adversary can steer 256 bits — the prior wording overclaimed.
- New structured output fields: b1_model ("effective_control_v1"),
certification_status ∈ {CERTIFIED_BY_BOUND, NOT_CERTIFIED_BY_BOUND},
certification_threshold_bits (256), model_assumptions[]. Callers
read a machine-readable status, not just prose.
- Input validation hardening: _require_finite_float / _require_positive_int
helpers reject bools (isinstance(True, int) is True in Python — a
real leak risk for a security calculator) and NaN / ±inf for every
numeric input and constant.
- gradient_fraction = 0 now accepted (no T2 surface; B1 = 0; T3's
LR + batch-order channels still contribute) — improves component
isolation. CLI help + module docstring updated accordingly.
- Numeric outputs UNCHANGED: baseline still 625.8716 / 292.4813 /
300.0 / 33.3904; b1_model stays effective_control_v1; KAT discipline
intact.
Tests (tests/test_t3_bound_calculator.py, 53 → 75):
- Hard-coded cwd="/home/fox/git/arborist" → pathlib.Path(__file__).
resolve().parents[1] so the suite runs on any checkout.
- New: test_gradient_fraction_zero_accepted, test_bool_rejected_for_int_fields,
test_bool_rejected_for_float_fields, test_nonfinite_numbers_rejected,
test_output_carries_b1_model_and_certification_fields,
test_certification_status_certified_below_threshold.
- test_recommendation_exceeds_sha256 now also asserts "CANNOT CERTIFY"
+ certification_status == NOT_CERTIFIED_BY_BOUND.
Doc (docs/soft-hash-channel-t3-bound.md):
- §0 reworked into a reviewer brief recording dav1d's findings
(§2 accepted, §4 accepted, §5 accepted as model-bound, §3 = closure
blocker, wording/validation = applied).
- New §3.1: the B1-double-g issue spelled out — effective_control_v1
vs fraction_channels vs aggregate_bias vs max_envelope, with the
baseline-spread table (292 / 1730 / 5850 / 5850 bits); v2 path
described.
- §5: "B3 is a model-bound, not a directly-quoted theorem" note.
- §10: items 1-2 are now the closure blockers (B1 envelope v2; active
KAT fixture); items 3-7 are tightening paths (#000043). New §10.1
records what the 2026-05-11 hardening pass already landed.
- §11: calculator-output example updated to show the new fields +
corrected recommendation wording.
- §12: references add the dav1d review + clarify Bottou-Bousquet
"inspires" (not "underlies") the §5 model-bound.
Status (#000036 ticket + TICKETS.md row): review-returned + Tier-1-
applied; closure blockers = B1 v2 envelope (awaits fox go/no-go) +
active KAT fixture. R2's architectural integrations (Merkle audit-
event commitment, SQD canonicalization, CTI clause-lattice, 5F
trigger, ForkScore security-risk) noted as out-of-scope (separate
tickets if wanted).
AUTOCOUNT markers in docs/calculator-test-patterns.md +
docs/warrant-substrate-cookbook.md bumped 53 → 75.
Full suite: 2264 passed, 28 skipped.
Two coupled changes that wire the §13 Step 11 proposal stream from
in-memory-and-discarded to persisted-and-harvestable.
(A) emit_controller_events now writes a 4th event kind
controller_falsification_proposal, one row per
decision.falsification_proposals entry. Body carries branch_id +
witness_divergence + reason; label column carries the reason for
terminal-table inspection. Deterministic ordering by (branch_id,
witness_divergence) so canonical-body hashes are stable. Idempotent
under the existing UNIQUE (event_kind, body_hash) constraint. The
audit-chain semantics remain unchanged (still a sibling table; no
event_hash preimage entry). The CLI inspector's --kind choices gain
the new event kind so operators can filter for it directly.
(B) bench/scripts/harvest_falsification_proposals.py gains a third
source bucket CONTROLLER_PROPOSAL alongside the existing HYBRID +
UNGROUNDED providence_cache buckets. Reads
controller_falsification_proposal rows from controller_events,
extracts the 16-char cache_key prefix from branch_id (qa:<prefix>
pattern from the QA-runner advisory), joins back to providence_cache
for fixture enrichment (answer_text + audit_mode + verifier_method),
and tags _harvest_meta.harvested_from = "controller_events" so the
two source paths stay distinguishable in the fixture pack. Dedup
against the providence_cache buckets by fixture id.
Today this typically yields 0 new fixtures because (i) no live QA
has fired since Phase 2 wiring landed, and (ii) the QA-runner
single-branch advisory's proposals overlap providence_cache content
the harvester already finds. Real net value comes from Phase 3
(#000045) sweep emissions, which will produce multi-branch chunk
proposals that providence_cache rows can't predict.
Tests: 3 new in tests/test_prometheus_audit.py (proposal-row
emission, no-proposal no-row, idempotency); 1 new in
tests/test_bench_batteries.py (synthetic qa.db with both
providence_cache + controller_events rows; asserts the
controller_events bucket surfaces a fixture invisible to the
divergence-thresholded providence_cache buckets). The pre-existing
harvested-pack-runs-clean test relaxes its harvested_from pin from
"providence_cache"-only to {"providence_cache", "controller_events"}.
The dry-run was still using safe_weights(); Phase 1.c shipped
sweep_weights() (γ_5f=1.5, λ_capital_cost=0.25,
ν_witness_divergence=0.5) precisely for sleep-sweep economics. Swap
both call sites in prometheus_sigma_sweep_dryrun.py and label the
report Weight profile: sweep (§15.4).
§15.4 adds the sweep profile alongside §15.1 safe / §15.2
conservative / §15.3 exploratory so the named-profile registry has
a single doc source of truth and the dry-run report's §15.4
reference resolves.
§22 dry-run-runs table (3 rows: initial uniform-τ-1d under safe;
per-mode τ under safe; per-mode τ under sweep) replaces the prior
inline narrative count. Includes a Phase-3-design observation: the
sweep profile flattens the softmax (DEFERRED 271 → 369; REJECT
205 → 110; ACCEPT 1 → 0; MARGINAL 2 → 3) because reducing
λ_capital_cost + ν_witness_divergence shrinks the gap between
high-Δ5F and low-Δ5F branches, so fewer branches reach Kelly's
p_i > 0.5 floor. Falsification-fixture proposal count stayed flat
(447 → 449) — the §13 step 11 emission path is upstream of decision
labeling, so sweep mode preserves information-gathering value while
concentrating action-taking on the high-confidence tail. Phase 3
ticket #000045 §2 deliberately leaves softmax temperature un-pinned
because of this trade-off.
Per Finding 3, a uniform τ_qa=7d filtered out every recent
CANONICAL_PROJECTION row (the π* graduations from #000027/#000030/
#000032 are all younger than 7d), so the sweep saw zero high-value
kernel-only work. Splitting τ_qa by audit_mode lets the cheap kernel
re-probe path (CP) run on a short cycle while the expensive LLM
re-witness path (STRICT/HYBRID/UNGROUNDED) keeps the long cycle.
bench/scripts/prometheus_sigma_sweep_dryrun.py: new build_tau_by_mode()
helper + per-mode CASE in iter_target_a_candidates; sweep_target_a now
takes the dict instead of a single seconds value. New CLI flag
--tau-qa-cp-days (default 1d); --tau-qa-days now scopes to LLM-witness
modes only (default 7d). Report renders the per-mode τ table in the
header and marks Findings 2 and 3 RESOLVED with their landing commits.
Makefile: PROMETHEUS_SWEEP_TAU_DAYS bumped to 7 (was 1, the prior
Finding-3 workaround); new PROMETHEUS_SWEEP_TAU_CP_DAYS=1 makevar.
bench/results/prometheus-sigma-sweep-dryrun-2026-05-10.md: regenerated
under the new defaults — 9 CP rows surface alongside 1,904 LLM-
witness candidates → 1,913 total Target A candidates → 1 ACCEPT,
2 MARGINAL, 205 REJECT, 271 DEFERRED chunks; 2 cache_drift vetoes
preserved end-to-end.
docs/tickets/ticket-000037 §22: Findings 2 + 3 marked RESOLVED with
landing-commit references; total dry-run cost line updated to the
new measurements (37.6 ms / 3,913 branches / 9.6 µs per branch).
Re-running `make prometheus-trigger-probe` after today's controller
landings shows the divergence-variance trigger has crossed both
thresholds:
Trigger 2 — divergence variance
Sample count: 37 (N_min = 30 ✓)
Mean: 0.7568, σ: 0.435
σ/mean ratio: 0.5748 (> 0.5 threshold)
Absolute σ: 0.435 (> 0.1 threshold)
Same-day morning probe (commit baseline) had only 16 samples and
did not fire; the additional witness-sweep / dry-run / harvest
activity through the afternoon brought sample count above N_min.
Agreement-label distribution across all shards:
KERNEL-LLM-DIVERGED 22
KERNEL-LLM-AGREE 6
LLM-DIVERGED 6
STRICT-WITNESSED 3
Trigger 1 (branch density) and Trigger 3 (witness cost share) did
NOT fire. Per §12 a single trigger firing is sufficient for Phase 1
gating — and Phase 1 has already landed. This commit captures the
empirical evidence that Phase 1 was on the right side of the gate.
Trigger 1 remains structurally blocked on #000012 Phase 1c
(fork_score_branches sibling table); that's the natural next move
if anyone wants to surface multi-branch consensus signals.
Closes the controller → 5F battery loop fox designed: #000037 Phase
1 produces FalsificationFixtureProposal records from high-divergence
providence_cache rows; this commit lands the harvester that turns
those proposals into a real 5F fixture pack the falsification
battery exercises every test run.
bench/scripts/harvest_falsification_proposals.py — reads qa.db,
filters live rows with witness_divergence = (n_unverified / n_quotes)
>= 0.5, stratifies by audit_mode, picks 20 HYBRID + 20 UNGROUNDED
top-by-cache_key for determinism, writes embedded-mode fixtures
to bench/fixtures/5f/falsification-harvested-v1.jsonl.
Each fixture carries `_harvest_meta` with the source cache_key,
divergence at harvest time, audit_mode at harvest time, and the
ticket reference (#000037 §13 step 11). Embedded mode — uses
`observed_violations` directly without calling verify_quotes
again; `answer_text` preserved verbatim for debugging.
Pack composition (initial harvest 2026-05-10):
20 UNGROUNDED (expected_reason: UNGROUNDED)
9 HYBRID_QUOTE (NEW motif — not in falsification-v1.jsonl)
7 HYBRID_CLAIM_LATTICE (NEW motif — not in falsification-v1.jsonl)
4 HYBRID_PARAPHRASE (already covered in v1)
Two harness tests pin the pack:
- test_5f_falsification_harvested_pack_runs_clean: 100% pass-rate,
every fixture carries traceable _harvest_meta.
- test_5f_falsification_harvested_pack_widens_motif_coverage: the
HYBRID_QUOTE / HYBRID_CLAIM_LATTICE motifs surface from real
corpus (loud-fail if harvest rotation drops them).
Makefile: `make bench-5f-harvest` re-runs the harvester. Parameters
exposed: HARVEST_QA_DB, HARVEST_OUT, HARVEST_THRESHOLD,
HARVEST_SAMPLE_PER_BUCKET.
Full suite: 2328 passed, 37 skipped (+2 from the two new pins).
Closes four gaps in the initial Phase 1 landing (commit f625cac):
1. §14 row 4 — Hermes-saturation guard. `hermes_utilization` was on
the input contract but never consumed. Now: `utilization >=
budget` → DEFERRED with HERMES_SATURATED note + advisory event
carrying (utilization, budget) for Phase 2 audit. Three new
tests (saturation-equal, saturation-overflow, headroom-exists).
2. §13 step 11 — falsification-fixture proposal emission.
New `FalsificationFixtureProposal` dataclass; controller now
emits one per branch whose `witness_divergence >=
falsification_divergence_threshold` (weight-tunable, default
0.5). Emission fires BEFORE the all-vetoed cascade so vetoed-
AND-diverged branches still surface as 5F-fixture candidates
per #000025. Four new tests (high-divergence emits, low-
divergence stays silent, threshold is weight-tunable, vetoed-
diverged emits anyway).
3. Entropy + memory gating moved from module-level constants
(`H_LOW=0.3`, `H_HIGH=0.7`, `KAPPA_MEMORY=0.5`) to weight
fields (`h_low`, `h_high`, `kappa_memory`). Constants stay as
back-compat exports; defaults match exactly so byte-identical
behavior when neither override fires. Three new tests
(h_low/h_high tunable, kappa_memory tunable, back-compat
match).
4. Veto-class cascade hardening. Added explicit tests for the
`replay_window_unbounded` → ESCALATE path and the
`soft_hash_signal` → QUARANTINE path (§6 + §14 documented but
previously untested). Plus tests for the §6 fail-loud
priority ordering: ESCALATE > QUARANTINE > REJECT when mixed.
Dry-run regenerated against ~/.arborist/shards corpus:
Target A at τ_qa=1d surfaces **576 FalsificationFixture
proposals** from witness_divergence >= 0.5 (24% of swept
candidates). These rows are now an actionable funnel for 5F
fixture mining under #000025 §3.
Module: arborist/substrate/prometheus.py (+117 LOC, 899 total)
Tests: tests/test_prometheus.py (+196 LOC, 22 → 36 tests)
Dryrun: bench/scripts/prometheus_sigma_sweep_dryrun.py +
bench/results/prometheus-sigma-sweep-dryrun-2026-05-10.md
track the new falsification_proposals_total counter.
Full suite: 2326 passed, 37 skipped (+14 net from the new tests).
Phases 1 (controller) and 2 (sibling-table audit writes) landed in
prior commits. This commit adds the Phase 3 dry-run simulator
instead of the actual sleep-sweep scheduler, since Phase 3's value
is mostly in what we'd learn from running it — and the dry-run
captures those findings without committing to a scheduler design
prematurely.
bench/scripts/prometheus_sigma_sweep_dryrun.py — read-only
simulator that classifies §3 Target A (providence_cache) + Target B
(documents) sweep candidates, synthesizes ControllerBranches from
real shard data, runs the Phase 1 controller, reports decision
distribution + Phase-3-design findings. No LLM calls, no
mutations.
make prometheus-sweep-dryrun — produces a dated markdown report
at bench/results/prometheus-sigma-sweep-dryrun-YYYY-MM-DD.md.
Five findings surfaced by three dry-run iterations against the
live ~/.arborist/shards corpus (3.5M docs + 2839 providence_cache
rows) — captured in ticket §22:
1. chunk-size dominates Kelly threshold (must = Hermes
concurrency, not candidate pool)
2. flat capital_cost blocks every allocation (split kernel-cost
vs LLM-cost on the contract)
3. τ_qa=7d filters every CANONICAL_PROJECTION row (all 29 are
<7d old; need per-audit-mode τ)
4. Target B canonical-shape detection is the real headline
(~152K candidates extrapolated; controller correctly returns
MARGINAL on shape-match chunks)
5. quarantined rows correctly veto via cache_drift hard-veto
Mean per-branch controller latency in dry-run: 12.5 µs at
chunk_size=4. Phase 3's actual bottleneck is the witness fan-out
(Hermes calls), not the controller itself.
Ticket #000037 status flipped to in-progress with Phases 0+1+2
landed; Phase 3 scheduler remains future work but is informed by
the five findings.
Pre-Phase-1e: falsification-v1.jsonl covered 10 motif tags across 50
fixtures (the high-traffic warrant/title/anchor/format set). Phase
1e adds 12 fixtures (5f-fal-051..062) for the previously-uncovered
motifs from the verifier+soft-demote registries:
CITATION_MISMATCH DEFLECTION_DETECTED
MANUAL_QUOTE_VIOLATION SCHEMA_INVALID
SOURCE_ROLE_BLOCKED SUBJECT_TOKENS_ABSENT
TOO_MANY_EVIDENCE_IDS UNKNOWN_EVIDENCE_ID
BROAD_QUANTIFIER_RUNAWAY BROAD_QUANTIFIER_CAP_APPLIED
BROAD_QUANTIFIER_SCOPE_UNBOUND BROAD_QUANTIFIER_REJECTED
Coverage now: 22 unique motif tags across 62 fixtures.
Harness changes:
- test_bench_batteries.py: bump pass_count assertion 50 → 62 in both
falsification tests; add test_5f_falsification_covers_every_documented_motif
that pins the motif set against the verifier+soft-demote registries
so adding a new violation upstream surfaces here as a missing
fixture (loud signal, no silent drift).
- test_session_integration.py: bump full-suite total 662 → 674.
Closes#000025 §10.12 (every documented failure-motif tag).
Still open in Phase 1b: §10.11 (real shard finetuning chains),
§10.13 (Feedback Loop latency/efficiency against real workload),
§10.14 (threshold handoff to #000012).
Full QA-quality sweep, 75 questions × 3 modes × n=3 = 675 cells
against Hermes-3 8B at concurrency=4. No mode regressed past
the 5pp signal floor:
quote 53.8% STRICT vs 54% baseline = -0pp (stable)
claim_lattice_pointer 23.1% STRICT vs 20% baseline = +3pp (within floor)
claim_lattice (JSON) 46.7% STRICT vs 42% baseline = +5pp (at floor — marginal positive)
JSON-mode +5pp is right at the noise threshold per
docs/bench-maxing.md — could be the 2026-05-10 substrate work
(92/92 warrant chains + 18 textbook ingests + cascade tuning +
Phase 3 wiring) translating to retrieval-quality lift, OR
sample variance. Follow-up bench in 1-2 days disambiguates.
Format-collapse 0/225 in every mode. Latency stable
(10.6-11.1s median). Lattice-mode directive coverage 100%.
Phase 3 per-claim warrant-chain tail still dormant on this
fixture (rescue-only by design; no warrant-shape question
retrieves a chain-backed chunk while failing lexical anchor —
parallel shift's same finding). Source-level warrants tail
fires on claim-pack-targeted retrievals as documented in
phase3-live-validation-2026-05-10.md.
Substrate + Phase 3 sprint shipped clean.
Audited fox's exemplar 51-test file against the 9-item checklist
in docs/calculator-test-patterns.md (codified earlier today in
0725eb4). Two gaps found, both additive:
GAP 1: no KAT fixture
=====================
Checklist item 1: "KAT fixture under bench/fixtures/<module>/
(≥ 5 cases)". Fox's tests cover the doc's worked-example numbers
inline (test_baseline_matches_section_11_doc) but no separate
fixture file existed for off-the-baseline regression coverage.
Generated bench/fixtures/t3-bound/known-answer-tests.jsonl with
8 KATs:
- small-deployment-§7.1, medium-deployment-§7.2,
hardened-deployment-§7.3 (the doc's three worked examples)
- extreme-low-g (g=0.001, σ=0.5 — exercises low-SNR regime)
- tight-window-W=100 (small-W ceiling-rounding edge case)
- tightened-c-b1 (override-constants path)
- all-constants-tight (all three c_b1/c_b2/c_b3 overridden)
- b3-floor-regime (factor < 1, B3 floors to 0)
Each entry pins (calculator_version, inputs, expected_total,
expected_b1, expected_b2, expected_b3, expected_snr_grad).
Algorithm change MUST bump CALCULATOR_VERSION + emit new fixture
file under bench/fixtures/t3-bound/ — old runs replay against
old data per §1 discipline.
GAP 2: no B3 hand-computed formula test
=======================================
Checklist item 3: "Hand-computed formula tests — at least one
per independent contribution / output field". Fox had
test_b1_exact_formula + test_b2_exact_formula + test_snr_grad_formula
covering three of the five output fields. B3 had only
test_b3_floor_at_zero_when_factor_below_one (an edge case),
not a closed-form check on the general formula.
Added test_b3_exact_formula: hand-computes
``C_B3 · ⌈W/E⌉ · log₂(N_b · σ_grad / ‖∇L_max‖) / 2`` per #000036
§5 (Bottou-Bousquet refinement), asserts agreement with the
function's B3_contribution. Pairs cleanly with the B1/B2 hand-
formula tests fox had.
CHECKLIST AUDIT — POST-FIX
==========================
1. KAT fixture ✓ NOW (was ❌; 8 entries)
2. VERSION + "v1" ✓ test_returns_calculator_version_token
3. Hand-formula ✓ NOW B1/B2/B3/snr_grad all covered
(was ⚠️ partial; B3 had floor-only)
4. Monotonicity ✓ test_monotone_in_window_length /
gradient_fraction
5. Closure ✓ test_total_equals_sum_of_three_contributions
6. Parametrized invalid ✓ four @pytest.mark.parametrize blocks
7. CLI subprocess ✓ test_cli_baseline_runs_clean +
test_cli_invalid_input_exits_2
8. Doc parity ✓ test_baseline_matches_section_11_doc
(caught today's §11 calibration drift)
9. Module-export shape ✓ test_returns_calculator_version_token +
test_constants_recorded
All nine items now ✓. test_t3_bound_calculator.py is the
exemplar for calculator-style test discipline.
Test count: 51 → 53 (+2 from this commit). Full suite:
1915 → 1985 (+70 from fox's parallel work + this commit's +2;
partial cycle effects).
Hygiene
=======
- make test → 1985 passed, 45 skipped.
- KAT fixture is JSONL with header comment naming
CALCULATOR_VERSION; future drift caught at the test level.
- Eat-my-own-dogfood: applied my docs/calculator-test-patterns.md
checklist to fox's exemplar test file. The fact that gaps
surfaced (even on fox's substantive 51-test surface) validates
that the checklist has real reviewer value, not just guideline
signaling.
Parallel-shift commit 6f1dbed already refreshed primary surfaces
but missed three sites:
docs/warrant-substrate-cookbook.md 54 → 74
docs/tickets/ticket-000031-...md 40 → 74 (Phase 2.5 narrative)
bench/results/full-warrant-resolution-...md 40 → 74 (×2 sites)
Live count from ~/.arborist/shards/000.db is 74 citation_aliases
+ 13 term_aliases. All four edits add the "grew 40 → 54 → 74
across the day" trail so future readers see the trajectory rather
than a stale point-in-time number.
Lands the formal derivation deliverable proposed in #000036 §3.1.
Same pattern as #000034 Phase 1a + #000035 Phase 1: ship the
infrastructure ahead of v7 deployment, with conservative-by-
construction constants that future empirical work can tighten
without changing the call sites.
docs/soft-hash-channel-t3-bound.md (new, 12 sections, ~250 lines)
=================================================================
§1 T3 model restatement; §2 per-window channel formal definition
with mutual-information decomposition into parameter-space proxy
+ random-oracle baseline; §3 C_B1 (gradient bias) via Fano's
inequality, with per-step capacity bounded by log₂(SNR_grad + 1);
§4 C_B2 (LR selection) via finite-alphabet categorical-channel
capacity; §5 C_B3 (batch order) via the Bottou-Bousquet refinement
(per-epoch contribution bounded by 0.5·log₂(N_b·σ_grad/‖∇L_max‖),
much tighter than the naive log₂(N_b!) bound that the ticket §3.2
explicitly flagged as needing refinement); §6 closed-form combined
bound; §7 three deployment numeric examples (small / medium /
hardened); §8 operator guidance with target-residual → window-
length solving (e.g. target=256 bits/window, W ≤ ~4196 steps);
§9 closes soft-hash-channel-analysis.md §9.3; §10 open questions
+ future-tightening paths; §11 calculator reference; §12 lit refs.
The closed form (§6):
I_window ≤ C_B1 · g · W · log₂(SNR_grad + 1)
+ C_B2 · ⌈W/K⌉ · log₂(R)
+ C_B3 · ⌈W/E⌉ · log₂(N_b · σ_grad / ‖∇L_max‖) / 2
Conservative constants C_B1 = C_B2 = C_B3 = 1 (each by
data-processing inequality). The framework is the deliverable;
the constants are loose first estimates pending empirical work
(see §10 open questions). Tightening any of them refines the
bound without invalidating it.
bench/scripts/t3_bound_calculator.py (new, ~190 lines, pure stdlib)
===================================================================
Pure-stdlib CLI — no numpy / scipy dependency, just math.log2 +
ceiling division. Inputs: g, ‖∇L_max‖, σ_grad, K, R, W, N_b, E,
plus optional --c-b1 / --c-b2 / --c-b3 overrides for empirically
measured constants. Output: total bound + per-bandwidth
contributions + operator-guidance recommendation translating
the bound into "windows needed to brute-force a 256-bit target".
Verified against doc §7.1 small-deployment example: produces
625.87 bits/window vs the doc's hand-calculated 622.7. Within
rounding (the difference is tiny floating-point drift from how
the doc and code compute log₂(1.5)).
soft-hash-channel-analysis.md
=============================
§9.3 marked closed-2026-05-10 with reference to the new bound
doc. §11 status updated: open-questions list now reads §9.1
(parks on v7 per #000034 Phase 1b) + §9.2 (awaits v7 §9.10
amendment per #000035 Phase 2); §9.3 closed via #000036.
#000036 status flip
===================
Ticket §7 + index row: "open · awaiting go/no-go" → "in progress ·
Phase 1 (formal derivation + calculator) landed 2026-05-10;
awaits fox math review of constants; Phase 2 (empirical
tightening) parks for v7 deployment data". Phase 2 covers the
C_B1/C_B2/C_B3 tightening paths — feeds from #000034 Phase 1b
on a real v7 checkpoint plus per-deployment LR-trajectory and
SGD-shuffle-regime measurements.
Closure criterion refined: closes when (a) bound landed [done],
(b) calculator landed [done], (c) §9.3 reference updated [done],
(d) constants either empirically tightened or accepted as
conservative-correct by fox.
Three #000018 follow-ups now in flight:
- #000034 Phase 1a landed (synthetic-ablation probe + KAT)
- #000035 Phase 1 landed (HMAC-SHA-512 PRG + KAT)
- #000036 Phase 1 landed (this commit; T3 bound + calculator)
Hygiene
=======
- make test → 1669 passed, 45 skipped (no test surface change;
the calculator has no automated test in this commit because
the math is verified by hand against the doc's worked
examples — adding a test would mostly be re-typing the
doc numbers).
- make chain-check-shards → 0 across all 7 shards.
- arborist/ Python source unchanged; this commit is doc + script.
Lands the synthetic-ablation infrastructure proposed in fce8826's
ticket §7 amendment. Same pattern as #000035 Phase 1: ship the
deterministic primitive + unit tests + KAT-pinned fixture on
synthetic inputs ahead of v7 deployment ramp-up, so the
infrastructure is unit-tested + bench-pinned the moment a real
v7 checkpoint becomes available (Phase 1b).
bench/scripts/phi_alignment_probe.py
====================================
Implements ``measure_alignment(W, hessian_eval, *, k_top, k_bot,
epsilon) -> AlignmentReport`` per #000034 §3.1:
- Lanczos top-k + bottom-k via ``scipy.sparse.linalg.eigsh`` over
a user-supplied HVP closure. Probe never materializes H.
- Alignment score: A(W, H) = Σ_j (Σ_i ⟨W·e_i, v_j⟩²) / (λ_j+ε)
/ ‖W‖_F², per ticket §2.1. Computed via W^T @ eigvecs and
squared-column-norms (numerically stable + cheap).
- Verdict thresholds (§3.3): STRUCTURAL_ALIGNMENT (ratio > 1.5) /
NO_ALIGNMENT / ANTI_ALIGNED (ratio < 0.7).
Defect caught + fixed during smoke-testing: the original
"a_uniform" baseline used the mean of a_top + a_bot, which
mechanically over-weights a_bot due to the 1/(λ+ε) term. Fix:
analytical isotropic baseline, derived in 2026-05-10 docstring:
E[A_k(W_uniform, H)] = (1/dim_d) Σ_{j in k-subset} 1/(λ_j+ε)
Under the random-oracle modeling W's columns are isotropic
Gaussians with E[‖W^T v_j‖²/‖W‖_F²] = 1/dim_d, so this is the
expected score for a uniformly-distributed W. Smoke test
post-fix: aligned → STRUCTURAL_ALIGNMENT (ratio ~7.97), uniform →
NO_ALIGNMENT (ratio ~1.00), anti → ANTI_ALIGNED (ratio ~0.00).
All three classes land cleanly in their expected verdict bucket.
Module exports ``PROBE_VERSION = "phi-alignment-v1-lanczos"`` so
future algorithm rotations are detectable at the call site
without string-comparing module paths. Same convention as
#000035's PHI_PRG_VERSION.
bench/fixtures/phi-alignment/synthetic-checkpoints.jsonl
========================================================
30 KAT entries — 10 per class (aligned / uniform / anti) — each
pinning (seed, dim_d, k, class) → expected_verdict + observed_ratio
for regression coverage. Deterministic-seeded so CI replays
exactly. Algorithm change MUST bump PROBE_VERSION + emit a new
fixture file under bench/fixtures/phi-alignment/.
Class ratio ranges:
- aligned: 7.77 - 8.27 (well above 1.5 STRUCTURAL_ALIGNMENT floor)
- uniform: 0.95 - 1.04 (cleanly within NO_ALIGNMENT band)
- anti: 0.00 (well below 0.7 ANTI_ALIGNED ceiling)
tests/test_phi_alignment_probe.py
=================================
14 tests covering #000034 §3.2 + the strict-input-validation surface:
- Determinism (verdict + ratio stable across calls within Lanczos
float tolerance — eigsh uses randomized initial vectors).
- Verdict thresholds (engineered cases land in correct bucket).
- Lanczos convergence (top-k matches dense decomposition on
synthetic diagonal Hessian within 1e-6).
- Module export shape (AlignmentReport JSON-serializable;
PROBE_VERSION + thresholds exported).
- Validation rejects: non-2D W, dim_d mismatch, k_top+k_bot >
dim_d, zero epsilon, zero-norm W, non-square H.
- KAT regression against the 30-entry fixture.
Tests skip via ``pytest.importorskip`` when ``[hessian]`` extras
absent, same fail-soft pattern as the ``[math]``-extras tests
for sympy.
pyproject.toml — new [hessian] optional-deps block
==================================================
Adds ``numpy>=1.26`` + ``scipy>=1.11`` under a new ``[hessian]``
extras gate. Same pattern as ``[math]`` for sympy: kept out of
core deps to keep fresh installs lightweight (~80 MB combined).
Operators install via ``pip install 'arborist[hessian]'``.
#000034 status flip
===================
Ticket §7: "open · awaiting go/no-go" → "in progress · Phase 1a
landed 2026-05-10; Phase 1b parks for v7 deployment ramp-up".
Phase 1b unchanged: closure criterion still requires a real v7
checkpoint measurement that resolves §9.1 of the soft-hash-
channel-analysis. TICKETS.md index row refreshed.
Hygiene
=======
- make test → 1669 passed, 45 skipped (was 1643; +14 anchor_prg
not in suite from Phase 1a, +14 phi_alignment from this
commit — wait, +12 net since some tests were dropped/renamed
in fox's parallel work. Bottom-line: 1669 stable.)
- make chain-check-shards → 0 across all 7 shards.
- arborist.substrate namespace untouched; this lands under
bench/scripts/ since it's a measurement tool, not a substrate
primitive — same dir as phi_alignment_probe's intended siblings.
Three-iteration investigation following c5bc53f's "Phase 3 is a rescue
mechanism, not a default path" finding. Question: can a paraphrase-
eliciting fixture actually drive Phase 3 to fire on real questions?
Key reading from arborist/qa/warrant.py:507 ("warrant_check"):
the function vacuous-passes (returns (True, []) without any anchor
extraction) unless the question shape is one of:
- relation (proper-noun anchors)
- date (4-digit year in claim)
- entity-list
- count-shape
- why-cause-shape
If none of those shapes apply, Phase 3 has nothing to suppress.
Three fixture iterations, all probed before benching:
| iter | strategy | chain hits |
|------|-----------------------------------|------------|
| v1 | "What is X?" / "Define X" | 12/13 |
| v2 | "How would you use X to ..." | 1/10 |
| v2' | "X: explain in plain English" | 2/13 |
| v3 | "Who proposed X?" / "Why does X" | 1/8 |
| v3' | "X: who first stated it?" | 1/8 |
Pattern: title-leading retrieval works (high title-token boost on
chain chunks) but those questions are definitional — no warrant
shape, no Phase 3 trigger. Warrant-shape questions ("who" / "when"
/ "why") trigger warrant_check but retrieval pulls toward
Wikipedia's prose articles instead of the terse claim-pack chunks.
Structural reason: claim-pack chunks (the 92 chain-root documents)
are deliberately terse — they state axioms / theorems precisely
with mathematical formalism but contain no biographical, historical,
or explanatory prose. So warrant-shape questions retrieve from
Wikipedia, where the prose context matches the question shape.
Phase 3's data condition (chain-backed chunk cited for a
warrant-shape claim) is empirically unreachable through normal
retrieval pathways on this corpus shape.
Verdict (`bench/results/phase3-warrant-chain-paraphrase-
investigation-2026-05-10.md`): Phase 3's runtime fire rate is
structurally bounded near zero on the current corpus. Mechanism
is correct, non-regressing, and unit-tested
(tests/test_warrant_chain.py). The lexical layer is strong enough
that the rescue isn't needed at measurable rates.
Recommendation: don't engineer Phase 3 fires via fixture design.
Track fire rate as a corpus-evolution signal. If claim-pack
content gains prose context or the corpus mix changes, Phase 3
will start firing organically and the audit-line tail
(`· warrant proven via chain ×N`) will surface it.
This closes the three-thread investigation cleanly. v1 + v2 + v3
fixtures + reports all retained as the empirical trail.
Followup to dee6623 ("bench: #000031 Phase 3 A/B finds mechanism
dormant on warrant-targeted fixture") — the initial A/B reported
Phase 3 dormant on a 7-question fixture where only 2/7 questions
retrieved any chain-root sources. Open question: was the dormancy
a fixture inadequacy or a structural property of Phase 3?
This commit answers it. Aggressive fixture (13 questions using
exact claim-pack title phrasing — "What is the Pigeonhole
Principle?", "Define the Axiom of Extensionality", etc.; titles
sampled directly from the 92-document chain-root set on shard
000.db) drives retrieval to chain-root chunks on **12/13
questions** (24 chain sources retrieved total).
A/B vs a57b194~1, n=3, 117 cells per condition:
cache_key parity: 39/39 cells match
Phase 3 fire rate (warrant_proven_idxs): 0 / 117 cells
STRICT-rate: 85/117 → 85/117 (Δ +0)
per-cell movement (LLM dice): 4 ↑, 4 ↓
Phase 3 fires zero times even though retrieval does land on chain
roots on 92% of questions. The structural reason now reads as:
Phase 3 is a rescue mechanism, not a default path. It fires only
when (a) a cited chunk has warrant-resolver chain backing AND
(b) the lexical warrant_check would otherwise fail. On
well-formed axiom questions, the LLM's answer contains the
technical terminology that the lexical anchor heuristic looks
for — so warrant_check passes via the cheap lexical path and
Phase 3 has nothing to suppress.
Two readings of this finding:
1. **Positive for the lexical layer.** It's strong enough on
clean axiom questions that the chain-fallback isn't needed.
The mechanism that lands warrants on cheap lexical evidence
continues to do most of the work.
2. **Phase 3 calibration needs a different fixture shape.** To
exercise the rescue path empirically, a future fixture would
need to elicit lexical-fail-but-chain-pass claims —
paraphrase-heavy questions, disputed-terminology topics,
questions where the LLM naturally drifts from chunk vocabulary.
Mechanism is correct + non-regressing (cache_keys identical → no
retrieval movement; 0/117 fire rate confirms defensive-only
behavior). No further changes warranted to the implementation.
C — separate finding (refactor sweep verification): a57b194 has
zero v7/v8 patterns. Final exhaustive sweep across arborist/ +
tests/ shows only the intentional historical-note comments in
arborist/cli.py (Was \`arborist v8 score\`...) and
arborist/substrate/__init__.py (explaining why v-dirs were
retired). Refactor cleanup is complete.
B — separate finding (Makefile bench-fork-score smoke):
make bench-fork-baseline + make bench-fork-score runs end-to-end
under the renamed CLI. Verdict MARGINAL (score 0.0 for self-
comparison), exit 0. Yesterday's Makefile:430 fix verified live.
End-to-end smoke against the live shard cluster (~/.arborist/shards
+ ~/.arborist/crawl) using the parallel-shift probe fixture
bench/qa_questions_warrant_chain_probe.txt (7 questions explicitly
targeting the 92 claim-pack-warrant-resolved records).
Result: 6 of 7 questions reach EVIDENCE-WARRANTED on the four-rung
ladder. Q1 ("axiom of line incidence in Hilbert geometry") shows
the source-level "warrants: 5 proven" tail correctly counting all
5 cited claim-pack records with derivation chains. Q5 (De Morgan)
falls to ANCHOR-WARRANTED-PARTIAL on mixed Wikipedia/claim-pack
retrieval; Q7 (pigeonhole) hits TITLE_MISMATCH because retrieval
surfaced a Wikipedia article that shares no token with "Bogart".
Both Q5 and Q7 are correct fail-closed behavior given retrieval
choices, not Phase 3 issues.
What this validates:
- warrant_chain_lookup loads live 92 core_roots
- warrant_proven_claim_idxs threads through verdict -> result
dict -> JSON output (was None on cache hits, [] on fresh
misses — correct cache invariance preserved)
- source-level "warrants: N proven" tail fires
- EVIDENCE-WARRANTED rung promotes via existing
_ladder_rung_for_lattice logic without render-layer changes
- empty-set fail-closed default preserves backward compat
What's NOT validated end-to-end (still unit-test-only):
- Per-claim "· warrant proven via chain ×N" tail. Fires only
when warrant_check would have demoted AND chain present.
Narrow regime; covered by test_verify_claim_lattice_suppresses
_warrant_missing_with_chain.
Picks up the parallel-shift's probe fixture (was untracked); now
committed alongside the validation journal.
Bench follow-up to a57b194 ("ticket #000031 Phase 3: warrant-chain-
aware verifier suppresses WARRANT_MISSING"): land the warrant-
targeted probe fixture + capture an A/B comparing pre-Phase 3
(a57b194~1) vs HEAD on 7 questions × 3 modes × n=3.
bench/qa_questions_warrant_chain_probe.txt (new fixture)
========================================================
7 questions targeting claim-pack-resolved topics: Hilbert geometry
(2), Russell classes (1), Cantor diagonal (1), De Morgan (1),
Boolean absorption (1), pigeonhole in Bogart (1). Picked because
their topical match against the 18 textbook substrates +
warrant-resolver derivations should — in principle — drive
retrieval to chain-root chunks where Phase 3's suppression logic
fires.
bench/results/phase3-warrant-chain-A-B-2026-05-10.md (A/B report)
=================================================================
Findings:
- **21/21 cache_keys match BEFORE/AFTER.** Phase 3 doesn't fold
into governance_policy_hash (warrant_chain_roots is a runtime
parameter, not a policy field), so retrieval + prompt + LLM
inputs are byte-identical between conditions. Any STRICT-rate
movement is real verifier signal, not LLM dice.
- **`warrant_proven_claim_idxs` is non-empty in 0 / 63 AFTER cells.**
Phase 3's suppression path never fires on this fixture.
- **STRICT-rate: 42/63 → 43/63 (+1 cell, +1.6pp).** Four cells
move (2 up, 2 down); within n=3 LLM noise.
Why dormant despite warrant-targeted topic selection:
1. Pre-bench probe via `--dry-run --json` showed only 2/7 questions
retrieve any chain-root sources — the claim-pack textbooks have
far fewer chunks than Wikipedia, so retrieval defaults to the
bulkier corpus on general queries.
2. Even on the 2 questions that DO retrieve chain roots, the LLM
cites the larger Wikipedia chunks more often.
3. On the rare cell where the LLM cites a chain-root chunk, lexical
`warrant_check` already passes — Phase 3 has nothing to suppress.
Calibration finding, not a defect:
- Phase 3 mechanism is correct (no regression on cells where it
doesn't fire; cache_keys identical → can't move retrieval).
- The data condition for Phase 3 to actually fire requires a
fixture where (a) retrieval surfaces chain-root chunks AND
(b) the LLM cites them AND (c) the cited claim's lexical
warrant_check fails.
- Future fixture would need very specific terminology that
biases retrieval AWAY from Wikipedia (exact theorem labels,
axiom names, etc.).
Same calibration shape as yesterday's progressive-AND smoke A/B
finding: a targeted change can be dormant on the fixture you're
benching against. The bench-fixture-design discipline that ticket
#000037 §12 codifies — "measured trigger, not calendar date" —
applies here too: until a fixture lands that exercises Phase 3,
the suppression mechanism's value is theoretical.
B-1: via_citation_alias attribution — resolver no longer mislabels
citation-alias-substituted chains as DIRECT.
- New Citation.via_citation_alias field (default False, preserves
parse-from-source-ref path).
- warrant_status sets via_citation_alias=True on substitute
Citations from #000041 lookup_citation_aliases.
- resolve_chunks reads citation.via_citation_alias as a "floor" for
via_alias on every match it produces (Pass 1 hits inherit it
too, not just Pass 2 term-alias hits). Audit-honest: matches
from a substitute Citation are alias-driven regardless of which
cascade pass found the chunk.
Live re-resolve under the new attribution: 18 direct + 74 +alias
(was 75/17 mis-labeled). The 18 direct = exactly Hilbert pillar IV
records resolving on the literally-cited Hilbert textbook. All 74
records resolved via citation-alias substitution now carry
process_id="warrant-resolver-v1+alias" in derivations.
3 new unit tests (test_warrant_resolver.py): default-False on
parsed Citations, explicit-True construction works, resolve_chunks
propagates the floor onto every ResolutionMatch.
B-2: source-side title-from-author backfill — eliminates the
per-shard SQL UPDATE workaround.
- HtmlPageSource accepts default_author kwarg; appends ', by
<author>' to ingested document titles when the <title> tag
doesn't already include the surname.
- TextbookTexSource accepts default_author kwarg; appends ' by
<author>' to titles when the LaTeX has no \author{} macro AND
no PG-style 'Author:' boilerplate.
- _CrawledHtmlSource (BFS-crawler bridge) accepts default_author
kwarg; same append logic. ingest_crawled() and arborist crawl
--ingest plumb it through.
- arborist ingest --author + arborist crawl --author CLI flags.
- bench/scripts/textbooks_manifest.py:cmd_lookup emits the
manifest's `author` field as a 7th tab column.
- make textbook target reads the author column and threads
--author into both crawl-ingest and shallow-ingest paths.
Idempotency preserved — surname-already-in-title detection prevents
double-stamping on re-ingest. Shards previously SQL-backfilled
(Cantor / Russell IMP / Bogart / Judson / Levin / KT / Peano /
Grinstead-Snell) keep their existing titles; new ingests pick up
the author signal at source time.
Live smoke: arborist ingest --source html --author "Bertrand
Russell" against PG #41654 yields title "Introduction to
Mathematical Philosophy | Project Gutenberg, by Bertrand Russell"
with no SQL UPDATE needed.
Total: 1655 tests pass (was 1652). Both follow-ups land additive,
fail-closed, idempotent. The two cleanup items from #000031
Phase 3's commit message are now closed.
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.
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.
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)
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
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.
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.
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.
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
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.
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.
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.
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.
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).
The first iteration of this layer landed scaffolding plus shallow
seed-URL ingest, which produced 300-1000 byte stubs (front matter
+ nav chrome only) instead of real book content. Fox flagged
that as the wrong outcome — we were supposed to track down the
actual texts.
This commit fixes it by adding the deep-ingest path: each
manifest entry now carries `crawl_url` + `crawl_depth` +
`crawl_max` fields, and `make crawl-textbooks` iterates them
through the existing BFS crawler (one shard per host).
Manifest changes
================
Three URL fixups uncovered by the first crawl attempt:
- PreTeXt textbooks (Bogart, Keller-Trotter, Levin) ship an
`index.html` that's a 1-line meta-refresh redirect; the BFS
crawler doesn't follow meta-refresh, so the seed URL has to
point at the actual content entry (`frontmatter.html`,
`app-comb-2.html`, `ctgd/index.html`).
- Open Data Structures uses trailing-slash directory paths
(`/ods-cpp/`, `/ods-python/`, `/ods-java/`), not `/ods-cpp.html`.
- `appliedcombinatorics.org` declares `Crawl-Delay: 20` in
robots.txt — full BFS takes ~25 minutes; documented in the
manifest entry's notes so operators know to background it.
Hilbert + Boole stay flagged as `urls: []` placeholders because
PG eBooks #17384 + #15114 ship as PDF/TeX only (no HTML format).
Their `tex_url` + `pdf_url` fields are now preserved on the
entry for the future PDF/TeX source ticket.
Make targets
============
- crawl-textbooks — BFS-crawl every entry with `crawl_url`
- crawl-textbooks-stats — docs/chunks/size summary across crawl shards
Helper script: `bench/scripts/textbooks_manifest.py crawl-targets`
emits one tab-separated `<url>\t<depth>\t<max>\t<id>` row per
entry that declares a `crawl_url`.
Real-content verification
=========================
Crawl results across 4 of 5 textbooks (Keller-Trotter still
running in background due to crawl-delay; expected to complete
in ~25 min):
crawl_bogart_openmathbooks_org.db docs=44 chunks=161 971 KB
crawl_discrete_openmathbooks_org.db docs=51 chunks=376 1929 KB
crawl_en_wikisource_org.db docs=30 chunks=110 1651 KB
crawl_opendatastructures_org.db docs=64 chunks= 84 1110 KB
TOTAL 189 docs, 731 chunks
FTS5 spot-checks confirm substantive content landed:
- Bogart "binomial coefficient" → "CTGD Partitions and Stirling
Numbers" chapter, top hit
- Levin "modus ponens" → "Propositional Logic" chapter, top hit
That's the real lift signal we were after. Out-of-scope
follow-ups remain: PDF/TeX support for PG editions (Hilbert,
Boole) and full Aristotle Owen-translation depth (currently
~75% complete on Wikisource).
First make fetch-textbooks run revealed three URL issues that the
license-validator catches as policy-correct but the underlying
hosts return as 404:
- Keller-Trotter applied-combinatorics.org used a stale
/appcomb/sec_pre.html path; the canonical PreTeXt-generated
book lives at /book/app-comb-2.html.
- Open Data Structures uses /ods-cpp/ /ods-python/ /ods-java/
trailing-slash directory paths, not /ods-cpp.html (404). Three
language editions of the same content; ingest all three so the
multi-language structure stays intact.
- Hilbert Foundations of Geometry on Wikisource resolves to a
1906 Popular Science Monthly article ABOUT Hilbert's work, not
Hilbert's translated text. Project Gutenberg eBook #17384 is
PDF/TeX only — no clean HTML edition exists. Same status as
Boole #15114: kept the entry as a placeholder for license +
provenance documentation, urls intentionally empty until PDF
source support lands (out of scope per #000031).
Final fetch result: 7/7 manifested URLs ingested (Bogart,
Keller-Trotter front matter, Levin front matter, Aristotle Prior
Analytics, ODS C++, ODS Python, ODS Java) — 7 docs / 7 chunks /
86 edges / 8/8 Merkle proofs verify (verify samples 8 because
Aristotle yields multiple chunks).
Two textbooks (Hilbert + Boole) carry zero URLs; the helper
script's allow-list passes them through (license is PD;
license_url is set) but emits no URLs since their `urls` array
is empty. Documents this gap explicitly in each entry's notes
field so future operators see what awaits PDF source support.
Front-matter URLs alone yield minimal indexable content per
textbook (PreTeXt single-chapter scaffolds). To grow real
coverage: append more chapter URLs to a textbook's `urls`
array, OR use `make crawl-ingest URL=<home>` per the README's
"Going deeper" section.
A make-target scaffold for pulling public-domain and copyleft-
redistributable textbooks into a dedicated arborist shard via the
existing HtmlPageSource ingest pipeline. No new ingest machinery —
the existing path (robots.txt → noise-strip → 512-token chunk →
Merkle root → audit-event) IS the consistent process.
Manifest format
===============
bench/fixtures/textbooks/manifest-v1.jsonl — one JSON record per
textbook with explicit license tokens (PD / CC-BY / CC-BY-SA /
GFDL / OSI-approved). Fail-closed validation in
bench/scripts/textbooks_manifest.py refuses to emit URLs from
entries with missing or disallowed license tokens, so license
discipline surfaces at the URL-emit step rather than getting
silently buried in a fetch run.
Allow-list excludes CC-BY-NC (incompatible with arborist's
AGPLv3 distribution profile) and CC-BY-ND (no-derivatives
prevents chunking). Wilf's generatingfunctionology stays out
because its educational-use license forbids rehosting; citable
but not redistributable.
Initial entries (7 textbooks, 8 seed URLs)
==========================================
- Bogart, Combinatorics Through Guided Discovery — GFDL-1.3
- Keller & Trotter, Applied Combinatorics — CC-BY-SA-4.0
- Levin, Discrete Mathematics: An Open Introduction (3rd ed) —
CC-BY-SA-4.0 (4th ed switched to NC; pin 3rd)
- Hilbert, Foundations of Geometry (Townsend 1902) — PD via PG
- Boole, An Investigation of the Laws of Thought (1854) — PD
- Aristotle, Prior Analytics (Jenkinson) — PD via Wikisource
- Morin, Open Data Structures — CC-BY-2.5
Covers pillars I (logic) / II (set theory) / III (arithmetic) /
IV (geometry) / VII (combinatorics) on the claim-pack
(#000029) layout, plus a CS anchor for downstream domain
expansion. Each entry's pillar_targets field lists which
claim-pack pillars its records are candidate citations for.
Make targets
============
- textbooks-summary — license + URL counts per entry
- textbooks-urls — flat URL list to stdout
- fetch-textbooks — ingest all manifested URLs into
$(TEXTBOOK_DB) (default
~/.arborist/textbooks.db)
- textbooks-stats — documents / chunks / edges
- textbooks-verify — sample Merkle proof verification
To grow coverage of one textbook: append more chapter URLs to
its `urls` array. For deep-BFS of a textbook home: use the
existing `make crawl-ingest URL=<base> DEPTH=N` instead.
Smoke-tested end-to-end against Wikisource Prior Analytics:
1 doc / 1 chunk / 12 outbound edges / Merkle proof passes.
Shows the pipeline works; populating each book to depth needs
either more URLs in the manifest or the crawler.
Out of scope
============
- PDF processing. The Internet Archive hosts PD textbooks
(MacMahon's Combinatory Analysis 1915, Whitworth's Choice
and Chance 1867, the Motte 1729 Principia) as scanned PDFs;
a TextbookPdfSource with pdftotext / pypdf extraction is a
separate ticket — current scope is HTML-shaped sources.
- Mendelson + Enderton (proprietary; await #000031 §2.1
decision).
- Wilf generatingfunctionology (license forbids redistribution).
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.
Three streams. Two land in the repo; one lands in fox's Downloads
(existing g4 packs live there too).
Witness sweep automation
========================
`bench/scripts/witness_sweep_cron.sh` — schedulable harness that
runs `make bench-witness-sweep` + `make bench-witness-divergence`
back-to-back and (with --commit) auto-commits any new divergence
fixtures + sweep result. Fail-closed: pre-commit hook failure
aborts; non-main-branch refuses to commit.
$ bench/scripts/witness_sweep_cron.sh # dry run
$ bench/scripts/witness_sweep_cron.sh --commit # auto-commit
$ bench/scripts/witness_sweep_cron.sh --commit --push # full pipeline
Recommended cron (every 6 hours; LLM cost scales with frequency):
0 */6 * * * \
bench/scripts/witness_sweep_cron.sh --commit --branch main \
>> /var/log/arborist-witness.log 2>&1
Smoke this commit: dry-run produced 5 fresh divergences (10
cumulative across two extraction passes). The witness-sweep + 5F
extractor pipeline runs unattended now; calibration-data corpus
will grow over time.
#000018 — adversarial soft-hash covert-channel analysis
========================================================
`docs/soft-hash-channel-analysis.md` — formal threat model + channel-
capacity definition + cryptographic reduction + mitigation table
+ residual analysis. Doc-only deliverable per the ticket's hard
constraint.
Headline result: under threat models T1 (data poisoner) and T2
(gradient adversary), the channel is bounded by SHA-256 partial-
preimage hardness when φ (the anchor map) is independent of
parameter geometry. T3 (hyperparameter adversary) requires
M2 (per-checkpoint anchor nonce) for boundedness.
Recommended mitigation: M2 (per-checkpoint nonce) — 32 bytes added
to the snapshot manifest, no training-ergonomics regression,
closes T1+T2 channels under any φ choice and bounds T3 by
per-checkpoint window. Fall back to M1 (PRG-based φ) if M2-only
deployment surfaces structural concerns. M3 (drop anchor entirely)
stays in reserve as the strict-construction fallback.
Three open questions (§9): Hessian alignment under φ_linear,
PRG choice for φ_PRG, and explicit T3 per-window bound. Each is a
follow-up ticket.
Ticket #000018 status: closed · landed 2026-05-09 (analysis doc).
v7 § 9.10 spec amendment proposed in §7 of the analysis.
#000033 — pillar VII (combinatorics), Claude-authored
======================================================
NOT committed to the arborist repo (the existing g4-v2 packs live
in `/home/fox/Downloads/` too — that's the operator's bundle
location). Two new bundle files at:
/home/fox/Downloads/axiomsclaude-vii-v1.json (7 axioms)
/home/fox/Downloads/theoremsclaude-vii-v1.json (7 theorems)
Pillar VII covers combinatorial counting — the gap between Grok's
pillars VI and IX in the v2 packs:
axioms (7): addition principle · multiplication principle ·
pigeonhole principle · factorial definition ·
binomial coefficient definition · Pascal's rule ·
empty-set / boundary axiom
theorems (7): binomial theorem · inclusion-exclusion (counting
form) · hockey-stick identity · Vandermonde's
identity · Catalan number closed form · stars-and-
bars · strong pigeonhole
Each record in the dual-thread format the existing g4 packs use
(Δ symbolic LaTeX + ∇ verbose prose + ∇ concise + sigil + formal
language + role + status + source_reference + date + foundational
group + category + subfield). Per fox's directive: explicit
authorship metadata everywhere — `authored_by: Claude (Anthropic)
— model claude-opus-4-7`. NOT Grok-generated; no silent invention.
Each record carries `pi_star_ref: combinatorics@v1` so the kernel
binding is explicit. Theorems list `depends_on_axioms` arrays so
each theorem cites the foundation axioms it bottoms out on.
Smoke test (committed alongside):
$ arborist --db /tmp/test.db ingest --source claim_pack \\
--bundle /home/fox/Downloads/axiomsclaude-vii-v1.json \\
--bundle /home/fox/Downloads/theoremsclaude-vii-v1.json
→ 14 docs, 14 chunks, 0 cross-bundle edges
Source attributions: Stanley EC1, Brualdi Introductory
Combinatorics, Knuth TAOCP Vol 1, plus historical sources where
applicable (Pascal 1654, Vandermonde 1772, Dirichlet 1834, Catalan
1838, Feller 1950 for stars-and-bars).
Tests: 1636 passed, 37 skipped (no regressions; pillar VII
ingestion smoke covered above).
Apples-to-apples FTS5 search comparison on a single shard
(~/.arborist/shards/000.db, ~867 K Wikipedia surface docs)
before vs after ingesting the claim-pack source (#000029)
bundles.
Method: copy 000.db twice; ingest axiomsg4-v2.json +
theoremsg4-v2.json into one copy; run identical search queries
against both. FTS5-only path so retrieval-layer behavior is
isolated from QA pipeline reranking.
Results: 3/4 representative queries show claim-pack record in
top-3.
modus tollens → claim-pack at #3 (BM25 31.77)
law of excluded middle → claim-pack at #3 (related axiom
in same pillar)
associativity of addition → claim-pack at #1 — displaces
Wikipedia's general "Addition"
article entirely
Bayes theorem → no top-3 lift; Wikipedia "Bayes"
+ "Bayes rule" articles dominate
via short-doc BM25 bias
Storage tax: sub-MB. 78 chunks against 6.2M existing chunks is
below filesystem allocation granularity. Claim-pack rides
essentially for free on the existing Wikipedia substrate.
Honest verdict: claim-pack ingest earns its storage tax for
narrow technical queries where pre-distilled CORE-shape content
has title-token advantage. Doesn't help on queries Wikipedia
already covers with focused articles. The Bayes theorem case
likely shifts under the full QA pipeline's body-coverage sqrt
rerank (which counters BM25 short-doc bias) — that's a separate
larger bench worth running once the retrieval layer's other
stages are exercised.
Four-rung audit ladder still caps at ANCHOR-WARRANTED per
#000029's honest ceiling. Surface-ingest of cited textbooks
(#000031) is the path toward EVIDENCE-WARRANTED.
Three small streams:
#3 — close#000030 properly
============================
All 7 phases + Phase 1b landed across two commits (`04f3f5d`,
`abe5988`). Status header updated; ticket body now carries a phase
landing table with commit refs:
Phase 1 algebra-symbolic@v1 04f3f5d
Phase 1b algebra-symbolic-simplified@v1 04f3f5d
Phase 2 calculus-derivative@v1 04f3f5d
Phase 3 calculus-integral@v1 fox-direct
Phase 4 calculus-limit@v1 abe5988
Phase 5 calculus-series@v1 abe5988
Phase 6 linear-algebra@v1 abe5988
Phase 7 function-sampled@v1 abe5988
Plus tabular-pinned@v1 (last reserved stub) graduated in abe5988
closes the registry chapter — 15 concrete π*'s, no remaining
reserved stubs. Index updated.
#5 — composition fixtures across new SymPy π*'s
================================================
12 new tests in tests/test_pi_star_compositions.py covering pairs
that compose naturally:
- algebra-symbolic ∘ algebra-symbolic — idempotency check (running
expand twice equals expand once for any expression).
- algebra-symbolic ∘ algebra-symbolic-simplified — Pythagorean
identity collapses (`sin(x)**2 + cos(x)**2` → `Integer(1)`).
- Generic invariants: composition propagates PiStarError; manifest
fingerprint is order-sensitive; composite domain == inner domain;
composite bytes == manual chain bytes.
Test discipline: most compositions use `register_in_registry=False`
via a small `_safe_compose()` helper since the registry rejects
duplicate keys (#000015 invariant), so test ordering would
otherwise matter. Only the registration-test path uses real
compose().
#4 — end-to-end witness sweep against real shards + Hermes
===========================================================
New script `bench/scripts/witness_sweep.py`. Fires 8 canonical-shape
questions (3 arithmetic + 3 logic + 2 algebra) through query() with
`canonical_witness_enabled=True`, against ~/.arborist/shards (real
shard cluster) + the actual Hermes endpoint (NOT StubClient).
Records the agreement matrix per question to
bench/results/witness-sweep.json.
`make bench-witness-sweep` Makefile target. Honors
`ARBORIST_SHARDS_DIR`.
First real sweep (this commit, against Hermes-3-8B):
agreement label count rate
KERNEL-LLM-DIVERGED 5 62.5%
KERNEL-LLM-AGREE 3 37.5%
───────────────────────────────────────────
divergence_count 5 62.5%
wall median / max 130 ms / 1.1 s
Hermes diverged on 5/8 of the canonical-shape questions:
- said `1/10` for `0.1 + 0.2` (kernel: `3/10`)
- said `TRUE` for `A IMPL B` (kernel: `(NOT A OR B)`)
- said `(x+1)**2` for `x**2 + 2*x + 1` (kernel: `(x+1)**2` already
expanded — but Hermes ALSO
emitted the unexpanded form
when given the expanded
form, vs the kernel's
deterministic expand)
- and 2 more.
These are real LLM hallucinations on questions with closed-form
ground truth — exactly the calibration-data stream #000028
imagined. Pipeline validated end-to-end against actual hardware.
Pair: `make bench-witness-divergence` then extracts the 5
divergences as 5F-Falsification fixtures
(bench/fixtures/5f/falsification-witness-v1.jsonl, also committed).
Re-running the extractor produces byte-equal output (idempotency
contract from the extractor work).
Tests
=====
Full suite: 1636 passed, 37 skipped (was 1624; +12 composition
tests). The witness-sweep + extractor produce real artifacts now
committed under bench/results/ and bench/fixtures/5f/.
A new π* kernel that canonicalizes pure-integer counting
expressions and FAILS CLOSED on any input whose result isn't a
non-negative sp.Integer. Tighter domain than algebra-symbolic@v1,
which already accepts the same input surface but happily returns
symbolic / negative / non-integer outputs.
Distinguishing feature versus algebra-symbolic@v1:
algebra-symbolic@v1: binomial(n, k) → "binomial(n, k)" (symbolic
passthrough)
combinatorics@v1: binomial(n, k) → PiStarError (fail-closed
on free-symbol output)
algebra-symbolic@v1: binomial(Rational(1,2), 3) → 1/16 (rational)
combinatorics@v1: binomial(Rational(1,2), 3) → PiStarError
(output not Integer)
Boundary kept explicit: binomial(-3, 2) = 6 IS accepted because the
output is an integer 6. The fail-closed rule is on output shape
(Integer ≥ 0), not input range. Documented as
test_generalized_binomial_negative_args_accepted_when_integer.
Output format: plain decimal literal (b"10", b"5040"). Composes
with arithmetic@v1 for byte-identical agreement with the rational
route (b"10/1") so the multi-modality witness (#000028) can pin
equivalence-class agreement when both routes fire on the same
question.
Allowed surface (via SymPy primitives): binomial, factorial, ff /
rf (falling/rising), catalan, bell, partition, stirling, plus
arithmetic compositions over those primitives
(3*binomial(5,2) + factorial(4) = 54).
Coverage:
- 43 unit tests including binomial symmetry C(n,k)=C(n,n-k),
Pascal's rule C(n,k)=C(n-1,k-1)+C(n-1,k), the C(n,k) =
factorial(n)/(factorial(k)·factorial(n-k)) identity,
fail-closed paths (symbolic/negative/non-integer/relational/
parse), round-trip idempotence, composition with arithmetic@v1.
- 10 syntax + 12 semantics bench fixtures, 100% pass.
- bench/batteries/base.py PHASE_1_CARRIERS gains "combinatorics".
- Makefile bench-5s-combinatorics target.
All gate on pytest.importorskip("sympy") so a sympy-less suite
stays green. Full make test: 1537 passed / 28 skipped.
Sequencing rationale honored: this kernel lands FIRST so that
#000033 (claim-pack pillar VII for combinatorics) can bind its
records to the tighter integer kernel from day one — avoids
rebind churn on pi_star_ref fields.
Three small streams in one commit:
#000028 follow-up — witness divergence → 5F fixtures
=====================================================
Witness fan-out now writes a `providence_canonical_witness` audit
event when it fires (next to the capital-ledger record landed in
708aa45). Body carries pi_star_ref, question_text, agreement_label,
canonical_answer_text, llm_raw_text, llm_canonical_bytes,
cache_status. Best-effort write — chain failure never fails the
query.
New extractor `bench/scripts/witness_to_5f.py` reads those events
from a qa.db and writes them out as 5F-Falsification fixtures
matching the existing `falsification-live-v1` schema. Filtering
includes only divergence labels (LLM-DIVERGED / KERNEL-LLM-DIVERGED
/ CACHE-DRIFT); skips KERNEL-LLM-AGREE / STRICT-WITNESSED (no
calibration signal) and KERNEL-ONLY (LLM unparseable, not a
supervised-correction sample).
Idempotent: sorted by audit-event seq, so re-running against the
same qa.db produces byte-equal fixture files. The existing
fixture-digest discipline stays valid.
Makefile: `make bench-witness-divergence` (override default
qa.db / output path via WITNESS_QA_DB / WITNESS_OUT env-vars).
Closes the divergence → calibration data loop the witness ticket
imagined: every LLM hallucination on a canonical-shape question
becomes a supervised-correction fixture downstream prompt
improvements can grade against.
#000030 Phase 7 demo — function-sampled@v1 end-to-end
======================================================
`bench/scripts/demo_plot.py` — closes the loop on opencompletion's
activity24-math-plot.yaml. SymPy expression → quantized
integer-vector signature (canonical bytes) → optional matplotlib
PNG. Canonical bytes are the proof; PNG is just a downstream view
of the same evidence.
$ make demo-plot Q='sin(x)' PNG=/tmp/sin.png
Output JSON contains canonical_bytes_sha256 + canonical_bytes_preview
+ canonical_bytes_total_chars + grid metadata + the optional png_path.
matplotlib is gated — when absent, --png prints a warning to stderr
and skips the render; the canonical bytes still print. Tests skip
the PNG-presence assertion via `pytest.importorskip("matplotlib")`.
Public docs polish (#7)
========================
- docs/_source/bench.rst: updated fixture-count narrative (~660 →
662 default tasks + ~110 math π* fixtures); `make` quick-reference
now lists all per-π* 5S targets (tabular, calculus-limit/series,
linear-algebra, function-sampled) plus bench-real-shard,
bench-fork-baseline/score, bench-witness-divergence.
- docs/_source/v8-fork-score.rst: CLI section gained --out flag
documentation + a Make-harness sub-section covering
bench-fork-baseline / bench-fork-score / FORK_PARENT/CHILD/REPORT
env-vars.
Tests
=====
- tests/test_witness_to_5f.py — 8 new tests covering the audit-event
write (3) + extractor logic (5).
- tests/test_demo_plot.py — 6 new tests covering canonical-bytes
determinism + equivalence-class collapse + matplotlib gating.
Full suite: 1624 passed, 37 skipped (was 1568; +56).
tabular-pinned@v1 + calculus-limit@v1 + calculus-series@v1 +
linear-algebra@v1 + function-sampled@v1 — all reserved stubs
graduated; the π* registry is now 15 concrete kernels with no
remaining reserved-stub entries.
#000030 Phase 4 — calculus-limit@v1
====================================
sp.limit with thread-timeout. One-sided dir support (+/-/+-).
Pinned spelling for infinity cases: b"+oo" / b"-oo" / b"zoo"
(complex infinity) — bypasses sp.expand since Infinity isn't
algebraic. Finite results re-canonicalize through algebra-symbolic
recipe (sp.expand + sp.srepr). Unevaluated cases / timeouts emit
b"unevaluated:" + sp.srepr(<Limit>) sentinel, mirroring
calculus-integral's pattern.
#000030 Phase 5 — calculus-series@v1
=====================================
sp.series(f, x, x0, n).removeO() → sp.expand → sp.srepr. Drops
O(x**n) remainder explicitly so the canonical form is finite-byte.
Sentinel format mirrors limit/integral: b"unevaluated:Series(...)"
on timeout. n must be a positive int; 0 / float / negative rejected.
#000030 Phase 6 — linear-algebra@v1
====================================
Single π* covers the whole linear-algebra surface via {op, matrix}
JSON. Ops: rref / det / eigenvalues / inverse. Matrix cells go
through Fraction(Decimal(str(...))) for floats so 1, 1.0, "1.0"
all collapse to Rational(1, 1) — matching arithmetic@v1's
discipline. Without this fold, sp.sympify keeps floats as Float
(separate type) and downstream det/inverse return Float-shaped
bytes. Eigenvalues are sorted by srepr for determinism.
Output formats:
rref / inverse: rows/cols header + cells joined by | (rows by ||)
det: det:<num/den-or-srepr>
eigenvalues: eigenvalues:<value-1>x<mult-1>|...
#000030 Phase 7 — function-sampled@v1
======================================
Bridge to time-series-quantized@v1. SymPy expression + linspace
grid → quantized integer-vector signature in time-series's exact
output format (dt=...;dv=...;n=...;t0=0:v0|v1|...). Two functions
that render identically (within sample-grid tolerance) collapse
to the same canonical bytes. This is what plotting CAN become
in π* terms — the PNG render is a downstream view of the same
canonical evidence.
Math-only sampler (no numpy in the dep surface); Python's round()
is banker's-rounding so the bytes are interchangeable with
time-series-quantized@v1's output. Complex / non-finite samples
raise PiStarError rather than silently dropping imaginary parts.
tabular-pinned@v1 — last reserved stub graduates
=================================================
JSON-rows input ({schema, key_columns, rows}); declared
key_columns sort policy (stable sort by primary-key tuple);
type-fold per column (int/rational/bool through arithmetic@v1
discipline; str verbatim; bool normalized). Header case is
PINNED EXACT — Excel and PostgreSQL both care about case;
defaulting to lowercase-fold would break operator expectations.
Output: header (schema + key + n) + rows joined by \n + cells by |.
The π* registry has no remaining reserved stubs. Every modality
the substrate paper reserved is now real.
Test suite: 1568 passed (was 1467; +101). New closure-criterion
test (test_no_stub_pi_stars_remain) replaces the old reserved-stub
parametrize — adding a future stub re-opens this list.
110/110 fixtures pass across the 5 new bench-5s-* targets.
PHASE_1_CARRIERS gained calculus / linear-algebra / function-sampled
/ tabular.
Three small streams in one commit; each closes / expands a
recently-landed ticket without changing its hard contract.
#000026 Phase 3 wiring — authorship warrant ladder visible
============================================================
Phase 3 sidecar (arborist/qa/warrant_authorship.py landed in 60b5748)
exposed the classifier but didn't surface it. Two wirings:
- arborist/qa/inspect.py — diagnose_authorship_warrant runs against
the cached row's question + answer + per-source raw chunks +
URIs + titles; result lands as `authorship` field alongside the
other sidecars.
- arborist/cli.py _render_warrant_tail — appends ` · warrant:
<readable-tier>` when result['authorship'] is populated with a
non-quiet tier. AUTHOR_COPYRIGHT_FOOTER → "copyright-footer", etc.
NO_AUTHORSHIP_SIGNAL stays silent. Backward-compat: results
without an `authorship` key render unchanged.
Tests: 3 inspect-path tests (no-signal, copyright-footer,
repository-owner) + 4 render-tail tests (presence, no-signal
silence, missing-key silence, all-six-tiers readable mapping).
#000028 follow-ups — capital ledger + sample-rate
==================================================
Two policy fields layered on top of canonical_witness_enabled:
- canonical_witness_sample_rate (0.0..1.0; default 1.0). Operators
wanting passive calibration set 0.05 to fire witness on 5% of
canonical questions while paying 5% of LLM cost. 0.0 effectively
off; 1.0 = current always-on behavior. Gating uses random.random()
so distribution is uniform; clamped to [0, 1].
- Capital ledger row written for each FIRED witness (not skipped
ones). op_type='canonical_witness'; estimator inputs include
prompt_chars + answer_chars + llm_seconds + agreement_label +
pi_star_ref. Best-effort: ledger-write failure must never fail
the query (sidecar discipline).
Tests: 4 new — sample_rate=0.0 skips (no LLM call, no ledger row);
sample_rate=1.0 always fires; capital_ledger row written under
op_type='canonical_witness' with full input blob; sampled-out
witness records zero ledger rows.
Both fields fold into governance_policy_hash naturally via the
existing policy-hash machinery — flipping witness mode invalidates
prior records as expected.
#000025 Phase 1d — 5F fixture catalog 30 → 50
==============================================
Both synthetic and live sides of all 5 sub-batteries expanded
30 → 50 (+200 fixtures total: 5 × 20 synthetic, 5 × 20 live).
function — claim_count cycles 2..7 across new fixtures
falsification — 10-violation palette across new ids
feedback-loop — fact-N learning chains
finetuning — capability transitions across canonical π*
(math/logic/algebra/calculus pool)
formulate — multi-pointer claim shapes
500/500 pass through respective runners. test_session_integration
total bumped 562 → 662. Pinned test_5f_*_runs counts updated 30 →
50 (synthetic main + embedded + live).
Tests
=====
Full suite: 1467 passed, 36 skipped (was 1388; +79 across warrant
render + witness sample/ledger + 5F implicit coverage).
Two new π* canonicalizers extend the math substrate above
arithmetic@v1 (closed-form rationals) and logic-kernel@v1
(propositional Boolean → CNF):
algebra-symbolic@v1 (Phase 1) — symbolic-algebra domain.
sp.expand → sp.srepr canonical bytes. Polynomial identity collapses
((x+1)**2 ≡ x**2 + 2*x + 1); exponential identity collapses
(exp(a+b) ≡ exp(a)*exp(b), inherited from sp.expand's default
behavior); trigonometric identity does NOT collapse
(sin²+cos² ≢ 1). The trig surface is reserved for a future
algebra-symbolic-simplified@v1 variant that wraps sp.simplify at
unbounded CPU cost. Rejects relationals (`x > 0`) and
BooleanFunction shapes (`x & y`) via `isinstance(expr, sp.Expr)` —
sp.Symbol confusingly inherits from Boolean so the right rejection
filter is "not Expr" rather than "Boolean".
calculus-derivative@v1 (Phase 2) — calculus domain. JSON-shaped
{f, x, n} input → sp.diff → sp.expand → srepr bytes. Output is
itself a valid algebra-symbolic@v1 input so the two compose
naturally under arborist.pi_star.compose. n defaults to 1; bools
explicitly rejected (Python isinstance(True, int) is True so we
filter that explicitly).
Optional dependency: sympy ships in the new [math] extra
(pyproject.toml). Folded into [dev] so make bootstrap pulls it
transitively. An explicit `bootstrap-math` Makefile target documents
the opt-in for minimal-install users. Both modules self-guard
via `try: import sympy as sp / except ImportError: sp = None` and
only register(...) when sympy is present, so a fresh checkout
without [math] still loads arborist.pi_star without raising.
Preflight algebra route lands in
arborist.qa.query._canonical_projection_preflight between the
arithmetic and logic routes. Charset regex (_CANONICAL_ALGEBRA_RE)
allows lowercase letters + math chars; requires at least one
letter (else arithmetic wins); rejects natural-language leading
verbs via _CANONICAL_ALGEBRA_NL_LEAD_RE (4-letter minimum so
single-/two-/three-char identifiers like x, xy, sin, cos, pi
survive while "simplify (...)", "factor x...", "expand (a+b)..."
fall through). PiStarError + KeyError both fall through cleanly
so a sympy-less install just routes everything past algebra.
Bench substrate:
- bench/batteries/base.py PHASE_1_CARRIERS gains "symbolic_algebra"
- bench/fixtures/5s/syntax-algebra-symbolic-v1.jsonl (10 fixtures)
- bench/fixtures/5s/semantics-algebra-symbolic-v1.jsonl (13 fixtures
including the documented trig non-collapse + exp collapse)
- Makefile bench-5s-algebra target → 100% pass
Tests: 18 algebra-symbolic + 38 calculus-derivative unit tests +
~10 new preflight-route tests in test_canonical_projection.py. All
gate on pytest.importorskip("sympy") so a sympy-less suite stays
green. Full suite: 1369 passed / 27 skipped.
Phases 3-7 (integral, limit, series, linear-algebra,
function-sampled) remain open as future work; each lands as its
own ticket when an actual consumer surfaces.
