TLFL 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 LayerBridge Lean library in lakefile.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

• PR: #5
• Branch: https://github.com/kernelpanic888/TMI-Lean-Formal-Library/tree/task24/layerbridge-publication
• Compare: main...task24/layerbridge-publication

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.ClaimPassport
• ClaimPassportVerdict
• ProofStateCertification
• ClaimPassportCertificate
• ClaimPassportPublicCertificateSurface
• ClaimPassportAuditSheet
• ClaimPassportReviewGate
• ClaimPassportReleaseGate
• 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.p

Expected 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.