# 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

```text
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

```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
```

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.

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

27. `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.

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

## Reviewer Checks

Run:

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

The expected axiom baseline is:

```text
[propext, Classical.choice, Quot.sound]
```