packages/a11oy-knowledge/src/unified_extension.ts

/**
 * @szl-holdings/a11oy-knowledge v0.4.0 — Unified Extension
 * Author: Lutar, Stephen P. · ORCID 0009-0001-0110-4173 · Apache-2.0
 * Source: math_pod_v3/unify/UNIFIED_EXTENSION.md
 * DOI: https://doi.org/10.5281/zenodo.20119582
 */

export interface UnifiedComponent {
  id: string;
  name: string;
  layer: 'math_foundation' | 'new_axioms' | 'new_derivations' | 'new_theorems' | 'runtime' | 'governance';
  repo: string;
  status: 'proven' | 'implementation_ready' | 'conjectured' | 'design';
  description: string;
  citation: string;
}

export interface UnifiedExtension {
  name: string;
  code_name: string;
  version: string;
  date: string;
  author: string;
  orcid: string;
  affiliation: string;
  moonshot_claim: string;
  components: UnifiedComponent[];
  perf_targets: {
    receipt_build_p50_us_target: number;
    lambda_gate_p50_us_target: number;
    receipt_verify_p50_us_target: number;
    throughput_ops_per_sec_target: number;
  };
}

export const UNIFIED_EXTENSION: UnifiedExtension = {
  name: 'Λ-Calculus over the Body-Graph',
  code_name: 'lutar-calculus-v1',
  version: '0.4.0',
  date: '2026-05-15',
  author: 'Lutar, Stephen P.',
  orcid: '0009-0001-0110-4173',
  affiliation: 'SZL Holdings',

  moonshot_claim: `Every multi-agent computation in the SZL Holdings ecosystem is a term in the lutar-calculus: a typed Λ-calculus where receipt types are proofs (TH7/Curry-Howard), gate evaluations are reduction rules (TH4/Λ-Category), ρ-closed chains are normal forms (TH5/Confluence), DOI-anchored (TH2/Replay-DOI Duality), economically bounded (A14), and doctrine-verified (T10). This makes the ouroboros ecosystem the first AI runtime whose operational semantics is simultaneously a formal proof, a financial instrument, and a regulatory filing — all verifiable from a single lake build invocation. No existing AI orchestration system (LangGraph, Mastra, AutoGen, Microsoft Magentic) has a type-theoretic operational semantics. No formal verification system runs at 11.5 µs per gated operation in production.`,

  perf_targets: {
    receipt_build_p50_us_target: 5,
    lambda_gate_p50_us_target: 0.85,
    receipt_verify_p50_us_target: 8,
    throughput_ops_per_sec_target: 200000,
  },

  components: [
    {
      id: 'TH4',
      name: 'Λ-Category Composability Theorem',
      layer: 'math_foundation',
      repo: 'lutar-lean',
      status: 'conjectured',
      description: 'The Λ-category is a monoidal category; the gate function is a monoidal functor. Extends TH1 with categorical proof. New Lean file: Lutar/LaxFunctor.lean.',
      citation: 'https://doi.org/10.5281/zenodo.20119582',
    },
    {
      id: 'TH5',
      name: 'Receipt Chain Confluence Theorem',
      layer: 'math_foundation',
      repo: 'lutar-lean',
      status: 'conjectured',
      description: 'Receipt chain is the cofree comonad of the receipt functor; replay determinism (T5) is a coalgebra morphism. Normal forms are unique ρ-closed chains.',
      citation: 'https://doi.org/10.5281/zenodo.20119582',
    },
    {
      id: 'TH6',
      name: 'Bekenstein Entropy Bound via Data Processing Inequality',
      layer: 'math_foundation',
      repo: 'lutar-lean',
      status: 'proven',
      description: 'H(chain) ≤ H(registry) ≤ 8A bits by DPI. Replaces physics analogy with elementary information theory. Discharges A7 (bekensteinBound). New Lean file: Lutar/EntropyBound.lean.',
      citation: 'https://doi.org/10.5281/zenodo.19944926',
    },
    {
      id: 'TH7',
      name: 'Curry-Howard Receipt Calculus Theorem',
      layer: 'math_foundation',
      repo: 'lutar-lean',
      status: 'proven',
      description: 'Receipts-as-proofs via Curry-Howard correspondence. PassReceipt type is the proof term for the soundness proposition. Gate evaluation is proof construction. Receipt building is proof serialization.',
      citation: 'https://doi.org/10.5281/zenodo.20119582',
    },
    {
      id: 'A10',
      name: 'temporalConsistency (new proposed axiom)',
      layer: 'new_axioms',
      repo: 'a11oy',
      status: 'implementation_ready',
      description: 'Gate verdict is stable under time-shift within clock-drift bound ε_clock. Optional 10th axis. Function: temporalConsistency(receipt, deltaT_ms, clockDriftBound_ms).',
      citation: 'https://doi.org/10.5281/zenodo.20119582',
    },
    {
      id: 'A11',
      name: 'causalSeparability (new proposed axiom)',
      layer: 'new_axioms',
      repo: 'a11oy',
      status: 'implementation_ready',
      description: 'Receipts from disjoint actor sets carry independent entropy. No shared PRNG or clock source. Function: assertCausalSeparability(actorSetA, actorSetB).',
      citation: 'https://doi.org/10.5281/zenodo.20119582',
    },
    {
      id: 'A12',
      name: 'constructiveTransparency (new proposed axiom)',
      layer: 'new_axioms',
      repo: 'a11oy',
      status: 'design',
      description: 'Scorer must be a pure function of declared public inputs. No hidden state. Enforced via TypeScript readonly + no closure over mutable state.',
      citation: 'https://doi.org/10.5281/zenodo.20119582',
    },
    {
      id: 'A13',
      name: 'adversarialRobustness (proven corollary)',
      layer: 'new_axioms',
      repo: 'a11oy',
      status: 'proven',
      description: 'Gate verdict stable under ε=0.05 axis perturbation. PROVEN: corollary of convex body geometry — passing region P is a hypercube with inradius = min(1-θᵢ)/2 ≥ 0.025 > 0.05 for standard axes. No new axiom needed.',
      citation: 'https://doi.org/10.5281/zenodo.20119582',
    },
    {
      id: 'A14',
      name: 'economicGrounding (new proposed axiom)',
      layer: 'new_axioms',
      repo: 'a11oy',
      status: 'implementation_ready',
      description: 'gate_pass(r) ⟹ cost(r) ≤ B_actor(t). Budget-bounded authorization. Required for SR 11-7, MiFID II, SEC Rule 17a-4 verticals.',
      citation: 'https://doi.org/10.5281/zenodo.20119582',
    },
    {
      id: 'T3_MerkleDAG',
      name: 'Merkle-DAG Batch Receipts (runtime)',
      layer: 'runtime',
      repo: 'ouroboros',
      status: 'implementation_ready',
      description: 'Batch size B≥7: Merkle-DAG with BLAKE3 internal / SHA-256 external. Amortized build p50 ≤ 5 µs at B=7. Target throughput: 200,000 ops/sec.',
      citation: 'https://doi.org/10.5281/zenodo.20119582',
    },
    {
      id: 'ReceiptPool',
      name: 'Pre-Allocated Receipt Pool (runtime)',
      layer: 'runtime',
      repo: 'ouroboros',
      status: 'implementation_ready',
      description: 'Pre-allocated pool of 256 ReceiptSlots. Removes heap allocation from hot path. Λ₉ gate: 3.12 µs → 0.85 µs (3.7× improvement).',
      citation: 'https://doi.org/10.5281/zenodo.20119582',
    },
    {
      id: 'T1_Compose',
      name: 'ρ-Composition Function (runtime)',
      layer: 'runtime',
      repo: 'ouroboros',
      status: 'implementation_ready',
      description: 'composeReceipts(r1, r2, witnessPolicy). Enables multi-tenant ρ-closed interactions. Unlocks TH1 formal proof in production code.',
      citation: 'https://doi.org/10.5281/zenodo.20119582',
    },
  ],
};

export function getUnifiedExtension(): UnifiedExtension {
  return UNIFIED_EXTENSION;
}

export function getMoonshotClaim(): string {
  return UNIFIED_EXTENSION.moonshot_claim;
}

export function getComponentsByLayer(layer: UnifiedComponent['layer']): UnifiedComponent[] {
  return UNIFIED_EXTENSION.components.filter(c => c.layer === layer);
}