diff --git a/docs/paper/ordvec_formalization_paper.pdf b/docs/paper/ordvec_formalization_paper.pdf
index f8f80d7..81bbb35 100644
Binary files a/docs/paper/ordvec_formalization_paper.pdf and b/docs/paper/ordvec_formalization_paper.pdf differ
diff --git a/docs/paper/ordvec_formalization_paper.tex b/docs/paper/ordvec_formalization_paper.tex
index e98f07d..fd0b029 100644
--- a/docs/paper/ordvec_formalization_paper.tex
+++ b/docs/paper/ordvec_formalization_paper.tex
@@ -103,6 +103,16 @@ \section{Purpose and Scope}
 question is whether a specific admission decision can be made with no loss
 after passing from \(\Omega\) to \(Z\).
 
+In applications, the chosen ``full'' observation space is already relative.
+A neural embedding, sparse lexical vector, chunked document view, or bitmap
+signature can itself be treated as an observation map out of a richer source.
+The formalization does not require this chain to end in an ontologically
+complete \(\Omega\).  It fixes the finite observation layer being audited and
+asks whether the target under discussion is invariant on the fibers of the next
+quotient.  The recursion stops at the target: once the decision, score,
+comparison, or multi-target signature is fixed, the theorem asks whether the
+proposed quotient preserves exactly that behavior.
+
 The Lean repository answers this question in a finite setting.  It proves that
 under exact factorization assumptions, quotient-form rules are sufficient for
 Bayes-optimal admission.  It also proves the converse kind of structural
@@ -414,7 +424,12 @@ \subsection{Cardinality reduction}
   \card{A^Z}=\card{A}^{\card{Z}}.
 \]
 These are \lean{card_fullTargets}, \lean{card_quotientRules}, and
-\lean{quotientCompatible_search_space_bound}.  Lean also defines
+\lean{quotientCompatible_search_space_bound}.  On a reachable image, the
+generic count
+\[
+  \card{A^{\im(Q)}}=\card{A}^{\card{\im(Q)}}
+\]
+is checked by \lean{card_quotientImageRules}.  Lean also defines
 \lean{UnobservedReachableQuotients} for the reachable image buckets not yet
 seen in the sample.  The induced full-target unobserved-bucket freedom
 has the corresponding count
@@ -434,7 +449,7 @@ \subsection{Cardinality reduction}
 full-target uncertainty is exactly the finite set of assignments on reachable
 unobserved image buckets.
 
-\subsection{Refinement and products}
+\subsection{Refinement and paired targets over one quotient}
 
 If a fine quotient \(Q_f\) determines a coarse quotient \(Q_c\), Lean writes
 this as \lean{QuotientRefines}.  Theorems
@@ -446,10 +461,12 @@ \subsection{Refinement and products}
 factor through the fine quotient rules out factorization through any coarser
 one.
 
-The product theorem \lean{RuleFactorsThrough.prod_iff} proves that a paired
-target factors through a quotient exactly when both components factor through
-it.  The sample-level analogue \lean{SampleConsistent.prod_iff} gives the same
-componentwise criterion for finite samples.
+The paired-target theorem \lean{RuleFactorsThrough.prod_iff} proves that a
+paired target factors through a single quotient exactly when both components
+factor through it.  The sample-level analogue \lean{SampleConsistent.prod_iff}
+gives the same componentwise criterion for finite samples.  This is distinct
+from the later product-map quotient \(C_q\times C_d\), which handles
+query/document-style product domains.
 
 \begin{interpretation}
 These theorems are useful for probe design.  A refined quotient gives more
@@ -604,6 +621,7 @@ \subsection{Product quotients, ranking, and kernel refinements}
 \begin{leanblock}
 \lean{productMap}\quad
 \lean{ProductFiberInvariant}\quad
+\lean{kernelContainedInTarget_productMap_iff_productFiberInvariant}\\
 \lean{ruleFactorsThrough_product_fiberInvariant}\\
 \lean{productFiberInvariant_ruleFactorsThrough_of_surjective}\\
 \lean{ruleFactorsThrough_productMap_image_iff_productFiberInvariant}
@@ -612,6 +630,13 @@ \subsection{Product quotients, ranking, and kernel refinements}
 constant on product fibers.  The surjective and image-restricted converses are
 the clean formal versions of working on the actually reached product image
 rather than pretending that the full ambient code space is populated.
+The finite product-search vocabulary names both observed and reachable
+unobserved product buckets:
+\begin{leanblock}
+\lean{ObservedProductQuotients}\quad
+\lean{UnobservedReachableProductQuotients}\quad
+\lean{card_productQuotientRules}
+\end{leanblock}
 The finite search space is then exactly controlled by the component images:
 \begin{leanblock}
 \lean{productMap_image_subset_product_images}\\
@@ -635,10 +660,16 @@ \subsection{Product quotients, ranking, and kernel refinements}
   \card{A}^{\card{\im(C_q)}\card{\im(C_d)}}
 \]
 for finite label type \(A\).
