# Theorem Map This document maps the checked Lean theorem surface. It is deliberately narrow: the formalization proves finite Bayes decision theorems, a quotient-form optimality theorem, a canonical overlap-tilt signal instantiation, a group-theoretic bitmap-overlap invariant theorem, a supplied calibrated-evidence wrapper, a finite quotient-search layer, a generic quotient-constraint layer, reachable-image/kernel/fiber layers, a finite product-quotient layer for pairwise and ranking targets, a finite observation-window layer for target-separating probe families, score-margin profile-stability layers, and an exact constant-weight bitmap null. ## Main Claim For `K`-active bitmaps in dimension `D`, under the canonical finite overlap-tilt signal model with uniform bitmap null and signal parameter `0 < theta`, a literal overlap-tail rule is Bayes-optimal among all deterministic admission rules on the constant-weight bitmap observation space. The same threshold event has exactly the hypergeometric upper-tail probability under the model null. Checked theorem: ```lean OrdvecFormalization.exists_uniformBitmapOverlapTail_finiteBayesRisk_le_and_hypergeomTail ``` Cost-sensitive checked theorem: ```lean OrdvecFormalization.exists_uniformBitmapOverlapTail_finiteCostedBayesRisk_le_and_hypergeomTail ``` General positive-base theorem, with separate uniform-null tail calibration at the same cutoff: ```lean OrdvecFormalization.exists_constantWeightBitmapOverlapTail_finiteBayesRisk_le_and_hypergeomTail ``` ## Supporting Layers Core FNCH overlap theorem: ```lean OrdvecFormalization.overlapNull_threshold_bayesRisk_optimal_of_lt OrdvecFormalization.fnch_overlap_threshold_bayes_optimal ``` Cost-sensitive extension: ```lean OrdvecFormalization.overlapNull_costed_threshold_bayesRisk_optimal_of_lt OrdvecFormalization.fnch_overlap_costed_threshold_bayes_optimal ``` Exact constant-weight bitmap null: ```lean OrdvecFormalization.card_bitmapOverlapFiber_of_query_card OrdvecFormalization.bitmapOverlapTailMass_eq_bitmapHypergeomTail_of_query_card OrdvecFormalization.bitmapUniformPMF_overlapFiber_prob OrdvecFormalization.bitmapUniformPMF_overlapTail_prob ``` Bitmap symmetry layer: ```lean OrdvecFormalization.bitmapOverlap_queryStabilizer_eq OrdvecFormalization.exists_queryStabilizer_permuteBitmap_eq_of_card_eq_overlap_eq OrdvecFormalization.exists_queryStabilizer_permuteBitmap_eq_iff_overlap_eq_of_card_eq OrdvecFormalization.invariantOn_constantWeightBitmapSpace_factorsThrough_overlap ``` Finite quotient search layer: ```lean OrdvecFormalization.quotientPullback OrdvecFormalization.RuleFactorsThrough OrdvecFormalization.QuotientCompatible OrdvecFormalization.ObservedQuotients OrdvecFormalization.ObservedQuotientsList OrdvecFormalization.SampleConsistent OrdvecFormalization.QuotientRuleFitsSample OrdvecFormalization.FullTargetFitsSample OrdvecFormalization.CompatibleTargets OrdvecFormalization.CompatibleQuotientRules OrdvecFormalization.quotientCompatible_exists_ruleq OrdvecFormalization.quotientRule_induces_compatible_target OrdvecFormalization.induced_targets_eq_of_ruleq_eq OrdvecFormalization.induced_targets_eq_of_agree_on_range OrdvecFormalization.sampleConsistent_of_quotientCompatible OrdvecFormalization.no_compatible_target_of_sample_collision OrdvecFormalization.sampleConsistent_of_exists_quotientRuleFitsSample OrdvecFormalization.exists_quotientRuleFitsSample_of_sampleConsistent OrdvecFormalization.sampleConsistent_iff_exists_quotientRuleFitsSample OrdvecFormalization.QuotientImageFinset OrdvecFormalization.QuotientImageBucket OrdvecFormalization.card_quotientImageRules OrdvecFormalization.UnobservedReachableQuotients OrdvecFormalization.restrictRuleToImage OrdvecFormalization.imageRuleToFullTarget OrdvecFormalization.imageRuleToFullTarget_quotientCompatible OrdvecFormalization.quotientRules_agree_on_observed_of_fit OrdvecFormalization.fitting_quotient_rules_determined_on_observed OrdvecFormalization.extendWithUnobserved OrdvecFormalization.extendWithUnobserved_fits_sample OrdvecFormalization.card_fullTargets OrdvecFormalization.card_quotientRules OrdvecFormalization.quotientCompatible_search_space_bound OrdvecFormalization.card_unobserved_assignments OrdvecFormalization.card_unobserved_bool_assignments OrdvecFormalization.QuotientRefines OrdvecFormalization.RuleFactorsThrough.of_refines OrdvecFormalization.not_ruleFactorsThrough_coarse_of_not_fine OrdvecFormalization.QuotientRefines.refl OrdvecFormalization.QuotientRefines.trans OrdvecFormalization.RuleFactorsThrough.prod_iff OrdvecFormalization.SampleConsistent.prod_iff ``` Quotient constraint layer: ```lean OrdvecFormalization.FiberInvariant OrdvecFormalization.HasNontrivialFiber OrdvecFormalization.SeparatesSameFiber OrdvecFormalization.ruleFactorsThrough_fiberInvariant OrdvecFormalization.ruleFactorsThrough_same_admission_on_fibers OrdvecFormalization.ruleFactorsThrough_same_evidence_on_fibers OrdvecFormalization.finiteLikelihoodRatioFactorsThrough_fiberInvariant OrdvecFormalization.finiteBayesAdmitFactorsThrough_same_on_fibers OrdvecFormalization.fiberInvariant_ruleFactorsThrough_of_surjective OrdvecFormalization.not_ruleFactorsThrough_of_separatesSameFiber OrdvecFormalization.not_injective_of_hasNontrivialFiber OrdvecFormalization.injective_of_not_hasNontrivialFiber OrdvecFormalization.hasNontrivialFiber_iff_not_injective OrdvecFormalization.exists_boolTarget_not_ruleFactorsThrough_of_hasNontrivialFiber OrdvecFormalization.exists_pair_quotientTarget_factorsThrough_and_otherTarget_not OrdvecFormalization.boolRuleFactorsThrough_positiveSet_eq_quotientPullback ``` Quotient image, kernel, fiber topology, product/pair quotient, refinement, margin, and profile-stability layer: ```lean OrdvecFormalization.QuotientImage OrdvecFormalization.imageQuotient OrdvecFormalization.imageQuotient_surjective OrdvecFormalization.Fiber OrdvecFormalization.ImageFiber OrdvecFormalization.ObservedBuckets OrdvecFormalization.UnobservedBuckets OrdvecFormalization.FiberSize OrdvecFormalization.HasCollision OrdvecFormalization.InjectiveOnSample OrdvecFormalization.Kernel OrdvecFormalization.TargetKernel OrdvecFormalization.KernelContainedInTarget OrdvecFormalization.ruleFactorsThrough_image_iff_fiberInvariant OrdvecFormalization.ruleFactorsThrough_image_iff_kernelContainedInTarget OrdvecFormalization.ruleFactorsThrough_image_of_kernelContainedInTarget OrdvecFormalization.kernelContainedInTarget_of_ruleFactorsThrough_image OrdvecFormalization.observedBucketFibers_pairwiseDisjoint OrdvecFormalization.sample_eq_disjiUnion_fibers_over_observed OrdvecFormalization.sample_card_eq_sum_fiberSize_observed OrdvecFormalization.hasCollision_iff_not_injectiveOnSample OrdvecFormalization.hasCollision_of_card_gt_observedBuckets_card OrdvecFormalization.no_compatible_target_of_same_bucket_label_disagreement OrdvecFormalization.productMap OrdvecFormalization.productMap_eq_iff OrdvecFormalization.ProductFiberInvariant OrdvecFormalization.kernelContainedInTarget_productMap_iff_productFiberInvariant OrdvecFormalization.ruleFactorsThrough_product_fiberInvariant OrdvecFormalization.productFiberInvariant_ruleFactorsThrough_of_surjective OrdvecFormalization.ruleFactorsThrough_productMap_image_iff_productFiberInvariant OrdvecFormalization.ruleFactorsThrough_product_fixedLeft OrdvecFormalization.ruleFactorsThrough_product_fixedRight OrdvecFormalization.ProductSampleConsistent OrdvecFormalization.productSampleConsistent_iff_sampleConsistent_productMap OrdvecFormalization.productSampleConsistent_of_ruleFactorsThrough OrdvecFormalization.productSampleConsistent_iff_exists_productRuleFitsSample OrdvecFormalization.no_productQuotientTarget_of_sample_collision OrdvecFormalization.ObservedProductQuotients OrdvecFormalization.UnobservedReachableProductQuotients OrdvecFormalization.card_productQuotientRules OrdvecFormalization.productMap_image_subset_product_images OrdvecFormalization.productMap_image_eq_product_images OrdvecFormalization.productMap_image_card_eq_product_images_card OrdvecFormalization.productMap_image_card_le_product_images_card OrdvecFormalization.card_productImageQuotientRules OrdvecFormalization.card_productImageQuotientRules_eq_product_images OrdvecFormalization.card_productImageQuotientRules_le_product_images OrdvecFormalization.RuleFactorsThrough.product_pair_iff OrdvecFormalization.ProductSampleConsistent.prod_iff OrdvecFormalization.ComparisonObs OrdvecFormalization.comparisonObsEquivProd OrdvecFormalization.comparisonMap OrdvecFormalization.comparisonMap_eq_iff OrdvecFormalization.ComparisonFiberInvariant OrdvecFormalization.ruleFactorsThrough_comparison_fiberInvariant OrdvecFormalization.rankByScore OrdvecFormalization.rankByScore_factorsThrough_of_score_factorsThrough OrdvecFormalization.ComparisonImageBox OrdvecFormalization.comparisonMap_image_subset_imageBox OrdvecFormalization.comparisonMap_image_eq_imageBox OrdvecFormalization.comparisonMap_image_card_eq_product_images_card OrdvecFormalization.comparisonMap_image_card_le_product_images_card OrdvecFormalization.card_comparisonImageQuotientRules OrdvecFormalization.card_comparisonImageQuotientRules_eq_product_images OrdvecFormalization.card_comparisonImageQuotientRules_le_product_images OrdvecFormalization.pairQuotient OrdvecFormalization.pairQuotient_eq_iff OrdvecFormalization.pairRuleFactorsThrough_same_on_quotient_fibers OrdvecFormalization.no_pair_compatible_target_of_sample_collision OrdvecFormalization.quotientRefines_kernel_subset OrdvecFormalization.quotientRefines_of_surjective_of_kernel_subset OrdvecFormalization.quotientRefines_iff_kernel_subset_of_surjective OrdvecFormalization.imageQuotient_refines_iff_kernel_subset OrdvecFormalization.imageQuotient_refines_of_kernel_subset OrdvecFormalization.ScoresWithin OrdvecFormalization.ThresholdMargin OrdvecFormalization.thresholdAdmitBool OrdvecFormalization.threshold_admit_iff_of_scoresWithin_and_margin OrdvecFormalization.thresholdAdmitBool_eq_of_scoresWithin_and_margin OrdvecFormalization.thresholdAdmitBool_factorsThrough_of_score_factorsThrough OrdvecFormalization.thresholdAdmitBool_factorsThrough_image_of_score_margin OrdvecFormalization.EncoderDistortionProfile OrdvecFormalization.QuotientGeometryProfile OrdvecFormalization.scoresWithin_trans_add OrdvecFormalization.scoresWithin_of_encoderDistortionProfile_and_quotientGeometryProfile OrdvecFormalization.thresholdAdmitBool_eq_of_distortion_and_quotientGeometry OrdvecFormalization.thresholdAdmitBool_factorsThrough_image_of_distortion_and_quotientGeometry OrdvecFormalization.kernelContainedInTarget_of_distortion_and_quotientGeometry ``` Quotient sufficiency layer: ```lean OrdvecFormalization.exists_quotientPullback_finiteWeightedRisk_le OrdvecFormalization.exists_quotientPullback_finiteWeightedRisk_le_of_likelihoodRatioFactorsThrough OrdvecFormalization.exists_orderedQuotientThreshold_finiteWeightedRisk_le_of_orderedEvidenceFactor OrdvecFormalization.exists_calibratedOrderedThreshold_finiteBayesRisk_le_of_orderedEvidenceFactor OrdvecFormalization.exists_calibratedOrderedThreshold_finiteCostedBayesRisk_le_of_orderedEvidenceFactor OrdvecFormalization.exists_overlapQuotientThreshold_finiteWeightedRisk_le_of_likelihoodRatioFactor OrdvecFormalization.exists_overlapQuotientThreshold_finiteWeightedRisk_le_of_canonicalTilt OrdvecFormalization.exists_overlapQuotientThreshold_finiteBayesRisk_le_of_canonicalTilt_of_lt OrdvecFormalization.exists_overlapQuotientThreshold_finiteBayesRisk_le_and_bitmapHypergeomTail OrdvecFormalization.constantWeightBitmapOverlapTailCalibration OrdvecFormalization.exists_constantWeightBitmapOverlapTail_finiteBayesRisk_le_and_hypergeomTail OrdvecFormalization.exists_uniformBitmapOverlapTail_finiteBayesRisk_le_and_hypergeomTail OrdvecFormalization.quotientFiberExample_quotientTarget_factorsThrough_not_fiberTarget OrdvecFormalization.weightedBayesAdmit_iff_cutoff_le_likelihoodRatio OrdvecFormalization.exponentialTilt_hasMLR_of_lt OrdvecFormalization.fnch_bayesAdmit_isActualOverlapThreshold OrdvecFormalization.fnch_actualOverlapThreshold_bayesRisk_optimal OrdvecFormalization.fnch_costed_actualOverlapThreshold_bayesRisk_optimal ``` The core overlap-null theorem quantifies over: - `p : FNCHParams`, carrying `k <= N` and `draws <= N`. - `theta0 theta1 : Real`, with strict hypothesis `theta0 < theta1`. - `prior : Prior`, a bundled prior probability for `H1`. - all deterministic admission sets `R : Set p.support`. It produces a cut `cut : Fin (p.hi - p.lo + 2)` such that the actual-overlap threshold set has Bayes risk no larger than any deterministic admission set. The cost-sensitive theorem additionally quantifies over `costs : DecisionCosts`, whose `falseAccept` and `falseReject` fields weight the two error types independently. ## Dependency Shape ```text BitmapSymmetry -> overlap is the query-stabilizer orbit classifier FiniteExperiment -> FiniteQuotientSearch -> QuotientConstraints -> FiniteQuotientImage / QuotientKernel / FiniteFiberTopology -> FiniteProductQuotient / FinitePairQuotient -> QuotientRefinementKernel / FiniteObservationWindow -> ScoreMarginQuotient -> ProfileStability -> FiniteBayesRisk -> OrdinalSufficiency / OverlapSufficiency -> CanonicalTilt / OverlapBayesOptimal FiniteBayesRisk + OrdinalSufficiency -> CalibratedEvidence BitmapNull -> BitmapIncidence CalibratedEvidence + BitmapIncidence + OverlapBayesOptimal -> BitmapCalibration -> exact hypergeometric null calibration ``` For the module-by-module proof narrative, see [`proof-spine.md`](proof-spine.md). ## Public Names This section is the stable public Lean-name surface. Renames should be deliberate, documented changes because downstream docs and papers cite these names. Public Lean names: - `finiteWeightedBayesAdmitSet_optimal` - `quotientPullback` - `RuleFactorsThrough` - `mem_quotientPullback_of_quotient_preserving` - `QuotientCompatible` - `ObservedQuotients` - `ObservedQuotientsList` - `SampleConsistent` - `QuotientRuleFitsSample` - `FullTargetFitsSample` - `CompatibleTargets` - `CompatibleQuotientRules` - `quotientCompatible_exists_ruleq` - `quotientRule_induces_compatible_target` - `induced_targets_eq_of_ruleq_eq` - `induced_targets_eq_of_agree_on_range` - `sampleConsistent_of_quotientCompatible` - `no_compatible_target_of_sample_collision` - `sampleConsistent_of_exists_quotientRuleFitsSample` - `exists_quotientRuleFitsSample_of_sampleConsistent` - `sampleConsistent_iff_exists_quotientRuleFitsSample` - `QuotientImageFinset` - `QuotientImageBucket` - `card_quotientImageRules` - `UnobservedReachableQuotients` - `restrictRuleToImage` - `imageRuleToFullTarget` - `imageRuleToFullTarget_quotientCompatible` - `quotientRules_agree_on_observed_of_fit` - `fitting_quotient_rules_determined_on_observed` - `extendWithUnobserved` - `extendWithUnobserved_fits_sample` - `card_fullTargets` - `card_quotientRules` - `quotientCompatible_search_space_bound` - `card_unobserved_assignments` - `card_unobserved_bool_assignments` - `QuotientRefines` - `RuleFactorsThrough.of_refines` - `not_ruleFactorsThrough_coarse_of_not_fine` - `QuotientRefines.refl` - `QuotientRefines.trans` - `RuleFactorsThrough.prod_iff` - `SampleConsistent.prod_iff` - `FiberInvariant` - `HasNontrivialFiber` - `SeparatesSameFiber` - `ruleFactorsThrough_fiberInvariant` - `ruleFactorsThrough_same_admission_on_fibers` - `ruleFactorsThrough_same_evidence_on_fibers` - `finiteLikelihoodRatioFactorsThrough_fiberInvariant` - `finiteBayesAdmitFactorsThrough_same_on_fibers` - `fiberInvariant_ruleFactorsThrough_of_surjective` - `not_ruleFactorsThrough_of_separatesSameFiber` - `not_injective_of_hasNontrivialFiber` - `injective_of_not_hasNontrivialFiber` - `hasNontrivialFiber_iff_not_injective` - `exists_boolTarget_not_ruleFactorsThrough_of_hasNontrivialFiber` - `exists_pair_quotientTarget_factorsThrough_and_otherTarget_not` - `boolRuleFactorsThrough_positiveSet_eq_quotientPullback` - `QuotientImage` - `imageQuotient` - `imageQuotient_val` - `imageQuotient_surjective` - `Fiber` - `ImageFiber` - `ObservedBuckets` - `UnobservedBuckets` - `FiberSize` - `HasCollision` - `InjectiveOnSample` - `Kernel` - `TargetKernel` - `KernelContainedInTarget` - `kernelContainedInTarget_iff_fiberInvariant` - `ruleFactorsThrough_image_iff_fiberInvariant` - `ruleFactorsThrough_image_iff_kernelContainedInTarget` - `ruleFactorsThrough_image_of_kernelContainedInTarget` - `kernelContainedInTarget_of_ruleFactorsThrough_image` - `observedBucketFibers_pairwiseDisjoint` - `sample_eq_disjiUnion_fibers_over_observed` - `sample_card_eq_sum_fiberSize_observed` - `hasCollision_iff_not_injectiveOnSample` - `hasCollision_of_card_gt_observedBuckets_card` - `no_compatible_target_of_same_bucket_label_disagreement` - `productMap` - `productMap_apply` - `productMap_eq_iff` - `ProductFiberInvariant` - `kernelContainedInTarget_productMap_iff_productFiberInvariant` - `ruleFactorsThrough_product_fiberInvariant` - `productFiberInvariant_ruleFactorsThrough_of_surjective` - `ruleFactorsThrough_productMap_image_iff_productFiberInvariant` - `ruleFactorsThrough_product_fixedLeft` - `ruleFactorsThrough_product_fixedRight` - `ProductSampleConsistent` - `productSampleConsistent_iff_sampleConsistent_productMap` - `productSampleConsistent_of_ruleFactorsThrough` - `productSampleConsistent_iff_exists_productRuleFitsSample` - `no_productQuotientTarget_of_sample_collision` - `ObservedProductQuotients` - `UnobservedReachableProductQuotients` - `card_productQuotientRules` - `productMap_image_subset_product_images` - `productMap_image_eq_product_images` - `productMap_image_card_eq_product_images_card` - `productMap_image_card_le_product_images_card` - `card_productImageQuotientRules` - `card_productImageQuotientRules_eq_product_images` - `card_productImageQuotientRules_le_product_images` - `RuleFactorsThrough.product_pair_iff` - `ProductSampleConsistent.prod_iff` - `ComparisonObs` - `comparisonObsEquivProd` - `comparisonMap` - `comparisonMap_left` - `comparisonMap_first` - `comparisonMap_second` - `comparisonMap_eq_iff` - `ComparisonFiberInvariant` - `ruleFactorsThrough_comparison_fiberInvariant` - `rankByScore` - `rankByScore_factorsThrough_of_score_factorsThrough` - `ComparisonImageBox` - `comparisonMap_image_subset_imageBox` - `comparisonMap_image_eq_imageBox` - `comparisonMap_image_card_eq_product_images_card` - `comparisonMap_image_card_le_product_images_card` - `card_comparisonImageQuotientRules` - `card_comparisonImageQuotientRules_eq_product_images` - `card_comparisonImageQuotientRules_le_product_images` - `pairQuotient` - `pairQuotient_apply` - `pairQuotient_eq_iff` - `pairRuleFactorsThrough_same_on_quotient_fibers` - `no_pair_compatible_target_of_sample_collision` - `quotientRefines_kernel_subset` - `quotientRefines_of_surjective_of_kernel_subset` - `quotientRefines_iff_kernel_subset_of_surjective` - `imageQuotient_refines_iff_kernel_subset` - `imageQuotient_refines_of_kernel_subset` - `observationFamilyMap` - `ObservationFamilyAgreement` - `ObservationFamilySeparates` - `ObservationFamilyTargetInvariant` - `observationFamilyMap_eq_iff` - `kernel_observationFamilyMap_iff` - `observationFamilyMap_injective_iff_separates` - `kernelContainedInTarget_familyMap_iff_targetInvariant` - `ruleFactorsThrough_familyMap_image_iff_targetInvariant` - `windowMap` - `WindowAgreement` - `WindowSeparates` - `WindowTargetInvariant` - `windowMap_eq_iff` - `kernel_windowMap_iff` - `windowSeparates_iff` - `kernelContainedInTarget_windowMap_iff_targetInvariant` - `ruleFactorsThrough_windowMap_image_iff_targetInvariant` - `observationCoincidenceLength` - `exists_windowTargetInvariant_iff_eventually_separates_target` - `exists_windowSeparates_iff_eventually_separates` - `windowMap_refines_of_le` - `windowMap_kernel_subset_of_le` - `windowTargetInvariant_of_le` - `ruleFactorsThrough_windowMap_of_le` - `ruleFactorsThrough_windowMap_image_of_le` - `no_window_compatible_target_of_same_code_label_disagreement` - `no_window_image_compatible_target_of_same_code_label_disagreement` - `windowMap_image_card_le` - `windowMap_image_card_of_injective` - `ScoresWithin` - `ThresholdMargin` - `thresholdAdmitBool` - `threshold_admit_iff_of_scoresWithin_and_margin` - `thresholdAdmitBool_eq_of_scoresWithin_and_margin` - `thresholdAdmitBool_factorsThrough_of_score_factorsThrough` - `thresholdAdmitBool_factorsThrough_image_of_score_margin` - `EncoderDistortionProfile` - `QuotientGeometryProfile` - `scoresWithin_trans_add` - `scoresWithin_of_encoderDistortionProfile_and_quotientGeometryProfile` - `thresholdAdmitBool_eq_of_distortion_and_quotientGeometry` - `thresholdAdmitBool_factorsThrough_image_of_distortion_and_quotientGeometry` - `kernelContainedInTarget_of_distortion_and_quotientGeometry` - `quotientBayesAdmitSet_pullback_eq` - `exists_quotientPullback_finiteWeightedRisk_le` - `finiteWeightedBayesAdmit_iff_cutoff_le_likelihoodRatio` - `finiteBayesAdmitFactorsThrough_of_likelihoodRatioFactorsThrough` - `exists_quotientPullback_finiteWeightedRisk_le_of_likelihoodRatioFactorsThrough` - `orderedQuotientThresholdSet` - `FiniteLikelihoodRatioFactorsThroughOrderedEvidence` - `exists_orderedQuotientThreshold_finiteWeightedRisk_le_of_monotone` - `exists_orderedQuotientThreshold_finiteWeightedRisk_le_of_orderedEvidenceFactor` - `OrderedTailCalibration` - `exists_calibratedOrderedThreshold_finiteBayesRisk_le_of_orderedEvidenceFactor` - `exists_calibratedOrderedThreshold_finiteCostedBayesRisk_le_of_orderedEvidenceFactor` - `overlapQuotientThresholdSet` - `overlapQuotientThresholdSet_eq_orderedQuotientThresholdSet` - `FiniteLikelihoodRatioFactorsThroughOverlapEvidence` - `exists_overlapQuotientThreshold_finiteWeightedRisk_le_of_overlapEvidenceFactor` - `exists_overlapQuotientThreshold_finiteWeightedRisk_le_of_likelihoodRatioFactor` - `finiteExponentialTilt` - `finiteLikelihoodRatio_finiteExponentialTilt_eq_factor` - `finiteExponentialTilt_likelihoodRatioFactorsThroughOrderedEvidence` - `finiteExponentialTilt_likelihoodRatioFactorsThroughOverlapEvidence` - `exists_overlapQuotientThreshold_finiteWeightedRisk_le_of_finiteExponentialTilt` - `exists_overlapQuotientThreshold_finiteWeightedRisk_le_of_canonicalTilt` - `finiteBayesRisk` - `finiteCostedBayesRisk` - `exists_overlapQuotientThreshold_finiteBayesRisk_le_of_canonicalTilt` - `exists_overlapQuotientThreshold_finiteCostedBayesRisk_le_of_canonicalTilt` - `exists_overlapQuotientThreshold_finiteBayesRisk_le_of_canonicalTilt_of_lt` - `exists_overlapQuotientThreshold_finiteCostedBayesRisk_le_of_canonicalTilt_of_lt` - `bitmapOverlapParams` - `BitmapCut` - `bitmapCutThreshold` - `ConstantWeightBitmap` - `constantWeightBitmapUniformLaw` - `constantWeightBitmapOverlapTailSet` - `constantWeightBitmapOverlapEvidence` - `overlapQuotientThresholdSet_constantWeightBitmapOverlapEvidence_eq` - `constantWeightBitmapOverlapTailCalibration` - `exists_overlapQuotientThreshold_finiteBayesRisk_le_and_bitmapHypergeomTail` - `exists_overlapQuotientThreshold_finiteCostedBayesRisk_le_and_bitmapHypergeomTail` - `exists_constantWeightBitmapOverlapTail_finiteBayesRisk_le_and_hypergeomTail` - `exists_constantWeightBitmapOverlapTail_finiteCostedBayesRisk_le_and_hypergeomTail` - `exists_uniformBitmapOverlapTail_finiteBayesRisk_le_and_hypergeomTail` - `exists_uniformBitmapOverlapTail_finiteCostedBayesRisk_le_and_hypergeomTail` - `quotientFiberExample_quotientTarget_factorsThrough` - `quotientFiberExample_fiberTarget_not_factorsThrough` - `quotientFiberExample_quotientTarget_factorsThrough_not_fiberTarget` - `mlr_monotone_weightedBayesAdmit` - `mlr_monotone_bayesAdmit` - `weightedBayesAdmit_iff_cutoff_le_likelihoodRatio` - `bayesAdmit_iff_priorOddsCutoff_le_likelihoodRatio` - `weightedBayesAdmit_isThreshold` - `bayesAdmit_isThreshold` - `costedBayesAdmit_isThreshold` - `weighted_threshold_bayesRisk_optimal` - `threshold_bayesRisk_optimal` - `costed_threshold_bayesRisk_optimal` - `exponentialTilt_hasMLR` - `exponentialTilt_hasMLR_of_lt` - `fnch_bayesAdmit_isActualOverlapThreshold` - `fnch_actualOverlapThreshold_bayesRisk_optimal` - `fnch_costed_actualOverlapThreshold_bayesRisk_optimal` - `fnchActualPMF_mass_eq_fnchPMF_mass` - `overlapNull_threshold_bayesRisk_optimal_of_lt` - `overlapNull_costed_threshold_bayesRisk_optimal_of_lt` - `card_constantWeightBitmapSpace` - `card_insideOutsideChoices_of_query_card` - `card_bitmapOverlapFiber_of_query_card` - `bitmapHypergeomMass_eq_insideOutsideChoices_card_ratio` - `bitmapHypergeomMass_eq_overlapFiber_card_ratio` - `card_bitmapOverlapTailEvent_eq_sum_overlapFiber_card_of_query_card` - `bitmapOverlapTailMass_eq_bitmapHypergeomTail_of_query_card` - `bitmapUniformPMF` - `bitmapUniformPMF_overlapFiber_prob` - `bitmapUniformPMF_overlapTail_prob` - `BitmapPerm` - `queryStabilizer` - `permuteBitmap` - `bitmapOverlap_queryStabilizer_eq` - `exists_queryStabilizer_permuteBitmap_eq_of_card_eq_overlap_eq` - `exists_queryStabilizer_permuteBitmap_eq_iff_overlap_eq_of_card_eq` - `invariantOn_constantWeightBitmapSpace_eq_of_overlap_eq` - `invariantOn_constantWeightBitmapSpace_factorsThrough_overlap` Compatibility aliases: - `fnchActual_overlap_hasMLR_of_lt` - `fnch_overlap_admit_threshold` - `fnch_overlap_threshold_bayes_optimal` - `fnch_overlap_costed_threshold_bayes_optimal` ## What Is Not Claimed - No empirical null calibration theorem is formalized here. The new bitmap-null route concerns the exact idealized constant-weight null, not real-corpus independence or effective dimension. - `CalibratedEvidence.lean` packages a supplied equality at the cutoff returned by the ordered Bayes-optimality theorem. It does not prove null adequacy, event equivalence, or any real-corpus calibration claim. - No claim is made that the textbook hypergeometric is the deployment null for real embeddings. - No claim is made that a real encoder's semantic evidence actually factors through an ordinal quotient; the quotient theorem states the exact sufficient condition under which such compression is decision-theoretically lossless. - No claim is made that real encoders satisfy the query-stabilizer symmetry assumption. The symmetry theorem identifies the canonical invariant when the bitmap problem is treated as invariant under query-preserving coordinate relabelings. - No claim is made that quotient sufficiency for one decision makes the quotient representation-complete. The quotient-constraint layer proves that factorized targets are fiber-invariant and that nontrivial quotients necessarily discard some possible other distinction. - The finite quotient-search layer turns consistent samples into partial bucket-level constraints, not proof of a global empirical quotient contract. Same-bucket label disagreements are formal falsifiers; same-bucket agreement is only finite sample evidence. - The image-quotient layer proves surjectivity only onto the reachable image of a finite compression map, not onto the full ambient quotient codomain. - The finite observation-window layer does not claim that any individual lossy probe is injective or that a real probe family is globally sufficient. It proves the generic kernel calculus: joint-window agreement is the relevant fiber relation, longer windows refine shorter windows, and target sufficiency only requires target invariance on joint-window fibers. - The score-margin layer is a sufficient-condition theorem for threshold stability under approximation; it does not prove contrastive training implies ordinal or bitmap quotient invariance. - The profile-stability layer packages supplied finite score certificates. It does not define manifest schema, estimate encoder distortion, or claim that a real encoder globally satisfies those profile assumptions. - No randomized tests, Neyman-Pearson lemma, UMP statement, or Karlin-Rubin theorem is included in this milestone. - No asymptotic or measure-theoretic probability result is used; the proof is finite and deterministic over `Fin`. ## Reviewer Checks Run: ```sh make build make verify make check-doc-names make audit make lint ``` `make verify` checks the public theorem dashboard and prints the axiom audit. `make check-doc-names` extracts documented names from the markdown files and checks that they resolve through Lean. Expected axioms are Lean's standard baseline: ```text [propext, Classical.choice, Quot.sound] ```