ℹ [3569/3805] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3696/3805] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3700/3805] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3780/3805] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaSummary
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`
⚠ [3822/4124] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4040/4124] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
ℹ [8695/8721] Built ResearchPNT.PrimeBins (2.8s)
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]
✔ [8696/8721] Built Research.SubsetSums (3.7s)
✔ [8697/8721] Built Research.Partition (3.8s)
⚠ [8698/8721] Built Research.Benchmark (4.4s)
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`
⚠ [8699/8721] Built Research.GoodIndices (3.7s)
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`
✔ [8700/8721] Built Research.LargePrime (4.6s)
⚠ [8701/8721] Built Research.LowerProduct (4.4s)
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`
⚠ [8702/8721] Built Research.Compatibility (4.5s)
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`
✔ [8703/8721] Built Research.CommonDenominator (3.6s)
✔ [8704/8721] Built Research.LowerMesh (4.1s)
✔ [8705/8721] Built Research.SmoothLcm (3.8s)
✔ [8706/8721] Built Research.LowerRecurrence (4.5s)
✔ [8707/8721] Built Research.LowerBenchmark (3.8s)
✔ [8708/8721] Built Research.AnalyticRecurrence (3.9s)
⚠ [8709/8721] Built Research.LowerAbel (5.5s)
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`
✔ [8710/8721] Built Research.LowerParameters (6.2s)
⚠ [8711/8721] Built ResearchPNT.Combined (5.8s)
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 (8.0s)
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 (12s)
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 (4.1s)
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 (9.2s)
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 (9.9s)
⚠ [8717/8721] Built ResearchPNT.LowerGlobal (9.5s)
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.3s)
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.1s)
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.5s)
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
