Spaces:
Runtime error
Runtime error
File size: 3,654 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 | // SPDX-License-Identifier: Apache-2.0
// © 2026 Lutar, Stephen P. — SZL Holdings
// ORCID: 0009-0001-0110-4173
//
// Layer 6 — a11oy policy gate for RhoClosureComposition (T1)
//
// Policy rationale:
// ρ(r1) ∧ ρ(r2) ⟹ ρ(r1∘r2) iff witness sets are pairwise disjoint
// OR a third independent witness co-signs. This gate validates that a
// composed receipt bundle satisfies the closure condition before admission.
//
// Lean derivation cited: `rhoClosureComposition` (T1)
// Lean file: Lutar/Gate/RhoClosureComposition.lean
// Lean commit SHA: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371
// Lean status: theorem (ENFORCED)
//
// References:
// Zenodo: https://doi.org/10.5281/zenodo.20119582
// INNOVATIONS.md §2 T1: ρ-closure composition derivation
export interface RhoClosureCompositionGateConfig {
/** Allow third-witness override for non-disjoint sets. Default: true. */
allowThirdWitness?: boolean;
}
export interface RhoClosureCompositionGateOpts {
witnessSet1: string[];
witnessSet2: string[];
thirdWitness?: string;
}
export interface RhoClosureCompositionDecision {
allow: boolean;
rationale: string;
formula: string;
leanTheorem: string;
leanFile: string;
leanCommitSha: string;
disjoint: boolean;
hasThirdWitness: boolean;
sharedWitnesses: string[];
lambdaScore: number;
}
const LEAN_THEOREM = "rhoClosureComposition";
const LEAN_FILE = "Lutar/Gate/RhoClosureComposition.lean";
const LEAN_COMMIT = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371";
// ── Inline formula ────────────────────────────────────────────────────────────
// T1: ρ(r1) ∧ ρ(r2) ⟹ ρ(r1∘r2) ⟺ W1 ∩ W2 = ∅ ∨ ∃w3 ∉ W1 ∪ W2
export function rhoClosureCompositionGate(
config: RhoClosureCompositionGateConfig = {}
): (opts: RhoClosureCompositionGateOpts) => RhoClosureCompositionDecision {
const allowThirdWitness = config.allowThirdWitness ?? true;
return function gate(opts: RhoClosureCompositionGateOpts): RhoClosureCompositionDecision {
const { witnessSet1, witnessSet2, thirdWitness } = opts;
if (!Array.isArray(witnessSet1) || !Array.isArray(witnessSet2)) {
throw new Error(`RhoClosureCompositionGate: witnessSet1 and witnessSet2 must be arrays`);
}
const set1 = new Set(witnessSet1);
const union = new Set([...witnessSet1, ...witnessSet2]);
const sharedWitnesses = witnessSet2.filter(w => set1.has(w));
const disjoint = sharedWitnesses.length === 0;
const hasThirdWitness = !!thirdWitness && !union.has(thirdWitness);
const allow = disjoint || (allowThirdWitness && hasThirdWitness);
const lambdaScore = allow ? 1.0 : 0.5;
const rationale = allow
? disjoint
? `RhoClosureComposition (T1): witness sets disjoint — ρ-closure of composition holds. Passes. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`
: `RhoClosureComposition (T1): sets non-disjoint but third-witness "${thirdWitness}" ∉ W1∪W2 — ρ-closure holds. Passes. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`
: `RhoClosureComposition (T1): witness sets overlap [${sharedWitnesses.join(',')}] and no valid third witness — ρ-closure fails. Denied. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`;
return { allow, rationale, formula: "RhoClosureComposition", leanTheorem: LEAN_THEOREM, leanFile: LEAN_FILE, leanCommitSha: LEAN_COMMIT, disjoint, hasThirdWitness, sharedWitnesses, lambdaScore };
};
}
|