Spaces:
Running
Running
File size: 3,464 Bytes
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 | // 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) ≤ k·A / (4 ln 2). A registry of sizeBytes bytes admits
// a chain entropy of at most 8·sizeBytes bits. This gate validates that
// the Shannon-estimated chain entropy falls within the bound.
//
// Lean derivation cited: `bekensteinEntropyMeasure` (T4)
// Lean file: Lutar/Gate/BekensteinEntropyMeasure.lean
// Lean commit SHA: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371
// Lean status: theorem (conjectured — formal proof pending)
//
// References:
// Zenodo: https://doi.org/10.5281/zenodo.19944926
// INNOVATIONS.md §2 T4: Bekenstein entropy bound derivation
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 = "bekensteinEntropyMeasure";
const LEAN_FILE = "Lutar/Gate/BekensteinEntropyMeasure.lean";
const LEAN_COMMIT = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371";
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 };
};
}
|