Proof ↔ Artifact Bridge (Sky Bundle)

This page explains which Lean proofs justify which runtime artifacts.

Lean Claims

• Labeled step enumerator (soundness): HeytingLean.LoF.Comb.stepEdges_sound and HeytingLean.LoF.Comb.stepEdgesList_sound prove every enumerated labeled edge corresponds to a valid Comb.Step.
• Labeled step enumerator (completeness): HeytingLean.LoF.Comb.stepEdges_complete and HeytingLean.LoF.Comb.stepEdgesList_complete prove every Comb.Step appears in the enumerator with some label.
• Kernel footprint: HeytingLean/LoF/Combinators/AxiomsAudit.lean prints #print axioms for the headline results.

Runtime Artifacts

• Proof/declaration maps (UMAP): ./sky_2d.html, ./sky_3d.html (sky_artifacts_data.js links selected proof nodes to artifacts below).
• Multiway/branchial JSON (Lean): ../generated_sky_demo_sk.json, ../generated_sky_demo_y.json
• Wolfram Language cross-check outputs: ../wl_generated_sky_demo_sk.json, ../wl_generated_sky_demo_y.json
• DOT/SVG exports: ./index.html
• Interactive viewer: ../sky_viewer.html
• Compiler artifacts: artifacts/compiler/ (LambdaIR/MiniC/C + compiled C binary)
• CAB artifacts: artifacts/cab/ (kernel commitment + CAB JSON + local checker)