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