Skip to content

proof-spine.md

Latest commit

 

History

History
293 lines (246 loc) · 13 KB

proof-spine.md

File metadata and controls

293 lines (246 loc) · 13 KB
Raw

Proof Spine

This is the module-by-module path through the checked Lean development. The front-door README stays short; this file is for reviewers who want to follow the formal dependency story.

Conceptual Stack

Finite observations
  -> quotient search / version-space reduction
  -> generic quotient constraints / fiber equivalence
  -> reachable quotient image / kernel containment
  -> finite fiber topology / product and pair quotients / refinement kernels
  -> finite observation windows / target-separating probe families
  -> score-margin threshold stability
  -> finite profile-stability certificates
  -> quotient by symmetry / factorization contract
  -> ordered overlap evidence
  -> monotone likelihood ratio
  -> Bayes-optimal threshold
  -> supplied calibration equality at the same cutoff
  -> exact finite bitmap-null calibration

The algebraic and decision-theoretic layers do different jobs:

  • BitmapSymmetry.lean explains why literal bitmap overlap is the canonical invariant when the problem is invariant under query-preserving coordinate relabelings.
  • FiniteExperiment.lean, FiniteQuotientSearch.lean, and QuotientConstraints.lean separate the generic finite quotient API from version-space reduction and the structural consequence that factorized rules are fiber-invariant, while nontrivial quotients necessarily discard some other possible full-space distinction.
  • FiniteQuotientImage.lean, QuotientKernel.lean, and FiniteFiberTopology.lean keep quotient reasoning on the reachable image, relate factorization to kernel containment, and count the observed fiber clumps induced by finite samples.
  • FiniteProductQuotient.lean, FinitePairQuotient.lean, QuotientRefinementKernel.lean, and FiniteObservationWindow.lean add generic product quotients for pairwise, multi-target, and ranking-comparison targets; a retrieval-style pair wrapper; refinement as kernel inclusion; and a generic windowed-observation bridge: individual lossy probes may collide, while a finite family/window is sufficient for a target exactly when joint-code agreement preserves that target.
  • ScoreMarginQuotient.lean adds a sufficient margin-stability theorem for threshold admission under score approximation.
  • ProfileStability.lean packages supplied encoder-distortion and quotient-geometry score certificates inside the finite model, composes their errors, and reuses the margin theorem. It does not estimate encoder distortion or define a manifest schema.
  • OrdinalSufficiency.lean, MLR.lean, and BayesThreshold.lean explain why monotone quotient evidence gives an optimal deterministic threshold.
  • CalibratedEvidence.lean packages a supplied ordered-tail calibration equality with the Bayes-optimal cutoff. It does not prove null adequacy or identify the calibrated event with a bitmap event.
  • BitmapIncidence.lean, BitmapNull.lean, and BitmapCalibration.lean identify the bitmap event bridge and the exact hypergeometric tail under the idealized uniform constant-weight bitmap null.

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

Lean import order is not identical to conceptual dependence: BitmapSymmetry imports bitmap definitions from BitmapNull, but it does not depend on BitmapCalibration.

