'Omega.weighted_mean' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.displacement_conjugacy' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.affine_iterate' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.homothety_comp' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.homothety_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.observation_commutes' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.observation_iterate' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.real_time_semigroup' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.arbitrary_intercept_defect' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.grid_interface' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.phi_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.phi_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.phi_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.denominator_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.lam_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.lam_lt_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.shares_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.mu_eq_one_sub' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.lam_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.q_lt_lam' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.lam_lt_q_plus' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.delta_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.delta_lt_half_pi' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.s_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.c_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.sc_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.one_arcsecond' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.seeds_distinct' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.marks_collinear' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.marks_affine_dimension' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.seed_linear_combination' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.centered_span' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.center_relative_rank' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.center_adjoined_affine_dimension' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.moment_matrix' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.coordinates_rank' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.gram_rank' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.gram_entries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.embedded_center_relative_rank' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.step_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.extinction_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.threshold_values' does not depend on any axioms
'Omega.extinction_by_ten' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.deepest_seeds' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.all_twenty_three_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.gcd_constants' depends on axioms: [propext]
'Omega.inverse_identity' does not depend on any axioms
'Omega.remainder_halved' depends on axioms: [propext, Quot.sound]
'Omega.first_remainder_reconstruction' depends on axioms: [propext, Quot.sound]
'Omega.first_remainder_injective' depends on axioms: [propext, Quot.sound]
'Omega.first_remainder_injective_domain' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.finite_gap_certificate' does not depend on any axioms
'Omega.certified_gap' depends on axioms: [propext, Quot.sound]
'Omega.minimum_gap_attained' depends on axioms: [propext]
'Omega.finite_certificate_inequality' does not depend on any axioms
'Omega.S_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.Q_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.Q_lt_S' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.division_identity' depends on axioms: [propext]
'Omega.remainder_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.step_zero' depends on axioms: [propext]
'Omega.step_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.step_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.forward_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.step_monotone' depends on axioms: [propext]
'Omega.q_in_interval' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.lam_in_interval' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.floor_q' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.no_interior_boundary' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.floor_agreement_of_interval' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.exact_parameter_interval' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.certified_floor_equality' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.trajectory_equality' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.truncation_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.truncation_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.truncation_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.truncation_seven' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.truncation_eight' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.precision_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.arc_length' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.semicircle_retained' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.semicircle_in_outline' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.major_arc_no_retracing' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.upper_seed_endpoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.lower_seed_endpoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.mark_re' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.mark_im' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.bilateral_reflection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.mark_distance' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.inner_extension_length' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.outer_extension_length' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.negative_outer_extension_length' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.total_extension_length' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.chord_length' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.outer_segment_retained' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.G_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.C_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.W_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.geometric_provenance' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.outline_length' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.reference_not_outline' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.marked_coordinate_uniqueness' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.heights_strictly_ordered' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.sequential_extensions' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.scalar_roundtrip' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.scalar_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.scalar_canonical' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.rational_residual' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.real_residual' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.positive_residual_difference' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.grid_finite_interface' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.grid_trajectory' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.repeated_rounding_counterexample' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.ledger_interface' depends on axioms: [propext]
'Omega.external_factorization' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.predecessor_inequalities' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.point_reconstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.Ledger.euclidean_identity' depends on axioms: [propext]
'Omega.Ledger.remainder_bounds' depends on axioms: [propext]
'Omega.Ledger.one_step_inverse' depends on axioms: [propext]
'Omega.Ledger.roundtrip' depends on axioms: [propext]
'Omega.Ledger.encode_length' depends on axioms: [propext]
'Omega.Ledger.generated_admissible' depends on axioms: [propext]
'Omega.Ledger.canonical_division' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.Ledger.admissible_roundtrip' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.Ledger.encoding_injective' depends on axioms: [propext]
'Omega.Ledger.admissibility_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.Ledger.weighted_identity' depends on axioms: [propext]
'Omega.Ledger.encoded_weighted_identity' depends on axioms: [propext]
'Omega.Ledger.trajectory_reconstruction' depends on axioms: [propext]
'Omega.central_provenance_theorem' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.mark_dot' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.mark_radius' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.mark_angle_cosine' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.seed_angle' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.triangle_area' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.placed_distance' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.placed_arc_derivative' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.placed_G' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.placed_C' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.provenance_all_placements' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.mark_scale' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.circle_scale' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.outline_scale' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.placed_homothety' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.readout_scale' depends on axioms: [propext, Classical.choice, Quot.sound]
'Omega.curve_reconstruction' depends on axioms: [propext, Classical.choice, Quot.sound]