Spaces:
Running
Running
File size: 3,035 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 | // SPDX-License-Identifier: Apache-2.0
// © 2026 Lutar, Stephen P. — SZL Holdings
// ORCID: 0009-0001-0110-4173
//
// Layer 6 — a11oy policy gate for AnatomyReduction (TH3)
//
// Policy rationale:
// Any multi-agent system implementing (R,A,E,Λ,ρ,W) with |R|>8 is bisimilar
// to the canonical 8-region anatomy. Systems with |R|<8 are missing capability.
// 8 is both necessary and sufficient. This gate validates that a submitted
// system topology meets the 8-region requirement before admission.
//
// Lean theorem cited: `anatomyReduction` (TH3)
// Lean file: Lutar/Composition/AnatomyReduction.lean
// Lean commit SHA: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371
// Lean status: theorem (derived)
//
// References:
// Zenodo: https://doi.org/10.5281/zenodo.20162352
export interface AnatomyReductionGateConfig {
/** Required region count. Default: 8. */
canonicalRegionCount?: number;
}
export interface AnatomyReductionGateOpts {
/** Count of unique typed regions in the submitted system. */
regionCount: number;
}
export interface AnatomyReductionDecision {
allow: boolean;
rationale: string;
formula: string;
leanTheorem: string;
leanFile: string;
leanCommitSha: string;
regionCount: number;
canonicalRegionCount: number;
bisimilar: boolean;
missing: boolean;
lambdaScore: number;
}
const LEAN_THEOREM = "anatomyReduction";
const LEAN_FILE = "Lutar/Composition/AnatomyReduction.lean";
const LEAN_COMMIT = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371";
const DEFAULT_REGIONS = 8;
export function anatomyReductionGate(
config: AnatomyReductionGateConfig = {}
): (opts: AnatomyReductionGateOpts) => AnatomyReductionDecision {
const canonicalRegionCount = config.canonicalRegionCount ?? DEFAULT_REGIONS;
return function gate(opts: AnatomyReductionGateOpts): AnatomyReductionDecision {
const { regionCount } = opts;
if (!Number.isInteger(regionCount) || regionCount < 1) {
throw new Error(`AnatomyReductionGate: regionCount must be ≥ 1; got ${regionCount}`);
}
const missing = regionCount < canonicalRegionCount;
const bisimilar = regionCount >= canonicalRegionCount;
const allow = bisimilar;
const lambdaScore = Math.min(1, regionCount / canonicalRegionCount);
const rationale = allow
? `AnatomyReduction (TH3): |R|=${regionCount} ≥ ${canonicalRegionCount} — bisimilar to canonical 8-region anatomy. Passes. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`
: `AnatomyReduction (TH3): |R|=${regionCount} < ${canonicalRegionCount} — missing ${canonicalRegionCount - regionCount} region(s); capability incomplete. Denied. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`;
return { allow, rationale, formula: "AnatomyReduction", leanTheorem: LEAN_THEOREM, leanFile: LEAN_FILE, leanCommitSha: LEAN_COMMIT, regionCount, canonicalRegionCount, bisimilar, missing, lambdaScore };
};
}
|