IndisputableMonolith.Verification.YardstickAssignmentChoiceSet
Finite choice set of sector yardstick exponents (B-powers) compatible with Anchor mass formulas and the Yardstick Assignment Principle. Defines the canonical map, its orientation-mirrored twin, the shared magnitude pool, the unit-sum target, and structural plus principle constraints. Verification work cites it to treat admissible exponent maps as a discrete filtered set. Mostly definitions and short equalities linking the pool to Anchor and the sum target to the principle module.
claimA B-power assignment maps each particle sector to a real yardstick exponent. The module fixes a canonical assignment $B^{\mathrm{can}}$, its orientation-reflected twin $B^{\mathrm{mir}}$ (same magnitudes, flipped active-edge sign), the finite pool of those magnitudes, the normalisation $\sum B = 1$, and the structural and principle constraint sets. It shows the pool matches the Anchor closed forms and that the sum target equals one and agrees with the Yardstick Assignment Principle.
background
Recognition Science places sector mass yardsticks on a phi-ladder: each sector carries a B-power (exponent) and an $r_0$ offset fixed by counting, not by fit. The upstream Yardstick Assignment Principle (open problem O1) asks why each sector receives its particular exponents from the 3-cube combinatorial layer: each sector couples to a distinct cube level, and that coupling is meant to force the exponents.
The Anchor module centralises the parameter-free mass constants in the Model layer, with no experimental-agreement claims. Those closed forms supply the concrete magnitude list any assignment choice set must reproduce.
This module sits between those two. It turns the principle and the Anchor formulas into an explicit finite choice set of B-power maps, including the orientation-reflected counterpart of the canonical map, so later verification can quantify over admissible assignments rather than one hard-coded table.
proof idea
Definition-heavy module, not a single theorem. It introduces the assignment type, the canonical and mirrored maps, the magnitude pool, list-to-assignment coercion, and the enumerated family of all pool-based assignments. Short equality lemmas discharge bookkeeping: the pool matches Anchor closed forms; the sum target equals one; that target matches the principle module normalisation; and two constraint bundles (structural versus principle) package the filters an assignment must pass. Proofs are algebraic or list equalities against the imported Anchor and principle definitions.
why it matters in Recognition Science
Closes the discrete search space for open problem O1 (sector to cube coupling) by making admissible B-power maps a finite checkable set rather than an open parameter family. Downstream mass and verification work can quantify over the enumerated assignments subject to the structural and principle constraint bundles, and can treat canonical versus mirrored orientation as the only sign ambiguity. Ties the mass yardstick story (Anchor formulas, phi-ladder rungs) to the forcing-chain geometry (eight-tick octave, $D=3$ cube) without claiming experimental lock-in. No downstream used-by edges are recorded yet; the module is infrastructure for later uniqueness or exhaustion arguments over the choice set.
scope and limits
- Does not prove uniqueness of the canonical B-power map among all real assignments.
- Does not claim experimental mass agreement; Anchor stays in the Model layer.
- Does not derive exponents from the 3-cube count; that remains O1 upstream.
- Does not fix r0 offsets or full mass formulas, only the B-power choice set.
- Does not select which orientation (canonical vs mirrored) is physical.
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