+This exact product-image equality is a theorem about the full formal product
+domain \(\Omega_q\times\Omega_d\).  A logged candidate graph, prefiltered
+trace, or finite benchmark subset need not realize every independent
+query/document pair; such restricted empirical surfaces should be treated as
+their own finite observed images.
 
 Finite pair samples get the corresponding falsifier:
 \begin{leanblock}
 \lean{ProductSampleConsistent}\quad
+\lean{productSampleConsistent_iff_sampleConsistent_productMap}\\
 \lean{productSampleConsistent_of_ruleFactorsThrough}\\
 \lean{productSampleConsistent_iff_exists_productRuleFitsSample}\\
 \lean{no_productQuotientTarget_of_sample_collision}
@@ -667,8 +698,11 @@ \subsection{Product quotients, ranking, and kernel refinements}
 Ranking comparisons are handled by a three-field comparison observation:
 \begin{leanblock}
 \lean{ComparisonObs}\quad
+\lean{comparisonObsEquivProd}\quad
 \lean{comparisonMap}\quad
-\lean{ComparisonFiberInvariant}\\
+\lean{comparisonMap_eq_iff}\\
+\lean{ComparisonFiberInvariant}\quad
+\lean{ruleFactorsThrough_comparison_fiberInvariant}\\
 \lean{rankByScore}\quad
 \lean{rankByScore_factorsThrough_of_score_factorsThrough}
 \end{leanblock}
@@ -699,6 +733,7 @@ \subsection{Product quotients, ranking, and kernel refinements}
 \lean{FinitePairQuotient.lean} remains as a retrieval-facing wrapper around the
 generic product API:
 \begin{leanblock}
+\lean{pairQuotient}\quad
 \lean{pairQuotient_eq_iff}\quad
 \lean{pairRuleFactorsThrough_same_on_quotient_fibers}\quad
 \lean{no_pair_compatible_target_of_sample_collision}
@@ -1216,6 +1251,26 @@ \subsection{What gets reduced}
 unobserved, Boolean extrapolations have size \(2^m\).  This is exactly the
 ``smaller finite set of extrapolations'' established by the Lean search layer.
 
+For pairwise retrieval targets, the haystack is not a document-only bucket
+space.  It is the reachable product image of compressed query and document
+codes.  On the full formal product domain this has size
+\(\card{\im(C_q)}\card{\im(C_d)}\), and comparison/ranking targets live over
+the one-query/two-document image box of size
+\(\card{\im(C_q)}\card{\im(C_d)}^2\).  On a finite logged sample or prefiltered
+trace, the observed image may be smaller, and the same finite-bucket logic
+applies to that restricted surface.
+
+For probe families, the reduction is by the realized joint-code image.  The
+point is not that each bitmap, ordinal, lexical, query-transform, or
+context-window probe is injective by itself.  The finite question is whether
+agreement on the whole joint code preserves the target behavior being audited.
+
+For score-threshold decisions, the margin/profile layer gives a different
+kind of reduction: supplied finite error and margin certificates can turn an
+approximate quotient score into an exact threshold-decision certificate.  Near
+the decision boundary, this requires explicit margin evidence; absent that
+evidence, the theorem intentionally does not certify equality.
+
 \subsection{How bitmap probes fit}
 
 For small bitmap probes, the constant-weight theorem gives an idealized target
@@ -1260,6 +1315,16 @@ \section{Non-Claims}
 \item It does not prove that any concrete family of production probes is
   globally target-sufficient.  The window layer proves the finite kernel
   calculus for such probe families once the observations and target are fixed.
+\item It does not prove top-\(k\) list equality, tie-policy preservation, or
+  nDCG preservation from the ranking-comparison theorem alone.  Those require
+  additional ordering, tie, or margin assumptions.
+\item It does not let product-image equalities for the full formal product
+  domain be read as claims about arbitrary logged candidate graphs or
+  prefiltered empirical traces.
+\item It does not certify near-threshold score decisions unless the supplied
+  score-error and margin hypotheses exclude those near ties.
+\item It does not prove a continuous Takens-style embedding theorem.  The
+  observation-window layer is a finite-domain target-separation calculus.
 \item It does not include randomized tests, Neyman--Pearson optimality,
   uniformly most powerful tests, Karlin--Rubin theory, asymptotics, or
   measure-theoretic probability.
@@ -1288,8 +1353,8 @@ \section{Lean Verification Surface}
   [\texttt{propext},\ \texttt{Classical.choice},\ \texttt{Quot.sound}].
 \]
 
-The root import file and public verification dashboard cover these main
-modules and support layers:
+The root import file covers the main modules directly, and the public
+verification dashboard also checks their lower support layers:
 \begin{leanblock}
 \lean{FiniteExperiment}\quad
 \lean{FiniteQuotientSearch}\quad
@@ -1323,7 +1388,7 @@ \section{Lean Verification Surface}
 
 \section{Conclusion}
 
