Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Readable signature
CeilDivSix(n,q)Exact expansion
((exists bcs_lower_gap_bertrand_defined_ceil_div_six. bcs_lower_gap_bertrand_defined_ceil_div_six + (n) = 6 * (q)) /\ exists bcs_upper_gap_bertrand_defined_ceil_div_six. bcs_upper_gap_bertrand_defined_ceil_div_six + S (6 * (q)) = (n) + 6)This node is conservative notation, not a theorem, new axiom, predicate constant, or kernel rule. Its expansion is checked for exact first-order AST equivalence.
Definition neighborhood
Expands using
Used by definitions
none
Used by theorem statements or local proof propositions
BT00R0 ceil_div_six_shift BT00R1 ceil_div_six_total BT00R2 ceil_div_six_functional BT00R5 ceil_div_six_square_six_step BT00RF ceil_div_six_le_of_upper BT00RI floor_ceil_complement_budget BT00RJ floor_ceil_division_budget BT00SW bertrand_h_six_step_transport_from_total BT00SY bertrand_hj_six_step_from_total BT00WE ceil_div_six_budget_of_scaled_le BT00WP bertrand_h_root_32_from_total BT00WQ bertrand_h_root_33_from_total BT00WR bertrand_h_root_34_from_total BT00WS bertrand_h_root_35_from_total BT00WT bertrand_h_root_36_from_total BT00WU bertrand_h_root_37_from_total BT00WW bertrand_hj_base_window_thirty_two_from_total BT00X2 bertrand_hj_six_block_iterate_from_total BT00X3 bertrand_hj_envelope_thirty_two BT00X6 bertrand_main_inequality_factorized_from_total