claimroutineinferred_dep

Fresh isomorphisms make genericity typical

Fresh isomorphisms make the next domain nongeneric with probability ≤ ε0\varepsilon_0
feeds the per-level rank-drop bound
Claim·§3.4 Linear lifts and loss of rank·inside propFull lifts detect the leaf symbol

Statement (paper)

For every j≥0j\ge0, conditional on Fj\mathcal F_j and AjA_j, the next domain Sj+1=Jj∗Ej,AjS_{j+1}=J_j^*E_{j,A_j} is a uniformly random subspace of B∗B^* of the fixed rank rj+1=dim⁡Ej,Ajr_{j+1}=\dim E_{j,A_j}, so that, with BjB_j the indicator that rj>0r_j>0 and SjS_j is nongeneric, E[Bj+1∣Fj,Aj]≤ε0\E[B_{j+1}\mid\mathcal F_j,A_j]\le\eps_0.

In plain English

Conditional on the history Fj\mathcal F_j and the chosen child AjA_j, the next domain Sj+1=Jj∗Ej,AjS_{j+1}=J_j^*E_{j,A_j} is a uniformly random subspace of B∗B^* of fixed rank rj+1=dim⁡Ej,Ajr_{j+1}=\dim E_{j,A_j}. Hence the chance that Sj+1S_{j+1} is nongeneric with positive rank is at most ε0\eps_0, i.e. E[Bj+1∣Fj,Aj]≤ε0\E[B_{j+1}\mid\mathcal F_j,A_j]\le\eps_0.

Why it's here

The subspace Ej,AjE_{j,A_j} is determined by the history and the child, while the child's isomorphism JjJ_j is fresh randomness, so applying Jj∗J_j^* randomizes the subspace uniformly. The random-subspace genericity lemma then bounds the probability of nongeneric Sj+1S_{j+1} by ε0\eps_0, and this feeds the per-level expected rank-drop bound that uses it.
Classified routine:
Follows directly from the fact that a uniformly random linear isomorphism maps a fixed subspace to a uniformly random subspace of the same rank, combined with the earlier random-subspace genericity lemma (lem-latent-generic).

Uses

lemRandom binary subspaces are genericlemChild characters factor through a common latent map

Used by

claimExpected harmonic rank drop per level

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Fresh isomorphisms make genericity typical" rests on lem:latent-generic
  • info
    inferred_dep
    outline: "Fresh isomorphisms make genericity typical" rests on lem:latent-lift-factorization