lemmaroutine

Child characters factor through a common latent map

Child characters of a lift factor through one shared linear map γ\gamma
shows children share γ\gamma, enabling the fresh-isomorphism step
Lemma·lem:latent-lift-factorization·§3.4 Linear lifts and loss of rank

Statement (paper)

Let a lift with domain SS be given on PtP_t, where t≥1t\ge1. For each child (A,J)(A,J), restriction to that child's shift space factors through λt−1\lambda_{t-1}. The resulting characters on the child output space BB have the form ϕAJ(z)=J∗((γz,z)∣UA)∈B∗, \phi_{AJ}(z)=J^*\bigl((\gamma_z,z)|_{U_A}\bigr)\in B^*, where γ:S→X∗\gamma:S\to X^* is a single binary linear map common to all the children.

In plain English

For a lift with domain SS on PtP_t with t≥1t\ge1, restricting to each child's shift space factors through λt−1\lambda_{t-1}. The resulting characters on the child output space BB are ϕAJ(z)=J∗((γz,z)∣UA)\phi_{AJ}(z)=J^*((\gamma_z,z)|_{U_A}), where γ:S→X∗\gamma:S\to X^* is one binary linear map shared by all children.

Why it's here

This lemma shows that all the children's characters are governed by a single linear map γ\gamma and differ only through the child data (A,J)(A,J). That common structure lets later arguments, such as the genericity claim for fresh isomorphisms, treat the next domain J∗EJ^*E as determined by γ\gamma and the random child, rather than by separate data for each child.
Classified routine:
A structural bookkeeping step about the paper's own recursive lift construction. It writes the restricted characters through one shared linear map, using only linear algebra on the child shift spaces.

Uses

Nothing else in the paper

Used by

claimFresh isomorphisms make genericity typical

Sources

PaperOpen
Section
§3.4 Linear lifts and loss of rank
Page
—
Label
lem:latent-lift-factorization
Line
sections/02-latent.tex:486
Leannot aligned

Phase 2 aligns this node to a Lean declaration.