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
“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune
A janitor who proves a theorem outranks a tenured professor who publishes noise.
Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
Ethics, review & quality assurance
Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.
Contribution Certificates
Immutable contribution records per MENTAT-CA-001. Each certificate is a cryptographically anchored MCR documenting authorship, contribution level, and provenance chain. Artifacts are content-addressed and pinned to IPFS.
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerDeriving Type Theory from Distinction
Contributor
Apoth3osis Labs
R&D Division
Core conceptual insight: a dependent type checker can be derived from the simplest possible computational substrate — Spencer-Brown’s mark/unmark distinction. By building a verified pipeline through progressively richer structures (boolean gates, λ-calculus, SKY combinators, eigenforms, Heyting algebras), we ground Lean 4’s type-checking algorithms in the ontology of distinction itself.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological Engineer25-Phase Pipeline Architecture: LoF → Bool → λ → SKY → DT
Contributor
Apoth3osis Labs
R&D Division
Complete mathematical framework spanning 25 verified phases: (0) Laws of Form distinction calculus, (1) Boolean gate synthesis via AIG/MuxNet, (2) Simply-typed λ-calculus with Church-Rosser, (3) SKY combinator algebra with S·K·x=x and S·x·y·z = (x·z)·(y·z), (4) Eigenforms via Y combinator fixed points, (5) Heyting algebras with nucleus operators, through to a fully operational dependent type kernel.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Ontological EngineerLean 4 Formalization — 25 Phases, 0 Sorry
Contributor
Apoth3osis Labs
R&D Division
Machine-checked Lean 4 formalization of the complete LoF-to-type-theory pipeline. All 25 phases verified by the Lean kernel without sorry or admit. Covers Laws of Form arithmetic, boolean gate synthesis, λ-calculus confluence, SKY combinator laws, eigenform existence, Heyting algebra nucleus properties, and dependent type kernel correctness. Part of the HeytingLean formal verification project.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
Ontological EngineerLoF Kernel Verified — Hostile Audit Clean
Contributor
Apoth3osis Labs
R&D Division
Complete formal verification of the LoF Kernel pipeline through adversarial audit. All 25 phases kernel-checked by Lean 4. Guard-no-sorry passes across all modules. Standard axioms only (no additional axioms beyond Lean kernel defaults).
Builds Upon
MENTAT Contribution Record
BRIDGE
Cross-Level Connection
CONTRIBUTION LEVEL: BRIDGE
Ontological EngineerStandalone Repository + HeytingLean Integration
Contributor
Apoth3osis Labs
R&D Division
Published as standalone GitHub repository (lean-kernel-sky) with all source files, documentation, and license. Serves as the ontological backbone of the HeytingLean project — every other formalization in the Heyting ecosystem rests on the computational substrate this pipeline derives.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026