Bounded Collatz reachability — a §4 relational exhibit on ℕ. More...
#include <algorithm>#include <cstddef>#include <limits>#include <optional>#include <ranges>#include <type_traits>#include <utility>import dedekind.sets;import dedekind.sequences;import dedekind.relational;import dedekind.order;import dedekind.category;
Classes | |
| struct | dedekind::numbers::ReachPath |
The reach indicator's type: a Path<Ternary> monotone in {Unknown, True} (True absorbs), constructible only through collatz_reach_path, which guarantees that shape; registered absorptive in sequences below, as DivergencePath is. More... | |
Namespaces | |
| namespace | dedekind::numbers |
Functions | |
| constexpr std::size_t | dedekind::numbers::collatz_rule (std::size_t n) |
The recurrence, spelled out explicitly as a named function (not a lambda): n even ↦ n/2, n odd ↦ 3n+1. Computed on the native size_t shadow, which saturates where 3n+1 would leave the word, the posture of ℕ's proxy (the point-free relation on Cardinality saturates to ℵ₀ the same way). The word's top is odd, so it is a fixpoint of the rule: an orbit that reaches it never reaches 1, and the verdict below stays Unknown rather than wrapping into a false True. | |
| constexpr auto | dedekind::numbers::collatz_orbit (std::size_t n) |
The orbit \(\{n\} ; T^{\le N}\) presented as the arrow's iterate — a lazy Path<std::size_t>. | |
| constexpr ReachPath | dedekind::numbers::collatz_reach_path (std::size_t n) |
True once 1 is present, Unknown before — a monotone {Unknown,True} absorptive path (the ℕ analogue of Mandelbrot's escape indicator). | |
| constexpr std::optional< std::size_t > | dedekind::numbers::collatz_reach_time (std::size_t n, std::size_t budget) |
The first index \(k \le\) budget at which the orbit hits 1, else nullopt — the efficient materialization (one forward pass). | |
| constexpr Ternary | dedekind::numbers::reaches_1_within (std::size_t n, std::size_t budget) |
The Rosolini-dominance verdict: reaches 1 within budget ⟹ True (IN); not yet ⟹ Unknown (U). Never False. | |
| template<std::size_t W, std::size_t B> | |
| constexpr bool | dedekind::numbers::all_reach_1_within () |
The collapse: the open \(\forall\)-conjecture, restricted to a finite window \([1, W)\) and a budget B, is a decidable compile-time fact. | |
Variables | |
| constexpr auto | dedekind::numbers::n_even = ℕ * ℕ & π_1 % 2 == 0 |
The parity discriminant \(\{(n,m) : n \text{ even}\}\) — the axis restriction spelled once, so \(T\) never repeats the \(\pi_1 \bmod
2\) test. Its complement \(\sim\)n_even is \(\{n \text{ odd}\}\) (on ℕ the two parities exhaust and are disjoint), which makes the case split structural rather than two independent guards. | |
| constexpr auto | dedekind::numbers::halve = ℕ * ℕ & π_2 * 2 == π_1 |
| The even step \(m = n/2\), spelled without division as \(2\pi_2 = \pi_1\) (the doubling graph read backwards). | |
| constexpr auto | dedekind::numbers::triple_plus_1 = ℕ * ℕ & π_1 * 3 + 1 == π_2 |
The odd step \(m = 3n+1\) — the affine graph ( | |
| constexpr auto | dedekind::numbers::collatz |
The Trsk relation \(T \subseteq \mathbb{N}\times\mathbb{N}\), spelled point-free as the McCarthy conditional \(T = (\text{even} \cap \text{halve}) \cup (\text{odd} \cap
\text{triple})\) — no lambda, no graph, the recurrence is the relation, spelled in uniform set-grammar: & (meet), ~ (complement), OrPredicate union of #365). Mirrors the divides relation of §4; the parity test appears exactly once. | |
| constexpr auto | dedekind::numbers::converges_in_1 |
converges_in_1 \(= \mathrm{collatz}^{\circ}(1) = \{n \mid
\mathrm{collatz}(n) = 1\}\) — the pre-image of the fixed-point target \(\{1\}\): the naturals that reach 1 in exactly one step. Point-free, via the converse fibre. | |
| constexpr auto | dedekind::numbers::collatzM = collatz & (π_1 < 64) |
collatz restricted to the finite ℕ-prefix \([0,64)\) by a half-space domain cut — the bound 64 rides in the pivot VALUE, so >> recovers it. | |
| constexpr auto | dedekind::numbers::collatz2 = collatzM >> collatzM |
collatz2 \(= \mathrm{collatz};\mathrm{collatz}\) over the finite \([0,64)\) middle — two steps, the bare relative product, middle inferred from the bound (no argument, no shadow, no graph, no array). | |
| constexpr auto | dedekind::numbers::back2 = converse(collatz2) |
converged_2 \(= \mathrm{collatz2}^{\circ}(\{1,2,4\})\) — the naturals captured by the attractor within two steps: the pre-image of the cycle, spelled as the finite relational image (fibre of the converse over the three cycle points), which distributes to the union of the point-fibres. | |
| constexpr auto | dedekind::numbers::converged_2 |
| constexpr auto | dedekind::numbers::pending_2 = ~converged_2 |
pending_2 \(= \sim\)converged_2 — the naturals not yet captured within two steps: the honest "Unknown", complemented on the domain (unary), not on the pair universe. | |
| template<> | |
| constexpr bool | dedekind::sequences::is_absorptive_sequence_v< dedekind::numbers::ReachPath > |
Opt-in: every ReachPath is absorptive (eventually constant: True once 1 is seen, or the constant Unknown). The shape is guaranteed by its only constructor, so the registration is sound. | |
Detailed Description
Bounded Collatz reachability — a §4 relational exhibit on ℕ.
@partition :collatz
The recurrence is spelled once, point-free, as the Trsk relation collatz \(= T \subseteq \mathbb{N}\times\mathbb{N}\) (an IsRelation — whether the even/odd guard-union is inferred IsFunction is a follow-up), and then finitely iterated via its native size_t shadow collatz_rule.
The set \(\{\, n : \text{the orbit of } n \text{ reaches } 1 \,\}\) is de facto undecidable: universality is the open Collatz conjecture, the generalized problem is provably undecidable (Conway), and the search is unbounded a priori. We make no closure statement — reachability would be \(\mathrm{dom}(T^{*} ; \eta(1))\), but \(T^{*}\) is not a point-free operator (the relative product >> is Boolean-middle only, and the Kleene star is FIXME(#786)). So reachability strength-reduces to the finite iteration on its native size_t shadow — the honest boundary this exhibit names, and a motivating case for point-free \(R^{*}\) (#786).
The "reaches 1" indicator mirrors :mandelbrot's escape indicator (its ℕ sibling): a monotone {Unknown,True}-valued absorptive Path<Ternary>. Layer 2 (bounded): reaches_1_within(n, N) : Ternary True = reached 1 within N steps (IN) Unknown = not within N (U) (no False: "never reaches 1" has no finite certificate — the open problem, rendered honestly.)
- Copyright
- 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.
- Note
- "Mathematics is not yet ready for such problems." – Paul Erdős, on the Collatz conjecture.
Variable Documentation
◆ is_absorptive_sequence_v< dedekind::numbers::ReachPath >
|
inlineconstexprexport |
Opt-in: every ReachPath is absorptive (eventually constant: True once 1 is seen, or the constant Unknown). The shape is guaranteed by its only constructor, so the registration is sound.
