https://rsk0315.hatenablog.com/entry/2025/04/07/020139

ずんだもんなのだ
今日はこの解法の正当性の証明をやっていくのだ pic.twitter.com/UeXkq4BG5O
— えびちゃん🍑🍝🦃 (@rsk0315_h4x) 2025年4月5日

fn solve_f64(n: f64, m: i32) -> Option<u32> {
    if n == 1.0 || m == 1 {
        (n + (m as f64) <= 1.0e9).then(|| n as u32 + m as u32)
    } else {
        let res = (n.powi(m + 1) - 1.0) / (n - 1.0);
        (res <= 1.0e9).then(|| res as u32)
    }
}

20 分くらいかけて全部のケースを回して正しい答えを出力することがわかったのだ
今回も簡単だったのだ
見てくれてありがとうなのだ
— えびちゃん🍑🍝🦃 (@rsk0315_h4x) 2025年4月5日

バ、
馬鹿もーんっ・・・・！
なんだっ・・！この証明はっ・・・・・・・・！
通るかっ・・・・・・！
こんなもん・・！*1

まぁ通るんですが、つまらないかなということで、やっていきます。

記事化を待つ
— ねぼこ (@nebocco27) 2025年4月6日

問題リンク：ABC 400 B

証明

下記が成り立つことは既知とします。 $$ \sum_{i=0}^M N^i = \begin{cases} M+1, & \text{if}\: N=1; \\ \displaystyle\frac{N^{M+1}-1}{N-1}, & \text{if}\: N\ne 1. \end{cases} $$

powi について

'llvm.powi.*' Intrinsic には下記の記述があります。

Semantics: This function returns the first value raised to the second power with an unspecified sequence of rounding operations.

たとえば、$\texttt{powi}(n, 7)$ は $( (n\otimes n)\otimes (n\otimes n) ) \otimes ( (n\otimes n)\otimes n)$ かもしれないし、$( ( (n\otimes n)\otimes n)\otimes ( (n\otimes n)\otimes n) )\otimes n$ かもしれないし、$( ( ( ( ( (n\otimes n)\otimes n)\otimes n)\otimes n)\otimes n)\otimes n)\otimes n$ かもしれないし、みたいな感じだと思います。

コード (src) は繰り返し二乗法のようですが、累乗のアルゴリズムはそれだけではないですし、それに限定した仕様にする理由はないのでこういう感じになっているのでしょうかね。$\roundcirc{n^{3.5}}\otimes\roundcirc{n^{3.5}}$ とか $\roundcirc{n^8}\oslash n$ のようにされると困りますが、そういうことはないと仮定しておきます。

上記の前提であれば、非負整数 $n\le 2^{53}$ と $i$ に対して、$n^i \le 2^{53}$ であれば $\texttt{powi}(n, i) = n^i$ が成り立ちます。また、$n^i\gt 2^{53}$ の場合でも、$\texttt{powi}(n, i)\lt\infty$ ならば、ある実数 $|\theta|\le (1+2^{-53})^{i-1}-1$ に対して $\texttt{powi}(n, i) = (1+\theta)n^i$ が成り立ちます。

場合分け

整数 $1\le N\le 10^9$, $1\le M\le 100$ について考えます。

Claim 1: $N = 1 \wedge M+1 \le 10^9 \implies M\oplus 1 = M+1$ が成り立つ。

Proof: 明らか。$\qed$

Claim 2: $N = 1 \wedge M+1 \gt 10^9 \implies M\oplus 1 \gt 10^9$ が成り立つ。

Proof: 明らか。$\qed$

Claim 3: $N \gt 1 \wedge M = 1 \wedge N+1 \le 10^9 \implies N\oplus 1 = N+1$ が成り立つ。

Proof: 明らか。$\qed$

Claim 4: $N \gt 1 \wedge M = 1 \wedge N+1 \gt 10^9 \implies N\oplus 1\gt 10^9$ が成り立つ。

Proof: 明らか。$\qed$

$f(N, M) = (\texttt{powi}(N, M+1)\ominus 1)\oslash(N\ominus 1)$ とします。

Lemma 5: $M\gt 1 \implies \frac{\log_2(10^9)}M \le \frac{53}{M+1}$ が成り立つ。

Proof

$$ \begin{aligned} \frac{\log_2(10^9)}M \le \frac{53}{M+1} &\iff 1+\frac1M \le \frac{53}{\log_2(10^9)} \\ &\iff \frac1M \le \frac{53-\log_2(10^9)}{\log_2(10^9)} \\ &\iff M\ge \frac{\log_2(10^9)}{53-\log_2(10^9)} \gt 1.294. \end{aligned} $$

$M$ の整数性より従う。$\qed$

Claim 6: $N \gt 1 \wedge M\gt 1 \wedge \frac{N^{M+1}-1}{N-1}\le 10^9 \implies f(N, M) = \frac{N^{M+1}-1}{N-1}$ が成り立つ。

Proof

