{"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":"proved","lean_verified":true},{"name":"anatomyReduction","file":"anatomyReduction_gate.ts","description":"a11oy policy gate for AnatomyReduction (TH3)","formula":"AnatomyReduction","lean_theorem":"composition_overhead_bound","lean_file":"Lutar/Composition/CompositionOverhead.lean","lean_status":"proved","lean_verified":true},{"name":"bekensteinBound","file":"bekensteinBound_gate.ts","description":"a11oy policy gate for BekensteinBound (A7)","formula":"BekensteinBound","lean_theorem":"bousso_bound_rhs_nonneg","lean_file":"Lutar/Putnam/BekensteinBousso.lean","lean_status":"proved","lean_verified":true},{"name":"bekensteinEntropyDpi","file":"bekensteinEntropyDpi_gate.ts","description":"a11oy policy gate for BekensteinEntropyDpi (TH6)","formula":"BekensteinEntropyDpi","lean_theorem":"dpi_bound_monotone","lean_file":"Lutar/DPI/DPIBound.lean","lean_status":"proved","lean_verified":true},{"name":"bekensteinEntropyMeasure","file":"bekensteinEntropyMeasure_gate.ts","description":"a11oy policy gate for BekensteinEntropyMeasure (T4)","formula":"BekensteinEntropyMeasure","lean_theorem":"dpi_receipt_chain_entropy_bound","lean_file":"Lutar/DPI/TH6_DPI_Soundness.lean","lean_status":"conjecture — proof-deferred (sorry)","lean_verified":false},{"name":"bekensteinSoundness","file":"bekensteinSoundness_gate.ts","description":"a11oy policy gate for BekensteinSoundness (TH_L3)","formula":"BekensteinSoundness","lean_theorem":"dpi_bound_positive","lean_file":"Lutar/DPI/DPIBound.lean","lean_status":"proved","lean_verified":true},{"name":"causalSeparability","file":"causalSeparability_gate.ts","description":"a11oy policy gate for CausalSeparability (A11)","formula":"CausalSeparability","lean_theorem":"r3_invariance","lean_file":"Lutar/Knot/ReidemeisterConjecture.lean","lean_status":"proved","lean_verified":true},{"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":"proved","lean_verified":true},{"name":"composability","file":"composability_gate.ts","description":"a11oy policy gate for Composability (TH1)","formula":"Composability","lean_theorem":"composition_preserves_doctrine","lean_file":"Lutar/Composition/TH1_Composition.lean","lean_status":"proved","lean_verified":true},{"name":"conjunctiveGateCounterexample","file":"conjunctiveGateCounterexample_gate.ts","description":"a11oy policy gate for ConjunctiveGateCounterexample (T6)","formula":"ConjunctiveGateCounterexample","lean_theorem":null,"lean_file":null,"lean_status":"deferred — no theorem","lean_verified":false},{"name":"constructiveTransparency","file":"constructiveTransparency_gate.ts","description":"a11oy policy gate for ConstructiveTransparency (A12)","formula":"ConstructiveTransparency","lean_theorem":"ReceiptSlot.verified_ne_markedUnverifiable","lean_file":"Lutar/DoctrineV3/MeasurabilityHonesty.lean","lean_status":"proved","lean_verified":true},{"name":"crossRegionPolicy","file":"crossRegionPolicy_gate.ts","description":"a11oy policy gate for CrossRegionPolicy (T9)","formula":"CrossRegionPolicy","lean_theorem":null,"lean_file":null,"lean_status":"deferred — no theorem","lean_verified":false},{"name":"curryHowardReceiptCalculus","file":"curryHowardReceiptCalculus_gate.ts","description":"a11oy policy gate for CurryHowardReceiptCalculus (TH7)","formula":"CurryHowardReceiptCalculus","lean_theorem":"receipt_transduction_invariant","lean_file":"Lutar/Transduction/ReceiptInvariant.lean","lean_status":"proved","lean_verified":true},{"name":"deterministicReplay","file":"deterministicReplay_gate.ts","description":"a11oy policy gate for DeterministicReplay (A5)","formula":"DeterministicReplay","lean_theorem":"isReplayRoot_sound","lean_file":"Lutar/PRNG/K10v2_ReplayRoot.lean","lean_status":"proved","lean_verified":true},{"name":"doctrineCompleteness","file":"doctrineCompleteness_gate.ts","description":"a11oy policy gate for DoctrineCompleteness (A9)","formula":"DoctrineCompleteness","lean_theorem":"doctrine_compliant","lean_file":"Lutar/Feynman/FeynmanLineage.lean","lean_status":"proved","lean_verified":true},{"name":"doctrineEnforcement","file":"doctrineEnforcement_gate.ts","description":"a11oy policy gate for DoctrineEnforcement (T10)","formula":"DoctrineEnforcement","lean_theorem":"doctrine_cross_invariant","lean_file":"Lutar/Doctrine/CrossComponentInvariant.lean","lean_status":"proved","lean_verified":true},{"name":"dualWitnessDisjointness","file":"dualWitnessDisjointness_gate.ts","description":"a11oy policy gate for DualWitnessDisjointness (A4)","formula":"DualWitnessDisjointness","lean_theorem":"two_witness_KS18_soundness","lean_file":"Lutar/TwoWitness.lean","lean_status":"proved","lean_verified":true},{"name":"economicGrounding","file":"economicGrounding_gate.ts","description":"a11oy policy gate for EconomicGrounding (A14)","formula":"EconomicGrounding","lean_theorem":"vcgReceiptValid_iff","lean_file":"Lutar/MechanismDesign/VCG.lean","lean_status":"proved","lean_verified":true},{"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":"proved","lean_verified":true},{"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":"proved","lean_verified":true},{"name":"hashChainIntegrity","file":"hashChainIntegrity_gate.ts","description":"a11oy policy gate for HashChainIntegrity (A6)","formula":"HashChainIntegrity","lean_theorem":"sbom_lambda_chain_total_order","lean_file":"Lutar/SBOMProvenance.lean","lean_status":"proved","lean_verified":true},{"name":"ingestDiscipline","file":"ingestDiscipline_gate.ts","description":"a11oy policy gate for IngestDiscipline (A8)","formula":"IngestDiscipline","lean_theorem":null,"lean_file":null,"lean_status":"deferred — no theorem","lean_verified":false},{"name":"lambdaCategoryComposability","file":"lambdaCategoryComposability_gate.ts","description":"a11oy policy gate for LambdaCategoryComposability (TH4)","formula":"LambdaCategoryComposability","lean_theorem":"composeList_doctrine_locked","lean_file":"Lutar/Composition/TH1_Composition.lean","lean_status":"proved","lean_verified":true},{"name":"lambdaMinMaxBounds","file":"lambdaMinMaxBounds_gate.ts","description":"a11oy policy gate for LambdaMinMaxBounds (TH_L2)","formula":"LambdaMinMaxBounds","lean_theorem":"lambda_isBounded","lean_file":"Lutar/Uniqueness.lean","lean_status":"proved","lean_verified":true},{"name":"lambdaMonotonicity","file":"lambdaMonotonicity_gate.ts","description":"a11oy policy gate for LambdaMonotonicity (T2)","formula":"LambdaMonotonicity","lean_theorem":"lambda_isMonotone","lean_file":"Lutar/Uniqueness.lean","lean_status":"proved","lean_verified":true},{"name":"lambdaUniqueness","file":"lambdaUniqueness_gate.ts","description":"a11oy policy gate for LambdaUniqueness (TH_L1)","formula":"LambdaUniqueness","lean_theorem":"lutar_unique","lean_file":"Lutar/Uniqueness.lean","lean_status":"conjecture — Conjecture 1 (NOT a theorem)","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":"proved","lean_verified":true},{"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":"proved","lean_verified":true},{"name":"measurabilityHonestyFloor","file":"measurabilityHonestyFloor_gate.ts","description":"a11oy policy gate for MeasurabilityHonestyFloor (A3)","formula":"MeasurabilityHonestyFloor","lean_theorem":"MeasurabilityHonestyTheorem","lean_file":"Lutar/DoctrineV3/MeasurabilityHonesty.lean","lean_status":"proved","lean_verified":true},{"name":"merkleDagBatch","file":"merkleDagBatch_gate.ts","description":"a11oy policy gate for MerkleDagBatch (T3)","formula":"MerkleDagBatch","lean_theorem":"merkle_dag_height_bound","lean_file":"Lutar/DPI/MerkleDAGBuild.lean","lean_status":"proved","lean_verified":true},{"name":"moralGroundingFloor","file":"moralGroundingFloor_gate.ts","description":"a11oy policy gate for MoralGroundingFloor (A2)","formula":"MoralGroundingFloor","lean_theorem":"MoralGroundingTheorem","lean_file":"Lutar/DoctrineV3/MoralGrounding.lean","lean_status":"proved","lean_verified":true},{"name":"pareto_stabilization","file":"pareto_stabilization.ts","description":"Pareto Finite Stabilization Gate — multi-objective governance optimization","formula":"th_v18_11_pareto_stabilization","lean_theorem":"th_v18_11_pareto_stabilizes","lean_file":"Lutar/Thesis/TH_V18_11_ParetoFiniteStabilization.lean","lean_status":"proved","lean_verified":true},{"name":"privacyMask","file":"privacyMask_gate.ts","description":"a11oy policy gate for PrivacyMask (T7)","formula":"PrivacyMask","lean_theorem":"scitt_mask_entropy_bound","lean_file":"Lutar/DPI/SCITTMaskEntropy.lean","lean_status":"proved","lean_verified":true},{"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":"proved","lean_verified":true},{"name":"receiptChainConfluence","file":"receiptChainConfluence_gate.ts","description":"a11oy policy gate for ReceiptChainConfluence (TH5)","formula":"ReceiptChainConfluence","lean_theorem":"iterated_chain_obligation_tracked","lean_file":"Lutar/Composition/AdversarialRobustness.lean","lean_status":"proved","lean_verified":true},{"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":"proved","lean_verified":true},{"name":"replayDeterminism","file":"replayDeterminism_gate.ts","description":"a11oy policy gate for ReplayDeterminism (T5)","formula":"ReplayDeterminism","lean_theorem":"findReplayRoot_sound","lean_file":"Lutar/PRNG/K10v2_ReplayRoot.lean","lean_status":"proved","lean_verified":true},{"name":"replayDoiDuality","file":"replayDoiDuality_gate.ts","description":"a11oy policy gate for ReplayDoiDuality (TH2)","formula":"ReplayDoiDuality","lean_theorem":null,"lean_file":null,"lean_status":"deferred — no theorem","lean_verified":false},{"name":"rhoClosureComposition","file":"rhoClosureComposition_gate.ts","description":"a11oy policy gate for RhoClosureComposition (T1)","formula":"RhoClosureComposition","lean_theorem":null,"lean_file":null,"lean_status":"deferred — no theorem","lean_verified":false},{"name":"rhoClosureProduction","file":"rhoClosureProduction_gate.ts","description":"a11oy policy gate for RhoClosureProduction (TH_L4)","formula":"RhoClosureProduction","lean_theorem":null,"lean_file":null,"lean_status":"deferred — no theorem","lean_verified":false},{"name":"singleWitnessExclusion","file":"singleWitnessExclusion_gate.ts","description":"a11oy policy gate for SingleWitnessExclusion (T8)","formula":"SingleWitnessExclusion","lean_theorem":"no_NCHV","lean_file":"Lutar/TwoWitness.lean","lean_status":"conjecture — proof-deferred (sorry)","lean_verified":false},{"name":"soundnessAxiom","file":"soundnessAxiom_gate.ts","description":"a11oy policy gate for SoundnessAxiom (A1)","formula":"SoundnessAxiom","lean_theorem":null,"lean_file":null,"lean_status":"deferred — no theorem","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":"proved","lean_verified":true},{"name":"temporalConsistency","file":"temporalConsistency_gate.ts","description":"a11oy policy gate for TemporalConsistency (A10)","formula":"TemporalConsistency","lean_theorem":"wheeler_window_safety","lean_file":"Lutar/Wheeler/DelayedChoiceClosure.lean","lean_status":"proved","lean_verified":true},{"name":"thresholdPolicySeverity","file":"thresholdPolicySeverity_gate.ts","description":"severity-indexed witness threshold policy gate.","formula":"ThresholdPolicySeverity","lean_theorem":null,"lean_file":null,"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/VCG.lean","lean_status":"conjecture — proof-deferred (sorry)","lean_verified":false},{"name":"dualStreamRouting","file":"dualStreamRouting_gate.ts","description":"a11oy policy gate for DualStreamRoutingAxiom (A36)","formula":"dualStreamRouting","lean_theorem":null,"lean_file":null,"lean_status":"deferred — no theorem","lean_verified":false},{"name":"internalFeedback","file":"internalFeedback_gate.ts","description":"a11oy policy gate for InternalFeedbackIntegrity (A37)","formula":"internalFeedback","lean_theorem":null,"lean_file":null,"lean_status":"deferred — no theorem","lean_verified":false},{"name":"hierarchicalLinearization","file":"hierarchicalLinearization_gate.ts","description":"a11oy policy gate for HierarchicalLinearizationRoundTrip (A38)","formula":"hierarchicalLinearization","lean_theorem":null,"lean_file":null,"lean_status":"deferred — no theorem","lean_verified":false}],"doctrine":"v11","canonical":{"declarations":749,"axioms":14,"sorries":163,"mcp_tools":12},"lean_citation_audit":{"verified_against":"LEAN_PROOF_CITATION_MATRIX.csv","real_theorem_citations":34,"deferred_no_theorem":15,"phantom_Lutar_Gate_dir_refs":0}}