TLFL Comparator Passport Helper
++ Правая панель копирует полный Lean-файл без Markdown-шума. + Левая панель Comparator получает Challenge, правая панель Comparator получает Solution. +
+loading...+
From 5670790927af7f6d6b20082384602221fe681400 Mon Sep 17 00:00:00 2001 From: osalkutsan-godaddy <99120669+osalkutsan-godaddy@users.noreply.github.com> Date: Wed, 24 Jun 2026 15:35:53 +0200 Subject: [PATCH 01/14] Add TLFL library passport --- README.md | 2 + docs/PASSPORT_AUDIENCE_INTROS.md | 50 +++++++++ docs/TLFL_LIBRARY_PASSPORT.md | 177 +++++++++++++++++++++++++++++++ 3 files changed, 229 insertions(+) create mode 100644 docs/PASSPORT_AUDIENCE_INTROS.md create mode 100644 docs/TLFL_LIBRARY_PASSPORT.md diff --git a/README.md b/README.md index 0447e21..f0e7fe7 100644 --- a/README.md +++ b/README.md @@ -27,6 +27,8 @@ and not empirical closure. Public passport: +- [`docs/TLFL_LIBRARY_PASSPORT.md`](docs/TLFL_LIBRARY_PASSPORT.md) +- [`docs/PASSPORT_AUDIENCE_INTROS.md`](docs/PASSPORT_AUDIENCE_INTROS.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) diff --git a/docs/PASSPORT_AUDIENCE_INTROS.md b/docs/PASSPORT_AUDIENCE_INTROS.md new file mode 100644 index 0000000..40dde76 --- /dev/null +++ b/docs/PASSPORT_AUDIENCE_INTROS.md @@ -0,0 +1,50 @@ +# 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. +``` + +## 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/TLFL_LIBRARY_PASSPORT.md b/docs/TLFL_LIBRARY_PASSPORT.md new file mode 100644 index 0000000..667da34 --- /dev/null +++ b/docs/TLFL_LIBRARY_PASSPORT.md @@ -0,0 +1,177 @@ +# 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/RESERVOIR_READINESS.md + docs/AUTHOR_LEAN_COMMUNITY_ENTRY_RU.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. +``` From ece6f131417d23dc1ceddac802e2094019cf6ddc Mon Sep 17 00:00:00 2001 From: osalkutsan-godaddy <99120669+osalkutsan-godaddy@users.noreply.github.com> Date: Wed, 24 Jun 2026 15:55:26 +0200 Subject: [PATCH 02/14] Add Lean Zulip MWE --- README.md | 1 + docs/LEAN_ZULIP_MWE.md | 79 ++++++++++++++++++++++++++++++++ docs/PASSPORT_AUDIENCE_INTROS.md | 19 +++++++- docs/TLFL_LIBRARY_PASSPORT.md | 4 ++ examples/lean/TLFL_MWE.lean | 27 +++++++++++ 5 files changed, 129 insertions(+), 1 deletion(-) create mode 100644 docs/LEAN_ZULIP_MWE.md create mode 100644 examples/lean/TLFL_MWE.lean diff --git a/README.md b/README.md index f0e7fe7..9c632ae 100644 --- a/README.md +++ b/README.md @@ -29,6 +29,7 @@ Public passport: - [`docs/TLFL_LIBRARY_PASSPORT.md`](docs/TLFL_LIBRARY_PASSPORT.md) - [`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) diff --git a/docs/LEAN_ZULIP_MWE.md b/docs/LEAN_ZULIP_MWE.md new file mode 100644 index 0000000..2bae98f --- /dev/null +++ b/docs/LEAN_ZULIP_MWE.md @@ -0,0 +1,79 @@ +# 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 +``` + +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 +``` + +## 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/PASSPORT_AUDIENCE_INTROS.md b/docs/PASSPORT_AUDIENCE_INTROS.md index 40dde76..8b75908 100644 --- a/docs/PASSPORT_AUDIENCE_INTROS.md +++ b/docs/PASSPORT_AUDIENCE_INTROS.md @@ -18,6 +18,24 @@ 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 @@ -47,4 +65,3 @@ ShowPassport := Do not start with a total-theory claim. Start with package, build, import, boundary, review. ``` - diff --git a/docs/TLFL_LIBRARY_PASSPORT.md b/docs/TLFL_LIBRARY_PASSPORT.md index 667da34..14e4f93 100644 --- a/docs/TLFL_LIBRARY_PASSPORT.md +++ b/docs/TLFL_LIBRARY_PASSPORT.md @@ -143,9 +143,13 @@ Lean package: 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 + Experiment sandbox: https://github.com/kernelpanic888/TMI-OS-Experiment ``` 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 From 9075702c5095ad6a6814f092d52e0c6677e06d58 Mon Sep 17 00:00:00 2001 From: osalkutsan-godaddy <99120669+osalkutsan-godaddy@users.noreply.github.com> Date: Wed, 24 Jun 2026 16:53:21 +0200 Subject: [PATCH 03/14] Add standalone canonical passport MWE --- docs/LEAN_ZULIP_MWE.md | 24 ++++++- docs/TLFL_LIBRARY_PASSPORT.md | 3 + .../TLFL_CANONICAL_PASSPORT_STANDALONE.lean | 70 +++++++++++++++++++ 3 files changed, 96 insertions(+), 1 deletion(-) create mode 100644 examples/lean/TLFL_CANONICAL_PASSPORT_STANDALONE.lean diff --git a/docs/LEAN_ZULIP_MWE.md b/docs/LEAN_ZULIP_MWE.md index 2bae98f..0346c6d 100644 --- a/docs/LEAN_ZULIP_MWE.md +++ b/docs/LEAN_ZULIP_MWE.md @@ -9,6 +9,7 @@ From the repository root: ```bash lake env lean examples/lean/TLFL_MWE.lean +lake env lean examples/lean/TLFL_CANONICAL_PASSPORT_STANDALONE.lean ``` Expected: @@ -49,6 +50,28 @@ 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 +``` + ## Zulip Text ```text @@ -76,4 +99,3 @@ https://github.com/kernelpanic888/TMI-Lean-Formal-Library/blob/llm-gpt-codex-lea This MWE demonstrates package imports and boundary facts. It does not ask reviewers to evaluate the full philosophical surface. ``` - diff --git a/docs/TLFL_LIBRARY_PASSPORT.md b/docs/TLFL_LIBRARY_PASSPORT.md index 14e4f93..9bc1b99 100644 --- a/docs/TLFL_LIBRARY_PASSPORT.md +++ b/docs/TLFL_LIBRARY_PASSPORT.md @@ -150,6 +150,9 @@ Community entry: Minimal working example: examples/lean/TLFL_MWE.lean +Standalone canonical passport: + examples/lean/TLFL_CANONICAL_PASSPORT_STANDALONE.lean + Experiment sandbox: https://github.com/kernelpanic888/TMI-OS-Experiment ``` 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 From a9b2c18957dca4d08ffb25233e88bca63433c529 Mon Sep 17 00:00:00 2001 From: osalkutsan-godaddy <99120669+osalkutsan-godaddy@users.noreply.github.com> Date: Wed, 24 Jun 2026 17:13:57 +0200 Subject: [PATCH 04/14] Add comparator passport split --- docs/LEAN_ZULIP_MWE.md | 37 ++++++++++ docs/TLFL_LIBRARY_PASSPORT.md | 4 ++ .../TLFL_CANONICAL_PASSPORT_CHALLENGE.lean | 70 +++++++++++++++++++ .../TLFL_CANONICAL_PASSPORT_SOLUTION.lean | 70 +++++++++++++++++++ 4 files changed, 181 insertions(+) create mode 100644 examples/lean/TLFL_CANONICAL_PASSPORT_CHALLENGE.lean create mode 100644 examples/lean/TLFL_CANONICAL_PASSPORT_SOLUTION.lean diff --git a/docs/LEAN_ZULIP_MWE.md b/docs/LEAN_ZULIP_MWE.md index 0346c6d..7ec87a7 100644 --- a/docs/LEAN_ZULIP_MWE.md +++ b/docs/LEAN_ZULIP_MWE.md @@ -10,6 +10,8 @@ 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: @@ -72,6 +74,41 @@ 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 +``` + ## Zulip Text ```text diff --git a/docs/TLFL_LIBRARY_PASSPORT.md b/docs/TLFL_LIBRARY_PASSPORT.md index 9bc1b99..8aed802 100644 --- a/docs/TLFL_LIBRARY_PASSPORT.md +++ b/docs/TLFL_LIBRARY_PASSPORT.md @@ -153,6 +153,10 @@ Minimal working example: 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 + Experiment sandbox: https://github.com/kernelpanic888/TMI-OS-Experiment ``` 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 From 73f946474b75026533bc49f76be2987338b9ab37 Mon Sep 17 00:00:00 2001 From: osalkutsan-godaddy <99120669+osalkutsan-godaddy@users.noreply.github.com> Date: Wed, 24 Jun 2026 17:37:54 +0200 Subject: [PATCH 05/14] Add comparator passport copy helper --- docs/LEAN_ZULIP_MWE.md | 6 + tools/comparator_passport_helper.html | 224 ++++++++++++++++++++++++++ 2 files changed, 230 insertions(+) create mode 100644 tools/comparator_passport_helper.html diff --git a/docs/LEAN_ZULIP_MWE.md b/docs/LEAN_ZULIP_MWE.md index 7ec87a7..015e3c5 100644 --- a/docs/LEAN_ZULIP_MWE.md +++ b/docs/LEAN_ZULIP_MWE.md @@ -109,6 +109,12 @@ Do not paste Markdown into either panel. The first line should be: namespace TLFLLibraryPassport ``` +A local copy-helper page is available at: + +```text +tools/comparator_passport_helper.html +``` + ## Zulip Text ```text diff --git a/tools/comparator_passport_helper.html b/tools/comparator_passport_helper.html new file mode 100644 index 0000000..f6a106f --- /dev/null +++ b/tools/comparator_passport_helper.html @@ -0,0 +1,224 @@ + + +
+ + ++ Правая панель копирует полный Lean-файл без Markdown-шума. + Левая панель Comparator получает Challenge, правая панель Comparator получает Solution. +
+loading...+