← All the evidence

axioms.txt

SHA-256 544e052ab570c75dff2802ace606c8ef34b31d58971af7396da1be35751a28cd · download the original

'SentinelProofs.clip_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelProofs.blend_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelProofs.coefficient_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelProofs.step_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelProofs.trajectory_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelProofs.weight_nonnegative' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelProofs.weight_sum_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelProofs.weight_sum_below_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.event_dependent_rates_bounded' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.trace_matches_clipped_update' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.trace_zero_time' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.trace_time_subdivision' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.future_change_telescopes' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.future_probability_difference_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.exponential_width_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.normalized_square_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.ellipse_expansion_contains_old' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.branch_union_preserves_old' depends on axioms: [propext, Quot.sound]
'SentinelTheory.path_product_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.strongest_route_can_lose_mass' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.path_mass_geometric_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.dominated_path_series_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.geometric_tail_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.dominated_path_tail_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.euler_phase_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.phase_has_unit_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.phase_composition' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_xor_explanations_ambiguous' does not depend on any axioms
'SentinelTheory.evidence_common_flip_invariant' depends on axioms: [propext]
'SentinelTheory.evidence_observations_cannot_decode_h' depends on axioms: [propext]
'SentinelTheory.evidence_correction_recovers' does not depend on any axioms
'SentinelTheory.evidence_same_group_disagreement_cancels' does not depend on any axioms
'SentinelTheory.evidence_cross_group_disagreement' does not depend on any axioms
'SentinelTheory.evidence_majority_flip_equivariant' does not depend on any axioms
'SentinelTheory.evidence_majority_ignores_one_fault' does not depend on any axioms
'SentinelTheory.evidence_majority_follows_common_fault' does not depend on any axioms
'SentinelTheory.evidence_bias_shift_unidentifiable' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_posterior_odds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_log_ratios_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_duplicate_overcounts' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_cusum_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_cusum_dominates' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_cusum_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_cusum_resets' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_cusum_growth_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_value_of_information_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_no_value_when_decision_fixed' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_smoothed_table_normalized' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_smoothed_table_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_chain_rule' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_disagreement_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_disagreement_symm' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_disagreement_self' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.evidence_disagreement_triangle' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.xor_conditional_entropy_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.xor_joint_information_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.xor_single_information_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.xor_joint_information_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.noiseless_xor_one_bit' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.independent_noise_zero_information' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_silence_is_an_option' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_adding_option_never_lowers' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_silence_wins_when_all_negative' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_budgeted_selection_silence' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_value_of_information_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_value_of_information_nonneg_joint' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_value_of_information_zero_of_constant_best' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'SentinelTheory.language_mismatch_complement' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_independent_mismatch_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_brier_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_mean_brier_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_constant_forecast_decomposition' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_base_rate_brier_at_most_quarter' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_half_forecast_brier' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_identical_inputs_brier_floor' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_expression_count' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_novel_combination_count' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_novel_combination_exists' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_codebook_flip_invariant' does not depend on any axioms
'SentinelTheory.language_flip_sequence_same_observations' depends on axioms: [Quot.sound]
'SentinelTheory.language_no_detector_separates_flip' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_same_history_one_world_wrong' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.language_fusion_nonzero' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.interest_ceiling' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.interest_zero_relevance' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.interest_increases_with_exposure' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.hard_constraint_zero_activation' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.unresolved_keeps_allowance' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.positive_exploration_can_activate' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.uniform_second_moment' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.uniform_fourth_moment' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.orthogonal_cubic_zero_linear_moment' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.cubic_from_intermediate_multiplication' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.corroboration_false_positive_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.confirming_alerts_are_subset' does not depend on any axioms
'SentinelTheory.noisy_xor_single_feature_blind' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.noisy_xor_other_feature_blind' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.noisy_xor_output_fair' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.noisy_xor_joint_is_informative' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.noisy_xor_mass_nonnegative' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.noisy_xor_mass_normalized' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.xor_is_linear_over_two' depends on axioms: [propext, Quot.sound]
'SentinelTheory.independent_clean_sample_mass' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.two_step_path_composition' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.inverse_certifies_unique_linear_solution' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.disjunction_from_and_not' does not depend on any axioms
'SentinelTheory.expression_renaming_preserves_meaning' depends on axioms: [propext]
'SentinelTheory.finite_boolean_function_expressible' depends on axioms: [propext, Quot.sound]
'SentinelTheory.boolean_function_count' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.three_bit_function_count' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.macro_substitution_preserves_meaning' depends on axioms: [propext]
'SentinelTheory.language_growth_preserves_known' does not depend on any axioms
'SentinelTheory.finite_expression_in_limit' does not depend on any axioms
'SentinelTheory.pathway_operator_norm_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.pathway_matrix_series_inverse' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.pathway_matrix_series_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.pathway_matrix_tail_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.empirical_update_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.empirical_update_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.beta_mean_strict_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.beta_variance_expression_nonnegative' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.uniform_beta_unknown' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.missing_evidence_unchanged' does not depend on any axioms
'SentinelTheory.posterior_nonnegative' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.posterior_normalized' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.zero_prior_stays_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.posterior_uninformative' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.mixture_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.markov_mixture_normalized' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.charger_example' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.propagated_battery_example' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.propagated_task_example' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.fourier_delay_phase' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.fourier_gain_and_delay' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.cross_spectrum_factorization' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.forced_trace_initial_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.forced_trace_convolution' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.forced_trace_solves_relaxation' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.feasibility_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.adding_resources_preserves_feasibility' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.indicator_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.indicator_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.feasibility_gain_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.product_unit_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.opportunity_relevance_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.alternative_routes_monotone' depends on axioms: [propext, Quot.sound]
'SentinelTheory.new_route_preserves_possibilities' does not depend on any axioms
'SentinelTheory.missing_requirements_shrink' does not depend on any axioms
'SentinelTheory.failure_of_one_route_allows_another' does not depend on any axioms
'SentinelTheory.action_does_not_identify_preference' does not depend on any axioms
'SentinelTheory.identical_observations_cannot_decode_distinct_targets' does not depend on any axioms
'SentinelTheory.refinement_preserves_old_representation' does not depend on any axioms
'SentinelTheory.refinement_separates_distinctions' does not depend on any axioms
'SentinelTheory.fixed_representation_cannot_predict_different_futures' does not depend on any axioms
'SentinelTheory.unknown_zero_gate_blocks_activity' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.net_gain_positive_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.uniform_coverage_budget' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.information_can_be_ignored' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_clock_compose' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_clock_inverse' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_offset_latency_not_identifiable' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_clock_error_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_periodic_shift_indistinguishable' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_decay_semigroup' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_decay_bounded_between_updates' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_wake_time_hits_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_wake_time_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_value_of_computation_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_compute_only_if_gain_exceeds_cost' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_budget_active_count_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_budget_subset_feasible' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_budget_shrink_drops_member' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_beta_estimate_open_unit' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_beta_estimate_monotone_in_successes' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_suspend_discount_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_compression_pigeonhole' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_compression_not_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_inspect_budget_success_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_effective_sample_size_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_effective_sample_size_independent' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.timing_effective_sample_size_decreasing' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_tentative_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_tentative_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_interrupt_rule_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_optimal_with_silence_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_unconstrained_threshold_optimal' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_gated_budget_value_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_silent_history_hides_sign' depends on axioms: [propext, Quot.sound]
'SentinelTheory.value_selective_feedback_bias' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_joint_survival_factorization' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_exponential_survival_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_survival_decreases_with_delay' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_waiting_cannot_raise_utility' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_verification_posterior_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_verification_posterior_vs_prior' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_verification_posterior_mean' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_two_outcome_option_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_verification_never_worse_before_cost' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_filter_step_normalized' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_rotation_nonidentifiable' depends on axioms: [propext, Quot.sound]
'SentinelTheory.value_flip_nonidentifiable' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_alignment_candidate_count' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_blocked_action_value_survives' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_equal_likelihood_posterior_is_prior' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_pursuit_switch_deviation' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_pursuit_switch_contracts' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_pursuit_switch_iterate' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_pursuit_drifts_to_uncertainty' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_shrinkage_between' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_policy_permission_gate' depends on axioms: [propext, Classical.choice, Quot.sound]
'SentinelTheory.value_policy_normalized' depends on axioms: [propext, Classical.choice, Quot.sound]