Z_index
plain-language theorem explainer
The abbreviation introduces the charge index as the integer map from the anchor relation, supplying the Z input to the gap term in the phi-ladder mass formula. Mass-spectrum modelers cite it when converting species charges to rung offsets. The definition is a direct alias to the upstream integer map with no additional steps.
Claim. $Z_{index} := Z$, where $Z$ is the integer map that assigns $Q_6^2 + Q_6^4$ to leptons and $4 + Q_6^2 + Q_6^4$ to quarks for charge $Q_6 = 6Q$.
background
In the masses anchor-policy module the integer map Z converts rational charges into the index used by the gap function on the phi-ladder. The upstream Anchor.Z definition computes this map sector-by-sector: for leptons it returns $Q_6^2 + Q_6^4$; for up and down quarks it returns $4 + Q_6^2 + Q_6^4$, with $Q_6 = 6Q$. The companion upstream Z for Species simply forwards to ZOf f, confirming the integer output convention. This supplies the local notation for the mass formula yardstick times phi to the power (rung minus 8 plus gap of Z).
proof idea
The declaration is a one-line abbreviation that directly aliases the charge index to the upstream integer map Z.
why it matters
The abbreviation supplies the Z argument required by the gap function inside the mass formula, thereby linking charge data to rung positions on the phi-ladder. It supports the anchor-policy layer that feeds predict_mass and related siblings, consistent with the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain. No downstream uses are recorded, so the definition remains a local interface rather than a theorem with parents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.