SKY/SKI — Visuals

Proof/declaration maps (UMAP), import graphs, and multiway/branchial previews. Most artifacts are generated by scripts/verify_sky.sh (GraphViz required for SVG previews).

Quick Links

Topos / Sheaf Layer

SKY reachability induces a preorder site; the dense Grothendieck topology induces sieve-closure; closure is packaged as an inflationary nucleus; fixed points are the closed (already-glued) sieves.

Since Sieve X is a frame, the stable sieves Ω_J inherit a bundled Heyting algebra structure (a frame).

Lean entry points: HeytingLean/LoF/Combinators/Topos/StepsSite.lean, HeytingLean/LoF/Combinators/Topos/SieveNucleus.lean.

2D Proof Map

Pan/zoom, hover for names, click for details.

Open sky_2d.html

3D Proof Map

Drag to rotate, wheel to zoom, hover/click nodes.

If WebGL is unavailable: static preview / animated preview.

Open sky_3d.html

Import Graphs

Import graph: HeytingLean.LoF.Combinators.SKYMultiway

Import graph: HeytingLean.CLI.SkyMultiwayMain

Multiway Graph Previews

SK demo (depth 3)

Combined multiway + branchial view: SVG · DOT

Y demo (depth 2)

Combined multiway + branchial view: SVG · DOT

Load the JSON outputs in the interactive viewer: ../generated_sky_demo_sk.json, ../generated_sky_demo_y.json.

UMAP Interpretation (Limitations)

UMAP is a non-linear projection of high-dimensional feature vectors (here: Lean source text features) into 2D/3D.
Only local neighborhoods are intended to be meaningful; global distances and cluster geometry are not proof-theoretic invariants.
Treat these maps as navigational aids; the formal guarantee is the Lean kernel check.

Data source: sky_proofs.json.