Building OptimalOTS.Challenge.UpperCompressions
⚠ [2689/2689] Built OptimalOTS.Challenge.UpperCompressions (1.9s)
warning: OptimalOTS/Challenge/UpperCompressions.lean:8:18: declaration uses `sorry`
warning: OptimalOTS/Challenge/UpperCompressions.lean:12:8: declaration uses `sorry`
warning: OptimalOTS/Challenge/UpperCompressions.lean:15:8: declaration uses `sorry`
warning: OptimalOTS/Challenge/UpperCompressions.lean:18:8: declaration uses `sorry`
Build completed successfully (2689 jobs).
Exporting #[OptimalOTS.Challenge.UpperCompressions.admissible, OptimalOTS.Challenge.UpperCompressions.secure, OptimalOTS.Challenge.UpperCompressions.cost, propext, Quot.sound, Classical.choice, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList, Char.ofNat, List, eagerReduce, OptimalOTS.Challenge.UpperCompressions.scheme] from OptimalOTS.Challenge.UpperCompressions
Building Submissions.UpperCompressions.Solution
✔ [8798/8856] Built ToMathlib.Probability.UniformOn (1.6s)
✔ [8799/8856] Built ToMathlib.MeasureTheory.Measure.IndependentDraws (1.9s)
✔ [8800/8856] Built ToMathlib.MeasureTheory.Measure.Bounds (1.0s)
✔ [8801/8856] Built VCVio.OracleComp.QueryTracking.RandomOracle.Simulation (3.3s)
✔ [8802/8856] Built VCVio.EvalDist.Monad.Measure (1.9s)
✔ [8803/8856] Built ToMathlib.MeasureTheory.Measure.UniformTable (2.5s)
✔ [8804/8856] Built VCVio.OracleComp.Constructions.SampleableType.MeasureCompatibility (1.9s)
✔ [8805/8856] Built VCVio.EvalDist.Monad.UniformTable (1.5s)
ℹ [8806/8856] Built Submissions.UpperCompressions.ProofBundle02 (6.3s)
info: Submissions/UpperCompressions/ProofBundle02.lean:1234:0: 'OptimalOTS.WeightedSampling.run_loop_fixed_row' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle02.lean:1236:0: 'OptimalOTS.WeightedSampling.loop_support' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle02.lean:1237:0: 'OptimalOTS.WeightedSampling.run_loop_extend' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle02.lean:1239:0: 'OptimalOTS.WeightedSampling.select_source' depends on axioms: [propext]
info: Submissions/UpperCompressions/ProofBundle02.lean:1240:0: 'OptimalOTS.WeightedSampling.select_none_iff' depends on axioms: [propext, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle02.lean:1241:0: 'OptimalOTS.WeightedSampling.select_rank_le' depends on axioms: [propext, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle02.lean:1242:0: 'OptimalOTS.WeightedSampling.select_first' depends on axioms: [propext]
info: Submissions/UpperCompressions/ProofBundle02.lean:1243:0: 'OptimalOTS.WeightedSampling.costAtMost_loop86' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle02.lean:2109:0: 'OptimalOTS.WeightedConstruction.NonceCodec.decode_encode' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle02.lean:2110:0: 'OptimalOTS.WeightedConstruction.NonceCodec.encode_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle02.lean:2111:0: 'OptimalOTS.WeightedConstruction.NonceCodec.encode_decode' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle02.lean:2112:0: 'OptimalOTS.WeightedConstruction.NonceCodec.canonical_of_payload_positive' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle02.lean:2113:0: 'OptimalOTS.WeightedConstruction.NonceCodec.signature86_length' depends on axioms: [propext, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle02.lean:2801:0: 'OptimalOTS.WeightedConstruction.GraphKeygenBridge.E_run_keygen' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle02.lean:2802:0: 'OptimalOTS.WeightedConstruction.GraphKeygenBridge.costAtMost_keygen_bind' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
✔ [8807/8856] Built VCVio.OracleComp.QueryTracking.RandomOracle.EagerTable (1.7s)
⚠ [8808/8856] Built Submissions.UpperCompressions.ProofBundle00 (78s)
info: Submissions/UpperCompressions/ProofBundle00.lean:122:0: 'OptimalOTS.ShallowResearch.single_shape_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:123:0: 'OptimalOTS.ShallowResearch.single_shape_102_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:178:0: 'OptimalOTS.WeightedResearch92.enough_classes92' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:179:0: 'OptimalOTS.WeightedResearch92.aliases_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:180:0: 'OptimalOTS.WeightedResearch92.acceptance_fraction' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:264:0: 'WeightedAvailability.empirical_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:364:0: 'WeightedReplacement.kernel_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:365:0: 'WeightedReplacement.kernel_scale' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:366:0: 'WeightedReplacement.sub_mul_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:367:0: 'WeightedReplacement.kernel_symm' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:368:0: 'WeightedReplacement.first_minimum_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:369:0: 'WeightedReplacement.kernel_additive_envelope' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:370:0: 'WeightedReplacement.kernel_eq_div' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:594:0: 'WeightedReplacement.iidMean_allPass' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:595:0: 'WeightedReplacement.iid_first_minimum_probability' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:596:0: 'WeightedReplacement.iid_first_minimum_event_probability' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:597:0: 'WeightedReplacement.iidMean_eq_uniform_vectors' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:598:0: 'WeightedReplacement.uniform_vectors_first_minimum_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:717:0: 'WeightedReplacement.finite_bayes_likelihood_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:718:0: 'WeightedReplacement.coordinateLikelihood_survival' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:719:0: 'WeightedReplacement.coordinate_posterior_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle00.lean:816:23: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
info: Submissions/UpperCompressions/ProofBundle00.lean:892:0: 'WeightedMGF.factorial_geometric' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:893:0: 'WeightedMGF.exp_bernstein' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:894:0: 'WeightedMGF.centered_mgf' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:895:0: 'WeightedMGF.nonnegative_centered_mgf' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:896:0: 'WeightedMGF.compensated_mgf' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle00.lean:1026:2: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
info: Submissions/UpperCompressions/ProofBundle00.lean:1087:0: 'WeightedKernel.iterate_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1088:0: 'WeightedKernel.iterate_one' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1089:0: 'WeightedKernel.iterate_supermartingale' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1090:0: 'WeightedKernel.exponential_step' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1091:0: 'WeightedKernel.exponential_tail' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1092:0: 'WeightedKernel.optimized_exponent' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1093:0: 'WeightedKernel.freedman_tail' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1094:0: 'WeightedKernel.finite_kernel_freedman' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1248:0: 'WeightedConstants.first_survival' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1249:0: 'WeightedConstants.penultimate_survival' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1250:0: 'WeightedConstants.referenceMean_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1251:0: 'WeightedConstants.relative_peak_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1430:0: 'WeightedReference.weight_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1431:0: 'WeightedReference.reference_mean_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1432:0: 'WeightedReference.post_excess_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1433:0: 'WeightedReference.common_envelope' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle00.lean:1543:8: automatically included section variable(s) unused in theorem `_private.Submissions.UpperCompressions.ProofBundle00.0.WeightedRow.Weights.avg_new`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:1550:8: automatically included section variable(s) unused in theorem `_private.Submissions.UpperCompressions.ProofBundle00.0.WeightedRow.Weights.avg_old`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:1560:8: automatically included section variable(s) unused in theorem `_private.Submissions.UpperCompressions.ProofBundle00.0.WeightedRow.Weights.avg_singleton`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:1590:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.hazard_change_rejected`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:1646:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.rejection_nonneg`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:1648:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_one`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:1652:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.unseenMean_nonneg`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:1660:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.unseenMean_le_mean`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:1668:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.singleton_le_score`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:1751:8: automatically included section variable(s) unused in theorem `_private.Submissions.UpperCompressions.ProofBundle00.0.WeightedRow.Weights.row_ratio_bounds`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:1752:13: Variable name `hL` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hL

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:1834:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_const`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:1838:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_add`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:1843:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_sub`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:1848:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_smul`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
info: Submissions/UpperCompressions/ProofBundle00.lean:1908:0: 'WeightedRow.Weights.drift_outside' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1909:0: 'WeightedRow.Weights.drift_inside' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1910:0: 'WeightedRow.Weights.drift_outside_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1911:0: 'WeightedRow.Weights.drift_inside_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1912:0: 'WeightedRow.Weights.expect_one' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1913:0: 'WeightedRow.Weights.positiveOutside_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1914:0: 'WeightedRow.Weights.positiveInside_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1915:0: 'WeightedRow.Weights.centered_variance_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1916:0: 'WeightedRow.Weights.centered_abs_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:1917:0: 'WeightedRow.Weights.center_predictable_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle00.lean:1990:8: automatically included section variable(s) unused in theorem `WeightedRow.Weights.mean_scoreJump`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:1993:8: automatically included section variable(s) unused in theorem `WeightedRow.Weights.mean_pairJump`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:2011:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.scoreJump_bounds`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:2114:8: automatically included section variable(s) unused in theorem `WeightedRow.Weights.step_not_fresh`:
  [Fintype ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
info: Submissions/UpperCompressions/ProofBundle00.lean:2138:0: 'WeightedRow.Weights.score_bump' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2139:0: 'WeightedRow.Weights.pairScore_bump' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2140:0: 'WeightedRow.Weights.score_drift' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2141:0: 'WeightedRow.Weights.pair_drift' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2142:0: 'WeightedRow.Weights.score_variance_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2143:0: 'WeightedRow.Weights.M1_mean_next' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2144:0: 'WeightedRow.Weights.M2_mean_next' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2145:0: 'WeightedRow.Weights.M1_square_next_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2146:0: 'WeightedRow.Weights.M1_compensated_square_next_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2147:0: 'WeightedRow.Weights.uniform_decoder_expect' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2148:0: 'WeightedRow.Weights.M1_step_mean' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2149:0: 'WeightedRow.Weights.M2_step_mean' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2150:0: 'WeightedRow.Weights.M1_step_square_compensated' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle00.lean:2163:0: automatically included section variable(s) unused in theorem `WeightedPublicCounts.counts_insert_apply`:
  [Fintype ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:2182:56: This simp argument is unused:
  Function.update_of_ne hij

Hint: Omit it from the simp argument list.
  [apply] simp [counts_insert_apply, hq, he, advance, bump, hij, Ne.symm hij]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:2184:0: automatically included section variable(s) unused in theorem `WeightedPublicCounts.counts_update_absent`:
  [Fintype ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:2202:0: automatically included section variable(s) unused in theorem `WeightedPublicCounts.counts_cached`:
  [Fintype ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
info: Submissions/UpperCompressions/ProofBundle00.lean:2205:0: 'WeightedPublicCounts.counts_insert_update' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2206:0: 'WeightedPublicCounts.counts_cached' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle00.lean:2226:0: automatically included section variable(s) unused in theorem `WeightedCacheCounts.not_seen_of_none`:
  [DecidableEq D]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq D] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:2234:20: This simp argument is unused:
  Function.update_of_ne ht

Hint: Omit it from the simp argument list.
  [apply] simp [seen, ht]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:2241:20: This simp argument is unused:
  Function.update_of_ne ht

Hint: Omit it from the simp argument list.
  [apply] simp [seen, ht]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:2243:0: automatically included section variable(s) unused in theorem `WeightedCacheCounts.decoded_update`:
  [Fintype ι]
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype ι] [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle00.lean:2276:0: automatically included section variable(s) unused in theorem `WeightedCacheCounts.seen_card_le`:
  [DecidableEq D]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq D] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
info: Submissions/UpperCompressions/ProofBundle00.lean:2279:0: 'WeightedCacheCounts.classCounts_update_of_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2280:0: 'WeightedCacheCounts.classCounts_update_of_not_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2281:0: 'WeightedCacheCounts.seen_card_update' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2282:0: 'WeightedCacheCounts.seen_card_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2477:0: 'WeightedFirstHit.stoppedKernel_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2478:0: 'WeightedFirstHit.stoppedKernel_one' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2479:0: 'WeightedFirstHit.iterate_stopped' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2480:0: 'WeightedFirstHit.iterate_hit_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2481:0: 'WeightedFirstHit.stopped_exponential_drift' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle00.lean:2482:0: 'WeightedFirstHit.firstHit_freedman' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8809/8856] Built Submissions.UpperCompressions.EqualityCollision91 (6.8s)
warning: Submissions/UpperCompressions/EqualityCollision91.lean:26:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.collisionMass_eq`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:30:6: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:30:6: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:32:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.collisionMass_nonneg`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:113:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.Qrev_eq_D_add_X`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:179:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.qrevJump_eq`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:181:44: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:183:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_dJump`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:190:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_xJump`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:198:6: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:198:6: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:207:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_qfwdJump`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:218:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.unseenDiagonalMean_le`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:227:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.rowSquareScore_nonneg`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:231:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.rowSquareScore_le_score_mul`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:246:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.rowSquareScore_le_total`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:314:41: This simp argument is unused:
  h

Hint: Omit it from the simp argument list.
  [apply] simp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:346:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_freshPiece_sq_le`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:361:26: This simp argument is unused:
  mul_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [if_neg h0, zero_pow]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:361:36: This simp argument is unused:
  zero_pow

Hint: Omit it from the simp argument list.
  [apply] simp only [if_neg h0, mul_zero]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:364:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_forwardPiece_sq`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:374:8: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:374:8: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:376:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_reversePiece_sq_le`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:386:26: This simp argument is unused:
  zero_pow

Hint: Omit it from the simp argument list.
  [apply] simp only [if_neg h1, mul_zero]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:386:36: This simp argument is unused:
  mul_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [if_neg h1, zero_pow]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:416:10: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:425:10: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:416:10: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:425:10: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:440:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.positiveInside_eq_pieces`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:450:74: This simp argument is unused:
  h1

Hint: Omit it from the simp argument list.
  [apply] simp [positiveInside, freshPiece, forwardPiece, reversePiece, h0]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:452:72: This simp argument is unused:
  h0

Hint: Omit it from the simp argument list.
  [apply] simp [positiveInside, freshPiece, forwardPiece, reversePiece, h1]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:477:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.positiveOutside_eq_pieces`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:486:61: This simp argument is unused:
  h1

Hint: Omit it from the simp argument list.
  [apply] simp [positiveOutside, freshPiece, reversePiece, h0]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:488:59: This simp argument is unused:
  h0

Hint: Omit it from the simp argument list.
  [apply] simp [positiveOutside, freshPiece, reversePiece, h1]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:514:12: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/EqualityCollision91.lean:514:12: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
info: Submissions/UpperCompressions/EqualityCollision91.lean:624:0: 'WeightedRow.Weights.Qrev_eq_D_add_X' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/EqualityCollision91.lean:625:0: 'WeightedRow.Weights.X_bump' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/EqualityCollision91.lean:626:0: 'WeightedRow.Weights.expect_xJump' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/EqualityCollision91.lean:627:0: 'WeightedRow.Weights.positiveInside_square_envelope' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/EqualityCollision91.lean:628:0: 'WeightedRow.Weights.positiveOutside_square_envelope' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/EqualityCollision91.lean:629:0: 'WeightedRow.Weights.xJump_compensated_mgf_of_cap' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/EqualityCollision91.lean:630:0: 'WeightedRow.Weights.xJump_upper_compensated_mgf_of_cap' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8810/8856] Built Submissions.UpperCompressions.ProofBundle01 (9.7s)
info: Submissions/UpperCompressions/ProofBundle01.lean:60:0: 'WeightedEmpirical.score_step_mgf' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle01.lean:112:0: 'WeightedEmpirical.lower_score_step_mgf' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle01.lean:126:0: automatically included section variable(s) unused in theorem `WeightedEmpirical.rate_le_linear`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle01.lean:154:4: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/UpperCompressions/ProofBundle01.lean:165:6: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
info: Submissions/UpperCompressions/ProofBundle01.lean:169:0: 'WeightedEmpirical.rate_le_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle01.lean:170:0: 'WeightedEmpirical.mixed_global_constants' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle01.lean:222:0: 'WeightedEmpirical.mixed_row_exponent' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle01.lean:223:0: 'WeightedEmpirical.exp_neg_pow30_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle01.lean:224:0: 'WeightedEmpirical.mixed_row_union_margin' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle01.lean:245:8: automatically included section variable(s) unused in theorem `WeightedRow.Weights.withScore_classMass`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
info: Submissions/UpperCompressions/ProofBundle01.lean:278:0: 'WeightedRow.Weights.withScore_classMass' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle01.lean:279:0: 'WeightedRow.Weights.prefix_deficit' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle01.lean:295:0: automatically included section variable(s) unused in theorem `WeightedCacheEvidence.mem`:
  [DecidableEq Q]
  [Fintype I]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq Q] [Fintype I] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
info: Submissions/UpperCompressions/ProofBundle01.lean:326:0: 'WeightedCacheEvidence.one' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle01.lean:327:0: 'WeightedCacheEvidence.two' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle01.lean:356:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Submissions/UpperCompressions/ProofBundle01.lean:480:6: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
info: Submissions/UpperCompressions/ProofBundle01.lean:541:0: 'WeightedStopping.covariance_young' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle01.lean:542:0: 'WeightedStopping.endpoint' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle01.lean:543:0: 'WeightedStopping.stopped_payoff' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle01.lean:544:0: 'WeightedStopping.mixed72_young_coefficient' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle01.lean:545:0: 'WeightedStopping.covariance_coefficient' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle01.lean:546:0: 'WeightedStopping.mixed72_covariance' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle01.lean:547:0: 'WeightedStopping.stopped_mixed72_payoff' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle01.lean:548:0: 'WeightedStopping.pre_authentication_domination' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle01.lean:577:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.seen_nonneg`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle01.lean:581:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.seen_le_score`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle01.lean:591:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.bad_le_twice_pairScore`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
info: Submissions/UpperCompressions/ProofBundle01.lean:618:0: 'WeightedRow.Weights.hazard_le_score_pair' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8811/8856] Built Submissions.UpperCompressions.ProofBundle03 (20s)
info: Submissions/UpperCompressions/ProofBundle03.lean:1097:0: 'OptimalOTS.WeightedScheme.Scheme.correct' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:1099:0: 'OptimalOTS.WeightedScheme.Scheme.keygenCost' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:1100:0: 'OptimalOTS.WeightedScheme.Scheme.signCost' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:1101:0: 'OptimalOTS.WeightedScheme.Scheme.verifyCost' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:1102:0: 'OptimalOTS.WeightedScheme.Scheme.verifyDeterministic' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:1103:0: 'OptimalOTS.WeightedScheme.Scheme.signatureSize' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:1104:0: 'OptimalOTS.WeightedScheme.Scheme.rejectsOversized' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle03.lean:1612:34: Variable name `hh` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hh

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: Submissions/UpperCompressions/ProofBundle03.lean:1626:0: 'OptimalOTS.WeightedConstruction.WideForest.graph_keygenCost' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:1628:0: 'OptimalOTS.WeightedConstruction.WideForest.hash_output_width' depends on axioms: [propext]
info: Submissions/UpperCompressions/ProofBundle03.lean:1629:0: 'OptimalOTS.WeightedConstruction.WideForest.input_costs' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2077:0: 'OptimalOTS.WeightedConstruction.WideForest.exists_mem_evaluated_of_ne' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2078:0: 'OptimalOTS.WeightedConstruction.WideForest.reconstructCost_eq' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2581:0: 'OptimalOTS.WeightedConstruction.WideForest.card_family_of_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2582:0: 'OptimalOTS.WeightedConstruction.WideForest.isCut_of_mem_family' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2583:0: 'OptimalOTS.WeightedConstruction.WideForest.card_of_mem_family' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2584:0: 'OptimalOTS.WeightedConstruction.WideForest.cost_of_mem_family' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2585:0: 'OptimalOTS.WeightedConstruction.WideForest.reconstructCost_cutOf' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2586:0: 'OptimalOTS.WeightedConstruction.WideForest.revealBits_cutOf' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2601:0: 'OptimalOTS.WeightedConstruction.WideForest.revealBits_of_mem_family' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2602:0: 'OptimalOTS.WeightedConstruction.WideForest.reconstruction_of_mem_family' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2603:0: 'OptimalOTS.WeightedConstruction.WideForest.disclosure_and_nonce_bits' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2623:0: 'OptimalOTS.WeightedConstruction.WideForest.card_family' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2624:0: 'OptimalOTS.WeightedConstruction.WideForest.card_family_numeric' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2694:0: 'OptimalOTS.WeightedConstruction.TruncFiber.fiberEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2695:0: 'OptimalOTS.WeightedConstruction.TruncFiber.card_filter_setWidth' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2696:0: 'OptimalOTS.WeightedConstruction.TruncFiber.card_256_128' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2697:0: 'OptimalOTS.WeightedConstruction.TruncFiber.card_256_129' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2815:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.card_class' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2816:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.card_alias' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2817:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.rawClass_fiber' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2918:0: 'OptimalOTS.WeightedConstruction.WideForest.typed_cost' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2919:0: 'OptimalOTS.WeightedConstruction.WideForest.typed_correct' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2920:0: 'OptimalOTS.WeightedConstruction.WideForest.typed_signatureSize' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2921:0: 'OptimalOTS.WeightedConstruction.WideForest.typed_rejectsOversized' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2922:0: 'OptimalOTS.WeightedConstruction.WideForest.typed_keygenCost' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2923:0: 'OptimalOTS.WeightedConstruction.WideForest.typed_signCost' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2924:0: 'OptimalOTS.WeightedConstruction.WideForest.typed_verifyDeterministic' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:3122:0: 'OptimalOTS.WeightedConstruction.WideWire.cost' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:3123:0: 'OptimalOTS.WeightedConstruction.WideWire.correct' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:3124:0: 'OptimalOTS.WeightedConstruction.WideWire.signatureSize' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:3125:0: 'OptimalOTS.WeightedConstruction.WideWire.rejectsOversized' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:3126:0: 'OptimalOTS.WeightedConstruction.WideWire.keygenCost' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:3127:0: 'OptimalOTS.WeightedConstruction.WideWire.signCost' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:3128:0: 'OptimalOTS.WeightedConstruction.WideWire.verifyDeterministic' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:3269:0: 'OptimalOTS.WeightedSampling.Availability.loop_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8812/8856] Built Submissions.UpperCompressions.ProofBundle04 (21s)
info: Submissions/UpperCompressions/ProofBundle04.lean:37:0: 'OptimalOTS.WeightedSampling.Availability.uniform_option_miss' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:168:0: 'OptimalOTS.WeightedFreshness.graph_keygen_preservesLength' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:202:0: 'WeightedAvailability.replacement_envelope' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:343:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.decodeRaw_fiber' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:344:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.rawTier_fiber' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:375:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.decode_fiber' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:376:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.accepted_decode_count' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:478:0: 'OptimalOTS.WeightedConstruction.WideHonest.uniform_miss' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:479:0: 'OptimalOTS.WeightedConstruction.WideHonest.signing_failure_half' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:480:0: 'OptimalOTS.WeightedConstruction.WideHonest.admissible' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle04.lean:583:10: This simp argument is unused:
  Function.comp_def

Hint: Omit it from the simp argument list.
  [apply] simp [(hc v).mpr rfl, strictRank]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle04.lean:599:10: This simp argument is unused:
  ha

Hint: Omit it from the simp argument list.
  [apply] simp [hav]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/ProofBundle04.lean:638:0: 'WeightedReplacement.select_eq_firstMinimumEvent' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:639:0: 'WeightedReplacement.firstMinimumEvent_map_iff' depends on axioms: [propext, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:640:0: 'WeightedReplacement.iid_select_probability' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:641:0: 'WeightedReplacement.tagged_candidate_target_iff' depends on axioms: [propext]
info: Submissions/UpperCompressions/ProofBundle04.lean:642:0: 'WeightedReplacement.iid_tagged_table_probability' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle04.lean:687:28: This simp argument is unused:
  E_pure

Hint: Omit it from the simp argument list.
  [apply] simp [drawList, iidMean]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle04.lean:727:24: This simp argument is unused:
  Function.comp_apply

Hint: Omit it from the simp argument list.
  [apply] simp only [candidate, apply_ite, ENNReal.ofReal_one, ENNReal.ofReal_zero] at he ⊢

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/ProofBundle04.lean:732:0: 'WeightedReplacement.E_drawList_ofReal' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:733:0: 'WeightedReplacement.E_loop_fixed_row_target' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:822:0: 'WeightedReplacement.prefixRun_eq_of_eq_off' depends on axioms: [propext, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:823:0: 'WeightedReplacement.prefixRun_update' depends on axioms: [propext, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:824:0: 'WeightedReplacement.prefix_event_update' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:941:0: 'WeightedReplacement.oracleImpl_overwrite' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:942:0: 'WeightedReplacement.hybridPrefix_overwrite' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle04.lean:1040:50: This simp argument is unused:
  E_pure

Hint: Omit it from the simp argument list.
  [apply] simp [publicHit, hybridPrefix_pure]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle04.lean:1053:14: This simp argument is unused:
  E_pure

Hint: Omit it from the simp argument list.
  [apply] simp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/ProofBundle04.lean:1146:0: 'WeightedReplacement.publicHit_eq_prefix' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:1147:0: 'WeightedReplacement.publicHit_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:1148:0: 'WeightedReplacement.publicHit_sum_le_indexPaid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:1149:0: 'WeightedReplacement.paid_shared_budget' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:1976:0: 'OptimalOTS.WeightedConstruction.WideForest.card_updHash_input_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:1977:0: 'OptimalOTS.WeightedConstruction.WideForest.card_updSrc_input_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:1978:0: 'OptimalOTS.WeightedConstruction.WideForest.not_spr_kc' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:2523:0: 'OptimalOTS.WeightedConstruction.WideForest.hits_charge_A' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:2524:0: 'OptimalOTS.WeightedConstruction.WideForest.hits_charge_B' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:2526:0: 'OptimalOTS.WeightedConstruction.WideForest.hits_charge_A' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle04.lean:2527:0: 'OptimalOTS.WeightedConstruction.WideForest.hits_charge_B' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8813/8856] Built Submissions.UpperCompressions.ProofBundle05 (9.6s)
info: Submissions/UpperCompressions/ProofBundle05.lean:144:0: 'OptimalOTS.WeightedConstruction.WideForest.spr_charge' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:145:0: 'OptimalOTS.WeightedConstruction.WideForest.authentication_charge_budget' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle05.lean:160:38: Variable name `ξ` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ξ

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: Submissions/UpperCompressions/ProofBundle05.lean:382:0: 'OptimalOTS.WeightedConstruction.WideForest.authPotential_charge' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:383:0: 'OptimalOTS.WeightedConstruction.WideForest.joint_continuation' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle05.lean:412:40: Variable name `ξ` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ξ

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: Submissions/UpperCompressions/ProofBundle05.lean:490:0: 'OptimalOTS.WeightedConstruction.WideForest.fiber_weights_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:491:0: 'OptimalOTS.WeightedConstruction.WideForest.fiber_continuation' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle05.lean:515:30: This simp argument is unused:
  E_pure

Hint: Omit it from the simp argument list.
  [apply] simp [run_pure]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/ProofBundle05.lean:533:0: 'WeightedExpectedCharge.master_expected' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:625:0: 'OptimalOTS.WeightedConstruction.WideForest.authPotential_after_sign' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:717:0: 'OptimalOTS.WeightedConstruction.WideForest.auth_query_expected' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:718:0: 'OptimalOTS.WeightedConstruction.WideForest.auth_continuation_expected' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:719:0: 'OptimalOTS.WeightedConstruction.WideForest.fiber_auth_expected' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:814:0: 'OptimalOTS.ReplacementLocality.loop_new_cache_row' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:815:0: 'OptimalOTS.ReplacementLocality.sign_new_cache_row' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:852:0: 'OptimalOTS.WeightedConstruction.WideForest.authPotential_after_actual_sign' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:1002:0: 'OptimalOTS.WeightedConstruction.WideForest.fiber_costs_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:1003:0: 'OptimalOTS.WeightedConstruction.WideForest.postsign_auth_expected' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:1004:0: 'OptimalOTS.WeightedConstruction.WideForest.actual_sign_auth_expected' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:1005:0: 'OptimalOTS.WeightedConstruction.WideForest.record_shared_paid_budget' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:1529:0: 'OptimalOTS.WeightedConstruction.WideForest.events_none' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:1530:0: 'OptimalOTS.WeightedConstruction.WideForest.events_ne' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:1531:0: 'OptimalOTS.WeightedConstruction.WideForest.events_same' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:1587:0: 'OptimalOTS.WeightedScheme.verify_support' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:1649:0: 'OptimalOTS.WeightedConstruction.WideForest.accepted_none_event' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:1650:0: 'OptimalOTS.WeightedConstruction.WideForest.accepted_class_cases' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:1699:0: 'OptimalOTS.WeightedConstruction.WideForest.accepted_strong_event' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle05.lean:1779:0: 'OptimalOTS.WeightedConstruction.WideForest.postsign_continuation' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8814/8856] Built Submissions.UpperCompressions.LongChain91Geometry (54s)
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:142:37: This simp argument is unused:
  lowerOfChain

Hint: Omit it from the simp argument list.
  [apply] simp only [Name.idx, upperOfLower, upperOfChain]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:363:14: Variable name `ab` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ab

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:740:14: Variable name `f` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _f

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:804:21: Variable name `a` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _a

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:804:31: Variable name `b` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:804:41: Variable name `g` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _g

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:870:3: Variable name `x` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _x

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:1018:27: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:1018:27: Unused tactic linter: `contradiction` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:1033:27: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:1033:27: Unused tactic linter: `contradiction` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:1047:26: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:1049:26: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:1047:26: Unused tactic linter: `contradiction` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:1049:26: Unused tactic linter: `contradiction` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:1110:19: This simp argument is unused:
  hl

Hint: Omit it from the simp argument list.
  [apply] simp only

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:1113:19: This simp argument is unused:
  hl

Hint: Omit it from the simp argument list.
  [apply] simp only

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:1122:48: Variable name `hw` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hw

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:1148:25: This simp argument is unused:
  hl

Hint: Omit it from the simp argument list.
  [apply] simp only

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/LongChain91Geometry.lean:1151:19: This simp argument is unused:
  hl

Hint: Omit it from the simp argument list.
  [apply] simp only

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [8815/8856] Built Submissions.UpperCompressions.CompactSchedule91 (56s)
warning: Submissions/UpperCompressions/CompactSchedule91.lean:1173:46: Variable name `hx` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hx

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: Submissions/UpperCompressions/CompactSchedule91.lean:1401:0: 'OptimalOTS.Chain18Compact.familyCardinality_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/CompactSchedule91.lean:1402:0: 'OptimalOTS.Chain18Compact.acceptedAliases_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/CompactSchedule91.lean:1403:0: 'OptimalOTS.Chain18Compact.moment_envelopes' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/CompactSchedule91.lean:1404:0: 'OptimalOTS.Chain18Compact.exact_sum_g' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/CompactSchedule91.lean:1405:0: 'OptimalOTS.Chain18Compact.collisionAwareAvailability' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8816/8856] Built Submissions.UpperCompressions.ProofBundle06 (9.2s)
info: Submissions/UpperCompressions/ProofBundle06.lean:123:0: 'OptimalOTS.WeightedConstruction.WideForest.stB_events_some' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:124:0: 'OptimalOTS.WeightedConstruction.WideForest.stB_iub_some' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:200:0: 'OptimalOTS.WeightedConstruction.WideForest.stBWithForgery_map' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:201:0: 'OptimalOTS.WeightedConstruction.WideForest.stBWithForgery_index_witness' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:368:0: 'OptimalOTS.WeightedConstruction.WideForest.stageA_auth_expected' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:369:0: 'OptimalOTS.WeightedConstruction.WideForest.no_sign_auth_expected' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:370:0: 'OptimalOTS.WeightedConstruction.WideForest.stB_iub_none' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:371:0: 'OptimalOTS.WeightedConstruction.WideForest.failed_sign_success_expected' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle06.lean:393:30: This simp argument is unused:
  E_pure

Hint: Omit it from the simp argument list.
  [apply] simp [run_pure]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/ProofBundle06.lean:428:0: 'WeightedReplacement.expectedCharge_bind' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:429:0: 'WeightedReplacement.expectedCharge_map' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:430:0: 'WeightedReplacement.expectedCharge_three_phases' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:513:0: 'WeightedReplacement.loop_otherPaid_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:514:0: 'WeightedReplacement.sign_otherPaid_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:515:0: 'WeightedReplacement.sign_post_otherPaid' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle06.lean:562:30: This simp argument is unused:
  E_pure

Hint: Omit it from the simp argument list.
  [apply] simp [run_pure]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/ProofBundle06.lean:624:0: 'WeightedReplacement.publicHit_bind_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:625:0: 'WeightedReplacement.publicHit_query_output' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:626:0: 'WeightedReplacement.selected_input_union' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle06.lean:746:20: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:756:41: This simp argument is unused:
  Nat.not_lt

Hint: Omit it from the simp argument list.
  [apply] simp [weakRank, lowerRank]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/ProofBundle06.lean:794:0: 'WeightedReplacement.fraction_update' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:795:0: 'WeightedReplacement.tableWinnerLikelihood_update' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:796:0: 'WeightedReplacement.updated_table_posterior_class_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:875:0: 'WeightedReplacement.finite_bayes_evidence_mixture_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:876:0: 'WeightedReplacement.coordinate_evidence_mixture_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:965:0: 'WeightedReplacement.E_taggedBind_event' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:966:0: 'WeightedReplacement.E_taggedPrefix_update' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:967:0: 'WeightedReplacement.E_taggedPrefix_ofReal' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:1091:0: 'WeightedReplacement.uniformMean_product' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:1092:0: 'WeightedReplacement.uniform_table_deficit' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:1220:0: 'WeightedReplacement.E_uniform_restrict' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:1221:0: 'WeightedReplacement.E_table_deficit' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:1222:0: 'WeightedReplacement.full_table_bad_probability' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:1381:0: 'WeightedReplacement.finite_likelihood_joint' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:1382:0: 'WeightedReplacement.coordinate_uniform_joint' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:1383:0: 'WeightedReplacement.resampledSignedPrefix_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle06.lean:1424:42: This simp argument is unused:
  Ne.symm hq

Hint: Omit it from the simp argument list.
  [apply] simp [overwrite, Function.update, hq, hη, Ne.symm hη, hc]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1424:58: This simp argument is unused:
  Ne.symm hη

Hint: Omit it from the simp argument list.
  [apply] simp [overwrite, Function.update, hq, Ne.symm hq, hη, hc]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1484:10: This simp argument is unused:
  Function.comp_def

Hint: Omit it from the simp argument list.
  [apply] simp [hret]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1538:27: Unused tactic linter: `congr 1` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1538:39: Unused tactic linter: `(try funext r)` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1538:58: Unused tactic linter: `split_ifs` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1538:72: Unused tactic linter: `rfl` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1551:27: Unused tactic linter: `congr 1` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1551:39: Unused tactic linter: `(try funext r)` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1551:58: Unused tactic linter: `split_ifs` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1551:72: Unused tactic linter: `rfl` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1538:27: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1538:39: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1538:58: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1538:72: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1551:27: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1551:39: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1551:58: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/ProofBundle06.lean:1551:72: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
info: Submissions/UpperCompressions/ProofBundle06.lean:1553:0: 'WeightedReplacement.actualSignedPrefix_fixed_row' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:1554:0: 'WeightedReplacement.actual_prefix_class_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:1695:0: 'WeightedReplacement.signedChosen_union' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:1696:0: 'WeightedReplacement.signedHit_actual_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle06.lean:1697:0: 'WeightedReplacement.integrated_signedChosen_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8817/8856] Built Submissions.UpperCompressions.LongChain91Codec (5.1s)
info: Submissions/UpperCompressions/LongChain91Codec.lean:231:0: 'OptimalOTS.WeightedConstruction.LongChain91Schedule.card_class' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Codec.lean:232:0: 'OptimalOTS.WeightedConstruction.LongChain91Schedule.card_alias' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Codec.lean:233:0: 'OptimalOTS.WeightedConstruction.LongChain91Schedule.decode_fiber' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Codec.lean:234:0: 'OptimalOTS.WeightedConstruction.LongChain91Schedule.rawTier_fiber' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Codec.lean:235:0: 'OptimalOTS.WeightedConstruction.LongChain91Schedule.accepted_count' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Codec.lean:236:0: 'OptimalOTS.WeightedConstruction.LongChain91Schedule.class_probability_real' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8818/8856] Built Submissions.UpperCompressions.LongChain91Dag (10s)
warning: Submissions/UpperCompressions/LongChain91Dag.lean:324:11: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Submissions/UpperCompressions/LongChain91Dag.lean:329:11: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Submissions/UpperCompressions/LongChain91Dag.lean:348:11: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Submissions/UpperCompressions/LongChain91Dag.lean:367:11: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Submissions/UpperCompressions/LongChain91Dag.lean:480:29: Variable name `hh` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hh

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: Submissions/UpperCompressions/LongChain91Dag.lean:487:0: 'OptimalOTS.WeightedConstruction.LongChain91.graph_keygenCost' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Dag.lean:488:0: 'OptimalOTS.WeightedConstruction.LongChain91.hash_output_width' depends on axioms: [propext]
info: Submissions/UpperCompressions/LongChain91Dag.lean:489:0: 'OptimalOTS.WeightedConstruction.LongChain91.input_costs' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8819/8856] Built Submissions.UpperCompressions.ProofBundle07 (8.6s)
info: Submissions/UpperCompressions/ProofBundle07.lean:213:0: 'WeightedReplacement.QuerySlice.preload_update_of_none' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:214:0: 'WeightedReplacement.E_uniform_update' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:215:0: 'WeightedReplacement.outE_finite_preload' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:290:0: 'WeightedReplacement.outE_length_preload' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:291:0: 'WeightedReplacement.outE_index342_preload' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:292:0: 'WeightedReplacement.preload_index342_outside' depends on axioms: [propext]
warning: Submissions/UpperCompressions/ProofBundle07.lean:326:44: This simp argument is unused:
  Ne.symm hr

Hint: Omit it from the simp argument list.
  [apply] simp [overwrite, Function.update, hr]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:330:20: This simp argument is unused:
  hrd

Hint: Omit it from the simp argument list.
  [apply] simp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:336:12: This simp argument is unused:
  hrd

Hint: Omit it from the simp argument list.
  [apply] simp [Function.update, hdd, Ne.symm hdd]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:336:39: This simp argument is unused:
  Ne.symm hdd

Hint: Omit it from the simp argument list.
  [apply] simp [hrd, Function.update, hdd]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/ProofBundle07.lean:412:0: 'WeightedReplacement.E_preload_resampling' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:413:0: 'WeightedReplacement.eager_prefix_class_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:547:0: 'WeightedReplacement.other_row_class_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:548:0: 'WeightedReplacement.eager_cross_row_class_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:663:0: 'WeightedReplacement.eager_fresh_hit_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:664:0: 'WeightedReplacement.eager_fresh_chosen_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:741:0: 'WeightedReplacement.loop_preload_extend' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:742:0: 'WeightedReplacement.eager_fresh_chosen_overlay_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:781:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.rawTier_eq_decodeTier' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:782:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.decodeTier_fiber' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:810:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.decode_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:811:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.acceptance_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle07.lean:851:39: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
info: Submissions/UpperCompressions/ProofBundle07.lean:893:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.sum_tier' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:894:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.tier_probability_eq' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:895:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.relative_class_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:1019:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.mean_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:1020:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.mean_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:1021:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.referenceWeight_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:1022:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.classProbability_sum' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:1023:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.referenceWeight_sum' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:1024:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.excess_mean_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:1119:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.securityWeights' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:1120:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.weight_ratio_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:1121:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.excessScore_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:1122:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.empirical_kernel_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle07.lean:1145:27: This simp argument is unused:
  eq_comm

Hint: Omit it from the simp argument list.
  [apply] simp [score]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1147:0: automatically included section variable(s) unused in theorem `WeightedCompletion.mean_sum`:
  [Nonempty Ω]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Nonempty Ω] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1152:0: automatically included section variable(s) unused in theorem `WeightedCompletion.mean_mul`:
  [Nonempty Ω]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Nonempty Ω] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1174:0: automatically included section variable(s) unused in theorem `WeightedCompletion.known_score`:
  [Fintype D]
  [Nonempty D]
  [DecidableEq D]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype D] [Nonempty D] [DecidableEq D] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
info: Submissions/UpperCompressions/ProofBundle07.lean:1237:0: 'WeightedCompletion.joint_good_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:1238:0: 'WeightedCompletion.completion_score' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle07.lean:1261:0: automatically included section variable(s) unused in theorem `WeightedCompletion.referencePayoff_nonneg`:
  [Fintype Ω]
  [Nonempty Ω]
  [Nonempty D]
  [Fintype I]
  [DecidableEq I]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype Ω] [Nonempty Ω] [Nonempty D] [Fintype I] [DecidableEq I] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1269:25: This simp argument is unused:
  ht

Hint: Omit it from the simp argument list.
  [apply] simp [score]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1271:22: This simp argument is unused:
  ht

Hint: Omit it from the simp argument list.
  [apply] simp only [score, Option.map_some, Option.getD_some]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1321:23: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
info: Submissions/UpperCompressions/ProofBundle07.lean:1363:0: 'WeightedCompletion.replay_reference_mean' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:1364:0: 'WeightedCompletion.replay_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:1365:0: 'WeightedCompletion.excess_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle07.lean:1383:0: automatically included section variable(s) unused in theorem `WeightedCompletion.selected_consistent`:
  [Fintype D]
  [Nonempty D]
  [DecidableEq D]
  [DecidableEq I]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype D] [Nonempty D] [DecidableEq D] [DecidableEq I] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1405:28: This simp argument is unused:
  score

Hint: Omit it from the simp argument list.
  [apply] simp [hs]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1405:35: This simp argument is unused:
  hs

Hint: Omit it from the simp argument list.
  [apply] simp [score]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1410:23: This simp argument is unused:
  hs

Hint: Omit it from the simp argument list.
  [apply] simp [score, ht]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1416:21: This simp argument is unused:
  hs

Hint: Omit it from the simp argument list.
  [apply] simp [score, hn, Ne.symm hba]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1416:25: This simp argument is unused:
  hn

Hint: Omit it from the simp argument list.
  [apply] simp [score, hs, Ne.symm hba]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1419:0: automatically included section variable(s) unused in theorem `WeightedCompletion.iidMean_sum`:
  [DecidableEq D]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq D] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1429:0: automatically included section variable(s) unused in theorem `WeightedCompletion.iidMean_mul_const`:
  [Nonempty D]
  [DecidableEq D]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Nonempty D] [DecidableEq D] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1439:0: automatically included section variable(s) unused in theorem `WeightedCompletion.iidMean_const`:
  [DecidableEq D]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq D] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1446:0: automatically included section variable(s) unused in theorem `WeightedCompletion.iidMean_mono`:
  [Nonempty D]
  [DecidableEq D]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Nonempty D] [DecidableEq D] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1472:25: This simp argument is unused:
  ht

Hint: Omit it from the simp argument list.
  [apply] simp [score, iidMean_const]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle07.lean:1474:22: This simp argument is unused:
  ht

Hint: Omit it from the simp argument list.
  [apply] simp only [score, Option.map_some, Option.getD_some]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/ProofBundle07.lean:1503:0: 'WeightedCompletion.iid_selected_score' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle07.lean:1504:0: 'WeightedCompletion.tableKernel_le' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8820/8856] Built Submissions.UpperCompressions.LongChain91CutBridge (5.7s)
info: Submissions/UpperCompressions/LongChain91CutBridge.lean:722:0: 'OptimalOTS.WeightedConstruction.LongChain91.family_root_not_mem' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CutBridge.lean:723:0: 'OptimalOTS.WeightedConstruction.LongChain91.family_no_hidden_source' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CutBridge.lean:724:0: 'OptimalOTS.WeightedConstruction.LongChain91.family_reconstructCost' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CutBridge.lean:725:0: 'OptimalOTS.WeightedConstruction.LongChain91.family_disclosure_and_nonce' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [8821/8856] Built Submissions.UpperCompressions.LongChain91SecurityData (12s)
info: Submissions/UpperCompressions/LongChain91SecurityData.lean:499:0: 'OptimalOTS.WeightedConstruction.LongChain91Security.securityWeights' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityData.lean:500:0: 'OptimalOTS.WeightedConstruction.LongChain91Security.decoder_law' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityData.lean:501:0: 'OptimalOTS.WeightedConstruction.LongChain91Security.empirical_kernel_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityData.lean:502:0: 'OptimalOTS.WeightedConstruction.LongChain91Security.securityWeights_mean_lt' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityData.lean:503:0: 'OptimalOTS.WeightedConstruction.LongChain91Security.score_square_sum_lt' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityData.lean:504:0: 'OptimalOTS.WeightedConstruction.LongChain91Security.probability_score_square_sum_lt' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityData.lean:505:0: 'OptimalOTS.WeightedConstruction.LongChain91Security.totalWinnerMass_eq' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityData.lean:506:0: 'OptimalOTS.WeightedConstruction.LongChain91Security.postSignPositive_lt' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityData.lean:507:0: 'OptimalOTS.WeightedConstruction.LongChain91Security.postSignExcess_lt' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8822/8856] Built Submissions.UpperCompressions.ProofBundle08 (7.6s)
info: Submissions/UpperCompressions/ProofBundle08.lean:38:0: 'WeightedCompletion.E_loop_fixed_row_score' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle08.lean:55:0: automatically included section variable(s) unused in theorem `WeightedCompletion.tableKernel_reference_le`:
  [Fintype Ω]
  [Nonempty Ω]
  [Nonempty D]
  [Fintype I]
  [DecidableEq I]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype Ω] [Nonempty Ω] [Nonempty D] [Fintype I] [DecidableEq I] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle08.lean:68:25: This simp argument is unused:
  ht

Hint: Omit it from the simp argument list.
  [apply] simp [score]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle08.lean:70:22: This simp argument is unused:
  ht

Hint: Omit it from the simp argument list.
  [apply] simp only [score, Option.map_some, Option.getD_some]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/ProofBundle08.lean:126:0: 'WeightedCompletion.replay_kernel_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:127:0: 'WeightedCompletion.excess_kernel_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle08.lean:158:0: automatically included section variable(s) unused in theorem `WeightedCompletion.completionTable_known`:
  [Fintype D]
  [Fintype W]
  [Nonempty W]
  [DecidableEq I]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype D] [Fintype W] [Nonempty W] [DecidableEq I] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle08.lean:169:0: automatically included section variable(s) unused in theorem `WeightedCompletion.uniformMean_indicator`:
  [Nonempty W]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Nonempty W] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
info: Submissions/UpperCompressions/ProofBundle08.lean:200:0: 'WeightedCompletion.uniformMean_coordinate' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:201:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.completion_decode_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle08.lean:225:47: This simp argument is unused:
  Nat.lt_succ_iff

Hint: Omit it from the simp argument list.
  [apply] simp [prefixLe, prefixLt]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/ProofBundle08.lean:331:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.prefixLe_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:332:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.weakRank_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:333:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.strictRank_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:398:0: 'WeightedReplacement.concrete_posterior_rate_ennreal_base_excess' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:399:0: 'WeightedReplacement.concrete_weak_mass_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:400:0: 'WeightedReplacement.concrete_posterior_rate_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:455:0: 'OptimalOTS.WeightedConstruction.WideForest.verifyForgery_queries_chosen' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:456:0: 'OptimalOTS.WeightedConstruction.WideForest.stBWithForgery_selected_input_union' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:623:0: 'OptimalOTS.WeightedConstruction.WideForest.concrete_fresh_overlay' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:624:0: 'OptimalOTS.WeightedConstruction.WideForest.forgery_replay_or_fresh' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:625:0: 'OptimalOTS.WeightedConstruction.WideForest.signed_success_replay_fresh' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:729:0: 'WeightedReplacement.signedCharge_remaining' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:730:0: 'WeightedReplacement.signed_excess_remaining' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:731:0: 'WeightedReplacement.integrated_shared_budget' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:732:0: 'WeightedReplacement.signedCharge_weighted_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:849:0: 'OptimalOTS.WeightedConstruction.WideForest.exists_encQuery_of_length' depends on axioms: [propext, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:850:0: 'OptimalOTS.WeightedConstruction.WideForest.preloaded_loop_indexExtension' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:851:0: 'OptimalOTS.WeightedConstruction.WideForest.signed_game_leaf' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:852:0: 'OptimalOTS.WeightedConstruction.WideForest.retained_success_eq' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:1033:0: 'OptimalOTS.WeightedConstruction.WideForest.signedAverage_fresh_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:1034:0: 'OptimalOTS.WeightedConstruction.WideForest.signedAverage_graph_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:1157:0: 'OptimalOTS.WeightedConstruction.WideForest.signed_cost_budget' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:1158:0: 'OptimalOTS.WeightedConstruction.WideForest.signed_winner_master' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:1271:0: 'OptimalOTS.WeightedConstruction.WideForest.none_fiber_leaf' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:1272:0: 'OptimalOTS.WeightedConstruction.WideForest.signed_none_master' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle08.lean:1427:32: This simp argument is unused:
  Finset.sum_add_distrib

Hint: Omit it from the simp argument list.
  [apply] simp only [Finset.mul_sum]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/ProofBundle08.lean:1442:0: 'OptimalOTS.WeightedConstruction.WideForest.conditionalGame_partition' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:1443:0: 'OptimalOTS.WeightedConstruction.WideForest.authRate_ofReal' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:1444:0: 'OptimalOTS.WeightedConstruction.WideForest.conditional_game_master' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:1529:0: 'OptimalOTS.WeightedSampling.loop_step_budget' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle08.lean:1530:0: 'OptimalOTS.WeightedSampling.loop_reserve' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8823/8856] Built Submissions.UpperCompressions.LongChain91Scheme (6.6s)
info: Submissions/UpperCompressions/LongChain91Scheme.lean:286:0: 'OptimalOTS.WeightedConstruction.LongChain91.typed_cost' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/LongChain91Scheme.lean:287:0: 'OptimalOTS.WeightedConstruction.LongChain91.typed_correct' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/LongChain91Scheme.lean:288:0: 'OptimalOTS.WeightedConstruction.LongChain91.typed_signingFailure' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Scheme.lean:289:0: 'OptimalOTS.WeightedConstruction.LongChain91.typed_signatureSize' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Scheme.lean:290:0: 'OptimalOTS.WeightedConstruction.LongChain91.typed_rejectsOversized' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Scheme.lean:291:0: 'OptimalOTS.WeightedConstruction.LongChain91.typed_keygenCost' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Scheme.lean:292:0: 'OptimalOTS.WeightedConstruction.LongChain91.typed_signCost' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/LongChain91Scheme.lean:293:0: 'OptimalOTS.WeightedConstruction.LongChain91.typed_verifyDeterministic' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Scheme.lean:294:0: 'OptimalOTS.WeightedConstruction.LongChain91.wire_admissible' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8824/8856] Built Submissions.UpperCompressions.LongChain91Auth (5.2s)
warning: Submissions/UpperCompressions/LongChain91Auth.lean:728:38: Variable name `ξ` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ξ

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: Submissions/UpperCompressions/LongChain91Auth.lean:923:0: 'OptimalOTS.WeightedConstruction.LongChain91.spr_charge' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/LongChain91Auth.lean:924:0: 'OptimalOTS.WeightedConstruction.LongChain91.authentication_charge_budget' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Auth.lean:925:0: 'OptimalOTS.WeightedConstruction.LongChain91.not_spr_kc' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/LongChain91Auth.lean:926:0: 'OptimalOTS.WeightedConstruction.LongChain91.authPotential_index' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Auth.lean:927:0: 'OptimalOTS.WeightedConstruction.LongChain91.authPotential_after_actual_sign' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8825/8856] Built Submissions.UpperCompressions.ProofBundle09 (9.6s)
info: Submissions/UpperCompressions/ProofBundle09.lean:184:0: 'OptimalOTS.WeightedConstruction.WideInitialGame.E_experiment' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:185:0: 'OptimalOTS.WeightedConstruction.WideInitialGame.keygen_remaining' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:186:0: 'OptimalOTS.WeightedConstruction.WideInitialGame.global_reduced' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:252:0: 'OptimalOTS.WeightedConstruction.WideInitialGame.afterChoose_eager' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:253:0: 'OptimalOTS.WeightedConstruction.WideInitialGame.conditional_eager' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle09.lean:326:34: This simp argument is unused:
  E_pure

Hint: Omit it from the simp argument list.
  [apply] simp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/ProofBundle09.lean:350:0: 'WeightedReplacement.runRemaining_project' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:351:0: 'WeightedReplacement.runRemaining_family_support' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:352:0: 'WeightedReplacement.expected_spent_remaining_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:395:0: 'WeightedReplacement.run_output_mem_support' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:396:0: 'WeightedReplacement.actual_loop_reserve' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle09.lean:429:2: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
warning: Submissions/UpperCompressions/ProofBundle09.lean:476:2: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
info: Submissions/UpperCompressions/ProofBundle09.lean:500:0: 'OptimalOTS.WeightedConstruction.WideInitialGame.global_reduced_clock' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:501:0: 'OptimalOTS.WeightedConstruction.WideInitialGame.choose_supported_sign_reserve' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:502:0: 'OptimalOTS.WeightedConstruction.WideInitialGame.experiment_choose_reserve' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:503:0: 'OptimalOTS.WeightedConstruction.WideInitialGame.choose_spent_remaining_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:611:0: 'OptimalOTS.WeightedConstruction.WideInitialGame.global_reduced_hits' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:612:0: 'OptimalOTS.WeightedConstruction.WideInitialGame.global_payoff_clock' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:689:0: 'OptimalOTS.WeightedConstruction.WideForest.conditional_actual_master' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:690:0: 'OptimalOTS.WeightedConstruction.WideForest.supportedPostBudget_of_experiment' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:691:0: 'OptimalOTS.WeightedConstruction.WideForest.global_actual_game_payoff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:760:0: 'OptimalOTS.WeightedConstruction.WideForest.conditional_le_fiber' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:761:0: 'OptimalOTS.WeightedConstruction.WideForest.global_actual_game_payoff_gated' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:804:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.decoder_law' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:877:0: 'OptimalOTS.WeightedConstruction.WideDomains.row_card' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:878:0: 'OptimalOTS.WeightedConstruction.WideDomains.seen_row_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:879:0: 'OptimalOTS.WeightedConstruction.WideDomains.fresh_counts_zero' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1025:0: 'WeightedRealExecution.realEval_bind' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1026:0: 'WeightedRealExecution.realEval_mono_of_support' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1027:0: 'WeightedRealExecution.realEval_const' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1028:0: 'WeightedRealExecution.ofReal_realEval' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1029:0: 'WeightedRealExecution.realEval_simulate_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1030:0: 'WeightedRealExecution.realEval_simulate_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle09.lean:1077:8: automatically included section variable(s) unused in theorem `WeightedRealExecution.realEval_map`:
  [Fintype α]
  [SampleableType α]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype α] [SampleableType α] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
info: Submissions/UpperCompressions/ProofBundle09.lean:1089:0: 'WeightedRealExecution.realEval_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1090:0: 'WeightedRealExecution.realEval_decoded_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle09.lean:1177:0: automatically included section variable(s) unused in theorem `WeightedDirectCache.hash_count_le_one`:
  [Fintype B]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype B] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
info: Submissions/UpperCompressions/ProofBundle09.lean:1210:0: 'WeightedDirectCache.hash_count_le_one' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1211:0: 'WeightedDirectCache.protected_count_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1213:0: 'WeightedDirectCache.protected_query_law' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1215:0: 'WeightedDirectCache.hash_query_law' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle09.lean:1380:0: automatically included section variable(s) unused in theorem `WeightedOracleExecution.state_bound_of_query_budget`:
  [spec.Inhabited]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [spec.Inhabited] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle09.lean:1428:8: automatically included section variable(s) unused in theorem `WeightedOracleExecution.firstHitRun_pure`:
  [spec.Inhabited]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [spec.Inhabited] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle09.lean:1434:8: automatically included section variable(s) unused in theorem `WeightedOracleExecution.firstHitRun_query_bind`:
  [spec.Inhabited]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [spec.Inhabited] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle09.lean:1484:19: This simp argument is unused:
  classify_clock

Hint: Omit it from the simp argument list.
  [apply] simp only [classify_value, bind_assoc, pure_bind]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/ProofBundle09.lean:1484:35: This simp argument is unused:
  classify_value

Hint: Omit it from the simp argument list.
  [apply] simp only [classify_clock, bind_assoc, pure_bind]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/ProofBundle09.lean:1491:0: 'WeightedOracleExecution.expected_simulate_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1492:0: 'WeightedOracleExecution.expected_stopped_step_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1493:0: 'WeightedOracleExecution.expected_stopped_simulate_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1494:0: 'WeightedOracleExecution.actual_exponential_tail' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1495:0: 'WeightedOracleExecution.actual_stopped_freedman' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1496:0: 'WeightedOracleExecution.state_bound_of_query_budget' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1497:0: 'WeightedOracleExecution.state_bound_of_protected_budget' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1498:0: 'WeightedOracleExecution.stopped_simulate_of_stop' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle09.lean:1499:0: 'WeightedOracleExecution.prob_stopped_hit_eq_firstHitRun' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8826/8856] Built Submissions.UpperCompressions.LongChain91AuthClosure (5.2s)
warning: Submissions/UpperCompressions/LongChain91AuthClosure.lean:94:32: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
info: Submissions/UpperCompressions/LongChain91AuthClosure.lean:747:0: 'OptimalOTS.WeightedConstruction.LongChain91.visited_iff_clear' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthClosure.lean:748:0: 'OptimalOTS.WeightedConstruction.LongChain91.yv_hash' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthClosure.lean:749:0: 'OptimalOTS.WeightedConstruction.LongChain91.up' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthClosure.lean:750:0: 'OptimalOTS.WeightedConstruction.LongChain91.accepted_none_event' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthClosure.lean:751:0: 'OptimalOTS.WeightedConstruction.LongChain91.accepted_none_expected' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8827/8856] Built Submissions.UpperCompressions.ProofBundle10 (8.6s)
warning: Submissions/UpperCompressions/ProofBundle10.lean:74:38: This simp argument is unused:
  zero_pow

Hint: Omit it from the simp argument list.
  [apply] simp only [Nat.cast_zero, mul_zero, sub_zero] at hcomp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/ProofBundle10.lean:94:0: 'WeightedActualMoments.actual_stopped_moments' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:153:0: 'WeightedOracleExecution.actual_linear_boundary' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle10.lean:260:4: Unused tactic linter: `change G * w.mean * (qCount s : ℝ) ≤ G ^ 2 * N` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
info: Submissions/UpperCompressions/ProofBundle10.lean:305:0: 'WeightedActualScore.mixed_global' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:306:0: 'WeightedActualScore.mixed_row' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:308:0: 'WeightedActualScore.query_mgf' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:309:0: 'WeightedActualScore.global_boundary' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:310:0: 'WeightedActualScore.row_freedman' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:402:0: 'WeightedProtectedCache.count_le_cost' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:403:0: 'WeightedProtectedCache.count_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:404:0: 'WeightedProtectedCache.stopped_moments' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:406:0: 'WeightedProtectedCache.protectedImpl_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:407:0: 'WeightedProtectedCache.query_law' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:443:0: 'OptimalOTS.WeightedConstruction.WidePreSign.primitive_law' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:444:0: 'OptimalOTS.WeightedConstruction.WidePreSign.index_initial' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:524:0: 'WeightedProtectedCache.global_score' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:525:0: 'WeightedProtectedCache.row_score' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle10.lean:540:0: automatically included section variable(s) unused in theorem `WeightedCacheCounts.classCounts_mono`:
  [DecidableEq D]
  [Fintype ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq D] [Fintype ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
info: Submissions/UpperCompressions/ProofBundle10.lean:572:0: 'OptimalOTS.WeightedConstruction.WideDomains.row_class_le_global' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:573:0: 'OptimalOTS.WeightedConstruction.WideDomains.fresh_row_succ_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:686:0: 'OptimalOTS.WeightedConstruction.WideConcentration.global_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:687:0: 'OptimalOTS.WeightedConstruction.WideConcentration.row_withScore_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:688:0: 'OptimalOTS.WeightedConstruction.WideConcentration.row_excess_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle10.lean:819:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
info: Submissions/UpperCompressions/ProofBundle10.lean:829:0: 'WeightedOracleExecution.stopped_hit_union_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:830:0: 'WeightedOracleExecution.stopped_mixed_union' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:831:0: 'WeightedOracleExecution.terminal_bad_le_firstHit' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:833:0: 'WeightedOracleExecution.firstHitRun_union_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:834:0: 'WeightedOracleExecution.stopped_hit_union_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:943:0: 'OptimalOTS.WeightedConstruction.WideEmpirical.all_crossings' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:944:0: 'OptimalOTS.WeightedConstruction.WideEmpirical.terminal_bad' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle10.lean:965:0: automatically included section variable(s) unused in theorem `OptimalOTS.WeightedConstruction.WeightedSchedule.rowGood_kernel`:
  [Nonempty D]
  [DecidableEq D]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Nonempty D] [DecidableEq D] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
info: Submissions/UpperCompressions/ProofBundle10.lean:1013:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.concrete_replay_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:1014:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.concrete_excess_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:1087:0: 'OptimalOTS.WeightedConstruction.WideEmpirical.good_global' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:1088:0: 'OptimalOTS.WeightedConstruction.WideEmpirical.good_row_score' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:1089:0: 'OptimalOTS.WeightedConstruction.WideEmpirical.good_prefix' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:1090:0: 'OptimalOTS.WeightedConstruction.WideEmpirical.good_excess_payoff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle10.lean:1105:0: automatically included section variable(s) unused in theorem `WeightedCacheCounts.seen_image`:
  [DecidableEq D]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq D] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle10.lean:1119:0: automatically included section variable(s) unused in theorem `WeightedCacheCounts.counts_image`:
  [Fintype I]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype I] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Submissions/UpperCompressions/ProofBundle10.lean:1189:24: This simp argument is unused:
  hs

Hint: Omit it from the simp argument list.
  [apply] simp [score]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/ProofBundle10.lean:1215:0: 'OptimalOTS.WeightedConstruction.WideCachedRow.exposed_card' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:1216:0: 'OptimalOTS.WeightedConstruction.WideCachedRow.fixed_counts' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:1217:0: 'OptimalOTS.WeightedConstruction.WideCachedRow.cached_fresh_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:1218:0: 'OptimalOTS.WeightedConstruction.WideCachedRow.actual_sign_payoff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle10.lean:1349:0: 'WeightedReplacement.cacheE_finite_completion' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8828/8856] Built Submissions.UpperCompressions.ProofBundle11 (8.3s)
info: Submissions/UpperCompressions/ProofBundle11.lean:116:0: 'WeightedReplacement.completed_bad_probability_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:117:0: 'WeightedReplacement.completed_full_bad_probability' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:118:0: 'WeightedReplacement.completed_chosen_row_bad_probability' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:221:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.fullTableGood_row' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:222:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.fullTableGood_kernel' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:223:0: 'OptimalOTS.WeightedConstruction.WeightedSchedule.fullTableGood_bad_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:268:0: 'WeightedReplacement.actual_rowGood_completion_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:376:0: 'OptimalOTS.WeightedConstruction.WideCachedRow.actual_replay_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:377:0: 'OptimalOTS.WeightedConstruction.WideCachedRow.actual_excess_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:378:0: 'OptimalOTS.WeightedConstruction.WideCachedRow.tableFailure_average' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:488:0: 'OptimalOTS.WeightedConstruction.WideCachedRow.alternative_replayScore' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:489:0: 'OptimalOTS.WeightedConstruction.WideCachedRow.actual_alternative_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle11.lean:546:5: Variable name `hq` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hq

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: Submissions/UpperCompressions/ProofBundle11.lean:569:0: 'WeightedBudgetClosure.small_payoff' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:570:0: 'WeightedBudgetClosure.large_payoff' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle11.lean:599:4: Try this: 
  haveI̵

The goal is a proposition, so `have` is preferred over `haveI`.
The difference between `have` and `haveI` is that `haveI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
info: Submissions/UpperCompressions/ProofBundle11.lean:606:0: 'WeightedReplacement.costAtMost_prefix_reserved' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:649:0: 'OptimalOTS.WeightedConstruction.WideInitialGame.choose_reserved_budget' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:650:0: 'OptimalOTS.WeightedConstruction.WideInitialGame.experiment_full_reserve' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:696:0: 'WeightedReplacement.expected_spent_reserved_remaining_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:746:0: 'OptimalOTS.WeightedConstruction.WideInitialGame.choose_spent_post_remaining_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:747:0: 'OptimalOTS.WeightedConstruction.WideInitialGame.global_public_clock_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:930:0: 'OptimalOTS.WeightedConstruction.WideForest.signer_replay_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:931:0: 'OptimalOTS.WeightedConstruction.WideForest.concrete_continuation_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:932:0: 'OptimalOTS.WeightedConstruction.WideForest.weightedClock_tableError_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:933:0: 'OptimalOTS.WeightedConstruction.WideForest.global_actual_payoff_expanded' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:1008:0: 'OptimalOTS.WeightedConstruction.WideStoppedPayoff.moments' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:1009:0: 'OptimalOTS.WeightedConstruction.WideStoppedPayoff.small_payoff_actual' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:1054:0: 'WeightedRealExecution.ofReal_realEval_on_support' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle11.lean:1095:26: Variable name `ht` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ht

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: Submissions/UpperCompressions/ProofBundle11.lean:1157:0: 'OptimalOTS.WeightedConstruction.WideStoppedPayoff.actual_small_shared_ennreal' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:1158:0: 'OptimalOTS.WeightedConstruction.WideStoppedPayoff.hazard_le_pairEnvelope' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle11.lean:1159:0: 'OptimalOTS.WeightedConstruction.WideStoppedPayoff.actual_small_shared_real' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8829/8856] Built Submissions.UpperCompressions.ProofBundle12 (9.4s)
warning: Submissions/UpperCompressions/ProofBundle12.lean:42:0: automatically included section variable(s) unused in theorem `WeightedDualCache.after_comp`:
  [Fintype ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
info: Submissions/UpperCompressions/ProofBundle12.lean:118:0: 'WeightedDualCache.protected_query_law' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle12.lean:135:0: automatically included section variable(s) unused in theorem `WeightedDualCache.hash_payoff_support`:
  [Fintype B]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype B] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
info: Submissions/UpperCompressions/ProofBundle12.lean:197:0: 'WeightedDualCache.protected_payoff_support' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:243:0: 'WeightedDualCache.actual_query_law' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:244:0: 'WeightedDualCache.actual_payoff_support' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle12.lean:263:0: automatically included section variable(s) unused in theorem `WeightedDualCache.phase_steps`:
  [SampleableType B]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [SampleableType B] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
info: Submissions/UpperCompressions/ProofBundle12.lean:325:0: 'WeightedDualCache.actual_seen_count' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:378:0: 'WeightedDualCache.expected_seen_le_indexPaid' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:410:0: 'OptimalOTS.WeightedConstruction.WideDomains.distinct_index_le_expected_paid' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:411:0: 'OptimalOTS.WeightedConstruction.WideDomains.distinct_other_remaining_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
warning: Submissions/UpperCompressions/ProofBundle12.lean:478:2: exponent 512 exceeds the threshold 256, exponentiation operation was not evaluated, use `set_option exponentiation.threshold <num>` to set a new threshold
info: Submissions/UpperCompressions/ProofBundle12.lean:481:0: 'WeightedHazardConstants.large_exponent' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:482:0: 'WeightedHazardConstants.message_union_margin' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:483:0: 'WeightedHazardConstants.all_exception_margin' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:547:0: 'WeightedBudgetClosure.large_shared_ennreal' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:548:0: 'WeightedBudgetClosure.all_exception_margin_ennreal' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:698:0: 'OptimalOTS.WeightedConstruction.WideSmallSecurity.actual_small_security' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:699:0: 'OptimalOTS.WeightedConstruction.WideSmallSecurity.choose_shared_clock' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:700:0: 'OptimalOTS.WeightedConstruction.WideSmallSecurity.bad_gate_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:701:0: 'OptimalOTS.WeightedConstruction.WideSmallSecurity.small_core_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:802:0: 'OptimalOTS.WeightedConstruction.WideHazard.primitive_delta_law' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:803:0: 'OptimalOTS.WeightedConstruction.WideHazard.inside_rowCount_succ_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:804:0: 'OptimalOTS.WeightedConstruction.WideHazard.primitive_delta_support' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:966:0: 'OptimalOTS.WeightedConstruction.WideHazard.actual_drift_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:967:0: 'OptimalOTS.WeightedConstruction.WideHazard.gain_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:968:0: 'OptimalOTS.WeightedConstruction.WideHazard.actual_variance_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:969:0: 'OptimalOTS.WeightedConstruction.WideHazard.centered_delta_abs_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:970:0: 'OptimalOTS.WeightedConstruction.WideHazard.actual_centered_abs_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:1063:0: 'OptimalOTS.WeightedConstruction.WideHazard.good_global_seen' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:1064:0: 'OptimalOTS.WeightedConstruction.WideHazard.good_delta_drift' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:1065:0: 'OptimalOTS.WeightedConstruction.WideHazard.good_gain_mean' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:1132:0: 'OptimalOTS.WeightedConstruction.WideHazard.good_delta_mgf' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:1133:0: 'OptimalOTS.WeightedConstruction.WideHazard.actual_good_delta_mgf' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:1233:0: 'OptimalOTS.WeightedConstruction.WideHazard.actual_potential_step' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:1234:0: 'OptimalOTS.WeightedConstruction.WideHazard.W_budget_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:1295:0: 'OptimalOTS.WeightedConstruction.WideHazard.ZW_initial' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle12.lean:1296:0: 'OptimalOTS.WeightedConstruction.WideHazard.stopped_large_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8830/8856] Built Submissions.UpperCompressions.CollisionCache91 (4.5s)
warning: Submissions/UpperCompressions/CollisionCache91.lean:295:17: This simp argument is unused:
  hfresh