-The Lean development proves a finite theorem stack with two complementary
+The Lean development proves a finite theorem stack with three complementary
 messages.
 
 First, if the Bayes-relevant evidence for a binary admission task factors
@@ -1338,6 +1403,16 @@ \section{Conclusion}
 leave unobserved extrapolation freedom.  It narrows the field of possible
 global structures without pretending to identify real encoders automatically.
 
+Third, the same contract composes into retrieval-facing structures.  Product
+quotients express pairwise query/document targets and multi-target signatures;
+comparison quotients express score-induced ranking decisions; observation
+windows express finite bundles of lossy probes; and margin/profile theorems
+turn supplied finite score certificates into exact threshold-decision
+consequences.  These layers do not remove the empirical burden.  They specify
+what must be tested: which compressed buckets, product codes, joint probe
+codes, and near-boundary margins would falsify or support the claimed quotient
+contract.
+
 \begin{thebibliography}{9}
 
 \bibitem{Fisher1922}
diff --git a/docs/paper/ordvec_formalization_paper.txt b/docs/paper/ordvec_formalization_paper.txt
index 87740db..7eb0cdb 100644
--- a/docs/paper/ordvec_formalization_paper.txt
+++ b/docs/paper/ordvec_formalization_paper.txt
@@ -44,6 +44,13 @@ Q:Ω→Z
 throws away all distinctions inside each fiber Q−1 (z). The central question is not whether Q
 preserves the whole representation. The central question is whether a specific admission decision
 can be made with no loss after passing from Ω to Z.
+In applications, the chosen “full” observation space is already relative. A neural embedding,
+sparse lexical vector, chunked document view, or bitmap signature can itself be treated as an
+observation map out of a richer source. The formalization does not require this chain to end in an
+ontologically complete Ω. It fixes the finite observation layer being audited and asks whether the
+target under discussion is invariant on the fibers of the next quotient. The recursion stops at the
+target: once the decision, score, comparison, or multi-target signature is fixed, the theorem asks
+whether the proposed quotient preserves exactly that behavior.
 The Lean repository answers this question in a finite setting. It proves that under exact
 factorization assumptions, quotient-form rules are sufficient for Bayes-optimal admission. It also
 proves the converse kind of structural pressure: if a rule, target, evidence statistic, or likelihood
@@ -79,6 +86,7 @@ map is treated as surjective onto its reachable image; factorization through tha
 to containment of the compression kernel inside the target kernel. Sample fibers are counted as
 observed clumps; product quotients handle query/document decisions, multi-target signatures,
 and score-induced ranking comparisons; refinement is characterized by kernel inclusion; and score
+
 approximation plus margin separation gives a sufficient condition for threshold decisions to remain
 quotient-factorized. Between refinement and score margins, the observation-window layer proves
 that a finite family of lossy probes is target-sufficient exactly when agreement on the whole joint
@@ -86,7 +94,6 @@ code preserves the target. The profile-stability layer packages supplied finite
 composes their errors.
 The final band specializes the quotient machinery. Ordered quotient evidence and monotone
 likelihood ratios give threshold-form Bayes rules. A supplied calibration equality can be attached to
-
 the same cutoff. Canonical finite overlap tilts instantiate the ordered-evidence assumptions. Bitmap
 symmetry explains why literal overlap is the canonical invariant under query-preserving coordinate
 relabelings, and the constant-weight bitmap null supplies the exact hypergeometric tail for the
@@ -135,11 +142,11 @@ Quotient pullbacks
 A quotient-level rule is a set RZ ⊆ Z. Its pullback is
 Q−1 (RZ ) = {ω ∈ Ω : Q(ω) ∈ RZ }.
 Lean calls this quotientPullback.
+
 Definition 3.2 (Factorization through a quotient). A rule or target δ : Ω → A factors through
 Q : Ω → Z if there exists a function δZ : Z → A such that
 δ(ω) = δZ (Q(ω))
 for every ω ∈ Ω.
-
 This is the formal predicate RuleFactorsThrough.
 Theorem 3.3 (Quotient-form Bayes optimality). If the pointwise Bayes admission predicate is
 constant on every quotient fiber, then there is a quotient-level set RZ ⊆ Z whose pullback has
@@ -185,6 +192,7 @@ bucket, anything claimed to factor through that quotient must give them the same
 encoder-derived quotient is proposed as sufficient for a target decision, then two probes with the
 same quotient value but different required decisions falsify the exact global contract.
 
+
 4.2
 
 Recovering factorization from fiber invariance
@@ -198,7 +206,6 @@ fiber invariant + surjective Q
 factors through Q.
 
 This is fiberInvariant_ruleFactorsThrough_of_surjective. Thus, in the surjective finite setting, factorization and fiber invariance are the same structural condition.
-
 The important qualification is the codomain. For an ambient compression C : Ω → Z, Lean
 does not require surjectivity onto all of Z. The right codomain is the reachable image im(C), where
 surjectivity holds by construction. This is the bridge from global quotient algebra to finite empirical
