Apoth3osis
Paper → Proof → Code/Hybrid Zeckendorf
>_PROJECT.HYBRID_ZECKENDORF

Hybrid Hierarchical Representation of Numbers
Based on the Zeckendorf System

A Synthesis of Sparsity and Efficiency

Vladimir Veselov | Russian Academy of Sciences, Moscow | February 26, 2026

DOWNLOAD PAPER (PDF)LEAN 4 PROOFSVERIFIED CSAFE RUST

Abstract

This paper proposes a novel approach to the representation and processing of non-negative integers, combining the hierarchical sparse weight structure introduced by V. Veselov with the canonical Zeckendorf representation based on Fibonacci numbers. The hybrid model is designed for compact storage and accelerated arithmetic processing of giant numbers with extremely low density of non-zero “units” (ρ<10−3\rho < 10^{-3}). Empirical estimates indicate a potential speedup of 100–500 times compared to standard arbitrary-precision libraries for specific problem classes in cryptography and computer algebra.

Modules

6

Lean 4 files

Theorems

24

Machine-verified

Lines

872

Proof code

Sorry

0

Zero gaps

Audit Rounds

4

Hostile audits passed

>_PROOF.FLOW

Paper ↔ Proof Correspondence

Every section of the paper that defines a structure, algorithm, or theorem has a corresponding Lean 4 module with a machine-checked proof. Sections without a Lean counterpart are expository (introduction, applications, conclusion).

Paper SectionLean ModuleStatus
1expositoryN/A
2.1WeightSystem.leanPROVED
2.2FibIdentities.leanPROVED
2.3HybridNumber.leanPROVED
2.4Normalization.leanPROVED
3.1Addition.leanPROVED
3.2Multiplication.leanPROVED
3.3Normalization.leanPROVED
4Multiplication.lean (density)PROVED
5expositoryN/A
6expositoryN/A
7expositoryN/A
8expositoryN/A
>_PROOF.BLUEPRINT

Proof Modules

Each module below shows two views. Mathematics renders the definitions and theorems in standard mathematical notation. Lean 4 shows the corresponding formal proof code.

WeightSystem

HeytingLean/Bridge/Veselov/HybridZeckendorf/WeightSystem.lean | 78 lines | Paper 2.1 Weight System

WeightSystem.lean

Super-exponential weight hierarchy defining the level structure of hybrid numbers.

Definitions

w0=1,w1=1000,wi+2=wi+1 2w_0 = 1, \quad w_1 = 1000, \quad w_{i+2} = w_{i+1}^{\,2}

Recurrence defining the weight sequence

Verified Theorems

QED
∀ i∈N,wi+1=10002i\forall\, i \in \mathbb{N},\quad w_{i+1} = 1000^{2^i}
weight_closed|Closed-form expression for all levels above 0
QED
∀ i∈N,wi>0\forall\, i \in \mathbb{N},\quad w_i > 0
weight_pos|All weights are strictly positive
QED
i<j  ⟹  wi<wji < j \;\Longrightarrow\; w_i < w_j
weight_strict_mono|The weight sequence is strictly increasing

FibIdentities

HeytingLean/Bridge/Veselov/HybridZeckendorf/FibIdentities.lean | 44 lines | Paper 2.2 Fibonacci Coefficients

FibIdentities.lean

Fibonacci recurrence identities used by intra-level normalization rewrite rules.

Definitions

eval⁡(z)=∑k∈zFkwhere Fk=fib(k)\operatorname{eval}(z) = \sum_{k \in z} F_k \quad \text{where } F_k = \text{fib}(k)

Lazy Zeckendorf payload evaluation via Fibonacci sum

Verified Theorems

QED
2 Fk+2=Fk+3+Fk2\,F_{k+2} = F_{k+3} + F_k
fib_double_identity|Duplicate rewrite rule: two copies of F_{k+2} can be replaced
QED
eval⁡(z1+ ⁣+z2)=eval⁡(z1)+eval⁡(z2)\operatorname{eval}(z_1 \mathbin{+\!+} z_2) = \operatorname{eval}(z_1) + \operatorname{eval}(z_2)
lazyEvalFib_append|Evaluation distributes over list concatenation

HybridNumber

HeytingLean/Bridge/Veselov/HybridZeckendorf/HybridNumber.lean | 141 lines | Paper 2.3 Structure of a Hybrid Number (Def 2.1)

HybridNumber.lean

Core hybrid number type as a finitely-supported map from levels to Zeckendorf payloads, with evaluation and embedding.

Definitions

X:N→finZeckPayloadX : \mathbb{N} \to_{\text{fin}} \text{ZeckPayload}

A hybrid number is a finitely-supported function from levels to payloads

eval⁡(X)=∑i∈supp⁡(X)levelEval⁡(Xi)⋅wi\operatorname{eval}(X) = \sum_{i \in \operatorname{supp}(X)} \operatorname{levelEval}(X_i) \cdot w_i

Total semantic value: weighted sum over active levels

fromNat⁡(n)=single⁡0(zeckendorf⁡(n))\operatorname{fromNat}(n) = \operatorname{single}_0(\operatorname{zeckendorf}(n))

Embed a natural number at level 0 using its canonical Zeckendorf representation

Verified Theorems

QED
eval⁡(A+B)=eval⁡(A)+eval⁡(B)\operatorname{eval}(A + B) = \operatorname{eval}(A) + \operatorname{eval}(B)
eval_add|Evaluation is a homomorphism with respect to addition
QED
eval⁡(single⁡i(z))=levelEval⁡(z)⋅wi\operatorname{eval}(\operatorname{single}_i(z)) = \operatorname{levelEval}(z) \cdot w_i
eval_single|Evaluation of a single-level number
QED
eval⁡(fromNat⁡(n))=n\operatorname{eval}(\operatorname{fromNat}(n)) = n
eval_fromNat|Round-trip: embedding then evaluating recovers the original

Addition

HeytingLean/Bridge/Veselov/HybridZeckendorf/Addition.lean | 60 lines | Paper 3.1 Addition (Algorithm 1)

Addition.lean

Lazy level-wise addition by payload concatenation, followed by normalization for canonical output.

Definitions

add⁡(A,B)=normalize⁡(addLazy⁡(A,B))\operatorname{add}(A, B) = \operatorname{normalize}(\operatorname{addLazy}(A, B))

Canonical addition: lazy merge then full normalization

Verified Theorems

QED
eval⁡(add⁡(A,B))=eval⁡(A)+eval⁡(B)\operatorname{eval}(\operatorname{add}(A, B)) = \operatorname{eval}(A) + \operatorname{eval}(B)
add_correct|Correctness: addition preserves semantic value
QED
eval⁡(add⁡(A,B))=eval⁡(add⁡(B,A))\operatorname{eval}(\operatorname{add}(A, B)) = \operatorname{eval}(\operatorname{add}(B, A))
add_comm_eval|Commutativity at the semantic level

Normalization

HeytingLean/Bridge/Veselov/HybridZeckendorf/Normalization.lean | 353 lines | Paper 2.4 + 3.3 Normalization (Algorithms 1, 3)

Normalization.lean

Two-stage normalization: bounded intra-level rewriting via Fibonacci identities, then inter-level Euclidean carry propagation.

Definitions

