stringCompactificationCert
plain-language theorem explainer
stringCompactificationCert assembles a certificate that string compactification proceeds from 10 to 4 dimensions with exactly five families and six internal directions partitioned as the B3 rank sum 3+2+1. Physicists deriving extra dimensions from Recognition Science would cite it to confirm the reduction matches the color, weak, and hypercharge axes. The definition is built by direct field assignment from three decide lemmas that compute the relevant cardinalities and equalities.
Claim. A structure $C$ such that the number of compactification families is 5, $10-4=6$ internal dimensions, and $6=3+2+1$ (the rank sum of $B_3$).
background
The module derives string compactification from RS by observing that reduction from 10 to 4 macroscopic dimensions removes 6 internal directions. In the RS framing these 6 directions equal 3 colour axes + 2 weak axes + 1 hypercharge, which is the rank sum of $B_3$. Five canonical families are listed: Calabi-Yau, torus, orbifold, warped (RS1/RS2), and brane-world.
proof idea
The definition constructs the StringCompactificationCert structure by assigning its three fields directly to the results of compactFamily_count, ten_minus_four, and six_eq_rank_sum. Each upstream result is a theorem proved by the decide tactic.
why it matters
This definition supplies a concrete certificate linking RS compactification to the standard 10D string-theory reduction and the B3 rank sum. It populates the Physics.StringCompactificationFromRS module that extracts dimensional facts from the forcing chain. No downstream theorems yet reference it, but it supports the claim that RS yields the observed macroscopic dimension count together with the internal partition 3+2+1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.