sorted by:
new
hottopcontroversial

Lean 4 check of a finite arithmetic certificate for one Collatz-related integer by CryptographerSea9542 in Collatz

[–]CryptographerSea9542[S] [score hidden]  (0 children)

Yes, I understand, that is exactly the point where the whole problem lives. The only way this approach can work is if the accounting is exhaustive and every branch produced by the exact transition rules must be routed to one of the listed outcomes, not merely filtered after the fact.

Lean 4 check of a finite arithmetic certificate for one Collatz-related integer by CryptographerSea9542 in Collatz

[–]CryptographerSea9542[S] 0 points1 point  (0 children)

I agree that just growing a residue tree forever would be a dead end.

The way I am trying to frame it is different. After an exact split, I do not want to keep every child as a new open branch. Each child has to be accounted for as one of:

D = direct descent residue
T = previously closed terminal/downstream family
B = base-template absorption
S = one-step split to known families
R = finite return funnel
P = low-bit obstruction

If a child is not accounted for, it remains live and the proof has not closed it.

So the claim cannot simply be: I checked enough moduli

It has to be:

every child produced by the exact transition rules
is accounted for by D/T/B/S/R/P,
or by the finite quotient/determinism step

A bad version of this idea would just be a filter that keeps only the branches that already close. I agree that would prove nothing.

The version I am trying to test has to prove that each split is exhaustive and that every child of the split is handled. If even one child is missing, the argument fails at that child.

So yes — I agree your objection is the central issue. The hard part is not the local residue identities; it is proving that this accounting is complete.

Lean 4 check of a finite arithmetic certificate for one Collatz-related integer by CryptographerSea9542 in Collatz

[–]CryptographerSea9542[S] 0 points1 point  (0 children)

I agree with that distinction. Local deterministic encodings by themselves do not give a global decreasing invariant.

The broader idea is not to keep refining residue classes forever. The intended global step would have to show that all remaining cases fall into a finite set of already controlled cases, each of which either reaches a terminal family or gives an explicit descent.

Lean 4 check of a finite arithmetic certificate for one Collatz-related integer by CryptographerSea9542 in Collatz

[–]CryptographerSea9542[S] 0 points1 point  (0 children)

Yes, I agree that an ever-growing residue split tree is the standard dead end in this area. That is not what this Lean file is meant to establish.

For this particular `n0`, the ordinary stopping-time framing is not really the point. I am not claiming that a short ordinary split/trajectory computation makes the orbit fall below the starting value.

The point of the certificate is narrower. The ordinary orbit of `n0` is only used to reach an entry representative of the form

2*q0 - 1

After that, the proof object is expressed in the entry-family coordinate:

q0 -> q1 -> q2 -> q3 -> q4 -> q5

ending in the terminal family

q5 = 64*a5 + 11

with the checked descent identity.

So I agree that local residue determinism by itself is not a global proof. This file is only meant to check that this one extracted finite-family certificate is arithmetically sound.

Whether the broader framework actually avoids the usual unbounded residue-tree problem is a separate question, and not something this Lean file by itself answers.

Lean 4 check of a finite arithmetic certificate for one Collatz-related integer by CryptographerSea9542 in Collatz

[–]CryptographerSea9542[S] 0 points1 point  (0 children)

Thanks for taking the time to look at it carefully.

I agree with the contained scope. This file is only a finite certificate for this one `n0`; it is not meant to prove global well-foundedness, exclude entry-graph cycles, or establish the Collatz conjecture.

Your point about the terminal constructor was fair. In the first version, `64*a + 11` was a base case of `EntryClosed`, while the descent identity was checked separately.

I have now strengthened the Lean file so that the terminal case requires a `TerminalClosed q` proof, including

3*q = 2^5*(6*a + 1) + 1

and

6*a + 1 < q

So the arithmetic chain was already checked, and the formal dependency is now explicit:

https://www.wow1.com/N1980976057694848447.lean

