---
name: Finitization Toolbox (STEP 674)
description: 10-engine unified framework for infinite-to-finite reduction in open math problems, with Walnut bridge and Collatz application
type: project
originSessionId: cd413b52-217d-49a2-ae30-92af7ffedf9b
---
STEP 674: Finitization Toolbox — `src/axiom-os/finitization-toolbox.ts` + `src/axiom-os/walnut-bridge.ts`

**Why:** Proposed in response to the question "is there open source that converts infinite search into finite proofs?" The answer: partial tools exist (AProVE, Walnut, dReal, Coq-Interval, etc.) but no unified framework. Built one.

**How to apply:** When attacking an open math problem formulated as ∀n.P(n), dynamical system, or recurrence, instantiate a `FinitizationProblem` and run `new FinitizationToolbox().run(problem)`. Each of the 10 engines reports a verdict with D-FUMT₈ tag and a "gap" field identifying where the technique fails.

## 10 engines implemented

| # | Engine | Classical tool analog | Verdict on Collatz |
|---|---|---|---|
| 1 | Well-Founded Induction | AProVE lex ranking | open (no simple lex measure works) |
| 2 | Size-Change Termination | Lee-Jones-Ben-Amram SCT | open (no measure is always-down) |
| 3 | Polynomial Ranking Synth | T2, InvGen | open (1200 failures / 6913 transitions) |
| 4 | k-Automatic Decider (Walnut-style) | Walnut, Pecan | open (over-approximation has spurious cycles — confirms Conway's negative) |
| 5 | Positivstellensatz (SOS) | SOSTOOLS | likely (peak² ≤ 160·n⁴ holds on corpus) |
| 6 | Interval Verifier | Coq-Interval, Arb | closed (112 orbits verified ≤ 10000 steps) |
| 7 | Compactness (Löwenheim-Skolem) | Isabelle | inapplicable (wrong direction for ∀) |
| 8 | Ramsey Finitization | Paris-Harrington | likely (all 112 orbits have descending subseq ≥ log₂(start)) |
| 9 | Well-Quasi-Order (Higman) | — | likely (94% Higman-comparable parity-signatures) |
| 10 | Büchi Eventual-Periodicity | NuSMV | open (over-approx LTS has spurious cycles) |

## Walnut Bridge (separate module)

`src/axiom-os/walnut-bridge.ts` — TypeScript reimplementation of Walnut (Shallit) core:
- DFA / LTS data structures
- product / complement / emptiness / universality checks
- `decideForAll(predicateDFA)` — decides first-order ∀n for k-automatic predicates
- `collatzModLTS(k)` — non-deterministic abstraction of Collatz mod 2^k
- Sanity-checked: "n even" correctly fails universality with counterexample=1

## Key structural discovery

**Collatz lies exactly in the D-FUMT₈ "NEITHER" region:**
- NOT k-automatic (Conway) → Walnut decider fails
- NOT polynomially rankable → linear-combination search fails
- NOT SCT-terminating with basic measures → every candidate has "up" transitions

**Only engines exploiting ORBIT STRUCTURE (Ramsey, WQO) give positive results.**

This confirms STEP 673's conclusion: the F-entropy for Collatz must be path-dependent, not state-dependent.

## New structural theorem (from engine synthesis)

Combining Büchi + WQO + Ramsey engines:
- (A) over-approximation LTS at resolution k=10 has 1024 reachable states
- (B) Higman WQO guarantees: any infinite set of orbit parity-signatures has Higman-comparable pairs
- (C) Ramsey: every orbit has a descending subsequence of length ≥ log₂(start)

Conjecture: Ramsey × WQO descent argument. If an infinite counterexample orbit existed, its parity-signature would be Higman-embedded in infinitely many other orbits, giving a descent chain — but WQO then forces termination.

Not yet a formal proof — missing: how to convert Higman-comparability into numerical descent.

## SEED_KERNEL theories added
- T-FT-1: Finitization Toolbox [SELF]
- T-FT-2: D-FUMT₈ Applicability Index [FLOWING]
- T-FT-3: Gap Visualization Theorem [NEITHER]
- T-FT-4: Walnut-Collatz Boundary [BOTH]
- T-FT-5: Positive-Results Inventory [BOTH]
- T-WB-1: Walnut Bridge [TRUE]
- T-WB-2: Collatz-mod-2^k LTS [FLOWING]
- T-WB-3: k-Automatic Boundary Theorem [BOTH]

Test: `npx tsx test/step674-finitization-toolbox-test.ts` (4 passed, 0 failed)
1 closed, 3 likely, 5 open, 1 inapplicable.