@@ -241,6 +248,8 @@ be a labeling function. A sample is quotient-consistent when labels are constant
 fibers:
 ω1 , ω2 ∈ S, Q(ω1 ) = Q(ω2 ) =⇒ y(ω1 ) = y(ω2 ).
 This is SampleConsistent.
+
+
 Theorem 5.1 (Sample consistency equals quotient-rule fit). Assuming A is inhabited, a finite
 sample is quotient-consistent if and only if there exists a quotient-level rule rZ : Z → A fitting the
 sample:
@@ -280,11 +289,15 @@ Lean proves the exact cardinality of the full target space and the quotient-rule
 |AZ | = |A||Z| .
 
 These are card_fullTargets, card_quotientRules, and quotientCompatible_search_space_
-bound. Lean also defines UnobservedReachableQuotients for the reachable image buckets not yet
-seen in the sample. The induced full-target unobserved-bucket freedom has the corresponding count
+bound. On a reachable image, the generic count
+|Aim(Q) | = |A||im(Q)|
+is checked by card_quotientImageRules. Lean also defines UnobservedReachableQuotients for
+the reachable image buckets not yet seen in the sample. The induced full-target unobserved-bucket
+freedom has the corresponding count
 |A||{z∈im(Q):z /∈Q(S)}| ,
 checked by card_unobserved_assignments. For Boolean labels this specializes to
 2|{z∈im(Q):z /∈Q(S)}| ,
+
 checked by card_unobserved_bool_assignments.
 This is the formal search-space result. A quotient hypothesis replaces an arbitrary function
 on Ω by a function on quotient buckets. Observed consistent labels then pin down the observed
@@ -293,7 +306,7 @@ unobserved image buckets.
 
 5.4
 
-Refinement and products
+Refinement and paired targets over one quotient
 
 If a fine quotient Qf determines a coarse quotient Qc , Lean writes this as QuotientRefines.
 Theorems QuotientRefines.refl and QuotientRefines.trans prove that refinement behaves as
@@ -301,10 +314,11 @@ expected. The factorization transfer theorem RuleFactorsThrough.of_refines says
 factoring through a coarse quotient also factors through a finer quotient. The contrapositive
 form not_ruleFactorsThrough_coarse_of_not_fine says that failure to factor through the fine
 quotient rules out factorization through any coarser one.
-The product theorem RuleFactorsThrough.prod_iff proves that a paired target factors
-through a quotient exactly when both components factor through it. The sample-level analogue
-SampleConsistent.prod_iff gives the same componentwise criterion for finite samples.
-
+The paired-target theorem RuleFactorsThrough.prod_iff proves that a paired target factors
+through a single quotient exactly when both components factor through it. The sample-level
+analogue SampleConsistent.prod_iff gives the same componentwise criterion for finite samples.
+This is distinct from the later product-map quotient Cq × Cd , which handles query/document-style
+product domains.
 Interpretation 5.3. These theorems are useful for probe design. A refined quotient gives more
 buckets and can only make factorization easier. Pairing multiple labels or probe tasks makes the
 quotient contract stricter: the pair factors only if each component does.
@@ -338,6 +352,7 @@ Interpretation 6.1. This is the formal version of working on the observed encode
 rather than pretending that every code in the full ambient quotient codomain is reachable. It is
 exactly the move from “globally surjective onto all possible codes” to “surjective onto the actual
 finite image being studied.”
+
 The same file gives the finite vocabulary for image reasoning:
 QuotientImage
 
@@ -373,8 +388,6 @@ y(ω1 ) = y(ω2 ).
 KernelContainedInTarget(C, y),
 
 meaning that every compression collision is also a target indistinguishability.
-
-
 Theorem 6.2 (Image quotient factorization equals kernel containment). For finite Ω, a target
 y : Ω → A factors through the reachable image quotient of C if and only if
 Kernel(C) ⊆ TargetKernel(y).
@@ -435,20 +448,26 @@ Cq (q1 ) = Cq (q2 ),
 
 Cd (d1 ) = Cd (d2 )
 
-Lean exposes this through
-
 =⇒
 
 y(q1 , d1 ) = y(q2 , d2 ).
 
-productMap ProductFiberInvariant ruleFactorsThrough_product_fiberInvariant
+Lean exposes this through
+productMap ProductFiberInvariant
+kernelContainedInTarget_productMap_iff_productFiberInvariant
+ruleFactorsThrough_product_fiberInvariant
 productFiberInvariant_ruleFactorsThrough_of_surjective
 ruleFactorsThrough_productMap_image_iff_productFiberInvariant
 
 The first direction is the retrieval contract: any product-factorized target is constant on product
 fibers. The surjective and image-restricted converses are the clean formal versions of working on
 the actually reached product image rather than pretending that the full ambient code space is
