IndisputableMonolith.Verification.YardstickAssignmentChoiceSet
Enumerates the discrete choice set of sector B_pow yardstick assignments: canonical and orientation-mirrored maps, a finite value pool tied to Anchor formulas, sum-to-one targets, and structural versus principle constraints. Verification authors cite it when discharging Open Problem O1 (sector-to-cube coupling). The module is mostly definitions plus matching lemmas, not a deep existence proof.
claimThe module defines admissible $B_{\mathrm{pow}}$ yardstick assignments for particle sectors: a canonical assignment, its orientation-reflected counterpart (same magnitudes, flipped active-edge sign), the finite pool of $B_{\mathrm{pow}}$ values matching Anchor mass formulas, a sum target equal to $1$, and the structural and principle constraint sets inherited from the Yardstick Assignment Principle (sector $\leftrightarrow$ 3-cube coupling).
background
Recognition Science places sector masses on a $\varphi$-ladder with a sector yardstick prefactor. Open Problem O1 asks why each sector receives a definite $B_{\mathrm{pow}}$ (and $r_0$) from the counting layer rather than by fit. The Yardstick Assignment Principle answers by coupling each sector to a distinct combinatorial level of the 3-cube.
Upstream, Masses.Anchor centralises the parameter-free Model-layer constants from the mass manuscripts (no experimental-agreement claims). The principle module states the sector $\leftrightarrow$ cube coupling story. This module sits one step downstream: it turns that principle into an explicit finite choice set of $B_{\mathrm{pow}}$ assignments, including the orientation-reflected twin of the canonical map (same magnitudes, flipped active-edge sign).
Notation in-module: assignment types, a value pool, list-to-assignment coercion, an all-assignments enumerator, a sum target, and two constraint bundles (structural versus principle).
proof idea
Definition-and-matching module, not a single theorem. It introduces assignment types and the canonical versus mirrored $B_{\mathrm{pow}}$ maps; builds a finite value pool; proves the pool matches Anchor formula shapes; coerces lists into assignments and enumerates all candidates; defines a sum target and shows it equals one and agrees with the principle module; packages structural constraints and principle constraints as the filters on that choice set. Equalities are direct algebraic or list-level checks against Anchor and the principle imports.
why it matters in Recognition Science
Closes the choice-set side of Open Problem O1: once sectors couple to 3-cube levels, the admissible $B_{\mathrm{pow}}$ data must be a small, fully listed set with sum-one and Anchor-compatible values. Canonical and mirrored assignments make orientation symmetry explicit without enlarging magnitudes. Downstream used-by edges are empty in the current graph, so the module is a verification leaf: it supplies the concrete assignment universe that principle-level and mass-ladder arguments can quantify over. Ties to the RS mass formula (yardstick $\times \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) by pinning the yardstick exponents to a forced discrete pool rather than free parameters.
scope and limits
- Does not prove experimental mass agreement; Anchor is Model-layer only.
- Does not derive why the principle holds; it only packages the choice set.
- Does not fix unique physical orientation; canonical and mirrored are both listed.
- Does not construct r0 formulas beyond B_pow assignment data.
- Does not claim completeness outside the imported Anchor and principle interfaces.
depends on (2)
declarations in this module (80)
-
structure
BPowAssignment -
def
canonicalBPow -
def
mirroredBPow -
def
bPowValuePool -
theorem
bpow_pool_matches_anchor_formulas -
def
listToBPowAssignment -
def
allBPowAssignments -
def
bpowSumTarget -
theorem
bpow_sum_target_eq_one -
theorem
bpow_sum_target_matches_principle -
def
bpowStructuralConstraints -
def
bpowPrincipleConstraints -
def
validBPowAssignments -
theorem
all_bpow_assignments_count -
theorem
valid_bpow_assignment_count -
theorem
valid_bpow_assignments_are_singleton -
theorem
bpow_constraints_true_iff -
theorem
bpow_constraints_force_canonical -
theorem
bpow_principle_normal_form -
theorem
bpow_unrestricted_forcing_from_passive_coupling -
theorem
bpow_unrestricted_forcing_from_down_role -
theorem
bpow_lepton_forced_from_down_role_and_sign_sum -
theorem
bpow_lepton_role_iff_down_role_under_sign_sum -
theorem
bpow_sign_forced_from_lepton_down_sum -
theorem
bpow_principle_constraints_forced_from_edge_roles -
theorem
bpow_principle_constraints_forced_from_passive_active_roles -
theorem
bpow_bool_constraints_forced_from_edge_roles -
theorem
bpow_bool_constraints_forced_from_passive_active_roles -
theorem
bpow_unrestricted_forcing_from_edge_roles -
theorem
bpow_unrestricted_forcing_from_passive_active_roles -
theorem
bpow_unrestricted_forcing_from_passive_down_roles -
theorem
bpow_two_branch_under_down_role -
theorem
bpow_orientation_selects_canonical_from_two_branch -
theorem
bpow_orientation_selects_canonical_from_passive_down_roles -
theorem
bpow_principle_iff_active_unit_under_down_role -
theorem
bpow_principle_iff_active_unit_under_passive_down_roles -
theorem
bpow_bool_constraints_iff_active_unit_under_down_role -
theorem
bpow_bool_constraints_iff_active_unit_under_passive_down_roles -
structure
R0Assignment -
def
canonicalR0 -
def
r0ValuePool -
theorem
r0_pool_matches_anchor_formulas -
def
listToR0Assignment -
def
allR0Assignments -
def
r0SumTarget -
theorem
r0_sum_target_eq_147 -
theorem
r0_sum_target_matches_principle -
def
r0StructuralConstraints -
def
r0PrincipleConstraints -
def
validR0Assignments -
theorem
all_r0_assignments_count -
theorem
valid_r0_assignment_count -
theorem
valid_r0_assignments_are_singleton -
theorem
r0_constraints_true_iff -
theorem
r0_constraints_force_canonical -
theorem
r0_unrestricted_forcing_from_affine_roles_and_sum -
theorem
r0_depth_gap_iff_ew_role_under_affine_roles_and_sum -
theorem
r0_unrestricted_forcing_from_affine_roles_and_ew_role -
theorem
r0_unrestricted_forcing_from_affine_roles -
theorem
r0_principle_iff_sum_under_affine_roles_and_depth_gap -
theorem
r0_bool_constraints_iff_sum_under_affine_roles_and_depth_gap -
theorem
r0_principle_constraints_forced_from_affine_roles_and_sum -
theorem
r0_bool_constraints_forced_from_affine_roles_and_sum -
def
anchorBPowAssignment -
def
anchorR0Assignment -
theorem
anchor_bpow_matches_canonical -
theorem
anchor_r0_matches_canonical -
theorem
anchor_is_unique_valid_bpow -
theorem
anchor_is_unique_valid_r0 -
theorem
anchor_bpow_structural_identities -
theorem
anchor_bpow_constraints_from_principle -
theorem
anchor_r0_structural_identities -
theorem
anchor_r0_constraints_from_principle -
theorem
yardstick_choice_sets_collapsed -
theorem
yardstick_unrestricted_forcing_from_role_kernels_and_sums -
theorem
yardstick_unrestricted_forcing_from_cube_roles_and_r0_sum -
theorem
yardstick_unrestricted_forcing_from_cube_roles -
theorem
yardstick_filter_family_forced_from_cube_partition_principle -
theorem
yardstick_assignment_forced_from_cube_partition_principle -
theorem
yardstick_assignment_iff_cube_partition_principle