Spaces:
Running
Running
File size: 4,697 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 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 | // SPDX-License-Identifier: Apache-2.0
// © 2026 Lutar, Stephen P. — SZL Holdings
// ORCID: 0009-0001-0110-4173
//
// Layer 6 — a11oy policy gate for MadhavaBound
//
// Policy rationale:
// A request is allowed only when the Mādhava arctan remainder bound
// (madhavaRemainderBound) is below a configured precision threshold.
// A high remainder bound means the truncated series is far from arctan(x),
// indicating insufficient convergence — the governance signal is unreliable.
//
// Lean theorem cited: `madhavaRemainderBound_nonneg`
// Lean file: Lutar/PACBayes/MadhavaBound.lean
// Lean commit SHA: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371
//
// Policy: if madhavaBound(opts) ≤ threshold → policy.allow; else → policy.deny
//
// References:
// Lean: szl-holdings/lutar-lean Lutar/PACBayes/MadhavaBound.lean
// Runtime: szl-holdings/ouroboros agentic/formulas/madhavaBound.ts
/** Policy decision record. */
export interface PolicyDecision {
allow: boolean;
rationale: string;
formula: string;
leanTheorem: string;
leanFile: string;
leanCommitSha: string;
remainderBound: number;
threshold: number;
lambdaScore: number;
}
/** Configuration for the MadhavaBound policy gate. */
export interface MadhavaBoundGateConfig {
/**
* Maximum allowed remainder bound.
* Default: 0.01 (1% precision — arctan partial sum within 1% of true value).
*/
threshold?: number;
}
/** Inputs for the gate (mirror of MadhavaBoundOpts). */
export interface MadhavaBoundGateOpts {
/** |x| ≤ 1 — input to the arctan series. */
x: number;
/** N ≥ 1 — number of terms summed. */
N: number;
}
// ── Inline formula (mirrors ouroboros/agentic/formulas/madhavaBound.ts) ──────
// Cited: Lean `madhavaRemainderBound_nonneg` (Lutar/PACBayes/MadhavaBound.lean)
// Theorem: ∀ x N, 0 ≤ |x|^(2N+1)/(2N+1)
function _remainderBound(x: number, N: number): number {
return Math.pow(Math.abs(x), 2 * N + 1) / (2 * N + 1);
}
function _partial(x: number, N: number): number {
let s = 0;
for (let n = 0; n < N; n++) s += (n % 2 === 0 ? 1 : -1) * Math.pow(x, 2*n+1) / (2*n+1);
return s;
}
// ── Gate function ─────────────────────────────────────────────────────────────
const LEAN_THEOREM = "madhavaRemainderBound_nonneg";
const LEAN_FILE = "Lutar/PACBayes/MadhavaBound.lean";
const LEAN_COMMIT = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371";
const DEFAULT_THRESHOLD = 0.01;
/**
* MadhavaBound policy gate.
*
* Allows a governance action only when the Mādhava remainder bound
* for the given (x, N) is at or below the configured threshold.
*
* Lean theorem: `madhavaRemainderBound_nonneg`
* Lean file: Lutar/PACBayes/MadhavaBound.lean (commit 1dca00032dfc9aa8559cc6c2e4b63192fcf52371)
*
* @example
* const gate = madhavaBoundGate({ threshold: 0.001 });
* const decision = gate({ x: 1, N: 100 });
* if (decision.allow) policy.allow("series-converged");
* else policy.deny("series-not-converged", decision.rationale);
*/
export function madhavaBoundGate(
config: MadhavaBoundGateConfig = {}
): (opts: MadhavaBoundGateOpts) => PolicyDecision {
const threshold = config.threshold ?? DEFAULT_THRESHOLD;
if (!Number.isFinite(threshold) || threshold <= 0) {
throw new Error(`MadhavaBoundGate: threshold must be > 0; got ${threshold}`);
}
return function gate(opts: MadhavaBoundGateOpts): PolicyDecision {
const { x, N } = opts;
if (!Number.isFinite(x) || Math.abs(x) > 1 + Number.EPSILON) {
throw new Error(`MadhavaBoundGate: |x| must be ≤ 1; got ${x}`);
}
if (!Number.isInteger(N) || N < 1) {
throw new Error(`MadhavaBoundGate: N must be ≥ 1; got ${N}`);
}
const remainderBound = _remainderBound(x, N);
const lambdaScore = Math.max(0, Math.min(1, 1 - remainderBound));
const allow = remainderBound <= threshold;
const rationale = allow
? `Mādhava bound ${remainderBound.toExponential(4)} ≤ threshold ${threshold}: ` +
`series sufficiently converged. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`
: `Mādhava bound ${remainderBound.toExponential(4)} > threshold ${threshold}: ` +
`series not converged — governance signal unreliable. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`;
return {
allow,
rationale,
formula: "MadhavaBound",
leanTheorem: LEAN_THEOREM,
leanFile: LEAN_FILE,
leanCommitSha: LEAN_COMMIT,
remainderBound,
threshold,
lambdaScore,
};
};
}
|