Hint: Omit it from the simp argument list.
  [apply] simp only [step, Bool.false_eq_true, ite_false, expect_const]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/CollisionCache91.lean:298:17: This simp argument is unused:
  hfresh

Hint: Omit it from the simp argument list.
  [apply] simp only [step, ite_true]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/CollisionCache91.lean:329:17: This simp argument is unused:
  hfresh

Hint: Omit it from the simp argument list.
  [apply] simp only [step, Bool.false_eq_true, ite_false, expect_const]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/CollisionCache91.lean:332:17: This simp argument is unused:
  hfresh

Hint: Omit it from the simp argument list.
  [apply] simp only [step, ite_true]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/CollisionCache91.lean:385:24: This simp argument is unused:
  ha

Hint: Omit it from the simp argument list.
  [apply] simp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/CollisionCache91.lean:386:26: This simp argument is unused:
  ha

Hint: Omit it from the simp argument list.
  [apply] simp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/CollisionCache91.lean:477:17: This simp argument is unused:
  hs

Hint: Omit it from the simp argument list.
  [apply] simp only [after, expect_const]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/CollisionCache91.lean:480:17: This simp argument is unused:
  hs

Hint: Omit it from the simp argument list.
  [apply] simp only [after, expect_const]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/CollisionCache91.lean:483:17: This simp argument is unused:
  hs

