diff --git a/README.md b/README.md
index 0447e21..9a66881 100644
--- a/README.md
+++ b/README.md
@@ -27,6 +27,13 @@ and not empirical closure.
Public passport:
+- [`docs/TLFL_LIBRARY_PASSPORT.md`](docs/TLFL_LIBRARY_PASSPORT.md)
+- [`examples/lean/TLFL_CANONICAL_PASSPORT_STANDALONE.lean`](examples/lean/TLFL_CANONICAL_PASSPORT_STANDALONE.lean)
+- [`examples/lean/TLFL_CANONICAL_PASSPORT_CHALLENGE.lean`](examples/lean/TLFL_CANONICAL_PASSPORT_CHALLENGE.lean)
+- [`examples/lean/TLFL_CANONICAL_PASSPORT_SOLUTION.lean`](examples/lean/TLFL_CANONICAL_PASSPORT_SOLUTION.lean)
+- [`lean/TMI/ClaimPassport.lean`](lean/TMI/ClaimPassport.lean)
+- [`docs/PASSPORT_AUDIENCE_INTROS.md`](docs/PASSPORT_AUDIENCE_INTROS.md)
+- [`docs/LEAN_ZULIP_MWE.md`](docs/LEAN_ZULIP_MWE.md)
- [`docs/TMI_OS_PUBLIC_PASSPORT.md`](docs/TMI_OS_PUBLIC_PASSPORT.md)
- [`docs/TMI_OS_REPOSITORY_PROFILE.md`](docs/TMI_OS_REPOSITORY_PROFILE.md)
- [`docs/TMI_OS_FIRST_PUBLIC_PROGRAM_RU.md`](docs/TMI_OS_FIRST_PUBLIC_PROGRAM_RU.md)
@@ -37,9 +44,11 @@ Public passport:
- [`docs/TMI_OS_PUBLICATION_REFUSAL_CRITERIA_RU.md`](docs/TMI_OS_PUBLICATION_REFUSAL_CRITERIA_RU.md)
- [`docs/RELEASE_v0.3.0_I1_ENGINEERING_SURFACE.md`](docs/RELEASE_v0.3.0_I1_ENGINEERING_SURFACE.md)
- [`docs/RELEASE_v0.3.1_LEAN_COMMUNITY_ENTRY.md`](docs/RELEASE_v0.3.1_LEAN_COMMUNITY_ENTRY.md)
+- [`docs/RELEASE_v0.4.0_MONUMENTAL_ARTIFACT.md`](docs/RELEASE_v0.4.0_MONUMENTAL_ARTIFACT.md)
- [`docs/LEAN_COMMUNITY_ENTRY.md`](docs/LEAN_COMMUNITY_ENTRY.md)
- [`docs/RESERVOIR_READINESS.md`](docs/RESERVOIR_READINESS.md)
- [`docs/AUTHOR_LEAN_COMMUNITY_ENTRY_RU.md`](docs/AUTHOR_LEAN_COMMUNITY_ENTRY_RU.md)
+- [`publications/monumental_artifact_2026_06_29/README_RU.md`](publications/monumental_artifact_2026_06_29/README_RU.md)
First public program:
@@ -97,9 +106,10 @@ TMI-Lean-Formal-Library
```
Versions live in GitHub releases, tags, and status documents rather than in the
-repository slug. The current source line includes the TLFL 0.3 public
-engineering-surface slice and the `v0.3.1-lean-community-entry` technical entry
-layer for Lean package review. The Lake package id remains
+repository slug. The current source line includes the TLFL 0.4 monumental
+artifact publication-map slice, the TLFL 0.3 public engineering-surface slice,
+and the `v0.3.1-lean-community-entry` technical entry layer for Lean package
+review. The Lake package id remains
`tmi_lean_formal_library_0_1` as a historical package identifier; release tags
carry the public version surface.
diff --git a/docs/COMPARATOR_CHALLENGE_PASSPORT.md b/docs/COMPARATOR_CHALLENGE_PASSPORT.md
new file mode 100644
index 0000000..2edad45
--- /dev/null
+++ b/docs/COMPARATOR_CHALLENGE_PASSPORT.md
@@ -0,0 +1,44 @@
+# Comparator Challenge Passport
+
+This passport records the trusted browser-local challenge slice for the
+standalone TLFL canonical passport used in Comparator-style checking.
+
+## Passport Line
+
+```text
+You have previously chosen to trust this challenge in this browser (SHA256 b67c8f1be23b73884083beb319d530c9b89d9b8fd2a62c6e020226656c21855d)
+```
+
+## Subject
+
+```text
+Subject := TLFL_CANONICAL_PASSPORT_CHALLENGE
+File := examples/lean/TLFL_CANONICAL_PASSPORT_CHALLENGE.lean
+SHA256 := b67c8f1be23b73884083beb319d530c9b89d9b8fd2a62c6e020226656c21855d
+Role := Comparator challenge / theorem target
+```
+
+## Paired Solution
+
+```text
+File := examples/lean/TLFL_CANONICAL_PASSPORT_SOLUTION.lean
+SHA256 := 323a85d7dfe3eebfb72572292e98e188dd26915a5127b68abee624be400fb6c1
+Role := Comparator candidate solution / proof body
+```
+
+## Passport Formula
+
+```text
+ComparatorChallengePassport :=
+ identifies(challenge_file)
+ ∧ preserves(challenge_hash)
+ ∧ separates(challenge, solution)
+ ∧ marks(challenge_tail, "sorry")
+ ∧ marks(solution_tail, "simp [PassportCertified, canonicalPassport]")
+ ∧ does_not_change(Lean_statement)
+```
+
+## Guard
+
+This is a trust-surface passport only. It does not change the Lean statement,
+the solution proof, the TLFL package passport, or any public claim boundary.
diff --git a/docs/LEAN_ZULIP_MWE.md b/docs/LEAN_ZULIP_MWE.md
new file mode 100644
index 0000000..b63b256
--- /dev/null
+++ b/docs/LEAN_ZULIP_MWE.md
@@ -0,0 +1,150 @@
+# Lean Zulip Minimal Working Example
+
+This document follows the Lean community MWE rule: include all imports and make
+the snippet copy-pasteable into an empty Lean file after cloning the package.
+
+## How To Test Locally
+
+From the repository root:
+
+```bash
+lake env lean examples/lean/TLFL_MWE.lean
+lake env lean examples/lean/TLFL_CANONICAL_PASSPORT_STANDALONE.lean
+lake env lean examples/lean/TLFL_CANONICAL_PASSPORT_CHALLENGE.lean
+lake env lean examples/lean/TLFL_CANONICAL_PASSPORT_SOLUTION.lean
+```
+
+Expected:
+
+```text
+the file elaborates successfully and prints #check output
+```
+
+## Copy-Paste MWE
+
+```lean
+import TMI.Library
+import OLean
+
+#check TMI.libraryName
+#check TMI.manifest
+#check TMI.tmi_lean_library_compiled_by_lean_kernel
+#check TMI.tmi_lean_library_is_not_lean_fork
+
+#check OLean.boundary
+#check OLean.olean_imports_tmi_library
+#check OLean.olean_uses_lean_kernel
+#check OLean.olean_does_not_introduce_new_kernel
+
+example : TMI.manifest.compiledByLeanKernel := by
+ exact TMI.tmi_lean_library_compiled_by_lean_kernel
+
+example : ¬ TMI.manifest.isLeanFork := by
+ exact TMI.tmi_lean_library_is_not_lean_fork
+
+example : OLean.boundary.importsTMILibrary := by
+ exact OLean.olean_imports_tmi_library
+
+example : OLean.boundary.usesLeanKernel := by
+ exact OLean.olean_uses_lean_kernel
+
+example : ¬ OLean.boundary.introducesNewKernel := by
+ exact OLean.olean_does_not_introduce_new_kernel
+```
+
+## Standalone Canonical Passport
+
+If the target environment does not contain the TLFL package and only accepts
+plain Lean code, use the standalone passport file:
+
+```text
+examples/lean/TLFL_CANONICAL_PASSPORT_STANDALONE.lean
+```
+
+It has no imports and starts directly with:
+
+```lean
+namespace TLFLLibraryPassport
+```
+
+This avoids two common copy/paste failure modes:
+
+```text
+Markdown headers before Lean code
+late import commands after pasted prose
+```
+
+## Comparator Split
+
+Comparator-style tools need two separate surfaces:
+
+```text
+Challenge panel:
+ examples/lean/TLFL_CANONICAL_PASSPORT_CHALLENGE.lean
+
+Candidate Solution panel:
+ examples/lean/TLFL_CANONICAL_PASSPORT_SOLUTION.lean
+```
+
+The challenge file ends with a theorem admitted by `sorry`, so the challenge
+itself can build:
+
+```lean
+theorem canonical_passport_certified :
+ PassportCertified canonicalPassport := by
+ sorry
+```
+
+The solution file ends with the real proof:
+
+```lean
+theorem canonical_passport_certified :
+ PassportCertified canonicalPassport := by
+ simp [PassportCertified, canonicalPassport]
+```
+
+Do not paste Markdown into either panel. The first line should be:
+
+```lean
+namespace TLFLLibraryPassport
+```
+
+A local copy-helper page is available at:
+
+```text
+tools/comparator_passport_helper.html
+```
+
+The browser-local trusted challenge hash is recorded as a passport in:
+
+```text
+docs/COMPARATOR_CHALLENGE_PASSPORT.md
+```
+
+## Zulip Text
+
+```text
+Hi! I’m preparing a standalone Lean 4 package for technical review.
+
+Here is a minimal working example after cloning the repo:
+
+ lake env lean examples/lean/TLFL_MWE.lean
+
+It imports the package entry point and checks the package manifest and OLean
+boundary facts. I’d appreciate feedback on whether this is a good MWE and on
+the package shape: Lake setup, imports, module boundaries, naming, and
+Reservoir readiness.
+
+Package passport:
+https://github.com/kernelpanic888/TMI-Lean-Formal-Library/blob/llm-gpt-codex-lean-tlfl-i1/latest-public-surface/docs/TLFL_LIBRARY_PASSPORT.md
+
+MWE:
+https://github.com/kernelpanic888/TMI-Lean-Formal-Library/blob/llm-gpt-codex-lean-tlfl-i1/latest-public-surface/examples/lean/TLFL_MWE.lean
+```
+
+## Guard
+
+```text
+This MWE demonstrates package imports and boundary facts.
+It does not ask reviewers to evaluate the full philosophical surface.
+```
diff --git a/docs/MANIFEST.md b/docs/MANIFEST.md
index 52c9ed5..730a829 100644
--- a/docs/MANIFEST.md
+++ b/docs/MANIFEST.md
@@ -65,6 +65,9 @@ Date: 2026-06-24
| `docs/RELEASE_v0.3.1_LEAN_COMMUNITY_ENTRY.md` | GitHub release notes for `v0.3.1-lean-community-entry` |
| `docs/LEAN_COMMUNITY_ENTRY.md` | Lean community-facing package entry point |
| `docs/RESERVOIR_READINESS.md` | Reservoir/package-registry readiness checklist |
+| `docs/PASSPORT_INDEX.md` | Index of public passport surfaces |
+| `docs/TLFL_LIBRARY_PASSPORT.md` | Main TLFL library passport |
+| `docs/COMPARATOR_CHALLENGE_PASSPORT.md` | Trusted Comparator challenge hash passport |
| `docs/GITHUB_PUBLICATION_TEXT.md` | Copy-ready GitHub repository/release publication text |
| `docs/TLFL_EXTENDED_PUBLICATION_EN.md` | Extended English public explanation: what TLFL is and why it exists |
| `docs/TLFL_EXTENDED_PUBLICATION_RU.md` | Extended Russian public explanation: what TLFL is and why it exists |
diff --git a/docs/PASSPORT_AUDIENCE_INTROS.md b/docs/PASSPORT_AUDIENCE_INTROS.md
new file mode 100644
index 0000000..8b75908
--- /dev/null
+++ b/docs/PASSPORT_AUDIENCE_INTROS.md
@@ -0,0 +1,67 @@
+# Passport Audience Intros
+
+Ready-to-use short intros for showing the TLFL Library Passport to different
+audiences.
+
+## Lean Community Intro
+
+```text
+Hi! I’m preparing a Lean 4 package for technical review.
+
+Instead of a long introduction, here is the package passport:
+https://github.com/kernelpanic888/TMI-Lean-Formal-Library/blob/llm-gpt-codex-lean-tlfl-i1/latest-public-surface/docs/TLFL_LIBRARY_PASSPORT.md
+
+It states the package identity, canonical imports, build commands, proof-status
+boundary, claims/non-claims, and the review request.
+
+I’d appreciate feedback on Lake packaging, imports, module boundaries, naming,
+documentation, and Reservoir readiness.
+```
+
+## Lean Community Intro With MWE
+
+```text
+Hi! I’m preparing a standalone Lean 4 package for technical review.
+
+Here is the package passport:
+https://github.com/kernelpanic888/TMI-Lean-Formal-Library/blob/llm-gpt-codex-lean-tlfl-i1/latest-public-surface/docs/TLFL_LIBRARY_PASSPORT.md
+
+Here is a minimal working example after cloning the repo:
+https://github.com/kernelpanic888/TMI-Lean-Formal-Library/blob/llm-gpt-codex-lean-tlfl-i1/latest-public-surface/examples/lean/TLFL_MWE.lean
+
+It can be checked with:
+lake env lean examples/lean/TLFL_MWE.lean
+
+I’d appreciate feedback on Lake packaging, imports, module boundaries, naming,
+documentation, and Reservoir readiness.
+```
+
+## Wider Public Intro
+
+```text
+Я показываю не манифест, а паспорт библиотеки.
+
+Паспорт отвечает на простые вопросы:
+кто пакет, где лежит, как собирается, что импортировать, что проверено,
+что НЕ утверждается, и какой review нужен.
+
+TLFL Library Passport:
+https://github.com/kernelpanic888/TMI-Lean-Formal-Library/blob/llm-gpt-codex-lean-tlfl-i1/latest-public-surface/docs/TLFL_LIBRARY_PASSPORT.md
+```
+
+## Short Formula
+
+```text
+ShowPassport :=
+ one_link
+ + build_commands
+ + non_claims
+ + review_request
+```
+
+## Guard
+
+```text
+Do not start with a total-theory claim.
+Start with package, build, import, boundary, review.
+```
diff --git a/docs/PASSPORT_INDEX.md b/docs/PASSPORT_INDEX.md
new file mode 100644
index 0000000..c251af5
--- /dev/null
+++ b/docs/PASSPORT_INDEX.md
@@ -0,0 +1,18 @@
+# Passport Index
+
+This index keeps the public passport surfaces easy to find.
+
+| Passport | Role |
+|---|---|
+| `docs/TLFL_LIBRARY_PASSPORT.md` | Main TLFL library passport |
+| `docs/TMI_OS_PUBLIC_PASSPORT.md` | Public TMI-OS surface passport |
+| `docs/COMPARATOR_CHALLENGE_PASSPORT.md` | Trusted Comparator challenge hash passport |
+| `docs/CODEX_PROJECTION_INTELLIGENCE_PASSPORT_RU.md` | Guarded Codex role passport reference |
+| `publications/monumental_artifact_2026_06_29/README_RU.md` | Russian monumental artifact navigation passport |
+| `docs/RELEASE_v0.4.0_MONUMENTAL_ARTIFACT.md` | Full publication-map release note |
+
+The Comparator challenge hash is:
+
+```text
+b67c8f1be23b73884083beb319d530c9b89d9b8fd2a62c6e020226656c21855d
+```
diff --git a/docs/RELEASE_v0.4.0_MONUMENTAL_ARTIFACT.md b/docs/RELEASE_v0.4.0_MONUMENTAL_ARTIFACT.md
new file mode 100644
index 0000000..9a21c4c
--- /dev/null
+++ b/docs/RELEASE_v0.4.0_MONUMENTAL_ARTIFACT.md
@@ -0,0 +1,115 @@
+# TLFL v0.4.0-monumental-artifact
+
+Release type: full publication-map release with guarded monumental artifact
+node.
+
+Date: 2026-06-29
+
+## Summary
+
+`v0.4.0-monumental-artifact` publishes the next full public TLFL/TMI-OS slice:
+a repository-level navigation passport that links the formal TLFL library,
+the TMI-OS / I1 engineering surface, publication snapshots, proof-status
+artifacts, and claim-boundary notes.
+
+This release does not raise the empirical status of any claim. It makes the
+public map easier to review.
+
+Public formula:
+
+```text
+MonumentalArtifact :=
+ TLFL formal library
+ + TMI-OS / I1 engineering surface
+ + guarded passports
+ + publication map
+ + proof-status boundary
+```
+
+## Main Additions
+
+- `publications/monumental_artifact_2026_06_29/README_RU.md` as the Russian
+ public navigation passport.
+- `publications/monumental_artifact_2026_06_29/MONUMENTAL_ARTIFACT_README_RU.pdf`
+ as the rendered A4 PDF version.
+- `publications/monumental_artifact_2026_06_29/POST_EN.md` as a short English
+ public post.
+- `publications/monumental_artifact_2026_06_29/SHA256SUMS.txt` as the local
+ integrity passport for the added files.
+- `publications/monumental_artifact_2026_06_29/figures/AUTHOR_VISUAL_CARD_INTERNAL_2026_06_29.png`
+ as an internal author visual card linked from the passport, not used as
+ public evidence.
+- README, `docs/PASSPORT_INDEX.md`, and `docs/THEORY_LINKS.md` now link the
+ new monumental artifact node.
+
+## Public Links
+
+```text
+TLFL repository:
+https://github.com/kernelpanic888/TMI-Lean-Formal-Library
+
+TMI-OS repository:
+https://github.com/osalkutsan-godaddy/TMI-OS
+
+Elusive Graviton Zenodo snapshot:
+https://doi.org/10.5281/zenodo.21011196
+
+Proof/source package snapshot:
+https://doi.org/10.5281/zenodo.20938776
+
+LinkedIn public announcement trace:
+https://www.linkedin.com/posts/oleksiy-salkutsan-276a40184_released-tlfl-v040-a-guarded-monumental-share-7477151831459180544-aU9c/
+```
+
+## Claim Boundary
+
+Allowed:
+
+- repository-level publication navigation;
+- proof-status and artifact-status mapping;
+- linking public publication snapshots;
+- linking public announcement traces;
+- linking internal author visual material as clearly bounded author material;
+- SHA256 integrity checks for files added in this node.
+
+Not allowed:
+
+- empirical detection claims;
+- physics consensus claims;
+- treating diagrams as proofs;
+- treating automated prover traces as empirical validation;
+- treating author visual cards as public evidence;
+- using LLM assistance as scientific authority.
+
+Canonical guard:
+
+```text
+diagram != proof
+candidate != detected particle
+formal prover != empirical validation
+LLM assistance != scientific authority
+author visual card != public evidence
+```
+
+## Verification Status
+
+Local checks completed for this release layer:
+
+```text
+SHA256SUMS: OK
+PDF metadata: A4, 4 pages, no JavaScript, not encrypted
+PDF render preview: visually checked
+git diff --check: OK
+```
+
+The release is a publication-map release. It does not claim a new Lean theorem
+pass beyond the previously documented TLFL proof-status gates.
+
+## Release Assets
+
+The GitHub release/tag should include:
+
+- GitHub-generated source archives for tag `v0.4.0-monumental-artifact`;
+- this release note;
+- the monumental artifact folder:
+ `publications/monumental_artifact_2026_06_29/`.
diff --git a/docs/THEORY_LINKS.md b/docs/THEORY_LINKS.md
index 2643338..248f11d 100644
--- a/docs/THEORY_LINKS.md
+++ b/docs/THEORY_LINKS.md
@@ -16,6 +16,25 @@ Intent -> FormalLogic -> CanonicalRecord -> Passport -> GuardedAction
- TMI-OS public repository: https://github.com/osalkutsan-godaddy/TMI-OS
- TLFL progenitor line: https://github.com/kernelpanic888/TMI-Lean-Formal-Library
+## Publication Map
+
+This section links public publication snapshots without raising their claim
+status. A publication snapshot is a fixed artifact, not empirical closure.
+
+- Monumental artifact Russian passport node: [`publications/monumental_artifact_2026_06_29/README_RU.md`](../publications/monumental_artifact_2026_06_29/README_RU.md)
+- Elusive Graviton preprint Zenodo snapshot: https://doi.org/10.5281/zenodo.21011196
+- Proof/source package snapshot: https://doi.org/10.5281/zenodo.20938776
+- LinkedIn public announcement trace: https://www.linkedin.com/posts/oleksiy-salkutsan-276a40184_released-tlfl-v040-a-guarded-monumental-share-7477151831459180544-aU9c/
+
+Guard:
+
+```text
+publication_snapshot != empirical_detection_claim
+author_visual_card != public evidence
+repository_link != external validation
+public_announcement_trace != peer_review
+```
+
## Ruliad / RuliadChain Motif
```text
diff --git a/docs/TLFL_LIBRARY_PASSPORT.md b/docs/TLFL_LIBRARY_PASSPORT.md
new file mode 100644
index 0000000..d73c4ca
--- /dev/null
+++ b/docs/TLFL_LIBRARY_PASSPORT.md
@@ -0,0 +1,192 @@
+# TLFL Library Passport
+
+This is the short passport for the whole Lean package.
+
+It is written for Lean community review: build surface first, claim boundary
+first, no overclaim.
+
+## Identity
+
+```text
+Name: TMI-Lean Formal Library (TLFL)
+Repository: https://github.com/kernelpanic888/TMI-Lean-Formal-Library
+Release line: v0.3.1-lean-community-entry
+Lake package id: tmi_lean_formal_library_0_1
+License: Apache-2.0
+Lean toolchain: leanprover/lean4:v4.31.0-rc1
+```
+
+The Lake package id is historical and intentionally preserved for compatibility.
+Public versioning is carried by Git tags and release notes.
+
+## Purpose
+
+```text
+TLFL :=
+ Lean4Package
+ + TMI formal vocabulary
+ + OLean boundary adapter
+ + claim-passport/proof-status surfaces
+ + high-level bridge sketches
+ + external proof-status mirrors
+```
+
+Human reading:
+
+```text
+TLFL is a Lean 4 library for representing proof-status structures,
+interface-mathematics vocabulary, claim boundaries, and bridge surfaces.
+It is not a new proof kernel and not a replacement for mathlib.
+```
+
+## Canonical Imports
+
+```lean
+import TMI.Library
+import TMI.SelfThinkingUniverse
+import TMI.ClaimPassport
+import TMI.ProofChainSelfModel
+import OLean
+import OLean.SelfCheck
+import OLean.SelfCheckAsThinker
+```
+
+Minimal reviewer entry:
+
+```lean
+import TMI.Library
+```
+
+## Build Commands
+
+Run from the repository root:
+
+```bash
+lake build TMI
+lake build OLean
+lake env lean lean/TMI/Regression.lean
+lake build TMI.SelfThinkingUniverse
+```
+
+Current checked status for this public surface:
+
+```text
+lake build TMI: PASS
+lake build OLean: PASS
+lean/TMI/Regression.lean: PASS
+lake build TMI.SelfThinkingUniverse: PASS
+```
+
+## Proof-Status Matrix
+
+The synchronized proof-lab surface reports:
+
+```text
+198 theorem targets
+63 model boundaries
+295 TPTP files
+Z3 / Vampire / E gates: PASS in the checked proof-lab surface
+```
+
+This is a proof-status and package-status statement. It is not an empirical
+physics validation statement.
+
+## What The Package Claims
+
+```text
+Claimed:
+ Lean modules compile through the ordinary Lean 4 kernel.
+ OLean states a boundary adapter layer.
+ Claim passports record proof-status boundaries.
+ High-level bridge sketches are represented as Lean structures/definitions/theorems.
+ External prover artifacts act as proof-status mirrors for the checked surface.
+```
+
+## What The Package Does Not Claim
+
+```text
+NotClaimed:
+ not a new Lean kernel
+ not a replacement for mathlib
+ not a theorem of biological life
+ not a proof of consciousness
+ not a legal-identity claim
+ not empirical physics closure
+ not a proof that visual artifacts are mathematical proofs by themselves
+ not a literal identity between time and memory
+ not a literal identity between time and the speed-of-light constant
+```
+
+## Community Review Request
+
+```text
+Please review this as a standalone Lean 4/Lake package:
+ imports,
+ module boundaries,
+ naming,
+ build reproducibility,
+ documentation,
+ Reservoir readiness.
+```
+
+The first requested review is technical packaging feedback, not philosophical
+endorsement.
+
+## Public Surfaces
+
+```text
+Lean package:
+ lean/
+ lakefile.lean
+ lake-manifest.json
+ lean-toolchain
+
+Community entry:
+ docs/LEAN_COMMUNITY_ENTRY.md
+ docs/LEAN_ZULIP_MWE.md
+ docs/RESERVOIR_READINESS.md
+ docs/AUTHOR_LEAN_COMMUNITY_ENTRY_RU.md
+
+Minimal working example:
+ examples/lean/TLFL_MWE.lean
+
+Standalone canonical passport:
+ examples/lean/TLFL_CANONICAL_PASSPORT_STANDALONE.lean
+
+Comparator challenge / solution:
+ examples/lean/TLFL_CANONICAL_PASSPORT_CHALLENGE.lean
+ examples/lean/TLFL_CANONICAL_PASSPORT_SOLUTION.lean
+ docs/COMPARATOR_CHALLENGE_PASSPORT.md
+
+Passport index:
+ docs/PASSPORT_INDEX.md
+
+Experiment sandbox:
+ https://github.com/kernelpanic888/TMI-OS-Experiment
+```
+
+The experiment sandbox is separate from the TLFL kernel package. It exists for
+passport-gated deployment slices, installer checks, and local Lean / Vampire /
+E smoke runs.
+
+## Passport Formula
+
+```text
+TLFLLibraryPassport :=
+ public_repository
+ ∧ apache_2_license
+ ∧ lake_package
+ ∧ canonical_import
+ ∧ reproducible_build_commands
+ ∧ proof_status_boundary
+ ∧ external_prover_status_surface
+ ∧ no_overclaim
+```
+
+## One-Sentence Introduction
+
+```text
+TLFL is a standalone Lean 4 package for proof-status interfaces, claim
+passports, OLean boundary checks, and high-level bridge surfaces; it builds
+with Lake and asks first for Lean packaging and documentation review.
+```
diff --git a/examples/lean/TLFL_CANONICAL_PASSPORT_CHALLENGE.lean b/examples/lean/TLFL_CANONICAL_PASSPORT_CHALLENGE.lean
new file mode 100644
index 0000000..e7cdba5
--- /dev/null
+++ b/examples/lean/TLFL_CANONICAL_PASSPORT_CHALLENGE.lean
@@ -0,0 +1,70 @@
+namespace TLFLLibraryPassport
+
+def subject : String :=
+ "TMI-Lean Formal Library (TLFL)"
+
+def repository : String :=
+ "https://github.com/kernelpanic888/TMI-Lean-Formal-Library"
+
+def canonicalStack : String :=
+ "Lean4 -> TLFL -> OLean -> ProofStatusSurface"
+
+structure CanonicalPassport where
+ subject : String
+ repository : String
+ canonicalStack : String
+ isLean4Package : Prop
+ hasLakeBuildAxis : Prop
+ hasCanonicalImport : Prop
+ hasOLeanBoundary : Prop
+ hasClaimPassportSurface : Prop
+ hasProofStatusSurface : Prop
+ hasExternalProverMirror : Prop
+ hasNoOverclaimGuard : Prop
+ claimsNewLeanKernel : Prop
+ claimsMathlibReplacement : Prop
+ claimsEmpiricalPhysicsClosure : Prop
+ claimsBiologicalLife : Prop
+ claimsLegalIdentity : Prop
+ claimsConsciousnessProof : Prop
+
+def canonicalPassport : CanonicalPassport :=
+ { subject := subject
+ repository := repository
+ canonicalStack := canonicalStack
+ isLean4Package := True
+ hasLakeBuildAxis := True
+ hasCanonicalImport := True
+ hasOLeanBoundary := True
+ hasClaimPassportSurface := True
+ hasProofStatusSurface := True
+ hasExternalProverMirror := True
+ hasNoOverclaimGuard := True
+ claimsNewLeanKernel := False
+ claimsMathlibReplacement := False
+ claimsEmpiricalPhysicsClosure := False
+ claimsBiologicalLife := False
+ claimsLegalIdentity := False
+ claimsConsciousnessProof := False }
+
+def PassportCertified (p : CanonicalPassport) : Prop :=
+ p.isLean4Package ∧
+ p.hasLakeBuildAxis ∧
+ p.hasCanonicalImport ∧
+ p.hasOLeanBoundary ∧
+ p.hasClaimPassportSurface ∧
+ p.hasProofStatusSurface ∧
+ p.hasExternalProverMirror ∧
+ p.hasNoOverclaimGuard ∧
+ ¬ p.claimsNewLeanKernel ∧
+ ¬ p.claimsMathlibReplacement ∧
+ ¬ p.claimsEmpiricalPhysicsClosure ∧
+ ¬ p.claimsBiologicalLife ∧
+ ¬ p.claimsLegalIdentity ∧
+ ¬ p.claimsConsciousnessProof
+
+theorem canonical_passport_certified :
+ PassportCertified canonicalPassport := by
+ sorry
+
+end TLFLLibraryPassport
diff --git a/examples/lean/TLFL_CANONICAL_PASSPORT_SOLUTION.lean b/examples/lean/TLFL_CANONICAL_PASSPORT_SOLUTION.lean
new file mode 100644
index 0000000..37871a2
--- /dev/null
+++ b/examples/lean/TLFL_CANONICAL_PASSPORT_SOLUTION.lean
@@ -0,0 +1,70 @@
+namespace TLFLLibraryPassport
+
+def subject : String :=
+ "TMI-Lean Formal Library (TLFL)"
+
+def repository : String :=
+ "https://github.com/kernelpanic888/TMI-Lean-Formal-Library"
+
+def canonicalStack : String :=
+ "Lean4 -> TLFL -> OLean -> ProofStatusSurface"
+
+structure CanonicalPassport where
+ subject : String
+ repository : String
+ canonicalStack : String
+ isLean4Package : Prop
+ hasLakeBuildAxis : Prop
+ hasCanonicalImport : Prop
+ hasOLeanBoundary : Prop
+ hasClaimPassportSurface : Prop
+ hasProofStatusSurface : Prop
+ hasExternalProverMirror : Prop
+ hasNoOverclaimGuard : Prop
+ claimsNewLeanKernel : Prop
+ claimsMathlibReplacement : Prop
+ claimsEmpiricalPhysicsClosure : Prop
+ claimsBiologicalLife : Prop
+ claimsLegalIdentity : Prop
+ claimsConsciousnessProof : Prop
+
+def canonicalPassport : CanonicalPassport :=
+ { subject := subject
+ repository := repository
+ canonicalStack := canonicalStack
+ isLean4Package := True
+ hasLakeBuildAxis := True
+ hasCanonicalImport := True
+ hasOLeanBoundary := True
+ hasClaimPassportSurface := True
+ hasProofStatusSurface := True
+ hasExternalProverMirror := True
+ hasNoOverclaimGuard := True
+ claimsNewLeanKernel := False
+ claimsMathlibReplacement := False
+ claimsEmpiricalPhysicsClosure := False
+ claimsBiologicalLife := False
+ claimsLegalIdentity := False
+ claimsConsciousnessProof := False }
+
+def PassportCertified (p : CanonicalPassport) : Prop :=
+ p.isLean4Package ∧
+ p.hasLakeBuildAxis ∧
+ p.hasCanonicalImport ∧
+ p.hasOLeanBoundary ∧
+ p.hasClaimPassportSurface ∧
+ p.hasProofStatusSurface ∧
+ p.hasExternalProverMirror ∧
+ p.hasNoOverclaimGuard ∧
+ ¬ p.claimsNewLeanKernel ∧
+ ¬ p.claimsMathlibReplacement ∧
+ ¬ p.claimsEmpiricalPhysicsClosure ∧
+ ¬ p.claimsBiologicalLife ∧
+ ¬ p.claimsLegalIdentity ∧
+ ¬ p.claimsConsciousnessProof
+
+theorem canonical_passport_certified :
+ PassportCertified canonicalPassport := by
+ simp [PassportCertified, canonicalPassport]
+
+end TLFLLibraryPassport
diff --git a/examples/lean/TLFL_CANONICAL_PASSPORT_STANDALONE.lean b/examples/lean/TLFL_CANONICAL_PASSPORT_STANDALONE.lean
new file mode 100644
index 0000000..37871a2
--- /dev/null
+++ b/examples/lean/TLFL_CANONICAL_PASSPORT_STANDALONE.lean
@@ -0,0 +1,70 @@
+namespace TLFLLibraryPassport
+
+def subject : String :=
+ "TMI-Lean Formal Library (TLFL)"
+
+def repository : String :=
+ "https://github.com/kernelpanic888/TMI-Lean-Formal-Library"
+
+def canonicalStack : String :=
+ "Lean4 -> TLFL -> OLean -> ProofStatusSurface"
+
+structure CanonicalPassport where
+ subject : String
+ repository : String
+ canonicalStack : String
+ isLean4Package : Prop
+ hasLakeBuildAxis : Prop
+ hasCanonicalImport : Prop
+ hasOLeanBoundary : Prop
+ hasClaimPassportSurface : Prop
+ hasProofStatusSurface : Prop
+ hasExternalProverMirror : Prop
+ hasNoOverclaimGuard : Prop
+ claimsNewLeanKernel : Prop
+ claimsMathlibReplacement : Prop
+ claimsEmpiricalPhysicsClosure : Prop
+ claimsBiologicalLife : Prop
+ claimsLegalIdentity : Prop
+ claimsConsciousnessProof : Prop
+
+def canonicalPassport : CanonicalPassport :=
+ { subject := subject
+ repository := repository
+ canonicalStack := canonicalStack
+ isLean4Package := True
+ hasLakeBuildAxis := True
+ hasCanonicalImport := True
+ hasOLeanBoundary := True
+ hasClaimPassportSurface := True
+ hasProofStatusSurface := True
+ hasExternalProverMirror := True
+ hasNoOverclaimGuard := True
+ claimsNewLeanKernel := False
+ claimsMathlibReplacement := False
+ claimsEmpiricalPhysicsClosure := False
+ claimsBiologicalLife := False
+ claimsLegalIdentity := False
+ claimsConsciousnessProof := False }
+
+def PassportCertified (p : CanonicalPassport) : Prop :=
+ p.isLean4Package ∧
+ p.hasLakeBuildAxis ∧
+ p.hasCanonicalImport ∧
+ p.hasOLeanBoundary ∧
+ p.hasClaimPassportSurface ∧
+ p.hasProofStatusSurface ∧
+ p.hasExternalProverMirror ∧
+ p.hasNoOverclaimGuard ∧
+ ¬ p.claimsNewLeanKernel ∧
+ ¬ p.claimsMathlibReplacement ∧
+ ¬ p.claimsEmpiricalPhysicsClosure ∧
+ ¬ p.claimsBiologicalLife ∧
+ ¬ p.claimsLegalIdentity ∧
+ ¬ p.claimsConsciousnessProof
+
+theorem canonical_passport_certified :
+ PassportCertified canonicalPassport := by
+ simp [PassportCertified, canonicalPassport]
+
+end TLFLLibraryPassport
diff --git a/examples/lean/TLFL_MWE.lean b/examples/lean/TLFL_MWE.lean
new file mode 100644
index 0000000..bf449b9
--- /dev/null
+++ b/examples/lean/TLFL_MWE.lean
@@ -0,0 +1,27 @@
+import TMI.Library
+import OLean
+
+#check TMI.libraryName
+#check TMI.manifest
+#check TMI.tmi_lean_library_compiled_by_lean_kernel
+#check TMI.tmi_lean_library_is_not_lean_fork
+
+#check OLean.boundary
+#check OLean.olean_imports_tmi_library
+#check OLean.olean_uses_lean_kernel
+#check OLean.olean_does_not_introduce_new_kernel
+
+example : TMI.manifest.compiledByLeanKernel := by
+ exact TMI.tmi_lean_library_compiled_by_lean_kernel
+
+example : ¬ TMI.manifest.isLeanFork := by
+ exact TMI.tmi_lean_library_is_not_lean_fork
+
+example : OLean.boundary.importsTMILibrary := by
+ exact OLean.olean_imports_tmi_library
+
+example : OLean.boundary.usesLeanKernel := by
+ exact OLean.olean_uses_lean_kernel
+
+example : ¬ OLean.boundary.introducesNewKernel := by
+ exact OLean.olean_does_not_introduce_new_kernel
diff --git a/programs/tmi_os_mathematical_board/README_RU.md b/programs/tmi_os_mathematical_board/README_RU.md
index 423bf97..05fd8ec 100644
--- a/programs/tmi_os_mathematical_board/README_RU.md
+++ b/programs/tmi_os_mathematical_board/README_RU.md
@@ -1,9 +1,9 @@
-# фотонная теория времяни или теория интерфейсных интелектов
+# фотонная теория времени или теория интерфейсных интеллектов
Первая публичная программа TMI-OS / И1.
```text
-ProgramName := "фотонная теория времяни или теория интерфейсных интелектов"
+ProgramName := "фотонная теория времени или теория интерфейсных интеллектов"
SurfaceClass := "инженерная поверхность"
LanguageVersion := "последняя"
LanguageMode := "безверсионный язык"
diff --git a/programs/tmi_os_mathematical_board/TMI_OS_MATHEMATICAL_BOARD.html b/programs/tmi_os_mathematical_board/TMI_OS_MATHEMATICAL_BOARD.html
index 4d325a4..4498e39 100644
--- a/programs/tmi_os_mathematical_board/TMI_OS_MATHEMATICAL_BOARD.html
+++ b/programs/tmi_os_mathematical_board/TMI_OS_MATHEMATICAL_BOARD.html
@@ -3,7 +3,7 @@
- фотонная теория времяни или теория интерфейсных интелектов
+ фотонная теория времени или теория интерфейсных интеллектов
+
+
+
+
+
TLFL Comparator Passport Helper
+
+ Правая панель копирует полный Lean-файл без Markdown-шума.
+ Левая панель Comparator получает Challenge, правая панель Comparator получает Solution.
+
+
Rule :=
+ Challenge panel <- full CHALLENGE file with `sorry`
+ Candidate panel <- full SOLUTION file with `simp`
+
+First line must be:
+ namespace TLFLLibraryPassport
+
+Do not paste:
+ Markdown
+ screenshots
+ shortened `...`
+ only theorem tail