ClosingTheLoop + Noneism — Proof/Declaration Map
Standalone 2D/3D visualizations of the HeytingLean.ClosingTheLoop and
HeytingLean.Noneism slices. Open one of the viewers below.
2D Viewer
Pan/zoom, hover for names, click for details. Now includes Noneism declarations.
3D Viewer
Drag to rotate, wheel to zoom, hover/click nodes. Now includes Noneism declarations.
If WebGL is unavailable: static preview.
Computation (WASM)
Runs an extracted C artifact fully in-browser (no backend), linked to a Lean theorem node.
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.
Module Import Graphs (SVG)
ClosingTheLoop
Combined + Noneism
ClosingTheLoop Proof DAGs (SVG)
-
MR.closeSelector.idem— Loop closure idempotence -
Cat.curryNatIso— Currying natural isomorphism -
Cat.idem_of_yoneda_map_idem— Yoneda faithfulness -
Cat.map_close_eq— Concreteness computation -
FunctorialTime.futureKernel.idem— Time kernel closure -
Realizability.realizable_invariant_of_simulation— Invariant transport
Noneism Extension Proof DAGs (SVG)
The eigencomputable framework for grounding the inverse evaluation map β.
See Eigencomputable Framework docs.
-
Eigen.determined_by_dynamics— Unique fixed point determines value -
Bridge.selectorDynamics_stable_iff— Stability characterization -
Bridge.selectorDynamics_unique_stable— Key theorem: unique stable selector per metabolism -
Bridge.beta_right_inverse— Eigencomputable β is a right inverse (eq 2.4) -
Bridge.beta_stable— β outputs are stable under selector dynamics -
Bridge.beta_eq_const— β(f) = (fun _ => f), the constant selector
Statistics
| ClosingTheLoop modules | 27 |
| Noneism modules | 30 |
| Total declarations in UMAP | 238 |
| Proof DAGs generated | 12 |
Data source: closing_the_loop_proofs.json (UMAP over Lean source text features).
Generated: Dec 2025