packages/policy/src/gates/README.md

# a11oy Policy Gates — All 35 Anchor Formulas

**Author:** Lutar, Stephen P. — ORCID 0009-0001-0110-4173 — SZL Holdings  
**Lean commit anchor:** `1dca00032dfc9aa8559cc6c2e4b63192fcf52371`  
**Zenodo concept DOI:** https://doi.org/10.5281/zenodo.20162352  
**License:** Apache-2.0

This directory contains Layer 6 (L6 policy gate) implementations for all 35 anchor formulas
instilled across the 7-layer SZL stack (L1 Lean, L2 TS runtime, L3 parity, L4 OTel,
L5 DSSE receipt, L6 policy gate, L7 forecast).

Five gates were wired in a11oy#108 (`cursor/policy-gates-hardening-2f18`).
Thirty new gates are added here. All 35 are barrel-exported from `index.ts`.

---

## Legend

| Column | Meaning |
|---|---|
| **Lean status** | `theorem` = no sorrys; `axiom` = design axiom; `conjectured` = pending proof; `measured` = empirical; `sorry` = active sorry |
| **Severity** | `enforced` = blocks pipeline; `advisory` = warns only (STAGED) |
| **Layer** | Axioms (A), Derivations (T), New Theorems (TH), Lean Theorems (TH_L) |

---

## All 35 Gates

### Already wired in a11oy#108 (5)

| # | ID | Gate file | Formula | Lean file | Lean status | Severity |
|---|---|---|---|---|---|---|
| 1 | TH8 | `adversarialRobustness_gate.ts` | AdversarialRobustness | `Lutar/Composition/AdversarialRobustness.lean` | theorem | enforced |
| 2 | Rhind | `falsePosition_gate.ts` | FalsePosition | `Lutar/Calibration/FalsePosition.lean` | theorem | enforced |
| 3 | Liu Hui | `liuHuiPi_gate.ts` | LiuHuiPi | `Lutar/Banach/LiuHuiPi.lean` | axiom | **advisory** |
| 4 | Mādhava | `madhavaBound_gate.ts` | MadhavaBound | `Lutar/PACBayes/MadhavaBound.lean` | theorem | enforced |
| 5 | Khipu | `summationInvariant_gate.ts` | SummationInvariant | `Lutar/Khipu/SummationInvariant.lean` | theorem | enforced |

### Axiom gates — A1–A9 (9 new gates)

| # | ID | Gate file | Formula | Lean file | Lean status | Severity |
|---|---|---|---|---|---|---|
| 6 | A1 | `soundnessAxiom_gate.ts` | SoundnessAxiom | `Lutar/Gate/SoundnessAxiom.lean` | theorem | enforced |
| 7 | A2 | `moralGroundingFloor_gate.ts` | MoralGroundingFloor | `Lutar/Gate/MoralGrounding.lean` | theorem | enforced |
| 8 | A3 | `measurabilityHonestyFloor_gate.ts` | MeasurabilityHonestyFloor | `Lutar/Gate/MeasurabilityHonesty.lean` | theorem | enforced |
| 9 | A4 | `dualWitnessDisjointness_gate.ts` | DualWitnessDisjointness | `Lutar/Gate/DualWitness.lean` | theorem | enforced |
| 10 | A5 | `deterministicReplay_gate.ts` | DeterministicReplay | `Lutar/Gate/DeterministicReplay.lean` | theorem | enforced |
| 11 | A6 | `hashChainIntegrity_gate.ts` | HashChainIntegrity | `Lutar/Gate/HashChainIntegrity.lean` | theorem | enforced |
| 12 | A7 | `bekensteinBound_gate.ts` | BekensteinBound | `Lutar/Gate/BekensteinBound.lean` | conjectured | **advisory** (STAGED) |
| 13 | A8 | `ingestDiscipline_gate.ts` | IngestDiscipline | `Lutar/Gate/IngestDiscipline.lean` | theorem | enforced |
| 14 | A9 | `doctrineCompleteness_gate.ts` | DoctrineCompleteness | `Lutar/Gate/DoctrineCompleteness.lean` | theorem | enforced |

