assignment_valid
plain-language theorem explainer
The four-sector yardstick assignment (lepton, up, down, electroweak) meets every cube-partition constraint: active-edge sign duality, lepton–EW complement equaling down-quark B_pow, W-multipliers summing to eight vertices, and r₀ additive corrections exhausting eleven passive edges. Cite it as the packaged admissibility witness for the O1 formulas. It is a structure instance that wires four already-proved identities into AssignmentConstraints.
Claim. The sector yardstick assignment satisfies the cube-partition constraints: $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 $r_0$ wallpaper multipliers obey $4+2+(-1)+3=V=8$; and the additive $r_0$ corrections obey $-6+1+12+4=E_p=11$.
background
Open Problem O1 asks why each particle sector receives a definite $B_{\mathrm{pow}}$ and $r_0$ from the counting layer. The module’s answer is a sector–cube coupling principle: leptons couple to passive edges ($B_{\mathrm{pow}}=-2E_p=-22$, $r_0=4W-6=62$), up quarks and electroweak to the active edge ($\pm A=\pm 1$), and down quarks to total edges ($2E-1=23$). Here $W=17$ (wallpaper groups), $E=12$, $E_p=11$, $A=1$, and $V=8$ (cube vertices in $D=3$).
AssignmentConstraints packages five structural filters on any candidate assignment. The two used here as nontrivial equalities are C2 (up–EW sign duality of the active edge) and C3 (lepton–EW magnitudes sum to down-quark $B_{\mathrm{pow}}$). C4 and C5 are pure integer exhaustions: W-multipliers ${4,2,-1,3}$ sum to $V=8$, and additive $r_0$ corrections ${-6,1,12,4}$ sum to $E_p=11$.
Sibling lemmas already establish the numerical identities (lepton_ew_complement_down, up_ew_sign_duality, depth and additive-sum facts). This definition only records that the current formulas inhabit the constraint structure.
proof idea
Pure structure construction, not a tactic proof. Each field of AssignmentConstraints is filled by a named sibling identity:
sign_duality←up_ew_sign_duality(C2: $B_{\mathrm{pow}}(\mathrm{up})=-B_{\mathrm{pow}}(\mathrm{EW})$),complement←lepton_ew_complement_down(C3: $|B_{\mathrm{pow}}(\mathrm{lepton})|+|B_{\mathrm{pow}}(\mathrm{EW})|=B_{\mathrm{pow}}(\mathrm{down})$),vertex_exhaustion←depths_exhaust_vertices(C4: $4+2+(-1)+3=V$),edge_exhaustion←additive_corrections_sum_to_Ep(C5: $-6+1+12+4=E_p$).
No new algebra is performed; the def is the witness bundle that those four lemmas jointly satisfy the constraint interface.
why it matters
O1 is the gap between combinatorial cube counts and the concrete sector yardsticks that enter the mass ladder (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). This definition is the module’s closure certificate that the tabulated assignment is constraint-admissible, not an ad hoc fit.
The in-file status note places uniqueness and canonical forcing in Verification.YardstickAssignmentChoiceSet, via unrestricted forcing theorems built on these principle lemmas (yardstick_filter_family_forced_from_cube_partition_principle, yardstick_assignment_forced_from_cube_partition_principle). Together the two modules claim O1 closed.
Framework landmarks in view: $D=3$ (T8) supplies the 3-cube whose $V=8$ vertices match the eight-tick octave (T7); the passive/active edge split ($E_p=11$, $A=1$) is the same counting layer that feeds $\alpha$ calibration. No downstream Lean edge is recorded yet; the intended consumer is the choice-set forcing package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.