Skip to content

TestPlan.md

Latest commit

 

History

History
665 lines (650 loc) · 46.4 KB

TestPlan.md

File metadata and controls

665 lines (650 loc) · 46.4 KB
Raw

Test Plan

The test suite exists to catch public API regressions, import-boundary breaks, policy violations, and text encoding damage.

Main Commands

python .github/scripts/check_text_quality.py
python scripts/judge_policy_check.py
lake build
lake build HighDimProb.Examples
lake build HighDimProbJudge
lake test

For docs-only edits, run at least:

python .github/scripts/check_text_quality.py
python scripts/judge_policy_check.py
git diff --check

Important Test Surfaces

  • Root import smoke tests: HighDimProbTest/Smoke.lean, PublicImports.lean, BranchImports.lean, ExperimentalImports.lean.
  • Scalar API tests: probability, tail, Lp/moment, Orlicz, subGaussian, subExponential, real-inequality helpers, and scalar concentration files under HighDimProbTest.
  • Random-family and process API checks: HighDimProbTest/RandomFamilyAPI.lean plus BranchImports.lean and ExperimentalImports.lean.
  • PrecisionDA application checks: HighDimProbTest/PrecisionDAAPI.lean covers the deterministic PrecisionDA object/provider surface, HighDimProbTest/ExamplesAPI.lean covers the reader-facing example import, and HighDimProbJudge/PrecisionDA/CovarianceTraceExpansionUse.lean covers the judge consumer. It also covers the deterministic H2 event factorization names paperH2ResolventGoodEvent, paperH2ResolventBadEvent, paperH2ResolventBadEvent_mem_iff, paperH2ResolventBadEvent_eq_compl, paperH2LeaveOneOutResolventGoodEvent, paperH2LeaveOneOutGoodEvent_mem_iff, paperH2LeaveOneOutGoodEvent_eq_inter, paperH2LeaveOneOutBadEvent_mem_imp_lowerBad_or_resolventBad, paperH2LeaveOneOutBadEvent_subset_lowerBad_union_resolventBad, and the lower/resolvent projection plus constructor theorems, including paperH2LeaveOneOutGoodEvent_of_lowerEventProvider_and_resolvent and paperH2LeaveOneOutGoodEvent_eq_resolventGood_of_lowerEventProvider. The same API test covers the lower-provider/resolvent-provider measurability convenience wrappers paperH2LeaveOneOutGoodEvent_measurable_of_lowerEventProvider_and_resolventProvider, paperH2LeaveOneOutGoodEventMeasurabilityProvider_of_lowerEventProvider_and_resolventProvider, and paperH2LeaveOneOutBadEventMeasurabilityProvider_of_lowerEventProvider_and_resolventProvider. It also covers the H2 good-event measurability provider records and projection/bridge names: PaperH2LowerSingularValueGoodEventMeasurabilityProvider, PaperH2LowerSingularValueBadEventMeasurabilityProvider, PaperH2ResolventGoodEventMeasurabilityProvider, PaperH2ResolventBadEventMeasurabilityProvider, PaperH2LeaveOneOutGoodEventMeasurabilityProvider, PaperH2LowerSingularValueStatement_eta_positive, PaperH2LowerSingularValueStatement_good_event, paperH2LowerSingularValueEventProvider_h2_lower_singular_value, paperH2LowerSingularValueEventProvider_eta_positive, paperH2LowerSingularValueGoodEventMeasurabilityProvider_lower_singular_value_good_event_measurable, paperH2LowerSingularValueBadEventMeasurabilityProvider_lower_singular_value_bad_event_measurable, paperH2ResolventGoodEventMeasurabilityProvider_resolvent_good_event_measurable, paperH2ResolventBadEventMeasurabilityProvider_resolvent_bad_event_measurable, paperH2LeaveOneOutGoodEventMeasurabilityProvider_good_event_measurable, paperH2LeaveOneOutBadEventMeasurabilityProvider_bad_event_measurable, paperH2LowerSingularValueGoodEvent_measurable_of_provider, paperH2LowerSingularValueBadEvent_measurable_of_provider, paperH2LowerSingularValueGoodEvent_measurable_of_badEventProvider, paperH2LowerSingularValueGoodEventMeasurabilityProvider_of_badEventProvider, paperH2LowerSingularValueBadEventMeasurabilityProvider_of_goodEventProvider, paperH2LowerSingularValueGoodEvent_eq_univ_of_statement, paperH2LowerSingularValueGoodEvent_eq_univ_of_eventProvider, paperH2LowerSingularValueGoodEvent_mem_of_eventProvider, paperH2LeaveOneOutGoodEvent_of_lowerEventProvider_and_resolvent, paperH2LeaveOneOutGoodEvent_eq_resolventGood_of_lowerEventProvider, paperH2LeaveOneOutGoodEvent_measurable_of_lowerEventProvider_and_resolventProvider, paperH2LeaveOneOutGoodEventMeasurabilityProvider_of_lowerEventProvider_and_resolventProvider, paperH2LeaveOneOutBadEventMeasurabilityProvider_of_lowerEventProvider_and_resolventProvider, paperH2LowerSingularValueBadEvent_eq_empty_of_statement, paperH2LowerSingularValueGoodEvent_measurable_of_statement, paperH2LowerSingularValueBadEvent_measurable_of_statement, paperH2LowerSingularValueGoodEventMeasurabilityProvider_of_eventProvider, paperH2LowerSingularValueBadEventMeasurabilityProvider_of_eventProvider, paperH2LeaveOneOutGoodEventMeasurabilityProvider_of_h1_and_lowerEventProvider, paperH2LeaveOneOutBadEventMeasurabilityProvider_of_h1_and_lowerEventProvider, paperH2LowerSingularValueBadEvent_measure_eq_zero_of_statement, paperH2LowerSingularValueBadEvent_eq_empty_of_eventProvider, paperH2LowerSingularValueBadEvent_measure_eq_zero_of_eventProvider, PaperH2LowerSingularValueBadEventProbabilityStatement, PaperH2LowerSingularValueBadEventProbabilityProvider, paperH2LowerSingularValueBadEventProbabilityProvider_lower_bad_event_probability, paperH2LowerSingularValueBadEventProbabilityStatement_of_statement, paperH2LowerSingularValueBadEventProbabilityProvider_of_eventProvider, paperH2LowerSingularValueBadEventProbability_bound_of_eventProvider, PaperH2ResolventBadEventProbabilityStatement, PaperH2ResolventBadEventProbabilityProvider, paperH2ResolventBadEventProbabilityProvider_resolvent_bad_event_probability, paperH2ResolventBadEventProbabilityStatement_of_provider, paperH2ResolventBadEventProbability_bound_of_provider, PaperH2LeaveOneOutBadEventUnionBoundStatement, PaperH2LeaveOneOutBadEventUnionBoundStatement_lower_bad_event_probability, PaperH2LeaveOneOutBadEventUnionBoundStatement_resolvent_bad_event_probability, PaperH2LeaveOneOutBadEventUnionBoundStatement_bad_event_probability, paperH2LeaveOneOutBadEventUnionBoundStatement_of_probabilityProviders, paperH2LeaveOneOutBadEventUnionBound_bound_of_probabilityProviders, paperH2LeaveOneOutBadEventUnionBoundRHS, paperH2LeaveOneOutBadEventUnionBoundRHS_nonnegative, paperH2LeaveOneOutBadEventUnionBound_bound_of_probabilityProviders_realRHS, PaperH2LeaveOneOutBadEventUnionBoundRHSProvider, paperH2LeaveOneOutBadEventUnionBoundRHSProvider_self, paperH2LeaveOneOutBadEventUnionBoundRHSProvider_rhs_eq, paperH2LeaveOneOutBadEventUnionBoundRHSProvider_nonnegative, paperH2LeaveOneOutBadEventUnionBound_bound_of_probabilityProviders_rhsProvider, paperH2LeaveOneOutBadEventUnionBoundStatement_of_lowerEventProvider_and_resolventProbabilityProvider, paperH2LeaveOneOutBadEventUnionBound_bound_of_lowerEventProvider_and_resolventProbabilityProvider, paperH2LeaveOneOutBadEventUnionBound_bound_of_lowerEventProvider_and_resolventProbabilityProvider_realRHS, PaperH2LeaveOneOutGoodEventStatement_eta_positive, PaperH2LeaveOneOutGoodEventStatement_good_event, paperH2LeaveOneOutGoodEventProvider_h2, paperH2LeaveOneOutGoodEventProbabilityProvider_of_unionBoundProbabilityProviders, paperH2LeaveOneOutGoodEventProbabilityProvider_of_lowerEventProvider_and_resolventProbabilityProvider, PaperH2LeaveOneOutGoodEventProbabilityStatement_eta_positive, PaperH2LeaveOneOutGoodEventProbabilityStatement_rhs_nonnegative, PaperH2LeaveOneOutGoodEventProbabilityStatement_bad_event_probability, paperH2LowerSingularValueProvider_eta_positive, paperH2LowerSingularValueProvider_rhs_nonnegative, paperH2LowerSingularValueProvider_bad_event_measurable, paperH2LowerSingularValueProvider_bad_event_probability, paperH2LeaveOneOutGoodEventProbabilityProvider_h2_probability, paperH2LeaveOneOutProbabilityConsumerStatement_bad_event_measurable, paperH2LeaveOneOutProbabilityConsumerStatement_h2_probability, paperH2LeaveOneOutProbabilityConsumerStatement_bad_event_probability, shrinkageTheorem1PaperTailH2UnionBoundStatement_of_providers, shrinkageTheorem1PaperTailH2UnionBound_badEventProbability_of_providers, shrinkageTheorem1PaperTailH2UnionBound_realRHS_badEventProbability_of_providers, shrinkageTheorem1PaperTailH2UnionBoundStatement_of_lowerEventProvider_and_resolventProbabilityProvider, shrinkageTheorem1PaperTailH2UnionBound_badEventProbability_of_lowerEventProvider_and_resolventProbabilityProvider, shrinkageTheorem1PaperTailH2UnionBound_realRHS_badEventProbability_of_lowerEventProvider_and_resolventProbabilityProvider, shrinkageTheorem1PaperTailH2Probability_of_unionBoundProbabilityProviders, shrinkageTheorem1PaperTailH2Probability_of_lowerEventProvider_and_resolventProbabilityProvider, shrinkageTheorem1PaperTailH2ProbabilityConsumerStatement_of_unionBoundProbabilityProviders, shrinkageTheorem1PaperTailH2ProbabilityConsumerStatement_of_lowerEventProvider_and_resolventProbabilityProvider, shrinkageTheorem1PaperTailH2ProbabilityConsumerStatement_of_lowerEventProvider_and_resolventPaperRHSBounds, shrinkageTheorem1PaperTailH2ProbabilityConsumer_of_unionBoundProbabilityProviders, shrinkageTheorem1PaperTailH2ProbabilityConsumer_of_lowerEventProvider_and_resolventProbabilityProvider, shrinkageTheorem1PaperTailH2ProbabilityConsumer_of_lowerEventProvider_and_resolventPaperRHSBounds, shrinkageTheorem1PaperTailH2ProbabilityConsumer_badEventProbability_of_unionBoundProbabilityProviders, shrinkageTheorem1PaperTailH2ProbabilityConsumer_badEventProbability_of_lowerEventProvider_and_resolventProbabilityProvider, shrinkageTheorem1PaperTailH2ProbabilityConsumer_badEventProbability_of_lowerEventProvider_and_resolventPaperRHSBounds, ShrinkageTheorem1PaperTailWithH2ResolventProbabilityStatement, shrinkageTheorem1PaperTailWithH2ResolventProbabilityStatement_of_provider, paperH2ResolventBadEventProbabilityProvider_of_statement, ShrinkageTheorem1PaperTailWithH2ConsumerStatement, shrinkageTheorem1PaperTailWithH2ConsumerStatement_of_unionBoundProbabilityProviders, shrinkageTheorem1PaperTailWithH2ConsumerStatement_of_lowerEventProvider_and_resolventProbabilityProvider, shrinkageTheorem1PaperTailWithH2ConsumerStatement_of_lowerEventProvider_and_resolventPaperRHSBounds, shrinkageTheorem1PaperTailWithH2ConsumerStatement_of_lowerEventProvider_and_resolventProbabilityProvider_fromH1, shrinkageTheorem1PaperTailWithH2ConsumerStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1, shrinkageTheorem1PaperTailWithH2ConsumerStatement_of_resolventProbabilityStatement_and_lowerEventProvider, ShrinkageTheorem1ProofReadinessObligations, shrinkageTheorem1ProofReadinessObligations_of_lowerEventProvider, shrinkageTheorem1PaperTailWithH2ConsumerStatement_of_proofReadinessObligations, ShrinkageTheorem1PaperRHSProofReadinessObligations, shrinkageTheorem1PaperRHSProofReadinessObligations_of_lowerEventProvider, shrinkageTheorem1PaperTailWithH2ConsumerStatement_of_paperRHSProofReadinessObligations, shrinkageTheorem1PaperTailH2ProbabilityConsumer_of_paperRHSProofReadinessObligations, shrinkageTheorem1PaperTailH2ProbabilityConsumer_badEventProbability_of_paperRHSProofReadinessObligations, shrinkageTheorem1TailStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1_and_finalEventSubsetStatement, shrinkageTheorem1TailWithMeasurabilityStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1_and_finalEventSubsetStatement, shrinkageTheorem1TailWithMeasurabilityStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1_and_finalEventSubsetStatement_error_measurable, ShrinkageTheorem1PaperRHSFinalBridgeObligations, shrinkageTheorem1PaperRHSFinalBridgeObligations_paper_rhs_readiness, shrinkageTheorem1PaperRHSFinalBridgeObligations_final_tail_bound, shrinkageTheorem1TailStatement_of_paperRHSFinalBridgeObligations, ShrinkageTheorem1FinalTailMeasurabilityProvider, shrinkageTheorem1FinalTailMeasurabilityProvider_final_tail_event_measurable, shrinkageTheorem1TailEvent_measurable_of_provider, shrinkageTheorem1FinalTailMeasurabilityProvider_of_measurable, shrinkageTheorem1TailEvent_measurable_of_error_measurable, and shrinkageTheorem1FinalTailMeasurabilityProvider_of_error_measurable, ShrinkageTheorem1TailWithMeasurabilityStatement, shrinkageTheorem1TailWithMeasurabilityStatement_of_tailStatement_and_finalMeasurability, shrinkageTheorem1TailWithMeasurabilityStatement_of_tailStatement_and_error_measurable, shrinkageTheorem1TailWithMeasurability_tailStatement, shrinkageTheorem1TailWithMeasurability_finalTailMeasurabilityProvider, shrinkageTheorem1TailWithMeasurability_finalTailEvent_measurable, shrinkageTheorem1TailWithMeasurability_tail_bound, shrinkageTheorem1TailWithMeasurability_providers, shrinkageTheorem1TailWithMeasurability_h1_provider, shrinkageTheorem1TailWithMeasurability_h2_provider, shrinkageTheorem1TailWithMeasurability_lambda_positive, shrinkageTheorem1TailWithMeasurability_threshold_nonnegative, shrinkageTheorem1TailWithMeasurability_tail_rhs_nonnegative, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSFinalBridgeObligations, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSFinalBridgeObligations_error_measurable, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_eventSubset, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_eventSubset_error_measurable, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_finalEventSubsetStatement, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_finalEventSubsetStatement_error_measurable, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_finalEventSubsetComparisonProvider, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_finalEventSubsetComparisonProvider_error_measurable, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_randomPaperErrors, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_randomPaperErrors_error_measurable, shrinkageTheorem1TailWithMeasurabilityStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1_and_randomPaperErrors, shrinkageTheorem1TailWithMeasurabilityStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1_and_randomPaperErrors_error_measurable, shrinkageTheorem1TailWithMeasurabilityStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1_and_paperTheorem1DeltaBiasComponents, shrinkageTheorem1TailWithMeasurabilityStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1_and_paperTheorem1DeltaBiasComponents_error_measurable, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_randomPaperErrors_biasStatement, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_randomPaperErrors_biasStatement_error_measurable, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_addPaperBiasUpperBounds, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_addPaperBiasUpperBounds_error_measurable, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_paperTheorem1VariancePlusExponentialBiasComponent, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_paperTheorem1VariancePlusExponentialBiasComponent_error_measurable, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_paperTheorem1DeltaBiasComponent, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_paperTheorem1DeltaBiasComponent_error_measurable, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_paperTheorem1DeltaBiasComponents, shrinkageTheorem1TailWithMeasurabilityStatement_of_paperRHSProofReadinessObligations_and_paperTheorem1DeltaBiasComponents_error_measurable, ShrinkageTheorem1FinalEventSubsetStatement, ShrinkageTheorem1FinalEventSubsetComparisonProvider, shrinkageTheorem1FinalEventSubsetComparisonProvider_true_error_eq, shrinkageTheorem1FinalEventSubsetComparisonProvider_estimated_error_eq, shrinkageTheorem1FinalEventSubsetComparisonProvider_paper_bias_le_final_bias, ShrinkageTheorem1FinalBiasDominanceStatement, ShrinkageTheorem1FinalBiasDominanceProvider, shrinkageTheorem1FinalBiasDominanceStatement_of_provider, shrinkageTheorem1FinalBiasDominance_bound_of_provider, shrinkageTheorem1FinalBiasDominanceProvider_of_statement, shrinkageTheorem1FinalBiasDominanceStatement_mono, shrinkageTheorem1FinalBiasDominanceProvider_mono, constantPaperShrinkageBias, paperTheorem1VarianceBiasComponent, paperTheorem1VariancePaperBias, paperTheorem1VarianceBiasComponent_nonnegative, paperTheorem1ExponentialBiasComponent, paperTheorem1ExponentialPaperBias, paperTheorem1ExponentialBiasComponent_nonnegative, paperTheorem1DeterministicEquivalentBiasComponent, paperTheorem1DeterministicEquivalentPaperBias, paperTheorem1DeterministicEquivalentBiasComponent_nonnegative, paperTheorem1DeltaBiasComponent, paperTheorem1DeltaPaperBias, paperTheorem1VariancePlusExponentialBiasComponent, paperTheorem1VariancePlusExponentialPaperBias, paperShrinkageBiasTerm_constant, paperShrinkageBiasTerm_paperTheorem1VariancePaperBias, paperShrinkageBiasTerm_paperTheorem1ExponentialPaperBias, paperShrinkageBiasTerm_paperTheorem1DeterministicEquivalentPaperBias, paperShrinkageBiasTerm_paperTheorem1DeltaPaperBias, paperShrinkageBiasTerm_paperTheorem1VariancePlusExponentialPaperBias, randomPaperShrinkageBiasTerm_constant, randomPaperShrinkageBiasTerm_paperTheorem1VariancePaperBias, randomPaperShrinkageBiasTerm_paperTheorem1ExponentialPaperBias, randomPaperShrinkageBiasTerm_paperTheorem1DeterministicEquivalentPaperBias, randomPaperShrinkageBiasTerm_paperTheorem1DeltaPaperBias, randomPaperShrinkageBiasTerm_paperTheorem1VariancePlusExponentialPaperBias, addPaperShrinkageBias, paperShrinkageBiasTerm_add, randomPaperShrinkageBiasTerm_add, paperTheorem1VarianceBiasControlProvider, paperTheorem1ExponentialBiasControlProvider, paperTheorem1DeterministicEquivalentBiasControlProvider, paperTheorem1DeltaBiasControlProvider, paperTheorem1VariancePlusExponentialBiasControlProvider, paperShrinkageBiasControlProvider_of_uniformNonneg, paperShrinkageBiasControlProvider_of_constantPaperBias, paperShrinkageBiasControlProvider_of_addPaperBias, PaperShrinkageBiasUpperBoundStatement, PaperShrinkageBiasUpperBoundProvider, paperShrinkageBiasUpperBoundStatement_of_provider, paperShrinkageBiasUpperBound_of_provider, paperShrinkageBiasUpperBoundProvider_of_statement, paperShrinkageBiasUpperBoundStatement_of_constantPaperBias, paperShrinkageBiasUpperBoundProvider_of_constantPaperBias, paperShrinkageBiasUpperBoundStatement_of_paperTheorem1VarianceBiasComponent, paperShrinkageBiasUpperBoundProvider_of_paperTheorem1VarianceBiasComponent, paperShrinkageBiasUpperBoundStatement_of_paperTheorem1ExponentialBiasComponent, paperShrinkageBiasUpperBoundProvider_of_paperTheorem1ExponentialBiasComponent, paperShrinkageBiasUpperBoundStatement_of_paperTheorem1DeterministicEquivalentBiasComponent, paperShrinkageBiasUpperBoundProvider_of_paperTheorem1DeterministicEquivalentBiasComponent, paperShrinkageBiasUpperBoundStatement_of_paperTheorem1DeltaBiasComponent, paperShrinkageBiasUpperBoundProvider_of_paperTheorem1DeltaBiasComponent, paperShrinkageBiasUpperBoundStatement_of_paperTheorem1DeltaBiasComponents, paperShrinkageBiasUpperBoundProvider_of_paperTheorem1DeltaBiasComponents, paperShrinkageBiasUpperBoundStatement_of_paperTheorem1VariancePlusExponentialBiasComponent, paperShrinkageBiasUpperBoundProvider_of_paperTheorem1VariancePlusExponentialBiasComponent, paperShrinkageBiasUpperBoundStatement_mono, paperShrinkageBiasUpperBoundProvider_mono, paperShrinkageBiasUpperBoundStatement_le_max_left, paperShrinkageBiasUpperBoundStatement_le_max_right, paperShrinkageBiasUpperBoundProvider_le_max_left, paperShrinkageBiasUpperBoundProvider_le_max_right, paperShrinkageBiasUpperBoundStatement_of_addPaperBias, paperShrinkageBiasUpperBoundProvider_of_addPaperBias, paperShrinkageBiasUpperBoundStatement_of_uniformBound, paperShrinkageBiasUpperBoundProvider_of_uniformBound, shrinkageTheorem1FinalBiasDominanceStatement_of_constantPaperBias, shrinkageTheorem1FinalBiasDominanceProvider_of_constantPaperBias, shrinkageTheorem1FinalBiasDominanceStatement_of_biasUpperBoundProvider, shrinkageTheorem1FinalBiasDominanceProvider_of_biasUpperBoundProvider, shrinkageTheorem1FinalBiasDominanceStatement_of_addPaperBiasUpperBounds, shrinkageTheorem1FinalBiasDominanceProvider_of_addPaperBiasUpperBounds, shrinkageTheorem1FinalBiasDominanceStatement_of_paperTheorem1VariancePlusExponentialBiasComponent, shrinkageTheorem1FinalBiasDominanceProvider_of_paperTheorem1VariancePlusExponentialBiasComponent, shrinkageTheorem1FinalBiasDominanceStatement_of_paperTheorem1DeltaBiasComponent, shrinkageTheorem1FinalBiasDominanceProvider_of_paperTheorem1DeltaBiasComponent, shrinkageTheorem1FinalBiasDominanceStatement_of_paperTheorem1DeltaBiasComponents, shrinkageTheorem1FinalBiasDominanceProvider_of_paperTheorem1DeltaBiasComponents, shrinkageTheorem1FinalBiasDominanceStatement_of_uniformPaperBiasBound, shrinkageTheorem1FinalBiasDominanceProvider_of_uniformPaperBiasBound, shrinkageTheorem1FinalEventSubsetStatement_of_comparisonProvider, shrinkageTheorem1FinalEventSubsetComparisonProvider_of_randomPaperErrors, shrinkageTheorem1FinalEventSubsetStatement_of_randomPaperErrors, shrinkageTheorem1FinalEventSubsetComparisonProvider_of_addPaperBiasUpperBounds, shrinkageTheorem1FinalEventSubsetStatement_of_addPaperBiasUpperBounds, shrinkageTheorem1FinalEventSubsetComparisonProvider_of_paperTheorem1DeltaBiasComponents, shrinkageTheorem1FinalEventSubsetStatement_of_paperTheorem1DeltaBiasComponents, shrinkageTheorem1TailBound_of_eventSubset_paperTailBound, shrinkageTheorem1TailBound_of_finalEventSubsetStatement, shrinkageTheorem1PaperRHSFinalBridgeObligations_of_eventSubset, shrinkageTheorem1PaperRHSFinalBridgeObligations_of_finalEventSubsetStatement, shrinkageTheorem1TailStatement_of_paperRHSProofReadinessObligations_and_eventSubset, shrinkageTheorem1TailStatement_of_paperRHSProofReadinessObligations_and_finalEventSubsetStatement, shrinkageTheorem1TailStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1_and_finalEventSubsetStatement, shrinkageTheorem1TailWithMeasurabilityStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1_and_finalEventSubsetStatement, shrinkageTheorem1TailWithMeasurabilityStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1_and_finalEventSubsetStatement_error_measurable, shrinkageTheorem1TailStatement_of_paperRHSProofReadinessObligations_and_finalEventSubsetComparisonProvider, shrinkageTheorem1TailStatement_of_paperRHSProofReadinessObligations_and_randomPaperErrors, shrinkageTheorem1TailStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1_and_randomPaperErrors, shrinkageTheorem1TailWithMeasurabilityStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1_and_randomPaperErrors, shrinkageTheorem1TailWithMeasurabilityStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1_and_randomPaperErrors_error_measurable, shrinkageTheorem1TailStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1_and_paperTheorem1DeltaBiasComponents, shrinkageTheorem1TailWithMeasurabilityStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1_and_paperTheorem1DeltaBiasComponents, shrinkageTheorem1TailWithMeasurabilityStatement_of_lowerEventProvider_and_resolventPaperRHSBounds_fromH1_and_paperTheorem1DeltaBiasComponents_error_measurable, shrinkageTheorem1TailStatement_of_paperRHSProofReadinessObligations_and_addPaperBiasUpperBounds, shrinkageTheorem1TailStatement_of_paperRHSProofReadinessObligations_and_paperTheorem1VariancePlusExponentialBiasComponent, shrinkageTheorem1TailStatement_of_paperRHSProofReadinessObligations_and_paperTheorem1DeltaBiasComponent, shrinkageTheorem1TailStatement_of_paperRHSProofReadinessObligations_and_paperTheorem1DeltaBiasComponents, shrinkageTheorem1PaperTailEvent_subset_left_of_addPaperBias_nonneg, shrinkageTheorem1PaperTailProviders_of_addPaperBias_left, shrinkageTheorem1PaperTailBound_of_addPaperBias_left, shrinkageTheorem1PaperRHSProofReadinessObligations_of_addPaperBias_left, shrinkageTheorem1PaperTailEvent_subset_right_of_addPaperBias_nonneg, shrinkageTheorem1PaperTailProviders_of_addPaperBias_right, shrinkageTheorem1PaperTailBound_of_addPaperBias_right, shrinkageTheorem1PaperRHSProofReadinessObligations_of_addPaperBias_right, shrinkageTheorem1PaperRHSProofReadinessObligations_of_paperTheorem1DeltaBias_left, shrinkageTheorem1PaperRHSProofReadinessObligations_of_paperTheorem1DeltaBias_right, shrinkageTheorem1PaperTailEvent_measurable_of_provider, shrinkageTheorem1PaperTailMeasurabilityProvider_of_measurable, paperTheorem1DeltaPaperTailEvent_measurable_of_provider, and paperTheorem1DeltaPaperTailMeasurabilityProvider_of_measurable, shrinkageTheorem1PaperTailMeasurabilityProvider_of_providers, shrinkageTheorem1PaperTailEvent_measurable_of_providers, paperTheorem1DeltaPaperTailMeasurabilityProvider_of_providers, and paperTheorem1DeltaPaperTailEvent_measurable_of_providers, shrinkageTheorem1TailStatement_of_paperRHSProofReadinessObligations_and_randomPaperErrors_biasStatement, paperH2ResolventGoodEventMeasurabilityProvider_resolvent_good_event_measurable, paperH2ResolventGoodEvent_measurable_of_provider, paperH2ResolventBadEventMeasurabilityProvider_resolvent_bad_event_measurable, paperH2ResolventBadEvent_measurable_of_provider, paperH2ResolventBadEventMeasurabilityProvider_of_goodEventProvider, paperH2LeaveOneOutGoodEventMeasurabilityProvider_good_event_measurable, paperH2LeaveOneOutGoodEvent_measurable_of_provider, paperH2LeaveOneOutBadEventMeasurabilityProvider_bad_event_measurable, paperH2LeaveOneOutGoodEvent_measurable_of_factor_providers, paperH2LeaveOneOutGoodEventMeasurabilityProvider_of_factor_providers, and paperH2LeaveOneOutBadEventMeasurabilityProvider_of_goodEventProvider, plus the direct factor-to-bad-event provider bridge paperH2LeaveOneOutBadEventMeasurabilityProvider_of_factor_providers. The same API file covers the resolvent atomic-event vocabulary and primitive-measurability finite intersection layer: paperH2ShrinkageShiftedDetUnitEvent, paperH2LeaveOneOutShiftedDetUnitEvent, paperH2WoodburyDenominatorNonzeroEvent, paperH2ResolventGoodEvent_mem_iff_atomic_events, paperH2ShrinkageShiftedDetBadEvent, paperH2LeaveOneOutShiftedDetBadEvent, paperH2WoodburyDenominatorBadEvent, paperH2ShrinkageShiftedDetBadEvent_eq_compl, paperH2LeaveOneOutShiftedDetBadEvent_eq_compl, paperH2WoodburyDenominatorBadEvent_eq_compl, paperH2ResolventAtomicBadUnionEvent, paperH2ResolventBadEvent_mem_imp_atomic_bad, paperH2ResolventBadEvent_subset_atomicBadUnion, PaperH2ShrinkageShiftedDetTailEstimateStatement, PaperH2ShrinkageShiftedDetTailEstimateProvider, paperH2ShrinkageShiftedDetTailEstimateStatement_of_provider, paperH2ShrinkageShiftedDetTailEstimateProvider_of_statement, paperH2ShrinkageShiftedDetTailEstimate_bound_of_provider, paperH2ShrinkageShiftedDetTailEstimate_rhs_nonnegative_of_provider, paperH2ShrinkageShiftedDetTailEstimateStatement_of_bound, paperH2ShrinkageShiftedDetTailEstimateProvider_of_bound, PaperH2ShrinkageShiftedDetTailPaperParameters, paperH2ShrinkageShiftedDetTailPaperRHS, paperH2ShrinkageShiftedDetTailPaperRHS_nonnegative, paperH2ShrinkageShiftedDetTailEstimateStatement_of_paperRHS_bound, paperH2ShrinkageShiftedDetTailEstimateProvider_of_paperRHS_bound, PaperH2LeaveOneOutShiftedDetPointTailEstimateStatement, PaperH2LeaveOneOutShiftedDetPointTailEstimateProvider, paperH2LeaveOneOutShiftedDetPointTailEstimateStatement_of_provider, paperH2LeaveOneOutShiftedDetPointTailEstimateProvider_of_statement, paperH2LeaveOneOutShiftedDetPointTailEstimate_bound_of_provider, paperH2LeaveOneOutShiftedDetPointTailEstimate_rhs_nonnegative_of_provider, paperH2LeaveOneOutShiftedDetPointTailEstimateStatement_of_bound, paperH2LeaveOneOutShiftedDetPointTailEstimateProvider_of_bound, PaperH2LeaveOneOutShiftedDetPointTailPaperParameters, paperH2LeaveOneOutShiftedDetPointTailPaperRHS, paperH2LeaveOneOutShiftedDetPointTailPaperRHS_nonnegative, paperH2LeaveOneOutShiftedDetPointTailEstimateStatement_of_paperRHS_bound, paperH2LeaveOneOutShiftedDetPointTailEstimateProvider_of_paperRHS_bound, paperH2ShiftedDetBadEventProbabilityStatement_of_tailEstimateProviders, paperH2ShiftedDetBadEventProbabilityProvider_of_tailEstimateProviders, paperH2ShiftedDetBadEventProbabilityStatement_of_paperRHS_bounds, paperH2ShiftedDetBadEventProbabilityProvider_of_paperRHS_bounds, PaperH2ShiftedDetBadEventProbabilityStatement, PaperH2ShiftedDetBadEventProbabilityProvider, paperH2ShiftedDetBadEventProbabilityProvider_shifted_det_bad_event_probability, paperH2ShiftedDetBadEventProbabilityStatement_of_provider, paperH2ShiftedDetBadEventProbabilityProvider_of_statement, paperH2ShrinkageShiftedDetBadEventProbability_bound_of_provider, paperH2LeaveOneOutShiftedDetBadEventProbability_bound_of_provider, paperH2ResolventAtomicBadEventProbabilityProvider_of_shiftedDetProvider_and_denominatorBounds, paperH2ResolventAtomicBadEventProbabilityProvider_of_paperRHS_bounds, PaperH2WoodburyDenominatorPointTailEstimateStatement, PaperH2WoodburyDenominatorPointTailEstimateProvider, paperH2WoodburyDenominatorPointTailEstimateStatement_of_provider, paperH2WoodburyDenominatorPointTailEstimateProvider_of_statement, paperH2WoodburyDenominatorPointTailEstimate_bound_of_provider, paperH2WoodburyDenominatorPointTailEstimate_rhs_nonnegative_of_provider, paperH2WoodburyDenominatorPointTailEstimateStatement_of_bound, paperH2WoodburyDenominatorPointTailEstimateProvider_of_bound, PaperH2WoodburyDenominatorPointTailPaperParameters, paperH2WoodburyDenominatorPointTailPaperRHS, paperH2WoodburyDenominatorPointTailPaperRHS_nonnegative, paperH2WoodburyDenominatorPointTailEstimateStatement_of_paperRHS_bound, paperH2WoodburyDenominatorPointTailEstimateProvider_of_paperRHS_bound, paperH2WoodburyDenominatorBadEventProbabilityStatement_of_pointTailEstimateProviders, paperH2WoodburyDenominatorBadEventProbabilityProvider_of_pointTailEstimateProviders, PaperH2WoodburyDenominatorBadEventProbabilityStatement, PaperH2WoodburyDenominatorBadEventProbabilityProvider, paperH2WoodburyDenominatorBadEventProbabilityProvider_woodbury_denominator_bad_event_probability, paperH2WoodburyDenominatorBadEventProbabilityStatement_of_provider, paperH2WoodburyDenominatorBadEventProbabilityProvider_of_statement, paperH2WoodburyDenominatorBadEventProbability_bound_of_provider, paperH2ResolventAtomicBadEventProbabilityProvider_of_shiftedDetProvider_and_denominatorProvider, paperH2ResolventAtomicBadEventUnionBoundRHS, paperH2ResolventAtomicBadEventUnionBoundRHS_nonnegative, PaperH2ResolventAtomicTailRHSProvider, PaperH2ResolventAtomicTailRHSProvider_shrinkage_rhs_nonnegative, PaperH2ResolventAtomicTailRHSProvider_leave_one_out_rhs_nonnegative, PaperH2ResolventAtomicTailRHSProvider_denominator_rhs_nonnegative, paperH2ResolventAtomicBadEventUnionBoundRHS_nonnegative_of_rhsProvider, PaperH2ResolventAtomicPointTailEstimateProviders, paperH2ResolventAtomicTailRHSProvider_of_pointTailEstimateProviders, paperH2ResolventAtomicBadEventProbabilityProvider_of_pointTailEstimateProviders, PaperH2ResolventAtomicBadEventProbabilityProvider, PaperH2ResolventAtomicBadEventProbabilityProvider_shrinkage_rhs_nonnegative, PaperH2ResolventAtomicBadEventProbabilityProvider_leave_one_out_rhs_nonnegative, PaperH2ResolventAtomicBadEventProbabilityProvider_denominator_rhs_nonnegative, PaperH2ResolventAtomicBadEventProbabilityProvider_shrinkage_bad_event_probability, PaperH2ResolventAtomicBadEventProbabilityProvider_leave_one_out_bad_event_probability, PaperH2ResolventAtomicBadEventProbabilityProvider_denominator_bad_event_probability, PaperH2ResolventAtomicBadEventUnionBoundStatement, PaperH2ResolventAtomicBadEventUnionBoundStatement_atomic_bad_event_probability, PaperH2ResolventAtomicBadEventUnionBoundStatement_atomic_bad_union_probability, PaperH2ResolventAtomicBadEventUnionBoundStatement_resolvent_bad_event_probability, paperH2ResolventAtomicBadUnionEventProbability_bound_of_atomicProvider, paperH2ResolventAtomicBadEventUnionBoundStatement_of_atomicProvider, paperH2ResolventAtomicBadEventUnionBound_bound_of_atomicProvider, paperH2ResolventBadEventProbabilityProvider_of_atomicProvider, paperH2ResolventBadEventProbabilityProvider_of_paperRHS_bounds, PaperH2ResolventGoodEventPrimitiveMeasurabilityStatement, paperH2ResolventGoodEventPrimitiveMeasurability, paperH2ResolventGoodEvent_measurable_of_atomic_events, paperH2ResolventGoodEventMeasurabilityProvider_of_atomic_events, PaperH2ResolventAtomicMeasurabilityProvider, paperH2ResolventAtomicMeasurabilityProvider_shrinkage_shifted_det_unit_measurable, paperH2ResolventAtomicMeasurabilityProvider_leave_one_out_shifted_det_unit_measurable, paperH2ResolventAtomicMeasurabilityProvider_woodbury_denominator_nonzero_measurable, paperH2ResolventGoodEvent_measurable_of_atomic_provider, paperH2ResolventGoodEventMeasurabilityProvider_of_atomic_provider, paperH2ResolventBadEvent_measurable_of_atomic_provider, paperH2ResolventBadEventMeasurabilityProvider_of_atomic_provider, paperH2ShrinkageShiftedDetUnitEvent_measurable_of_det_measurable, paperH2LeaveOneOutShiftedDetUnitEvent_measurable_of_det_measurable, paperH2WoodburyDenominatorNonzeroEvent_measurable_of_denominator_measurable, paperH2ResolventAtomicMeasurabilityProvider_of_denominator_measurable, paperH2ResolventAtomicMeasurabilityProvider_of_det_and_denominator_measurable, squareMatrix_det_measurable_of_entry_measurable, paperH2ResolventAtomicMeasurabilityProvider_of_shifted_entry_and_denominator_measurable, shrinkageShiftedMatrix_entry_measurable_of_data_entry_measurable, leaveOneOutShiftedMatrix_entry_measurable_of_data_entry_measurable, paperH2ResolventAtomicMeasurabilityProvider_of_data_entry_and_denominator_measurable, shrinkageLeaveOneOutWoodburyDenominator_measurable_of_resolvent_entry_measurable, paperH2ResolventAtomicMeasurabilityProvider_of_data_entry_and_resolvent_entry_measurable, PaperH2ResolventGoodEventPrimitiveMeasurabilityProvider, paperH2ResolventGoodEventPrimitiveMeasurabilityStatement_of_provider, paperH2ResolventGoodEventPrimitiveMeasurabilityProvider_primitive_measurability, and paperH2ResolventGoodEvent_measurable_of_primitive_provider. H1-to-resolvent measurability convenience checks include paperH2ResolventGoodEventMeasurabilityProvider_of_h1_provider and paperH2ResolventBadEventMeasurabilityProvider_of_h1_provider. The paper-tail measurability provider direct field projection shrinkageTheorem1PaperTailMeasurabilityProvider_tail_event_measurable is checked alongside the existing _measurable_of_provider wrapper. These checks assert the finite-intersection consumer, atomic-provider unpacking, scalar determinant-unit and Woodbury nonzero-event bridges, determinant measurability from shifted entries, shifted-entry measurability from random-data entries, Woodbury denominator finite-algebra measurability from resolvent-entry measurability, total inverse/resolvent-entry measurability from matrix entries, eta-only lower good/bad complement measurability bridges, H1 observed-data measurability projection into the H2 atomic provider, H1 plus explicit lower-singular-value good- or bad-event measurability provider packaging for H2 good/bad events, final tail-event measurability packaging from explicit MeasurableSet or measurable true/estimated error functions, the bundled final-tail statement plus final-tail measurability consumer, paper-RHS proof-readiness consumers for that bundled final-tail/measurability surface, including the pointwise comparison-provider, random-paper-error, statement-shaped final-bias-dominance, additive paper-bias upper-bound, variance-plus-exponential, and one-shot/componentwise Delta_X(lambda) routes, final-event pointwise comparison packaging, random-paper-error specialization with only typed bias dominance remaining, bias-dominance provider projection/constructor, scalar-monotonicity wrappers, deterministic bias-control constructors, constant, variance-component, exponential-component, and variance-plus-exponential partial-envelope paper-bias scalar-upper-bound / final-bias wrappers, and general scalar upper-bound statement/provider roundtrip wrappers, including constant and uniform deterministic paper-bias upper-bound wrappers plus monotonicity / max weakening wrappers, additive paper-bias composition/final-dominance/final-event/tail-statement wrappers, additive-left/right paper-tail readiness reuse via deterministic event inclusion plus measure_mono, full-Delta left/right proof-readiness specializations from DeterministicEquivalent plus VariancePlusExponential, direct three-component full-Delta final-bias/final-event subset wrappers and the direct three-component full-Delta tail-statement consumer, plus type-level measurability packaging only; they do not assert primitive H1 construction, lower-singular-value measurability/probability, H2 probability, concentration, or Theorem 1 behavior. Focused commands: lake build HighDimProb.Applications.PrecisionDA, lake build HighDimProbTest.PrecisionDAAPI, and lake build HighDimProbJudge.PrecisionDA.CovarianceTraceExpansionUse.
  • RandomMatrix API tests: variance proxy, spectral, trace-exp, hardbone statement targets, thin consumers, rank/support trace bridge, excess-support trace bridge, centered-square expectation expansion, PSD Loewner variance-proxy norm monotonicity, MatrixExpSupportDomination, MatrixExpExcessSupportDomination, trace-exp eigenvalue-sum bridge, effective-rank consumer, ambient trace certificate, ambient effective-rank wrapper, star-projection trace/rank/PSD certificate and rank consumer, Laplace, concentration, and example API checks.
  • RandomMatrix bookkeeping checks: trace-exp endpoint wrappers and the natural-state TraceExp route are covered in HighDimProbTest/RandomMatrixTraceExpAPI.lean and HighDimProbJudge/RandomMatrix/TraceExpUse.lean; example modules, including the StatementRoutes statement-route index, are covered through lake build HighDimProb.Examples.
  • RandomMatrix hardbone statement-target checks, including the proved Bernstein CFC hardbone leaf, the proved matrix-exp/log normalization and log-domain leaves, the proved matrix log/order bridge leaf, the proved excess-support trace bridge leaf, the proved centered-square expectation bridge leaf, the progress-first conditional finite-family trace-MGF assumption-composition consumer, and the S10 tail/conditioning assumption bundle wrapper are covered in HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean, HighDimProbTest/RandomMatrixConcentrationAPI.lean, HighDimProbJudge/RandomMatrix/TraceExpUse.lean, and HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean.
  • RandomMatrix sample-covariance negative-side provider-transfer adapters, the compact SampleCovarianceTailTarget / SampleCovarianceBoundedRowTroppAssumptions route, bridge-layer exact-row centered-square wrappers/bundles, and CFC-free sample-covariance wrappers, including the positive-side exact-row variance-proxy quadratic-form wrapper, are covered in HighDimProbTest/RandomMatrixConcentrationAPI.lean, HighDimProbTest/ExamplesAPI.lean, and HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean.
  • RandomMatrix CFC-free Matrix Bernstein assumption bundles and preferred *_of_troppAssumptions wrappers are covered in HighDimProbTest/RandomMatrixConcentrationAPI.lean, HighDimProbTest/ExamplesAPI.lean, and HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean.
  • Variance-proxy and hardbone API coverage includes the centered second-moment comparison, rank-one second-moment consumer, exact row second-moment hardbone consumer, deterministic variance-proxy norm subadditivity, exact rank-one second-moment norm providers, the rank-one square-integrability four-product, MemLp 4, bounded-row, centered-family providers, and the row-specific exact-row sample-covariance hardbone consumer in RandomMatrixVarianceProxyAPI, RandomMatrixHardboneStatementsAPI, and the corresponding judge/example surfaces.
  • Judge tests: HighDimProbJudge plus scripts/judge_policy_check.py.