Hint: Omit it from the simp argument list.
  [apply] simp only [after]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/CollisionCache91.lean:569:0: 'EqualityCollisionCache91.actual_clock_law' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/CollisionCache91.lean:570:0: 'EqualityCollisionCache91.actual_D_martingale' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/CollisionCache91.lean:571:0: 'EqualityCollisionCache91.actual_Qfwd_supermartingale' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/CollisionCache91.lean:572:0: 'EqualityCollisionCache91.actual_xPhi_step' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/CollisionCache91.lean:573:0: 'EqualityCollisionCache91.actual_stopped_x_freedman' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8831/8856] Built Submissions.UpperCompressions.ProofBundle13 (6.4s)
info: Submissions/UpperCompressions/ProofBundle13.lean:120:0: 'WeightedOracleExecution.terminal_union_or_kill_le_stopped' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:121:0: 'WeightedOracleExecution.terminal_union_le_stopped' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:246:0: 'OptimalOTS.WeightedConstruction.WideHazard.terminal_hits_or_bad_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:247:0: 'OptimalOTS.WeightedConstruction.WideHazard.actual_large_good_hazard_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:248:0: 'OptimalOTS.WeightedConstruction.WideHazard.terminal_hits_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:249:0: 'OptimalOTS.WeightedConstruction.WideHazard.actual_large_hazard_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:380:0: 'OptimalOTS.WeightedConstruction.WideForest.global_count_other_post_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:381:0: 'OptimalOTS.WeightedConstruction.WideForest.large_bad_clock_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:382:0: 'OptimalOTS.WeightedConstruction.WideForest.large_hazard_clock_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:438:0: 'OptimalOTS.WeightedConstruction.WideForest.actual_large_security' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:439:0: 'OptimalOTS.WeightedConstruction.WideForest.actual_large_security_strict' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:491:0: 'OptimalOTS.WeightedConstruction.WideBudgetEndpoints.experiment_budget' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:492:0: 'OptimalOTS.WeightedConstruction.WideBudgetEndpoints.raw_experiment_budget' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:493:0: 'OptimalOTS.WeightedConstruction.WideBudgetEndpoints.raw_secure_of_typed' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:556:0: 'OptimalOTS.WeightedConstruction.WideSecurityClosure.probTrue_eq_success' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:557:0: 'OptimalOTS.WeightedConstruction.WideSecurityClosure.security_rate' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:558:0: 'OptimalOTS.WeightedConstruction.WideSecurityClosure.typed_secure_of_bounds' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:583:0: 'OptimalOTS.WeightedConstruction.WideSecure.typed_secure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle13.lean:584:0: 'OptimalOTS.WeightedConstruction.WideSecure.raw_secure' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8832/8856] Built Submissions.UpperCompressions.LongChain91SecurityClosure (4.2s)
info: Submissions/UpperCompressions/LongChain91SecurityClosure.lean:68:0: 'OptimalOTS.WeightedConstruction.LongChain91BudgetEndpoints.experiment_budget' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityClosure.lean:69:0: 'OptimalOTS.WeightedConstruction.LongChain91BudgetEndpoints.raw_experiment_budget' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityClosure.lean:70:0: 'OptimalOTS.WeightedConstruction.LongChain91BudgetEndpoints.small_strict' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityClosure.lean:71:0: 'OptimalOTS.WeightedConstruction.LongChain91BudgetEndpoints.large_strict' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityClosure.lean:72:0: 'OptimalOTS.WeightedConstruction.LongChain91BudgetEndpoints.above_trivial_budget' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityClosure.lean:73:0: 'OptimalOTS.WeightedConstruction.LongChain91BudgetEndpoints.raw_secure_of_typed' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityClosure.lean:155:0: 'OptimalOTS.WeightedConstruction.LongChain91SecurityClosure.probTrue_eq_success' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityClosure.lean:156:0: 'OptimalOTS.WeightedConstruction.LongChain91SecurityClosure.security_rate' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityClosure.lean:157:0: 'OptimalOTS.WeightedConstruction.LongChain91SecurityClosure.successValue_le_one' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityClosure.lean:158:0: 'OptimalOTS.WeightedConstruction.LongChain91SecurityClosure.typed_secure_of_bounds' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SecurityClosure.lean:159:0: 'OptimalOTS.WeightedConstruction.LongChain91SecurityClosure.raw_secure_of_bounds' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8833/8856] Built Submissions.UpperCompressions.LongChain91Empirical (25s)
warning: Submissions/UpperCompressions/LongChain91Empirical.lean:55:18: This simp argument is unused:
  h