Modules

  1. FiniteExperiment.lean Defines finite positive laws, finite weighted risk, quotient pullbacks, and the quotient-form optimality theorem. If pointwise Bayes evidence or the likelihood ratio factors through a quotient, then some quotient-form admit set has no larger risk than any full-space deterministic rule. It also includes the finite witness that a quotient can preserve one decision target while discarding another.

  2. FiniteQuotientSearch.lean Formalizes version-space reduction under a quotient contract. Quotient-compatible targets are bucket-level rules; sampled same-bucket label disagreements falsify quotient compatibility; consistent samples admit quotient-level fitting rules; observed buckets are fixed while reachable, unobserved image buckets describe the remaining induced full-target uncertainty; refinement transfers factorization from coarser quotients to finer quotients; and paired targets factor exactly when their components factor.

  3. QuotientConstraints.lean Defines generic quotient-fiber invariance, nontrivial quotient fibers, and same-fiber separation. It proves that factorized rules, evidence values, and finite likelihood ratios are constant on quotient fibers; that a surjective quotient can recover factorization from fiber invariance; and that nontrivial quotients are necessarily incomplete for some other target.

  4. FiniteQuotientImage.lean Restricts a finite compression map to its reachable image. The map imageQuotient C is surjective by construction, so quotient reasoning can use the image actually reached by an encoder/corpus map without assuming the full ambient quotient codomain is populated.

  5. QuotientKernel.lean Defines compression kernels and target kernels. It proves that a target factors through the image quotient exactly when the compression kernel is contained in the target kernel, equivalently when the target is constant on the compression fibers.

  6. FiniteFiberTopology.lean Records the finite clump structure of a sample under a quotient map: observed bucket fibers are pairwise disjoint, sample size is the sum of observed fiber sizes, collisions are exactly failure of sample injectivity, and too many sampled points for the observed bucket count forces a collision.

  7. FiniteProductQuotient.lean Defines the generic product quotient productMap Q₁ Q₂ and its fiber invariance contract. It proves that product factorization implies invariance under same left and right compressed buckets; that surjective and image-restricted product quotients recover factorization from that invariance; that a product-factorized target specializes to fixed-left and fixed-right quotient rules; that finite same-product-code label disagreements are falsifiers; that product quotient rule spaces have the expected finite cardinality; that reachable product images are exactly component-image products; that product targets and sample consistency split componentwise; and that a score factoring through the query/document product quotient induces ranking comparisons factoring through the corresponding query/document/document comparison quotient, whose reachable image is exactly the one-left/two-right component-image box.

  8. FinitePairQuotient.lean Packages the generic product quotient under query/document names for retrieval-facing docs and compatibility. It keeps the small API for pairQuotient, same compressed query/document bucket invariance, and the finite same-product-bucket label-disagreement falsifier.

  9. QuotientRefinementKernel.lean Relates quotient refinement to kernel inclusion. Refinement implies fine-kernel collisions are coarse-kernel collisions; conversely, kernel inclusion builds a refinement when the fine quotient is surjective, in particular for image quotients.

  10. FiniteObservationWindow.lean Defines arbitrary observation-family maps and countable-prefix window maps. It proves that a window kernel is exactly coordinatewise agreement; that target factorization through the reachable image of a window is equivalent to target invariance on joint-code fibers; that longer windows refine shorter windows and can only shrink kernels; that same-window-code label disagreement is a finite falsifier; and that, on a finite domain, a target-sufficient finite window exists exactly when every target-disagreeing pair is eventually separated by some coordinate. Full window injectivity is recorded as the special case where the target is identity.

  11. ScoreMarginQuotient.lean Gives a sufficient-condition theorem for score-based admission: if an approximate quotient score is uniformly close to a full score and full-score threshold margins exceed the error, then Boolean threshold admission is unchanged and factors through the same image quotient when the approximate score does.

  12. ProfileStability.lean Packages two supplied finite score certificates: an EncoderDistortionProfile, saying an encoder score is uniformly close to a source/task score, and a QuotientGeometryProfile, saying a quotient score factors through the reachable image quotient while approximating the encoder score. The module composes the errors and proves threshold-decision preservation, image-quotient factorization, and kernel containment under the composed margin condition.

  13. FiniteBayesRisk.lean Gives Bayes-risk and cost-sensitive Bayes-risk names to the generic finite weighted-risk API.

  14. OrdinalSufficiency.lean Adds ordered quotient evidence. If the full likelihood ratio is a monotone function of ordered quotient evidence, then some pulled-back ordinal threshold is Bayes-optimal among all deterministic full-space rules.

  15. CalibratedEvidence.lean Combines the ordered threshold theorem with an externally supplied OrderedTailCalibration, returning one cutoff that is both Bayes-optimal and calibrated by the supplied equality. This layer is graph-neutral and does not prove empirical null adequacy.

  16. OverlapSufficiency.lean Specializes the ordered quotient bridge to overlap coordinates, exposing the actual-overlap threshold set used by later theorems.

  17. CanonicalTilt.lean Instantiates the factorization contract with a finite exponential family over arbitrary full observations. Tilting a positive base law by quotient-level overlap evidence makes the likelihood ratio a monotone function of that evidence.

  18. OverlapBayesOptimal.lean Uses the finite Bayes-risk and cost-sensitive wrappers to expose the canonical overlap-tilt theorem in Bayes-risk form.

  19. BitmapIncidence.lean Defines the constant-weight bitmap subtype, the uniform finite law on that subtype, literal bitmap overlap evidence, and the bridge showing pulled-back actual-overlap thresholds are literal bitmap overlap tail events.

  20. BitmapCalibration.lean Connects the canonical overlap-tilt theorem to constant-weight bitmap observations. It proves that the Bayes-optimal pulled-back cutoff is the literal bitmap overlap tail event and that the uniform bitmap null assigns that event the corresponding hypergeometric upper-tail probability.

  21. BitmapSymmetry.lean Defines coordinate permutations, the query stabilizer, and the induced action on bitmaps. It proves query-stabilizer permutations preserve overlap, that equal-cardinality bitmaps with equal query overlap lie in the same query-stabilizer orbit, and that every invariant constant-weight bitmap statistic factors through literal overlap.

  22. FiniteDecision.lean Proves that every monotone predicate on a finite ordered support is represented by a threshold cut, including accept-all and reject-all boundary cuts.

  23. MLR.lean States monotone likelihood ratio by cross multiplication and proves it makes weighted pointwise Bayes admission monotone. It also connects admission to the usual likelihood-ratio cutoff when denominators are positive.

  24. BayesThreshold.lean Proves Bayes and cost-sensitive Bayes thresholds minimize finite pointwise risk by summing pointwise inequalities.

  25. ExponentialTilt.lean Proves positive finite exponential tilts have monotone likelihood ratio as the tilt parameter increases.

  26. FNCH.lean Connects literal actual-overlap Fisher noncentral hypergeometric weights to the shifted exponential-tilt implementation after normalization.

  27. OverlapNull.lean Provides overlap-null theorem wrappers and compatibility aliases for the FNCH overlap threshold optimality surface.

  28. BitmapNull.lean Defines constant-weight bitmap spaces, overlap fibers, tail events, and the inside/outside choice space. It proves the hypergeometric overlap-fiber cardinality and the exact upper-tail probability under the uniform finite bitmap law.

  29. Verify.lean Checks the public theorem names and prints their axiom footprint.

Reviewer Checks

Run:

make build
make verify
make check-doc-names
make audit
make lint

The expected axiom baseline is:

[propext, Classical.choice, Quot.sound]