engineering/arborist
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

docs/tickets: open #000032 (combinatorics@v1 π*) + #000033 (pillar VII)

Browse source 
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.
This commit is contained in:
russell@unturf.com 2026-05-09 12:59:29 -04:00
parent 5257f9a8f3
commit d34ecb27c1
No known key found for this signature in database
3 changed files with 711 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
docs/TICKETS.md
View file

@ -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`

349
docs/tickets/ticket-000032-combinatorics-pi-star.md Normal file
View file

@ -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
``"<num>/<den>"`` 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.

359
docs/tickets/ticket-000033-claim-pack-pillar-vii-combinatorics.md Normal file
View file

@ -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.