Hint: Omit it from the simp argument list.
  [apply] simp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/LongChain91Empirical.lean:56:20: This simp argument is unused:
  h

Hint: Omit it from the simp argument list.
  [apply] simp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/LongChain91Empirical.lean:106:52: This simp argument is unused:
  hx

Hint: Omit it from the simp argument list.
  [apply] simp [prefixLt, hr, WeightedCompletion.score]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/LongChain91Empirical.lean:120:52: This simp argument is unused:
  hx

Hint: Omit it from the simp argument list.
  [apply] simp [prefixLe, hr, WeightedCompletion.score]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/LongChain91Empirical.lean:184:48: This simp argument is unused:
  Nat.lt_succ_iff

Hint: Omit it from the simp argument list.
  [apply] simp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/LongChain91Empirical.lean:1006:0: 'OptimalOTS.WeightedConstruction.LongChain91Empirical.rawTier_full_output_fiber' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Empirical.lean:1007:0: 'OptimalOTS.WeightedConstruction.LongChain91Empirical.prefixLt_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Empirical.lean:1008:0: 'OptimalOTS.WeightedConstruction.LongChain91Empirical.prefixLe_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Empirical.lean:1009:0: 'OptimalOTS.WeightedConstruction.LongChain91Empirical.prefix_deficits_rowGood' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Empirical.lean:1010:0: 'OptimalOTS.WeightedConstruction.LongChain91Empirical.rowGood_kernel' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Empirical.lean:1011:0: 'OptimalOTS.WeightedConstruction.LongChain91Empirical.excessWeights_mean' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Empirical.lean:1012:0: 'OptimalOTS.WeightedConstruction.LongChain91Empirical.all_crossings' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Empirical.lean:1013:0: 'OptimalOTS.WeightedConstruction.LongChain91Empirical.terminal_bad' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Empirical.lean:1014:0: 'OptimalOTS.WeightedConstruction.LongChain91Empirical.good_prefix' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Empirical.lean:1015:0: 'OptimalOTS.WeightedConstruction.LongChain91Empirical.good_row_excess' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Empirical.lean:1016:0: 'OptimalOTS.WeightedConstruction.LongChain91Empirical.full_table_bad_probability160' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Empirical.lean:1017:0: 'OptimalOTS.WeightedConstruction.LongChain91Empirical.fullTableGood_kernel' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Empirical.lean:1018:0: 'OptimalOTS.WeightedConstruction.LongChain91Empirical.completed_full_bad_probability160' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Empirical.lean:1019:0: 'OptimalOTS.WeightedConstruction.LongChain91Empirical.actual_rowGood_completion_failure' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [8834/8856] Built Submissions.UpperCompressions.LongChain91Occupancy (4.9s)
