Spaces:
Building
Building
File size: 3,767 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 | // SPDX-License-Identifier: Apache-2.0
// © 2026 Lutar, Stephen P. — SZL Holdings
// ORCID: 0009-0001-0110-4173
//
// Layer 6 — a11oy policy gate for LambdaMinMaxBounds (TH_L2)
//
// Policy rationale:
// Λ_k lies in [0,1] with min=0 iff any axis=0 and max=1 iff all axes=1.
// This gate validates that a submitted Λ score and axis vector satisfy the
// min/max bound theorem, rejecting any score outside [0,1] or inconsistent
// with the all-zero/all-one boundary conditions.
//
// Lean theorem cited: `lambdaMinMaxBounds` (TH_L2)
// Lean file: Lutar/Bound.lean
// Lean commit SHA: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371
// Lean status: proven (2 sorrys in Lutar/Bound.lean — see architect report)
//
// References:
// Zenodo: https://doi.org/10.5281/zenodo.20053148
export interface LambdaMinMaxBoundsGateConfig {
/** Floating-point tolerance for boundary checks. Default: 1e-9. */
tolerance?: number;
}
export interface LambdaMinMaxBoundsGateOpts {
lambdaScore: number;
axisScores: number[];
}
export interface LambdaMinMaxBoundsDecision {
allow: boolean;
rationale: string;
formula: string;
leanTheorem: string;
leanFile: string;
leanCommitSha: string;
inRange: boolean;
boundaryConsistent: boolean;
hasZeroAxis: boolean;
allOnesAxes: boolean;
lambdaScore: number;
}
const LEAN_THEOREM = "lambdaMinMaxBounds";
const LEAN_FILE = "Lutar/Bound.lean";
const LEAN_COMMIT = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371";
const DEFAULT_TOL = 1e-9;
// ── Inline formula ────────────────────────────────────────────────────────────
// TH_L2: Λ_k ∈ [0,1]; min=0 ⟺ ∃i: x_i=0; max=1 ⟺ ∀i: x_i=1
export function lambdaMinMaxBoundsGate(
config: LambdaMinMaxBoundsGateConfig = {}
): (opts: LambdaMinMaxBoundsGateOpts) => LambdaMinMaxBoundsDecision {
const tolerance = config.tolerance ?? DEFAULT_TOL;
return function gate(opts: LambdaMinMaxBoundsGateOpts): LambdaMinMaxBoundsDecision {
const { lambdaScore, axisScores } = opts;
if (!Number.isFinite(lambdaScore)) throw new Error(`LambdaMinMaxBoundsGate: lambdaScore must be finite`);
if (!Array.isArray(axisScores) || axisScores.length === 0) throw new Error(`LambdaMinMaxBoundsGate: axisScores required`);
const inRange = lambdaScore >= -tolerance && lambdaScore <= 1 + tolerance;
const hasZeroAxis = axisScores.some(s => s <= tolerance);
const allOnesAxes = axisScores.every(s => s >= 1 - tolerance);
// Boundary consistency: if has zero axis → lambda ≈ 0; if all ones → lambda ≈ 1
const minBoundOk = !hasZeroAxis || lambdaScore <= tolerance;
const maxBoundOk = !allOnesAxes || lambdaScore >= 1 - tolerance;
const boundaryConsistent = minBoundOk && maxBoundOk;
const allow = inRange && boundaryConsistent;
const rationale = allow
? `LambdaMinMaxBounds (TH_L2): Λ=${lambdaScore.toFixed(6)} ∈ [0,1]; boundary consistent (zero=${hasZeroAxis}, ones=${allOnesAxes}). Passes. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`
: !inRange
? `LambdaMinMaxBounds (TH_L2): Λ=${lambdaScore} outside [0,1]. Denied. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`
: `LambdaMinMaxBounds (TH_L2): boundary inconsistency — zero axis=${hasZeroAxis} but Λ=${lambdaScore.toFixed(6)} not near 0. Denied. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`;
return { allow, rationale, formula: "LambdaMinMaxBounds", leanTheorem: LEAN_THEOREM, leanFile: LEAN_FILE, leanCommitSha: LEAN_COMMIT, inRange, boundaryConsistent, hasZeroAxis, allOnesAxes, lambdaScore };
};
}
|