axis/documents/db_guide.md

⸻

VERANTYX Database Construction & Extension Guide

Building, Expanding, and Auditing rules.json

⸻

0. What “the Database” Means in VERANTYX

In VERANTYX, the database is not storage. It is the reasoning substrate. • Code executes rules • Rules encode knowledge • The database defines what the system can and cannot reason about

Therefore:

Expanding the DB expands capability without increasing noise.

⸻

1. DB Construction Principles (Non-Negotiable) 1. Explicit scope beats coverage Narrow rules are better than broad ones. 2. Gated entry Every rule must have strict requires. 3. Refutation > Proof Counterexamples must dominate optimistic claims. 4. Auditability over cleverness If you can’t explain why a rule fired, don’t add it. 5. Deletion is success A good DB allows safe removal.

⸻

2. Initial DB Design (v0 Strategy)

2.1 Start with Axioms, Not Results

Prefer: • Modal axioms (T / 4 / 5) • Structural facts (n<k ⇒ πₙ(Sᵏ)=0)

Avoid initially: • Long theorems • High-level classifications • Meta statements (“in general”, “it is known that”)

2.2 Encode What Breaks First

Add counterexamples early: • “always”, “all”, “for any” • vacuity traps • missing-assumption failures

This prevents false confidence from day one.

⸻

3. Recommended DB Growth Order
   1. Core axioms / invariants
   2. Counterexamples for overgeneralization
   3. Necessity rules for exactness
   4. Language normalization helpers
   5. Domain expansion (new fields)

Never skip directly to step 4 or 5.

⸻

4. Adding a New Rule: Safe Extension Workflow

Step 1 — Identify the gap

Ask: • Did Phase 1 return “insufficient evidence”? • Was the failure correct?

Only proceed if the failure is legitimate knowledge absence.

⸻

Step 2 — Decide rule type

Goal Rule Type Support a valid claim theorem Kill a bad claim counter_example Enforce necessity necessity_counterexample

Never mix purposes.

⸻

Step 3 — Define requires FIRST

Before writing entails: • List the minimum assumptions • Encode them as atomic props

If you can’t list assumptions → do not add the rule.

⸻

Step 4 — Choose matching strategy • Use entails if formula is fixed • Use match_all only if unavoidable • Keep tokens minimal

⸻

Step 5 — Assign evidence weight

Guideline: • If a counterexample exists → weight ≤ -8 • If necessity is involved → weight ≤ -10

⸻

Step 6 — Dry-run mentally

Ask: • Could this fire in an unrelated problem? • Would I regret this rule in 6 months?

If yes → narrow it.

⸻

5. Adding a New Domain (Domain Expansion)

5.1 Domain Onboarding Checklist

Before adding a new domain: • Define canonical notation • Add normalization rules • Add at least one counterexample

Never add a domain with proofs only.

⸻

5.2 Minimal Domain Starter Pack

For any new domain, aim for: • 2–3 core theorems • 2 strong counterexamples • 1 necessity rule (if applicable)

This prevents “optimistic-only” reasoning.

⸻

6. LLM Mining Integration (DB-Safe Use)

Mining output must: • Be reviewed manually • Enter DB only after rewrite • Never be copied verbatim

Recommended pipeline:

LLM mining → provisional rule → human rewrite → DB entry

Mining discovers candidates, not truth.

⸻

7. Versioning & Review Policy

7.1 Rule Stability Levels (Recommended) • experimental (new, unstable) • stable (used across problems) • legacy (kept for backward audit)

Use comments or metadata to mark status.

⸻

7.2 Review Questions Before Merge • Is requires minimal and sufficient? • Is there a matching counterexample? • Can this rule be abused by match_all? • Does it reduce or increase ambiguity?

⸻

8. When NOT to Add to the DB

Do not add rules when: • The issue is parsing/decomposition • The issue is language normalization • The issue is scoring heuristics • The issue is UI or presentation

DB is not a fix-all.

⸻

9. DB Health Indicators

A healthy DB: • Produces many “insufficient evidence” results • Rejects more than it accepts • Grows slowly • Can be partially deleted safely

If everything becomes solvable → you introduced noise.

⸻

Closing Note (English)

A VERANTYX database should feel: • Conservative • Skeptical • Occasionally frustrating

That frustration is the sound of noise being blocked.

⸻

⸻

VERANTYX DB 構築・追加ガイド

rules.json の設計・拡張・監査

⸻

0. VERANTYX における「DB」とは

VERANTYX の DB は保存庫ではありません。 推論そのものです。 • コードは実行するだけ • ルールが知識 • DB が「考えられる範囲」を決める

つまり：

DB を増やすこと＝能力拡張（ノイズなし）

⸻

1. DB 構築の原則（絶対条件）
   1. 広さより明示性
   2. requires による厳密な入場制限
   3. 反例は証明より強い
   4. 監査できない賢さは不要
   5. 消せることが正義

⸻

2. 初期 DB 設計（v0 戦略）

2.1 結果より公理

最初は： • 公理（T/4/5） • 構造的不変量

から始める。

⸻

2.2 まず壊れるものを書く • 「常に」 • 「すべて」 • 空虚真理

を潰す反例を最優先で入れる。

⸻

3. DB 成長の正しい順序
   1. 基本公理
   2. 過剰一般化の反例
   3. 必要条件（Exactness）
   4. 記法・言語補助
   5. 新分野

⸻

4. ルール追加の安全フロー

Step 1 — 本当に知識不足か？ • Phase 1 の失敗は正しいか？ • それとも仕様の問題か？

⸻

Step 2 — 種類を決める

目的 種類 支持 theorem 否定 counter_example 必要条件 necessity_counterexample

⸻

Step 3 — requires を先に書く

仮定が書けないルールは 禁止。

⸻

Step 4 — マッチ方式選択 • 固定式 → entails • 言語依存 → match_all（最小限）

⸻

Step 5 — 重み設定 • 反例は強く • 必要条件は必ず -10 以上

⸻

5. 新分野追加の作法

最低セット • 証明 2–3 • 強反例 2 • 必要条件 1

証明だけの分野は禁止。

⸻

6. 採掘（LLM）の扱い • 直接 DB に入れない • 人が書き直す • provenance を残す

⸻

7. レビュー指針 • requires は十分に狭いか • 反例は存在するか • 悪用できないか • 消しても壊れないか

⸻

8. DB に入れてはいけないもの • 分解失敗の補正 • 正規化漏れ • UI 問題 • スコア調整

⸻

9. 健全な DB の兆候 • 証拠不足が多い • 否定が強い • 成長が遅い • 部分削除できる

全部解けるなら危険信号。

⸻

終わりに（日本語）

VERANTYX の DB は • 保守的で • 疑い深く • 不親切

であるべきです。

それはノイズが遮断されている証拠です。