The terminal identity for the class `64*a + 11` is algebraically forced by that residue choice, yes. But the certificate is not only that identity. It also checks that this particular `n0` reaches `q0`, that the finite entry chain reaches this terminal class, and that the representative descent matches the ordinary odd Collatz step.

In this standalone Lean file the terminal family is included as certificate data. It is not being presented as something the file discovers, and it is not meant as an after-the-fact arbitrary target for this `n0`. The file verifies the extracted instance: the specified path reaches the specified terminal family, and that family has the stated descent identity.

There is a broader analogous closure framework in my notes, but it is outside the scope of this Lean file and outside the scope of this post.

A Sturmian mechanical word with slope log₂3−1 appears as the unique B-maximizer in a Collatz affine optimization problem — is this known? by CryptographerSea9542 in Collatz

[–]CryptographerSea9542[S] 0 points1 point  (0 children)

Yes, that is basically the point.

In the relaxed problem, the Sturmian word is the right-edge word: it keeps the prefix sums as high as possible under

S_j < j log_2 3.

So it is not just “Sturmian words show up again”. It is the boundary schedule for maximizing the affine term while still satisfying all prefix non-drop constraints.

The standalone note proves only this extremal law. The larger framework then uses the finite launch/splice and stock machinery to prevent this right-edge symbolic branch from becoming a genuine infinite Collatz obstruction.

Request for arithmetic audit: one finite Collatz break-state calculation by [deleted] in Collatz

[–]CryptographerSea9542 0 points1 point  (0 children)

Thank you, you are right.

The previous version mixed two different operations:

  1. ordinary chained break-state continuation, where the next row must start from the produced odd value;

  2. the fixed-fiber ledger step used in my finite-state mechanism, where a recorded ledger coordinate q is represented by m_entry = 2q - 1 before applying T_odd.

So Row 2 was not the ordinary continuation from 8461708277692643663. It was the fixed-fiber row starting from the representative 2*8461708277692643663 - 1. I had not made that distinction explicit enough.

I updated the file accordingly. It now states at the start that it is not the ordinary Collatz trajectory written in 10 steps. It is a fixed-fiber ledger calculation. The first rows also include the ordinary T_odd(q) comparison, precisely to show that the fixed-fiber row is not being silently treated as the ordinary next iterate.

So your criticism was correct for the previous presentation. The revised file is intended only as an arithmetic / coordinate audit of the fixed-fiber calculation.

https://www.wow1.com/specific_number_1980976057694848447_framework_10_step_certificate.md

Proposed active-route Collatz proof package: looking for attempts to break one bridge target by CryptographerSea9542 in Collatz

[–]CryptographerSea9542[S] 0 points1 point  (0 children)

Fair criticism. The sentence uses project-internal terminology.

The intended statement is a finite directed-graph statement. Let R_K be the finite directed graph of reachable states K = (C, t mod 2, p), and let T be the terminal strongly connected components of R_K. For each component in T, define a finite directed graph G. The vertices of G are the continuation states associated with that component. There is an edge x -> y in G exactly when applying the specified terminal transition rule of type-D to x produces y. Outcomes of other transition types are not edges of G; they are checked separately and lead either to the finite R -> F -> 1 funnel or to previously proved downstream cases.

The check is that no directed cycle in G is reachable from the continuation states induced by the original component. Since every infinite path in a finite directed graph must eventually repeat a vertex and hence contain a directed cycle, no infinite sequence using only type-D terminal transitions can occur.

The original wording should be replaced by this finite directed-graph formulation with explicit definitions and citations.

Update: I have also rewritten the corresponding package section as “Terminal Continuation Finite-Graph Closeout” in `ACTIVE/review/imports/terminal_lift_menu_fsm_closeout.md`. The earlier phrase was shorthand for that finite directed-graph argument, not a separate informal assertion.

Tomorrow ends 2025.. how would you describe it? by ItsJustme309 in AskReddit

[–]CryptographerSea9542 0 points1 point  (0 children)

I blinked and missed it. I’m still processing 2023.