ℹ [1432/1543] Replayed SentinelProofs
info: SentinelProofs.lean:89:0: 'SentinelProofs.clip_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SentinelProofs.lean:90:0: 'SentinelProofs.blend_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SentinelProofs.lean:91:0: 'SentinelProofs.coefficient_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SentinelProofs.lean:92:0: 'SentinelProofs.step_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SentinelProofs.lean:93:0: 'SentinelProofs.trajectory_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SentinelProofs.lean:94:0: 'SentinelProofs.weight_nonnegative' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SentinelProofs.lean:95:0: 'SentinelProofs.weight_sum_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SentinelProofs.lean:96:0: 'SentinelProofs.weight_sum_below_one' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [2553/2560] Built SentinelTheory.Evidence (44s)
✔ [2554/2560] Built SentinelTheory.Timing (44s)
✔ [2555/2560] Built SentinelTheory.Language (44s)
✔ [2556/2560] Built SentinelTheory.Values (45s)
✔ [2557/2560] Built SentinelTheory (37s)
ℹ [2559/2560] Built Audit (85s)
info: Audit.lean:4:0: 'SentinelProofs.clip_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:5:0: 'SentinelProofs.blend_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:6:0: 'SentinelProofs.coefficient_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:7:0: 'SentinelProofs.step_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:8:0: 'SentinelProofs.trajectory_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:9:0: 'SentinelProofs.weight_nonnegative' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:10:0: 'SentinelProofs.weight_sum_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:11:0: 'SentinelProofs.weight_sum_below_one' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:12:0: 'SentinelTheory.event_dependent_rates_bounded' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:13:0: 'SentinelTheory.trace_matches_clipped_update' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:14:0: 'SentinelTheory.trace_zero_time' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:15:0: 'SentinelTheory.trace_time_subdivision' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:16:0: 'SentinelTheory.future_change_telescopes' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:17:0: 'SentinelTheory.future_probability_difference_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:18:0: 'SentinelTheory.exponential_width_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:19:0: 'SentinelTheory.normalized_square_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:20:0: 'SentinelTheory.ellipse_expansion_contains_old' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:21:0: 'SentinelTheory.branch_union_preserves_old' depends on axioms: [propext, Quot.sound]
info: Audit.lean:22:0: 'SentinelTheory.path_product_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:23:0: 'SentinelTheory.strongest_route_can_lose_mass' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:24:0: 'SentinelTheory.path_mass_geometric_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:25:0: 'SentinelTheory.dominated_path_series_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:26:0: 'SentinelTheory.geometric_tail_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:27:0: 'SentinelTheory.dominated_path_tail_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:28:0: 'SentinelTheory.euler_phase_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:29:0: 'SentinelTheory.phase_has_unit_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:30:0: 'SentinelTheory.phase_composition' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:31:0: 'SentinelTheory.evidence_xor_explanations_ambiguous' does not depend on any axioms
info: Audit.lean:32:0: 'SentinelTheory.evidence_common_flip_invariant' depends on axioms: [propext]
info: Audit.lean:33:0: 'SentinelTheory.evidence_observations_cannot_decode_h' depends on axioms: [propext]
info: Audit.lean:34:0: 'SentinelTheory.evidence_correction_recovers' does not depend on any axioms
info: Audit.lean:35:0: 'SentinelTheory.evidence_same_group_disagreement_cancels' does not depend on any axioms
info: Audit.lean:36:0: 'SentinelTheory.evidence_cross_group_disagreement' does not depend on any axioms
info: Audit.lean:37:0: 'SentinelTheory.evidence_majority_flip_equivariant' does not depend on any axioms
info: Audit.lean:38:0: 'SentinelTheory.evidence_majority_ignores_one_fault' does not depend on any axioms
info: Audit.lean:39:0: 'SentinelTheory.evidence_majority_follows_common_fault' does not depend on any axioms
info: Audit.lean:40:0: 'SentinelTheory.evidence_bias_shift_unidentifiable' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:41:0: 'SentinelTheory.evidence_posterior_odds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:42:0: 'SentinelTheory.evidence_log_ratios_add' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:43:0: 'SentinelTheory.evidence_duplicate_overcounts' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:44:0: 'SentinelTheory.evidence_cusum_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:45:0: 'SentinelTheory.evidence_cusum_dominates' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:46:0: 'SentinelTheory.evidence_cusum_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:47:0: 'SentinelTheory.evidence_cusum_resets' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:48:0: 'SentinelTheory.evidence_cusum_growth_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:49:0: 'SentinelTheory.evidence_value_of_information_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:50:0: 'SentinelTheory.evidence_no_value_when_decision_fixed' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:51:0: 'SentinelTheory.evidence_smoothed_table_normalized' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:52:0: 'SentinelTheory.evidence_smoothed_table_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:53:0: 'SentinelTheory.evidence_chain_rule' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:54:0: 'SentinelTheory.evidence_disagreement_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:55:0: 'SentinelTheory.evidence_disagreement_symm' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:56:0: 'SentinelTheory.evidence_disagreement_self' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:57:0: 'SentinelTheory.evidence_disagreement_triangle' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:58:0: 'SentinelTheory.xor_conditional_entropy_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:59:0: 'SentinelTheory.xor_joint_information_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:60:0: 'SentinelTheory.xor_single_information_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:61:0: 'SentinelTheory.xor_joint_information_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:62:0: 'SentinelTheory.noiseless_xor_one_bit' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:63:0: 'SentinelTheory.independent_noise_zero_information' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:64:0: 'SentinelTheory.language_silence_is_an_option' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:65:0: 'SentinelTheory.language_adding_option_never_lowers' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:66:0: 'SentinelTheory.language_silence_wins_when_all_negative' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:67:0: 'SentinelTheory.language_budgeted_selection_silence' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:68:0: 'SentinelTheory.language_value_of_information_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:69:0: 'SentinelTheory.language_value_of_information_nonneg_joint' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:70:0: 'SentinelTheory.language_value_of_information_zero_of_constant_best' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Audit.lean:71:0: 'SentinelTheory.language_mismatch_complement' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:72:0: 'SentinelTheory.language_independent_mismatch_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:73:0: 'SentinelTheory.language_brier_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:74:0: 'SentinelTheory.language_mean_brier_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:75:0: 'SentinelTheory.language_constant_forecast_decomposition' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:76:0: 'SentinelTheory.language_base_rate_brier_at_most_quarter' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:77:0: 'SentinelTheory.language_half_forecast_brier' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:78:0: 'SentinelTheory.language_identical_inputs_brier_floor' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:79:0: 'SentinelTheory.language_expression_count' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:80:0: 'SentinelTheory.language_novel_combination_count' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:81:0: 'SentinelTheory.language_novel_combination_exists' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:82:0: 'SentinelTheory.language_codebook_flip_invariant' does not depend on any axioms
info: Audit.lean:83:0: 'SentinelTheory.language_flip_sequence_same_observations' depends on axioms: [Quot.sound]
info: Audit.lean:84:0: 'SentinelTheory.language_no_detector_separates_flip' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:85:0: 'SentinelTheory.language_same_history_one_world_wrong' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:86:0: 'SentinelTheory.language_fusion_nonzero' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:87:0: 'SentinelTheory.interest_ceiling' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:88:0: 'SentinelTheory.interest_zero_relevance' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:89:0: 'SentinelTheory.interest_increases_with_exposure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:90:0: 'SentinelTheory.hard_constraint_zero_activation' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:91:0: 'SentinelTheory.unresolved_keeps_allowance' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:92:0: 'SentinelTheory.positive_exploration_can_activate' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:93:0: 'SentinelTheory.uniform_second_moment' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:94:0: 'SentinelTheory.uniform_fourth_moment' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:95:0: 'SentinelTheory.orthogonal_cubic_zero_linear_moment' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:96:0: 'SentinelTheory.cubic_from_intermediate_multiplication' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:97:0: 'SentinelTheory.corroboration_false_positive_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:98:0: 'SentinelTheory.confirming_alerts_are_subset' does not depend on any axioms
info: Audit.lean:99:0: 'SentinelTheory.noisy_xor_single_feature_blind' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:100:0: 'SentinelTheory.noisy_xor_other_feature_blind' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:101:0: 'SentinelTheory.noisy_xor_output_fair' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:102:0: 'SentinelTheory.noisy_xor_joint_is_informative' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:103:0: 'SentinelTheory.noisy_xor_mass_nonnegative' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:104:0: 'SentinelTheory.noisy_xor_mass_normalized' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:105:0: 'SentinelTheory.xor_is_linear_over_two' depends on axioms: [propext, Quot.sound]
info: Audit.lean:106:0: 'SentinelTheory.independent_clean_sample_mass' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:107:0: 'SentinelTheory.two_step_path_composition' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:108:0: 'SentinelTheory.inverse_certifies_unique_linear_solution' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:109:0: 'SentinelTheory.disjunction_from_and_not' does not depend on any axioms
info: Audit.lean:110:0: 'SentinelTheory.expression_renaming_preserves_meaning' depends on axioms: [propext]
info: Audit.lean:111:0: 'SentinelTheory.finite_boolean_function_expressible' depends on axioms: [propext, Quot.sound]
info: Audit.lean:112:0: 'SentinelTheory.boolean_function_count' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:113:0: 'SentinelTheory.three_bit_function_count' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:114:0: 'SentinelTheory.macro_substitution_preserves_meaning' depends on axioms: [propext]
info: Audit.lean:115:0: 'SentinelTheory.language_growth_preserves_known' does not depend on any axioms
info: Audit.lean:116:0: 'SentinelTheory.finite_expression_in_limit' does not depend on any axioms
info: Audit.lean:117:0: 'SentinelTheory.pathway_operator_norm_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:118:0: 'SentinelTheory.pathway_matrix_series_inverse' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:119:0: 'SentinelTheory.pathway_matrix_series_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:120:0: 'SentinelTheory.pathway_matrix_tail_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:121:0: 'SentinelTheory.empirical_update_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:122:0: 'SentinelTheory.empirical_update_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:123:0: 'SentinelTheory.beta_mean_strict_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:124:0: 'SentinelTheory.beta_variance_expression_nonnegative' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:125:0: 'SentinelTheory.uniform_beta_unknown' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:126:0: 'SentinelTheory.missing_evidence_unchanged' does not depend on any axioms
info: Audit.lean:127:0: 'SentinelTheory.posterior_nonnegative' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:128:0: 'SentinelTheory.posterior_normalized' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:129:0: 'SentinelTheory.zero_prior_stays_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:130:0: 'SentinelTheory.posterior_uninformative' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:131:0: 'SentinelTheory.mixture_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:132:0: 'SentinelTheory.markov_mixture_normalized' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:133:0: 'SentinelTheory.charger_example' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:134:0: 'SentinelTheory.propagated_battery_example' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:135:0: 'SentinelTheory.propagated_task_example' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:136:0: 'SentinelTheory.fourier_delay_phase' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:137:0: 'SentinelTheory.fourier_gain_and_delay' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:138:0: 'SentinelTheory.cross_spectrum_factorization' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:139:0: 'SentinelTheory.forced_trace_initial_value' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:140:0: 'SentinelTheory.forced_trace_convolution' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:141:0: 'SentinelTheory.forced_trace_solves_relaxation' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:142:0: 'SentinelTheory.feasibility_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:143:0: 'SentinelTheory.adding_resources_preserves_feasibility' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:144:0: 'SentinelTheory.indicator_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:145:0: 'SentinelTheory.indicator_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:146:0: 'SentinelTheory.feasibility_gain_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:147:0: 'SentinelTheory.product_unit_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:148:0: 'SentinelTheory.opportunity_relevance_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:149:0: 'SentinelTheory.alternative_routes_monotone' depends on axioms: [propext, Quot.sound]
info: Audit.lean:150:0: 'SentinelTheory.new_route_preserves_possibilities' does not depend on any axioms
info: Audit.lean:151:0: 'SentinelTheory.missing_requirements_shrink' does not depend on any axioms
info: Audit.lean:152:0: 'SentinelTheory.failure_of_one_route_allows_another' does not depend on any axioms
info: Audit.lean:153:0: 'SentinelTheory.action_does_not_identify_preference' does not depend on any axioms
info: Audit.lean:154:0: 'SentinelTheory.identical_observations_cannot_decode_distinct_targets' does not depend on any axioms
info: Audit.lean:155:0: 'SentinelTheory.refinement_preserves_old_representation' does not depend on any axioms
info: Audit.lean:156:0: 'SentinelTheory.refinement_separates_distinctions' does not depend on any axioms
info: Audit.lean:157:0: 'SentinelTheory.fixed_representation_cannot_predict_different_futures' does not depend on any axioms
info: Audit.lean:158:0: 'SentinelTheory.unknown_zero_gate_blocks_activity' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:159:0: 'SentinelTheory.net_gain_positive_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:160:0: 'SentinelTheory.uniform_coverage_budget' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:161:0: 'SentinelTheory.information_can_be_ignored' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:162:0: 'SentinelTheory.timing_clock_compose' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:163:0: 'SentinelTheory.timing_clock_inverse' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:164:0: 'SentinelTheory.timing_offset_latency_not_identifiable' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:165:0: 'SentinelTheory.timing_clock_error_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:166:0: 'SentinelTheory.timing_periodic_shift_indistinguishable' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:167:0: 'SentinelTheory.timing_decay_semigroup' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:168:0: 'SentinelTheory.timing_decay_bounded_between_updates' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:169:0: 'SentinelTheory.timing_wake_time_hits_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:170:0: 'SentinelTheory.timing_wake_time_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:171:0: 'SentinelTheory.timing_value_of_computation_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:172:0: 'SentinelTheory.timing_compute_only_if_gain_exceeds_cost' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:173:0: 'SentinelTheory.timing_budget_active_count_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:174:0: 'SentinelTheory.timing_budget_subset_feasible' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:175:0: 'SentinelTheory.timing_budget_shrink_drops_member' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:176:0: 'SentinelTheory.timing_beta_estimate_open_unit' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:177:0: 'SentinelTheory.timing_beta_estimate_monotone_in_successes' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:178:0: 'SentinelTheory.timing_suspend_discount_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:179:0: 'SentinelTheory.timing_compression_pigeonhole' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:180:0: 'SentinelTheory.timing_compression_not_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:181:0: 'SentinelTheory.timing_inspect_budget_success_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:182:0: 'SentinelTheory.timing_effective_sample_size_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:183:0: 'SentinelTheory.timing_effective_sample_size_independent' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:184:0: 'SentinelTheory.timing_effective_sample_size_decreasing' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:185:0: 'SentinelTheory.value_tentative_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:186:0: 'SentinelTheory.value_tentative_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:187:0: 'SentinelTheory.value_interrupt_rule_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:188:0: 'SentinelTheory.value_optimal_with_silence_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:189:0: 'SentinelTheory.value_unconstrained_threshold_optimal' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:190:0: 'SentinelTheory.value_gated_budget_value_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:191:0: 'SentinelTheory.value_silent_history_hides_sign' depends on axioms: [propext, Quot.sound]
info: Audit.lean:192:0: 'SentinelTheory.value_selective_feedback_bias' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:193:0: 'SentinelTheory.value_joint_survival_factorization' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:194:0: 'SentinelTheory.value_exponential_survival_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:195:0: 'SentinelTheory.value_survival_decreases_with_delay' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:196:0: 'SentinelTheory.value_waiting_cannot_raise_utility' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:197:0: 'SentinelTheory.value_verification_posterior_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:198:0: 'SentinelTheory.value_verification_posterior_vs_prior' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:199:0: 'SentinelTheory.value_verification_posterior_mean' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:200:0: 'SentinelTheory.value_two_outcome_option_value' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:201:0: 'SentinelTheory.value_verification_never_worse_before_cost' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:202:0: 'SentinelTheory.value_filter_step_normalized' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:203:0: 'SentinelTheory.value_rotation_nonidentifiable' depends on axioms: [propext, Quot.sound]
info: Audit.lean:204:0: 'SentinelTheory.value_flip_nonidentifiable' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:205:0: 'SentinelTheory.value_alignment_candidate_count' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:206:0: 'SentinelTheory.value_blocked_action_value_survives' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:207:0: 'SentinelTheory.value_equal_likelihood_posterior_is_prior' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:208:0: 'SentinelTheory.value_pursuit_switch_deviation' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:209:0: 'SentinelTheory.value_pursuit_switch_contracts' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:210:0: 'SentinelTheory.value_pursuit_switch_iterate' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:211:0: 'SentinelTheory.value_pursuit_drifts_to_uncertainty' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:212:0: 'SentinelTheory.value_shrinkage_between' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:213:0: 'SentinelTheory.value_policy_permission_gate' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Audit.lean:214:0: 'SentinelTheory.value_policy_normalized' depends on axioms: [propext, Classical.choice, Quot.sound]
Build completed successfully (2560 jobs).