intraStep⁡:{[a, a, …]↦[a+1, a−2, …]duplicate (a≥2)[a, a+1, …]↦[a+2, …]consecutive\operatorname{intraStep} : \begin{cases} [a,\, a,\, \ldots] \mapsto [a{+}1,\, a{-}2,\, \ldots] & \text{duplicate } (a \geq 2) \\ [a,\, a{+}1,\, \ldots] \mapsto [a{+}2,\, \ldots] & \text{consecutive} \end{cases}

Single rewrite step using Fibonacci identities

carryAt⁡(i,X):q=⌊ciwi⌋,  r=ci mod wi⇒Xi′←zeck⁡(r),  Xi+1′←zeck⁡(ci+1+q)\operatorname{carryAt}(i, X) : \quad q = \left\lfloor \frac{c_i}{w_i} \right\rfloor,\; r = c_i \bmod w_i \quad \Rightarrow \quad X_i' \leftarrow \operatorname{zeck}(r),\; X_{i+1}' \leftarrow \operatorname{zeck}(c_{i+1} + q)

Inter-level carry: Euclidean division propagates overflow upward

Verified Theorems

QED
eval⁡(intraStep⁡(z))=eval⁡(z)\operatorname{eval}(\operatorname{intraStep}(z)) = \operatorname{eval}(z)
intraStep_preserves_eval|Each rewrite step preserves the payload's Fibonacci-sum value
QED
levelEval⁡(intraNormalize⁡(z))=lazyEvalFib⁡(z)\operatorname{levelEval}(\operatorname{intraNormalize}(z)) = \operatorname{lazyEvalFib}(z)
intraNormalize_sound|Intra-normalization preserves the per-level semantic value
QED
IsZeckendorfRep⁡(intraNormalize⁡(z))\operatorname{IsZeckendorfRep}(\operatorname{intraNormalize}(z))
intraNormalize_canonical|Output satisfies the Zeckendorf canonicality predicate (no duplicates, no consecutives)
QED
eval⁡(normalize⁡(X))=lazyEval⁡(X)\operatorname{eval}(\operatorname{normalize}(X)) = \operatorname{lazyEval}(X)
normalize_sound|Full normalization preserves the total semantic value
QED
IsCanonical⁡(normalize⁡(X))\operatorname{IsCanonical}(\operatorname{normalize}(X))
normalize_canonical|Every level of the output is in canonical Zeckendorf form

Multiplication

HeytingLean/Bridge/Veselov/HybridZeckendorf/Multiplication.lean | 213 lines | Paper 3.2 Multiplication (Algorithm 2) + Section 4

Multiplication.lean

Structural multiplication via bounded level fold, with halving/doubling primitives and density analysis.

Definitions

multiply⁡(A,B)=∑i=0d−1repeatAdd⁡ ⁣(A,  levelEval⁡(Bi)⋅wi)\operatorname{multiply}(A, B) = \sum_{i=0}^{d-1} \operatorname{repeatAdd}\!\left(A,\; \operatorname{levelEval}(B_i) \cdot w_i\right)

Binary multiplication: bounded fold over B's support depth d

ρ(X)=∣supp⁡(X)∣log⁡φ ⁣(eval⁡(X)),φ=1+52\rho(X) = \frac{|\operatorname{supp}(X)|}{\log_\varphi\!\bigl(\operatorname{eval}(X)\bigr)}, \quad \varphi = \tfrac{1+\sqrt{5}}{2}

Density statistic measuring sparsity relative to the golden ratio

Verified Theorems

QED
0<i  ⟹  2∣wi0 < i \;\Longrightarrow\; 2 \mid w_i
weight_even_of_pos|All positive-level weights are even (enables structural halving)
QED
eval⁡(double⁡(X))=2⋅eval⁡(X)\operatorname{eval}(\operatorname{double}(X)) = 2 \cdot \operatorname{eval}(X)
doubleHybrid_correct
QED
eval⁡(halve⁡(X))=⌊eval⁡(X)2⌋\operatorname{eval}(\operatorname{halve}(X)) = \left\lfloor \frac{\operatorname{eval}(X)}{2} \right\rfloor
halveHybrid_correct
QED
eval⁡(repeatAdd⁡(A, n))=eval⁡(A)⋅n\operatorname{eval}(\operatorname{repeatAdd}(A,\, n)) = \operatorname{eval}(A) \cdot n
repeatAdd_correct
QED
eval⁡(multiply⁡(A, B))=eval⁡(A)⋅eval⁡(B)\operatorname{eval}(\operatorname{multiply}(A,\, B)) = \operatorname{eval}(A) \cdot \operatorname{eval}(B)
multiplyBinary_correct|Correctness of structural multiplication
>_DEPENDENCY.GRAPH

Module Dependencies

Hover over a module to trace its imports. Solid lines show direct dependencies; dashed lines show transitive imports used for specific operations.

FOUNDATIONCORE TYPEALGORITHMSTOP-LEVELWeightSystemFibIdentitiesHybridNumberNormalizationAdditionMultiplication
Foundation Core Type Algorithm Top-levelimportstransitive
>_VERIFIED.C

Verified C Artifacts

Generated via CAB pipeline: Lean 4 → LambdaIR → MiniC → C. Each file carries a correctness certificate verifying semantic preservation.

C

hybrid_zeckendorf_weight.c

Weight sequence computation | from WeightSystem

DOWNLOAD
C

hybrid_zeckendorf_fib.c

Fibonacci identity helpers | from FibIdentities

DOWNLOAD
C

hybrid_zeckendorf_eval.c

Evaluation and constructors | from HybridNumber

DOWNLOAD
C

hybrid_zeckendorf_add.c

Lazy addition | from Addition

DOWNLOAD
C

hybrid_zeckendorf_normalize.c

Two-stage normalization | from Normalization

DOWNLOAD
C

hybrid_zeckendorf_multiply.c

Structural multiplication | from Multiplication

DOWNLOAD
>_SAFE.RUST

Safe Rust Artifacts

Transpiled from verified C to idiomatic safe Rust. Raw pointers replaced with owned types, slices, and iterators. Correctness inherited from the C verification chain. Download the full crate (includes Cargo.toml and lib.rs) and run cargo test.

Rs

Cargo.toml

Crate manifest (cargo build) | from Crate

DOWNLOAD
Rs

lib.rs

Crate root — declares all modules | from Crate

DOWNLOAD
Rs

hybrid_zeckendorf_weight.rs

Weight sequence (safe Rust) | from WeightSystem

DOWNLOAD
Rs

hybrid_zeckendorf_fib.rs

Fibonacci helpers (safe Rust) | from FibIdentities

DOWNLOAD
Rs

hybrid_zeckendorf_eval.rs

Eval and constructors (safe Rust) | from HybridNumber

DOWNLOAD
Rs

hybrid_zeckendorf_add.rs

Lazy addition (safe Rust) | from Addition

DOWNLOAD
Rs

hybrid_zeckendorf_normalize.rs

Normalization (safe Rust) | from Normalization

DOWNLOAD
Rs

hybrid_zeckendorf_multiply.rs

Multiplication (safe Rust) | from Multiplication

DOWNLOAD
>_PROVENANCE

Provenance Chain

1

Research Paper

Veselov, V. “Hybrid Hierarchical Representation of Numbers Based on the Zeckendorf System.” February 2026. Defines Def 2.1, Algorithms 1-3, complexity analysis.

2

Lean 4 Formalization

6 modules, 24 theorems, 872 lines. Kernel-verified by Lean 4 + Mathlib. 4 rounds of hostile adversarial audit passed. Zero sorry/admit.

3

CAB-Certified C

Lean 4 → LambdaIR → MiniC → C. Each transformation step carries a certificate hash verifying semantic preservation.

4

Safe Rust

C → Rust transpilation. Ownership semantics, no unsafe blocks. Correctness inherited from verified C source.

All Projects

Back to the Paper → Proof → Code index.

CAB Certification

Learn about the verified compilation pipeline.

Lean Blueprint

Full HeytingLean proof corpus and dependency graph.

Hybrid Zeckendorf | Paper → Proof → Code | Apoth3osis

All proofs machine-verified using Lean 4 and Mathlib