Spaces:
Running
Running
File size: 3,390 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 | // SPDX-License-Identifier: Apache-2.0
// © 2026 Lutar, Stephen P. — SZL Holdings
// ORCID: 0009-0001-0110-4173
//
// Layer 6 — a11oy policy gate for RhoClosureProduction (TH_L4)
//
// Policy rationale:
// 100% ρ-closure on 8,000/8,000 paired calls under v11 platform. This gate
// validates that a production ρ-closure measurement meets the ≥ 100% target
// (i.e., all paired calls close successfully). Any failure in a paired call
// is a ρ-closure regression requiring immediate investigation.
//
// Lean theorem cited: `rhoClosureProduction` (TH_L4)
// Lean file: Lutar/RhoClosureProduction.lean
// Lean commit SHA: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371
// Lean status: measured (100% empirical on ouroboros v6.3.0)
//
// References:
// Zenodo: https://doi.org/10.5281/zenodo.20119582
export interface RhoClosureProductionGateConfig {
/** Required ρ-closure rate (0..1). Default: 1.0 (100%). */
requiredRate?: number;
}
export interface RhoClosureProductionGateOpts {
closedCalls: number;
totalCalls: number;
}
export interface RhoClosureProductionDecision {
allow: boolean;
rationale: string;
formula: string;
leanTheorem: string;
leanFile: string;
leanCommitSha: string;
closureRate: number;
requiredRate: number;
openCalls: number;
lambdaScore: number;
}
const LEAN_THEOREM = "rhoClosureProduction";
const LEAN_FILE = "Lutar/RhoClosureProduction.lean";
const LEAN_COMMIT = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371";
const DEFAULT_RATE = 1.0;
export function rhoClosureProductionGate(
config: RhoClosureProductionGateConfig = {}
): (opts: RhoClosureProductionGateOpts) => RhoClosureProductionDecision {
const requiredRate = config.requiredRate ?? DEFAULT_RATE;
if (!Number.isFinite(requiredRate) || requiredRate < 0 || requiredRate > 1) {
throw new Error(`RhoClosureProductionGate: requiredRate must be in [0,1]`);
}
return function gate(opts: RhoClosureProductionGateOpts): RhoClosureProductionDecision {
const { closedCalls, totalCalls } = opts;
if (!Number.isInteger(closedCalls) || closedCalls < 0) throw new Error(`RhoClosureProductionGate: closedCalls must be non-negative integer`);
if (!Number.isInteger(totalCalls) || totalCalls < 1) throw new Error(`RhoClosureProductionGate: totalCalls must be ≥ 1`);
if (closedCalls > totalCalls) throw new Error(`RhoClosureProductionGate: closedCalls cannot exceed totalCalls`);
const closureRate = closedCalls / totalCalls;
const openCalls = totalCalls - closedCalls;
const allow = closureRate >= requiredRate;
const lambdaScore = closureRate;
const rationale = allow
? `RhoClosureProduction (TH_L4): ρ-closure=${(closureRate*100).toFixed(2)}% (${closedCalls}/${totalCalls}) ≥ required ${(requiredRate*100).toFixed(0)}%. Production target met. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`
: `RhoClosureProduction (TH_L4): ρ-closure=${(closureRate*100).toFixed(2)}% (${closedCalls}/${totalCalls}); ${openCalls} calls open — below required ${(requiredRate*100).toFixed(0)}%. Denied. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`;
return { allow, rationale, formula: "RhoClosureProduction", leanTheorem: LEAN_THEOREM, leanFile: LEAN_FILE, leanCommitSha: LEAN_COMMIT, closureRate, requiredRate, openCalls, lambdaScore };
};
}
|