info: Submissions/UpperCompressions/LongChain91Occupancy.lean:349:0: 'OptimalOTS.WeightedConstruction.LongChain91Occupancy.cap_mean' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Occupancy.lean:350:0: 'OptimalOTS.WeightedConstruction.LongChain91Occupancy.rowOverfull_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Occupancy.lean:351:0: 'OptimalOTS.WeightedConstruction.LongChain91Occupancy.full_table_overfull_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8835/8856] Built Submissions.UpperCompressions.LongChain91CachedRow (8.6s)
warning: Submissions/UpperCompressions/LongChain91CachedRow.lean:105:25: This simp argument is unused:
  hs

Hint: Omit it from the simp argument list.
  [apply] simp [score]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/LongChain91CachedRow.lean:501:0: 'OptimalOTS.WeightedConstruction.LongChain91CachedRow.exposed_card' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CachedRow.lean:502:0: 'OptimalOTS.WeightedConstruction.LongChain91CachedRow.cached_fresh_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CachedRow.lean:503:0: 'OptimalOTS.WeightedConstruction.LongChain91CachedRow.actual_sign_payoff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CachedRow.lean:504:0: 'OptimalOTS.WeightedConstruction.LongChain91CachedRow.actual_replay_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CachedRow.lean:505:0: 'OptimalOTS.WeightedConstruction.LongChain91CachedRow.good_excess_payoff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CachedRow.lean:506:0: 'OptimalOTS.WeightedConstruction.LongChain91CachedRow.actual_excess_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CachedRow.lean:507:0: 'OptimalOTS.WeightedConstruction.LongChain91CachedRow.tableFailure_average' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CachedRow.lean:508:0: 'OptimalOTS.WeightedConstruction.LongChain91CachedRow.fullTableGood_cached_kernel' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CachedRow.lean:509:0: 'OptimalOTS.WeightedConstruction.LongChain91CachedRow.actual_replay_bound_full' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CachedRow.lean:510:0: 'OptimalOTS.WeightedConstruction.LongChain91CachedRow.actual_excess_bound_full' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CachedRow.lean:511:0: 'OptimalOTS.WeightedConstruction.LongChain91CachedRow.alternate_replayScore' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CachedRow.lean:512:0: 'OptimalOTS.WeightedConstruction.LongChain91CachedRow.actual_alternative_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8836/8856] Built Submissions.UpperCompressions.LongChain91CollisionCap (5.7s)
