Verification Yardstick Assignment Choice Set

The assignment choice set

A verification yardstick is a fixed scale used to check that the framework's internal constants and particle assignments are consistent. The choice set is the finite list of all ways those constants could be assigned to the four particle sectors: lepton, up quark, down quark, and electroweak. The module enumerates every permutation of four candidate values across those four sectors, producing 24 possible assignments for each yardstick, then filters them through the structural constraints that the framework's principles require.

The two yardsticks are named B_pow and r0. For B_pow, the four candidate values are built from framework constants E_passive, E_total, and A. For r0, the candidates use W, E_total, and A. The module defines each assignment as a structure with four integer fields, one per sector, and constructs the full list by permuting the value pool and converting each permutation into an assignment record.

The central result is a collapse to a singleton. After applying the structural constraints, the 24 possible assignments for B_pow reduce to exactly one valid assignment, and the same happens for r0. The theorem valid_bpow_assignments_are_singleton and its r0 counterpart state this directly: the filtered list equals a single canonical assignment. Two further theorems, bpow_constraints_force_canonical and r0_constraints_force_canonical, prove that any assignment satisfying the principle constraints must equal the canonical one. This means the constraints do not merely pick out a preferred assignment; they rule out all alternatives.

The module also proves the assignments are mutually forced. The theorem yardstick_assignment_forced_from_cube_partition_principle shows that if both assignments satisfy their respective role equations and sum targets, then both must be the canonical ones simultaneously. The anchor assignments, which come from the framework's own formulas, match the canonical assignments exactly, as shown by anchor_bpow_matches_canonical and anchor_r0_matches_canonical. The proofs are computational, using native_decide to check finite cases, and they are machine-checked in the framework's library of formal theorems.

What this establishes in plain language is that the framework's yardstick assignments are not arbitrary choices. Given the candidate values and the structural constraints, there is exactly one way to assign them to the sectors. The framework's own anchor formulas land on that unique assignment, confirming internal consistency. The finite search is exhaustive, so no alternative assignment survives the constraints.

theorem valid_bpow_assignments_are_singleton :
    validBPowAssignments = [canonicalBPow] := by
  native_decide

theorem valid_r0_assignments_are_singleton :
    validR0Assignments = [canonicalR0] := by
  native_decide

theorem bpow_constraints_force_canonical (a : BPowAssignment)
    (ha : a ∈ allBPowAssignments)
    (hP : bpowPrincipleConstraints a) :
    a = canonicalBPow := by
  have htrue : bpowStructuralConstraints a = true := (bpow_constraints_true_iff a).2 hP
  have hmem : a ∈ validBPowAssignments := by
    unfold validBPowAssignments
    exact List.mem_filter.mpr ⟨ha, htrue⟩
  rw [valid_bpow_assignments_are_singleton] at hmem
  simpa using hmem

theorem r0_constraints_force_canonical (a : R0Assignment)
    (ha : a ∈ allR0Assignments)
    (hP : r0PrincipleConstraints a) :
    a = canonicalR0 := by
  have htrue : r0StructuralConstraints a = true := (r0_constraints_true_iff a).2 hP
  have hmem : a ∈ validR0Assignments := by
    unfold validR0Assignments
    exact List.mem_filter.mpr ⟨ha, htrue⟩
  rw [valid_r0_assignments_are_singleton] at hmem
  simpa using hmem

/-- Cube-partition first-principles forcing:
    once the role kernels and structural sums are fixed, sector yardstick assignments
    are uniquely forced to the canonical formulas. -/
theorem yardstick_assignment_forced_from_cube_partition_principle
    (b : BPowAssignment) (r : R0Assignment)
    (hbLepton : b.lepton = -(2 * (E_passive : ℤ)))
    (hbDown : b.down = 2 * (E_total : ℤ) - 1)
    (hbEwPos : 0 < b.ew)
    (hbEwMag : Int.natAbs b.ew = A)
    (hbSum : b.lepton + b.up + b.down + b.ew = bpowSumTarget)
    (hrUpRole : r.up = 2 * (W : ℤ) + (A : ℤ))
    (hrDownRole : r.down = (E_total : ℤ) - (W : ℤ))
    (hrDepthGap : r.lepton - r.ew = (W : ℤ) - 10)
    (hrSum : r.lepton + r.up + r.down + r.ew = r0SumTarget) :
    b = canonicalBPow ∧ r = canonicalR0 := by
  exact yardstick_unrestricted_forcing_from_role_kernels_and_sums
    b r hbLepton hbDown hbEwPos hbEwMag hbSum hrUpRole hrDownRole hrDepthGap hrSum

theorem anchor_bpow_matches_canonical :
    anchorBPowAssignment = canonicalBPow := by
  native_decide

theorem anchor_r0_matches_canonical :
    anchorR0Assignment = canonicalR0 := by
  native_decide

What this page does not claim

No claim that these assignments determine particle masses or any measured physical quantity. No claim that the structural constraints are derived from first principles within this module. No claim that the framework's constants E_passive, E_total, W, and A are themselves derived here.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/YardstickAssignmentChoiceSet.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: