Verification run

Run 149

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via github_backfill

succeeded commit c16e19c49cdb toolchain lean-v4-30-0 prover lean took 9h 9m · finished 5d ago

Package inputs

This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.

Trust verification

Recomputes trust checks from the recorded attestations, manifest, and command history.

(verification not run)

Manifest

Loads the published files manifest and location metadata for this job.

(manifest not loaded)

Verifier log excerpt

e4ExtData_06:blueprint (3.2s)
✔ [4248/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07:blueprint (3.1s)
✔ [4249/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08:blueprint (3.2s)
✔ [4250/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09:blueprint (3.1s)
✔ [4251/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10:blueprint (3.2s)
✔ [4252/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11:blueprint (3.1s)
✔ [4253/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12:blueprint (3.1s)
✔ [4254/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13:blueprint (3.1s)
⚠ [4255/4261] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
✔ [4257/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext:blueprint (3.2s)
⚠ [4258/4262] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
✔ [4260/4290] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor:blueprint (5.4s)
⚠ [4270/4290] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2061:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4299/4399] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.1s)
⚠ [4300/4399] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:93:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:104:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:117:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:154:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:179:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:187:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:195:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:341:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:470:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:564:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:573:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:591:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:600:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:616:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:625:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:678:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:687:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:696:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:756:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:767:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:778:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:788:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:805:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:814:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:937:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:957:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:987:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1013:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1027:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1035:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1050:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1065:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1074:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1089:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1107:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1119:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1136:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1183:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1254:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1306:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1334:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1369:8: declaration uses `sorry`
ℹ [4328/4399] Replayed PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
⚠ [4329/4399] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline

Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
✔ [4331/4399] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (45s)
⚠ [4332/4399] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:214:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:338:8: declaration uses `sorry`
✔ [4352/4399] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (10s)
✔ [4353/4399] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (7.3s)
⚠ [4354/4399] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4367/4399] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.3s)
✔ [4373/4399] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (11s)
✔ [4374/4399] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (3.2s)
✔ [4375/4399] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (15s)
⚠ [4394/4399] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:134:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:496:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1443:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1613:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2843:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2869:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3475:8: declaration uses `sorry`
✔ [4397/4400] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (6.6s)
ℹ [4398/4400] Replayed PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint
info: Blueprint indexing
Build completed successfully (4400 jobs).

stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-a)
exit_code=Some(0) duration_ms=504936
stdout:
apx-semantic-phase	{"duration_ms":23,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":354,"diagnostic_count":229,"duration_ms":31384,"module_name":"PrimeNumberTheoremAnd.IEANTN.Mertens","module_path":"PrimeNumberTheoremAnd/IEANTN/Mertens.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":417026,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Mertens","module_path":"PrimeNumberTheoremAnd/IEANTN/Mertens.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":354,"diagnostic_count":229,"duration_ms":22,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Mertens","module_path":"PrimeNumberTheoremAnd/IEANTN/Mertens.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":2005231,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":5,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":2005231,"phase":"lean_module_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":25}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":9158,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":51,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":494888,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-b)
exit_code=Some(0) duration_ms=1344589
stdout:
apx-semantic-phase	{"duration_ms":23,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":33,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimaryDefinitions.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":411318,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimaryDefinitions.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimaryDefinitions.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":510,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":510,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":471,"diagnostic_count":322,"duration_ms":48065,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaAppendix","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":424205,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaAppendix","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":471,"diagnostic_count":322,"duration_ms":24,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaAppendix","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":4207991,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":3,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":4207991,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":6,"diagnostic_count":0,"duration_ms":542,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaSummary","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":414493,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaSummary","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":6,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaSummary","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":11072,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":11072,"phase":"lean_module_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":21}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":11918,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":64,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1331787,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r2)
exit_code=Some(0) duration_ms=1333035
stdout:
apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":136,"diagnostic_count":71,"duration_ms":10690,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":442000,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":136,"diagnostic_count":71,"duration_ms":5,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":509774,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":509774,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":69,"diagnostic_count":54,"duration_ms":5063,"module_name":"PrimeNumberTheoremAnd.IEANTN.MobiusLemma","module_path":"PrimeNumberTheoremAnd/IEANTN/MobiusLemma.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":416535,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.MobiusLemma","module_path":"PrimeNumberTheoremAnd/IEANTN/MobiusLemma.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":69,"diagnostic_count":54,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.MobiusLemma","module_path":"PrimeNumberTheoremAnd/IEANTN/MobiusLemma.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":430031,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":430031,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":36,"diagnostic_count":27,"duration_ms":2705,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":428459,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":36,"diagnostic_count":27,"duration_ms":2,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":189395,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":189395,"phase":"lean_module_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":17062,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":39,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1314212,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r3)
exit_code=Some(0) duration_ms=2254668
stdout:
apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":57,"diagnostic_count":33,"duration_ms":4151,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":453149,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":57,"diagnostic_count":33,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":166420,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":166420,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":442,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":436728,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":74842,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":74842,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":610,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":435101,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":68407,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":68407,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":17,"diagnostic_count":10,"duration_ms":1353,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimeInInterval","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":433972,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimeInInterval","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":17,"diagnostic_count":10,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimeInInterval","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":101503,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":101503,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":297,"diagnostic_count":259,"duration_ms":22869,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":442457,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":297,"diagnostic_count":259,"duration_ms":15,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":1556361,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":1556361,"phase":"lean_module_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":17327,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":52,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":2236669,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r4)
exit_code=Some(0) duration_ms=1880178
stdout:
apx-semantic-phase	{"duration_ms":3,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":480,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":452888,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":77992,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":77992,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":402,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":445210,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":80054,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":80054,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":394,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":467953,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":82759,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":82759,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":362,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":451161,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":85603,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":85603,"phase":"lean_module_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":15127,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":28,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1863905,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r5)
exit_code=Some(0) duration_ms=1778420
stdout:
apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":428,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":432866,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":87967,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":87967,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":447,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":435056,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":90257,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":90257,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":396,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":439022,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":92539,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":92539,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":437,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":440278,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":94376,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":94376,"phase":"lean_module_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":19}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":17651,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":55,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1759727,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r6)
exit_code=Some(0) duration_ms=1798954
stdout:
apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":455,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":446274,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":96327,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":96327,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":466,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":443444,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":101240,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":101240,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":452,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":444736,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":102723,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":102723,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":466,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":440988,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":107456,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":107456,"phase":"lean_module_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":11119,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":48,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1787202,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r7)
exit_code=Some(0) duration_ms=1357161
stdout:
apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":150,"diagnostic_count":101,"duration_ms":11101,"module_name":"PrimeNumberTheoremAnd.IEANTN.Dusart","module_path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":419830,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Dusart","module_path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":150,"diagnostic_count":101,"duration_ms":13,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Dusart","module_path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":849814,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":849814,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":679,"diagnostic_count":493,"duration_ms":66055,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":425619,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":679,"diagnostic_count":493,"duration_ms":44,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":3913891,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":3913891,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":16,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":418150,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":502,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":502,"phase":"lean_module_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":10815,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":49,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1345726,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r8)
exit_code=Some(0) duration_ms=900754
stdout:
apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":41,"diagnostic_count":6,"duration_ms":2784,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":433001,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":41,"diagnostic_count":6,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":344830,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":344830,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":258,"diagnostic_count":135,"duration_ms":21698,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":427742,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":258,"diagnostic_count":135,"duration_ms":9,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1269379,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1269379,"phase":"lean_module_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":21}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":10347,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":49,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":889864,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r9)
exit_code=Some(0) duration_ms=448195
stdout:
apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":32,"diagnostic_count":19,"duration_ms":2395,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":430479,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":32,"diagnostic_count":19,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":94339,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":94339,"phase":"lean_module_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":10112,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":51,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":437504,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r10)
exit_code=Some(0) duration_ms=453016
stdout:
apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":27,"diagnostic_count":9,"duration_ms":2050,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":435642,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":27,"diagnostic_count":9,"duration_ms":2,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":169753,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":169753,"phase":"lean_module_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":10130,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":45,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":442287,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r11)
exit_code=Some(0) duration_ms=446954
stdout:
apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":67,"diagnostic_count":53,"duration_ms":5116,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":426880,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":67,"diagnostic_count":53,"duration_ms":5,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":257157,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":257157,"phase":"lean_module_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":9764,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":40,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":436601,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r12)
exit_code=Some(0) duration_ms=459519
stdout:
apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":70,"diagnostic_count":54,"duration_ms":5074,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":439343,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":70,"diagnostic_count":54,"duration_ms":4,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":396745,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":396745,"phase":"lean_module_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":9990,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":52,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":448878,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r13)
exit_code=Some(0) duration_ms=479925
stdout:
apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":235,"diagnostic_count":164,"duration_ms":18469,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":445326,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":235,"diagnostic_count":164,"duration_ms":23,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1491369,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1491369,"phase":"lean_module_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":25}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":10397,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":53,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":468890,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r14)
exit_code=Some(0) duration_ms=478231
stdout:
apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":263,"diagnostic_count":178,"duration_ms":23345,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":439680,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":263,"diagnostic_count":178,"duration_ms":27,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1806664,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1806664,"phase":"lean_module_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":25}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":9741,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":43,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":467557,"ok":true}

