AssignmentConstraints
plain-language theorem explainer
Packages four integer identities that any admissible sector yardstick assignment must obey: up–EW sign duality of B_pow, lepton–EW absolute complement equaling down-quark B_pow, W-multipliers summing to the 3-cube vertex count, and additive r₀ corrections summing to the passive-edge count. Cited by anyone checking that a proposed (B_pow, r₀) table is combinatorially legal. Pure structure definition; no proof body.
Claim. An assignment of sector yardstick exponents is constrained by four equalities: $B_{\mathrm{pow}}(\mathrm{up})= -B_{\mathrm{pow}}(\mathrm{EW})$; $|B_{\mathrm{pow}}(\mathrm{lepton})|+|B_{\mathrm{pow}}(\mathrm{EW})|=B_{\mathrm{pow}}(\mathrm{down})$; the wallpaper multipliers satisfy $4+2+(-1)+3=2^{D}$ with $D=3$; and the additive $r_0$ corrections satisfy $(-6)+1+12+4=11$.
background
Open Problem O1 asks why each particle sector receives a specific binary power $B_{\mathrm{pow}}$ and offset $r_0$ from the counting layer. The module’s answer is a sector–cube coupling principle: leptons, up quarks, down quarks, and the electroweak sector each couple to a distinct level of the 3-cube hierarchy (passive edges, active edge, total edges, active edge again).
Combinatorial constants are fixed upstream. Spatial dimension is $D=3$ (T8), so the hypercube has $V=2^D=8$ vertices. Passive edges number $E_p=11$; the active-edge bit is $A=1$; total edges $E=12$. The wallpaper constant is $W=17$. Concrete formulas in the module table are $B_{\mathrm{pow}}\in{-22,-1,23,+1}$ and $r_0\in{62,35,-5,55}$.
The structure records only the cross-sector identities (C2)–(C5) that any such table must satisfy. (C1), that $B_{\mathrm{pow}}$ is built from ${E_p,A,E}$ alone, is stated in the doc-comment but not reified as a field.
proof idea
No proof: this is a structure bundling four Prop fields. Inhabitation is supplied downstream by assignment_valid, which fills the fields with the named lemmas up_ew_sign_duality, lepton_ew_complement_down, depths_exhaust_vertices, and additive_corrections_sum_to_Ep. Those lemmas are ordinary integer arithmetic on the fixed constants $A$, $E_p$, $E$, $W$, and $2^D$.
why it matters
This is the constraint interface for the Yardstick Assignment Principle (O1). Downstream, assignment_valid is the witness that the current four-sector table meets every listed identity, so the assignment is not an ad-hoc fit but a point in a sharply restricted combinatorial space.
The vertex-exhaustion field ties the $r_0$ wallpaper multipliers ${4,2,-1,3}$ directly to $V=8=2^D$ with $D=3$ from the forcing chain (T8). Edge exhaustion ties the additive corrections to the passive-edge count $E_p=11$. Sign duality and the absolute complement encode the module’s structural observation that binary shifts measure how much each sector’s recognition boundary borrows from the cube edge network.
Together with the distinct-yardstick requirement noted in the doc-comment, these constraints are what make O1 falsifiable rather than purely narrative: a rival assignment must still hit the same four equalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.