Building OptimalOTS.Challenge.UpperCompressions
⚠ [2689/2689] Built OptimalOTS.Challenge.UpperCompressions (3.2s)
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/8846] Built Submissions.UpperCompressions.TypedScheme (3.1s)
✔ [8799/8846] Built Submissions.UpperCompressions.Semantics (3.1s)
✔ [8800/8846] Built Submissions.UpperCompressions.Cache (3.3s)
ℹ [8801/8846] Built Submissions.UpperCompressions.ShallowAvailability (3.7s)
info: Submissions/UpperCompressions/ShallowAvailability.lean:63:0: 'AvailabilityCubic.block_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowAvailability.lean:64:0: 'AvailabilityCubic.signing_failure_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8802/8846] Built Submissions.UpperCompressions.ShallowNames (6.5s)
info: Submissions/UpperCompressions/ShallowNames.lean:493:0: 'OptimalOTS.ShallowForest.graph_keygenCost' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8803/8846] Built Submissions.UpperCompressions.Adapter (2.4s)
✔ [8804/8846] Built Submissions.UpperCompressions.IUB (2.5s)
✔ [8805/8846] Built Submissions.UpperCompressions.KeygenSupport (2.5s)
ℹ [8806/8846] Built Submissions.UpperCompressions.ShallowTree (3.6s)
info: Submissions/UpperCompressions/ShallowTree.lean:444:0: 'OptimalOTS.ShallowForest.exists_mem_evaluated_of_ne' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowTree.lean:445:0: 'OptimalOTS.ShallowForest.reconstructCost_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8807/8846] Built Submissions.UpperCompressions.Deterministic (2.7s)
✔ [8808/8846] Built Submissions.UpperCompressions.AlgorithmCosts (3.0s)
✔ [8809/8846] Built Submissions.UpperCompressions.IndexedScheme (3.3s)
✔ [8810/8846] Built Submissions.UpperCompressions.Master (3.4s)
ℹ [8811/8846] Built Submissions.UpperCompressions.TightDrift (9.8s)
info: Submissions/UpperCompressions/TightDrift.lean:108:0: 'TightIndex.exp_drift' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/TightDrift.lean:109:0: 'TightIndex.positive_part_le_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/TightDrift.lean:110:0: 'TightIndex.row_cap_le_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/TightDrift.lean:111:0: 'TightIndex.cachePotential_step' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/TightDrift.lean:112:0: 'TightIndex.cachePotential_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/TightDrift.lean:113:0: 'TightIndex.initial_slack' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8812/8846] Built Submissions.UpperCompressions.WireAdapter (2.8s)
✔ [8813/8846] Built Submissions.UpperCompressions.Resources (3.1s)
ℹ [8814/8846] Built Submissions.UpperCompressions.MasterReserve (2.0s)
info: Submissions/UpperCompressions/MasterReserve.lean:42:0: 'OptimalOTS.master_family_reserve' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/MasterReserve.lean:43:0: 'OptimalOTS.reserve_cancellation' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8815/8846] Built Submissions.UpperCompressions.Keygen (4.5s)
⚠ [8816/8846] Built Submissions.UpperCompressions.TightRow (13s)
warning: Submissions/UpperCompressions/TightRow.lean:16:46: Variable name `hb` 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] _hb

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: Submissions/UpperCompressions/TightRow.lean:74:0: 'TightIndex.row_main' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/TightRow.lean:75:0: 'TightIndex.row_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8817/8846] Built Submissions.UpperCompressions.Reconstruct (3.8s)
✔ [8818/8846] Built Submissions.UpperCompressions.SignIdx (4.0s)
✔ [8819/8846] Built Submissions.UpperCompressions.IndexedResources (3.1s)
ℹ [8820/8846] Built Submissions.UpperCompressions.IndexedSampling (4.2s)
info: Submissions/UpperCompressions/IndexedSampling.lean:616:0: 'OptimalOTS.IndexedAnalysis.sign_eq_map' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/IndexedSampling.lean:617:0: 'OptimalOTS.IndexedAnalysis.signIdx_support' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8821/8846] Built Submissions.UpperCompressions.Correctness (2.4s)
✔ [8822/8846] Built Submissions.UpperCompressions.IndexedCharges (3.1s)
ℹ [8823/8846] Built Submissions.UpperCompressions.SigningReserve (3.1s)
info: Submissions/UpperCompressions/SigningReserve.lean:171:0: 'OptimalOTS.IndexedAnalysis.SigningReserve.signIdx_reserve' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/SigningReserve.lean:173:0: 'OptimalOTS.IndexedAnalysis.SigningReserve.none_reserve' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/SigningReserve.lean:174:0: 'OptimalOTS.IndexedAnalysis.SigningReserve.some_reserve' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/SigningReserve.lean:175:0: 'OptimalOTS.IndexedAnalysis.SigningReserve.signIdx_reserve_of_answers' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [8824/8846] Built Submissions.UpperCompressions.IndexedAvailability (3.2s)
info: Submissions/UpperCompressions/IndexedAvailability.lean:166:0: 'OptimalOTS.IndexedAnalysis.Availability.loop_failure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/IndexedAvailability.lean:167:0: 'OptimalOTS.IndexedAnalysis.Availability.sign_failure_le' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8825/8846] Built Submissions.UpperCompressions.IndexedCorrectness (3.0s)
info: Submissions/UpperCompressions/IndexedCorrectness.lean:130:0: 'OptimalOTS.IndexedAnalysis.Correctness.correct' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8826/8846] Built Submissions.UpperCompressions.ShallowValues (3.0s)
✔ [8827/8846] Built Submissions.UpperCompressions.IndexedFreshness (2.9s)
ℹ [8828/8846] Built Submissions.UpperCompressions.IndexedReconstruct (2.7s)
info: Submissions/UpperCompressions/IndexedReconstruct.lean:53:0: 'OptimalOTS.IndexedAnalysis.verify_support' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8829/8846] Built Submissions.UpperCompressions.ShallowEvents (3.4s)
info: Submissions/UpperCompressions/ShallowEvents.lean:495:0: 'OptimalOTS.ShallowForest.events_none' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowEvents.lean:496:0: 'OptimalOTS.ShallowForest.events_ne' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowEvents.lean:497:0: 'OptimalOTS.ShallowForest.events_same' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8830/8846] Built Submissions.UpperCompressions.ShallowResample (3.8s)
info: Submissions/UpperCompressions/ShallowResample.lean:544:0: 'OptimalOTS.ShallowForest.hits_charge_A' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowResample.lean:545:0: 'OptimalOTS.ShallowForest.hits_charge_B' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8831/8846] Built Submissions.UpperCompressions.IndexedRho (5.3s)
warning: Submissions/UpperCompressions/IndexedRho.lean:317:27: This simp argument is unused:
  mul_add

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/IndexedRho.lean:451:0: 'OptimalOTS.IndexedAnalysis.signRho_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8832/8846] Built Submissions.UpperCompressions.ReservedHazard (2.4s)
info: Submissions/UpperCompressions/ReservedHazard.lean:131:0: 'OptimalOTS.IndexedAnalysis.ReservedHazard.costAtMost_signIdxLoop' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ReservedHazard.lean:132:0: 'OptimalOTS.IndexedAnalysis.ReservedHazard.reserved_signRho_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: Submissions/UpperCompressions/ReservedHazard.lean:133:0: 'OptimalOTS.IndexedAnalysis.ReservedHazard.reserved_signRho_bound_of_cost' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
⚠ [8833/8846] Built Submissions.UpperCompressions.IndexedRows (2.5s)
warning: Submissions/UpperCompressions/IndexedRows.lean:52:10: This simp argument is unused:
  BitVec.getLsbD_setWidth

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

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ℹ [8834/8846] Built Submissions.UpperCompressions.RepeatedFibers (2.1s)
info: Submissions/UpperCompressions/RepeatedFibers.lean:87:0: 'TightIndex.repeated_card_le_twice_excess' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/RepeatedFibers.lean:132:0: 'TightIndex.rowBad_card_le_twice_excess' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8835/8846] Built Submissions.UpperCompressions.TightPotential (4.8s)
info: Submissions/UpperCompressions/TightPotential.lean:130:0: 'OptimalOTS.IndexedAnalysis.Tight.A_cacheQuery' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/TightPotential.lean:131:0: 'OptimalOTS.IndexedAnalysis.Tight.encCount_cacheQuery_fresh' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/TightPotential.lean:132:0: 'OptimalOTS.IndexedAnalysis.Tight.rho_of_ne' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/TightPotential.lean:133:0: 'OptimalOTS.IndexedAnalysis.Tight.rho_empty' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/TightPotential.lean:304:0: 'OptimalOTS.IndexedAnalysis.Tight.rho_charge' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/TightPotential.lean:305:0: 'OptimalOTS.IndexedAnalysis.Tight.rho_dom' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8836/8846] Built Submissions.UpperCompressions.ShallowCount (52s)
info: Submissions/UpperCompressions/ShallowCount.lean:119:0: 'OptimalOTS.ShallowResearch.single_shape_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowCount.lean:120:0: 'OptimalOTS.ShallowResearch.single_shape_102_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8837/8846] Built Submissions.UpperCompressions.ShallowCount100 (29s)
info: Submissions/UpperCompressions/ShallowCount100.lean:165:0: 'OptimalOTS.IndexTightResearch.fixed12_cost82_sufficient' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowCount100.lean:166:0: 'OptimalOTS.IndexTightResearch.fixed12_cost81_insufficient' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowCount100.lean:167:0: 'OptimalOTS.IndexTightResearch.fresh_trials_failure127' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8838/8846] Built Submissions.UpperCompressions.ShallowCuts (4.5s)
info: Submissions/UpperCompressions/ShallowCuts.lean:500:0: 'OptimalOTS.ShallowForest.card_family' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowCuts.lean:501:0: 'OptimalOTS.ShallowForest.isCut_of_mem_family' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowCuts.lean:502:0: 'OptimalOTS.ShallowForest.card_of_mem_family' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowCuts.lean:503:0: 'OptimalOTS.ShallowForest.cost_of_mem_family' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowCuts.lean:504:0: 'OptimalOTS.ShallowForest.reconstructCost_cutOf' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowCuts.lean:505:0: 'OptimalOTS.ShallowForest.revealBits_cutOf' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8839/8846] Built Submissions.UpperCompressions.ShallowScheme (3.7s)
✔ [8840/8846] Built Submissions.UpperCompressions.ShallowResources (3.8s)
⚠ [8841/8846] Built Submissions.UpperCompressions.ShallowPotentials (4.9s)
warning: Submissions/UpperCompressions/ShallowPotentials.lean:122: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`
warning: Submissions/UpperCompressions/ShallowPotentials.lean:365:44: Variable name `hc` 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] _hc

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: Submissions/UpperCompressions/ShallowPotentials.lean:465:0: 'OptimalOTS.ShallowForest.ΦA_charge' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowPotentials.lean:466:0: 'OptimalOTS.ShallowForest.ΦB_charge_some' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowPotentials.lean:467:0: 'OptimalOTS.ShallowForest.ΦB_charge_none' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowPotentials.lean:469:0: 'OptimalOTS.ShallowForest.encTerm_dom' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowPotentials.lean:470:0: 'OptimalOTS.ShallowForest.encTerm_empty_le' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowPotentials.lean:471:0: 'OptimalOTS.ShallowForest.ΦA_empty' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8842/8846] Built Submissions.UpperCompressions.ShallowStageB (5.6s)
info: Submissions/UpperCompressions/ShallowStageB.lean:548:0: 'OptimalOTS.ShallowForest.stageB' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8843/8846] Built Submissions.UpperCompressions.ShallowAssembly (4.4s)
✔ [8844/8846] Built Submissions.UpperCompressions.ShallowMain (3.8s)
ℹ [8845/8846] Built Submissions.UpperCompressions.ShallowWire (3.8s)
info: Submissions/UpperCompressions/ShallowWire.lean:78:0: 'OptimalOTS.ShallowUpperForest.Wire.secure' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowWire.lean:79:0: 'OptimalOTS.ShallowUpperForest.Wire.admissible' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Submissions/UpperCompressions/ShallowWire.lean:80:0: 'OptimalOTS.ShallowUpperForest.Wire.cost' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8846/8846] Built Submissions.UpperCompressions.Solution (3.6s)
Build completed successfully (8846 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!