{"count":49,"gates":[{"name":"adversarialRobustness","file":"adversarialRobustness_gate.ts","description":"a11oy policy gate for AdversarialRobustness","formula":"AdversarialRobustness","lean_theorem":"robustness_preserved_by_composition","lean_file":"Lutar/Composition/AdversarialRobustness.lean","lean_status":"real","lean_verified":false},{"name":"anatomyReduction","file":"anatomyReduction_gate.ts","description":"a11oy policy gate for AnatomyReduction (TH3)","formula":"AnatomyReduction","lean_theorem":"anatomyReduction","lean_file":"Lutar/Composition/AnatomyReduction.lean","lean_status":"phantom","lean_verified":false},{"name":"bekensteinBound","file":"bekensteinBound_gate.ts","description":"a11oy policy gate for BekensteinBound (A7)","formula":"BekensteinBound","lean_theorem":"bekensteinBound","lean_file":"Lutar/Gate/BekensteinBound.lean","lean_status":"phantom","lean_verified":false},{"name":"bekensteinEntropyDpi","file":"bekensteinEntropyDpi_gate.ts","description":"a11oy policy gate for BekensteinEntropyDpi (TH6)","formula":"BekensteinEntropyDpi","lean_theorem":"bekensteinEntropyDpi","lean_file":"Lutar/EntropyBound.lean","lean_status":"phantom","lean_verified":false},{"name":"bekensteinEntropyMeasure","file":"bekensteinEntropyMeasure_gate.ts","description":"a11oy policy gate for BekensteinEntropyMeasure (T4)","formula":"BekensteinEntropyMeasure","lean_theorem":"Lutar.DPI.dpi_bound_monotone","lean_file":"Lutar/DPI/DPIBound.lean","lean_status":"real","lean_verified":false},{"name":"bekensteinSoundness","file":"bekensteinSoundness_gate.ts","description":"a11oy policy gate for BekensteinSoundness (TH_L3)","formula":"BekensteinSoundness","lean_theorem":"bekensteinSoundness","lean_file":"Lutar/BekensteinSoundness.lean","lean_status":"phantom","lean_verified":false},{"name":"causalSeparability","file":"causalSeparability_gate.ts","description":"a11oy policy gate for CausalSeparability (A11)","formula":"CausalSeparability","lean_theorem":"causalSeparability","lean_file":"Lutar/Gate/CausalSeparability.lean","lean_status":"phantom","lean_verified":false},{"name":"certifiedRobustness","file":"certifiedRobustness_gate.ts","description":"a11oy policy gate for CertifiedRobustnessRadius (G39)","formula":"certifiedRobustness","lean_theorem":"certifiedRobustnessRadiusBound","lean_file":"Lutar/Robustness/CertifiedRadius.lean","lean_status":"real","lean_verified":false},{"name":"composability","file":"composability_gate.ts","description":"a11oy policy gate for Composability (TH1)","formula":"Composability","lean_theorem":"composability","lean_file":"Lutar/Composition/Composability.lean","lean_status":"phantom","lean_verified":false},{"name":"conjunctiveGateCounterexample","file":"conjunctiveGateCounterexample_gate.ts","description":"a11oy policy gate for ConjunctiveGateCounterexample (T6)","formula":"ConjunctiveGateCounterexample","lean_theorem":"conjunctiveGateCounterexample","lean_file":"Lutar/Gate/ConjunctiveGate.lean","lean_status":"phantom","lean_verified":false},{"name":"constructiveTransparency","file":"constructiveTransparency_gate.ts","description":"a11oy policy gate for ConstructiveTransparency (A12)","formula":"ConstructiveTransparency","lean_theorem":"constructiveTransparency","lean_file":"Lutar/Gate/ConstructiveTransparency.lean","lean_status":"phantom","lean_verified":false},{"name":"crossRegionPolicy","file":"crossRegionPolicy_gate.ts","description":"a11oy policy gate for CrossRegionPolicy (T9)","formula":"CrossRegionPolicy","lean_theorem":"crossRegionPolicy","lean_file":"Lutar/Gate/CrossRegionPolicy.lean","lean_status":"phantom","lean_verified":false},{"name":"curryHowardReceiptCalculus","file":"curryHowardReceiptCalculus_gate.ts","description":"a11oy policy gate for CurryHowardReceiptCalculus (TH7)","formula":"CurryHowardReceiptCalculus","lean_theorem":"curryHowardReceiptCalculus","lean_file":"Lutar/CurryHoward.lean","lean_status":"phantom","lean_verified":false},{"name":"deterministicReplay","file":"deterministicReplay_gate.ts","description":"a11oy policy gate for DeterministicReplay (A5)","formula":"DeterministicReplay","lean_theorem":"deterministicReplay","lean_file":"Lutar/Gate/DeterministicReplay.lean","lean_status":"phantom","lean_verified":false},{"name":"doctrineCompleteness","file":"doctrineCompleteness_gate.ts","description":"a11oy policy gate for DoctrineCompleteness (A9)","formula":"DoctrineCompleteness","lean_theorem":"doctrineCompleteness","lean_file":"Lutar/Gate/DoctrineCompleteness.lean","lean_status":"phantom","lean_verified":false},{"name":"doctrineEnforcement","file":"doctrineEnforcement_gate.ts","description":"a11oy policy gate for DoctrineEnforcement (T10)","formula":"DoctrineEnforcement","lean_theorem":"doctrineEnforcement","lean_file":"Lutar/Gate/DoctrineEnforcement.lean","lean_status":"phantom","lean_verified":false},{"name":"dualWitnessDisjointness","file":"dualWitnessDisjointness_gate.ts","description":"a11oy policy gate for DualWitnessDisjointness (A4)","formula":"DualWitnessDisjointness","lean_theorem":"dualWitnessDisjointness","lean_file":"Lutar/Gate/DualWitness.lean","lean_status":"phantom","lean_verified":false},{"name":"economicGrounding","file":"economicGrounding_gate.ts","description":"a11oy policy gate for EconomicGrounding (A14)","formula":"EconomicGrounding","lean_theorem":"economicGrounding","lean_file":"Lutar/Gate/EconomicGrounding.lean","lean_status":"phantom","lean_verified":false},{"name":"falsePosition","file":"falsePosition_gate.ts","description":"a11oy policy gate for FalsePosition","formula":"FalsePosition","lean_theorem":"false_position_correct","lean_file":"Lutar/Calibration/FalsePosition.lean","lean_status":"real","lean_verified":false},{"name":"gaussianMechanismDP","file":"gaussianMechanismDP_gate.ts","description":"a11oy policy gate for GaussianMechanismDP (G36)","formula":"gaussianMechanismDP","lean_theorem":"gaussianNoiseSufficiency","lean_file":"Lutar/DP/GaussianMechanism.lean","lean_status":"real","lean_verified":false},{"name":"hashChainIntegrity","file":"hashChainIntegrity_gate.ts","description":"a11oy policy gate for HashChainIntegrity (A6)","formula":"HashChainIntegrity","lean_theorem":"hashChainIntegrity","lean_file":"Lutar/Gate/HashChainIntegrity.lean","lean_status":"phantom","lean_verified":false},{"name":"ingestDiscipline","file":"ingestDiscipline_gate.ts","description":"a11oy policy gate for IngestDiscipline (A8)","formula":"IngestDiscipline","lean_theorem":"ingestDiscipline","lean_file":"Lutar/Gate/IngestDiscipline.lean","lean_status":"phantom","lean_verified":false},{"name":"lambdaCategoryComposability","file":"lambdaCategoryComposability_gate.ts","description":"a11oy policy gate for LambdaCategoryComposability (TH4)","formula":"LambdaCategoryComposability","lean_theorem":"lambdaCategoryComposability","lean_file":"Lutar/LaxFunctor.lean","lean_status":"phantom","lean_verified":false},{"name":"lambdaMinMaxBounds","file":"lambdaMinMaxBounds_gate.ts","description":"a11oy policy gate for LambdaMinMaxBounds (TH_L2)","formula":"LambdaMinMaxBounds","lean_theorem":"lambdaMinMaxBounds","lean_file":"Lutar/Bound.lean","lean_status":"real","lean_verified":false},{"name":"lambdaMonotonicity","file":"lambdaMonotonicity_gate.ts","description":"a11oy policy gate for LambdaMonotonicity (T2)","formula":"LambdaMonotonicity","lean_theorem":"lambdaMonotonicity","lean_file":"Lutar/Gate/LambdaMonotonicity.lean","lean_status":"phantom","lean_verified":false},{"name":"lambdaUniquenessConjecture","file":"lambdaUniquenessConjecture_gate.ts","description":"a11oy policy gate for LambdaUniquenessConjecture (TH_L1) — Conjecture 1, NOT a theorem","formula":"LambdaUniquenessConjecture","lean_theorem":"lambdaUniquenessConjecture","lean_file":"Lutar/Uniqueness.lean","lean_status":"real","lean_verified":false},{"name":"liuHuiPi","file":"liuHuiPi_gate.ts","description":"a11oy policy gate for LiuHuiPi","formula":"LiuHuiPi","lean_theorem":"sideSquared_bounds","lean_file":"Lutar/Banach/LiuHuiPi.lean","lean_status":"real","lean_verified":false},{"name":"madhavaBound","file":"madhavaBound_gate.ts","description":"a11oy policy gate for MadhavaBound","formula":"MadhavaBound","lean_theorem":"madhavaRemainderBound_nonneg","lean_file":"Lutar/PACBayes/MadhavaBound.lean","lean_status":"real","lean_verified":false},{"name":"measurabilityHonestyFloor","file":"measurabilityHonestyFloor_gate.ts","description":"a11oy policy gate for MeasurabilityHonestyFloor (A3)","formula":"MeasurabilityHonestyFloor","lean_theorem":"measurabilityHonestyFloor","lean_file":"Lutar/Gate/MeasurabilityHonesty.lean","lean_status":"phantom","lean_verified":false},{"name":"merkleDagBatch","file":"merkleDagBatch_gate.ts","description":"a11oy policy gate for MerkleDagBatch (T3)","formula":"MerkleDagBatch","lean_theorem":"merkleDagBatch","lean_file":"Lutar/Gate/MerkleDagBatch.lean","lean_status":"phantom","lean_verified":false},{"name":"moralGroundingFloor","file":"moralGroundingFloor_gate.ts","description":"a11oy policy gate for MoralGroundingFloor (A2)","formula":"MoralGroundingFloor","lean_theorem":"moralGroundingFloor","lean_file":"Lutar/Gate/MoralGrounding.lean","lean_status":"phantom","lean_verified":false},{"name":"pareto_stabilization","file":"pareto_stabilization.ts","description":"Pareto Finite Stabilization Gate — multi-objective governance optimization","formula":"th_v18_11_pareto_stabilization","lean_theorem":"Lutar.Thesis.ParetoStabilization.th_v18_11_pareto_stabilization","lean_file":"Lutar/Thesis/TH_V18_11_ParetoFiniteStabilization.lean","lean_status":"real","lean_verified":false},{"name":"privacyMask","file":"privacyMask_gate.ts","description":"a11oy policy gate for PrivacyMask (T7)","formula":"PrivacyMask","lean_theorem":"privacyMask","lean_file":"Lutar/Gate/PrivacyMask.lean","lean_status":"phantom","lean_verified":false},{"name":"rdpComposition","file":"rdpComposition_gate.ts","description":"a11oy policy gate for RDPSequentialComposition (G38)","formula":"rdpComposition","lean_theorem":"rdpSequentialCompositionAdditivity","lean_file":"Lutar/DP/RDPComposition.lean","lean_status":"real","lean_verified":false},{"name":"receiptChainConfluence","file":"receiptChainConfluence_gate.ts","description":"a11oy policy gate for ReceiptChainConfluence (TH5)","formula":"ReceiptChainConfluence","lean_theorem":"receiptChainConfluence","lean_file":"Lutar/Composition/ReceiptChainConfluence.lean","lean_status":"phantom","lean_verified":false},{"name":"reedSolomonSingleton","file":"reedSolomonSingleton_gate.ts","description":"a11oy policy gate for ReedSolomonSingletonBound (G40)","formula":"reedSolomonSingleton","lean_theorem":"reedSolomonMDSProperty","lean_file":"Lutar/CodingTheory/ReedSolomonSingleton.lean","lean_status":"real","lean_verified":false},{"name":"replayDeterminism","file":"replayDeterminism_gate.ts","description":"a11oy policy gate for ReplayDeterminism (T5)","formula":"ReplayDeterminism","lean_theorem":"replayDeterminism","lean_file":"Lutar/Gate/ReplayDeterminism.lean","lean_status":"phantom","lean_verified":false},{"name":"replayDoiDuality","file":"replayDoiDuality_gate.ts","description":"a11oy policy gate for ReplayDoiDuality (TH2)","formula":"ReplayDoiDuality","lean_theorem":"replayDoiDuality","lean_file":"Lutar/Composition/ReplayDoiDuality.lean","lean_status":"phantom","lean_verified":false},{"name":"rhoClosureComposition","file":"rhoClosureComposition_gate.ts","description":"a11oy policy gate for RhoClosureComposition (T1)","formula":"RhoClosureComposition","lean_theorem":"rhoClosureComposition","lean_file":"Lutar/Gate/RhoClosureComposition.lean","lean_status":"phantom","lean_verified":false},{"name":"rhoClosureProduction","file":"rhoClosureProduction_gate.ts","description":"a11oy policy gate for RhoClosureProduction (TH_L4)","formula":"RhoClosureProduction","lean_theorem":"rhoClosureProduction","lean_file":"Lutar/RhoClosureProduction.lean","lean_status":"phantom","lean_verified":false},{"name":"singleWitnessExclusion","file":"singleWitnessExclusion_gate.ts","description":"a11oy policy gate for SingleWitnessExclusion (T8)","formula":"SingleWitnessExclusion","lean_theorem":"singleWitnessExclusion","lean_file":"Lutar/Gate/SingleWitnessExclusion.lean","lean_status":"phantom","lean_verified":false},{"name":"soundnessAxiom","file":"soundnessAxiom_gate.ts","description":"a11oy policy gate for SoundnessAxiom (A1)","formula":"SoundnessAxiom","lean_theorem":"soundnessAxiom","lean_file":"Lutar/Gate/SoundnessAxiom.lean","lean_status":"phantom","lean_verified":false},{"name":"summationInvariant","file":"summationInvariant_gate.ts","description":"a11oy policy gate for SummationInvariant","formula":"SummationInvariant","lean_theorem":"khipuReceipt_checksum_invariant","lean_file":"Lutar/Khipu/SummationInvariant.lean","lean_status":"real","lean_verified":false},{"name":"temporalConsistency","file":"temporalConsistency_gate.ts","description":"a11oy policy gate for TemporalConsistency (A10)","formula":"TemporalConsistency","lean_theorem":"temporalConsistency","lean_file":"Lutar/Gate/TemporalConsistency.lean","lean_status":"phantom","lean_verified":false},{"name":"thresholdPolicySeverity","file":"thresholdPolicySeverity_gate.ts","description":"severity-indexed witness threshold policy gate.","formula":"ThresholdPolicySeverity","lean_theorem":"","lean_file":"","lean_status":"deferred — no theorem","lean_verified":false},{"name":"vcgTruthfulness","file":"vcgTruthfulness_gate.ts","description":"a11oy policy gate for VCGTruthfulness (G37)","formula":"vcgTruthfulness","lean_theorem":"vcgDominantStrategyTruth","lean_file":"Lutar/MechanismDesign/VCGTruthfulness.lean","lean_status":"phantom","lean_verified":false},{"name":"dualStreamRoutingAxiom","file":"packages/policy/src/gates/InternalFeedback.lean","description":"a11oy policy gate for DualStreamRoutingAxiom (A36) — Hickok dual-stream axis.","formula":"DualStreamRoutingAxiom","lean_theorem":"dual_stream_routing","lean_file":"Lutar/Gate/InternalFeedback.lean","lean_status":"phantom","lean_verified":false},{"name":"internalFeedbackIntegrity","file":"conduction_aphasia.py","description":"a11oy policy gate for InternalFeedbackIntegrity (A37) — Hickok state feedback control. The Conduction-Aphasia Detector IS the live evaluator.","formula":"InternalFeedbackIntegrity","lean_theorem":"internal_feedback_intact","lean_file":"Lutar/Gate/InternalFeedback.lean","lean_status":"phantom","lean_verified":false},{"name":"hierarchicalLinearizationRoundTrip","file":"packages/policy/src/gates/InternalFeedback.lean","description":"a11oy policy gate for HierarchicalLinearizationRoundTrip (A38) — Hickok hierarchical linearization, Khipu chain losslessness.","formula":"HierarchicalLinearizationRoundTrip","lean_theorem":"hier_linearization_round_trip","lean_file":"Lutar/Gate/InternalFeedback.lean","lean_status":"phantom","lean_verified":false}],"doctrine":"v11","canonical":{"declarations":749,"axioms":14,"sorries":163,"mcp_tools":12,"experimental_scope":{"kernel_commit":"7885fd9","lean":"v4.18.0","declarations":1304,"axioms_unique":22,"theorems_ci_green":36,"note":"CI-green, kernel-verified (Wave5-8 + agentic P1-P6 + airtight Λ + coder); NOT folded into the locked count of 8; Λ stays Conjecture 1"}},"lean_citation_audit":{"verified_against":"LEAN_PROOF_CITATION_MATRIX.csv","real_theorem_citations":0,"deferred_no_theorem":49,"phantom_Lutar_Gate_dir_refs":0}}