IndisputableMonolith.Verification.YardstickAssignmentPrinciple
Records the four-sector candidate values of $B_{\mathrm{pow}}$ and $r_0$ that seed the yardstick assignment search, plus the sum and complement identities that constrain them. Verification readers cite it when checking that the O1 choice set is not free parameters but fixed algebraic data. Content is mostly explicit value tables and short algebraic identities over the mass-anchor constants.
claimFor the four mass sectors, the module fixes candidate $B_{\mathrm{pow}}$ values and candidate $r_0$ values, proves the sector-sum identities $\sum B_{\mathrm{pow}} = A$ and $\sum r_0 = VW + E_{\mathrm{passive}}$, and records lepton–electroweak complement and sign relations (same magnitude on the up/EW pair, opposite signs).
background
Recognition Science places particle masses on a $\varphi$-ladder of the form yardstick $\cdot \varphi^{(\mathrm{rung}-8+\mathrm{gap}(Z))}$. The yardstick itself is not a free fit: it is assembled from a small set of sector-level exponents and offsets. This module lives in the Verification layer and makes those sector numbers explicit before any combinatorial assignment is attempted.
Upstream, Constants supplies the RS-native time quantum $\tau_0 = 1$ tick, AlphaDerivation contributes the cubic-ledger seed geometry used in coupling constructions, and Masses.Anchor centralises the parameter-free mass constants in the Model layer ("no proofs claim experimental agreement"). Against that backdrop the module names two families of sector data: $B_{\mathrm{pow}}$ (power/bookkeeping exponents) and $r_0$ (base rung offsets).
Sibling lemmas package the concrete lists, closed-form identities, total sums, and the lepton–EW complement facts (including natural-absolute-value forms and the up/EW sign pattern). Those facts are the raw input to the finite search in the downstream choice-set module.
proof idea
This is primarily a values-and-identities module, not a deep existence proof. It states the four $B_{\mathrm{pow}}$ candidates and four $r_0$ candidates, then discharges short algebraic checks: formula identities for each family, the global sum equalities $B_{\mathrm{pow}}$-sum $= A$ and $r_0$-sum $= V\cdot W + E_{\mathrm{passive}}$, and elementary magnitude/sign lemmas for the lepton and electroweak sectors (complements, natAbs forms, opposite signs on the up/EW pair). Expect rfl, arithmetic simplification, and direct rewriting over the anchor constants rather than a long tactic script.
why it matters in Recognition Science
The module exists to ground the O1 yardstick discussion in fixed sector data. Downstream, YardstickAssignmentChoiceSet "makes the O1 discussion explicit as a finite combinatorial search: start from the four candidate $B_{\mathrm{pow}}$ values and the four candidate $r_0$ values, enumerate all sector-to-value assignments, [and] filter by structural constraints." Without the present identities, that enumeration would be floating numerology.
In the broader RS chain this sits under mass-ladder bookkeeping (yardstick $\cdot \varphi^{(\mathrm{rung}-8+\mathrm{gap}(Z))}$), not under the T0–T8 forcing of $J$, $\varphi$, the eight-tick octave, or $D=3$. It does not settle $\alpha^{-1}(0)$ (still OPEN per AlphaDerivation); it only stabilises the discrete assignment inputs that verification uses when auditing how sector exponents are chosen.
scope and limits
- Does not derive the four $B_{\mathrm{pow}}$ or $r_0$ values from the T0–T8 forcing chain.
- Does not claim experimental mass agreement; anchor constants remain Model-layer.
- Does not enumerate or filter sector permutations; that is the downstream choice-set module.
- Does not close the open infrared $\alpha^{-1}(0)$ boundary condition.
- Does not prove uniqueness of the yardstick assignment, only supplies candidate data and sum identities.
used by (1)
depends on (3)
declarations in this module (23)
-
theorem
B_pow_values -
theorem
B_pow_formula_identities -
theorem
B_pow_sum -
theorem
B_pow_sum_eq_A -
theorem
lepton_ew_complement_down -
theorem
lepton_ew_natAbs_complement_down -
theorem
up_ew_same_magnitude -
theorem
up_negative_and_ew_positive -
theorem
r0_values -
theorem
r0_formula_identities -
theorem
r0_sum -
theorem
r0_sum_eq_V_mul_W_add_Epassive -
theorem
r0_lepton_ew_depth_gap -
theorem
r0_sum_decomposition -
theorem
W_multipliers_sum_to_V -
theorem
additive_corrections_sum_to_Ep -
theorem
r0_sum_from_cube -
theorem
up_ew_sign_duality -
theorem
depths_exhaust_vertices -
theorem
r0_order_constraints -
theorem
cube_partition_budget -
structure
AssignmentConstraints -
def
assignment_valid