<sub>Our tech stack is ontological:
Hardware — Physics
Software — Mathematics

Our engineering workflow is simple: discover, build, grow, learn & teach</sub>

---

_{Acknowledgment
We humbly thank the collective intelligence of humanity for providing the technology and culture we cherish. We do our best to properly reference the authors of the works utilized herein, though we may occasionally fall short. Our formalization acts as a reciprocal validation—confirming the structural integrity of their original insights while securing the foundation upon which we build. In truth, all creative work is derivative; we stand on the shoulders of those who came before, and our contributions are simply the next link in an unbroken chain of human ingenuity.}

---

From Distinction to Dependent Types: A Machine-Verified Compilation of Lean's Kernel to Three Combinators

Paper companion repository for the Goodman-Veselov SKY kernel manuscript. This repository packages the LoF-to-SKY-to-Lean-kernel formalization slice, the curated semantic cross-validation entry points, and the benchmark/result artifacts needed to substantiate the paper without exposing unrelated private-repository HeytingLean infrastructure.

What Is This?

This is a standalone public extraction target for the paper's 25-phase compilation pipeline. It is intentionally narrower than the private repository: only the LoF foundation, SKY combinator pipeline, Lean-kernel compilation phases, reviewer-facing verification scripts, and benchmark/result artifacts are meant to live here.

Current Status

This standalone export was created from an isolated worktree so it would not disturb concurrent SKY-kernel development in the shared source repository.

• Lean pipeline files listed in the paper brief have been copied or wrapped compatibly.
• Reviewer-result source artifacts already measured in the private source measurement infrastructure are preserved under benchmarks/results/source_*.json.
• scripts/run_verification_suite.py records build/demo outcomes into benchmarks/results/verification_runs.json.
• scripts/materialize_reviewer_results.py derives public-facing summaries such as cross_validation_inventory.json, term_characterization.json, and gpu_batch_launch_amortization.json.
• licenses/Apoth3osis-Enterprise-Commercial-License-1.0.md is included as a public-facing CECL access stub so the tri-license stack is complete even though the negotiated commercial terms are not published verbatim here.

Quick Start

./scripts/verify_lean_kernel.sh

• ./scripts/verify_lean_kernel.sh runs the exported build/demo suite, records the outcomes to benchmarks/results/verification_runs.json, refreshes the derived benchmark summaries, and updates artifacts/build_hashes.json.

Repository Structure

heytinglean-sky-kernel/
├── HeytingLean/               Lean formalization slice for the paper
├── benchmarks/                test cases, retained source artifacts, and derived result files
├── scripts/                   verification + benchmark materialization entry points
├── artifacts/                 visual and build-attestation outputs
├── assets/                    Apoth3osis branding assets
├── REVIEWER_NOTES.md          claim-boundary note for the manuscript
├── LICENSE.md                 Apoth3osis License Stack v1
├── CITATION.cff               citation metadata
└── VERIFICATION.md            independent verification instructions

Claim Boundaries

• The theoremized result in this repo is a type-correct compilation path into the bounded SKY machine.
• Universal semantic equivalence with native Lean 4 is not presently proved here by a simulation theorem.
• Semantic agreement is instead supported by curated cross-validation and export-triage evidence.
• GPU performance evidence is reported only for the exact benchmark that was measured; it is not presented as a Lean-vs-SKY type-checker comparison.

See REVIEWER_NOTES.md for paper-safe wording that matches the exported evidence.

Cross-Validation Inventory

The public companion now publishes the case inventory directly instead of compressing semantic evidence to a single aggregate number.

• benchmarks/results/cross_validation_inventory.json records the Phase 15, Phase 20, and Phase 25 case breakdowns plus the smoke/fast benchmark workloads.
• benchmarks/results/verification_runs.json records explicit pass/fail outcomes for the curated Phase 15, Phase 20, and Phase 25 cases on the current host.
• benchmarks/results/term_characterization.json records the 15-subcase FullKernel export triage, including which cases are tractable under the retained export budget.
• The curated Phase 20 and Phase 25 cases are generated by the Lean demo executables on demand; they are documented in cross_validation_inventory.json rather than stored as 47 separate checked-in machine-state fixtures.

On the recorded host run dated 2026-03-23 UTC, the exported suite finished with 39 named commands: the package build and all 6 Phase 15 cases passed, while the longer Phase 20 and Phase 25 cases are recorded individually as either passes or 300-second timeouts instead of being hidden behind a bundled aggregate timeout.

GPU Acceleration

The GPU result exported here is a batch-launch amortization measurement over already-exported bounded-machine states, rerun with the paper's benchmark settings (repeat=32, trials=3).

• benchmarks/results/gpu_batch_launch_amortization.json summarizes the retained source measurement.
• benchmarks/results/source_cuda_batch_launch_amortization_2026-03-22.json is the underlying source artifact.
• benchmarks/results/scalability_curve.json now records the retained multi-batch-size launch-amortization curve.
• benchmarks/results/density_landscape.json and benchmarks/results/ablation_results.json preserve the HZ-density evidence cited in the paper.

This benchmark compares sequential single-case CUDA launches with one batched CUDA launch over the same exact-parity machine states. It is not a comparison against native Lean 4 or lean4lean.

The retained public artifact is the authoritative value for this companion repository. If a manuscript draft still cites a different numeric GPU headline, that draft should be revised or the archived source measurement that produced the older number must be recovered and published alongside it.

Adaptive Sparse Representation

The benchmark surface packages the existing Hybrid Zeckendorf comparison artifacts and density summaries from the private repository. The benchmark wrappers are careful to preserve the current trust boundary: they report measured reducer-exported workloads, not aspirational whole-kernel claims.

The retained density summary now exposes the paper-facing Mersenne headline directly:

• exact Mersenne hits: about 0.21%
• inclusive Hamming-distance-1 proximity: about 1.70%

See benchmarks/results/density_landscape.json for the machine-readable summary and caveats.

CUDA Surface

The public repo does not ship the enterprise CUDA reducer implementation itself. Instead it ships:

• the Lean formalization that defines the bounded-machine target
• retained measurement artifacts generated from the private source measurement surface
• a public cuda/README.md explaining the access boundary for the reducer implementation

If you need the CUDA/Rust reducer source or a hosted verification service, see cuda/README.md.

Pipeline Diagram

The requested static pipeline figure is committed at artifacts/pipeline_8layer.svg. The colors follow the paper-facing staging:

• gray: foundational LoF and combinator strata
• blue: Lean-kernel modeling strata
• green: SKY compilation and validation strata
• orange: empirical artifact and reviewer-evidence strata

Glossary

• kernel: Lean's trusted type-checking core.
• nucleus operator: a meet-preserving closure operator on a Heyting algebra satisfying monotonicity, inflation, idempotence, and preservation of finite meets.
• eigenform: a stable self-referential fixed point produced by repeated re-entry or iterative dynamics.
• WHNF: weak head normal form.
• DefEq: definitional equality.
• bracket abstraction: the elimination of bound variables by compiling lambda terms into closed combinator expressions.
• Heyting algebra: algebraic semantics for intuitionistic logic.
• topos: a category-theoretic generalized universe of sets/sheaves.
• sieve: a downward-closed family of arrows into a fixed object.

Dependency Note

Some modules remain in the export because the paper slice imports them transitively. In particular, HeytingLean/MiniC, HeytingLean/Meta/LeanTT0, HeytingLean/LoF/HoTT/Identity.lean, and HeytingLean/LoF/Bauer/ScottReflexiveDomain.lean are dependency-retained support modules, not additional paper claims.

Citation

See CITATION.cff.

License

Apoth3osis License Stack v1