Spaces:
Running
Running
File size: 3,999 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 81 82 83 84 85 86 87 88 89 90 91 | // SPDX-License-Identifier: Apache-2.0
// © 2026 Lutar, Stephen P. — SZL Holdings
// ORCID: 0009-0001-0110-4173
//
// Layer 6 — a11oy policy gate for BekensteinSoundness (TH_L3)
//
// *** STAGED — ADVISORY ONLY ***
// Lean status: measured/conjectured (formal proof pending lutar-lean PR #12)
//
// Policy rationale:
// Bekenstein indicator fires at 49.5% under uniform seed (measured).
// This gate validates that a submitted fire-rate measurement falls within
// the expected range [45%, 55%] around the 49.5% measured value.
// Advisory only until the Lean proof is formally discharged.
//
// Lean theorem cited: `bekensteinSoundness` (TH_L3)
// Lean file: Lutar/BekensteinSoundness.lean (pending PR #12)
// Lean commit SHA: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371
//
// References:
// https://github.com/szl-holdings/lutar-lean (pending PR #12)
export interface BekensteinSoundnessGateConfig {
/** Expected fire rate center. Default: 0.495 (49.5%). */
expectedFireRate?: number;
/** Acceptable deviation from expected rate. Default: 0.05. */
rateDeviation?: number;
/** If true, block on violation. Default: false (advisory). */
enforced?: boolean;
}
export interface BekensteinSoundnessGateOpts {
/** Measured fire rate (0..1). */
measuredFireRate: number;
/** Sample size used to measure the rate. */
sampleSize: number;
}
export interface BekensteinSoundnessDecision {
allow: boolean;
rationale: string;
formula: string;
leanTheorem: string;
leanFile: string;
leanCommitSha: string;
severity: 'advisory' | 'error';
staged: boolean;
measuredFireRate: number;
expectedFireRate: number;
deviation: number;
withinBand: boolean;
lambdaScore: number;
}
const LEAN_THEOREM = "bekensteinSoundness";
const LEAN_FILE = "Lutar/BekensteinSoundness.lean";
const LEAN_COMMIT = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371";
const DEFAULT_RATE = 0.495;
const DEFAULT_DEVIATION = 0.05;
export function bekensteinSoundnessGate(
config: BekensteinSoundnessGateConfig = {}
): (opts: BekensteinSoundnessGateOpts) => BekensteinSoundnessDecision {
const expectedFireRate = config.expectedFireRate ?? DEFAULT_RATE;
const rateDeviation = config.rateDeviation ?? DEFAULT_DEVIATION;
const enforced = config.enforced ?? false;
return function gate(opts: BekensteinSoundnessGateOpts): BekensteinSoundnessDecision {
const { measuredFireRate, sampleSize } = opts;
if (!Number.isFinite(measuredFireRate) || measuredFireRate < 0 || measuredFireRate > 1) {
throw new Error(`BekensteinSoundnessGate: measuredFireRate must be in [0,1]`);
}
if (!Number.isInteger(sampleSize) || sampleSize < 100) {
throw new Error(`BekensteinSoundnessGate: sampleSize must be ≥ 100`);
}
const deviation = Math.abs(measuredFireRate - expectedFireRate);
const withinBand = deviation <= rateDeviation;
const severity = enforced ? 'error' as const : 'advisory' as const;
const allow = withinBand || !enforced;
const lambdaScore = withinBand ? 1 - deviation / rateDeviation * 0.5 : 0;
const stagedNote = enforced ? '' : ' [STAGED-ADVISORY]';
const rationale = withinBand
? `BekensteinSoundness (TH_L3): rate=${(measuredFireRate*100).toFixed(1)}% within ±${(rateDeviation*100).toFixed(0)}% of ${(expectedFireRate*100).toFixed(1)}% (n=${sampleSize}).${stagedNote} Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`
: `BekensteinSoundness (TH_L3): rate=${(measuredFireRate*100).toFixed(1)}% deviation=${(deviation*100).toFixed(1)}% > band.${stagedNote} Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`;
return { allow, rationale, formula: "BekensteinSoundness", leanTheorem: LEAN_THEOREM, leanFile: LEAN_FILE, leanCommitSha: LEAN_COMMIT, severity, staged: !enforced, measuredFireRate, expectedFireRate, deviation, withinBand, lambdaScore };
};
}
|