Building OptimalOTS.Challenge.UpperCompressions
⚠ [2689/2689] Built OptimalOTS.Challenge.UpperCompressions (1.0s)
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 ToMathlib.MeasureTheory.Measure.IndependentDraws (2.1s)
✔ [8799/8821] Built ToMathlib.MeasureTheory.Measure.Bounds (2.1s)
✔ [8800/8821] Built ToMathlib.Probability.UniformOn (2.2s)
ℹ [8801/8821] Built Submissions.UpperCompressions.ProofBundle02 (6.2s)
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]
✔ [8802/8821] Built VCVio.OracleComp.QueryTracking.RandomOracle.Simulation (3.1s)
✔ [8803/8821] Built VCVio.EvalDist.Monad.Measure (1.4s)
✔ [8804/8821] Built ToMathlib.MeasureTheory.Measure.UniformTable (1.6s)
✔ [8805/8821] Built VCVio.OracleComp.Constructions.SampleableType.MeasureCompatibility (1.5s)
✔ [8806/8821] Built VCVio.EvalDist.Monad.UniformTable (1.4s)
✔ [8807/8821] Built VCVio.OracleComp.QueryTracking.RandomOracle.EagerTable (1.8s)
⚠ [8808/8821] Built Submissions.UpperCompressions.ProofBundle00 (77s)
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] Building Submissions.UpperCompressions.ProofBundle03 (12s)
trace: .> LEAN_PATH=/srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/packages/Cli/.lake/build/lib/lean:/srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/packages/cslib/.lake/build/lib/lean:/srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/packages/batteries/.lake/build/lib/lean:/srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/packages/Qq/.lake/build/lib/lean:/srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/packages/aesop/.lake/build/lib/lean:/srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/packages/proofwidgets/.lake/build/lib/lean:/srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/packages/importGraph/.lake/build/lib/lean:/srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/packages/plausible/.lake/build/lib/lean:/srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/packages/loom2/.lake/build/lib/lean:/srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/packages/PolyFun/.lake/build/lib/lean:/srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/packages/mathlib/.lake/build/lib/lean:/srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/packages/Sail/.lake/build/lib/lean:/srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/packages/VCVio/.lake/build/lib/lean:/srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/packages/riscv-zkvm/.lake/build/lib/lean:/srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/build/lib/lean /srv/ots/.elan/toolchains/leanprover--lean4---v4.33.1/bin/lean /srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/Submissions/UpperCompressions/ProofBundle03.lean -o /srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/build/lib/lean/Submissions/UpperCompressions/ProofBundle03.olean -i /srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/build/lib/lean/Submissions/UpperCompressions/ProofBundle03.ilean -c /srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/build/ir/Submissions/UpperCompressions/ProofBundle03.c --setup /srv/ots-work/6cf2a687d9fc89a1dd8f1cf4cba2211e/project/formal/.lake/build/ir/Submissions/UpperCompressions/ProofBundle03.setup.json --json
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]
error: Submissions/UpperCompressions/ProofBundle03.lean:2870:4: 'show' tactic failed, pattern
  graph.keygenCost ≤ 1024
is not definitionally equal to target
  graph.keygenCost ≤ keygenBudget
info: Submissions/UpperCompressions/ProofBundle03.lean:2918:0: 'OptimalOTS.WeightedConstruction.WideForest.typed_cost' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2919:0: 'OptimalOTS.WeightedConstruction.WideForest.typed_correct' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2920:0: 'OptimalOTS.WeightedConstruction.WideForest.typed_signatureSize' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2921:0: 'OptimalOTS.WeightedConstruction.WideForest.typed_rejectsOversized' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2922:0: 'OptimalOTS.WeightedConstruction.WideForest.typed_keygenCost' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2923:0: 'OptimalOTS.WeightedConstruction.WideForest.typed_signCost' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:2924:0: 'OptimalOTS.WeightedConstruction.WideForest.typed_verifyDeterministic' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:3122:0: 'OptimalOTS.WeightedConstruction.WideWire.cost' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:3123:0: 'OptimalOTS.WeightedConstruction.WideWire.correct' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:3124:0: 'OptimalOTS.WeightedConstruction.WideWire.signatureSize' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:3125:0: 'OptimalOTS.WeightedConstruction.WideWire.rejectsOversized' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:3126:0: 'OptimalOTS.WeightedConstruction.WideWire.keygenCost' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:3127:0: 'OptimalOTS.WeightedConstruction.WideWire.signCost' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:3128:0: 'OptimalOTS.WeightedConstruction.WideWire.verifyDeterministic' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ProofBundle03.lean:3269:0: 'OptimalOTS.WeightedSampling.Availability.loop_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
error: Lean exited with code 1
Some required targets logged failures:
- Submissions.UpperCompressions.ProofBundle03
error: build failed
uncaught exception: Child exited with 1