LoF Kernel: From Distinction to Type Theory
Formal Verification Certificate
Every phase of the 25-phase pipeline has been formally verified in Lean 4 with zero sorry gaps. Each claim is machine-checked by the Lean kernel.
LoF Kernel • Lean 4 + Mathlib • Apoth3osis Labs
The Central Question
Can a dependent type checker be derived from the simplest possible computational substrate? This project answers yes. Starting from Spencer-Brown’s distinction — the mark/unmark boundary that precedes all computation — we trace a complete, machine-verified path through boolean gates, lambda calculus, SKY combinators, eigenform fixed points, and Heyting algebras, arriving at a fully operational dependent type kernel. Every step is Lean 4 kernel-checked. This is the ontological backbone of the entire Heyting project.
VOID (pre-distinction)
|
v
LOF DISTINCTION (mark/unmark) Phase 0
|
v
BOOLEAN GATES (AIG, MuxNet, BDD) Phase 1
|
v
LAMBDA CALCULUS (STLC, confluence) Phase 2
|
v
SKY COMBINATORS (S, K, Y) Phase 3
|
v
EIGENFORMS (Y·f = f·(Y·f)) Phase 4
|
v
HEYTING ALGEBRAS (nuclei, frames) Phase 5
|
v
DEPENDENT TYPE KERNEL Phase 6+Why This Matters
Most type theories take their foundations as given: here are types, here are terms, here is the typing judgment. But where do types come from? This project answers that question constructively, starting from nothing but distinction.
Spencer-Brown’s Laws of Form (1969) showed that all of boolean logic emerges from a single operation: drawing a distinction. We take this further: from distinction, we derive boolean gates; from boolean gates, lambda calculus; from lambda calculus, SKY combinators; from combinators, eigenform fixed points; from eigenforms, Heyting algebras; from Heyting algebras, dependent types.
The result is not a philosophical argument but a machine-checked derivation. Every step is verified by the Lean 4 kernel. The type checker that verifies the derivation is itself the endpoint of the derivation — a self-referential loop that grounds the Heyting project’s entire ontology.
What Is Proved vs. What Is Philosophical
Proved (all 25 phases)
- •LoF expressions reduce to mark or void
- •AIG/MuxNet correctly implement boolean functions
- •β-reduction is confluent (Church-Rosser)
- •SKY combinator laws hold (S·K·x=x, etc.)
- •Y combinator produces fixed points
- •Nucleus operators are idempotent and monotone
Philosophical (not proved)
- •Distinction as the “true” foundation of mathematics
- •Ontological priority of LoF over set theory or HoTT
- •Whether this pipeline is “the” canonical derivation
- •Self-referential loop as genuine grounding vs. bootstrap
Pipeline Phases
Spencer-Brown’s distinction calculus: the mark/unmark boundary as the pre-computational substrate. Void arithmetic, cross/uncross laws, and the fundamental theorem that every expression reduces to either mark or void.
- ▸Mark/unmark distinction as computational primitive
- ▸Cross/uncross arithmetic laws
- ▸Every LoF expression reduces to mark or void
And-Inverter Graph (AIG) synthesis and MuxNet multiplexer circuits. BDD reduction for canonical boolean forms. The bridge from distinction to digital logic.
- ▸AIG node synthesis from LoF primitives
- ▸MuxNet circuit evaluation
- ▸BDD-based canonical reduction
Simply-typed λ-calculus with β-reduction and Church-Rosser confluence. The computational core: functions as first-class values, substitution, and the guarantee that reduction order doesn’t matter.
- ▸Church-Rosser: β-reduction is confluent
- ▸β-reduction preserves typing
- ▸Substitution lemma for well-typed terms
S, K, Y combinator algebra with bracket abstraction from λ-terms. S·K·x = x (identity), S·x·y·z = (x·z)·(y·z) (distribution). Simulation equivalence: λ ↔ SK bidirectional translation.
- ▸S·K·x = x identity law
- ▸S·x·y·z = (x·z)·(y·z) distribution
- ▸λ ↔ SK simulation via bracket abstraction
Y combinator eigenform fixed points: Y·f = f·(Y·f). Self-referential patterns as stable computational attractors. Heyting algebra nucleus operators, frames, and locales provide the intuitionistic logic substrate for dependent types.
- ▸Y·f = f·(Y·f) eigenform fixed point
- ▸Nucleus idempotence and monotonicity
- ▸Heyting implication via frame adjunction
The culmination: a fully operational dependent type kernel derived from the computational substrate below. Type checking, type inference, and the propositions-as-types correspondence grounded in LoF distinction.
- ▸Dependent function types (Π-types)
- ▸Universe hierarchy
- ▸Type-checking algorithm correctness