Interactive visualizations of the ISAR kernel geometry, invariant layer structure, and combinator reduction flows. Theorems referenced are machine-checked in Lean 4.
Live
Theoretical and Philosophical Foundations of the ISAR Kernel.
Nonlinear Turing-like pattern generation and excitable cellular automata simulating discrete rewrite steps on the nilpotent operator grid.
Step-by-step reduction of arbitrary ITerm expressions to normal form, with confluence path visualization. Linked to ISAR.lean confluence proof.
Interactive force-directed tree visualizer and leftmost-outermost reducer for open system combinator terms, tracking live carrier fingerprints.
Interactive diagram of the morphism_uniqueness terminal object result: select a dialect and trace its unique factorization morphism into the Invariant Layer.
Side-by-side evaluation of the same term in lambda, SKI, TRS, and bytecode dialects, with the shared invariant normal form shown in the center column.
Discrete-to-continuous wave embedding sweep showing length contraction ($1/\gamma$) and KL divergence shape fidelity as nodes $N \to \infty$.
Planned
Visualizes the bounded-fuel normalization certificate from sufficient_fuel_correct: shows fuel consumption per reduction step alongside the HVM2 interaction net analogue.
Planned demo of compact-open approximation under the named axiom ISAR_UAT. There is no metric on KernelAddress; KernelAddressLimit is not Mathlib completion.