available_ticks_boson
plain-language theorem explainer
Available boson ticks equal the full eight-tick octave period 2^D. Unification and g_star arithmetic use this as the bosonic side of the tick budget, opposite the fermionic dimension gap. The declaration is a one-line alias of the eight-tick constant already fixed by D.
Claim. The number of available recognition ticks for bosons is defined to be the full eight-tick period $2^{D}$.
background
The module records exact arithmetic identities that relate imported Standard Model degree-of-freedom counts to combinatorial quantities built from spatial dimension $D$. After external review it explicitly does not claim to derive the SM spectrum: gauge representations, Higgs content, and the Fermi/Bose thermal weights remain imported physics; only the kernel-checked re-expressions in $D$-flavored notation are proved here.
Upstream, $D$ is forced to 3 (T8 / DimensionForcing) and the fundamental cadence of the recognition operator is the eight-tick period $\mathrm{eightTick} := 2^D$ (T7). That period is the full discrete clock against which fermionic and bosonic tick budgets are compared. The sibling dimensionGap measures how many of those ticks are unavailable to fermions; bosons are assigned the complementary full budget.
TraceLogic.all appears only as a dependency edge for verifier bookkeeping and does not constrain the numeric value.
proof idea
One-line definitional alias: the value is set equal to eightTick, which itself is defined as $2^D$. No tactic proof or lemma application is required.
why it matters
In the Fermion DOF / dimension-gap bridge, bosons sit on the full eight-tick octave while fermions see a combinatorial gap. This constant is the bosonic half of that split and supplies the tick count that pairs with dimensionGap and the fermionic DOF identities (e.g. $90 = 2 \times \mathrm{dimensionGap}(3)$ and the assembled $g_\star = 106.75$ arithmetic).
Framework landmarks: T7 (eight-tick period $2^3$) and T8 ($D = 3$). The module status note is deliberate: these are exact re-expressions of already-known counts, not an RS derivation of the SM matter content. No downstream theorems currently depend on this name; it exists as the named bosonic counterpart inside the local identity suite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.