TMI-Lean-Formal-Library/CITATION.cff at main · kernelpanic888/TMI-Lean-Formal-Library · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
cff-version: 1.2.0
message: "If you use this library, please cite it using this metadata."
title: "TMI-Lean Formal Library (TLFL): Formal Library for Interface-Event Theory in Lean 4"
version: "0.5.0-alpha"
date-released: "2026-07-30"
type: software
url: "https://github.com/kernelpanic888/TMI-Lean-Formal-Library"
license: "Apache-2.0"
authors:
  - family-names: "Salkutsan"
    given-names: "Aleksey"
    orcid: "https://orcid.org/0009-0006-8717-0492"
keywords:
  - "TMI"
  - "Lean 4"
  - "formal library"
  - "interface-event theory"
  - "OLean"
  - "formal verification"
  - "proof-chain self-model"
  - "I1"
  - "engineering surface"
  - "programming on mathematics"
abstract: "TMI-Lean Formal Library (TLFL) is an independent Lean 4 library for core TMI definitions, event structures, bridge surfaces, interface mathematics, OLean kernel-checking boundaries, and guarded proof-status passports. The v0.5.2-alpha release adds a separate experimental interface-foundations module for two-sided interfaces, PlanckTouch and HorizonTouch boundary records, third-body criteria, memory, energy, two-axis time relations, and predictive gates. This alpha status does not claim empirical physics validation or stable API closure."