**Also known as: The Index Number (TIN)**
**Author:** S. R. Miller
**Date:** May 29, 2026
**Version:** V14.4.7
**License:** CC BY-SA 4.0
*Core philosophy, proof framework: S. R. Miller*
*Formal definitions, algorithm pseudocode: S. R. Miller and AI (DeepSeek), collaboratively.*
*Commercial use and modifications are permitted, provided attribution is given and shared under the same license.*
**Conception:** The core philosophy of this paper—the dual foundation of {0,1}* and SK calculus, the co-evolution mechanism, and the indexing philosophy—originates from the author.
**Formalization and Review:** The formal definitions, proof framework, and algorithm pseudocode in this paper were completed collaboratively by the author and AI (DeepSeek). The author provided direction and design decisions, while the AI assisted in executing rigorous formalization. The full text has undergone multiple rounds of review by the author, as well as auxiliary review by AI in the role of a critical reader. All raised issues have been addressed or explicitly noted as open problems.
**Statement:** The author assumes final responsibility for all content of this paper.
---
## Abstract
This paper defines **The Cosmic Number (TCN)**, the largest natural number indexable under a given capacity constraint. TCN is built upon two primitive concepts: {0,1}* (the set of all finite binary strings) and SK calculus (the minimal Turing-complete combinatory logic). All formal systems are encoded as SK terms, and through a co-evolution mechanism—where meta-interpreters and agents alternately enhance each other—all axiomatizable logical systems within the capacity are exhaustively enumerated. The numerical value is produced by the objective execution of SK reduction, rather than by semantic definition. The well-definedness of TCN relies on SK syntax, the inevitable termination of finite search, and the simplest induction on finite structures (used only in meta-level termination and uniqueness proofs). It does not depend on ZFC or any strong set theory. This paper provides the complete formal definition of TCN, its core theorems and their proofs, and proves that for sufficiently large C, C(C) > Rayo(C)—the fundamental reason being that TCN imposes no restriction on the logical order of candidate systems, whereas Rayo's number is restricted to first-order logic.
---
## Table of Symbols
| Symbol | Meaning |
|:------:|---------|
| **SK** | The set of legal terms of SK calculus |
| T | Formal system (agent) |
| U | The universe, {0,1}* |
| V_k | The k-th generation meta-interpreter |
| L_k | The k-th generation inspection depth, L_k = 2^k |
| → | One-step reduction |
| ⇒ | Material implication (in formula contexts) |
| →* | Multi-step reduction |
| ⊥ | The false constant |
| ¬P | P ⇒ ⊥ |
| = | Syntactic equality (for natural numbers) |
| ≈ | Reductional equality |
| Nat | The natural number predicate |
| Defined | The expression-defined predicate |
| succ | The successor function |
| ∧ | Conjunction (macro) |
---
## 0. Foundations
**Definition 0.1 (The Universe U)**
U = {0,1}*, the set of all finite binary strings. 0 and 1 are primitive concepts. U is the absolute domain of discourse for this paper.
**Definition 0.2 (SK Calculus)**
The set **SK** of legal terms of SK calculus is recursively defined:
1. S ∈ **SK**, K ∈ **SK**
2. If X ∈ **SK** and Y ∈ **SK**, then (XY) ∈ **SK**
Reduction rules (one-step reduction, denoted →): KXY → X; SXYZ → (XZ)(YZ). →* is the reflexive transitive closure of →. A normal form is a term that cannot be further reduced. S and K are primitive concepts. SK calculus is Turing-complete. SK calculus satisfies the Church-Rosser property.
**Definition 0.3 (The Interlock of Foundations)**
U and SK constitute a self-contained dual foundation: SK terms can be encoded into U; elements of U can be represented by SK terms; the capacity C constrains the length of SK terms; SK can describe the structure of U. The entire construction of this paper is derived from this.
**Definition 0.4 (Metatheoretic Commitments)**
The well-definedness of this paper relies on SK syntax, the inevitable termination of finite search, and the simplest induction on finite structures (used only in meta-level termination and uniqueness proofs). Induction does not appear in the object language of TCN—PROVER, SKPRA, and all candidate systems are pure SK terms. It does not depend on ZFC or any strong set theory. See Property 8.8 for details.
> **Note (Meta-language Clarification):** Concepts such as "finite set", "enumeration", and "sequence" used in this paper are all subject to hard constraints imposed by capacity C or depth L. Their meaning corresponds to operations mechanically realizable in bounded steps within SK calculus, requiring no external set theory as a foundation. Appendix A provides an algorithmic example of bounded enumeration.
---
## 1. Encoding
**Definition 1.1 (Symbol Encoding)**
A fixed 2-bit fixed-length encoding is adopted: S→00, K→01, (→10, )→11.
**Definition 1.2 (Term Encoding)**
For any legal SK term E, its symbol sequence is sequentially encoded to obtain a binary string ⟨E⟩. |E| = |⟨E⟩|, always even. The encoding is injective and decodable.
**Definition 1.3 (Capacity Parameters)**
C_prog, C_data ∈ N are independent parameters. C_prog is the maximum binary length for agent encoding, and C_data is the maximum binary length for candidate expressions. Abbreviated notation: C(C) = C(C, C).
**Definition 1.4 (Candidate Expression Space)**
E_data = { E ∈ **SK** | |E| ≤ C_data }, a finite set, where |E| denotes the binary encoding length of E (per Definition 1.2).
---
## 2. Binary Natural Numbers
**Definition 2.1 (Pair and Nil)**
Pair = the SK compilation of λx.λy.λf.f x y, Nil = K(SKK). Their sizes are constants, accounted for in C_prog.
**Definition 2.2 (Syntax)**
A legal binary natural number satisfies:
n := Nil
| (Pair K n) -- prepend 0 as high bit
| (Pair S n) -- prepend 1 as high bit
K = 0, S = 1, Nil = empty list (value 0). High-order bits come first. E.g., 5 (binary 101) = (Pair S (Pair K (Pair S Nil))).
**Definition 2.3 (Normalization)**
A normalized representation requires the highest bit to be S, or to be Nil. Non-normalized representations are excluded from formula spaces. Nil is the unique normalized representation of the value 0. Normalization ensures each natural number has a unique representation.
**Definition 2.4 (Size)**
|n|_bin = the SK encoding length of n. |Nil|_bin = c_nil, |(Pair K n)|_bin = c_pair + 2 + |n|_bin, |(Pair S n)|_bin = c_pair + 2 + |n|_bin. The length is Θ(log n).
**Definition 2.5 (Upper Bound)**
B(L) = the natural number value represented by the largest normalized binary natural number with size ≤ L. B(L) = 2^{Θ(L)}.
**Notation:** n_bin denotes the SK term corresponding to the normalized binary representation of the natural number n.
---
## 3. Formal Systems
**Definition 3.1 (Uniform Format)**
A formal system T is a finite list of SK terms [A_1, ..., A_m]. Each A_i is a closed λ-term of the form λv₁...λvₙ.Body, where Body consists of variables, binary natural numbers, ⇒, and ⊥.
Body may contain the following predicate and function symbols: Nat (unary predicate), Defined (unary predicate), = (binary predicate, syntactic equality of natural numbers), ≈ (binary predicate, reductional equality), succ (unary function), + (binary function), × (binary function), etc. ∀φ is treated as a bounded quantifier macro—the quantification domain is limited to terms in the formula space with size ≤ L. ∧ is a macro for (P ⇒ (Q ⇒ ⊥)) ⇒ ⊥.
**Encoding Scheme for Higher-Order Quantifiers:** A second-order quantifier ∀P (where P is a predicate variable) is encoded as bounded quantification over SK terms satisfying a specific type constraint. In the untyped SK framework, a predicate is a function returning a ⇒-type. ∀P. φ(P) is encoded as: for all SK terms P with size ≤ L that satisfy the predicate type constraint (i.e., P applied to any term t reduces to an expression of type ⇒ or ⊥), check whether φ(P) holds. This encoding is realizable in SK as a bounded search. Encodings for higher-order quantifiers are analogous. Definition 3.6 ensures that Prog imposes no restriction on logical order, thus the encoding scheme for higher-order systems is admitted by the framework.
Each axiom carries a tag bit: **CR** (Construction Rule) or **LA** (Logical Axiom). ⇒ is the logical implication built into PROVER, and ⊥ is the false constant. ¬P := P ⇒ ⊥.
All candidate systems accept a uniform formula language composed of SK terms, ⇒, and ⊥.
**Definition 3.2 (Encoding)**
⟨T⟩ is the binary string obtained by concatenating the axiom list in a prescribed format (1 tag bit + the SK encoding of the axiom). |T| = |⟨T⟩|.
**Definition 3.3 (Candidate Space)**
Prog = { T | |T| ≤ C_prog and ⟨T⟩ is legally decodable }. A finite set.
**Definition 3.4 (Sufficient Arithmetic)**
T satisfies sufficient arithmetic if and only if its axiom list contains formalizations of: binary natural number constructors (tagged CR), the successor function succ, addition and multiplication (in binary), and the induction axiom schema (tagged LA).
**Definition 3.4.1 (SKPRA — The Initial System)**
T_{-1} = SKPRA. A minimal arithmetic system natively defined on the SK substrate. Its axioms are written directly as SK terms.
**Construction Rules (CR):**
CR1-CR3 are meta-level primitive declarations—stating that Nil, K, S may serve as leaf nodes of construction trees without needing construction rules. They do not have λ-term forms and are not used by PROVER in CR matching. PROVER hardcodes Base = {Nil, K, S} in the leaf node check of Phase 1. Nil, although a derived term (K(SKK)), is specially treated as a primitive as the unique normalized representation of the natural number zero.
CR4: λA.λB.(⇒ (∧ (Defined A) (Defined B)) (Defined (A B)))
CR5: λn.(⇒ (Nat n) (Nat (Pair K n)))
CR6: λn.(⇒ (Nat n) (Nat (Pair S n)))
**Logical Axioms (LA):**
A1. Nat(Nil); ∀n.Nat(n) ⇒ Nat(Pair K n); ∀n.Nat(n) ⇒ Nat(Pair S n)
A2. Equality: reflexive, symmetric, transitive.
For natural numbers: ∀n,m. n = m ↔ same_nf(n,m).
Define x ≈ y as: ∃z. x →* z ∧ y →* z (x and y have a common reduct).
where same_nf is a syntactic judgment built into PROVER:
same_nf(Nil, Nil) = true
same_nf(Nil, (Pair _ _)) = false
same_nf((Pair _ _), Nil) = false
same_nf((Pair b1 n1), (Pair b2 n2)) = (b1 ≡ b2) ∧ same_nf(n1, n2)
same_nf(S, S) = true; same_nf(K, K) = true
same_nf(S, K) = false; same_nf(K, S) = false
same_nf(S, (Pair _ _)) = false; same_nf(K, (Pair _ _)) = false
same_nf((Pair _ _), S) = false; same_nf((Pair _ _), K) = false
≡ denotes syntactic identity.
> **Note on the distinction between = and ≈:** = is used only for syntactic equality of natural numbers (decidable in finite steps), while ≈ is used for reductional equivalence (potentially undecidable, but can be approximated within a bounded depth L). PROVER's same_nf implements the judgment of =. The contradiction check (Phase 3) and axiom instance judgment (Phase 1) use same_nf for syntactic identity checks.
A3. succ(Nil) = (Pair S Nil); recursive definition of binary addition.
A4. Primitive Recursive Definition Schema: For any function symbol f defined by SK terms, if f satisfies
f(Nil, x̄) = g(x̄)
f(succ(n), x̄) = h(n, f(n, x̄), x̄)
where g and h are already defined SK terms, then f is a legally defined primitive recursive function.
This schema is expanded into an independent axiom for each (g,h) pair.
A5. Induction Axiom Schema: φ(Nil) ⇒ (∀n.φ(n) ⇒ φ(succ n)) ⇒ ∀n.φ(n)
A6. SK Reduction Factuality: ∀x,y. x →* y ⇒ x ≈ y
**Encoding of SKPRA:** Each axiom is compiled into a pure SK term using the standard bracket abstraction algorithm. |SKPRA| is a finite constant (estimated on the order of 10³–10⁴ bits, depending on specific encoding details). Selected T_k in the evolution extend T_{k-1} and thus automatically inherit sufficient arithmetic.
**Definition 3.5 (Two-Layer Architecture)**
PROVER has a built-in syntactic recognizer for binary natural numbers (pattern matching). T recognizes natural numbers at the proof level via the Nat predicate. The normalized encoding guarantees a one-to-one correspondence between syntactic legality and standard natural numbers.
**Definition 3.6 (No Restriction on Logical Order)**
Prog imposes no restriction on the logical order of candidate systems. Any effectively axiomatizable system, as long as its encoding length ≤ C_prog and it satisfies sufficient arithmetic, is a legal candidate. The encoding scheme for higher-order quantifiers (Definition 3.1) ensures that higher-order logical systems can be expressed in the uniform format.
---
## 4. The Three-Layer Architecture
The core architecture of this paper is a three-layer separation: the computation layer performs objective reduction, the proof layer verifies construction processes, and the evolution layer exhaustively enumerates all paths.
**Definition 4.1 (Computation Layer — SK Reduction Executor)**
PROVER has a built-in capability for direct execution of SK reduction.
**Symbol Note:** In this paper, → denotes one-step SK reduction (Definition 0.2), while ⇒ denotes the logical implication built into PROVER (Definition 3.1). →* denotes multi-step reduction. In the proof layer, it is used to check equivalence; in the computation layer, it is used to execute reduction to produce numerical values. The underlying rules are identical; the purposes differ. ⇒ is a built-in logical connective inside PROVER—in Phase 1 (construction tree verification), the matching of CR axioms for internal nodes depends on the syntactic structure of ⇒; in Phase 3 (contradiction check), ⇒ is the core symbol of the detachment rule.
**One-Step Reduction:** Locate the leftmost outermost redex (of the form KXY or SXYZ) and perform reduction according to the left-outermost priority.
**Reduction Path:** A sequence of terms E = E₀ → E₁ → E₂ → ..., exhaustively enumerating all possible paths, each path taking at most L steps. The left-outermost strategy and exhaustive enumeration are equivalent regarding reachability of normal forms (guaranteed by Church-Rosser); exhaustive enumeration serves to capture all intermediate results.
**Result Collection:** If a legal normalized binary natural number n_bin is reached in ≤ L steps, record n; if a non-n_bin normal form or no normal form is reached, no value is produced. Non-terminating paths do not affect the exhaustive enumeration of other paths.
**Contribution of E:** If any reduction path of E reaches n_bin in ≤ L steps, then E contributes n. The Church-Rosser property guarantees that all paths reaching a normal form converge to the same normal form, so E contributes at most one definite value.
**Determinism:** For given E and L, the contribution of E is uniquely determined.
**Definition 4.2 (Formula Space)**
Given E ∈ E_data and L, F_L(E) is the minimal set satisfying the following conditions:
1. E ∈ F_L(E); ⊥ ∈ F_L(E)
2. All normalized binary natural numbers n with |n|_bin ≤ L are in F_L(E)
3. For all SK terms t₁,t₂ with size ≤ L, the atomic formulas Nat(t₁), Defined(t₁), t₁=t₂, t₁≈t₂, succ(t₁)=t₂ are in F_L(E)
4. If A,B ∈ F_L(E), then (⇒ A B) ∈ F_L(E)
5. All terms in F_L(E) have size ≤ L
Here "size" refers to the encoding length of the SK term per Definition 1.2. F_L(E) is parameterized by E to control the size of the formula space—for each E to be verified, axiom instances are searched within its local space. F_L(E) is finite.
**Definition 4.3 (Axiom Instance Judgment)**
P is an instance of axiom A = λv₁...λvₙ.Body iff ∃t₁,...,tₙ ∈ F_L(E) such that A t₁...tₙ →* P. The reduction is checked within ≤ L steps. If P is not reached within L steps, the judgment is false. Decided by bounded enumeration.
**Definition 4.4 (Uniform Proof)**
A uniform proof of depth ≤ L in T is a sequence of formulas (P₁,...,Pₘ), with m ≤ L, where each step is either an axiom instance or an application of the detachment rule (P_j = (⇒ P_k P_i)). Uniform proofs are used for contradiction checking. Construction tree verification uses construction trees, not uniform proofs.
**Definition 4.4.1 (Global Formula Space)**
G_L is the set of all legal formulas with size ≤ L constructed from ⇒, ⊥, binary natural numbers, and the predicate/function symbols allowed by Definition 3.1. G_L is finite. The contradiction check of Phase 3 enumerates all uniform proof sequences of depth ≤ L over G_L.
**Definition 4.5 (Proof Layer — Construction Tree Verification)**
T constructively defines E at depth L if and only if there exists a construction tree satisfying the following conditions.
> **Note:** All operations of construction tree verification are performed at the level of logical terms (before compilation). The SK compilation of axioms is used only for the encoding of SKPRA and the SK implementation of PROVER, and does not affect verification logic. Judgments of syntactic containment and syntactic identity are performed on logical terms.
1. **Tree Structure:** A finite binary tree, with node count ≤ L and depth ≤ L. Each node contains an SK term (its content).
2. **Leaf Nodes:** The content must be in Base = {Nil, K, S}. Leaf nodes are automatically legal. Nil, although a derived term, is specially treated as a primitive as the unique normalized representation of zero.
3. **Internal Nodes:** Divided into two types:
**Application Node:** If Content is of the form (t₁ t₂) with n=2 and t₁,t₂ ∈ DefinedExprs, it is automatically legal without needing CR matching. This reflects that application is a built-in operation of SK calculus—the combination of any two already defined expressions is automatically legal.
**CR Instance Node:** Otherwise, the node must correspond to an application of one of T's CR axioms. Conditions:
- The child node contents are t₁,...,tₙ (n ≥ 1)
- There exists a CR axiom A = λv₁...λvₙ.Body such that A t₁...tₙ →* Content
- Content syntactically contains all of t₁,...,tₙ as subterms (determined by traversing the syntax tree of Content)
- Each child tᵢ belongs to Base, or has been verified at a shallower level of the current construction tree
4. **Root Node:** The content is syntactically equal to E.
**Construction Tree Enumeration:** PROVER enumerates all binary trees of size ≤ L and verifies them node by node according to the conditions. The number of such binary trees is finite, so the search terminates. A system without CR axioms can only generate application nodes—i.e., it can only construct SK terms generated from S and K by finite applications.
**Definition 4.6 (PROVER)**
PROVER is a fixed SK term. It takes as input (⟨T⟩, L) and outputs a set of natural numbers N_L(T).
PROVER provides two equivalent interfaces:
- **Set-valued interface:** PROVER(⟨T⟩, L) returns the result set of N_L(T).
- **Judgment interface:** PROVER_accept(⟨T⟩, ⟨E⟩, n_bin, L) returns true if and only if E passes the construction tree verification in Phase 1 and reduces to n_bin in Phase 2.
PROVER has built-in the same_nf judgment (Definition 3.4.1 A2) and the n_bin recognition algorithm.
**Construction Approach for PROVER's SK Encoding:** PROVER can be encoded as an SK term. The construction approach is as follows:
1. **Data Representation:** The axiom table ⟨T⟩ is encoded as an SK term (SK representation of the binary string). Natural numbers use the binary encoding of Definition 2.2. Terms in the formula spaces F_L(E) and G_L use nested Pair structures.
2. **Bounded Loops:** The upper bounds of all enumerations (E_data, binary trees, reduction paths, proof sequences) are hard-constrained by L and C_data. Loops are realized via recursion using the Y combinator, with recursion depth limited by L.
3. **Pattern Matching:** Recognition of binary natural numbers, formula syntax checking, term size comparison, etc., are realized through structural traversal of SK terms.
4. **Reduction Execution:** The reduction rules of Definition 4.1 are executed directly by SK reduction—PROVER loads E and exhaustively searches its reduction paths.
5. **Fixed Size:** The SK encoding size of the above components is fixed (independent of C) because the control logic is fixed. L and C are not encoded as constants within PROVER's symbols, but are passed in as runtime parameters. The depth of bounded loops is controlled by the parameter L, via recursion with the Y combinator.
By the Turing-completeness of SK, this construction approach is realizable in SK. The exact SK encoding length of PROVER depends on specific implementation details, but its existence is guaranteed by the construction approach above. |PROVER| is a finite constant.
**Fixity of PROVER:** PROVER does not change with evolution. V_k = PROVER(⟨T_{k-1}⟩, 2^k).
Algorithm PROVER(⟨T⟩, L):
// Phase 0: Decoding
1. Decode ⟨T⟩ into axiom table A = [(tag₁,A₁), ..., (tagₘ,Aₘ)]
where each tagᵢ ∈ {CR, LA}, and each Aᵢ is a closed λ-term.
// Phase 1: Construction Tree Verification (Bottom-Up)
2. DefinedExprs = Base = {Nil, K, S}
3. For each E ∈ E_data (in ascending order of |E|):
// Note: By the subterm containment constraint on internal nodes,
// child size < parent size. Ascending order ensures children are
// verified before parents, consistent with bottom-up traversal.
4. Enumerate all binary trees Tree with node count ≤ L and depth ≤ L:
5. If the content of Tree's root node ≠ E: continue to next Tree
6. legal = true
7. Traverse nodes of Tree bottom-up:
8. If node is a leaf:
9. If node content ∉ Base: legal = false
10. If node is internal:
11. Get child content list Children = [t₁,...,tₙ] (n ≥ 1)
12. If any tᵢ ∉ DefinedExprs: legal = false
13. Get node content Content
14. If Content is of the form (t₁ t₂) and n=2 and t₁,t₂ ∈ DefinedExprs:
// Application node, automatically legal
15. continue (skip CR matching)
16. Else (CR instance node):
17. Check whether Content syntactically contains all t₁,...,tₙ as subterms
18. If not: legal = false
19. Check whether there exists a CR axiom Aⱼ of T and substitution u₁,...,uₙ ∈ F_L(E) such that:
20. Aⱼ u₁ ... uₙ →* Content
21. and same_nf(uᵢ, tᵢ) = true (for all i)
22. If no such CR axiom exists: legal = false
23. If legal = true:
24. Add E to DefinedExprs, break out of Tree enumeration for E
// Phase 2: Execute SK Reduction
25. Results = ∅
26. For each E ∈ DefinedExprs:
27. Exhaustively search all reduction paths of E (each path at most L steps, per Definition 4.1)
28. For each path:
29. If E reduces in ≤ L steps to some term M, and M is a legal normalized binary natural number n_bin:
30. Add n to Results
// n_bin recognition algorithm:
// Check whether M satisfies the syntax of Definition 2.2 and the normalization requirement of Definition 2.3.
// If M = Nil, recognize as value 0.
// If M = (Pair S rest), recursively recognize rest as value k, return 2k+1.
// If M = (Pair K rest), reject (non-normalized).
// This recognition is executed automatically in Phase 2 without adding to reduction step overhead.
// Phase 3: Contradiction Check
31. On the global formula space G_L (Definition 4.4.1), enumerate all possible uniform proof sequences of T within depth L (per Definition 4.4):
32. If there exists a proof sequence whose conclusion is ⊥:
33. Return ∅
34. Return Results
**Definition 4.7 (Tier Numerical Value)**
N_L(T) = max{ n | n ∈ result set }. If the result set is empty, N_L(T) = 0.
**Lemma (Uniqueness of N_L(T)):** For any T and L, N_L(T) is uniquely determined. E_data is finite, binary trees are finite, reduction paths are finite, Church-Rosser guarantees the contribution of E is unique, and the contradiction check judgment is unique. ∎
**Definition 4.8 (Meta-Interpreter)**
V_k = PROVER(⟨T_{k-1}⟩, 2^k). PROVER is used here in its set-valued interface.
---
## 5. Co-Evolution
**Definition 5.1 (Extension Relation)**
T_i ≼ T_j if and only if both conditions hold simultaneously:
1. Consistency Preservation: ∀E ∈ E_data, if PROVER_accept(⟨T_i⟩, ⟨E⟩, n, L) = true (for some n), then PROVER_accept(⟨T_j⟩, ⟨E⟩, n, L) = true (for the same n).
2. N_L(T_j) ≥ N_L(T_i)
Since E_data is finite and L is finite, condition 1 can be checked by finite enumeration, so ≼ is a decidable relation.
**Definition 5.2 (Progressive Depth Evolution)**
L_k = 2^k (for k ≥ 0). Initialization: T_{-1} = SKPRA, L_0 = 1, Active_{-1} = {T_{-1}}, History = ∅.
For generation k (k = 0,1,2,...):
1. For each T ∈ Active_{k-1}, compute N_{L_k}(T) using depth L_k. The computation includes the contradiction check of PROVER Phase 3. If PROVER returns an empty set (contradiction), T is judged contradictory. If the new value exceeds the record for that system in History, update History.
2. Mark systems judged contradictory in Step 1 as "contaminated" and remove them from Active. Only the contradictory system itself is marked; its descendants are not marked—descendant systems will be independently evaluated in their respective evolutionary branches.
3. For each uncontaminated T, construct Cand(T) = { T' ∈ Prog | T ≼ T' }.
4. For each candidate T', compute N_{L_k}(T') (including contradiction check) using depth L_k. Remove candidates that return an empty set.
5. Active_k = uncontaminated systems from Active_{k-1} ∪ newly screened candidates.
6. If Active_k = Active_{k-1} and no N_{L_k} has increased compared to the previous generation, terminate; Final = Active_k.
> **Note:** The depth L* at evolutionary termination is the actual computation depth and does not guarantee exclusion of all inconsistent systems—absolute consistency is undecidable in principle. TCN indexes the maximum output of systems that appear consistent within depth L*. This is a constitutive feature of the bounded consistency framework, driven by Gödel's theorem.
7. Otherwise, set L_{k+1} = 2^{k+1} and continue.
**Definition 5.3 (Historical Maximum Retention)**
History records the maximum N_L value of every system across all generations. Even if a system is later removed due to contradiction, its historical maximum is retained. This means the final C(C) may include numerical values from systems later discovered to be contradictory—these values were produced at shallower depths when the contradiction had not yet been exposed. TCN does not claim these values come from absolutely consistent systems, only that they come from systems that appeared consistent at the depth when they were produced.
**Definition 5.4 (Termination)**
**Lemma:** The evolution necessarily terminates.
*Proof:* (1) Prog is finite—there are only finitely many binary strings of length ≤ C_prog. (2) Active expands monotonically and is ⊆ Prog; a monotonically expanding sequence on a finite set must saturate. (3) For a fixed T, N_L(T) is not necessarily monotonic as L increases—greater depth may reveal a contradiction, leading to an empty set being returned. However, History records the maximum value produced by each system at any depth, so History itself is monotonically non-decreasing with evolution. The condition "no N_{L_k} has increased" in the termination check means that for all systems in Active, their N values at the current depth L_k have not increased relative to the previous depth L_{k-1}. (4) N_L is bounded by B(L), and the N_L values of systems in Active, fluctuating within a bounded range, must saturate after finitely many steps. Therefore, the termination condition must be satisfied within finitely many generations. ∎
---
## 6. The Cosmic Number
**Definition 6.1**
C(C_prog, C_data) = max( History ∪ { N_{L(T)}(T) | T ∈ Final } ), where L(T) is the depth at termination.
**Definition 6.2**
C(C) = C(C, C).
**Monotonicity:** ∀C₁ ≤ C₂, C(C₂) ≥ C(C₁).
**Definition 6.3 (Boundary Cases)**
- C < C_min: Prog is empty; only SKPRA evolves to saturation. C(C) = N_{L*}(SKPRA).
- C = C_min: Prog contains only SKPRA itself; evolves to saturation. C(C_min) = N_{L*}(SKPRA).
- C > C_min: Normal evolution.
C_min = max(|SKPRA|, |PROVER|). |SKPRA| is estimated on the order of 10³–10⁴ bits; |PROVER| is a finite constant. C_min is a finite constant. For all C, C(C) ≥ N_{L*}(SKPRA).
---
## 7. Core Theorems
**Theorem 7.1 (Well-Definedness)**
For any C_prog, C_data, C(C_prog, C_data) exists and is unique.
*Proof:* Prog is finite, E_data is finite, evolution necessarily terminates (Definition 5.4), History and Final are finite sets, and N_L is unique (Definition 4.7 Lemma). PROVER is a fixed SK term (Definition 4.6) whose size |PROVER| is constant. The maximum value is uniquely determined by definition. ∎
**Theorem 7.2 (Bounded Maximality within Capacity)**
Given capacity C and evolutionary termination depth L*, TCN(C) is the largest natural number indexable by the rules defined in this paper (including historical maximum retention). This maximality holds within the bounded consistency framework—TCN does not guarantee that this value comes from an absolutely consistent system, only that it comes from a system that appeared consistent at the depth when it was produced.
*Proof:* Prog exhaustively enumerates all systems, E_data exhaustively enumerates all expressions, the evolution tree exhaustively enumerates all paths, and History retains all historical maxima. ∎
**Theorem 7.3 (Existence of a Universal Indexing Function Φ)**
There exists a unified SK term Φ such that for any c ∈ N, Φ c̄_bin →* the binary representation of C(c,c).
*Proof:* The indexing process is described by a fixed algorithm: decode parameter c, construct Prog = {T | |T| ≤ c}, execute progressive depth evolution (Definition 5.2), and compute the maximum of History and Final. The control logic of this algorithm does not depend on c. The entire process constitutes a definite computable function. By the Turing-completeness of SK, there exists an SK term Φ computing this function. ∎
**Theorem 7.4 (Surpassing Rayo's Number)**
For sufficiently large C, C(C) > Rayo(C).
*Proof:*
Define **Rayoₙ(C):** The largest natural number definable in n-th order logic with at most C symbols (definition rule analogous to Rayo's number—take the supremum of all definable natural numbers + 1. The truth predicate is defined in the (n+1)-th order language; Tarski's theorem only prohibits a language from defining its own truth predicate, not a higher-order language from defining the truth predicate of a lower-order language). The original Rayo number is Rayo₁(C).
**Step 1: Rayo's Framework Restriction.** Rayo(n) is defined using the language of first-order set theory. Its symbol set is Σ₁ (containing variables, ∈, =, ¬, ∧, ∃, parentheses, etc.). The expressive power of first-order logic is limited to quantification over individual variables—it cannot quantify over predicates or relations.
**Step 2: TCN's Candidate Space Has No Restriction on Logical Order.** Prog imposes no restriction on the logical order of candidate systems (Definition 3.6). The encoding scheme for higher-order quantifiers (Definition 3.1) guarantees that second-order and higher-order logical systems can be expressed in the uniform format. Therefore, for any finite order n, there exists an n-th order logical system in Prog (when C is sufficiently large).
**Step 3: Higher-Order Logic is Strictly Stronger Than First-Order Logic.** Second-order logic can quantify over predicates, and thus can define the truth predicate of a first-order language (Tarski's theorem only prohibits a first-order language from defining its own truth predicate, not a higher-order language from defining the truth predicate of a lower-order language). Third-order logic can define the truth predicate of second-order logic, and so on. Each increase in order brings a strict increase in expressive power. This is a standard result in combinatory logic and proof theory.
**Step 4: Encoding Efficiency Argument.** The axiomatization of second-order logic (including the axiom schema defining the first-order truth predicate) can be completed within a constant-length axiom table. Thus, when C is sufficiently large, the second-order system T₂ itself can be encoded within length |T₂| (a constant), leaving at least C - |T₂| space for defining natural numbers. |T₂| is the constant overhead. Under a 2-bit fixed-length encoding, the symbol table of (n+1)-th order logic has finitely many more symbols than that of n-th order logic (e.g., extra predicate variable symbols). Denote this overhead by the constant Δ. When capacity C is sufficiently large (C >> Δ), the effective number of symbols available for defining natural numbers in (n+1)-th order logic is at least C - Δ, compared to C for n-th order logic. Since expressive power strictly increases with order, there exists a sufficiently large C such that the natural numbers definable in (n+1)-th order logic within capacity C are strictly larger than those definable in n-th order logic within the same capacity.
In particular, taking n=1 (first-order logic, Rayo's framework), second-order logic can define strictly larger natural numbers than first-order logic under the same capacity C. That is, Rayo₂(C) > Rayo₁(C) = Rayo(C) for sufficiently large C.
**Step 5: TCN Takes the Maximum.** Prog contains second-order logical systems (when C is sufficiently large). These systems produce numerical values through construction tree verification and SK reduction. The Cosmic Number C(C) takes the maximum of History and Final, encompassing the output of all candidate systems. Therefore, for sufficiently large C:
C(C) ≥ Rayo₂(C) > Rayo(C)
**Step 6: Strict Inequality.** By the same reasoning, third-order logic can define the truth predicate of second-order logic, producing output strictly larger than that of second-order logic under the same capacity. For any fixed finite order n, the (n+1)-th order logical system T_{n+1} enters Prog when C is sufficiently large, and N(T_{n+1}) > Rayoₙ(C). Since Prog imposes no upper limit on logical order, TCN takes the maximum over all finite-order systems, which is strictly larger than Rayoₙ(C) for any fixed finite order n. In particular, taking n=1, C(C) > Rayo₁(C) = Rayo(C).
**Conclusion:** The fundamental reason TCN strictly exceeds Rayo's number is that TCN imposes no restriction on the logical order of candidate systems, whereas Rayo's number is restricted to first-order logic. Under comparable encoding efficiency, the expressive power of higher-order logic is strictly stronger than that of first-order logic. By exhaustively enumerating systems of all orders and taking the maximum, TCN necessarily transcends any fixed-order framework. ∎
---
## 8. Properties
**8.1 (Finiteness and Monotonicity)**
C(C) ∈ N, and C(C) is monotonically non-decreasing as C increases.
**8.2 (Bounded Maximality within Capacity)**
Given capacity and bounded depth L*, TCN is the largest natural number indexable by the rules of this paper. This is a restatement of Theorem 7.2.
**8.3 (Co-Evolution and Exhaustive Evolution Tree)**
The judge co-evolves with the judged. The evolution tree exhaustively enumerates all paths. All systems are continuously re-evaluated. The paths of inconsistent systems eventually terminate due to contradiction, but their historical contributions are retained. Paths of consistent systems develop independently to the capacity limit.
**8.4 (Construction Tree Verification)**
T must pass construction tree verification for an expression to enter the computation layer. Internal nodes are divided into application nodes (automatically legal) and CR instance nodes (for custom constructors). A system without CR axioms can only generate application nodes. This ensures that N_L reflects true logical strength, giving evolution a directional character.
**8.5 (Three-Layer Architecture)**
The computation layer is objective and mechanical; reduction behavior is independent of all formal systems. The proof layer defines the construction process of E via construction rules, with PROVER performing syntactic verification. The evolution layer exhaustively enumerates all paths, with historical maximum retention ensuring monotonicity. The three layers check and balance one another.
**8.6 (Transcending Logical Orders)**
Prog imposes no restriction on logical order. TCN is not limited by any fixed logical type. Theorem 7.4 provides a rigorous proof that it surpasses Rayo's number—the fundamental reason being that the expressive power of higher-order logic is strictly stronger than that of first-order logic.
**8.7 (Relation to Rayo's Number)**
Theorem 7.4 has rigorously proven that for sufficiently large C, C(C) > Rayo(C). The fundamental mechanism by which TCN surpasses Rayo's number is not "simulating" Rayo's semantic construction, but exploiting the unrestricted logical order of the candidate space—higher-order logic has strictly stronger expressive power than first-order logic under equivalent encoding capacity.
**8.7.1 (Response to Gödel's and Tarski's Theorems)**
**Gödel's Second Incompleteness Theorem:** This paper does not require systems to prove their own consistency. Contradiction checking is cross-system, depth-bounded, and exhaustively searched. TCN replaces absolute consistency with freedom from contradiction within a bounded depth L*—absolute consistency is undecidable in principle. History may contain values from systems later found contradictory—these values were produced at depths where they appeared consistent.
**Tarski's Undefinability Theorem:** The proof of Theorem 7.4 does not rely on constructing a "truth predicate for the set-theoretic universe V" within TCN. The argument relies solely on the standard result that higher-order logic is strictly stronger than first-order logic—second-order logic can define the truth predicate of first-order logic (which does not trigger Tarski's paradox, because a second-order language defines the truth of a lower-order language), third-order can define the truth of second-order, and so on.
**8.8 (Bounded Consistency Framework and Metatheoretic Commitments)**
The well-definedness of TCN relies on SK syntax, the inevitable termination of finite search, and the simplest induction on finite structures (used only in meta-level termination and uniqueness proofs). Induction does not appear in TCN's object language—PROVER, SKPRA, and all candidate systems are pure SK terms. It does not depend on ZFC or any strong set theory. In comparison with 's number: depends on ZFC to prove strong normalization, whereas TCN's metatheoretic commitments are weaker. TCN indexes the maximum output of systems that appear consistent within the evolutionary termination depth L*, as well as the maxima historically produced—this is a constitutive feature of the bounded consistency framework.
**8.9 (Physical Inaccessibility)**
For sufficiently large C, the evolution tree and exhaustive reduction grow at a super-exponential rate and are physically unexecutable. The numerical value is physically inaccessible but indexable in principle.
**8.10 (Philosophical Note — Unintelligibility)**
Co-evolution exhaustively enumerates all encodable formal systems within capacity C, including logical types never defined by humans. The final numerical value may transcend human cognition. The rules of this paper serve solely as an index.
---
## 9. Commentary and Comparison
**Characteristics of TCN:** Dual foundation of {0,1}* and SK; evolutionary starting point SKPRA; three-layer architecture; construction tree verification (application nodes + CR instance nodes); historical maximum retention and progressive depth evaluation ensuring monotonicity; precise reduction rules; executable PROVER algorithm (|PROVER| constant, parameter L passed via Y combinator); explicit proofs of N_L uniqueness and termination; contradiction check by detecting ⊥; complete treatment of boundary cases; no restriction on logical order; explicit encoding scheme for higher-order quantifiers; native binary encoding; metatheoretic commitment limited to simplest induction; response to Gödel and Tarski; existence of a universal indexing function Φ; rigorous proof of surpassing Rayo's number (based on higher-order logic > first-order logic).
**Comparison with Classic Large Numbers:**
| Large Number | Core Mechanism | External Dependency | Logical Restriction | Value Production | Judge | Monotonicity | Well-Definedness | Metatheoretic Strength |
|:------------:|:--------------:|:-------------------:|:-------------------:|:----------------:|:----:|:------------:|:----------------:|:----------------------:|
| Rayo's number | Truth in 1st-order set theory | ZFC + truth predicate | 1st-order logic | Semantic definition | Fixed | Monotonic | Depends on metatheory | ZFC |
| 's number | Calculus of constructions | ZFC | Fixed strength | Computational reduction | Fixed | Monotonic | Gold standard | ZFC |
| **TCN** | **Co-evolution + SK reduction** | **Simplest induction** | **Unrestricted** | **Computational reduction** | **Evolving** | **Monotonic** | **Gold standard** | **Bounded arithmetic** |
---
## 10. Formal Summary
The Cosmic Number (TCN) Also known as: The Index Number (TIN)
Foundation: U = {0,1}*, SK: S, K, application, KXY→X, SXYZ→(XZ)(YZ)
Church-Rosser property holds
Metatheory: Simplest induction (used only in meta-level proofs; not present in object language)
Encoding: 2-bit fixed-length: S=00, K=01, (=10, )=11
Parameters: C_prog, C_data ∈ N, C(C) = C(C, C)
C_min = max(|SKPRA|, |PROVER|), both finite constants
Binary Natural Numbers: Nil=0, K=0, S=1, Pair construction, big-endian, normalized
same_nf: Syntactic equivalence judgment built into PROVER
= denotes syntactic equality (natural numbers), ≈ denotes reductional equality
Candidate Systems: Prog = { T | |T| ≤ C_prog, legal axiom table (with CR/LA tags) }
Axioms: λv₁...λvₙ.Body (variables + binary numbers + ⇒ + ⊥ + predicate/function symbols)
∀ is a bounded quantifier macro, ∧ is a ⇒/⊥ macro
Higher-order quantifiers: Bounded quantification over SK terms satisfying type constraints
Initial System SKPRA: CR1-CR6, logical axioms A1-A6
A2: Natural number syntactic equality = and reductional equality ≈
A6: x→*y ⇒ x≈y
Three-Layer Architecture:
Computation layer: SK reduction executor (left-outermost priority, exhaustive paths, Church-Rosser)
Proof layer: Construction tree verification (bottom-up, leaves ∈ Base,
internal = application nodes (auto-legal) or CR instance nodes (subterm containment constraint))
Evolution layer: Exhaustive evolution tree + progressive depth evaluation + historical maxima
PROVER Algorithm:
Construction approach: Data representation + bounded loops + pattern matching + reduction execution, fixed size
L and C passed as runtime parameters (not encoded in PROVER's symbols)
Phase 1: Construction tree verification (bottom-up, E in ascending size order)
Phase 2: Execute SK reduction
Phase 3: Contradiction check (global formula space G_L, whether ⊥ is proved)
Evolution: Active expands monotonically to saturation
N_L(T) not guaranteed monotonic, but History is monotonically non-decreasing
Only the contradictory system itself is marked; descendants are not marked
TCN(C) = max(History ∪ {N_L(T) | T ∈ Final}), monotonically non-decreasing
Surpassing Rayo's number: C(C) > Rayo(C) for sufficiently large C
Fundamental reason: Higher-order logic has strictly stronger expressive power than first-order logic
Properties: Well-defined (gold standard), simplest induction metatheoretic commitment,
transcends logical orders, strictly surpasses Rayo's number,
bounded consistency framework, responds to Gödel and Tarski
---
## Appendix A: Algorithmic Example of Bounded Enumeration
The following demonstrates the algorithm for "enumerating all terms of size ≤ L and filtering legal binary trees."
Generate(L):
Terms = {S, K}
For depth d = 1 to L:
For each pair (A, B) ∈ Terms × Terms:
If |(A B)| ≤ L:
Terms = Terms ∪ {(A B)}
Return Terms
FilterTrees(Terms):
Trees = ∅
For each t ∈ Terms:
If IsTree(t):
Trees = Trees ∪ {t}
Return Trees
The IsTree judgment is realized through recursive pattern matching. All enumeration processes involved in TCN can similarly be realized in SK as bounded loops—the size of the search space is always explicitly constrained by C or L.
---
## References
1. Rayo, A. (2007). "Big Number Duel." MIT Big Number Duel.
2. , R. (2001). "A C program that outputs a large number."
3. Gödel, K. (1931). "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I." *Monatshefte für Mathematik und Physik*, 38, 173-198.
4. Tarski, A. (1936). "Der Wahrheitsbegriff in den formalisierten Sprachen." *Studia Philosophica*, 1, 261-405.
5. Curry, H. B., & Feys, R. (1958). *Combinatory Logic, Volume I*. North-Holland.
6. Schönfinkel, M. (1924). "Über die Bausteine der mathematischen Logik." *Mathematische Annalen*, 92, 305-316.
7. Church, A., & Rosser, J. B. (1936). "Some properties of conversion." *Transactions of the American Mathematical Society*, 39, 472-482.
8. Fish (2003). "Fish number 7." Googology Wiki.
source & further reading
gist.github.com — original article
AI use policy for Honeybadger blog
Claude Code skill: turn a session's findings into a self-contained HTML report (with Markdown source). Drop into ~/.claude/skills/html-report/SKILL.md.
Государство как машина стабильной коррупци.md