module module

`IndisputableMonolith.Verification.YardstickAssignmentPrinciple`

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Verification.YardstickAssignmentChoiceSet module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.AlphaDerivation module_import
IndisputableMonolith.Masses.Anchor module_import

declarations in this module (23)

theorem B_pow_values L61
theorem B_pow_formula_identities L67
theorem B_pow_sum L81
theorem B_pow_sum_eq_A L86
theorem lepton_ew_complement_down L93
theorem lepton_ew_natAbs_complement_down L99
theorem up_ew_same_magnitude L106
theorem up_negative_and_ew_positive L112
theorem r0_values L120
theorem r0_formula_identities L126
theorem r0_sum L140
theorem r0_sum_eq_V_mul_W_add_Epassive L146
theorem r0_lepton_ew_depth_gap L154
theorem r0_sum_decomposition L159
theorem W_multipliers_sum_to_V L164
theorem additive_corrections_sum_to_Ep L168
theorem r0_sum_from_cube L171
theorem up_ew_sign_duality L183
theorem depths_exhaust_vertices L191
theorem r0_order_constraints L195
theorem cube_partition_budget L204
structure AssignmentConstraints L219
def assignment_valid L230