Spaces:
Running
Running
File size: 3,588 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 | // SPDX-License-Identifier: Apache-2.0
// © 2026 Lutar, Stephen P. — SZL Holdings
// ORCID: 0009-0001-0110-4173
//
// Layer 6 — a11oy policy gate for LambdaMonotonicity (T2)
//
// Policy rationale:
// Adding consistent evidence to a receipt must weakly increase all axis
// scores. If a proposed evidence augmentation decreases any axis score, it
// is classified as conflicting evidence and rejected at the gate.
//
// Lean derivation cited: `lambdaMonotonicity` (T2)
// Lean file: Lutar/Gate/LambdaMonotonicity.lean
// Lean commit SHA: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371
// Lean status: theorem (ENFORCED)
//
// References:
// Zenodo: https://doi.org/10.5281/zenodo.20119582
// INNOVATIONS.md §2 T2: lambda monotonicity derivation
export interface LambdaMonotonicityGateConfig {
/** Allowed floating-point tolerance for monotonicity check. Default: 1e-9. */
tolerance?: number;
}
export interface LambdaMonotonicityGateOpts {
/** Original axis scores. */
originalScores: number[];
/** Proposed augmented axis scores (after adding evidence). */
augmentedScores: number[];
}
export interface LambdaMonotonicityDecision {
allow: boolean;
rationale: string;
formula: string;
leanTheorem: string;
leanFile: string;
leanCommitSha: string;
decreasingAxes: number[];
minDelta: number;
lambdaScore: number;
}
const LEAN_THEOREM = "lambdaMonotonicity";
const LEAN_FILE = "Lutar/Gate/LambdaMonotonicity.lean";
const LEAN_COMMIT = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371";
const DEFAULT_TOL = 1e-9;
// ── Inline formula ────────────────────────────────────────────────────────────
// T2: r' = r ⊕ e_consistent ⟹ Λ(r') ≥ Λ(r) (Lean A1: IsMonotone)
export function lambdaMonotonicityGate(
config: LambdaMonotonicityGateConfig = {}
): (opts: LambdaMonotonicityGateOpts) => LambdaMonotonicityDecision {
const tolerance = config.tolerance ?? DEFAULT_TOL;
return function gate(opts: LambdaMonotonicityGateOpts): LambdaMonotonicityDecision {
const { originalScores, augmentedScores } = opts;
if (!Array.isArray(originalScores) || !Array.isArray(augmentedScores)) {
throw new Error(`LambdaMonotonicityGate: both score arrays required`);
}
if (originalScores.length !== augmentedScores.length) {
throw new Error(`LambdaMonotonicityGate: score arrays must have equal length`);
}
const decreasingAxes: number[] = [];
let minDelta = Infinity;
for (let i = 0; i < originalScores.length; i++) {
const delta = augmentedScores[i] - originalScores[i];
if (delta < minDelta) minDelta = delta;
if (delta < -tolerance) decreasingAxes.push(i);
}
const allow = decreasingAxes.length === 0;
const lambdaScore = allow ? 1.0 : Math.max(0, 1 + minDelta);
const rationale = allow
? `LambdaMonotonicity (T2): all ${originalScores.length} axes weakly increased (minDelta=${minDelta.toExponential(4)}). Consistent evidence. Passes. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`
: `LambdaMonotonicity (T2): axes [${decreasingAxes.join(',')}] decreased — conflicting evidence. Denied. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`;
return { allow, rationale, formula: "LambdaMonotonicity", leanTheorem: LEAN_THEOREM, leanFile: LEAN_FILE, leanCommitSha: LEAN_COMMIT, decreasingAxes, minDelta, lambdaScore };
};
}
|