Stored Lean workspace build cache
Stored Lean semantic extraction cache

Command runs

lean_checker exit 0 duration 26m 5s · created 7/11/2026, 6:04:35 AM

lake build

ℹ [3536/3548] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3556/3572] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
⚠ [3695/3710] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3812/3819] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3817/3829] Built PrimeNumberTheoremAnd.IEANTN.Mertens (72s)
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1305:16: declaration uses `sorry`
⚠ [3880/3892] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (47s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2577:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2578:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2599:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2600:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2817:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2818:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2833:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2834:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2963:4: `simp [W]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2964:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3069:4: `simp [p]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3070:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: `simp [Set.uIcc_of_le hab]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: Try this:
  [apply] simp only [_root_.deriv_ofReal]
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3085:4: `fun_prop` uses `⊢`!
⚠ [3881/3892] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [3883/3893] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (3.1s)
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`
✔ [3887/3895] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (2.8s)
✔ [3890/3895] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (7.5s)
⚠ [3891/3895] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (5.8s)
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
✔ [3894/3901] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (8.8s)
⚠ [4017/4025] Built PrimeNumberTheoremAnd.IEANTN.Buthe (11s)
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
⚠ [4018/4025] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (16s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
⚠ [4020/4026] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (11s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4022/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (27s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
✔ [4034/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (4.9s)
✔ [4037/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (7.9s)
ℹ [4038/4068] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (45s)
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
✔ [4040/4068] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (3.9s)
✔ [4042/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85 (18s)
✔ [4043/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc (11s)
✔ [4044/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000 (66s)
✔ [4045/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500 (39s)
✔ [4046/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500 (38s)
✔ [4047/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500 (39s)
✔ [4048/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500 (39s)
✔ [4049/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875 (39s)
✔ [4050/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375 (40s)
✔ [4051/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875 (40s)
✔ [4052/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (40s)
✔ [4053/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (40s)
✔ [4054/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (39s)
✔ [4055/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (39s)
✔ [4056/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (5.6s)
✔ [4057/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (9.8s)
✔ [4058/4072] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (18s)
⚠ [4059/4072] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (12s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2634:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2723:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3093:4: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3685:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3713:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3725:8: declaration uses `sorry`
⚠ [4061/4072] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
✔ [4063/4074] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43 (62s)
✔ [4065/4074] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (14s)
⚠ [4066/4074] Built PrimeNumberTheoremAnd.IEANTN.Dusart (17s)
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:736:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:748:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:760:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:772:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:784:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:808:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:820:8: declaration uses `sorry`
✔ [4068/4074] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59 (39s)
✔ [4071/4074] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows (3.8s)
⚠ [4072/4074] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (58s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:316:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3781:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3784:6: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3786:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: The following tactic starts with 2 goals and ends with 2 goals, 1 of which is not operated on.
  ring
Please focus on the current goal, for instance using `·` (typed as "\.").

Note: This linter can be disabled with `set_option linter.style.multiGoal false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3827:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3830:8: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3836:4: `have h63 :=
  theorem_6_3 (by linarith : 14 ≤ x₁) x₂.toReal
    (by
      cases x₂ <;> norm_num at *; · linarith;
      · exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
    x hx₁
    (by
      cases x₂ <;> norm_num at *; · linarith;
      · exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
    (by
      cases x₂ <;> norm_num at *; · exact_mod_cast hc;
      · exact mul_nonneg (by linarith) (Real.log_nonneg (by linarith)))` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3846:4: `unfold μ_num_1` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: `simp_all +decide [ mul_assoc, mul_comm, mul_left_comm ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: Try this:
  [apply] simp_all +decide only [Fin.Iio_last_eq_map, Finset.sum_sub_distrib, Finset.sum_map, Fin.coe_castSuccEmb,
    Fin.coeSucc_eq_succ, ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3849:6: `exact absurd (this y hy₁) (by norm_num [h]; linarith)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3858:6: `exact absurd ‹_› (not_le_of_gt hc)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4652:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4679:8: declaration uses `sorry`
✔ [4073/4081] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch (17s)
✔ [4087/4108] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore (18s)
✔ [4091/4108] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13 (13s)
✔ [4092/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12 (21s)
✔ [4093/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11 (21s)
✔ [4094/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10 (22s)
✔ [4095/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09 (21s)
✔ [4096/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08 (22s)
✔ [4097/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07 (21s)
✔ [4098/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06 (22s)
✔ [4099/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05 (21s)
✔ [4100/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04 (21s)
✔ [4101/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03 (21s)
✔ [4102/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02 (21s)
✔ [4103/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01 (21s)
✔ [4104/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00 (21s)
⚠ [4107/4111] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext (3.9s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4109/4128] Built PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor (6.9s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
⚠ [4121/4165] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2061:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4127/4167] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (9.4s)
⚠ [4145/4173] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (14s)
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:93:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:104:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:117:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:154:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:179:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:187:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:195:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:341:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:470:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:564:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:573:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:591:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:600:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:616:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:625:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:678:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:687:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:696:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:756:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:767:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:778:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:788:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:805:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:814:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:937:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:957:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:987:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1013:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1027:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1035:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1050:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1065:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1074:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1089:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1107:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1119:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1136:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1183:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1254:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1306:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1334:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1369:8: declaration uses `sorry`
⚠ [4153/4189] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.3s)
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:214:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:338:8: declaration uses `sorry`
ℹ [4158/4189] Replayed PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
⚠ [4159/4189] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline

Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
✔ [4164/4189] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (11s)
⚠ [4167/4189] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (6.3s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4170/4189] Built PrimeNumberTheoremAnd.IEANTN.Lcm (27s)
✔ [4171/4189] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (53s)
✔ [4181/4189] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.6s)
⚠ [4187/4189] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:134:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:496:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1443:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1613:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2843:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2869:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3475:8: declaration uses `sorry`
✔ [4188/4189] Built PrimeNumberTheoremAnd (4.3s)
Build completed successfully (4189 jobs).

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

blueprint_build exit 0 duration 10m 41s · created 7/11/2026, 6:04:35 AM

lake build :blueprint

✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (1.5s)
✔ [26/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (507ms)
✔ [33/41] Built Cli:c.o (69ms)
ℹ [3594/3611] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3619/3643] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
⚠ [3765/3784] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3891/3901] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3894/3901] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1305:16: declaration uses `sorry`
✔ [3899/3916] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (55s)
⚠ [3960/3986] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2577:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2578:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2599:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2600:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2817:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2818:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2833:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2834:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2963:4: `simp [W]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2964:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3069:4: `simp [p]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3070:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: `simp [Set.uIcc_of_le hab]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: Try this:
  [apply] simp only [_root_.deriv_ofReal]
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3085:4: `fun_prop` uses `⊢`!
⚠ [3962/3986] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [3970/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (28s)
⚠ [3971/3988] 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`
✔ [3974/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (3.6s)
✔ [3981/3990] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (3.0s)
⚠ [3982/3990] Replayed PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
✔ [3984/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (16s)
✔ [3985/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (9.7s)
✔ [3988/4006] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (6.8s)
⚠ [4107/4122] Replayed PrimeNumberTheoremAnd.IEANTN.Buthe
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
⚠ [4111/4126] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [4114/4126] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (6.3s)
⚠ [4115/4126] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
✔ [4119/4177] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (21s)
✔ [4120/4177] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (17s)
⚠ [4122/4177] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
✔ [4125/4186] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (24s)
✔ [4137/4198] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (5.1s)
ℹ [4139/4198] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
✔ [4143/4200] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (51s)
⚠ [4144/4200] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2634:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2723:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3093:4: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3685:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3713:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3725:8: declaration uses `sorry`
✔ [4145/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (3.2s)
✔ [4164/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (4.7s)
⚠ [4166/4206] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
✔ [4168/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next:blueprint (3.2s)
✔ [4169/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values:blueprint (3.2s)
✔ [4171/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85:blueprint (3.3s)
✔ [4172/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95:blueprint (3.1s)
✔ [4173/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875:blueprint (3.2s)
✔ [4174/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375:blueprint (3.2s)
✔ [4175/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875:blueprint (3.2s)
✔ [4176/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375:blueprint (3.2s)
✔ [4177/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875:blueprint (3.2s)
✔ [4178/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375:blueprint (3.1s)
✔ [4179/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875:blueprint (3.2s)
✔ [4180/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500:blueprint (3.2s)
✔ [4181/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500:blueprint (3.1s)
✔ [4182/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500:blueprint (3.2s)
✔ [4183/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500:blueprint (3.2s)
✔ [4184/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000:blueprint (3.1s)
✔ [4185/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc:blueprint (3.2s)
✔ [4186/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (20s)
⚠ [4189/4206] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:736:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:748:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:760:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:772:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:784:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:808:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:820:8: declaration uses `sorry`
✔ [4193/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43:blueprint (3.3s)
✔ [4195/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (18s)
✔ [4196/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (19s)
⚠ [4198/4206] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:316:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3781:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3784:6: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3786:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: The following tactic starts with 2 goals and ends with 2 goals, 1 of which is not operated on.
  ring
Please focus on the current goal, for instance using `·` (typed as "\.").

Note: This linter can be disabled with `set_option linter.style.multiGoal false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3827:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3830:8: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3836:4: `have h63 :=
  theorem_6_3 (by linarith : 14 ≤ x₁) x₂.toReal
    (by
      cases x₂ <;> norm_num at *; · linarith;
      · exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
    x hx₁
    (by
      cases x₂ <;> norm_num at *; · linarith;
      · exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
    (by
      cases x₂ <;> norm_num at *; · exact_mod_cast hc;
      · exact mul_nonneg (by linarith) (Real.log_nonneg (by linarith)))` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3846:4: `unfold μ_num_1` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: `simp_all +decide [ mul_assoc, mul_comm, mul_left_comm ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: Try this:
  [apply] simp_all +decide only [Fin.Iio_last_eq_map, Finset.sum_sub_distrib, Finset.sum_map, Fin.coe_castSuccEmb,
    Fin.coeSucc_eq_succ, ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3849:6: `exact absurd (this y hy₁) (by norm_num [h]; linarith)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3858:6: `exact absurd ‹_› (not_le_of_gt hc)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4652:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4679:8: declaration uses `sorry`
✔ [4199/4211] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59:blueprint (3.2s)
✔ [4202/4211] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (33s)
✔ [4203/4213] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (3.2s)
✔ [4206/4214] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (16s)
✔ [4220/4259] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore:blueprint (3.2s)
✔ [4241/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00:blueprint (3.2s)
✔ [4242/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01:blueprint (3.2s)
✔ [4243/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02:blueprint (3.1s)
✔ [4244/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03:blueprint (3.1s)
✔ [4245/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04:blueprint (3.2s)
✔ [4246/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05:blueprint (3.2s)
✔ [4247/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06:blueprint (3.2s)
✔ [4248/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07:blueprint (3.1s)
✔ [4249/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08:blueprint (3.2s)
✔ [4250/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09:blueprint (3.1s)
✔ [4251/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10:blueprint (3.2s)
✔ [4252/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11:blueprint (3.1s)
✔ [4253/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12:blueprint (3.1s)
✔ [4254/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13:blueprint (3.1s)
⚠ [4255/4261] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
✔ [4257/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext:blueprint (3.2s)
⚠ [4258/4262] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
✔ [4260/4290] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor:blueprint (5.4s)
⚠ [4270/4290] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2061:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4299/4399] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.1s)
⚠ [4300/4399] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:93:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:104:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:117:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:154:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:179:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:187:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:195:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:341:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:470:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:564:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:573:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:591:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:600:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:616:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:625:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:678:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:687:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:696:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:756:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:767:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:778:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:788:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:805:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:814:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:937:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:957:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:987:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1013:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1027:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1035:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1050:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1065:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1074:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1089:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1107:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1119:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1136:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1183:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1254:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1306:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1334:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1369:8: declaration uses `sorry`
ℹ [4328/4399] Replayed PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
⚠ [4329/4399] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline

Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
✔ [4331/4399] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (45s)
⚠ [4332/4399] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:214:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:338:8: declaration uses `sorry`
✔ [4352/4399] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (10s)
✔ [4353/4399] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (7.3s)
⚠ [4354/4399] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4367/4399] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.3s)
✔ [4373/4399] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (11s)
✔ [4374/4399] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (3.2s)
✔ [4375/4399] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (15s)
⚠ [4394/4399] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:134:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:496:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1443:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1613:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2843:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2869:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3475:8: declaration uses `sorry`
✔ [4397/4400] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (6.6s)
ℹ [4398/4400] Replayed PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint
info: Blueprint indexing
Build completed successfully (4400 jobs).

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

git_clone exit 0 duration 1s · created 7/11/2026, 6:04:35 AM

git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-1101-source

Cloning into '/var/lib/apodeixis/repos/job-1101-source'...

git_checkout exit 128 duration 2 ms · created 7/11/2026, 6:04:35 AM

git checkout c16e19c49cdb8f452265de8515c1fa55c074e559

fatal: reference is not a tree: c16e19c49cdb8f452265de8515c1fa55c074e559

git_checkout exit 0 duration 942 ms · created 7/11/2026, 6:04:35 AM

git fetch --depth 1 origin c16e19c49cdb8f452265de8515c1fa55c074e559

From https://github.com/AlexKontorovich/PrimeNumberTheoremAnd
 * branch            c16e19c49cdb8f452265de8515c1fa55c074e559 -> FETCH_HEAD

git_checkout exit 0 duration 76 ms · created 7/11/2026, 6:04:35 AM

git checkout c16e19c49cdb8f452265de8515c1fa55c074e559 (after fetch)

Note: switching to 'c16e19c49cdb8f452265de8515c1fa55c074e559'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:

  git switch -c <new-branch-name>

Or undo this operation with:

  git switch -

Turn off this advice by setting config variable advice.detachedHead to false

HEAD is now at c16e19c Update Mertens.lean (#1611)

lake_cache exit 0 duration 50s · created 7/11/2026, 6:04:35 AM

lake exe cache get

Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 file(s)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8459 = 0%, 2 KB/s], Decompressed: 14
Downloaded: 39 file(s) [attempted 39/8459 = 0%, 15 KB/s], Decompressed: 32
Downloaded: 62 file(s) [attempted 62/8459 = 0%, 329 KB/s], Decompressed: 59
Downloaded: 86 file(s) [attempted 86/8459 = 1%, 429 KB/s], Decompressed: 82
Downloaded: 110 file(s) [attempted 110/8459 = 1%, 47 KB/s], Decompressed: 107
Downloaded: 145 file(s) [attempted 145/8459 = 1%, 85 KB/s], Decompressed: 141
Downloaded: 175 file(s) [attempted 175/8459 = 2%, 504 KB/s], Decompressed: 172
Downloaded: 210 file(s) [attempted 210/8459 = 2%, 275 KB/s], Decompressed: 206
Downloaded: 244 file(s) [attempted 244/8459 = 2%, 305 KB/s], Decompressed: 240
Downloaded: 275 file(s) [attempted 275/8459 = 3%, 172 KB/s], Decompressed: 268
Downloaded: 316 file(s) [attempted 316/8459 = 3%, 649 KB/s], Decompressed: 312
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 48 KB/s], Decompressed: 347
Downloaded: 388 file(s) [attempted 388/8459 = 4%, 1016 KB/s], Decompressed: 381
Downloaded: 425 file(s) [attempted 425/8459 = 5%, 910 KB/s], Decompressed: 422
Downloaded: 460 file(s) [attempted 460/8459 = 5%, 875 KB/s], Decompressed: 456
Downloaded: 494 file(s) [attempted 494/8459 = 5%, 408 KB/s], Decompressed: 490
Downloaded: 528 file(s) [attempted 528/8459 = 6%, 463 KB/s], Decompressed: 521
Downloaded: 563 file(s) [attempted 563/8459 = 6%, 239 KB/s], Decompressed: 559
Downloaded: 600 file(s) [attempted 600/8459 = 7%, 164 KB/s], Decompressed: 597
Downloaded: 640 file(s) [attempted 640/8459 = 7%, 154 KB/s], Decompressed: 627
Downloaded: 669 file(s) [attempted 669/8459 = 7%, 106 KB/s], Decompressed: 658
Downloaded: 699 file(s) [attempted 699/8459 = 8%, 280 KB/s], Decompressed: 696
Downloaded: 735 file(s) [attempted 735/8459 = 8%, 344 KB/s], Decompressed: 730
Downloaded: 771 file(s) [attempted 771/8459 = 9%, 156 KB/s], Decompressed: 768
Downloaded: 806 file(s) [attempted 806/8459 = 9%, 108 KB/s], Decompressed: 802
Downloaded: 836 file(s) [attempted 836/8459 = 9%, 38 KB/s], Decompressed: 830
Downloaded: 867 file(s) [attempted 867/8459 = 10%, 268 KB/s], Decompressed: 864
Downloaded: 902 file(s) [attempted 902/8459 = 10%, 310 KB/s], Decompressed: 898
Downloaded: 938 file(s) [attempted 938/8459 = 11%, 172 KB/s], Decompressed: 932
Downloaded: 971 file(s) [attempted 971/8459 = 11%, 574 KB/s], Decompressed: 963
Downloaded: 998 file(s) [attempted 998/8459 = 11%, 478 KB/s], Decompressed: 994
Downloaded: 1032 file(s) [attempted 1032/8459 = 12%, 1180 KB/s], Decompressed: 1028
Downloaded: 1066 file(s) [attempted 1066/8459 = 12%, 349 KB/s], Decompressed: 1065
Downloaded: 1100 file(s) [attempted 1100/8459 = 13%, 433 KB/s], Decompressed: 1093
Downloaded: 1135 file(s) [attempted 1135/8459 = 13%, 1706 KB/s], Decompressed: 1131
Downloaded: 1165 file(s) [attempted 1165/8459 = 13%, 769 KB/s], Decompressed: 1162
Downloaded: 1210 file(s) [attempted 1210/8459 = 14%, 114 KB/s], Decompressed: 1199
Downloaded: 1254 file(s) [attempted 1254/8459 = 14%, 266 KB/s], Decompressed: 1247
Downloaded: 1292 file(s) [attempted 1292/8459 = 15%, 133 KB/s], Decompressed: 1288
Downloaded: 1333 file(s) [attempted 1333/8459 = 15%, 62 KB/s], Decompressed: 1329
Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 218 KB/s], Decompressed: 1367
Downloaded: 1411 file(s) [attempted 1411/8459 = 16%, 302 KB/s], Decompressed: 1401
Downloaded: 1449 file(s) [attempted 1449/8459 = 17%, 175 KB/s], Decompressed: 1446
Downloaded: 1490 file(s) [attempted 1490/8459 = 17%, 2002 KB/s], Decompressed: 1487
Downloaded: 1531 file(s) [attempted 1531/8459 = 18%, 363 KB/s], Decompressed: 1524
Downloaded: 1573 file(s) [attempted 1573/8459 = 18%, 496 KB/s], Decompressed: 1569
Downloaded: 1613 file(s) [attempted 1613/8459 = 19%, 561 KB/s], Decompressed: 1607
Downloaded: 1648 file(s) [attempted 1648/8459 = 19%, 156 KB/s], Decompressed: 1644
Downloaded: 1689 file(s) [attempted 1689/8459 = 19%, 324 KB/s], Decompressed: 1682
Downloaded: 1726 file(s) [attempted 1726/8459 = 20%, 1699 KB/s], Decompressed: 1723
Downloaded: 1771 file(s) [attempted 1771/8459 = 20%, 473 KB/s], Decompressed: 1761
Downloaded: 1807 file(s) [attempted 1807/8459 = 21%, 274 KB/s], Decompressed: 1802
Downloaded: 1850 file(s) [attempted 1850/8459 = 21%, 751 KB/s], Decompressed: 1846
Downloaded: 1887 file(s) [attempted 1887/8459 = 22%, 297 KB/s], Decompressed: 1884
Downloaded: 1925 file(s) [attempted 1925/8459 = 22%, 74 KB/s], Decompressed: 1921
Downloaded: 1963 file(s) [attempted 1963/8459 = 23%, 923 KB/s], Decompressed: 1959
Downloaded: 2007 file(s) [attempted 2007/8459 = 23%, 273 KB/s], Decompressed: 2004
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 190 KB/s], Decompressed: 2045
Downloaded: 2086 file(s) [attempted 2086/8459 = 24%, 79 KB/s], Decompressed: 2082
Downloaded: 2127 file(s) [attempted 2127/8459 = 25%, 275 KB/s], Decompressed: 2123
Downloaded: 2162 file(s) [attempted 2162/8459 = 25%, 317 KB/s], Decompressed: 2158
Downloaded: 2202 file(s) [attempted 2202/8459 = 26%, 172 KB/s], Decompressed: 2199
Downloaded: 2242 file(s) [attempted 2242/8459 = 26%, 1216 KB/s], Decompressed: 2236
Downloaded: 2281 file(s) [attempted 2281/8459 = 26%, 196 KB/s], Decompressed: 2277
Downloaded: 2318 file(s) [attempted 2318/8459 = 27%, 441 KB/s], Decompressed: 2315
Downloaded: 2360 file(s) [attempted 2360/8459 = 27%, 115 KB/s], Decompressed: 2353
Downloaded: 2401 file(s) [attempted 2401/8459 = 28%, 944 KB/s], Decompressed: 2390
Downloaded: 2438 file(s) [attempted 2438/8459 = 28%, 191 KB/s], Decompressed: 2435
Downloaded: 2479 file(s) [attempted 2479/8459 = 29%, 357 KB/s], Decompressed: 2472
Downloaded: 2518 file(s) [attempted 2518/8459 = 29%, 51 KB/s], Decompressed: 2514
Downloaded: 2561 file(s) [attempted 2561/8459 = 30%, 791 KB/s], Decompressed: 2555
Downloaded: 2599 file(s) [attempted 2599/8459 = 30%, 123 KB/s], Decompressed: 2596
Downloaded: 2641 file(s) [attempted 2641/8459 = 31%, 25 KB/s], Decompressed: 2637
Downloaded: 2678 file(s) [attempted 2678/8459 = 31%, 64 KB/s], Decompressed: 2674
Downloaded: 2722 file(s) [attempted 2722/8459 = 32%, 524 KB/s], Decompressed: 2719
Downloaded: 2760 file(s) [attempted 2760/8459 = 32%, 23 KB/s], Decompressed: 2753
Downloaded: 2801 file(s) [attempted 2801/8459 = 33%, 133 KB/s], Decompressed: 2791
Downloaded: 2841 file(s) [attempted 2841/8459 = 33%, 101 KB/s], Decompressed: 2832
Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 164 KB/s], Decompressed: 2873
Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 121 KB/s], Decompressed: 2914
Downloaded: 2958 file(s) [attempted 2958/8459 = 34%, 233 KB/s], Decompressed: 2952
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 185 KB/s], Decompressed: 2989
Downloaded: 3037 file(s) [attempted 3037/8459 = 35%, 150 KB/s], Decompressed: 3027
Downloaded: 3075 file(s) [attempted 3075/8459 = 36%, 875 KB/s], Decompressed: 3071
Downloaded: 3116 file(s) [attempted 3116/8459 = 36%, 75 KB/s], Decompressed: 3102
Downloaded: 3156 file(s) [attempted 3156/8459 = 37%, 315 KB/s], Decompressed: 3150
Downloaded: 3195 file(s) [attempted 3195/8459 = 37%, 416 KB/s], Decompressed: 3191
Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 170 KB/s], Decompressed: 3225
Downloaded: 3273 file(s) [attempted 3273/8459 = 38%, 250 KB/s], Decompressed: 3270
Downloaded: 3313 file(s) [attempted 3313/8459 = 39%, 284 KB/s], Decompressed: 3307
Downloaded: 3353 file(s) [attempted 3353/8459 = 39%, 51 KB/s], Decompressed: 3345
Downloaded: 3390 file(s) [attempted 3390/8459 = 40%, 260 KB/s], Decompressed: 3386
Downloaded: 3428 file(s) [attempted 3428/8459 = 40%, 477 KB/s], Decompressed: 3424
Downloaded: 3467 file(s) [attempted 3467/8459 = 40%, 135 KB/s], Decompressed: 3458
Downloaded: 3503 file(s) [attempted 3503/8459 = 41%, 81 KB/s], Decompressed: 3499
Downloaded: 3547 file(s) [attempted 3547/8459 = 41%, 461 KB/s], Decompressed: 3544
Downloaded: 3588 file(s) [attempted 3588/8459 = 42%, 546 KB/s], Decompressed: 3585
Downloaded: 3629 file(s) [attempted 3629/8459 = 42%, 59 KB/s], Decompressed: 3622
Downloaded: 3670 file(s) [attempted 3670/8459 = 43%, 442 KB/s], Decompressed: 3667
Downloaded: 3707 file(s) [attempted 3707/8459 = 43%, 84 KB/s], Decompressed: 3701
Downloaded: 3749 file(s) [attempted 3749/8459 = 44%, 393 KB/s], Decompressed: 3746
Downloaded: 3790 file(s) [attempted 3790/8459 = 44%, 365 KB/s], Decompressed: 3787
Downloaded: 3831 file(s) [attempted 3831/8459 = 45%, 91 KB/s], Decompressed: 3824
Downloaded: 3872 file(s) [attempted 3872/8459 = 45%, 1218 KB/s], Decompressed: 3869
Downloaded: 3913 file(s) [attempted 3913/8459 = 46%, 144 KB/s], Decompressed: 3910
Downloaded: 3954 file(s) [attempted 3954/8459 = 46%, 198 KB/s], Decompressed: 3951
Downloaded: 3995 file(s) [attempted 3995/8459 = 47%, 200 KB/s], Decompressed: 3985
Downloaded: 4030 file(s) [attempted 4030/8459 = 47%, 106 KB/s], Decompressed: 4019
Downloaded: 4069 file(s) [attempted 4069/8459 = 48%, 292 KB/s], Decompressed: 4060
Downloaded: 4108 file(s) [attempted 4108/8459 = 48%, 380 KB/s], Decompressed: 4105
Downloaded: 4153 file(s) [attempted 4153/8459 = 49%, 45 KB/s], Decompressed: 4146
Downloaded: 4190 file(s) [attempted 4190/8459 = 49%, 323 KB/s], Decompressed: 4187
Downloaded: 4232 file(s) [attempted 4232/8459 = 50%, 501 KB/s], Decompressed: 4228
Downloaded: 4271 file(s) [attempted 4271/8459 = 50%, 95 KB/s], Decompressed: 4262
Downloaded: 4310 file(s) [attempted 4310/8459 = 50%, 90 KB/s], Decompressed: 4303
Downloaded: 4351 file(s) [attempted 4351/8459 = 51%, 484 KB/s], Decompressed: 4345
Downloaded: 4392 file(s) [attempted 4392/8459 = 51%, 35 KB/s], Decompressed: 4386
Downloaded: 4430 file(s) [attempted 4430/8459 = 52%, 102 KB/s], Decompressed: 4427
Downloaded: 4468 file(s) [attempted 4468/8459 = 52%, 53 KB/s], Decompressed: 4464
Downloaded: 4512 file(s) [attempted 4512/8459 = 53%, 267 KB/s], Decompressed: 4509
Downloaded: 4553 file(s) [attempted 4553/8459 = 53%, 479 KB/s], Decompressed: 4546
Downloaded: 4587 file(s) [attempted 4587/8459 = 54%, 282 KB/s], Decompressed: 4584
Downloaded: 4629 file(s) [attempted 4629/8459 = 54%, 44 KB/s], Decompressed: 4625
Downloaded: 4673 file(s) [attempted 4673/8459 = 55%, 424 KB/s], Decompressed: 4666
Downloaded: 4708 file(s) [attempted 4708/8459 = 55%, 160 KB/s], Decompressed: 4704
Downloaded: 4748 file(s) [attempted 4748/8459 = 56%, 118 KB/s], Decompressed: 4745
Downloaded: 4786 file(s) [attempted 4786/8459 = 56%, 62 KB/s], Decompressed: 4783
Downloaded: 4827 file(s) [attempted 4827/8459 = 57%, 397 KB/s], Decompressed: 4820
Downloaded: 4868 file(s) [attempted 4868/8459 = 57%, 196 KB/s], Decompressed: 4861
Downloaded: 4909 file(s) [attempted 4909/8459 = 58%, 272 KB/s], Decompressed: 4906
Downloaded: 4943 file(s) [attempted 4943/8459 = 58%, 433 KB/s], Decompressed: 4937
Downloaded: 4988 file(s) [attempted 4988/8459 = 58%, 111 KB/s], Decompressed: 4981
Downloaded: 5032 file(s) [attempted 5032/8459 = 59%, 219 KB/s], Decompressed: 5022
Downloaded: 5073 file(s) [attempted 5073/8459 = 59%, 473 KB/s], Decompressed: 5063
Downloaded: 5111 file(s) [attempted 5111/8459 = 60%, 449 KB/s], Decompressed: 5104
Downloaded: 5152 file(s) [attempted 5152/8459 = 60%, 129 KB/s], Decompressed: 5145
Downloaded: 5190 file(s) [attempted 5190/8459 = 61%, 155 KB/s], Decompressed: 5186
Downloaded: 5231 file(s) [attempted 5231/8459 = 61%, 251 KB/s], Decompressed: 5227
Downloaded: 5275 file(s) [attempted 5275/8459 = 62%, 263 KB/s], Decompressed: 5269
Downloaded: 5306 file(s) [attempted 5306/8459 = 62%, 25 KB/s], Decompressed: 5299
Downloaded: 5347 file(s) [attempted 5347/8459 = 63%, 143 KB/s], Decompressed: 5344
Downloaded: 5388 file(s) [attempted 5388/8459 = 63%, 75 KB/s], Decompressed: 5385
Downloaded: 5428 file(s) [attempted 5428/8459 = 64%, 199 KB/s], Decompressed: 5423
Downloaded: 5470 file(s) [attempted 5470/8459 = 64%, 278 KB/s], Decompressed: 5460
Downloaded: 5507 file(s) [attempted 5507/8459 = 65%, 299 KB/s], Decompressed: 5501
Downloaded: 5546 file(s) [attempted 5546/8459 = 65%, 1634 KB/s], Decompressed: 5539
Downloaded: 5587 file(s) [attempted 5587/8459 = 66%, 57 KB/s], Decompressed: 5583
Downloaded: 5625 file(s) [attempted 5625/8459 = 66%, 115 KB/s], Decompressed: 5621
Downloaded: 5663 file(s) [attempted 5663/8459 = 66%, 1309 KB/s], Decompressed: 5659
Downloaded: 5698 file(s) [attempted 5698/8459 = 67%, 339 KB/s], Decompressed: 5693
Downloaded: 5737 file(s) [attempted 5737/8459 = 67%, 67 KB/s], Decompressed: 5731
Downloaded: 5779 file(s) [attempted 5779/8459 = 68%, 115 KB/s], Decompressed: 5772
Downloaded: 5820 file(s) [attempted 5820/8459 = 68%, 103 KB/s], Decompressed: 5816
Downloaded: 5854 file(s) [attempted 5854/8459 = 69%, 93 KB/s], Decompressed: 5850
Downloaded: 5892 file(s) [attempted 5892/8459 = 69%, 174 KB/s], Decompressed: 5888
Downloaded: 5932 file(s) [attempted 5932/8459 = 70%, 1153 KB/s], Decompressed: 5929
Downloaded: 5977 file(s) [attempted 5977/8459 = 70%, 270 KB/s], Decompressed: 5974
Downloaded: 6021 file(s) [attempted 6021/8459 = 71%, 221 KB/s], Decompressed: 6015
Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 155 KB/s], Decompressed: 6052
Downloaded: 6093 file(s) [attempted 6093/8459 = 72%, 1246 KB/s], Decompressed: 6090
Downloaded: 6134 file(s) [attempted 6134/8459 = 72%, 221 KB/s], Decompressed: 6128
Downloaded: 6179 file(s) [attempted 6179/8459 = 73%, 45 KB/s], Decompressed: 6175
Downloaded: 6223 file(s) [attempted 6223/8459 = 73%, 176 KB/s], Decompressed: 6217
Downloaded: 6264 file(s) [attempted 6264/8459 = 74%, 328 KB/s], Decompressed: 6261
Downloaded: 6306 file(s) [attempted 6306/8459 = 74%, 500 KB/s], Decompressed: 6295
Downloaded: 6340 file(s) [attempted 6340/8459 = 74%, 58 KB/s], Decompressed: 6336
Downloaded: 6384 file(s) [attempted 6384/8459 = 75%, 121 KB/s], Decompressed: 6377
Downloaded: 6425 file(s) [attempted 6425/8459 = 75%, 218 KB/s], Decompressed: 6418
Downloaded: 6466 file(s) [attempted 6466/8459 = 76%, 86 KB/s], Decompressed: 6460
Downloaded: 6505 file(s) [attempted 6505/8459 = 76%, 78 KB/s], Decompressed: 6497
Downloaded: 6538 file(s) [attempted 6538/8459 = 77%, 553 KB/s], Decompressed: 6535
Downloaded: 6583 file(s) [attempted 6583/8459 = 77%, 81 KB/s], Decompressed: 6579
Downloaded: 6622 file(s) [attempted 6622/8459 = 78%, 556 KB/s], Decompressed: 6617
Downloaded: 6661 file(s) [attempted 6661/8459 = 78%, 156 KB/s], Decompressed: 6658
Downloaded: 6700 file(s) [attempted 6700/8459 = 79%, 121 KB/s], Decompressed: 6685
Downloaded: 6740 file(s) [attempted 6740/8459 = 79%, 292 KB/s], Decompressed: 6737
Downloaded: 6780 file(s) [attempted 6780/8459 = 80%, 81 KB/s], Decompressed: 6771
Downloaded: 6817 file(s) [attempted 6817/8459 = 80%, 805 KB/s], Decompressed: 6812
Downloaded: 6857 file(s) [attempted 6857/8459 = 81%, 396 KB/s], Decompressed: 6853
Downloaded: 6898 file(s) [attempted 6898/8459 = 81%, 895 KB/s], Decompressed: 6894
Downloaded: 6942 file(s) [attempted 6942/8459 = 82%, 264 KB/s], Decompressed: 6935
Downloaded: 6976 file(s) [attempted 6976/8459 = 82%, 54 KB/s], Decompressed: 6973
Downloaded: 7019 file(s) [attempted 7019/8459 = 82%, 461 KB/s], Decompressed: 7007
Downloaded: 7058 file(s) [attempted 7058/8459 = 83%, 101 KB/s], Decompressed: 7052
Downloaded: 7103 file(s) [attempted 7103/8459 = 83%, 288 KB/s], Decompressed: 7099
Downloaded: 7141 file(s) [attempted 7141/8459 = 84%, 646 KB/s], Decompressed: 7137
Downloaded: 7182 file(s) [attempted 7182/8459 = 84%, 91 KB/s], Decompressed: 7178
Downloaded: 7226 file(s) [attempted 7226/8459 = 85%, 453 KB/s], Decompressed: 7219
Downloaded: 7267 file(s) [attempted 7267/8459 = 85%, 805 KB/s], Decompressed: 7257
Downloaded: 7308 file(s) [attempted 7308/8459 = 86%, 378 KB/s], Decompressed: 7305
Downloaded: 7349 file(s) [attempted 7349/8459 = 86%, 295 KB/s], Decompressed: 7342
Downloaded: 7384 file(s) [attempted 7384/8459 = 87%, 57 KB/s], Decompressed: 7380
Downloaded: 7428 file(s) [attempted 7428/8459 = 87%, 100 KB/s], Decompressed: 7421
Downloaded: 7469 file(s) [attempted 7469/8459 = 88%, 301 KB/s], Decompressed: 7462
Downloaded: 7508 file(s) [attempted 7508/8459 = 88%, 213 KB/s], Decompressed: 7500
Downloaded: 7544 file(s) [attempted 7544/8459 = 89%, 211 KB/s], Decompressed: 7541
Downloaded: 7582 file(s) [attempted 7582/8459 = 89%, 118 KB/s], Decompressed: 7579
Downloaded: 7623 file(s) [attempted 7623/8459 = 90%, 1299 KB/s], Decompressed: 7620
Downloaded: 7671 file(s) [attempted 7671/8459 = 90%, 39 KB/s], Decompressed: 7668
Downloaded: 7709 file(s) [attempted 7709/8459 = 91%, 71 KB/s], Decompressed: 7705
Downloaded: 7743 file(s) [attempted 7743/8459 = 91%, 737 KB/s], Decompressed: 7736
Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 138 KB/s], Decompressed: 7781
Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 161 KB/s], Decompressed: 7822
Downloaded: 7870 file(s) [attempted 7870/8459 = 93%, 23 KB/s], Decompressed: 7863
Downloaded: 7909 file(s) [attempted 7909/8459 = 93%, 213 KB/s], Decompressed: 7900
Downloaded: 7941 file(s) [attempted 7941/8459 = 93%, 87 KB/s], Decompressed: 7938
Downloaded: 7979 file(s) [attempted 7979/8459 = 94%, 1928 KB/s], Decompressed: 7972
Downloaded: 8020 file(s) [attempted 8020/8459 = 94%, 44 KB/s], Decompressed: 8017
Downloaded: 8062 file(s) [attempted 8062/8459 = 95%, 161 KB/s], Decompressed: 8058
Downloaded: 8102 file(s) [attempted 8102/8459 = 95%, 152 KB/s], Decompressed: 8097
Downloaded: 8140 file(s) [attempted 8140/8459 = 96%, 106 KB/s], Decompressed: 8133
Downloaded: 8178 file(s) [attempted 8178/8459 = 96%, 98 KB/s], Decompressed: 8174
Downloaded: 8219 file(s) [attempted 8219/8459 = 97%, 143 KB/s], Decompressed: 8215
Downloaded: 8260 file(s) [attempted 8260/8459 = 97%, 113 KB/s], Decompressed: 8249
Downloaded: 8297 file(s) [attempted 8297/8459 = 98%, 125 KB/s], Decompressed: 8290
Downloaded: 8335 file(s) [attempted 8335/8459 = 98%, 1157 KB/s], Decompressed: 8332
Downloaded: 8374 file(s) [attempted 8374/8459 = 98%, 584 KB/s], Decompressed: 8369
Downloaded: 8417 file(s) [attempted 8417/8459 = 99%, 435 KB/s], Decompressed: 8414
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 111 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 111 KB/s], Decompressed: 8455

semantic_extract exit 0 duration 8m 25s · created 7/11/2026, 6:04:35 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-a)

apx-semantic-phase	{"duration_ms":23,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":354,"diagnostic_count":229,"duration_ms":31384,"module_name":"PrimeNumberTheoremAnd.IEANTN.Mertens","module_path":"PrimeNumberTheoremAnd/IEANTN/Mertens.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":417026,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Mertens","module_path":"PrimeNumberTheoremAnd/IEANTN/Mertens.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":354,"diagnostic_count":229,"duration_ms":22,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Mertens","module_path":"PrimeNumberTheoremAnd/IEANTN/Mertens.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":2005231,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":5,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":2005231,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":25}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":9158,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":51,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":494888,"ok":true}

semantic_extract exit 0 duration 22m 25s · created 7/11/2026, 6:04:35 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-b)

apx-semantic-phase	{"duration_ms":23,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":33,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimaryDefinitions.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":411318,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimaryDefinitions.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimaryDefinitions.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":510,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":510,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":471,"diagnostic_count":322,"duration_ms":48065,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaAppendix","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":424205,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaAppendix","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":471,"diagnostic_count":322,"duration_ms":24,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaAppendix","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":4207991,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":3,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":4207991,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":6,"diagnostic_count":0,"duration_ms":542,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaSummary","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":414493,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaSummary","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":6,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaSummary","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":11072,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":11072,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":21}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":11918,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":64,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1331787,"ok":true}

semantic_extract exit 0 duration 22m 13s · created 7/11/2026, 6:04:35 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r2)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":136,"diagnostic_count":71,"duration_ms":10690,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":442000,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":136,"diagnostic_count":71,"duration_ms":5,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":509774,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":509774,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":69,"diagnostic_count":54,"duration_ms":5063,"module_name":"PrimeNumberTheoremAnd.IEANTN.MobiusLemma","module_path":"PrimeNumberTheoremAnd/IEANTN/MobiusLemma.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":416535,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.MobiusLemma","module_path":"PrimeNumberTheoremAnd/IEANTN/MobiusLemma.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":69,"diagnostic_count":54,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.MobiusLemma","module_path":"PrimeNumberTheoremAnd/IEANTN/MobiusLemma.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":430031,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":430031,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":36,"diagnostic_count":27,"duration_ms":2705,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":428459,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":36,"diagnostic_count":27,"duration_ms":2,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":189395,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":189395,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":17062,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":39,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1314212,"ok":true}

semantic_extract exit 0 duration 37m 35s · created 7/11/2026, 6:04:35 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r3)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":57,"diagnostic_count":33,"duration_ms":4151,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":453149,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":57,"diagnostic_count":33,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":166420,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":166420,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":442,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":436728,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":74842,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":74842,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":610,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":435101,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":68407,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":68407,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":17,"diagnostic_count":10,"duration_ms":1353,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimeInInterval","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":433972,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimeInInterval","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":17,"diagnostic_count":10,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimeInInterval","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":101503,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":101503,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":297,"diagnostic_count":259,"duration_ms":22869,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":442457,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":297,"diagnostic_count":259,"duration_ms":15,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":1556361,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":1556361,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":17327,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":52,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":2236669,"ok":true}

semantic_extract exit 0 duration 31m 20s · created 7/11/2026, 6:04:35 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r4)

apx-semantic-phase	{"duration_ms":3,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":480,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":452888,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":77992,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":77992,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":402,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":445210,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":80054,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":80054,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":394,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":467953,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":82759,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":82759,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":362,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":451161,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":85603,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":85603,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":15127,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":28,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1863905,"ok":true}

semantic_extract exit 0 duration 29m 38s · created 7/11/2026, 6:04:35 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r5)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":428,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":432866,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":87967,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":87967,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":447,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":435056,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":90257,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":90257,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":396,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":439022,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":92539,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":92539,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":437,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":440278,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":94376,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":94376,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":19}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":17651,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":55,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1759727,"ok":true}

semantic_extract exit 0 duration 29m 59s · created 7/11/2026, 6:04:35 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r6)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":455,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":446274,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":96327,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":96327,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":466,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":443444,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":101240,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":101240,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":452,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":444736,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":102723,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":102723,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":466,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":440988,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":107456,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":107456,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":11119,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":48,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1787202,"ok":true}

semantic_extract exit 0 duration 22m 37s · created 7/11/2026, 6:04:35 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r7)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":150,"diagnostic_count":101,"duration_ms":11101,"module_name":"PrimeNumberTheoremAnd.IEANTN.Dusart","module_path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":419830,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Dusart","module_path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":150,"diagnostic_count":101,"duration_ms":13,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Dusart","module_path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":849814,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":849814,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":679,"diagnostic_count":493,"duration_ms":66055,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":425619,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":679,"diagnostic_count":493,"duration_ms":44,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":3913891,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":3913891,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":16,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":418150,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":502,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":502,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":10815,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":49,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1345726,"ok":true}

semantic_extract exit 0 duration 15m 1s · created 7/11/2026, 6:04:35 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r8)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":41,"diagnostic_count":6,"duration_ms":2784,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":433001,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":41,"diagnostic_count":6,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":344830,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":344830,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":258,"diagnostic_count":135,"duration_ms":21698,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":427742,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":258,"diagnostic_count":135,"duration_ms":9,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1269379,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1269379,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":21}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":10347,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":49,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":889864,"ok":true}

semantic_extract exit 0 duration 7m 28s · created 7/11/2026, 6:04:35 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r9)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":32,"diagnostic_count":19,"duration_ms":2395,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":430479,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":32,"diagnostic_count":19,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":94339,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":94339,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":10112,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":51,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":437504,"ok":true}

semantic_extract exit 0 duration 7m 33s · created 7/11/2026, 6:04:35 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r10)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":27,"diagnostic_count":9,"duration_ms":2050,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":435642,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":27,"diagnostic_count":9,"duration_ms":2,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":169753,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":169753,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":10130,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":45,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":442287,"ok":true}

semantic_extract exit 0 duration 7m 27s · created 7/11/2026, 6:04:35 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r11)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":67,"diagnostic_count":53,"duration_ms":5116,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":426880,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":67,"diagnostic_count":53,"duration_ms":5,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":257157,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":257157,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":9764,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":40,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":436601,"ok":true}

semantic_extract exit 0 duration 7m 40s · created 7/11/2026, 6:04:35 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r12)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":70,"diagnostic_count":54,"duration_ms":5074,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":439343,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":70,"diagnostic_count":54,"duration_ms":4,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":396745,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":396745,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":9990,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":52,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":448878,"ok":true}

semantic_extract exit 0 duration 8m 0s · created 7/11/2026, 6:04:35 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r13)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":235,"diagnostic_count":164,"duration_ms":18469,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":445326,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":235,"diagnostic_count":164,"duration_ms":23,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1491369,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1491369,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":25}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":10397,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":53,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":468890,"ok":true}

semantic_extract exit 0 duration 7m 58s · created 7/11/2026, 6:04:35 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r14)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":263,"diagnostic_count":178,"duration_ms":23345,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":439680,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":263,"diagnostic_count":178,"duration_ms":27,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1806664,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1806664,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":25}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":9741,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache d4df49831f0c286c4ca0c45d627e138315a8ca7e90d610b0ec7d6357c25bfb69
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":43,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":467557,"ok":true}