Track encoder-as-quotient composition layer and paper correction

[Fieldnote-Echo]

Motivation

We should correct the formal/narrative framing around neural embeddings. The current quotient machinery is sound, but the paper and theorem surface can read as if the neural embedding is a complete observation space Ω. In practice, an encoder is itself a quotient/statistic of a chosen finite experimental universe.

The intended pipeline is:

Ωraw --E--> Xembedding --Q--> Zquotient
C = Q ∘ E

So the right contract is:

target factors through Q ∘ E

not:

embedding coordinates are a complete Ω

Lean work

Add a small module, likely EncoderQuotientComposition.lean or QuotientPipeline.lean, that explicitly names the two-layer structure while reusing the existing generic machinery.

Candidate theorem targets:

• Define/abbrev composed compression:

composedQuotient E Q := Q ∘ E

• Later quotients only forget more:

Kernel E ⊆ Kernel (Q ∘ E)

• Final quotient sufficiency implies encoder-level sufficiency:

target factors through image quotient of Q ∘ E
  -> target factors through image quotient of E

or equivalently via kernels:

Kernel (Q ∘ E) ⊆ TargetKernel target
  -> Kernel E ⊆ TargetKernel target

• Image-size/search narrowing:

|im(Q ∘ E)| ≤ |im(E)|

• Optional n-layer formulation if useful, but avoid recursive overengineering: quotient chains collapse by composition.

Paper/doc work

Update docs/paper/ordvec_formalization_paper.tex and supporting docs to state:

• Ω is the finite experimental universe under discussion, not all semantic reality.
• A neural embedding is already a quotient/statistic of that chosen universe.
• OrdVec/bitmap/ordinal compression is a downstream quotient of the encoder image.
• Empirical bitmap probes test invariance of the composite map from finite probes through the real encoder into the quotient.
• The hierarchy is finite:

raw/probe finite universe
-> encoder image
-> OrdVec reachable image quotient
-> observed buckets

Boundary

Avoid "turtles all the way down" by making the domain boundary explicit:

Ω = the finite experimental universe for the claim being tested

For bitmap probes, Ω may be the finite set of generated probe images. For corpus tests, Ω may be the finite corpus/query-pair sample. Once that boundary is fixed, all downstream maps compose into one compression map, and the existing kernel/image quotient theorems apply.

This should sharpen the empirical contract without weakening the current formalization.