>_AETHER.VERIFIED.KERNEL

AETHER Verified Kernel
Formally Verified LLM Inference Primitives

Machine-checked Lean 4 proofs for four mathematical cores of AETHER runtime

Teerth Sharma | Independent Researcher | March 2026

IPFS PERMANENT STORAGEcontent-addressed · immutable

LEAN (IPFS)C (IPFS)RUST (IPFS)ALL (IPFS)

CID: bafybeiav6i76eskrs6kchduzfyioxhzzzce2o22q7jgyzeqsedysg6vweq

Abstract

This formalization provides machine-checked Lean 4 proofs for the four mathematical cores of Teerth Sharma's AETHER runtime: Cauchy-Schwarz block pruning for zero-false-negative attention sparsification, Lyapunov-stable PD governors with energy-based convergence certificates, Chebyshev GC guards bounding false collection rates at $1/k^2$ , and Betti approximation bounds bridging heuristic TDA with exact $F_2$ homology. All 23 theorems are sorry-free and kernel-checked, with verified C and safe Rust artifacts. Six rounds of hostile adversarial audit completed, final two consecutive CLEAN.

Modules

4 + 4

Core + sanity tests

Theorems

23

Machine-verified

Lines

818

Proof code

Sorry

0

Zero gaps

Audit Rounds

6

Final 2 CLEAN

>_PROOF.FLOW

Paper ↔ Proof Correspondence

Each AETHER runtime component has a corresponding Lean 4 module with machine-checked proofs covering all mathematical claims.

Component	Title	Lean Module	Status
Phase 1	Cauchy-Schwarz Block Pruning	AetherPruning.lean	PROVED
Phase 2	PD Governor Lyapunov Stability	AetherGovernor.lean	PROVED
Phase 3	Chebyshev GC Guard Safety	AetherChebyshev.lean	PROVED
Phase 4	Betti Approximation Bounds	AetherBetti.lean	PROVED
Pipeline	CAB Artifact Generation	C + Rust transpilations	PROVED

>_KEY.MATHEMATICS

Key Mathematics

Cauchy-Schwarz Pruning Bound

\langle q, k \rangle \leq \|q\| \cdot \|k\| \leq \|q\| \cdot (\|\mu_B\| + r_B)

Zero false negatives: every relevant token is preserved.

PD Governor Error Contraction

e_{t+1} = \frac{e_t \cdot (\varepsilon - \gamma r)}{\varepsilon + \gamma e_t} \;\Longrightarrow\; |e_{t+1}| \leq |e_t|

Lyapunov descent: $V(e_{t+1}) \leq V(e_t)$ .

Chebyshev GC Guard

|\{i : f_i \leq \bar{f} - k\sigma\}| \leq \frac{n}{k^2}

At most $1/k^2$ false collection rate (25% at $k=2$ ).

Betti Error Bound

\hat{\beta}_1 \leq \beta_1 + (n - 3)

Heuristic overcounts bounded by window overlap factor.

>_DEPENDENCY.GRAPH

Module Dependencies

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

Core Module Application Infrastructure Foundationimportstransitive

>_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.

>_VERIFIED.C

Verified C Artifacts

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

C

aether_pruning.c

Block pruning with Cauchy-Schwarz bound | from AetherPruning

DOWNLOAD

C

aether_governor.c

PD governor with Lyapunov stability | from AetherGovernor

DOWNLOAD

C

aether_chebyshev.c

Chebyshev GC guard analysis | from AetherChebyshev

DOWNLOAD

C

aether_betti.c

Betti approximation bounds | from AetherBetti

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

aether_pruning.rs

Block pruning (safe Rust) | from AetherPruning

DOWNLOAD

Rs

aether_governor.rs

PD governor (safe Rust) | from AetherGovernor

DOWNLOAD

Rs

aether_chebyshev.rs

GC guard (safe Rust) | from AetherChebyshev

DOWNLOAD

Rs

aether_betti.rs

Betti bounds (safe Rust) | from AetherBetti

DOWNLOAD

>_PROVENANCE

Provenance Chain

1

AETHER Runtime Primitives

Teerth Sharma's AETHER-Link and AETHER-Lang. Four mathematical cores: Cauchy-Schwarz pruning, PD governor, Chebyshev GC, TDA authentication.

2

Lean 4 Formalization

4 modules + 4 sanity tests, 23 theorems, 818 lines. Kernel-verified by Lean 4 + Mathlib. Imports HeytingLean chain complex and cycle rank infrastructure. Zero sorry/admit.

3

Hostile Audit (6 rounds)

R1: 6H/4M/3L. R2: 0H/3M/1L. R3: CLEAN. R4: 0H/1M/0L. R5: CLEAN. R6: CLEAN. All findings resolved. Final two consecutive CLEAN.

4

CAB-Certified C

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

5

Safe Rust

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

6

IPFS Pinned

All artifacts content-addressed and pinned to IPFS. CID: bafybeiav6i76eskrs6kchduzfyioxhzzzce2o22q7jgyzeqsedysg6vweq. Immutable, globally retrievable via any IPFS gateway.

AETHER Verified Kernel
Formally Verified LLM Inference Primitives

Abstract

Paper ↔ Proof Correspondence

Key Mathematics

Module Dependencies

Proof Modules

Verified C Artifacts

Safe Rust Artifacts

Provenance Chain

← All Projects

Hybrid Zeckendorf

Epistemic Calculi

AETHER Verified KernelFormally Verified LLM Inference Primitives

Abstract

Paper ↔ Proof Correspondence

Key Mathematics

Module Dependencies

Proof Modules

Verified C Artifacts

Safe Rust Artifacts

Provenance Chain

← All Projects

Hybrid Zeckendorf

Epistemic Calculi

AETHER Verified Kernel
Formally Verified LLM Inference Primitives