Q_tilde_up
plain-language theorem explainer
Integerized electric charge of the up quark on the recognition boundary: six times the SM value 2/3, hence 4. Used throughout the Z-map derivation as the bare charge coordinate for up-type quarks. Pure definitional constant; no proof content.
Claim. The face-count integerized charge of the up quark is $\tilde{Q}_{\mathrm{up}} := 6 \cdot (2/3) = 4 \in \mathbb{Z}$.
background
The module derives the charge-to-band polynomial $Z(\tilde{Q})$ from recognition topology on the 3-cube, without empirical mass anchors. Stage 1 fixes the integerization scale: a boundary of charge $Q$ couples to the $F = 2D$ faces of the cube. At $D = 3$ one has $F = 6$, and 6 is the least positive even integer sending every SM charge ${-1, 2/3, -1/3}$ into $\mathbb{Z}$ (ledger $\delta$-units $\simeq \mathbb{Z}$, T8).
For the up quark, $Q = +2/3$, so the integerized coordinate is $\tilde{Q} = FQ = 6 \cdot (2/3) = 4$. Parallel constants exist for the lepton ($\tilde{Q} = -6$) and down quark ($\tilde{Q} = -2$). The upstream species label up only records cosmological DOF; it is not used in the arithmetic here.
proof idea
Definitional abbreviation: the body is the integer literal 4, justified by the comment $6 \times (2/3)$. No tactics or lemmas.
why it matters
Feeds every concrete Z-evaluation in the module. Bare polynomial values use it to obtain $Z_{\mathrm{up}}(1,1) = 16 + 256 = 272$; with color offset $c = 4$ one gets the full anchor 276. Downstream uniqueness theorems (coefficients_forced_from_quark_bare_anchors, full_anchor_tuple_forces_coefficients_and_offset) treat 272 and 276 as the up anchors that force $(a,b) = (1,1)$ and $c = 4$. Hierarchy and separation lemmas (canonical_ordered, canonical_separates) likewise substitute this constant. Ties Stage 1 face-count integerization ($F = 6$ at $D = 3$, T8) to the Stage 2/3 polynomial $Z = a\tilde{Q}^2 + b\tilde{Q}^4$ plus quark offset $2^{D-1} = 4$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.