warning: Submissions/UpperCompressions/LongChain91CollisionCap.lean:69:8: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/LongChain91CollisionCap.lean:69:8: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
info: Submissions/UpperCompressions/LongChain91CollisionCap.lean:284:0: 'OptimalOTS.WeightedConstruction.LongChain91CollisionCap.capTier_kernel_numerator' depends on axioms: [propext]
info: Submissions/UpperCompressions/LongChain91CollisionCap.lean:285:0: 'OptimalOTS.WeightedConstruction.LongChain91CollisionCap.capTier_kernelUpper_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CollisionCap.lean:286:0: 'OptimalOTS.WeightedConstruction.LongChain91CollisionCap.security_collisionMass_eq' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CollisionCap.lean:287:0: 'OptimalOTS.WeightedConstruction.LongChain91CollisionCap.collision_cap' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CollisionCap.lean:288:0: 'OptimalOTS.WeightedConstruction.LongChain91CollisionCap.completed_occupancyGood' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [8837/8856] Built Submissions.UpperCompressions.LongChain91BudgetArithmetic (4.8s)
info: Submissions/UpperCompressions/LongChain91BudgetArithmetic.lean:138:0: 'OptimalOTS.WeightedConstruction.LongChain91BudgetArithmetic.mean_margin_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91BudgetArithmetic.lean:139:0: 'OptimalOTS.WeightedConstruction.LongChain91BudgetArithmetic.authRate_le_postRate' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91BudgetArithmetic.lean:140:0: 'OptimalOTS.WeightedConstruction.LongChain91BudgetArithmetic.authRate_le_C_alpha' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91BudgetArithmetic.lean:141:0: 'OptimalOTS.WeightedConstruction.LongChain91BudgetArithmetic.postRate_le_C_alpha' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91BudgetArithmetic.lean:142:0: 'OptimalOTS.WeightedConstruction.LongChain91BudgetArithmetic.large_coefficient_identity' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91BudgetArithmetic.lean:143:0: 'OptimalOTS.WeightedConstruction.LongChain91BudgetArithmetic.large_scalar_closure' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91BudgetArithmetic.lean:144:0: 'OptimalOTS.WeightedConstruction.LongChain91BudgetArithmetic.small_coefficient_identity' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91BudgetArithmetic.lean:145:0: 'OptimalOTS.WeightedConstruction.LongChain91BudgetArithmetic.small_scalar_closure' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91BudgetArithmetic.lean:146:0: 'OptimalOTS.WeightedConstruction.LongChain91BudgetArithmetic.small_below_security' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91BudgetArithmetic.lean:147:0: 'OptimalOTS.WeightedConstruction.LongChain91BudgetArithmetic.large_below_security' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [8838/8856] Built Submissions.UpperCompressions.LongChain91StoppedCollision (4.6s)
info: Submissions/UpperCompressions/LongChain91StoppedCollision.lean:233:0: 'OptimalOTS.WeightedConstruction.LongChain91StoppedCollision.actual_stopped_collision_freedman' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91StoppedCollision.lean:234:0: 'OptimalOTS.WeightedConstruction.LongChain91StoppedCollision.completed_occupancy_failure_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91StoppedCollision.lean:235:0: 'OptimalOTS.WeightedConstruction.LongChain91StoppedCollision.completed_allRowsOccupancyGood' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91StoppedCollision.lean:236:0: 'OptimalOTS.WeightedConstruction.LongChain91StoppedCollision.actual_allRows_occupancy_failure_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91StoppedCollision.lean:237:0: 'OptimalOTS.WeightedConstruction.LongChain91StoppedCollision.actual_chosen_row_occupancy_kill_probability' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8839/8856] Built Submissions.UpperCompressions.LongChain91AuthGame (7.3s)
warning: Submissions/UpperCompressions/LongChain91AuthGame.lean:168:26: This simp argument is unused:
  Fin.ext_iff

