From d34ecb27c1b0570b99d67d148e82502395a3f526 Mon Sep 17 00:00:00 2001 From: "russell@unturf.com" Date: Sat, 9 May 2026 12:59:29 -0400 Subject: [PATCH] =?UTF-8?q?docs/tickets:=20open=20#000032=20(combinatorics?= =?UTF-8?q?@v1=20=CF=80*)=20+=20#000033=20(pillar=20VII)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two design-only tickets opened together because they're tightly coupled — pillar VII records bind to combinatorics@v1 via pi_star_ref, and #000032 lands first to avoid rebind churn on that field. #000032 — combinatorics@v1 π* ============================= A new π* kernel that canonicalizes pure-integer counting expressions (binomial, factorial, permutations, partitions, Catalan, Bell, Stirling) and FAILS CLOSED on any input whose result is not a non-negative integer. Tighter domain than algebra-symbolic@v1, which already accepts the same input surface but happily returns symbolic / negative / rational outputs. Distinguishing feature: algebra-symbolic@v1 returns binomial(n,k) → "binomial(n,k)" (symbolic), binomial(-3,2) → 6 (generalized). combinatorics@v1 rejects both. Operators choose the kernel by what they want rejected. Output format: integer string (b"10"). Compose with arithmetic@v1 to get bytes-identical agreement (b"10/1") for the multi-modality witness flow. Estimated size: ~120 LOC module + ~80 LOC tests + ~22 fixtures. Single-commit feasible. #000033 — Claim-pack pillar VII (combinatorics) ================================================ Extend the claim-pack source (#000029) with a new combinatorics pillar slotting into the documented gap (existing v2 bundles use I, II, III, IV, V, VI, IX — VII and VIII reserved for extension). Counting axioms (Pascal's rule, addition principle, multiplication principle, pigeonhole, factorial / binomial definitions) + classical theorems (binomial theorem, inclusion-exclusion in counting form, hockey-stick, Vandermonde, Catalan closed form, stars-and-bars). Bundle provenance is the open question — three options documented: A. Commission a Grok-4 v3 bundle for parity with the existing pack. B. Hand-curate from textbooks (Stanley, Brualdi, Wilf, Knuth). C. Hybrid — LLM draft + human curation. Hard constraint: explicit authorship metadata. No silent invention. Bundle landing is a config + data exercise; no source-code changes to arborist/sources/claim_pack.py needed since the source already iterates arbitrary pillar names. Sequencing: #000032 first (kernel), #000033 next (records bind to it from day one), #000031 stays parallel-track (textbook ingest for warrant promotion). Both tickets stay open · awaiting go/no-go pending fox's implementation green-light. --- docs/TICKETS.md | 4 +- .../ticket-000032-combinatorics-pi-star.md | 349 +++++++++++++++++ ...033-claim-pack-pillar-vii-combinatorics.md | 359 ++++++++++++++++++ 3 files changed, 711 insertions(+), 1 deletion(-) create mode 100644 docs/tickets/ticket-000032-combinatorics-pi-star.md create mode 100644 docs/tickets/ticket-000033-claim-pack-pillar-vii-combinatorics.md diff --git a/docs/TICKETS.md b/docs/TICKETS.md index 62f4707..6520c02 100644 --- a/docs/TICKETS.md +++ b/docs/TICKETS.md @@ -61,6 +61,8 @@ Newest first. Update on every open/close. | ID | Title | Status | Opened | Directive | |----------|------------------------------------------------|-----------------------|------------|-----------| +| #000033 | Claim-pack pillar VII (combinatorics) | open · awaiting go/no-go | 2026-05-09 | — | +| #000032 | combinatorics@v1 π* (integer counting kernel) | open · awaiting go/no-go | 2026-05-09 | — | | #000031 | Surface-ingest cited textbooks for claim-pack warrant promotion | open · awaiting go/no-go | 2026-05-09 | — | | #000030 | Math π* expansion: SymPy substrate (algebra · calculus · linalg) | closed · Phases 1+2+1b+3 landed 2026-05-09 (4-7 future work) | 2026-05-09 | — | | #000029 | Claim-pack source (axiom/theorem JSON bundles) | closed · landed 2026-05-09 | 2026-05-09 | — | @@ -95,4 +97,4 @@ Newest first. Update on every open/close. ## Next ID -`000032` +`000034` diff --git a/docs/tickets/ticket-000032-combinatorics-pi-star.md b/docs/tickets/ticket-000032-combinatorics-pi-star.md new file mode 100644 index 0000000..d15f916 --- /dev/null +++ b/docs/tickets/ticket-000032-combinatorics-pi-star.md @@ -0,0 +1,349 @@ +# Ticket #000032 — combinatorics@v1 π* + +**Status:** open · awaiting go/no-go +**Opened:** 2026-05-09 +**Scope:** A new π* kernel that canonicalizes pure-integer +counting expressions — binomials, factorials, permutations, +partitions, Catalan, Bell, Stirling numbers — and **fails closed +on any input whose result is not a non-negative integer**. Tighter +domain than `algebra-symbolic@v1` (which already accepts the same +input surface but happily returns symbolic / negative / rational +results). +**Audience:** maintainers of arborist's π* layer + downstream +consumers (canonical-projection witness, math/logic preflight, +benchmark batteries, claim-pack pillar VII if #000033 lands). +**Hard constraint:** **fail-closed integer discipline.** Any input +whose canonical SymPy reduction is not a `sp.Integer ≥ 0` raises +`PiStarError`. This is the distinguishing feature versus +`algebra-symbolic@v1`. Operators choose the kernel by what they +want rejected, not by what they want accepted. + +--- + +## 1. Problem statement + +Today, combinatorial primitives (`binomial(5, 2)`, `factorial(7)`, +`catalan(5)`, etc.) already canonicalize through +`algebra-symbolic@v1` because SymPy understands them as +expressions. Confirmed in #000030 Phase 1+2 commit: + +``` +binomial(5,2) → Integer(10) +factorial(7) → Integer(5040) +3*binomial(5,2) + factorial(4) → Integer(54) +binomial(n,k) → binomial(Symbol('n'), Symbol('k')) ← symbolic +binomial(-3, 2) → Integer(6) ← negative-arg accepted +``` + +This works — but it accepts inputs that combinatorial-counting +semantics should reject: + +1. **Symbolic results** (`binomial(n,k)`) — counting only makes + sense once n,k are bound to concrete non-negative integers. + `algebra-symbolic@v1` returns the symbolic form unchanged, + which silently moves "the question is unanswerable" into + "the answer is this opaque expression." That's a false + confidence the witness flow can't catch without a separate + integer assertion. +2. **Generalized binomials** (`binomial(-3, 2) = 6`, + `binomial(0.5, 3) = 0.0625`) — SymPy's combinatorial + functions extend to negative integers, rationals, and complex + numbers via the Gamma function. The CLASSICAL counting + interpretation rejects all of these. A counting kernel + should fail closed. +3. **Composability with `arithmetic@v1`.** The output bytes of + `algebra-symbolic@v1` are `srepr(Integer(10))`. The output + bytes of `arithmetic@v1` are `b"10/1"`. Two callers asking + "how many ways to choose 2 from 5?" via different routes get + different canonical bytes for the same answer. A + combinatorics kernel that emits `b"10"` (or `arithmetic@v1`- + compatible `b"10/1"`) closes that discrepancy. + +The witness flow (#000028) becomes more useful when modalities +agree on the SHAPE of the answer. STRICT-WITNESSED for "how many +ways to choose 2 from 5" should not depend on which kernel the +preflight happened to dispatch to. + +## 2. Design choices + +### 2.1 Output format + +**A. Integer string (RECOMMENDED).** ``b"10"``, ``b"5040"``. +Compact, human-readable, and `arithmetic@v1`'s +``"/"`` recipe accepts it as ``10/1`` after one +re-canonicalization. Cross-modality agreement with +`arithmetic@v1` is one canonicalization step away — the +multi-modality witness can pin them as the same equivalence +class via composition. + +**B. SymPy srepr integer.** ``b"Integer(10)"``. Matches the +algebra-symbolic@v1 fast-path output. Less readable; requires +SymPy to re-parse for any downstream comparison. Loses the +"witness can pin equivalence with arithmetic@v1" argument. + +**C. Rational form.** ``b"10/1"`` via the existing +`arithmetic@v1` recipe. Bytes-identical to what +`arithmetic@v1` would output. Cleanest cross-kernel +agreement. Costs a denominator on every output (visual +clutter for pure counts). + +→ **A.** Compact, distinguishes counting outputs from rational +arithmetic at the byte level (`b"10"` vs `b"10/1"`), +canonicalizes round-trip-cleanly through `arithmetic@v1` if +operators want bytes-identical agreement. + +### 2.2 Allowed input surface + +Same parser as `algebra-symbolic@v1` (SymPy `sympify`); the +domain narrowing happens at the OUTPUT stage. Inputs that the +parser accepts but the kernel rejects: + +- Result is symbolic (any free symbols remain): reject. +- Result is non-integer: reject. +- Result is negative integer: reject (counting-domain rule; + generalized binomial doesn't qualify). + +Inputs the parser already rejects (PiStarError from sympify, +syntax error, relational/boolean): reject same as +`algebra-symbolic@v1`. + +### 2.3 Composition + +`combinatorics@v1` outputs bytes that look like a non-negative +integer. The natural composition target is `arithmetic@v1`: + +```python +from arborist.pi_star import compose +# combinatorics@v1 output "10" → arithmetic@v1 reads as 10 → "10/1" +chain = compose("combinatorics@v1", "arithmetic@v1") +chain.canonicalize(b"binomial(5,2)") == b"10/1" +``` + +Auto-registers as `combinatorics-then-arithmetic@v1` per the +existing composition algebra. The witness flow can use this +composition to pin equivalence-class agreement between +combinatorial and rational answers. + +### 2.4 Preflight routing + +Algebra route already accepts inputs like `binomial(5,2)` and +returns `Integer(10)`. Adding a combinatorics route ahead of +algebra would require a sniff that distinguishes counting +expressions (`binomial`, `factorial`, …) from general algebra. +Two options: + +**A. Don't wire to preflight.** Let `algebra-symbolic@v1` keep +catching combinatorial inputs at the preflight layer. Operators +who want the tighter integer discipline call +`combinatorics@v1` directly (or via composition). This preserves +the existing preflight order; no new sniff complexity. + +**B. Add a combinatorics sniff.** Detect known combinatorial +function names (`binomial`, `factorial`, `catalan`, `bell`, +`partition`, `stirling`) at the start of the input and route +accordingly. Adds a new regex + branch. + +→ **A.** Keep preflight simple. The kernel exists to enforce +discipline at call sites that want it; the preflight layer +already works for the question-shape case via algebra. + +### 2.5 Allowed function set + +SymPy combinatorial primitives that produce non-negative integer +outputs on integer inputs: + +| Name (SymPy) | Input | Output | +|---------------------------------------------------|--------------------|--------| +| ``sp.binomial(n, k)`` | n, k integers ≥ 0 | C(n, k), 0 if k > n | +| ``sp.factorial(n)`` | n integer ≥ 0 | n! | +| ``sp.ff(x, k)`` (falling factorial) | x, k integers ≥ 0 | x·(x-1)…(x-k+1) | +| ``sp.rf(x, k)`` (rising factorial / Pochhammer) | x, k integers ≥ 0 | x·(x+1)…(x+k-1) | +| ``sp.catalan(n)`` | n integer ≥ 0 | n-th Catalan | +| ``sp.bell(n)`` | n integer ≥ 0 | n-th Bell | +| ``sp.functions.combinatorial.numbers.partition(n)`` | n integer ≥ 0 | p(n) | +| ``sp.functions.combinatorial.numbers.stirling(n, k)`` | n, k integers ≥ 0 | S2(n, k) | + +These are all addressable by name through SymPy's standard +parser; users write `binomial(5,2)`, `partition(7)` etc. directly. +Operators with arithmetic compositions (e.g. +`3*binomial(5,2) + factorial(4)`) get a single integer output, +54 in this case. + +## 3. Recommendation + +Implement Phase 1 + Phase 2 together as one commit: + +- **Phase 1** — `arborist/pi_star/combinatorics.py` with the + `CombinatoricsV1` class, integer-only output discipline, and + registration. ~120 LOC. +- **Phase 2** — Tests covering integer-output cases (collapse), + symbolic rejection, negative rejection, generalized-binomial + rejection, composition with `arithmetic@v1`. Bench fixtures + pair (syntax + semantics). ~80 LOC tests + ~12 fixtures. + +## 4. Implementation sketch + +### 4.1 New file: `arborist/pi_star/combinatorics.py` + +```python +try: + import sympy as sp +except ImportError: + sp = None + + +@dataclass +class CombinatoricsV1: + name: str = "combinatorics" + version: str = "v1" + domain: str = "combinatorics" + + def canonicalize(self, raw: bytes) -> bytes: + if sp is None: + raise PiStarError("requires sympy; pip install 'arborist[math]'") + # ... bytes/UTF-8/empty checks (mirror algebra_symbolic.py) ... + try: + expr = sp.sympify(text) + except (sp.SympifyError, SyntaxError, TypeError) as exc: + raise PiStarError(f"cannot parse {text!r}: {exc}") from exc + if not isinstance(expr, sp.Expr): + raise PiStarError(f"rejects non-expression {text!r}") + # Reduce — sp.simplify on combinatorial primitives evaluates + # them to integer literals (or leaves them symbolic). + try: + reduced = sp.simplify(expr) + except (TypeError, ValueError) as exc: + raise PiStarError(f"simplify failed: {exc}") from exc + # Domain check: must be a non-negative concrete integer. + if not isinstance(reduced, sp.Integer): + raise PiStarError( + f"combinatorics@v1 result is not a concrete integer: " + f"{reduced!r}" + ) + if reduced < 0: + raise PiStarError( + f"combinatorics@v1 result is negative: {int(reduced)}" + ) + return str(int(reduced)).encode("utf-8") + + +if sp is not None: + register(CombinatoricsV1()) +``` + +### 4.2 Tests (`tests/test_pi_star_combinatorics.py`) + +```python +sympy = pytest.importorskip("sympy") + +def test_basic_counts(ps): + assert ps.canonicalize(b"binomial(5,2)") == b"10" + assert ps.canonicalize(b"factorial(7)") == b"5040" + assert ps.canonicalize(b"catalan(5)") == b"42" + assert ps.canonicalize(b"bell(5)") == b"52" + assert ps.canonicalize(b"partition(7)") == b"15" + +def test_arithmetic_composition_inside_input(ps): + # Mixing counting + arithmetic still must reduce to integer. + assert ps.canonicalize(b"3*binomial(5,2) + factorial(4)") == b"54" + +def test_symbolic_input_rejected(ps): + with pytest.raises(PiStarError, match="not a concrete integer"): + ps.canonicalize(b"binomial(n, k)") + +def test_negative_result_rejected(ps): + # Hand-crafted: 5 - factorial(4) = -19 → counting domain rejects. + with pytest.raises(PiStarError, match="negative"): + ps.canonicalize(b"5 - factorial(4)") + +def test_non_integer_result_rejected(ps): + # Generalized binomial(0.5, 3) = 0.0625 — SymPy supports it, + # combinatorics@v1 rejects. + with pytest.raises(PiStarError, match="not a concrete integer"): + ps.canonicalize(b"binomial(Rational(1,2), 3)") + +def test_composes_with_arithmetic(ps): + from arborist.pi_star import compose + chain = compose("combinatorics@v1", "arithmetic@v1") + assert chain.canonicalize(b"binomial(5, 2)") == b"10/1" +``` + +### 4.3 Bench fixtures + +`bench/fixtures/5s/syntax-combinatorics-v1.jsonl` — +10 inputs that produce non-negative integers (parse-pass). + +`bench/fixtures/5s/semantics-combinatorics-v1.jsonl` — +12 equivalence-class fixtures: + +- `binomial(5, 2)` ≡ `10` +- `binomial(5, 3)` ≡ `binomial(5, 2)` (symmetry) +- `factorial(0)` ≡ `1` +- `binomial(7, 0)` ≡ `binomial(7, 7)` ≡ `1` +- distinct: `factorial(5)` ≢ `factorial(6)`, etc. + +### 4.4 Carrier whitelist + Makefile + +`bench/batteries/base.py PHASE_1_CARRIERS` gains +`"combinatorics"`. `Makefile` gains `bench-5s-combinatorics`. + +## 5. Hard constraints (re-stated) + +1. **Fail-closed integer discipline.** Any input whose reduction + is not a non-negative `sp.Integer` raises `PiStarError`. No + silently-symbolic outputs. No negative-counting outputs. No + rational/float outputs. +2. **Optional dependency.** Same pattern as `algebra-symbolic@v1`: + `try/except` import, register only when sympy is present, tests + gate on `pytest.importorskip("sympy")`. +3. **No cache_key invariant changes.** Schema, chunker, + canonicalization versions stay pinned. New π* registers a new + key (`combinatorics@v1`); existing cache rows unaffected. +4. **No preflight wiring.** The kernel is direct-call; the + preflight algebra route already catches counting-shaped inputs + without a sniff change. + +## 6. Risks / things to watch + +- **`sp.simplify` cost.** Same risk as + `algebra-symbolic-simplified@v1`: pathological inputs can grow + exponentially. Combinatorial primitives are usually fast (≤ 10 + ms even for `partition(1000)`), but composition with + `algebra-symbolic` shapes can hit the slow path. No in-π* + timeout in v1 (matches Phase 1b); operators size budget at + call sites. +- **`stirling(n, k)` ambiguity.** SymPy distinguishes Stirling + numbers of the first vs second kind via a kwarg + (`stirling(n, k, kind=1)`). The default is second kind. Document + in module docstring; fixtures pin the kind explicitly. +- **`partition` namespace.** `sp.partition` exists at + `sp.functions.combinatorial.numbers.partition` but NOT on the + top-level `sp.` namespace as a standalone callable in some + SymPy versions. Verify `sympify("partition(7)")` resolves + consistently across SymPy ≥ 1.13; fall back to the longer + `sp.functions...` path inside the parser's `local_dict` if + needed. +- **Catalan-number test fragility.** Some SymPy versions return + `catalan(5) → 42` directly; older versions might return an + unevaluated `catalan(5)` Function call. Pin the version + expectation in `[math]` extra (`sympy>=1.13`). + +## 7. Forward links + +- **#000030** — Math π* expansion (SymPy substrate). This ticket + is its sibling, narrower-domain. +- **#000033** — Claim-pack pillar VII (combinatorics). If both + land, the pillar's records cite this kernel as its formal + projection (analogous to how Phase III arithmetic theorems + cite `arithmetic@v1`). +- **#000028** — Multi-modality witness. Combinatorial questions + become STRICT-WITNESSED-eligible once the kernel + the algebra + preflight produce equivalent canonical forms via composition. + +## 8. Status + +Open · awaiting go/no-go. + +Estimated size: ~120 LOC module + ~80 LOC tests + ~22 fixtures + +~5 LOC carrier-whitelist + ~5 LOC Makefile. Single-commit feasible +alongside #000033 if both land together; otherwise standalone. diff --git a/docs/tickets/ticket-000033-claim-pack-pillar-vii-combinatorics.md b/docs/tickets/ticket-000033-claim-pack-pillar-vii-combinatorics.md new file mode 100644 index 0000000..2bad871 --- /dev/null +++ b/docs/tickets/ticket-000033-claim-pack-pillar-vii-combinatorics.md @@ -0,0 +1,359 @@ +# Ticket #000033 — Claim-pack pillar VII (combinatorics) + +**Status:** open · awaiting go/no-go +**Opened:** 2026-05-09 +**Scope:** Extend the `claim_pack` source (#000029) with a new +combinatorics pillar (proposed numbering: VII, slotting between +classical physics VI and λ-Calculus IX). The pillar carries +counting-domain axioms (binomial coefficients, factorial, +Pascal's rule, addition/multiplication principles) and theorems +(inclusion-exclusion, pigeonhole, binomial theorem, generating +functions). Each record follows the existing v2-style dual- +threaded shape (Δ symbolic + ∇ verbose) and cites a stable +combinatorics text. Companion to #000032 (combinatorics@v1 π*). +**Audience:** maintainers of arborist's claim-pack source + +anyone running QA on combinatorial questions ("how many ways…", +"prove the binomial theorem", "what is the inclusion-exclusion +principle"). +**Hard constraint:** **bundle provenance is explicit.** The +existing v2 bundles are Grok-4-generated artifacts with +documented authorship metadata. A combinatorics pillar must come +from a comparable provenance: either a NEW LLM-generated bundle +(with the LLM model + run timestamp + seed all recorded) OR a +hand-curated bundle (with curator name + sources + curation date +recorded). **No silent invention.** Same audit discipline that +`#000029` documented for the existing axioms. + +--- + +## 1. Problem statement + +Today the claim-pack source (`#000029`) ingests two companion +JSONs covering 7 pillars. Pillar VII is missing — the existing +bundles use a Roman-numeral progression I → II → III → IV → V → +VI → IX, deliberately leaving VII (and VIII) un-numbered for +future extension. The combinatorics gap is real: + +- **No counting axioms.** Pascal's rule (`C(n,k) = C(n-1,k-1) + + C(n-1,k)`), addition principle, multiplication principle, the + pigeonhole foundational claim — none are present. +- **One combinatorics-flavored theorem in pillar V** — + Inclusion-Exclusion Principle (cited to Kolmogorov 1933). + Treated as a probability theorem, not a counting theorem. + That's correct framing for the probability pillar, but it + leaves the counting half of the I-E principle (set theory of + finite unions) without a home. +- **Combinatorics is a claim-pack-friendly domain.** Counting + identities have classical proofs, are formally stated as + closed expressions, and have a deep textbook tradition + (Riordan 1958, Comtet 1974, Stanley 1986, Aigner 2007, Wilf + generatingfunctionology 1990, Brualdi 2009). Plenty of + authoritative source citations. + +A claim-pack pillar VII for combinatorics gives: + +1. **Retrieval coverage** for combinatorial questions when an + operator runs claim-pack-augmented queries. +2. **Cross-pillar edges** — Pascal's rule connects to pillar III + (arithmetic) via successor + addition; the binomial theorem + connects to pillar I (logic) via finite induction. +3. **A natural target for `combinatorics@v1` π* (#000032).** + Each pillar VII record can carry a `pi_star_ref` pointing at + the kernel; the witness flow (#000028) becomes computable on + counting questions. + +## 2. Design choices + +### 2.1 Bundle provenance — where does the JSON come from + +The existing v2 bundles cite themselves as: + +```json +"identity": "Grok 4, operating as the GOD AI 'Prometheus' Maths Engine" +"deterministic_seed": 42 +"updated": "2025-07-11T12:00:00Z" +``` + +We have three honest options for pillar VII provenance: + +**A. Commission a Grok-4 v3 bundle (RECOMMENDED FOR PARITY).** +Run a prompt against Grok 4 (or whatever the current generation +is in 2026-05) requesting an additional pillar VII to extend the +existing v2 bundles. Same prompt template, same seed +discipline. Pro: identical authorship provenance to the rest of +the pack; no shape divergence. Con: requires access to Grok 4, +or substitute model with documented divergence note. + +**B. Hand-curate from established textbooks** (Stanley *Enumerative +Combinatorics*, Brualdi *Introductory Combinatorics*, Wilf +*generatingfunctionology*). Pro: canonical sources, audit-grade +citations, fox owns the process end-to-end. Con: substantially +more time investment per record (~30-60 min/axiom for +high-quality dual-threaded text); pillar VII would feel less +"of-a-piece" with the LLM-generated rest. + +**C. Hybrid — LLM draft, human curation.** Use a Grok-4 / Hermes +draft as the seed, then curate by hand against textbook +citations. Pro: balances speed with citation rigor. Con: the +authorship metadata becomes ambiguous ("LLM with human +edits" is a fuzzy provenance label). + +→ Default to **A** if Grok-4 access is straightforward; otherwise +**C** with explicit "human-curated from LLM draft, validated +against [list of textbook citations]" provenance metadata. **B** +is the fallback if both LLM access and curation budget are +unavailable. + +### 2.2 Pillar numbering + +The existing pack uses I, II, III, IV, V, VI, IX. There's a +2-pillar gap (VII, VIII) where this ticket and a future one +could land. Two questions: + +- **Should this pillar be VII or some other number?** The Roman- + numeral progression in the v2 bundles is documented as + reserving VII / VIII for "future pillars" without specifying + what — we get to choose. **VII** (combinatorics) is natural, + positioning it between physics (VI) and λ-Calculus (IX). VIII + stays open for whatever lands next (number theory? graph + theory? topology?). +- **Should re-numbering be considered?** No — the v2 bundles are + shipped artifacts in fox's `~/Downloads`; renumbering would + break references at runtime. New pillars get new numbers, no + mutation of existing ones. + +### 2.3 Axiom set (proposal) + +Foundational counting axioms — minimal set that supports the +classical theorems in §2.4: + +| # | Axiom | Δ form | Source | +|---|-------|--------|--------| +| 1 | Addition Principle | If A, B disjoint finite, ｜A ∪ B｜ = ｜A｜ + ｜B｜ | Brualdi §1 / Stanley I.1 | +| 2 | Multiplication Principle | ｜A × B｜ = ｜A｜ · ｜B｜ | Brualdi §1 / Stanley I.1 | +| 3 | Pigeonhole | If n+1 objects in n boxes, some box has ≥ 2 | Dirichlet 1834 / Brualdi §3 | +| 4 | Definition of Factorial | 0! = 1 ; n! = n · (n-1)! | Standard / Stanley §1.1 | +| 5 | Definition of Binomial | C(n, k) = n! / (k! (n-k)!) | Standard / Knuth TAOCP §1.2 | +| 6 | Pascal's Rule (axiom shape) | C(n,k) = C(n-1,k-1) + C(n-1,k) | Pascal 1654 / Brualdi §5 | +| 7 | Symmetry of Binomial | C(n,k) = C(n,n-k) | Standard | + +Six to seven axioms keeps pillar size comparable to the existing +pillars (V has 3 axioms + Kolmogorov's 3rd as fundamental; +III has 9 Peano-style; IV has 17 Hilbert-style). + +### 2.4 Theorem set (proposal) + +Classical results that the axioms support: + +| # | Theorem | Δ form | Source | +|---|---------|--------|--------| +| 1 | Binomial Theorem | (a+b)^n = Σ C(n,k) a^(n-k) b^k | Newton 1665 / Stanley §1.5 | +| 2 | Inclusion-Exclusion (counting form) | ｜∪ A_i｜ = Σ ｜A_i｜ - Σ ｜A_i ∩ A_j｜ + … | Da Silva / Sylvester / Brualdi §6 | +| 3 | Pigeonhole — strong form | n objects in k boxes ⇒ some box has ⌈n/k⌉ | Brualdi §3 | +| 4 | Vandermonde's Identity | C(m+n, k) = Σ C(m,i) C(n,k-i) | Vandermonde 1772 | +| 5 | Hockey-Stick Identity | Σ C(i, k) for i=k..n = C(n+1, k+1) | Standard / Knuth | +| 6 | Catalan numbers — closed form | C_n = C(2n, n) / (n+1) | Catalan 1838 | +| 7 | Stars-and-Bars | Number of weak compositions of n into k parts = C(n+k-1, k-1) | Standard | + +Seven theorems lines up with what the existing pillars carry +(I has 4, II has 2, III has 4, IV has 2, V has 2, VI has 2, +IX has 7). + +### 2.5 Cross-pillar edges + +`provenance.references` of pillar VII would point at: + +- Pillar III (arithmetic): Pascal's rule recurrence uses + successor + addition. +- Pillar I (logic): Inclusion-exclusion proof uses De Morgan's + laws + finite induction. +- Pillar II (set theory): finite union/intersection axioms support + the addition principle. +- Pillar V (probability): I-E principle in counting form is the + classical case of the probability-theory I-E. + +Pillar VII's outbound edges would be ~4 references at the +provenance level, matching the density of existing pillars' +references. + +### 2.6 π* binding + +Each axiom + theorem record carries a `pi_star_ref` field +identifying the formal projection it canonicalizes to: + +- Identity-shaped records (e.g., `binomial(n,k) = n! / (k! (n-k)!)`): + → `pi_star_ref: "algebra-symbolic@v1"` (the identity holds in + the polynomial-canonical equivalence class). +- Concrete-count examples (e.g., `binomial(5, 2) = 10`): → + `pi_star_ref: "combinatorics@v1"` if `#000032` lands; + otherwise `algebra-symbolic@v1`. + +Pillar VII landing AFTER `#000032` lets the pillar use the +tighter kernel from the start. Pillar VII landing FIRST means +the records start with `algebra-symbolic@v1` and rebind to +`combinatorics@v1` post-#000032; that's a re-canonicalize step +which would invalidate any cache rows pinned to the old hash. +**Land #000032 first** to avoid the rebind churn. + +## 3. Recommendation + +Sequence: + +1. **#000032 first** — combinatorics@v1 π* kernel. Cleanest + integer-output discipline lands without any pillar VII + coupling. +2. **#000033 next** — author the pillar VII JSON (option A: + Grok-4 v3 bundle if accessible; option C: hybrid; option B: + hand-curate as fallback). Produce + `pillar-vii-combinatorics-v1.json` (axioms) and + `pillar-vii-combinatorics-theorems-v1.json` (theorems) under + `~/.arborist/claim-packs/` (or wherever fox prefers; not + committed to repo unless small). +3. **Ingest** via the existing `ClaimPackSource` — it already + accepts arbitrary pillar names; no source-code changes + needed. + +If Grok-4 access is the binding constraint, fall back to +**option B** (hand-curate) or **option C** (hybrid). The pillar +content matters more than the authorship label; we just have +to record which path we took. + +## 4. Implementation sketch + +### 4.1 Bundle authoring + +Whichever provenance path we pick, the output is two JSON files +that mirror the existing v2 shape: + +```jsonc +// pillar-vii-combinatorics-v1.json +{ + "metadata": { + "version": "1.0.0", + "pillar_id": "VII", + "authorship": "...", // "Grok-4 ..." | "hand-curated by ..." | "hybrid: LLM-draft + human-curation" + "sources": [...], // list of textbook citations validated against + "deterministic_seed": ..., + "created": "2026-05-...", + "ingest_target": "claim_pack@v1" + }, + "pillars": { + "VII": { + "title": "Combinatorics axioms (counting principles)", + "description": "...", + "provenance": { + "delta": "...", + "references": [ + "axiomsg4.json:pillar.III.peano.successor", + "axiomsg4.json:pillar.II.zf.union", + "theoremg4.json:pillar.I.logic.deMorgan" + ] + }, + "axioms": [ + { "name": "Addition Principle", "runicLabel": "...", + "delta": "|A ∪ B| = |A| + |B| (when A ∩ B = ∅)", + "nablaVerbose": "If two finite sets share no elements, ...", + ... } + // 6 more axioms + ] + } + } +} +``` + +### 4.2 No source-code changes needed + +`arborist/sources/claim_pack.py` (#000029) already iterates any +pillar found in the bundle. New pillars register as documents +automatically. Adding pillar VII = adding two JSON files to the +ingest path; everything else flows through existing +infrastructure. + +### 4.3 Tests / validation + +The existing `tests/test_claim_pack.py` covers the source's +parsing + edge-emission behavior. Pillar VII inherits all of +that; no new test machinery needed at the source layer. + +What IS new: a small **manifest-content** test that asserts the +new JSON files parse cleanly via the lenient parser, the axiom ++ theorem counts match expectation, and the pillar has the +documented cross-pillar references. + +### 4.4 Bench fixtures + +Once pillar VII ingests, the bench-emergent battery (#000006) +gains a target for combinatorial questions. No new fixtures in +this ticket; downstream bench tickets pick that up. + +## 5. Hard constraints (re-stated) + +1. **Bundle provenance is explicit.** Either + "Grok-4 v3 generation, model-id, seed, timestamp" OR + "hand-curated by [name], sources [list], date [YYYY-MM-DD]" + OR "hybrid: LLM-draft + human curation, sources [list]". + No silent authorship. +2. **No re-numbering of existing pillars.** Pillar VII slots + into the documented gap; existing references stay valid. +3. **No retroactive changes to claim-pack records already in + shards.** New pillar = new documents = additive only. Cache + key invariants untouched. +4. **#000032 lands first.** Avoids rebind churn on + `pi_star_ref` fields; pillar VII records ship with the + tighter kernel reference from day one. + +## 6. Risks / things to watch + +- **Authorship-metadata consistency.** The v2 bundles' metadata + shape becomes load-bearing once we extend it. If we change + `authorship` from a string to a structured object, every + downstream consumer that reads the field has to know about + both shapes. Recommend: add `authorship` as a structured + field on the new bundle's metadata, document the schema, and + treat the v2 string field as a legacy alias. +- **Citation density.** Combinatorics has many overlapping + classical sources (Knuth TAOCP, Brualdi, Stanley, Wilf, Comtet, + Riordan). Pick ONE primary citation per record; multi-source + citations dilute the warrant resolution layer (#000031). +- **Symbol notation drift.** "C(n, k)" vs "binomial(n, k)" vs + "n choose k" notation matters at retrieval time. The Δ field + pins ONE notation. Pick `\binom{n}{k}` LaTeX consistent with + the existing pillar III arithmetic notation; the ∇ field + re-expresses in prose. +- **Pillar VIII placeholder.** Leaving VIII open for a future + pillar (e.g., number theory, graph theory) is fine; do NOT + pre-allocate or stub. +- **LLM availability.** Option A depends on Grok-4 (or successor) + access. If that's not available, fall back without re-opening + the ticket; document the substitution in the bundle's + authorship field. + +## 7. Forward links + +- **#000029** — claim-pack source. This ticket extends it. +- **#000032** — combinatorics@v1 π*. Kernel that pillar VII + records bind to via `pi_star_ref`. Lands FIRST. +- **#000031** — surface-ingest cited textbooks. If pillar VII + cites textbooks (Brualdi, Stanley, Knuth, etc.), those become + candidates for the textbook-ingest pipeline. Mostly + proprietary — yellow-light per #000031's license discipline. +- **#000028** — multi-modality witness. Pillar VII records that + bind to `combinatorics@v1` become STRICT-WITNESSED-eligible + on counting questions. + +## 8. Status + +Open · awaiting go/no-go. + +Estimated size: + +- Authoring effort: 4-12 hours depending on provenance path + (option A fastest if Grok-4 access available; option B + longest at hand-curation tempo; option C in between). +- Code: ~30 LOC manifest-content test. No source-code changes + in `arborist/sources/claim_pack.py`. +- Data: 2 JSON files (~100-200 KB total based on v2 sizing). + Stored under `~/.arborist/claim-packs/` or committed to repo + under `bench/fixtures/claim-packs/` if size is small. +- Bench: 0 LOC in this ticket; downstream bench tickets pick + up combinatorial fixtures separately.