Releases: kernelpanic888/TMI-Lean-Formal-Library
Release list
Chambers of the First Distinction v0.1.0
A self-contained public research map for a formal candidate architecture of intellectual digital life.
https://chertogi-razuma-research.kernelpanic888.chatgpt.site/
Release surface
- The Chambers of the First Distinction public research map
- TIDL-01: a status reader separating a formal architecture candidate from a ready autonomous intelligence
- DL-01 → DL-04: identity, trace, reflection, coherent growth, certificates, and the living-model test chamber
- Self-contained static HTML readers and an explicit claim-boundary passport
Living model · DL-04
https://chertogi-razuma-research.kernelpanic888.chatgpt.site/readers/digital-life-living-model/
Security boundary · PASS
- No secrets or hosting bindings
- No backend or admin routes
- No active embeds, forms, or network APIs
- External links are isolated in the public GitHub export
Claim boundary
An executable formal architecture candidate is not a claim of consciousness, biological life, autonomous goals, or physical realization.
Русское чтение
Самодостаточный публичный срез «Чертогов первого различия»: исследовательская карта, маршрут IDL/DL, живая модель DL-04 и паспорт границ утверждений.
Проверяемый формальный каркас и работающая модель не являются доказательством сознания или цифровой жизни в физическом мире.
TLFL v0.5.2-alpha - Explicit Selection Field
TLFL v0.5.2-alpha — Selection Field
RU
Возвращён отдельный селектор поля ближайших целей:
память -> поле возможностей -> селектор -> выбранная цель.
Поле не выбирает само себя. choose является дополнительной структурой.
Добавлены формальный frame, set-valued field, selection predicate, теорема о
непустоте и блуждание внутри поля. В PredictionBoundary исправлено
пропозициональное неравенство.
Lean build и аудит аксиом не запускались; статус authored / experimental.
EN
The separate nearby-goal selector has been restored:
memory -> possibility field -> selector -> selected goal.
The field does not select itself. choose is additional structure. The release
adds the formal frame, set-valued field, selection predicate, nonemptiness
result, and wandering inside the field. The prediction boundary now uses
propositional inequality.
No Lean build or axiom audit was run; status is authored / experimental.
TLFL v0.5.1-alpha - Modular Interface Foundations
TLFL v0.5.1-alpha — Interface Foundations
RU
Модульное расширение экспериментальной ветки Interface Foundations:
RawOccurs, явный PlanckTouchBridge, двусторонний контакт, минимальное
касание, двухосевое время, предсказательная граница, двухточечный внешний след,
семисимплициальное d squared = 0 и поле целей с памятью.
Красная граница сохранена: это не доказательство физики, сознания, внешнего
спрашивающего, замысла или наддомена. Lean build и аудит аксиом для этого
alpha-релиза не запускались.
EN
A modular expansion of the experimental Interface Foundations branch:
RawOccurs, an explicit PlanckTouchBridge, two-sided contact, minimum-touch
boundary, relational two-axis time, prediction boundary, two-point external
trace, semisimplicial d squared = 0, and a memory-bearing goal field.
The red boundary remains explicit: this is not proof of physics,
consciousness, an external questioner, design, or a supra-domain. No Lean build
or axiom audit was run for this alpha release.
TLFL v0.5.0-alpha - Interface Foundations
TLFL v0.5.0-alpha
RU
TLFL открывает отдельный экспериментальный слой оснований интерфейса.
Главная геометрия:
L <-> Sigma <-> R
PlanckTouch < допустимый коридор < HorizonTouch
Релиз добавляет формальные записи для двустороннего контакта, критерия третьего
тела, памяти, энергии, двухосевого времени, предсказательного шлюза и различия
между несхлопнутостью и ошибкой измерения.
Это alpha-релиз. Он не заявляет эмпирическую физическую валидацию, обнаружение
внешнего наддомена или доказательство сознания. PlanckTouch не влечёт
HorizonTouch без дополнительной структуры.
Канонический стабильный импорт:
import TMI.LibraryЯвный экспериментальный импорт:
import TMI.InterfaceFoundationsAlphaEN
TLFL opens a separate experimental interface-foundations layer.
Core geometry:
L <-> Sigma <-> R
PlanckTouch < admissible corridor < HorizonTouch
The release adds formal records for two-sided contact, the third-body
criterion, memory, energy, two-axis time, a prediction gate, and the distinction
between non-collapse and measurement error.
This is an alpha release. It does not claim empirical physics validation,
detection of an external super-domain, or a proof of consciousness.
PlanckTouch does not imply HorizonTouch without additional structure.
Canonical stable import:
import TMI.LibraryExplicit experimental import:
import TMI.InterfaceFoundationsAlphaTLFL v0.4.0-layerbridge
TLFL v0.4.0-layerbridge
This release adds LayerBridge, a small Lean-checked public surface for the
boundary between guarded experiments and stable TLFL modules.
The bridge records two directions:
ExperimentSpace --PromotionBridge--> TLFLModule
TLFLModule --ProjectionBridge--> ExperimentSpace
What changed
- Added
lean/LayerBridge.lean - Registered the
LayerBridgeLean library inlakefile.lean - Linked the bridge from
README.md - Added
docs/LAYER_BRIDGE_PUBLICATION_PASSPORT.md - Kept local/private operator surfaces out of the public source tree
Claim boundary
This release claims only that the bridge API is a checked public boundary
surface and that the promotion/projection rule is documented.
It does not claim autonomous operation, empirical closure, payment/business
approval, or certification of future promoted modules.
Verification
lake build LayerBridge TMI OLean
Build completed successfully (61 jobs).
Links
TLFL v0.2.0-claim-passport
TLFL v0.2.0-claim-passport
Release type: source-first GitHub release with proof package assets.
Date: 2026-06-20
Summary
v0.2.0-claim-passport publishes the first TLFL 0.2 proof-status slice:
claim passports and proof-state certification.
The release adds a formal path from a claim object and evidence bundle to a
public proof-status surface:
claim object
+ evidence bundle
+ TLFL classification
+ proof-state self-model
+ non-claim guard trace
-> claim passport
-> proof-state certification
-> claim-passport certificate
-> public certificate surface
-> audit sheet
-> review gate
-> release gate
-> release-candidate surface
This is a formal proof-status release. It does not claim empirical truth,
physical validation, consciousness, or empirical closure.
Main Additions
TMI.ClaimPassportClaimPassportVerdictProofStateCertificationClaimPassportCertificateClaimPassportPublicCertificateSurfaceClaimPassportAuditSheetClaimPassportReviewGateClaimPassportReleaseGate- external Z3 mirror for claim-passport theorem and guard checks
- external Vampire/E theorem bundle for the positive claim-passport chain
Canonical Public Boundary
The release uses the public TLFL proof-layer wording:
TLFL + External Proof Layer {Z3, Vampire, E}
TLFL classifies proof status. Z3, Vampire, and E provide external proof traces
for selected release-boundary claims.
Verification Commands
lake env lean lean/TMI/ClaimPassport.lean
lake env lean lean/TMI/Regression.lean
lake build TMI
lake build OLean
z3 external_proofs/tlfl_claim_passport_z3_0_1.smt2
vampire --mode casc --time_limit 10 external_proofs/tlfl_claim_passport_tptp_0_1.p
eprover --auto --cpu-limit=10 external_proofs/tlfl_claim_passport_tptp_0_1.pExpected proof status:
Lean ClaimPassport: pass
Lean Regression: pass
lake build TMI: pass
lake build OLean: pass
Z3 claim-passport mirror: theorem checks unsat, guard checks sat
Vampire claim-passport bundle: SZS status Theorem
E prover claim-passport bundle: SZS status Theorem
Release Assets
The GitHub release should contain:
- GitHub-generated source archives for tag
v0.2.0-claim-passport; tlfl-v0.2.0-claim-passport-source-proof-package.zip;tlfl-v0.2.0-claim-passport-release-summary.pdf;tlfl-v0.2.0-claim-passport-checksums.sha256.
Claim Boundary
Allowed:
- formal proof-status certification;
- claim passport and public certificate surfaces;
- audit, review, and release gates;
- mirrored external proof checks for selected release-boundary claims.
Not allowed:
- empirical truth;
- physical validation;
- consciousness;
- empirical closure.