Hint: Omit it from the simp argument list.
  [apply] simp_all

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/LongChain91AuthGame.lean:168:43: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Submissions/UpperCompressions/LongChain91AuthGame.lean:168:43: Unused tactic linter: `omega` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Submissions/UpperCompressions/LongChain91AuthGame.lean:209:44: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/UpperCompressions/LongChain91AuthGame.lean:282:37: This simp argument is unused:
  lowWord_lowWord

Hint: Omit it from the simp argument list.
  [apply] simp [coordOf, updHash_snd_self] at hz

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/LongChain91AuthGame.lean:289:37: This simp argument is unused:
  lowWord_lowWord

Hint: Omit it from the simp argument list.
  [apply] simp [coordOf, updHash_snd_self] at hz

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/LongChain91AuthGame.lean:294:37: This simp argument is unused:
  lowWord_lowWord

Hint: Omit it from the simp argument list.
  [apply] simp [coordOf, updHash_snd_self] at hz

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/LongChain91AuthGame.lean:1590:0: 'OptimalOTS.WeightedConstruction.LongChain91.authPotential_charge' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthGame.lean:1591:0: 'OptimalOTS.WeightedConstruction.LongChain91.events_same' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthGame.lean:1592:0: 'OptimalOTS.WeightedConstruction.LongChain91.accepted_class_cases' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthGame.lean:1593:0: 'OptimalOTS.WeightedConstruction.LongChain91.accepted_strong_event' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [8840/8856] Built Submissions.UpperCompressions.LongChain91Continuation (4.3s)
info: Submissions/UpperCompressions/LongChain91Continuation.lean:110:0: 'OptimalOTS.WeightedConstruction.LongChain91Continuation.direct_replay_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Continuation.lean:111:0: 'OptimalOTS.WeightedConstruction.LongChain91Continuation.direct_excess_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Continuation.lean:112:0: 'OptimalOTS.WeightedConstruction.LongChain91Continuation.concrete_postRate' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Continuation.lean:113:0: 'OptimalOTS.WeightedConstruction.LongChain91Continuation.direct_continuation_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [8841/8856] Built Submissions.UpperCompressions.LongChain91TailArithmetic (4.6s)
info: Submissions/UpperCompressions/LongChain91TailArithmetic.lean:72:0: 'OptimalOTS.WeightedConstruction.LongChain91TailArithmetic.completion_exception_margin' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91TailArithmetic.lean:73:0: 'OptimalOTS.WeightedConstruction.LongChain91TailArithmetic.completion_exception_margin_ennreal' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [8842/8856] Built Submissions.UpperCompressions.LongChain91SmallMoments (5.3s)
info: Submissions/UpperCompressions/LongChain91SmallMoments.lean:388:0: 'OptimalOTS.WeightedConstruction.LongChain91SmallMoments.moments' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SmallMoments.lean:389:0: 'OptimalOTS.WeightedConstruction.LongChain91SmallMoments.sharp_stopped_payoff_actual' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SmallMoments.lean:390:0: 'OptimalOTS.WeightedConstruction.LongChain91SmallMoments.stopped_core_actual' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SmallMoments.lean:391:0: 'OptimalOTS.WeightedConstruction.LongChain91SmallMoments.stopped_core_65_actual' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SmallMoments.lean:392:0: 'OptimalOTS.WeightedConstruction.LongChain91SmallMoments.small_coefficient_actual' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SmallMoments.lean:393:0: 'OptimalOTS.WeightedConstruction.LongChain91SmallMoments.queryCount_expectation_eq_ofReal' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SmallMoments.lean:394:0: 'OptimalOTS.WeightedConstruction.LongChain91SmallMoments.pairEnvelope_expectation_eq_ofReal' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SmallMoments.lean:395:0: 'OptimalOTS.WeightedConstruction.LongChain91SmallMoments.small_coefficient_ennreal' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SmallMoments.lean:396:0: 'OptimalOTS.WeightedConstruction.LongChain91SmallMoments.hazard_le_pairEnvelope' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8843/8856] Built Submissions.UpperCompressions.LongChain91AuthCrossCut (4.6s)
warning: Submissions/UpperCompressions/LongChain91AuthCrossCut.lean:38:23: This simp argument is unused:
  hl

Hint: Omit it from the simp argument list.
  [apply] simp only

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/LongChain91AuthCrossCut.lean:42:17: This simp argument is unused:
  hl

Hint: Omit it from the simp argument list.
  [apply] simp only [if_pos hj]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/LongChain91AuthCrossCut.lean:58:57: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/UpperCompressions/LongChain91AuthCrossCut.lean:75:61: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/UpperCompressions/LongChain91AuthCrossCut.lean:81:63: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/UpperCompressions/LongChain91AuthCrossCut.lean:108:24: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
