bayes_posterior tool v0.1

STEP: 1528 / Test: 27/27 PASS / Lean 4: 7 theorem zero sorry / Type: STEP 1487 データサイエンス 3rd tool (47 defer 16 番目、 姉妹 tool 19)

Beta-Binomial conjugate posterior: prior Beta(α, β) + observations (s successes, f failures) → posterior Beta(α+s, β+f)。 posterior mean + 95% CI → verdict。

7 case 決定表: strong evidence → TRUE / strong counter → FALSE / CI contains 0.5 → NEITHER / minimal shift → BOTH (non-informative) / posterior shifted → TRUE (moderate)。

決定表 (7 case)

ConditionVerdict
invalid (α≤0, β≤0, s>trials)NEITHER
posterior mean ≥ 0.9 (default)TRUE (strong_evidence)
posterior mean ≤ 0.1FALSE (strong_counter_evidence)
95% CI contains 0.5NEITHER (uncertain_posterior)
|posterior - prior| < 0.05BOTH (non_informative_update)
posterior shifted (moderate)TRUE (posterior_shifted)

使用例

// Strong evidence (100/100 successes with uniform prior)
bayesPosterior({ successes: 100, trials: 100 });
// { verdict: 'TRUE', posteriorMean: ~0.99, ciLower: ~0.97, ciUpper: 1.0 }

// Balanced data → NEITHER (CI contains 0.5)
bayesPosterior({ successes: 5, trials: 10 });
// { verdict: 'NEITHER', posteriorMean: 0.5, ciLower: ~0.25, ciUpper: ~0.75 }

// Custom prior Beta(2, 3) + 8/10 successes → posterior (10, 5)
bayesPosterior({ priorAlpha: 2, priorBeta: 3, successes: 8, trials: 10 });
// { verdict: 'TRUE', posteriorMean: ~0.667, reason: 'posterior_shifted' }

Lean 4 (7 theorem zero sorry)

posterior_alpha_shift          : posterior_alpha - prior_alpha = successes
posterior_beta_shift           : posterior_beta - prior_beta = failures
posterior_no_evidence_alpha    : 0 successes → posterior_alpha = prior_alpha
uniform_prior_all_successes    : Beta(1,1) + n successes → posterior (n+1, 1)
no_data_no_update              : successes=failures=0 → posterior = prior
bayes_balanced_gives_neither   : equal posterior → NEITHER
bayes_strong_alpha_gives_true  : posterior_a > 10 * b → TRUE

Honest scope

❶ Beta-Binomial のみ、 Normal-Normal / Gamma-Poisson 未 embed。

❂ Normal approx for CI (小 sample で 精度低下、 実 exact Beta CDF は 計算重い)。

❸ 「世界初」 なし = Bayes 1763 / Laplace 1812 既知 D-FUMT₈ mapping。

❹ 累計 defer 33 → 32。