Skip to content

theorem-map.md

Latest commit

 

History

History
652 lines (602 loc) · 27.7 KB

theorem-map.md

File metadata and controls

652 lines (602 loc) · 27.7 KB
Raw

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:

OrdvecFormalization.exists_uniformBitmapOverlapTail_finiteBayesRisk_le_and_hypergeomTail

Cost-sensitive checked theorem:

OrdvecFormalization.exists_uniformBitmapOverlapTail_finiteCostedBayesRisk_le_and_hypergeomTail

General positive-base theorem, with separate uniform-null tail calibration at the same cutoff:

OrdvecFormalization.exists_constantWeightBitmapOverlapTail_finiteBayesRisk_le_and_hypergeomTail

Supporting Layers

Core FNCH overlap theorem:

OrdvecFormalization.overlapNull_threshold_bayesRisk_optimal_of_lt
OrdvecFormalization.fnch_overlap_threshold_bayes_optimal

Cost-sensitive extension:

OrdvecFormalization.overlapNull_costed_threshold_bayesRisk_optimal_of_lt
OrdvecFormalization.fnch_overlap_costed_threshold_bayes_optimal

Exact constant-weight bitmap null:

OrdvecFormalization.card_bitmapOverlapFiber_of_query_card
OrdvecFormalization.bitmapOverlapTailMass_eq_bitmapHypergeomTail_of_query_card
OrdvecFormalization.bitmapUniformPMF_overlapFiber_prob
OrdvecFormalization.bitmapUniformPMF_overlapTail_prob

Bitmap symmetry layer:

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:

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:

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:

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:

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

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.

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:

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:

[propext, Classical.choice, Quot.sound]