-populated. The finite search space is then exactly controlled by the component images:
+populated. The finite product-search vocabulary names both observed and reachable unobserved
+product buckets:
+ObservedProductQuotients UnobservedReachableProductQuotients
+card_productQuotientRules
+
+The finite search space is then exactly controlled by the component images:
 productMap_image_subset_product_images
 productMap_image_eq_product_images
 productMap_image_card_eq_product_images_card
@@ -462,9 +481,14 @@ lets the two components vary independently, Lean proves equality:
 |im(Cq , Cd )| = |im(Cq )||im(Cd )|.
 Image-level pair rules therefore have size
 |A||im(Cq )||im(Cd )|
-for finite label type A.
+for finite label type A. This exact product-image equality is a theorem about the full formal product
+domain Ωq × Ωd . A logged candidate graph, prefiltered trace, or finite benchmark subset need not
+realize every independent query/document pair; such restricted empirical surfaces should be treated
+as their own finite observed images.
 Finite pair samples get the corresponding falsifier:
-ProductSampleConsistent productSampleConsistent_of_ruleFactorsThrough
+
+ProductSampleConsistent productSampleConsistent_iff_sampleConsistent_productMap
+productSampleConsistent_of_ruleFactorsThrough
 productSampleConsistent_iff_exists_productRuleFitsSample
 no_productQuotientTarget_of_sample_collision
 
@@ -486,7 +510,8 @@ ProductSampleConsistent.prod_iff
 Thus a combined pipeline target factors through the product quotient exactly when each component
 target does.
 Ranking comparisons are handled by a three-field comparison observation:
-ComparisonObs comparisonMap ComparisonFiberInvariant
+ComparisonObs comparisonObsEquivProd comparisonMap comparisonMap_eq_iff
+ComparisonFiberInvariant ruleFactorsThrough_comparison_fiberInvariant
 rankByScore rankByScore_factorsThrough_of_score_factorsThrough
 
 If a pairwise score factors through the query/document product quotient, then the score-induced
@@ -495,7 +520,6 @@ corresponding query/document/document comparison quotient. This proves a conditi
 from preserved pairwise scores to preserved pairwise ranking decisions; it does not prove top-k
 equality without separate tie or margin assumptions. The reachable comparison-code haystack is
 exactly one left image and two right images:
-
 ComparisonImageBox comparisonMap_image_subset_imageBox
 comparisonMap_image_eq_imageBox
 comparisonMap_image_card_eq_product_images_card
@@ -510,12 +534,14 @@ Thus comparison-level rules have size
 again for finite A.
 FinitePairQuotient.lean remains as a retrieval-facing wrapper around the generic product
 API:
-pairQuotient_eq_iff pairRuleFactorsThrough_same_on_quotient_fibers
+pairQuotient pairQuotient_eq_iff pairRuleFactorsThrough_same_on_quotient_fibers
 no_pair_compatible_target_of_sample_collision
 
 QuotientRefinementKernel.lean gives the kernel view of refinement. Finer quotients have
 smaller kernels; coarser quotients have larger fibers. For a surjective fine quotient, refinement is
 equivalent to kernel inclusion:
+
+
 quotientRefines_kernel_subset
 quotientRefines_of_surjective_of_kernel_subset
 quotientRefines_iff_kernel_subset_of_surjective
@@ -555,13 +581,12 @@ windowMap
 
 ObservationFamilyAgreement
 
+WindowAgreement
+
 with kernel characterizations
 kernel_observationFamilyMap_iff
 kernel_windowMap_iff
 
-
-WindowAgreement
-
 Theorem 7.1 (Window target factorization). For finite Ω, a target y : Ω → A factors through the
 reachable image quotient of Wk if and only if agreement on every coordinate in the window implies
 equal target behavior:
@@ -583,6 +608,7 @@ by the task target.
 Longer windows are monotone refinements of shorter windows. If m ≤ n, then Wn refines Wm ,
 so adding observations can split buckets or leave them unchanged, but it cannot merge points
 already separated by the shorter window:
+
 windowMap_refines_of_le
 windowMap_kernel_subset_of_le
 windowTargetInvariant_of_le
@@ -613,7 +639,6 @@ Score Margins and Profile Stability
 The formalization does not try to prove that contrastive training or any particular encoder architecture automatically implies ordinal or bitmap invariance. Instead, ScoreMarginQuotient.lean
 proves a sufficient condition for threshold decisions to survive quotient approximation.
 
-
 8.1
 
 Margin-stable threshold admission
@@ -639,6 +664,8 @@ Theorem 8.1 (Margin-stable threshold equality). If s̃ is within ε of s, and ev
 decision margin around τ exceeds ε, then thresholding s̃ gives exactly the same Boolean decisions as
 thresholding s.
 The checked names are:
+
+
 threshold_admit_iff_of_scoresWithin_and_margin
 thresholdAdmitBool_eq_of_scoresWithin_and_margin
 thresholdAdmitBool_factorsThrough_of_score_factorsThrough
