b3HalfOrder
plain-language theorem explainer
b3HalfOrder defines the natural number 48/2. Physicists matching SU(5) generator counts to the half-order of B3 in Recognition Science GUT models cite this value when certifying unification at the GUT scale. The definition is a direct arithmetic computation with no lemmas or hypotheses.
Claim. Define the half-order quantity $b_{3/2} := 48/2$ in the natural numbers.
background
The module treats grand unification in Recognition Science, where the GUT group rank equals 6 for the Standard Model factors or 5 for SU(5). SU(5) generators are given by $5^2 - 1 = 24$, set equal to $|B_3|/2$. This definition supplies the concrete integer for that half-order by evaluating 48/2. No upstream results are required; the declaration is foundational within the module.
proof idea
One-line definition that evaluates the arithmetic expression 48 divided by 2.
why it matters
The definition supplies the integer 24 that appears in GUTCert to equate su5GeneratorCount with b3HalfOrder and in the theorems b3Half_eq_24 and su5_matches_b3half. It fills the numerical anchor for the statement that five canonical GUT models (SU(5), SO(10), E6, flipped SU(5), trinification) align with configDim D = 5 at the GUT scale where forces unify. It touches the RS claim that SU(5) rank equals D + 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.