Spaces:
Running
Running
File size: 4,401 Bytes
518343a 1e7793b 518343a 1fdd5f0 518343a 1e7793b 518343a 1fdd5f0 518343a | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 | // SPDX-License-Identifier: Apache-2.0
// © 2026 Lutar, Stephen P. — SZL Holdings
// ORCID: 0009-0001-0110-4173
//
// Layer 6 — a11oy policy gate for BekensteinEntropyMeasure (T4)
//
// Policy rationale:
// H(R_n) ≤ 8·sizeBytes bits. A receipt chain of sizeBytes bytes admits a
// Shannon entropy of at most 8·sizeBytes bits (max-entropy of a uniform
// distribution over 2^(8·sizeBytes) symbols; processing cannot increase it
// — Data Processing Inequality). This gate validates that the
// Shannon-estimated chain entropy falls within that elementary byte bound.
//
// HONESTY (SZL Doctrine v11): this is the elementary DPI byte-count bound,
// NOT the physical Bekenstein entropy-area bound S ≤ 2πkRE/(ℏc) — that
// physical bound has no counterpart in the SZL codebase (F1-4 errata; see
// Lutar/DPI/DPIBound.lean, where the byte bound's positivity/monotonicity
// are the proven theorem TH6).
//
// 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)
// Zenodo: https://doi.org/10.5281/zenodo.19944926
export interface BekensteinEntropyMeasureGateConfig {
/** Bits per byte bound multiplier. Default: 8. */
bitsPerByte?: number;
}
export interface BekensteinEntropyMeasureGateOpts {
/** Shannon entropy estimate for the receipt hash distribution (bits). */
shannonEntropyBits: number;
/** Registry size in bytes (A). */
registrySizeBytes: number;
}
export interface BekensteinEntropyMeasureDecision {
allow: boolean;
rationale: string;
formula: string;
leanTheorem: string;
leanFile: string;
leanCommitSha: string;
shannonEntropyBits: number;
boundBits: number;
ratio: number;
lambdaScore: number;
}
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(
config: BekensteinEntropyMeasureGateConfig = {}
): (opts: BekensteinEntropyMeasureGateOpts) => BekensteinEntropyMeasureDecision {
const bitsPerByte = config.bitsPerByte ?? DEFAULT_BPB;
if (!Number.isFinite(bitsPerByte) || bitsPerByte <= 0) {
throw new Error(`BekensteinEntropyMeasureGate: bitsPerByte must be > 0; got ${bitsPerByte}`);
}
return function gate(opts: BekensteinEntropyMeasureGateOpts): BekensteinEntropyMeasureDecision {
const { shannonEntropyBits, registrySizeBytes } = opts;
if (!Number.isFinite(shannonEntropyBits) || shannonEntropyBits < 0) {
throw new Error(`BekensteinEntropyMeasureGate: shannonEntropyBits must be ≥ 0`);
}
if (!Number.isFinite(registrySizeBytes) || registrySizeBytes <= 0) {
throw new Error(`BekensteinEntropyMeasureGate: registrySizeBytes must be > 0`);
}
const boundBits = bitsPerByte * registrySizeBytes;
const allow = shannonEntropyBits <= boundBits;
const ratio = shannonEntropyBits / boundBits;
const lambdaScore = allow ? 1 - ratio * 0.5 : 0;
const rationale = allow
? `BekensteinEntropyMeasure (T4): H=${shannonEntropyBits.toFixed(2)} bits ≤ bound=${boundBits.toFixed(2)} bits (ratio=${ratio.toFixed(3)}). Passes. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`
: `BekensteinEntropyMeasure (T4): H=${shannonEntropyBits.toFixed(2)} bits > bound=${boundBits.toFixed(2)} bits. Denied. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`;
return { allow, rationale, formula: "BekensteinEntropyMeasure", leanTheorem: LEAN_THEOREM, leanFile: LEAN_FILE, leanCommitSha: LEAN_COMMIT, shannonEntropyBits, boundBits, ratio, lambdaScore };
};
}
|