module module

`IndisputableMonolith.Verification.YardstickAssignmentChoiceSet`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Masses.Anchor module_import
IndisputableMonolith.Verification.YardstickAssignmentPrinciple module_import

declarations in this module (80)

structure BPowAssignment L26
def canonicalBPow L33
def mirroredBPow L40
def bPowValuePool L46
theorem bpow_pool_matches_anchor_formulas L52
def listToBPowAssignment L57
def allBPowAssignments L61
def bpowSumTarget L65
theorem bpow_sum_target_eq_one L67
theorem bpow_sum_target_matches_principle L70
def bpowStructuralConstraints L80
def bpowPrincipleConstraints L88
def validBPowAssignments L95
theorem all_bpow_assignments_count L98
theorem valid_bpow_assignment_count L101
theorem valid_bpow_assignments_are_singleton L104
theorem bpow_constraints_true_iff L108
theorem bpow_constraints_force_canonical L114
theorem bpow_principle_normal_form L128
theorem bpow_unrestricted_forcing_from_passive_coupling L164
theorem bpow_unrestricted_forcing_from_down_role L200
theorem bpow_lepton_forced_from_down_role_and_sign_sum L223
theorem bpow_lepton_role_iff_down_role_under_sign_sum L244
theorem bpow_sign_forced_from_lepton_down_sum L275
theorem bpow_principle_constraints_forced_from_edge_roles L297
theorem bpow_principle_constraints_forced_from_passive_active_roles L329
theorem bpow_bool_constraints_forced_from_edge_roles L341
theorem bpow_bool_constraints_forced_from_passive_active_roles L352
theorem bpow_unrestricted_forcing_from_edge_roles L363
theorem bpow_unrestricted_forcing_from_passive_active_roles L374
theorem bpow_unrestricted_forcing_from_passive_down_roles L386
theorem bpow_two_branch_under_down_role L399
theorem bpow_orientation_selects_canonical_from_two_branch L437
theorem bpow_orientation_selects_canonical_from_passive_down_roles L453
theorem bpow_principle_iff_active_unit_under_down_role L467
theorem bpow_principle_iff_active_unit_under_passive_down_roles L499
theorem bpow_bool_constraints_iff_active_unit_under_down_role L510
theorem bpow_bool_constraints_iff_active_unit_under_passive_down_roles L520
structure R0Assignment L531
def canonicalR0 L538
def r0ValuePool L544
theorem r0_pool_matches_anchor_formulas L550
def listToR0Assignment L555
def allR0Assignments L559
def r0SumTarget L563
theorem r0_sum_target_eq_147 L568
theorem r0_sum_target_matches_principle L571
def r0StructuralConstraints L581
def r0PrincipleConstraints L588
def validR0Assignments L594
theorem all_r0_assignments_count L597
theorem valid_r0_assignment_count L600
theorem valid_r0_assignments_are_singleton L603
theorem r0_constraints_true_iff L607
theorem r0_constraints_force_canonical L613
theorem r0_unrestricted_forcing_from_affine_roles_and_sum L627
theorem r0_depth_gap_iff_ew_role_under_affine_roles_and_sum L663
theorem r0_unrestricted_forcing_from_affine_roles_and_ew_role L706
theorem r0_unrestricted_forcing_from_affine_roles L718
theorem r0_principle_iff_sum_under_affine_roles_and_depth_gap L729
theorem r0_bool_constraints_iff_sum_under_affine_roles_and_depth_gap L746
theorem r0_principle_constraints_forced_from_affine_roles_and_sum L757
theorem r0_bool_constraints_forced_from_affine_roles_and_sum L770
def anchorBPowAssignment L781
def anchorR0Assignment L787
theorem anchor_bpow_matches_canonical L793
theorem anchor_r0_matches_canonical L797
theorem anchor_is_unique_valid_bpow L801
theorem anchor_is_unique_valid_r0 L806
theorem anchor_bpow_structural_identities L814
theorem anchor_bpow_constraints_from_principle L833
theorem anchor_r0_structural_identities L851
theorem anchor_r0_constraints_from_principle L864
theorem yardstick_choice_sets_collapsed L880
theorem yardstick_unrestricted_forcing_from_role_kernels_and_sums L888
theorem yardstick_unrestricted_forcing_from_cube_roles_and_r0_sum L910
theorem yardstick_unrestricted_forcing_from_cube_roles L925
theorem yardstick_filter_family_forced_from_cube_partition_principle L940
theorem yardstick_assignment_forced_from_cube_partition_principle L963
theorem yardstick_assignment_iff_cube_partition_principle L981