@@ -673,7 +700,6 @@ does not define how to estimate those certificates, does not introduce a manifes
 not claim that any real encoder satisfies them globally.
 
 
-
 Ordered Evidence and Threshold Rules
 
 The quotient-search, image-kernel, and profile-stability layers are structural. The decision-theoretic
@@ -691,6 +717,7 @@ than every deterministic full-space rule.
 This is checked by:
 exists_orderedQuotientThreshold_finiteWeightedRisk_le_of_orderedEvidenceFactor
 
+
 It rests on two lower layers: MLR.lean, which proves that monotone likelihood ratio makes Bayes
 admission monotone, and FiniteDecision.lean, which proves that a monotone predicate on a
 finite ordered support is represented by a threshold cut. The use of monotone likelihood ratios as a
@@ -738,6 +765,7 @@ OverlapSufficiency.lean specializes ordered threshold sets to actual overlap coo
 with overlapQuotientThresholdSet_eq_orderedQuotientThresholdSet identifying the overlap
 threshold set with the ordered threshold set. The Bayes-risk wrappers in OverlapBayesOptimal.
 lean expose this as
+
 exists_overlapQuotientThreshold_finiteBayesRisk_le_of_canonicalTilt
 exists_overlapQuotientThreshold_finiteBayesRisk_le_of_canonicalTilt_of_lt
 exists_overlapQuotientThreshold_finiteCostedBayesRisk_le_of_canonicalTilt
@@ -765,7 +793,6 @@ The content is:
 • Query-stabilizer permutations preserve literal overlap with the query.
 • Among bitmaps of the same cardinality, equal query overlap is equivalent to being in the same
 query-stabilizer orbit.
-
 • Any statistic on the constant-weight bitmap space that is invariant under those query-stabilizer
 symmetries factors through literal overlap.
 This is a symmetry theorem, not an encoder theorem. It says that if the bitmap problem is
@@ -786,6 +813,7 @@ Under the uniform law on BD,K , the event
 {d : |q ∩ d| ≥ t}
 has the hypergeometric upper-tail mass obtained by summing inside/outside choices. Lean proves
 the supporting cardinality and probability identities:
+
 card_bitmapOverlapFiber_of_query_card
 bitmapHypergeomMass_eq_insideOutsideChoices_card_ratio
 bitmapHypergeomMass_eq_overlapFiber_card_ratio
@@ -811,7 +839,6 @@ the signal law be the finite exponential tilt of that uniform law by literal que
 1. the literal overlap-tail rule
 {d ∈ BD,K : |q ∩ d| ≥ t}
 has Bayes risk no larger than any deterministic admission rule R ⊆ BD,K ;
-
 2. the uniform bitmap null mass of that same tail event is exactly the checked hypergeometric
 upper-tail value.
 The cost-sensitive version is
@@ -836,6 +863,7 @@ exponentialTilt_hasMLR_of_lt
 
 FNCH.lean connects actual-overlap FNCH weights to the shifted exponential-tilt implementation
 after normalization, and exposes threshold optimality statements such as
+
 fnch_bayesAdmit_isActualOverlapThreshold
 fnch_actualOverlapThreshold_bayesRisk_optimal
 fnch_costed_actualOverlapThreshold_bayesRisk_optimal
@@ -858,7 +886,6 @@ How This Narrows Empirical Search
 The formalization does not measure real embedding coordinates. It does, however, give a precise
 checklist for what empirical probes are trying to refute or constrain.
 
-
 16.1
 
 What must hold if the contract is true
@@ -891,6 +918,7 @@ Observed buckets are then fixed; reachable unobserved image buckets remain free.
 finite version space is not arbitrary, but it is also not collapsed to a single global truth unless every
 relevant bucket has been observed or additional structure is imposed.
 
+
 16.3
 
 What gets reduced
@@ -899,6 +927,16 @@ Without the quotient, a finite target search ranges over |A||Ω| functions. Wit
 compatible targets are represented by bucket-level functions. If m reachable quotient buckets
 remain unobserved, Boolean extrapolations have size 2m . This is exactly the “smaller finite set of
 extrapolations” established by the Lean search layer.
+For pairwise retrieval targets, the haystack is not a document-only bucket space. It is the
+reachable product image of compressed query and document codes. On the full formal product
+domain this has size |im(Cq )||im(Cd )|, and comparison/ranking targets live over the one-query/twodocument image box of size |im(Cq )||im(Cd )|2 . On a finite logged sample or prefiltered trace, the
+observed image may be smaller, and the same finite-bucket logic applies to that restricted surface.
+For probe families, the reduction is by the realized joint-code image. The point is not that each
+bitmap, ordinal, lexical, query-transform, or context-window probe is injective by itself. The finite
+question is whether agreement on the whole joint code preserves the target behavior being audited.
+For score-threshold decisions, the margin/profile layer gives a different kind of reduction: supplied
+finite error and margin certificates can turn an approximate quotient score into an exact thresholddecision certificate. Near the decision boundary, this requires explicit margin evidence; absent that
+evidence, the theorem intentionally does not certify equality.
 
 16.4
 
@@ -913,7 +951,6 @@ then some overlap-tail cutoff is Bayes-optimal and has a hypergeometric null tai
 work can look for formal violations of the quotient, monotonicity, margin, and calibration contracts,
 or collect finite sample evidence consistent with them. Lean proves the consequences of the contracts,
 not that real encoders satisfy them.
-
 The observation-window layer lets these probes be combined. Several bitmap, ordinal, lexical,
 query-transform, or context-window views can be treated as a single joint code. Production-style
 falsification then checks whether same-joint-code examples ever disagree on the target, rather than
@@ -927,6 +964,7 @@ The formalization intentionally excludes several stronger statements.
 or overlap quotient.
 • It does not prove that same quotient value means same full embedding geometry.
 • It does not prove representation completeness.
+
 • It does not prove empirical calibration or real-corpus null adequacy.
 • It does not prove that the textbook hypergeometric distribution is the deployment null for
 real embeddings.
@@ -936,6 +974,15 @@ globally satisfy the supplied profile assumptions.
 • It does not prove that any concrete family of production probes is globally target-sufficient.
 The window layer proves the finite kernel calculus for such probe families once the observations
 and target are fixed.
+• It does not prove top-k list equality, tie-policy preservation, or nDCG preservation from
+the ranking-comparison theorem alone. Those require additional ordering, tie, or margin
+assumptions.
+• It does not let product-image equalities for the full formal product domain be read as claims
+about arbitrary logged candidate graphs or prefiltered empirical traces.
+• It does not certify near-threshold score decisions unless the supplied score-error and margin
+hypotheses exclude those near ties.
+• It does not prove a continuous Takens-style embedding theorem. The observation-window
+layer is a finite-domain target-separation calculus.
 • It does not include randomized tests, Neyman–Pearson optimality, uniformly most powerful
 tests, Karlin–Rubin theory, asymptotics, or measure-theoretic probability.
 These exclusions are not weaknesses in the formal theorem. They are the boundary that makes
@@ -951,12 +998,11 @@ make verify
 make check-doc-names
 make audit
 make lint
-
-
 The expected axiom baseline printed by the verification surface is:
 [propext, Classical.choice, Quot.sound].
-The root import file and public verification dashboard cover these main modules and support
-layers:
+The root import file covers the main modules directly, and the public verification dashboard
+also checks their lower support layers:
+
 FiniteExperiment FiniteQuotientSearch QuotientConstraints FiniteQuotientImage
 QuotientKernel
 FiniteFiberTopology FiniteProductQuotient FinitePairQuotient
@@ -970,7 +1016,7 @@ BayesThreshold ExponentialTilt FNCH
 
 Conclusion
 
-The Lean development proves a finite theorem stack with two complementary messages.
+The Lean development proves a finite theorem stack with three complementary messages.
 First, if the Bayes-relevant evidence for a binary admission task factors through a quotient, then
 quotient-form admission can be globally optimal. In the bitmap specialization, under the canonical
 overlap-tilt signal model and uniform constant-weight bitmap null, this optimal quotient-form rule
@@ -979,6 +1025,11 @@ Second, the quotient contract is structurally strong. It forces fiber invariance
 same-bucket falsifiers, bounds compatible target search by quotient-bucket assignments, and shows
 exactly where finite samples leave unobserved extrapolation freedom. It narrows the field of possible
 global structures without pretending to identify real encoders automatically.
+Third, the same contract composes into retrieval-facing structures. Product quotients express pairwise query/document targets and multi-target signatures; comparison quotients express
+score-induced ranking decisions; observation windows express finite bundles of lossy probes; and
+margin/profile theorems turn supplied finite score certificates into exact threshold-decision consequences. These layers do not remove the empirical burden. They specify what must be tested:
+which compressed buckets, product codes, joint probe codes, and near-boundary margins would
+falsify or support the claimed quotient contract.
 
 References
 [1] R. A. Fisher. On the mathematical foundations of theoretical statistics. Philosophical Transactions of the Royal Society of London. Series A, Containing Papers of a Mathematical or Physical
@@ -993,10 +1044,11 @@ Sons, New York, 1950.
 [5] Samuel Karlin and Herman Rubin. The Theory of Decision Procedures for Distributions with
 Monotone Likelihood Ratio. The Annals of Mathematical Statistics, 27(2):272–299, June 1956.
 DOI: https://doi.org/10.1214/aoms/1177728259.
+
+
 [6] Luc Devroye, László Györfi, and Gábor Lugosi. A Probabilistic Theory of Pattern Recognition.
 Stochastic Modelling and Applied Probability, volume 31. Springer New York, 1996. DOI:
 https://doi.org/10.1007/978-1-4612-0711-5.