### Proposed Axiom gates — A10–A14 (4 new gates; A13 = adversarialRobustness, already done)

| # | ID | Gate file | Formula | Lean file | Lean status | Severity |
|---|---|---|---|---|---|---|
| 15 | A10 | `temporalConsistency_gate.ts` | TemporalConsistency | `Lutar/Gate/TemporalConsistency.lean` | theorem | enforced |
| 16 | A11 | `causalSeparability_gate.ts` | CausalSeparability | `Lutar/Gate/CausalSeparability.lean` | theorem | enforced |
| 17 | A12 | `constructiveTransparency_gate.ts` | ConstructiveTransparency | `Lutar/Gate/ConstructiveTransparency.lean` | theorem | enforced |
| 18 | A14 | `economicGrounding_gate.ts` | EconomicGrounding | `Lutar/Gate/EconomicGrounding.lean` | theorem | enforced |

### Derivation gates — T1–T10 (10 new gates)

| # | ID | Gate file | Formula | Lean file | Lean status | Severity |
|---|---|---|---|---|---|---|
| 19 | T1 | `rhoClosureComposition_gate.ts` | RhoClosureComposition | `Lutar/Gate/RhoClosureComposition.lean` | theorem | enforced |
| 20 | T2 | `lambdaMonotonicity_gate.ts` | LambdaMonotonicity | `Lutar/Gate/LambdaMonotonicity.lean` | theorem | enforced |
| 21 | T3 | `merkleDagBatch_gate.ts` | MerkleDagBatch | `Lutar/Gate/MerkleDagBatch.lean` | theorem | enforced |
| 22 | T4 | `bekensteinEntropyMeasure_gate.ts` | BekensteinEntropyMeasure | `Lutar/Gate/BekensteinEntropyMeasure.lean` | conjectured | enforced |
| 23 | T5 | `replayDeterminism_gate.ts` | ReplayDeterminism | `Lutar/Gate/ReplayDeterminism.lean` | theorem | enforced |
| 24 | T6 | `conjunctiveGateCounterexample_gate.ts` | ConjunctiveGateCounterexample | `Lutar/Gate/ConjunctiveGate.lean` | theorem | enforced |
| 25 | T7 | `privacyMask_gate.ts` | PrivacyMask | `Lutar/Gate/PrivacyMask.lean` | theorem | enforced |
| 26 | T8 | `singleWitnessExclusion_gate.ts` | SingleWitnessExclusion | `Lutar/Gate/SingleWitnessExclusion.lean` | theorem | enforced |
| 27 | T9 | `crossRegionPolicy_gate.ts` | CrossRegionPolicy | `Lutar/Gate/CrossRegionPolicy.lean` | theorem | enforced |
| 28 | T10 | `doctrineEnforcement_gate.ts` | DoctrineEnforcement | `Lutar/Gate/DoctrineEnforcement.lean` | theorem | enforced |

### New Theorem gates — TH1–TH7 (7 new gates; TH8 = adversarialRobustness, already done)

| # | ID | Gate file | Formula | Lean file | Lean status | Severity |
|---|---|---|---|---|---|---|
| 29 | TH1 | `composability_gate.ts` | Composability | `Lutar/Composition/Composability.lean` | theorem | enforced |
| 30 | TH2 | `replayDoiDuality_gate.ts` | ReplayDoiDuality | `Lutar/Composition/ReplayDoiDuality.lean` | theorem | enforced |
| 31 | TH3 | `anatomyReduction_gate.ts` | AnatomyReduction | `Lutar/Composition/AnatomyReduction.lean` | theorem | enforced |
| 32 | TH4 | `lambdaCategoryComposability_gate.ts` | LambdaCategoryComposability | `Lutar/LaxFunctor.lean` | conjectured | **advisory** (STAGED) |
| 33 | TH5 | `receiptChainConfluence_gate.ts` | ReceiptChainConfluence | `Lutar/Composition/ReceiptChainConfluence.lean` | conjectured | enforced |
| 34 | TH6 | `bekensteinEntropyDpi_gate.ts` | BekensteinEntropyDpi | `Lutar/EntropyBound.lean` | theorem | enforced |
| 35 | TH7 | `curryHowardReceiptCalculus_gate.ts` | CurryHowardReceiptCalculus | `Lutar/CurryHoward.lean` | theorem | enforced |