info: Submissions/UpperCompressions/LongChain91AuthCrossCut.lean:439:0: 'OptimalOTS.WeightedConstruction.LongChain91.reconstructCost_cutOf_eq' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthCrossCut.lean:440:0: 'OptimalOTS.WeightedConstruction.LongChain91.family_reconstructCost_eq' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthCrossCut.lean:441:0: 'OptimalOTS.WeightedConstruction.LongChain91.exists_mem_evaluated_of_ne' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthCrossCut.lean:442:0: 'OptimalOTS.WeightedConstruction.LongChain91.crossCutAuthentication' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthCrossCut.lean:443:0: 'OptimalOTS.WeightedConstruction.LongChain91.accepted_strong_event_actual' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [8844/8856] Built Submissions.UpperCompressions.LongChain91CollisionArithmetic (4.7s)
info: Submissions/UpperCompressions/LongChain91CollisionArithmetic.lean:326:0: 'OptimalOTS.WeightedConstruction.LongChain91CollisionArithmetic.diagonalMean_eq' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CollisionArithmetic.lean:327:0: 'OptimalOTS.WeightedConstruction.LongChain91CollisionArithmetic.freshSquareMass_eq' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CollisionArithmetic.lean:328:0: 'OptimalOTS.WeightedConstruction.LongChain91CollisionArithmetic.diagonalMean_lt' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CollisionArithmetic.lean:329:0: 'OptimalOTS.WeightedConstruction.LongChain91CollisionArithmetic.freshSquareMass_lt' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CollisionArithmetic.lean:330:0: 'OptimalOTS.WeightedConstruction.LongChain91CollisionArithmetic.collisionMass_lt' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CollisionArithmetic.lean:331:0: 'OptimalOTS.WeightedConstruction.LongChain91CollisionArithmetic.large_hazard_exponent' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CollisionArithmetic.lean:332:0: 'OptimalOTS.WeightedConstruction.LongChain91CollisionArithmetic.message_union_margin' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CollisionArithmetic.lean:333:0: 'OptimalOTS.WeightedConstruction.LongChain91CollisionArithmetic.tight_mean_margin_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CollisionArithmetic.lean:334:0: 'OptimalOTS.WeightedConstruction.LongChain91CollisionArithmetic.large_scalar_closure_tight' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91CollisionArithmetic.lean:335:0: 'OptimalOTS.WeightedConstruction.LongChain91CollisionArithmetic.large_exception_margin' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [8845/8856] Built Submissions.UpperCompressions.LongChain91SmallShared (4.5s)
info: Submissions/UpperCompressions/LongChain91SmallShared.lean:178:0: 'OptimalOTS.WeightedConstruction.LongChain91SmallShared.small_payoff_actual' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SmallShared.lean:179:0: 'OptimalOTS.WeightedConstruction.LongChain91SmallShared.actual_small_shared_real' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SmallShared.lean:180:0: 'OptimalOTS.WeightedConstruction.LongChain91SmallShared.actual_small_shared_ennreal' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8846/8856] Built Submissions.UpperCompressions.LongChain91AuthActual (5.2s)
warning: Submissions/UpperCompressions/LongChain91AuthActual.lean:56:9: Variable name `xi` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _xi

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: Submissions/UpperCompressions/LongChain91AuthActual.lean:627:0: 'OptimalOTS.WeightedConstruction.LongChain91.stB_iub_some' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthActual.lean:628:0: 'OptimalOTS.WeightedConstruction.LongChain91.stBWithForgery_index_witness' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthActual.lean:629:0: 'OptimalOTS.WeightedConstruction.LongChain91.stageA_auth_expected' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthActual.lean:630:0: 'OptimalOTS.WeightedConstruction.LongChain91.failed_sign_success_expected' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthActual.lean:631:0: 'OptimalOTS.WeightedConstruction.LongChain91.actual_sign_auth_expected' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthActual.lean:632:0: 'OptimalOTS.WeightedConstruction.LongChain91.exists_encQuery_of_length' depends on axioms: [propext, Quot.sound]
ℹ [8847/8856] Built Submissions.UpperCompressions.LongChain91DiagonalClock (4.3s)
info: Submissions/UpperCompressions/LongChain91DiagonalClock.lean:295:0: 'OptimalOTS.WeightedConstruction.LongChain91DiagonalClock.collisionWeights_mean' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91DiagonalClock.lean:296:0: 'OptimalOTS.WeightedConstruction.LongChain91DiagonalClock.Drow_le_Dglobal' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91DiagonalClock.lean:297:0: 'OptimalOTS.WeightedConstruction.LongChain91DiagonalClock.Qfwd_le_Dglobal' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91DiagonalClock.lean:298:0: 'OptimalOTS.WeightedConstruction.LongChain91DiagonalClock.diagonal_rate_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91DiagonalClock.lean:299:0: 'OptimalOTS.WeightedConstruction.LongChain91DiagonalClock.global_diagonal_crossing_dyadic' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91DiagonalClock.lean:300:0: 'OptimalOTS.WeightedConstruction.LongChain91DiagonalClock.terminal_Dglobal_bad' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8848/8856] Built Submissions.UpperCompressions.LongChain91AuthConditional (6.3s)
info: Submissions/UpperCompressions/LongChain91AuthConditional.lean:144:0: 'OptimalOTS.WeightedConstruction.LongChain91.verifyForgery_queries_chosen' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthConditional.lean:145:0: 'OptimalOTS.WeightedConstruction.LongChain91.stBWithForgery_selected_input_union' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthConditional.lean:284:0: 'OptimalOTS.WeightedConstruction.LongChain91.concrete_fresh_overlay' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthConditional.lean:285:0: 'OptimalOTS.WeightedConstruction.LongChain91.forgery_replay_or_fresh' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthConditional.lean:286:0: 'OptimalOTS.WeightedConstruction.LongChain91.signed_success_replay_fresh' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthConditional.lean:534:0: 'OptimalOTS.WeightedConstruction.LongChain91.signedAverage_fresh_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthConditional.lean:535:0: 'OptimalOTS.WeightedConstruction.LongChain91.signedAverage_graph_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthConditional.lean:666:0: 'OptimalOTS.WeightedConstruction.LongChain91.signed_cost_budget' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthConditional.lean:760:0: 'OptimalOTS.WeightedConstruction.LongChain91.none_fiber_leaf' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthConditional.lean:761:0: 'OptimalOTS.WeightedConstruction.LongChain91.signed_none_master' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
warning: Submissions/UpperCompressions/LongChain91AuthConditional.lean:897:32: This simp argument is unused:
  Finset.sum_add_distrib

Hint: Omit it from the simp argument list.
  [apply] simp only [Finset.mul_sum]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/LongChain91AuthConditional.lean:912:0: 'OptimalOTS.WeightedConstruction.LongChain91.conditionalGame_partition' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthConditional.lean:913:0: 'OptimalOTS.WeightedConstruction.LongChain91.authRate_ofReal' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/LongChain91AuthConditional.lean:914:0: 'OptimalOTS.WeightedConstruction.LongChain91.conditional_game_master' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8849/8856] Built Submissions.UpperCompressions.LongChain91LargeHazard (5.2s)
warning: Submissions/UpperCompressions/LongChain91LargeHazard.lean:276:47: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/UpperCompressions/LongChain91LargeHazard.lean:479:17: This simp argument is unused:
  hs

Hint: Omit it from the simp argument list.
  [apply] simp only [gain, securityWeights.expect_const, globalStep, Nat.cast_zero, mul_zero]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/LongChain91LargeHazard.lean:476:8: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Submissions/UpperCompressions/LongChain91LargeHazard.lean:678:21: This simp argument is unused:
  hrow'

Hint: Omit it from the simp argument list.
  [apply] simp [Z, hazard, WeightedRow.Weights.hazard, WeightedRow.Weights.seen, WeightedRow.Weights.bad, hq', hk', hr']

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/LongChain91LargeHazard.lean:748:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeHazard.primitive_delta_law' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeHazard.lean:749:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeHazard.equality_clock_envelope' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeHazard.lean:750:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeHazard.gain_square_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeHazard.lean:751:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeHazard.actual_potential_step' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeHazard.lean:752:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeHazard.actual_stopped_large_hazard' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeHazard.lean:753:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeHazard.actual_stopped_self_collision' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8850/8856] Built Submissions.UpperCompressions.LongChain91LargeTerminal (5.5s)
warning: Submissions/UpperCompressions/LongChain91LargeTerminal.lean:42:10: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Submissions/UpperCompressions/LongChain91LargeTerminal.lean:130:45: This simp argument is unused:
  hh

Hint: Omit it from the simp argument list.
  [apply] simp only [firstHitRun_query_bind, hk, hnone, hknone, exists_false, if_false,
    probOutput_bind_eq_expectedValue]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/LongChain91LargeTerminal.lean:130:49: This simp argument is unused:
  hk

Hint: Omit it from the simp argument list.
  [apply] simp only [firstHitRun_query_bind, hh, hnone, hknone, exists_false, if_false,
    probOutput_bind_eq_expectedValue]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Submissions/UpperCompressions/LongChain91LargeTerminal.lean:198:45: This simp argument is unused:
  hh

Hint: Omit it from the simp argument list.
  [apply] simp only [firstHitRun_query_bind, hk, hnone, exists_false, or_false, if_false,
    probOutput_bind_eq_expectedValue]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Submissions/UpperCompressions/LongChain91LargeTerminal.lean:843:0: 'WeightedOracleExecution.firstHitRun_union_varying_kill_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeTerminal.lean:844:0: 'WeightedOracleExecution.firstHitRun_union_or_kill_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeTerminal.lean:845:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeTerminal.occupancy_crossing_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeTerminal.lean:846:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeTerminal.self_collision_exponent' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeTerminal.lean:847:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeTerminal.self_occupancy_crossing_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeTerminal.lean:848:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeTerminal.terminal_hits_or_cover_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeTerminal.lean:849:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeTerminal.actual_large_hazard_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeTerminal.lean:850:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeTerminal.actual_large_good_failure_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8851/8856] Built Submissions.UpperCompressions.LongChain91InitialGame (7.8s)
info: Submissions/UpperCompressions/LongChain91InitialGame.lean:185:0: 'OptimalOTS.WeightedConstruction.LongChain91InitialGame.E_experiment' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91InitialGame.lean:186:0: 'OptimalOTS.WeightedConstruction.LongChain91InitialGame.keygen_remaining' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91InitialGame.lean:187:0: 'OptimalOTS.WeightedConstruction.LongChain91InitialGame.global_reduced' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91InitialGame.lean:253:0: 'OptimalOTS.WeightedConstruction.LongChain91InitialGame.afterChoose_eager' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91InitialGame.lean:254:0: 'OptimalOTS.WeightedConstruction.LongChain91InitialGame.conditional_eager' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
warning: Submissions/UpperCompressions/LongChain91InitialGame.lean:287:2: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
warning: Submissions/UpperCompressions/LongChain91InitialGame.lean:334:2: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
info: Submissions/UpperCompressions/LongChain91InitialGame.lean:358:0: 'OptimalOTS.WeightedConstruction.LongChain91InitialGame.global_reduced_clock' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91InitialGame.lean:359:0: 'OptimalOTS.WeightedConstruction.LongChain91InitialGame.choose_supported_sign_reserve' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91InitialGame.lean:360:0: 'OptimalOTS.WeightedConstruction.LongChain91InitialGame.experiment_choose_reserve' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91InitialGame.lean:361:0: 'OptimalOTS.WeightedConstruction.LongChain91InitialGame.choose_spent_remaining_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91InitialGame.lean:469:0: 'OptimalOTS.WeightedConstruction.LongChain91InitialGame.global_reduced_hits' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91InitialGame.lean:470:0: 'OptimalOTS.WeightedConstruction.LongChain91InitialGame.global_payoff_clock' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91InitialGame.lean:547:0: 'OptimalOTS.WeightedConstruction.LongChain91.conditional_actual_master' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91InitialGame.lean:548:0: 'OptimalOTS.WeightedConstruction.LongChain91.supportedPostBudget_of_experiment' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91InitialGame.lean:549:0: 'OptimalOTS.WeightedConstruction.LongChain91.global_actual_game_payoff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91InitialGame.lean:618:0: 'OptimalOTS.WeightedConstruction.LongChain91.conditional_le_fiber' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91InitialGame.lean:619:0: 'OptimalOTS.WeightedConstruction.LongChain91.global_actual_game_payoff_gated' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [8852/8856] Built Submissions.UpperCompressions.LongChain91PayoffExpansion (4.6s)
info: Submissions/UpperCompressions/LongChain91PayoffExpansion.lean:50:0: 'OptimalOTS.WeightedConstruction.LongChain91InitialGame.choose_reserved_budget' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91PayoffExpansion.lean:51:0: 'OptimalOTS.WeightedConstruction.LongChain91InitialGame.experiment_full_reserve' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91PayoffExpansion.lean:101:0: 'OptimalOTS.WeightedConstruction.LongChain91InitialGame.choose_spent_post_remaining_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91PayoffExpansion.lean:102:0: 'OptimalOTS.WeightedConstruction.LongChain91InitialGame.global_public_clock_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91PayoffExpansion.lean:279:0: 'OptimalOTS.WeightedConstruction.LongChain91.signer_replay_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91PayoffExpansion.lean:280:0: 'OptimalOTS.WeightedConstruction.LongChain91.concrete_continuation_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91PayoffExpansion.lean:281:0: 'OptimalOTS.WeightedConstruction.LongChain91.weightedClock_tableError_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91PayoffExpansion.lean:282:0: 'OptimalOTS.WeightedConstruction.LongChain91.global_actual_payoff_expanded' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8853/8856] Built Submissions.UpperCompressions.LongChain91SmallSecurity (4.7s)
warning: Submissions/UpperCompressions/LongChain91SmallSecurity.lean:161:8: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
info: Submissions/UpperCompressions/LongChain91SmallSecurity.lean:176:0: 'OptimalOTS.WeightedConstruction.LongChain91SmallSecurity.actual_small_security' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SmallSecurity.lean:177:0: 'OptimalOTS.WeightedConstruction.LongChain91SmallSecurity.choose_shared_clock' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SmallSecurity.lean:178:0: 'OptimalOTS.WeightedConstruction.LongChain91SmallSecurity.bad_gate_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91SmallSecurity.lean:179:0: 'OptimalOTS.WeightedConstruction.LongChain91SmallSecurity.small_core_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8854/8856] Built Submissions.UpperCompressions.LongChain91LargeSecurity (4.8s)
warning: Submissions/UpperCompressions/LongChain91LargeSecurity.lean:282:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
info: Submissions/UpperCompressions/LongChain91LargeSecurity.lean:342:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeSecurity.large_scalar_closure_scaled' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeSecurity.lean:343:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeSecurity.large_shared_ennreal' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeSecurity.lean:344:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeSecurity.global_count_other_post_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeSecurity.lean:345:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeSecurity.large_bad_clock_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeSecurity.lean:346:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeSecurity.large_hazard_clock_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeSecurity.lean:347:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeSecurity.large_exception_margin_ennreal' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91LargeSecurity.lean:348:0: 'OptimalOTS.WeightedConstruction.LongChain91LargeSecurity.actual_large_security' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [8855/8856] Built Submissions.UpperCompressions.LongChain91Secure (3.8s)
info: Submissions/UpperCompressions/LongChain91Secure.lean:80:0: 'OptimalOTS.WeightedConstruction.LongChain91Secure.smallActualGameBound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Secure.lean:81:0: 'OptimalOTS.WeightedConstruction.LongChain91Secure.largeActualGameBound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Secure.lean:82:0: 'OptimalOTS.WeightedConstruction.LongChain91Secure.typed_secure' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/LongChain91Secure.lean:83:0: 'OptimalOTS.WeightedConstruction.LongChain91Secure.raw_secure' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
✔ [8856/8856] Built Submissions.UpperCompressions.Solution (3.6s)
Build completed successfully (8856 jobs).
Exporting #[OptimalOTS.Challenge.UpperCompressions.admissible, OptimalOTS.Challenge.UpperCompressions.secure, OptimalOTS.Challenge.UpperCompressions.cost, propext, Quot.sound, Classical.choice, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList, Char.ofNat, List, eagerReduce, OptimalOTS.Challenge.UpperCompressions.scheme] from Submissions.UpperCompressions.Solution
Running Lean default kernel on solution.
Lean default kernel accepts the solution
Your solution is okay!