INFO: bootstrapping pinned Lean dependencies
info: toolchain not updated; already up-to-date
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision 'db127794c79fdeb86f6b0cf6ff2c804026fbaff1'
info: PrimeCert: cloning https://github.com/b-mehta/PrimeCert
info: PrimeCert: checking out revision 'f699a3e5d3efb381b9ddfb61a1ca51be25f456bd'
info: leancert: cloning https://github.com/alerad/leancert.git
info: leancert: checking out revision '33a9d1762b284fe1914d481d6a8158520e14708e'
info: checkdecls: cloning https://github.com/PatrickMassot/checkdecls.git
info: checkdecls: checking out revision '3d425859e73fcfbef85b9638c2a91708ef4a22d4'
info: LeanArchitect: cloning https://github.com/hanwenzhu/LeanArchitect.git
info: LeanArchitect: checking out revision 'f38c848196b0467e7b9dcc3d129a866b4051c23c'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '63045536fe95024e6c18fc7b48e03f506701c5bc'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'c5d5b8fe6e5158def25cd28eb94e4141ad97c843'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '5c7542ed018c78194f1e2b903eaf6a792b74c03d'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '24b0d9dc081c5423f8eec7e866c441e5184f29d9'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'e3cb2f741431ce31bf73549fb52316a57368b06f'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'f46324995fca5f0483b742e4eb4daec7f4ee50d2'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'fc38104235ab6cf8a448a74405aa258804ef4e36'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '92564e5770e4d09f2d86dfbf8ada1e9c715b384c'
info: mathlib: running post-update hooks
✔ [1/5] Built Cache.Cli (508ms)
✔ [2/5] Built Cache.Lean (646ms)
✔ [8/26] Built Cache.Cli:c.o (302ms)
✔ [9/26] Built Cache.Lean:c.o (420ms)
✔ [10/26] Built Cache.Infra (849ms)
✔ [11/26] Built Cache.Infra:c.o (397ms)
✔ [12/26] Built Cache.IO (2.9s)
✔ [13/26] Built Cache.Hashing (2.1s)
✔ [14/26] Built Cache.Hashing:c.o (1.2s)
✔ [15/26] Built Cache.IO:c.o (3.5s)
✔ [16/26] Built Cache.Requests (5.2s)
✔ [17/26] Built Cache.Marker (1.4s)
✔ [18/26] Built Cache.Marker:c.o (292ms)
✔ [19/26] Built Cache.Query (1.6s)
✔ [20/26] Built Cache.Query:c.o (554ms)
✔ [21/26] Built Cache.Warning (1.4s)
✔ [22/26] Built Cache.Warning:c.o (434ms)
✔ [23/26] Built Cache.Requests:c.o (4.0s)
✔ [24/26] Built Cache.Main (2.0s)
✔ [25/26] Built Cache.Main:c.o (1.8s)
✔ [26/26] Built cache:exe (1.0s)
Current branch: HEAD
Using cache from origin: (some leanprover-community/mathlib4)
Decompressing 8360 already-cached file(s) (186 already decompressed)
No files to download
Decompressed 8360 already-cached file(s)
Completed successfully in 44613 ms!
Current branch: HEAD
Using cache from origin: (some leanprover-community/mathlib4)
No files to download
Already decompressed 8546 file(s)
✔ [2230/2403] Built Architect.Command (1.0s)
✔ [2952/3032] Built Architect.Basic (1.6s)
✔ [3883/4043] Built Architect.Content (1.5s)
✔ [3884/4043] Built Architect.CollectUsed (1.4s)
✔ [4509/4698] Built Architect.Tactic (2.1s)
✔ [4571/4783] Built PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support (1.8s)
✔ [6133/6317] Built PrimeNumberTheoremAnd.Tactic.AdditiveCombination (3.7s)
✔ [6192/6387] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic (3.8s)
✔ [6259/6449] Built PrimeNumberTheoremAnd.Auxiliary (4.6s)
✔ [6260/6449] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics (3.6s)
✔ [6465/6642] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv (3.8s)
✔ [6616/6812] Built Architect.Attribute (3.4s)
✔ [6852/7025] Built PrimeNumberTheoremAnd.EulerMaclaurin (4.9s)
✔ [6853/7025] Built LeanCert.Core.DerivativeIntervals (4.4s)
✔ [6957/7148] Built LeanCert.Core.Interval (4.7s)
✔ [7223/7418] Built LeanCert.Core.Dyadic (4.9s)
✔ [7224/7418] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables (4.5s)
✔ [7382/7557] Built Architect.Output (4.1s)
✔ [7711/7892] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (5.9s)
✔ [8206/8392] Built Architect.Load (1.3s)
✔ [8564/8717] Built LeanCert.Core.Expr (7.2s)
✔ [8565/8717] Built LeanCert.Contrib.Sinc (7.1s)
✔ [8588/8721] Built Architect (1.3s)
✔ [8589/8721] Built LeanCert.Core.Support (3.6s)
✔ [8590/8721] Built LeanCert.Meta.Numeral (5.6s)
✔ [8591/8721] Built PrimeNumberTheoremAnd.Sobolev (14s)
✔ [8592/8721] Built LeanCert.Core.Taylor (9.5s)
✔ [8593/8721] Built PrimeNumberTheoremAnd.ZetaConj (6.6s)
✔ [8594/8721] Built LeanCert.Core.IntervalRat.LogReduction (8.1s)
✔ [8595/8721] Built PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries (15s)
✔ [8596/8721] Built Research.Partition (8.7s)
✔ [8597/8721] Built PrimeNumberTheoremAnd.Rectangle (8.5s)
✔ [8598/8721] Built PrimeNumberTheoremAnd.SmoothExistence (8.7s)
✔ [8599/8721] Built Research.SubsetSums (9.2s)
✔ [8600/8721] Built LeanCert.Core.IntervalRat.Basic (13s)
⚠ [8601/8721] Built Research.Benchmark (11s)
warning: Research/Benchmark.lean:248:2: 'norm_num at hlower' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
✔ [8602/8721] Built LeanCert.Meta.ToExpr (10s)
✔ [8603/8721] Built PrimeNumberTheoremAnd.Fourier (10s)
✔ [8604/8721] Built LeanCert.Tactic.IntervalAuto.Types (7.3s)
✔ [8605/8721] Built LeanCert.Tactic.IntervalAuto.Extract (7.6s)
✔ [8606/8721] Built LeanCert.Core.TrigReduction (8.1s)
✔ [8607/8721] Built LeanCert.Core.IntervalRat.Transcendental (9.8s)
⚠ [8608/8721] Built Research.GoodIndices (11s)
warning: Research/GoodIndices.lean:96:2: 'norm_num only [Nat.cast_pow, Nat.cast_ofNat] at hlog' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
✔ [8609/8721] Built PrimeNumberTheoremAnd.MellinCalculus (22s)
✔ [8610/8721] Built Research.LargePrime (15s)
✔ [8611/8721] Built LeanCert.Tactic.IntervalAuto.Norm (6.9s)
✔ [8612/8721] Built PrimeNumberTheoremAnd.Defs (9.2s)
⚠ [8613/8721] Built Research.LowerProduct (13s)
warning: Research/LowerProduct.lean:445:49: Variable name `hU` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✔ [8614/8721] Built LeanCert.Tactic.IntervalAuto.Parse (10s)
✔ [8615/8721] Built PrimeNumberTheoremAnd.ResidueCalcOnRectangles (21s)
⚠ [8616/8721] Built Research.Compatibility (11s)
warning: Research/Compatibility.lean:99:52: Variable name `hn` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Research/Compatibility.lean:309:57: Variable name `hp` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✔ [8617/8721] Built PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions (6.5s)
✔ [8618/8721] Built LeanCert.Tactic.IntervalAuto.Diagnostic (4.3s)
✔ [8619/8721] Built Research.CommonDenominator (8.8s)
✔ [8620/8721] Built PrimeNumberTheoremAnd.IEANTN.Mertens (33s)
✔ [8621/8721] Built LeanCert.Core.IntervalRat.Taylor (23s)
✔ [8622/8721] Built Research.LowerMesh (10s)
⚠ [8623/8721] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta (5.4s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [8624/8721] Built LeanCert.Core.IntervalReal (3.9s)
✔ [8625/8721] Built PrimeNumberTheoremAnd.IEANTN.KLN (6.0s)
✔ [8626/8721] Built LeanCert.Core.IntervalRat.TrigReduced (4.2s)
✔ [8627/8721] Built PrimeNumberTheoremAnd.IEANTN.PVIdentity (47s)
✔ [8628/8721] Built Research.SmoothLcm (8.3s)
✔ [8629/8721] Built Research.LowerRecurrence (9.8s)
✔ [8630/8721] Built Research.LowerBenchmark (7.8s)
✔ [8631/8721] Built LeanCert.Core.IntervalRealEndpoints (6.2s)
✔ [8632/8721] Built LeanCert.Engine.Affine.Basic (9.0s)
✔ [8633/8721] Built Research.AnalyticRecurrence (10s)
✔ [8634/8721] Built LeanCert.Core.IntervalDyadic (14s)
✔ [8635/8721] Built LeanCert.Engine.Eval.Core (11s)
✔ [8636/8721] Built LeanCert.Engine.Affine.Nonlinear (8.1s)
⚠ [8637/8721] Built Research.LowerAbel (15s)
warning: Research/LowerAbel.lean:34:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/LowerAbel.lean:62:51: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Research/LowerAbel.lean:62:51: 'simp [hpm]' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Research/LowerAbel.lean:84:5: Variable name `hc` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Research/LowerAbel.lean:137:25: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [8638/8721] Built Research.LowerParameters (15s)
✔ [8639/8721] Built PrimeNumberTheoremAnd.IEANTN.LiSeries (20s)
✔ [8640/8721] Built LeanCert.Engine.Eval.Extended (5.1s)
✔ [8641/8721] Built LeanCert.Tactic.Bound.Lemmas (3.0s)
⚠ [8642/8721] Built PrimeNumberTheoremAnd.Wiener (48s)
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [8643/8721] Built LeanCert.Engine.IntervalEval (2.4s)
✔ [8644/8721] Built PrimeNumberTheoremAnd.ZetaBounds (37s)
✔ [8645/8721] Built LeanCert.Validity.Bounds.Core (3.3s)
✔ [8646/8721] Built LeanCert.Validity.Bounds.WithInv (3.4s)
✔ [8647/8721] Built LeanCert.Engine.AD.Basic (3.5s)
✔ [8648/8721] Built LeanCert.Engine.Optimization.Box (3.6s)
✔ [8649/8721] Built LeanCert.Engine.Affine.Transcendental (5.2s)
✔ [8650/8721] Built LeanCert.Engine.IntervalEvalDyadic (5.8s)
✔ [8651/8721] Built LeanCert.Engine.RootFinding.Basic (6.0s)
✔ [8652/8721] Built LeanCert.Engine.Integrate (7.1s)
✔ [8653/8721] Built LeanCert.Engine.AD.Transcendental (6.6s)
✔ [8654/8721] Built LeanCert.Validity.DyadicBounds (4.2s)
✔ [8655/8721] Built LeanCert.Engine.TaylorModel.Core (10s)
✔ [8656/8721] Built LeanCert.Engine.IntervalEvalAffine (5.9s)
✔ [8657/8721] Built LeanCert.Engine.RootFinding.Bisection (8.1s)
✔ [8658/8721] Built LeanCert.Engine.AD.Eval (4.2s)
✔ [8659/8721] Built LeanCert.Engine.TaylorModel.Special (4.7s)
✔ [8660/8721] Built LeanCert.Engine.TaylorModel.Integral (6.2s)
✔ [8661/8721] Built LeanCert.Engine.TaylorModel.Log1p (10s)
✔ [8662/8721] Built LeanCert.Engine.AD.Correctness (6.7s)
✔ [8663/8721] Built LeanCert.Engine.TaylorModel.ExpLog (12s)
✔ [8664/8721] Built LeanCert.Engine.TaylorModel.Trig (15s)
✔ [8665/8721] Built LeanCert.Examples.Li2Base (5.1s)
✔ [8666/8721] Built LeanCert.Engine.AD.Computable (4.9s)
✔ [8667/8721] Built LeanCert.Engine.TaylorModel.Hyperbolic (17s)
⚠ [8668/8721] Built LeanCert.Examples.Li2Bounds (3.5s)
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [8669/8721] Built LeanCert.Engine.AD.PartialCorrectness (8.4s)
✔ [8670/8721] Built LeanCert.Engine.TaylorModel.Functions (2.7s)
✔ [8671/8721] Built LeanCert.Engine.AD (2.1s)
✔ [8672/8721] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (4.2s)
✔ [8673/8721] Built LeanCert.Validity.Bounds.Smart (2.9s)
✔ [8674/8721] Built LeanCert.Meta.ProveSupported (3.7s)
✔ [8675/8721] Built LeanCert.Engine.TaylorModel.Expr (4.4s)
✔ [8676/8721] Built PrimeNumberTheoremAnd.Consequences (37s)
✔ [8677/8721] Built LeanCert.Engine.Optimize (5.3s)
✔ [8678/8721] Built LeanCert.Engine.TaylorModel (2.0s)
✔ [8679/8721] Built LeanCert.Validity.Bounds.Bridge (2.8s)
✔ [8680/8721] Built LeanCert.Meta.ProveContinuous (3.9s)
✔ [8681/8721] Built LeanCert.Validity.Bounds.Basic (2.5s)
✔ [8682/8721] Built LeanCert.Tactic.IntervalAuto.ProveCommon (5.2s)
✔ [8683/8721] Built LeanCert.Engine.IntervalEvalRefined (3.9s)
✔ [8684/8721] Built LeanCert.Engine.RootFinding.Newton (5.1s)
✔ [8685/8721] Built LeanCert.Engine.Optimization.Gradient (5.6s)
✔ [8686/8721] Built LeanCert.Tactic.IntervalAuto.Basic (3.8s)
✔ [8687/8721] Built LeanCert.Validity.Integration (5.7s)
✔ [8688/8721] Built LeanCert.Engine.RootFinding.MVTBounds (5.4s)
ℹ [8689/8721] Built PrimeNumberTheoremAnd.MediumPNT (47s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8690/8721] Built LeanCert.Engine.RootFinding.Contraction (4.4s)
✔ [8691/8721] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (51s)
✔ [8692/8721] Built LeanCert.Engine.RootFinding.Main (1.0s)
✔ [8693/8721] Built LeanCert.Engine.Optimization.Global (13s)
⚠ [8694/8721] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (2.9s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
✔ [8695/8721] Built LeanCert.Engine.Optimization.BoundVerify (3.4s)
✔ [8696/8721] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (3.3s)
✔ [8697/8721] Built LeanCert.Validity.Bounds (5.0s)
✔ [8698/8721] Built LeanCert.Tactic.IntervalAuto.OptBound (4.8s)
✔ [8699/8721] Built LeanCert.Tactic.IntervalAuto.RootBound (4.0s)
✔ [8700/8721] Built LeanCert.Tactic.IntervalAuto.Multivariate (8.0s)
✔ [8701/8721] Built LeanCert.Tactic.IntervalAuto.Bound (36s)
✔ [8702/8721] Built LeanCert.Tactic.IntervalAuto.Adaptive (10s)
✔ [8703/8721] Built LeanCert.Tactic.IntervalAuto.Subdiv (11s)
✔ [8704/8721] Built LeanCert.Tactic.IntervalAuto.PointIneq (20s)
✔ [8705/8721] Built LeanCert.Tactic.IntervalAuto (3.0s)
✔ [8706/8721] Built PrimeNumberTheoremAnd.IEANTN.LogTables (39s)
✔ [8707/8721] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (18s)
✔ [8708/8721] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (17s)
⚠ [8709/8721] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (27s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
ℹ [8710/8721] Built ResearchPNT.PrimeBins (7.5s)
info: ResearchPNT/PrimeBins.lean:128:0: 'ResearchPNT.exists_theta_error_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ResearchPNT/PrimeBins.lean:129:0: 'ResearchPNT.card_prime_Ioc_le_of_theta_error' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ResearchPNT/PrimeBins.lean:130:0: 'ResearchPNT.exists_prime_quotient_bin_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8711/8721] Built ResearchPNT.Combined (10s)
warning: ResearchPNT/Combined.lean:215:62: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: ResearchPNT/Combined.lean:563:44: Variable name `hD` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: ResearchPNT/Combined.lean:953:0: 'ResearchPNT.exists_logS_le_majorized_binSum' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ResearchPNT/Combined.lean:954:0: 'ResearchPNT.exists_logS_le_simple_binSum' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ResearchPNT/Combined.lean:955:0: 'ResearchPNT.exists_logS_le_coarse_binSum' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ResearchPNT/Combined.lean:956:0: 'ResearchPNT.exists_logS_le_logLower_binSum' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ResearchPNT/Combined.lean:957:0: 'ResearchPNT.exists_logS_le_uniform_binSum' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8712/8721] Built ResearchPNT.ParameterChoice (17s)
warning: ResearchPNT/ParameterChoice.lean:79:21: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: ResearchPNT/ParameterChoice.lean:322:8: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: ResearchPNT/ParameterChoice.lean:322:64: 'positivity' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: ResearchPNT/ParameterChoice.lean:322:64: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: ResearchPNT/ParameterChoice.lean:314:50: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: ResearchPNT/ParameterChoice.lean:315:21: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
info: ResearchPNT/ParameterChoice.lean:1042:0: 'ResearchPNT.exists_eventual_height_step' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ResearchPNT/ParameterChoice.lean:1043:0: 'ResearchPNT.exists_eventual_height_step_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ResearchPNT/ParameterChoice.lean:1044:0: 'ResearchPNT.exists_global_discrete_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ResearchPNT/ParameterChoice.lean:1045:0: 'ResearchPNT.exists_full_depth_product_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8713/8721] Built ResearchPNT.LowerBins (20s)
warning: ResearchPNT/LowerBins.lean:41:18: Variable name `hlogm` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ResearchPNT/LowerBins.lean:208:4: 'norm_num at hsqSmall' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
info: ResearchPNT/LowerBins.lean:394:0: 'ResearchPNT.exists_prime_interval_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8714/8721] Built ResearchPNT.LowerRenewal (7.0s)
warning: ResearchPNT/LowerRenewal.lean:63:40: 'ring' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: ResearchPNT/LowerRenewal.lean:63:40: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: ResearchPNT/LowerRenewal.lean:63:21: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: ResearchPNT/LowerRenewal.lean:117:40: 'ring' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: ResearchPNT/LowerRenewal.lean:117:40: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: ResearchPNT/LowerRenewal.lean:117:21: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
info: ResearchPNT/LowerRenewal.lean:119:0: 'ResearchPNT.eventually_coeffGood_lower_renewal' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ResearchPNT/LowerRenewal.lean:120:0: 'ResearchPNT.eventually_tailGood_lower_renewal' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8715/8721] Built ResearchPNT.LowerInduction (15s)
warning: ResearchPNT/LowerInduction.lean:144:27: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: ResearchPNT/LowerInduction.lean:298:27: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: ResearchPNT/LowerInduction.lean:322:5: Variable name `hfloorNext` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ResearchPNT/LowerInduction.lean:454:27: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: ResearchPNT/LowerInduction.lean:478:5: Variable name `hfloorNext` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ResearchPNT/LowerInduction.lean:610:27: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [8716/8721] Built ResearchPNT.LowerParameterChoice (13s)
⚠ [8717/8721] Built ResearchPNT.LowerGlobal (10s)
warning: ResearchPNT/LowerGlobal.lean:151:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: ResearchPNT/LowerGlobal.lean:153:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
info: ResearchPNT/LowerGlobal.lean:250:0: 'ResearchPNT.exists_global_adaptive_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8718/8721] Built ResearchPNT.LowerComparison (6.8s)
info: ResearchPNT/LowerComparison.lean:303:0: 'ResearchPNT.exists_eventual_full_product_tail_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [8719/8721] Built ResearchPNT.FinalEstimate (4.4s)
info: ResearchPNT/FinalEstimate.lean:89:0: 'ResearchPNT.exists_eventual_full_product_logS_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ResearchPNT/FinalEstimate.lean:90:0: 'ResearchPNT.exists_two_sided_full_product_estimate' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8720/8721] Built ResearchPNT (3.7s)
Build completed successfully (8721 jobs).
PASS: sorry/admit/axiom-free Lean build
'ResearchPNT.exists_two_sided_full_product_estimate' depends on axioms: [propext, Classical.choice, Quot.sound]
PASS: theorem axiom audit; only Classical.choice, Quot.sound, propext
