combinatorial_bound tool v0.1 (STEP 1517)

combinatorial_bound tool v0.1

STEP: 1517 / 公開日: 2026-08-28 / Test: 28/28 PASS / Lean 4: 8 theorem zero sorry / Type: STEP 1486 離散数学 arc candidate 実装 (**離散数学 domain 未着手 first**)

❶ 組合せ数 feasibility verdict: C(n,k) / P(n,k) / n! → 実行可能性判定 (feasible/borderline/infeasible)。 double 精度 overflow で INFINITY。

❷ 離散数学 domain 未着手 first tool (8/10 D-FUMT₈ × domain arc の少なくとも 1 tool 実装に前進)。

❸ 11 姉妹 verdict tool 目。

決定表 (6 case)

#	Condition	Verdict	Reason
1	invalid inputs (n<0, k<0, k>n, non-integer)	NEITHER	invalid_arguments
2	value = 0	ZERO	zero_combinations
3	value ≤ 1e6 (default)	TRUE	feasible_enumeration
4	1e6 < value ≤ 1e12	NEITHER	borderline_intractable
5	value > 1e12	INFINITY	combinatorial_explosion
6	overflow (Infinity)	INFINITY	numerical_overflow

Condition

Verdict

Reason

invalid inputs (n<0, k<0, k>n, non-integer)

NEITHER

invalid_arguments

value = 0

ZERO

zero_combinations

value ≤ 1e6 (default)

TRUE

feasible_enumeration

1e6 < value ≤ 1e12

NEITHER

borderline_intractable

value > 1e12

INFINITY

combinatorial_explosion

overflow (Infinity)

INFINITY

numerical_overflow

使用例

combinatorialBound({ fn: 'choose', n: 5, k: 2 }) // { verdict: 'TRUE', value: 10, reason: 'feasible_enumeration' } combinatorialBound({ fn: 'choose', n: 20, k: 10 }) // { verdict: 'TRUE', value: 184756 } combinatorialBound({ fn: 'factorial', n: 10 }) // { verdict: 'NEITHER', value: 3628800, reason: 'borderline_intractable' } combinatorialBound({ fn: 'choose', n: 50, k: 25 }) // { verdict: 'INFINITY', value: 126410606437752, reason: 'combinatorial_explosion' } combinatorialBound({ fn: 'factorial', n: 200 }) // { verdict: 'INFINITY', value: Infinity, reason: 'numerical_overflow' }

Lean 4 (8 theorem zero sorry)

verdict_zero_gives_zero : value=0 → ZERO verdict_feasible_gives_true : value ≤ feasible → TRUE verdict_borderline_gives_neither : feasibleborderline (well-formed f≤b) → INFINITY fact_zero / fact_one / fact_five : factorial base cases fact_positive : ∀n, n! > 0

Test coverage (28/28 PASS)

Guard 5 + TRUE 4 + NEITHER 2 + INFINITY 2 + Custom threshold 1 + Determinism 1 + edge cases

姉妹 verdict tool 11 揃った

SNR / BH FDR / Welch / 分布 / payoffs / bit strings / V(t) / 「は/が」 / population / S1/S2 / 組合せ

Honest scope

❶ double 精度 (IEEE 754) 制限、 200! 等は overflow で INFINITY 扱い。 BigInt 版は別 tool candidate。

❷ Stirling 近似 log10(n!) ≈ n log10(n) は未 embed、直接計算のみ。

❸ 「世界初」なし = 組合せ論 (Pascal) 既知構造 D-FUMT₈ verdict mapping。

❹ 累計 defer 41 → 40。