$N^{M+1}\le 2^{53}$ について考える。 $$ \begin{aligned} N^{M+1}\le 2^{53} % &\iff (M+1)\log_2(N) \le 53 \\ % &\iff M \le \frac{53}{\log_2(N)}-1 \\ % &\iff M \le \frac{53-\log_2(N)}{\log_2(N)}. &\iff N \le 2^{\frac{53}{M+1}}. \end{aligned} $$ また、$\frac{N^{M+1}-1}{N-1} \le 10^9$ について考える。 $$ \begin{aligned} \frac{N^{M+1}-1}{N-1} \le 10^9 &\implies N^M \le 10^9 \\ % &\iff M\log_2(N) \le 9\log_2(10) \\ % &\iff M \le \frac{9\log_2(10)}{\log_2(N)}. &\iff N \le 2^{\frac{\log_2(10^9)}M}. \end{aligned} $$ Lemma 5 より、$\frac{N^{M+1}-1}{N-1} \le 10^9 \implies N^{M+1}\le 2^{53}$ が成り立つ。

よって、$f(N, M) = (N^{M+1}\ominus)\oslash(N\oslash 1) = \frac{N^{M+1}-1}{N-1}$ となる。$\qed$

Lemma 7: $N \gt 1 \wedge M\gt 1 \wedge N^{M+1}\gt 2^{53} \implies \frac{N^{M+1}-1}{N-1}\gt 2^{53\cdot 2/3}$ が成り立つ。

Proof: Lemma 5, Claim 6 と同様にして示せる。$\qed$

Claim 8: $N \gt 1 \wedge M\gt 1 \wedge \frac{N^{M+1}-1}{N-1}\gt 10^9 \implies f(N, M) \gt 10^9$ が成り立つ。

Proof

Case 1: $N^{M+1}\le 2^{53}$

Claim 6 同様に $f(N, M) = \frac{N^{M+1}-1}{N-1}$ が成り立ち、$f(N, M)\gt 10^9$ となる。

Case 2: $N^{M+1}\gt 2^{53}$

$\texttt{powi}(N, M+1)=\infty$ のとき $f(N, M)=\infty\gt 10^9$ となる。

そうでないとき、実数 $|\theta_{\otimes}|\le (1+2^{-53})^M-1$, $|\theta_{\ominus}|\le 2^{-53}$, $|\theta_{\oslash}|\le 2^{-53}$ が存在し、下記が成り立つ。 $$ \begin{aligned} f(N, M+1) &= (\texttt{powi}(N, M+1)\ominus 1)\oslash (N\oslash 1) \\ &= ( (1+\theta_{\otimes})N^{M+1}\ominus 1)\oslash (N-1) \\ &= (1+\theta_{\ominus})( (1+\theta_{\otimes})N^{M+1}-1)\oslash (N-1) \\ &= (1+\theta_{\oslash})\cdot \frac{(1+\theta_{\ominus})( (1+\theta_{\otimes})N^{M+1}-1)}{N-1} \\ &= (1+\theta_{\oslash})(1+\theta_{\ominus})\cdot \frac{(1+\theta_{\otimes})N^{M+1}-1}{N-1} \\ &= (1+\theta_{\oslash})(1+\theta_{\ominus})\cdot \frac{(1+\theta_{\otimes})(N^{M+1}-1)+\theta_{\otimes}}{N-1} \\ &= (1+\theta_{\oslash})(1+\theta_{\ominus})(1+\theta_{\otimes})\cdot \frac{N^{M+1}-1}{N-1} \\ &\qquad + (1+\theta_{\oslash})(1+\theta_{\ominus})\cdot\frac{\theta_{\otimes}}{N-1} \\ &\gt (1-2^{-53})^{M+2}\cdot 2^{53\cdot 2/3} + (1+2^{-53})^2\cdot\frac{-( (1+2^{-53})^M -1)}{N-1} \\ &\ge (1-2^{-53})^{102}\cdot 2^{53\cdot 2/3} - (1+2^{-53})^2\cdot\frac{(1+2^{-53})^{100}-1}{2-1} \\ &\gt 4.329\times 10^{10} \\ &\gt 10^9. \quad\qed \end{aligned} $$

よって、各 $N$, $M$ について、$\sum_{i=0}^M N^i$ が $10^9$ 以下ならば $f(N, M) = \sum_{i=0}^M N^i$ であり、$10^9$ より大きいならば $f(N, M)\gt 10^9$ であることが示せました。

おまけ

$f(N, 1)$ がうまくいかない例について考えます。なお、結合の仕方は一通りしかないため $\texttt{powi}(N, 2) = N\otimes N$ となります。

たとえば $N=189812534$ のとき、下記のようになります。 $$ \begin{aligned} f(189812534, 1) &= ( (189812534\otimes 189812534)\ominus 1)\oslash(189812534\ominus 1) \\ &= ( (189812534^2-4)\ominus 1)\oslash(189812534\ominus 1) \\ &= (189812534^2-4)\oslash(189812534-1) \\ &= {\small 189812534.999999970197677}{\footnotesize 6123046875}. \end{aligned} $$ よって、これを切り捨てて整数にすると $1+N$ とは異なる値が得られます。

他にも、$189812538$ や $999999992$ など、たくさんの $N$ がこのようになります。

おわり

おわりです。全探索の方が早く済みました。いかがでしたか？

*1:出典：https://youtu.be/YPaJ30gY1ic?t=61。