module module

`IndisputableMonolith.Verification.NeutrinoBaselineChoiceSet`

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 (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Physics.NeutrinoSector module_import

declarations in this module (43)

structure BaselineCandidate L25
def r2_num L30
def r3_num L33
def quarterRung L36
def r1 L38
def r2 L39
def r3 L40
def canonicalCandidate L43
def candidatePool L46
def deepAtmosphericWindow L50
def quarterPhaseClass L54
def structuralGapProfile L58
def admissible L62
def validCandidates L65
def deepestEdgeOnlyAtmospheric L70
theorem candidate_pool_count L73
theorem structural_gap_profile_holds L76
theorem deepest_edge_atmospheric_num_eq L82
theorem deep_window_forced_from_edge_confinement L88
theorem quarter_phase_forced_from_eight_tick_offset L97
theorem filter_pair_forced_from_edge_confinement L106
theorem deepest_edge_only_forces_atmospheric_num L113
theorem deep_window_phase_forces_r3_num L122
theorem deep_window_phase_forces_r3_value L133
theorem deep_window_phase_forces_r1_num L141
theorem deep_window_phase_forces_r1_value L150
theorem deep_window_phase_forces_res_nu3 L158
theorem deep_window_phase_forces_res_nu1 L167
theorem edge_confinement_forces_canonical_baseline L177
theorem absolute_baseline_num_forced_from_deep_ladder L187
theorem absolute_baseline_num_forced_eq_neg239 L195
theorem deep_ladder_constraint_iff_canonical_candidate L205
def deepLadderForcedCandidate L219
theorem deep_ladder_forced_candidate_eq_canonical L223
theorem deep_ladder_geometry_forces_canonical_baseline L229
theorem valid_candidate_count L236
theorem valid_candidates_singleton L239
theorem canonical_is_valid L243
theorem unique_valid_candidate L248
theorem canonical_r1_matches_res_nu1 L254
theorem canonical_r3_matches_res_nu3 L259
theorem baseline_choice_set_collapsed L268
theorem admissible_baselines_match_res_nu1 L272