Llm gpt codex lean tlfl i1/latest public surface

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.
 

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.

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.
+```

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 |

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.
+```

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
+```