fix(policy): repoint T4 BekensteinEntropyMeasure gate at real proven TH6 (Lutar/DPI/DPIBound.lean); drop phantom citation

docs/theorem-runtime-manifest.json

@@ -347,18 +347,18 @@
     },
     {
       "id": "RUNTIME-T4-BEKENSTEIN-ENTROPY-MEASURE",
-      "theorem": "bekensteinEntropyMeasure",
+      "theorem": "Lutar.DPI.dpi_bound_monotone",
       "formula": "BekensteinEntropyMeasure",
-      "lineage": "Elementary DPI byte-count bound (Cover-Thomas, Elements of Information Theory 2006, sec 2.8.1): chain entropy <= 8*sizeBytes; structurally backed by TH6 DPI. NOT the physical Bekenstein entropy-area proportionality, which has no SZL counterpart (F1-4 errata).",
-      "leanFile": "Lutar/Gate/BekensteinEntropyMeasure.lean",
-      "leanStatus": "conjectured",
+      "lineage": "Elementary DPI byte-count bound (Cover-Thomas, Elements of Information Theory 2006, sec 2.8.1): chain entropy <= 8*sizeBytes; the bound's positivity and monotonicity are the proven theorem TH6 (Lutar/DPI/DPIBound.lean). NOT the physical Bekenstein entropy-area proportionality, which has no SZL counterpart (F1-4 errata).",
+      "leanFile": "Lutar/DPI/DPIBound.lean",
+      "leanStatus": "theorem",
       "runtimeFile": "packages/policy/src/gates/bekensteinEntropyMeasure_gate.ts",
       "exportFile": "packages/policy/src/gates/index.ts",
       "testFile": "packages/policy/src/gates/__tests__/policy_gates_extended.test.ts",
       "validationCommand": "npx tsx packages/policy/src/gates/__tests__/policy_gates_extended.test.ts",
       "claimStatus": "verified-runtime",
       "stagedAdvisory": false,
-      "caveat": "Runtime numeric predicate is independently testable; the cited Lean file Lutar/Gate/BekensteinEntropyMeasure.lean is a phantom/planned obligation (does not exist in lutar-lean). The elementary byte bound's structural properties (positivity, monotonicity) are the proven theorem TH6 (Lutar/DPI/DPIBound.lean)."
+      "caveat": "Runtime numeric predicate is independently testable; the byte bound dpiEntropyBound r = sizeBytes * 8 is kernel-checked (zero sorry) as theorem TH6 in Lutar/DPI/DPIBound.lean (dpi_bound_positive, dpi_bound_monotone). The prior phantom citation Lutar/Gate/BekensteinEntropyMeasure.lean never existed in lutar-lean and has been removed."
     },
     {
       "id": "RUNTIME-T5-REPLAY-DETERMINISM",

gates_manifest.json

@@ -50,13 +50,13 @@
     "name": "bekensteinEntropyMeasure",
     "file": "bekensteinEntropyMeasure_gate.ts",
     "description": "a11oy policy gate for BekensteinEntropyMeasure (T4)",
-    "lean_theorem": "bekensteinEntropyMeasure",
-    "lean_file": "Lutar/Gate/BekensteinEntropyMeasure.lean",
-    "lean_commit_sha": "1dca00032dfc9aa8559cc6c2e4b63192fcf52371",
+    "lean_theorem": "Lutar.DPI.dpi_bound_monotone",
+    "lean_file": "Lutar/DPI/DPIBound.lean",
+    "lean_commit_sha": "5bfeddf7e6fa5ef1bcdd96e01f565d64f6ac0fee",
     "formula": "BekensteinEntropyMeasure",
     "rationale": "H(R_n) \u2264 8\u00b7sizeBytes bits. A registry of sizeBytes bytes admits a chain entropy of at most 8\u00b7sizeBytes bits (elementary DPI byte-count bound: max-entropy of a uniform distribution over 2^(8\u00b7sizeBytes) symbols, non-increasing under processing). This gate validates that the Shannon-estimated chain entropy falls within that bound. This is NOT the physical Bekenstein entropy-area bound S <= 2*pi*k*R*E/(hbar*c), which has no SZL counterpart (F1-4 errata).",
-    "lean_status": "phantom",
-    "lean_status_note": "PHANTOM CITATION: this lean_file is a planned/aspirational proof obligation and does NOT yet exist in szl-holdings/lutar-lean. The TypeScript gate is live and runtime-enforced; the Lean formalization is NOT machine-checked. Disclosed honestly per SZL Doctrine v11 (honesty over checklist) \u2014 NOT counted toward the locked 749 declarations / 14 axioms / 163 sorries at kernel c7c0ba17. No .lean stub created to avoid mutating the LOCKED Lean corpus."
+    "lean_status": "real",
+    "lean_status_note": "REAL: the elementary byte bound dpiEntropyBound r = sizeBytes * 8 is kernel-checked in szl-holdings/lutar-lean at Lutar/DPI/DPIBound.lean (theorem TH6), proven strictly positive (dpi_bound_positive) and monotone (dpi_bound_monotone), zero sorry. The runtime gate enforces that same byte bound. Replaces the prior phantom citation Lutar/Gate/BekensteinEntropyMeasure.lean, which never existed in lutar-lean."
   },
   {
     "name": "bekensteinSoundness",

packages/policy/src/gates/bekensteinEntropyMeasure_gate.ts

@@ -17,13 +17,15 @@
 //   Lutar/DPI/DPIBound.lean, where the byte bound's positivity/monotonicity
 //   are the proven theorem TH6).
 //
-//   Lean derivation cited: `bekensteinEntropyMeasure` (T4)
-//   Lean file: Lutar/Gate/BekensteinEntropyMeasure.lean
-//   PHANTOM CITATION: this lean_file is a planned/aspirational proof
-//   obligation and does NOT yet exist in szl-holdings/lutar-lean. The
-//   TypeScript gate is live and runtime-enforced; the Lean formalization is
-//   NOT machine-checked. Disclosed per SZL Doctrine v11. The elementary byte
-//   bound it computes is structurally backed by TH6 (Lutar/DPI/DPIBound.lean).
+//   Lean derivation cited: TH6 — the elementary byte bound's structural
+//   properties (positivity + monotonicity) are kernel-checked in lutar-lean.
+//   Lean theorem: Lutar.DPI.dpi_bound_monotone (with Lutar.DPI.dpi_bound_positive)
+//   Lean file: Lutar/DPI/DPIBound.lean
+//   Lean status: REAL — machine-checked by the Lean 4 kernel (zero `sorry`) in
+//   szl-holdings/lutar-lean at the cited commit. `dpiEntropyBound r = sizeBytes * 8`
+//   is proven strictly positive and monotone; this gate enforces that same byte
+//   bound at runtime. (Replaces the prior phantom citation
+//   Lutar/Gate/BekensteinEntropyMeasure.lean, which never existed in lutar-lean.)
 //
 // References:
 //   Cover & Thomas, Elements of Information Theory (2006), §2.8 (DPI)
@@ -54,9 +56,9 @@ export interface BekensteinEntropyMeasureDecision {
   lambdaScore:        number;
 }
 
-const LEAN_THEOREM = "bekensteinEntropyMeasure";
-const LEAN_FILE    = "Lutar/Gate/BekensteinEntropyMeasure.lean";
-const LEAN_COMMIT  = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371";
+const LEAN_THEOREM = "Lutar.DPI.dpi_bound_monotone";
+const LEAN_FILE    = "Lutar/DPI/DPIBound.lean";
+const LEAN_COMMIT  = "5bfeddf7e6fa5ef1bcdd96e01f565d64f6ac0fee";
 const DEFAULT_BPB  = 8;
 
 export function bekensteinEntropyMeasureGate(