-
 [7] Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming
 Language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction – CADE 28,
 Lecture Notes in Computer Science, volume 12699, pages 625–635. Springer, Cham, 2021. DOI:
diff --git a/docs/rag-pipeline-guide.md b/docs/rag-pipeline-guide.md
index b8a0afe..c84658c 100644
--- a/docs/rag-pipeline-guide.md
+++ b/docs/rag-pipeline-guide.md
@@ -22,7 +22,10 @@ admission adds a different kind of gate: represent each item by a fixed-size
 ordinal or bitmap signature, then admit candidates whose query overlap clears a
 cutoff.
 
-The proof is about that gate.
+The bitmap theorem is about that gate. The broader quotient stack also gives
+finite contracts for product query/document behavior, multi-target signatures,
+finite bundles of lossy probes, and score-threshold decisions under supplied
+margin/profile certificates.
 
 ## Worked Example
 
@@ -103,7 +106,10 @@ assumptions. In particular, it does not prove:
 - ordinal signatures contain all semantic information;
 - a real corpus has the uniform constant-weight null;
 - every query type has monotone relevance as overlap increases;
-- a popcount gate replaces reranking, hybrid search, or evaluation.
+- a popcount gate replaces reranking, hybrid search, or evaluation;
+- pairwise ranking-comparison preservation by itself guarantees top-k list
+  equality, tie-policy preservation, or nDCG preservation;
+- near-threshold score decisions are safe without explicit margin evidence.
 
 The formal result is a conditional guarantee. Your benchmark harness still has
 to test whether the condition is credible for your encoder, corpus, and query
@@ -127,6 +133,10 @@ score-induced ordering comparison. A fixed query can look document-only, but the
 global contract is stronger because queries with the same compressed query code
 must induce the same quotient-level document behavior.
 
+Product-image equalities in the Lean stack are theorems about the full formal
+product domain. A logged candidate graph, prefiltered trace, or benchmark slice
+may realize only a smaller observed image; audit that restricted image directly.
+
 ## Why This Matters In A Real RAG System
 
 The useful real-world reading is not "Lean proves my retrieval stack works."
diff --git a/docs/reviewer-brief.md b/docs/reviewer-brief.md
index d849bcd..7bba00e 100644
--- a/docs/reviewer-brief.md
+++ b/docs/reviewer-brief.md
@@ -7,6 +7,17 @@ finite assumptions hold.
 For a developer-facing version of the same result in vector DB and RAG terms,
 see [`rag-pipeline-guide.md`](rag-pipeline-guide.md).
 
+## Full Quotient Stack
+
+The bitmap theorem is the clearest end-to-end specialization, but the checked
+Lean stack is broader. It also formalizes finite quotient search constraints,
+reachable-image/kernel containment, fiber topology, product quotients for
+query/document targets, score-induced ranking comparisons, componentwise
+multi-target signatures, finite observation windows for bundles of lossy
+probes, and margin/profile certificates for threshold decisions. These layers
+do not assert that a real encoder satisfies the contracts; they state what
+follows if finite observations, labels, scores, and margins support them.
+
 ## The Claim
 
 The checked theorem is:
@@ -179,6 +190,11 @@ The expected axiom baseline is:
 - Pairwise retrieval, ranking, and multi-target pipeline decisions are not
   proved preserved unless the corresponding product quotient contract is
   empirically supported.
+- Ranking-comparison preservation alone does not guarantee top-k equality,
+  tie-policy preservation, or nDCG preservation.
+- Product-image equalities are theorems about the full formal product domain,
+  not arbitrary prefiltered traces or logged candidate graphs.
+- Near-threshold score decisions require explicit margin evidence.
 - Real encoders are not proved to satisfy the query-stabilizer symmetry
   assumption; the symmetry theorem identifies the canonical invariant when that
   assumption is appropriate.
diff --git a/docs/theorem-map.md b/docs/theorem-map.md
index 3f8240a..84e8d30 100644
--- a/docs/theorem-map.md
+++ b/docs/theorem-map.md
@@ -75,6 +75,8 @@ OrdvecFormalization.invariantOn_constantWeightBitmapSpace_factorsThrough_overlap
 Finite quotient search layer:
 
 ```lean
+OrdvecFormalization.quotientPullback
+OrdvecFormalization.RuleFactorsThrough
 OrdvecFormalization.QuotientCompatible
 OrdvecFormalization.ObservedQuotients
 OrdvecFormalization.ObservedQuotientsList
@@ -248,6 +250,11 @@ 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:
@@ -305,6 +312,8 @@ names.
 Public Lean names:
 
 - `finiteWeightedBayesAdmitSet_optimal`
+- `quotientPullback`
+- `RuleFactorsThrough`
 - `mem_quotientPullback_of_quotient_preserving`
 - `QuotientCompatible`
 - `ObservedQuotients`
@@ -536,6 +545,7 @@ Public Lean names:
 - `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`
@@ -544,6 +554,10 @@ Public Lean names:
 - `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`