Policy Checks

The policy script rejects non-comment sorry, admit, axiom, and unsafe, forbids stable-root imports of HighDimProb.Experimental, checks judge import boundaries, and rejects anonymous negated-family signatures in public RandomMatrix, example, test, and judge files.

Maintenance Rule

Keep this file short. Add new details only when they change what contributors must run or what CI enforces. Archive old stage-by-stage test history in archive.md.

Provider-focused RandomMatrix Check

Run this after changing the provider-facing Lieb/Tropp layer, including the ambient or self-adjoint carrier matrix-exp derivative surface, the first-order CFC.log affine-line provider layer, the derivative-level Epstein consumer layer, the natural-history provider alias layer, or the provider-compressed natural-state tail route:

lake build HighDimProb.RandomMatrix.MatrixExpDerivativeProvider HighDimProb.RandomMatrix.CFCLogDerivativeProvider HighDimProb.RandomMatrix.EpsteinDerivativeProvider HighDimProb.RandomMatrix.LiebProvider HighDimProbTest.RandomMatrixMatrixExpDerivativeProviderAPI HighDimProbTest.RandomMatrixLiebProviderAPI HighDimProbJudge.RandomMatrix.LiebProviderUse
  • HighDimProbTest/PrecisionDAAPI.lean checks the minimal Theorem 1 provider bundle projections shrinkageTheorem1Providers_h1 and shrinkageTheorem1Providers_h2.
  • HighDimProbTest/PrecisionDAAPI.lean checks the base final-tail projection surface: shrinkageTheorem1TailStatement_providers, shrinkageTheorem1TailStatement_h1_provider, shrinkageTheorem1TailStatement_h2_provider, shrinkageTheorem1TailStatement_lambda_positive, shrinkageTheorem1TailStatement_threshold_nonnegative, shrinkageTheorem1TailStatement_tail_rhs_nonnegative, and shrinkageTheorem1TailStatement_tail_bound.
  • The same API file checks the paper-tail provider-bundle field projections shrinkageTheorem1PaperTailProviders_core, shrinkageTheorem1PaperTailProviders_rhs, shrinkageTheorem1PaperTailProviders_bias_control, and shrinkageTheorem1PaperTailProviders_measurability.
  • The same API file checks the nested paper-tail RHS provider projections shrinkageTheorem1PaperTailRHSProvider_rhs_identifies_tail and shrinkageTheorem1PaperTailRHSProvider_rhs_nonnegative.
  • The same API file checks the matching paper-tail statement projection surface: shrinkageTheorem1PaperTailStatement_providers, shrinkageTheorem1PaperTailStatement_h1_provider, shrinkageTheorem1PaperTailStatement_h2_provider, shrinkageTheorem1PaperTailStatement_lambda_positive, shrinkageTheorem1PaperTailStatement_threshold_nonnegative, shrinkageTheorem1PaperTailStatement_tail_rhs_nonnegative, and shrinkageTheorem1PaperTailStatement_tail_bound.
  • It also checks direct theorem-facing H2 wrapper projections: shrinkageTheorem1PaperTailWithH2ConsumerStatement_paper_tail, shrinkageTheorem1PaperTailWithH2ConsumerStatement_h2_consumer, shrinkageTheorem1PaperTailWithH2ResolventProbabilityStatement_paper_tail, and shrinkageTheorem1PaperTailWithH2ResolventProbabilityStatement_h2_resolvent_probability.
  • It checks the top-level ShrinkageTheorem1ProofReadinessObligations field projection API: shrinkageTheorem1ProofReadinessObligations_providers, shrinkageTheorem1ProofReadinessObligations_lambda_positive, shrinkageTheorem1ProofReadinessObligations_threshold_nonnegative, shrinkageTheorem1ProofReadinessObligations_paper_tail_bound, shrinkageTheorem1ProofReadinessObligations_h2_bad_event_measurability, shrinkageTheorem1ProofReadinessObligations_lower_rhs_nonnegative, shrinkageTheorem1ProofReadinessObligations_h2_union_rhs, shrinkageTheorem1ProofReadinessObligations_lower_singular_value_event, and shrinkageTheorem1ProofReadinessObligations_resolvent_bad_event_probability.
  • It checks the paper-RHS ShrinkageTheorem1PaperRHSProofReadinessObligations field projection API, from providers and side conditions through the three paper-RHS component-tail bound families: shrinkageTheorem1PaperRHSProofReadinessObligations_providers, shrinkageTheorem1PaperRHSProofReadinessObligations_lambda_positive, shrinkageTheorem1PaperRHSProofReadinessObligations_threshold_nonnegative, shrinkageTheorem1PaperRHSProofReadinessObligations_paper_tail_bound, shrinkageTheorem1PaperRHSProofReadinessObligations_h2_bad_event_measurability, shrinkageTheorem1PaperRHSProofReadinessObligations_lower_rhs_nonnegative, shrinkageTheorem1PaperRHSProofReadinessObligations_lower_singular_value_event, shrinkageTheorem1PaperRHSProofReadinessObligations_shrinkage_shifted_det_prefactor_nonnegative, shrinkageTheorem1PaperRHSProofReadinessObligations_leave_one_out_shifted_det_prefactor_nonnegative, shrinkageTheorem1PaperRHSProofReadinessObligations_woodbury_denominator_prefactor_nonnegative, shrinkageTheorem1PaperRHSProofReadinessObligations_shrinkage_shifted_det_tail_bound, shrinkageTheorem1PaperRHSProofReadinessObligations_leave_one_out_shifted_det_point_tail_bounds, and shrinkageTheorem1PaperRHSProofReadinessObligations_woodbury_denominator_point_tail_bounds.