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/8821] Built Submissions.UpperCompressions.ProofBundle02 (5.7s)
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]
✔ [8799/8821] Built ToMathlib.MeasureTheory.Measure.IndependentDraws (1.8s)
✔ [8800/8821] Built ToMathlib.MeasureTheory.Measure.Bounds (1.7s)
✔ [8801/8821] Built ToMathlib.Probability.UniformOn (1.9s)
✔ [8802/8821] Built VCVio.OracleComp.QueryTracking.RandomOracle.Simulation (2.4s)
✔ [8803/8821] Built VCVio.EvalDist.Monad.Measure (1.3s)
✔ [8804/8821] Built ToMathlib.MeasureTheory.Measure.UniformTable (1.5s)
✔ [8805/8821] Built VCVio.OracleComp.Constructions.SampleableType.MeasureCompatibility (1.4s)
✔ [8806/8821] Built VCVio.EvalDist.Monad.UniformTable (1.4s)
✔ [8807/8821] Built VCVio.OracleComp.QueryTracking.RandomOracle.EagerTable (1.7s)
⚠ [8808/8821] Built Submissions.UpperCompressions.ProofBundle00 (76s)
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/8821] Built Submissions.UpperCompressions.ProofBundle01 (7.1s)
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]
⚠ [8810/8821] Built Submissions.UpperCompressions.ProofBundle03 (15s)
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]
⚠ [8811/8821] Built Submissions.UpperCompressions.ProofBundle04 (10s)
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]
⚠ [8812/8821] Built Submissions.UpperCompressions.ProofBundle05 (8.9s)
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]
⚠ [8813/8821] Built Submissions.UpperCompressions.ProofBundle06 (8.5s)
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]
⚠ [8814/8821] Built Submissions.UpperCompressions.ProofBundle07 (7.9s)
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]
⚠ [8815/8821] Built Submissions.UpperCompressions.ProofBundle08 (7.4s)
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]
⚠ [8816/8821] Built Submissions.UpperCompressions.ProofBundle09 (8.0s)
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]
⚠ [8817/8821] Built Submissions.UpperCompressions.ProofBundle10 (8.4s)
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]
⚠ [8818/8821] 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]
⚠ [8819/8821] Built Submissions.UpperCompressions.ProofBundle12 (8.6s)
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]
ℹ [8820/8821] 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]
✔ [8821/8821] Built Submissions.UpperCompressions.Solution (3.6s)
Build completed successfully (8821 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!