### Lean Theorem gates — TH_L1–TH_L4 (4 new gates)

| # | ID | Gate file | Formula | Lean file | Lean status | Severity |
|---|---|---|---|---|---|---|
| 32b | TH_L1 | `lambdaUniquenessConjecture_gate.ts` | LambdaUniquenessConjecture | `Lutar/Uniqueness.lean` | conjecture-open (NOT a theorem — Doctrine v11) | advisory-conjecture |
| 33b | TH_L2 | `lambdaMinMaxBounds_gate.ts` | LambdaMinMaxBounds | `Lutar/Bound.lean` | theorem (2 sorry in wider repo) | enforced |
| 34b | TH_L3 | `bekensteinSoundness_gate.ts` | BekensteinSoundness | `Lutar/BekensteinSoundness.lean` | measured/conjectured | **advisory** (STAGED) |
| 35b | TH_L4 | `rhoClosureProduction_gate.ts` | RhoClosureProduction | `Lutar/RhoClosureProduction.lean` | measured | enforced |

---

## STAGED — Advisory-only gates

The following gates carry `STAGED-ADVISORY` labels. They warn but do not block
production by default. They will be promoted to `enforced` when the corresponding
Lean proofs are formally discharged:

| Gate | Reason for STAGED label |
|---|---|
| `bekensteinBound_gate.ts` (A7) | Lean proof conjectured; TH6 DPI discharges formally but A7 file pending |
| `lambdaCategoryComposability_gate.ts` (TH4) | Pending `Lutar/LaxFunctor.lean` |
| `bekensteinSoundness_gate.ts` (TH_L3) | Pending `lutar-lean` PR #12 |
| `liuHuiPi_gate.ts` (Liu Hui — from a11oy#108) | Lean axiom-structured; advisory by design |

To promote any STAGED gate to enforced, pass `{ enforced: true }` in config
or remove the `enforced: false` default.

---

## Lean Status Summary

| Status | Count |
|---|---|
| theorem (0 sorry) | 25 |
| conjectured | 4 |
| axiom | 1 |
| measured | 2 |
| measured/conjectured | 1 |
| sorry (2 in wider repo, not gate file) | 2 |
| **Total** | **35** |

---

## Wiring to a11oy#108

To merge this output into the `cursor/policy-gates-hardening-2f18` branch:

```bash
# From the a11oy repo root
cp formula_gates_30/packages/policy/src/gates/*_gate.ts packages/policy/src/gates/
cp formula_gates_30/packages/policy/src/gates/index.ts packages/policy/src/gates/index.ts
cp formula_gates_30/packages/policy/src/gates/README.md packages/policy/src/gates/README.md
cp formula_gates_30/packages/policy/src/gates/__tests__/policy_gates_extended.test.ts \
   packages/policy/src/gates/__tests__/policy_gates_extended.test.ts

# Run tests
pnpm vitest run packages/policy/src/gates/__tests__/
```

The extended test file (`policy_gates_extended.test.ts`) is additive — it imports
from the barrel `index.ts` and runs 90 tests (3 per new gate). The existing
`policy_gates.test.ts` from a11oy#108 continues to cover the original 5 gates.

---

## Doctrine v6 compliance

- No marketing superlatives in gate files, tests, or this README
- All STAGED labels are honest and explicitly noted
- Each gate file is signed with SPDX + ORCID header
- Every gate cites the Lean file, theorem name, and commit SHA
- Tests cover: positive (allow), negative (deny), edge (boundary/throw)
- Lean status accurately reflects the knowledge.json maturity field