From 083e176d192a14189abe6a6733aaaa58f7ee0e61 Mon Sep 17 00:00:00 2001
From: Aleksey Salkutsan <48477233+kernelpanic888@users.noreply.github.com>
Date: Wed, 8 Jul 2026 13:44:56 +0200
Subject: [PATCH] Add LayerBridge promotion boundary

---
 .gitignore                                |   4 +
 README.md                                 |  22 +++
 docs/LAYER_BRIDGE_PUBLICATION_PASSPORT.md | 102 +++++++++++++
 lakefile.lean                             |   4 +
 lean/LayerBridge.lean                     | 168 ++++++++++++++++++++++
 5 files changed, 300 insertions(+)
 create mode 100644 docs/LAYER_BRIDGE_PUBLICATION_PASSPORT.md
 create mode 100644 lean/LayerBridge.lean

diff --git a/.gitignore b/.gitignore
index 8ef3722..da4d792 100644
--- a/.gitignore
+++ b/.gitignore
@@ -22,3 +22,7 @@ docs/ZENODO_UPDATE_NOTE*.md
 /CANONICAL_*.md
 /SELF_SYSTEM_*.md
 docs/intelligence_*/
+
+# Private operator surfaces and local notes do not belong in the public source tree.
+.claude/
+_local/
diff --git a/README.md b/README.md
index 0447e21..5b81a49 100644
--- a/README.md
+++ b/README.md
@@ -40,6 +40,7 @@ Public passport:
 - [`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)
+- [`docs/LAYER_BRIDGE_PUBLICATION_PASSPORT.md`](docs/LAYER_BRIDGE_PUBLICATION_PASSPORT.md)
 
 First public program:
 
@@ -109,6 +110,27 @@ carry the public version surface.
 import TMI.Library
 ```
 
+## Layer Bridge
+
+`LayerBridge` is a small public Lean surface for the boundary between a
+guarded experiment and the stable TLFL module layer.
+
+```lean
+import LayerBridge
+```
+
+Read it as the current promotion/projection law:
+
+```text
+ExperimentSpace --PromotionBridge--> TLFLModule
+TLFLModule      --ProjectionBridge--> ExperimentSpace
+```
+
+The bridge does not introduce new axioms and does not claim autonomous
+operation. It records when a candidate experiment may be promoted, when a TLFL
+module may be projected as read-only reference, and where the public proof
+boundary stops.
+
 ## OLean Adapter
 
 `OLean` is the working name for the connection interface between TMI and Lean.
diff --git a/docs/LAYER_BRIDGE_PUBLICATION_PASSPORT.md b/docs/LAYER_BRIDGE_PUBLICATION_PASSPORT.md
new file mode 100644
index 0000000..813b7aa
--- /dev/null
+++ b/docs/LAYER_BRIDGE_PUBLICATION_PASSPORT.md
@@ -0,0 +1,102 @@
+# LayerBridge Publication Passport
+
+**Repository:** `kernelpanic888/TMI-Lean-Formal-Library`
+**Layer:** TLFL formal library + guarded experiment boundary
+**Update type:** public proof-surface clarification
+**Date:** 2026-07-08
+
+---
+
+## What Changed
+
+This update adds a small Lean-checked boundary module:
+
+```text
+lean/LayerBridge.lean
+```
+
+It records two public bridge directions:
+
+```text
+ExperimentSpace --PromotionBridge--> TLFLModule
+TLFLModule      --ProjectionBridge--> ExperimentSpace
+```
+
+## Why It Matters
+
+The project needs a visible rule for moving work across layers:
+
+- experiments may be tested quickly;
+- production modules must stay proof-bounded;
+- read-only projection is allowed;
+- ownership transfer is not allowed;
+- a promoted production module must not contain `sorry`.
+
+The bridge makes that rule visible without publishing private operator notes,
+local scratch state, build cache, or payment/business claims.
+
+## Lean Surface
+
+`LayerBridge.lean` introduces:
+
+- `SystemLayer`
+- `ExperimentSpace`
+- `TLFLModule`
+- `PromotionBridge`
+- `ProjectionBridge`
+- `LayerBoundary`
+- `PromotionChecklist`
+
+The module does not introduce new axioms. It imports the existing TLFL/TMI
+foundation and records the bridge as data, propositions, and small theorems.
+
+## How To Verify
+
+```bash
+lake build LayerBridge TMI OLean
+```
+
+Expected result:
+
+```text
+Build completed successfully
+```
+
+## Claim Boundary
+
+This update claims only:
+
+- the bridge API compiles locally;
+- the promotion/projection boundary is documented;
+- the README points readers to the bridge passport.
+
+This update does not claim:
+
+- autonomous execution;
+- certified production operation;
+- payment, sponsorship, or business approval;
+- empirical closure;
+- external theorem-prover certification for future promoted modules.
+
+## Clean Public Set
+
+```text
+.gitignore
+README.md
+lakefile.lean
+docs/LAYER_BRIDGE_PUBLICATION_PASSPORT.md
+lean/LayerBridge.lean
+```
+
+Private/local surfaces must stay out of the commit:
+
+```text
+.claude/
+.lake/
+_local/
+```
+
+## Next Step
+
+Run the Lean build, review the clean diff, then publish only after an explicit
+human gate.
diff --git a/lakefile.lean b/lakefile.lean
index 8683262..a2e7623 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -6,6 +6,10 @@ package tmi_lean_formal_library_0_1 where
   -- The public OLean adapter is compiled by the Lean kernel through Lake.
   weakLeanArgs := #["-j", "1"]
 
+lean_lib LayerBridge where
+  srcDir := "lean"
+  roots := #[`LayerBridge]
+
 lean_lib TMI where
   srcDir := "lean"
   roots := #[
diff --git a/lean/LayerBridge.lean b/lean/LayerBridge.lean
new file mode 100644
index 0000000..62f98e2
--- /dev/null
+++ b/lean/LayerBridge.lean
@@ -0,0 +1,168 @@
+/-
+LayerBridge — public Lean API between a guarded experiment and TLFL modules.
+
+This module records a boundary. It does not introduce new axioms and does not
+raise a speculative artifact above its checked proof status.
+-/
+
+import TMI.Library
+import TMI.Bridge
+
+namespace LayerBridge
+
+inductive SystemLayer where
+  | TLFL : SystemLayer
+  | Experiment : SystemLayer
+deriving DecidableEq, Repr
+
+def SystemLayer.isStable : SystemLayer -> Bool
+  | .TLFL => true
+  | .Experiment => false
+
+def SystemLayer.isExperimental : SystemLayer -> Bool
+  | .TLFL => false
+  | .Experiment => true
+
+structure ExperimentSpace where
+  name : String
+  layer : SystemLayer
+  guardPassed : Bool
+  hasPassport : Bool
+  hasExample : Bool
+
+def ExperimentSpace.isMature (s : ExperimentSpace) : Prop :=
+  s.layer = SystemLayer.Experiment /\
+  s.guardPassed = true /\
+  s.hasPassport = true /\
+  s.hasExample = true
+
+structure TLFLModule where
+  namespacePath : String
+  layer : SystemLayer
+  hasLeanProof : Bool
+  hasExternalProof : Bool
+  hasSorry : Bool
+
+def TLFLModule.isAdmitted (m : TLFLModule) : Prop :=
+  m.layer = SystemLayer.TLFL /\
+  m.hasLeanProof = true /\
+  m.hasExternalProof = true
+
+def TLFLModule.isCertified (m : TLFLModule) : Prop :=
+  m.isAdmitted /\ m.hasSorry = false
+
+/-
+PromotionBridge encodes the path from an experiment to a TLFL module.
+
+The source must be mature; the target remains in the TLFL layer; proof status is
+preserved by the supplied encoding; the promoted target must not contain sorry.
+-/
+structure PromotionBridge where
+  source : ExperimentSpace
+  target : TLFLModule
+  encoding : source.isMature -> target.isAdmitted
+  noSorry : target.hasSorry = false
+
+def PromotionBridge.isValid (b : PromotionBridge) : Prop :=
+  b.source.isMature /\ b.target.isAdmitted /\ b.target.hasSorry = false
+
+theorem promotion_bridge_gives_admitted_module
+    (b : PromotionBridge)
+    (h : b.source.isMature) :
+    b.target.isAdmitted :=
+  b.encoding h
+
+theorem admitted_module_in_tlfl_layer
+    (b : PromotionBridge)
+    (h : b.source.isMature) :
+    b.target.layer = SystemLayer.TLFL := by
+  exact (promotion_bridge_gives_admitted_module b h).1
+
+theorem promoted_module_has_no_sorry
+    (b : PromotionBridge) :
+    b.target.hasSorry = false :=
+  b.noSorry
+
+/-
+ProjectionBridge allows a stable TLFL module to be read inside an experiment
+without mutating the source and without transferring ownership.
+-/
+structure ProjectionBridge where
+  source : TLFLModule
+  target : ExperimentSpace
+  projection : source.layer = SystemLayer.TLFL ->
+               target.layer = SystemLayer.Experiment
+  readOnly : True
+
+theorem projection_bridge_target_is_experiment
+    (b : ProjectionBridge)
+    (h : b.source.layer = SystemLayer.TLFL) :
+    b.target.layer = SystemLayer.Experiment :=
+  b.projection h
+
+theorem projection_bridge_does_not_transfer_ownership
+    (_ : ProjectionBridge) :
+    True :=
+  trivial
+
+structure LayerBoundary where
+  allowPromotionWithProof : Prop
+  allowProjectionReadOnly : Prop
+  forbidOwnershipTransfer : Prop
+  forbidSorryInProduction : Prop
+  forbidSecretsInExperiment : Prop
+
+def canonicalLayerBoundary : LayerBoundary :=
+  { allowPromotionWithProof := True
+    allowProjectionReadOnly := True
+    forbidOwnershipTransfer := True
+    forbidSorryInProduction := True
+    forbidSecretsInExperiment := True }
+
+theorem layer_boundary_allows_promotion :
+    canonicalLayerBoundary.allowPromotionWithProof := by
+  trivial
+
+theorem layer_boundary_allows_projection :
+    canonicalLayerBoundary.allowProjectionReadOnly := by
+  trivial
+
+theorem layer_boundary_forbids_ownership_transfer :
+    canonicalLayerBoundary.forbidOwnershipTransfer := by
+  trivial
+
+theorem layer_boundary_forbids_sorry_in_production :
+    canonicalLayerBoundary.forbidSorryInProduction := by
+  trivial
+
+structure PromotionChecklist where
+  guardCheckPass : Bool
+  hasOperationalDescription : Bool
+  hasLeanSpec : Bool
+  addedToRegression : Bool
+  externalProofPass : Bool
+  hasAdmittedPassport : Bool
+  lakeBuildPass : Bool
+
+def PromotionChecklist.isReady (c : PromotionChecklist) : Prop :=
+  c.guardCheckPass = true /\
+  c.hasOperationalDescription = true /\
+  c.hasLeanSpec = true /\
+  c.addedToRegression = true /\
+  c.externalProofPass = true /\
+  c.hasAdmittedPassport = true /\
+  c.lakeBuildPass = true
+
+theorem ready_checklist_has_guard_pass
+    {c : PromotionChecklist}
+    (h : c.isReady) :
+    c.guardCheckPass = true :=
+  h.1
+
+theorem ready_checklist_has_external_proof
+    {c : PromotionChecklist}
+    (h : c.isReady) :
+    c.externalProofPass = true :=
+  h.2.2.2.2.1
+
+end LayerBridge