Spaces:
Running
Running
File size: 4,056 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 LambdaCategoryComposability (TH4)
//
// *** STAGED — ADVISORY ONLY ***
// Lean status: conjectured (pending Lutar/LaxFunctor.lean)
// This gate issues warnings but does NOT block production by default.
//
// Policy rationale:
// The Λ-Category is a monoidal category; the gate function Λ is a monoidal
// functor. Gate composition is a natural transformation. TH1 (composability)
// follows as a corollary. This gate validates that parallel receipt evaluation
// (monoidal product) preserves the gate semantics.
//
// Lean theorem cited: `lambdaCategoryComposability` (TH4)
// Lean file: Lutar/LaxFunctor.lean (pending — conjectured)
// Lean commit SHA: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371
//
// References:
// Zenodo: https://doi.org/10.5281/zenodo.20119582
// INNOVATIONS.md §4 TH4: Λ-Category composability theorem
export interface LambdaCategoryComposabilityGateConfig {
/** If true, deny on composition failure. Default: false (advisory). */
enforced?: boolean;
}
export interface LambdaCategoryComposabilityGateOpts {
/** Λ score of receipt r1. */
lambdaR1: number;
/** Λ score of receipt r2. */
lambdaR2: number;
/** Λ score of composed receipt r1⊗r2 (monoidal product). */
lambdaComposed: number;
}
export interface LambdaCategoryComposabilityDecision {
allow: boolean;
rationale: string;
formula: string;
leanTheorem: string;
leanFile: string;
leanCommitSha: string;
severity: 'advisory' | 'error';
staged: boolean;
monoidalValid: boolean;
lambdaScore: number;
}
const LEAN_THEOREM = "lambdaCategoryComposability";
const LEAN_FILE = "Lutar/LaxFunctor.lean";
const LEAN_COMMIT = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371";
// ── Inline formula ────────────────────────────────────────────────────────────
// TH4: Λ monoidal: Λ(r1⊗r2) ≥ min(Λ(r1), Λ(r2)) [lax functor inequality]
export function lambdaCategoryComposabilityGate(
config: LambdaCategoryComposabilityGateConfig = {}
): (opts: LambdaCategoryComposabilityGateOpts) => LambdaCategoryComposabilityDecision {
const enforced = config.enforced ?? false;
return function gate(opts: LambdaCategoryComposabilityGateOpts): LambdaCategoryComposabilityDecision {
const { lambdaR1, lambdaR2, lambdaComposed } = opts;
for (const [name, v] of [['lambdaR1', lambdaR1], ['lambdaR2', lambdaR2], ['lambdaComposed', lambdaComposed]] as [string, number][]) {
if (!Number.isFinite(v) || v < 0 || v > 1) throw new Error(`LambdaCategoryComposabilityGate: ${name} must be in [0,1]`);
}
// Lax functor: composed ≥ min(r1, r2) (may need additional witness for strict equality)
const minComponent = Math.min(lambdaR1, lambdaR2);
const monoidalValid = lambdaComposed >= minComponent - 1e-9;
const severity = enforced ? 'error' as const : 'advisory' as const;
const allow = monoidalValid || !enforced;
const lambdaScore = lambdaComposed;
const stagedNote = enforced ? '' : ' [STAGED-ADVISORY]';
const rationale = monoidalValid
? `LambdaCategoryComposability (TH4): Λ(r1⊗r2)=${lambdaComposed.toFixed(4)} ≥ min(${lambdaR1.toFixed(4)},${lambdaR2.toFixed(4)})=${minComponent.toFixed(4)}. Monoidal functor property holds.${stagedNote} Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`
: `LambdaCategoryComposability (TH4): Λ(composed)=${lambdaComposed.toFixed(4)} < min=${minComponent.toFixed(4)} — lax functor violation.${stagedNote} Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`;
return { allow, rationale, formula: "LambdaCategoryComposability", leanTheorem: LEAN_THEOREM, leanFile: LEAN_FILE, leanCommitSha: LEAN_COMMIT, severity, staged: !enforced, monoidalValid, lambdaScore };
};
}
|