diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9da23e50c..6e694fefd 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -56,6 +56,10 @@ jobs: python3 scripts/ci/check_benches_mathlib_free.py - name: Verify conformance matrix invariant run: python3 scripts/conformance_targets.py --check + - name: Validate committed PNT+ inventory (offline) + run: | + python3 -m unittest scripts/maintenance/test_pnt_inventory.py + python3 scripts/maintenance/pnt_inventory.py --check # --- System + Python deps (union of the bench comparator and the oracles) --- - name: Install system dependencies run: | diff --git a/SPEC/Libraries/hex-interval-mathlib.md b/SPEC/Libraries/hex-interval-mathlib.md index acb3e2077..2ade0c763 100644 --- a/SPEC/Libraries/hex-interval-mathlib.md +++ b/SPEC/Libraries/hex-interval-mathlib.md @@ -1019,9 +1019,12 @@ invocations, and 290 textual occurrences including ten explanatory prose or comment mentions, across 15 files. These counts define the audit surface, not a promise to clone every LeanCert API or preserve PNT+ source syntax. A checked manifest records the PNT+ commit, LeanCert pin, Lean toolchain and Mathlib -revision, every source occurrence's file and enclosing declaration, and the -generated batch families that one source occurrence expands into. Every entry -is classified as one of: +revision, every executable occurrence's file and enclosing declaration, raw +textual matches by file and line, and the generated batch families that one +source occurrence expands into. Declaration labels are the nearest preceding +declaration header found by the lexical scan, not elaborated ownership. Every +entry that represents executable or imported behavior is ultimately classified +as one of: - accepted unchanged by a Hex frontend; - accepted after a documented PNT+ source rewrite or proof reorganization; @@ -1031,6 +1034,22 @@ is classified as one of: - redundant, malformed, or a known false target with an expected-failure enclosure. +Before the D8 migration is performed, `pending` is an explicit allowed state; +raw matches in comments or strings are classified `not-a-call`. Qualified +LeanCert references are lexical audit evidence classified `inventory-only`; +the six imported-interface records, rather than every namespace-open token, +carry the migration obligation. The ordinary per-PR structural gate permits +`pending` so that adding the inventory does not pretend the port already +exists. The D8 migration/release gate must run the same checker with +`--require-classified`, which rejects every remaining obligation marked +`pending`. A completed classification also carries structured evidence: an +accepted fixture, documented rewrite, stronger replacement theorem, retained +dependency, or expected-failure fixture as appropriate. The release claim +requires both this classified manifest and the referenced ported proofs; a +status label alone cannot establish coverage. The inventory checker validates +that evidence references are structured and nonempty; the release profile must +also build and axiom-audit the referenced proof fixtures. + Refreshing an upstream pin must regenerate and review the manifest. The inventory prevents blind spots; it does not make exact-source compatibility a release criterion. It must cover, at minimum: @@ -1039,8 +1058,16 @@ release criterion. It must cover, at minimum: invocations, including nested logarithms, large exponential arguments, square roots, pi, and tails down to `10^-100`; - all 132 BKLNW textual occurrences across nine files, of which 128 are actual - tactic invocations, including the generated Table 10 and roughly 135-check - Table 12 batches rather than merely their outer tactic call sites; and + tactic invocations. The generated Table 10 row sources contain 87 target + proof sites and 38 supporting `a₂`-bound proof sites. The Table 12 theorem + expands to 130 checks: 24 ordinary rows by five columns plus two logarithmic + rows by five columns. The row partition is structurally derived from the + exact pinned list definition, including a first tuple placed on the opening + bracket's line; the five-column expansion is a reviewed reading of the + theorem's conjunction and tactic structure. Table 10 is currently recorded + at executable call-site granularity; complete row/column expansion is part + of its D9 shard work. Both families are recorded separately from their + aggregate source counts; and - all 17 remaining textual occurrences, of which 16 are actual tactic invocations, in `Dusart.lean`, `FKS2.lean`, `FKS2Cor23Cor14Tail.lean`, `FKS2Floor/Cor22Floor.lean`, and `Goldbach.lean`. @@ -1048,23 +1075,44 @@ release criterion. It must cover, at minimum: The complete 13,590-cell FKS2 stream is a generated workload in addition to this source-occurrence inventory. Counting the 280 actual tactic invocations while omitting that generated stream misses the main batch workload. -Conversely, importing the already-proved FKS2 result does not exercise Hex. A -drift check fails when the pinned PNT+ commit, LeanCert pin, toolchain, Mathlib -revision, occurrence inventory, or batch sizes change without an explicit -SPEC and fixture refresh. +Conversely, importing the already-proved FKS2 result does not exercise Hex. The +network-free per-PR gate detects an inconsistent or unexplained local change to +the pinned commit, dependency revisions, occurrence inventory, or batch sizes. +Because the upstream commit is immutable, checking for a deliberately updated +upstream pin is a maintainer operation: `--verify-source` regenerates from the +exact checkout and requires an explicit SPEC, constants, and fixture refresh. The committed inventory lives at `conformance-fixtures/HexIntervalMathlib/pnt-inventory.jsonl` and is generated -by `scripts/maintenance/pnt_inventory.py`. The generator tokenizes pinned Lean -sources, counts tactic identifiers outside comments and string literals, -records their enclosing declarations, separately records raw textual matches, -and expands the named generated-data families. Per-PR CI and the mandatory -release profile validate the committed manifest without network access. A -separate maintainer refresh command checks out the recorded upstream revisions, -regenerates it, and requires a reviewed diff when any count, classification, -toolchain, or batch size changes. These artifacts are D8 deliverables; the -paths name the required interface and do not imply that they exist before that -milestone. +by `scripts/maintenance/pnt_inventory.py`. The generator uses an +offset-preserving lexical mask over pinned Lean sources, counts tactic +identifiers outside nested comments and string literals, records the nearest +preceding declaration header, separately records raw textual matches, audits +the six directly imported LeanCert interface families, and expands the named +generated-data families. The committed metadata pins all 232 tracked Lean +source files in the PNT+ repository, records that count in the fixture, and +stores a digest of the fixed audit-record identity. That second digest covers +source locations together with reviewed interface roles and generated-workload +annotations; it is not presented as a pure parser result. Migration +classifications are deliberately excluded so +they can be filled in without weakening audit identity. After editing +classifications, `--update-classifications` validates their schema and refreshes +only the full record digest. `--refresh` carries existing decisions forward by +exact audit identity and refuses to discard a classified record; +`--verify-source` compares audit identity while allowing those decisions to +differ from freshly generated `pending` defaults. + +Per-PR CI runs the generator's unit tests and validates the committed manifest +without network access. For a pin bump, `--inspect-source --source +` reports the observed pins, digest, counts, imported modules, +and generated families without accepting or writing them. A maintainer reviews +that report, updates the constants and workload partitions, then uses +`--refresh` to reseal the fixture. Independent source verification uses +`--verify-source`; the accepting commands refuse an unreviewed difference in +HEAD, dependency pins, toolchain, Lean-source digest, counts, import surface, +or batch sizes. The artifacts exist before D8 as an audited backlog and local +integrity gate; they become a migration claim only when the classifications +and ported proof fixtures are complete. `interval_decide` is not the complete PNT+ dependency surface. The same pinned tree has 60 actual `interval_auto` calls in `TMEEMT.lean` and @@ -1090,8 +1138,26 @@ They therefore belong to the audit even though they do not spell tactic entry points as well as the certified-bound interfaces. The compatibility manifest records every `interval_auto` invocation, every -direct LeanCert import, every referenced LeanCert declaration, and every use of -compiled evaluation to establish a LeanCert checker result. A migration may +direct LeanCert import, and every qualified `LeanCert.` reference +outside comments and string literals, +the load-bearing role of each of the six imported public interface families, +and every executable textual `native_decide` occurrence as a starting list of +compiler-trusting proof sites. This lexical list is not the authoritative +trust audit: macro expansion and transitive dependencies are checked from the +ported theorems' axiom sets under the Axiom contract below. A lexical scan +cannot soundly name-resolve an +unqualified theorem used after `open`; the corresponding import/interface +record is the durable backlog item, and migration review must classify that +interface before it can leave `pending`. Qualified-reference occurrences are +inventory-only evidence beneath that decision. Each record names its reviewed +interface provenance; `LeanCert.Core` is reached through `LeanCert.ANT` or +`LeanCert.Validity.AffineCover`, while the parent `LeanCert.Validity` namespace +is attributed to the latter. The checker rejects a namespace absent from this +reviewed provenance table. This prevents the fixture from claiming semantic +name resolution it has not performed while still making every source-level +dependency site and imported role explicit. The 107 qualified-reference +occurrences include namespace opens; they are not 107 distinct declaration +dependencies. A migration may classify a finite natural-number `interval_auto` call as ordinary arithmetic automation rather than route it through the real interval engine. A direct certified-bound dependency may remain outside the interval migration or be @@ -1138,8 +1204,11 @@ claim unless a later workload explicitly selects them. records a false target exposed numerically. Failure diagnostics must report the incompatible enclosure rather than only request more precision. - PNT+ PR [#1405](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/1405) - records manual treatment of `exp (-log N / k)` and a theorem containing - roughly 135 interval checks. It also records four false original boundary + records manual treatment of `exp (-log N / k)` and describes the Table 12 + batch as roughly 135 checks. At the pinned source, this audit counts 24 + ordinary rows and two logarithmic rows, each expanded across five columns, + for exactly 130 checks. The PR also + records four false original boundary rows, at `b = log(5e10)`, `25`, `log(3.2e13)`, and `32`; at least one original row remains an expected-failure regression. These cases motivate certified normalization, batch replay, and useful failure bounds. @@ -1414,8 +1483,10 @@ The committed compatibility subset is `D8` unless marked `D9`: - representative `10^-20` and `10^-100` tail bounds; - BKLNW sums with upper limits 29, 37, 63, 145, 289, and 433; - `[D9]` one Table 10 shard and the recorded false target as an expected - failure; -- `[D9]` the approximately 135-case Table 12 batch, plus one of its four false + failure. The shard fixture must bind the intended paper row/column + coordinates and generated theorem family, not merely replay 87 target and 38 + supporting source-level tactic sites; +- `[D9]` the 130-case Table 12 batch, plus one of its four false original boundary rows as an expected failure; - `[D9]` a small deterministic FKS2 sample in per-PR `core`, a measured medium shard in per-PR `ci`, and all 13,590 cells in the `local`/release profile; diff --git a/conformance-fixtures/HexIntervalMathlib/pnt-inventory.jsonl b/conformance-fixtures/HexIntervalMathlib/pnt-inventory.jsonl new file mode 100644 index 000000000..fc1f30faf --- /dev/null +++ b/conformance-fixtures/HexIntervalMathlib/pnt-inventory.jsonl @@ -0,0 +1,568 @@ +{"audit_record_digest":"6cfed911ea5dc11a114be8cadad83aaf1a68972a166700ceea894a7145e2d07d","counts":{"bklnw_table10_a2_sites":38,"bklnw_table10_target_sites":87,"bklnw_table12_checks":130,"bklnw_table12_logarithmic_rows":2,"bklnw_table12_ordinary_rows":24,"dependency_interface":6,"fks2_cells":13590,"fks2_shards":14,"interval_auto_actual":60,"interval_auto_textual":61,"interval_decide_actual":280,"interval_decide_textual":290,"leancert_import":16,"leancert_reference":107,"native_decide_actual":83,"records":567},"format":1,"kind":"meta","lean_source_digest":"84b1cdfe1cae7b6ddc181aede13c35b276422a206f6815143c2a1c50c3c0b112","lean_source_files":232,"pins":{"lean_toolchain":"leanprover/lean4:v4.32.2","leancert":"58edbea59458e9b010262238eaca27b6e0240dae","mathlib":"905b95818eb32af7874a58b427f50c1711a5e96c","pnt":"21998bb6196b56789f72a52656a781a75e134eb0"},"record_digest":"a86c79de333d3cae4f6818e4d2401ca646da81b2243b3dbc13676284ae953ba9"} +{"import_sites":[{"line":2,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.lean"}],"kind":"dependency-interface","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.ANT","role":"whole-interval ANT expression checker used by the extended FKS2 table","workload":"fks2-table4ext"} +{"import_sites":[{"line":7,"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean"}],"kind":"dependency-interface","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.CertifiedBounds.BKLNW","role":"certified exponential and power bounds used by the BKLNW sums","workload":"bklnw-certified-bounds"} +{"import_sites":[{"line":9,"path":"PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean"},{"line":3,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean"},{"line":2,"path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean"}],"kind":"dependency-interface","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.CertifiedBounds.Chebyshev","role":"certified Chebyshev bounds used by Chebyshev, FKS2 floor, and Ramanujan proofs","workload":"chebyshev-certified-bounds"} +{"import_sites":[{"line":2,"path":"PrimeNumberTheoremAnd/IEANTN/Li2Bounds.lean"}],"kind":"dependency-interface","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.CertifiedBounds.Li2","role":"Li(2) integrand, positivity, boundedness, value, and integral bounds","workload":"li2-certified-bounds"} +{"import_sites":[{"line":6,"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean"},{"line":1,"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"line":4,"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean"},{"line":10,"path":"PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean"},{"line":6,"path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean"},{"line":5,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean"},{"line":9,"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean"},{"line":2,"path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean"},{"line":8,"path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean"}],"kind":"dependency-interface","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.Tactic.IntervalAuto","role":"interval_decide and interval_auto tactic entry points","workload":"interval-tactics"} +{"import_sites":[{"line":4,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean"}],"kind":"dependency-interface","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.Validity.AffineCover","role":"affine-cover certificate used by the small-x FKS2 floor","workload":"affine-cover"} +{"actual_interval_decide":128,"declarations":[{"declaration":"row21_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row22_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row23_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row24_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row26_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row27_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row28_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row29_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row30_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row31_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row32_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row33_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row34_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row35_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row36_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row37_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row38_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row39_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row40_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row41_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row42_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row43_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"table_10_row43_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"table_10_row43_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"table_10_row43_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"table_10_row43_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"table_10_row43_k5","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row44_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row45_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row46_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row47_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row48_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row49_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row50_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row51_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row52_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row53_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row54_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row55_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row56_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row57_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row58_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row59_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"table_10_row65_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row65_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row65_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row65_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row65_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row70_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row70_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row70_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row70_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row70_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row75_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row75_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row75_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row75_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row75_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row80_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row80_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row80_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row80_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row80_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row85_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row85_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row85_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row85_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row85_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row90_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row90_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row90_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row90_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row90_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row95_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row95_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row95_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row95_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row95_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row19log10_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row19log10_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row19log10_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row19log10_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row19log10_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row60_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row60_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row60_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row60_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row60_k5","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row60_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row13800_7464_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_12600_24000.lean"},{"declaration":"table_10_row13800_7464_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_12600_24000.lean"},{"declaration":"table_10_row13800_7464_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_12600_24000.lean"},{"declaration":"table_10_row13800_7464_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_12600_24000.lean"},{"declaration":"table_10_row13800_7464_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_12600_24000.lean"},{"declaration":"table_12_check","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_tables.lean"}],"family":"bklnw-all-source-checks","kind":"generated-family","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"source":"PrimeNumberTheoremAnd/IEANTN/BKLNW/*.lean"} +{"declarations":[{"declaration":"row21_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row22_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row23_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row24_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row26_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row27_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row28_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row29_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row30_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row31_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row32_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row33_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row34_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row35_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row36_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row37_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row38_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row39_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row40_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row41_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row42_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row43_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"table_10_row43_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"table_10_row43_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"table_10_row43_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"table_10_row43_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"table_10_row43_k5","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean"},{"declaration":"row44_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row45_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row46_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row47_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row48_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row49_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row50_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row51_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row52_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row53_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row54_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row55_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row56_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row57_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row58_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"row59_a2_le","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean"},{"declaration":"table_10_row65_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row65_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row65_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row65_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row65_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row70_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row70_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row70_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row70_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row70_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row75_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row75_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row75_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row75_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row75_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row80_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row80_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row80_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row80_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row80_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row85_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row85_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row85_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row85_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row85_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"},{"declaration":"table_10_row90_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row90_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row90_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row90_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row90_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row95_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row95_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row95_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row95_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row95_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean"},{"declaration":"table_10_row19log10_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row19log10_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row19log10_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row19log10_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row19log10_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row60_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row60_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row60_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row60_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row60_k5","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row60_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean"},{"declaration":"table_10_row13800_7464_k1_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_12600_24000.lean"},{"declaration":"table_10_row13800_7464_k2_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_12600_24000.lean"},{"declaration":"table_10_row13800_7464_k3_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_12600_24000.lean"},{"declaration":"table_10_row13800_7464_k4_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_12600_24000.lean"},{"declaration":"table_10_row13800_7464_k5_margin","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_12600_24000.lean"}],"family":"bklnw-table10-source-sites","kind":"generated-family","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"source":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows*.lean","supporting_a2_check_sites":38,"target_check_sites":87} +{"annotation_provenance":"pinned BKLNW_tables.lean row count plus reviewed five-column expansion; false rows from PNT+ PR #1405","check_declaration":"table_12_check","checks_per_row":5,"expanded_checks":130,"false_original_boundary_rows":["log(5e10)","25","log(3.2e13)","32"],"family":"bklnw-table12-cells","kind":"generated-family","logarithmic_rows":2,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"ordinary_rows":24,"rows":26,"source":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_tables.lean"} +{"cells":13590,"family":"fks2-table4ext","kind":"generated-family","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"shards":[{"cells":1000,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.lean"},{"cells":1000,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.lean"},{"cells":1000,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.lean"},{"cells":1000,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.lean"},{"cells":1000,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.lean"},{"cells":1000,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.lean"},{"cells":1000,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.lean"},{"cells":1000,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.lean"},{"cells":1000,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.lean"},{"cells":1000,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.lean"},{"cells":1000,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.lean"},{"cells":1000,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.lean"},{"cells":1000,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.lean"},{"cells":590,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.lean"}],"source":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_*.lean"} +{"kind":"leancert-import","line":6,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.Tactic.IntervalAuto","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean"} +{"kind":"leancert-import","line":7,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.CertifiedBounds.BKLNW","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean"} +{"kind":"leancert-import","line":1,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.Tactic.IntervalAuto","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean"} +{"kind":"leancert-import","line":4,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.Tactic.IntervalAuto","path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean"} +{"kind":"leancert-import","line":9,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.CertifiedBounds.Chebyshev","path":"PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean"} +{"kind":"leancert-import","line":10,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.Tactic.IntervalAuto","path":"PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean"} +{"kind":"leancert-import","line":6,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.Tactic.IntervalAuto","path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean"} +{"kind":"leancert-import","line":3,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.CertifiedBounds.Chebyshev","path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean"} +{"kind":"leancert-import","line":4,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.Validity.AffineCover","path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean"} +{"kind":"leancert-import","line":5,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.Tactic.IntervalAuto","path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean"} +{"kind":"leancert-import","line":2,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.ANT","path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.lean"} +{"kind":"leancert-import","line":2,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.CertifiedBounds.Li2","path":"PrimeNumberTheoremAnd/IEANTN/Li2Bounds.lean"} +{"kind":"leancert-import","line":9,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.Tactic.IntervalAuto","path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean"} +{"kind":"leancert-import","line":2,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.CertifiedBounds.Chebyshev","path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean"} +{"kind":"leancert-import","line":2,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.Tactic.IntervalAuto","path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean"} +{"kind":"leancert-import","line":8,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.Tactic.IntervalAuto","path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean"} +{"column":15,"declaration":"f_eq_leancert_f","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":25,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.f"} +{"column":5,"declaration":"a2_20_exp_lower","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":46,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_20_exp_lower"} +{"column":5,"declaration":"a2_20_exp_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":52,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_20_exp_upper"} +{"column":9,"declaration":"cert_pow29_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":58,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.pow29_upper"} +{"column":5,"declaration":"a2_25_exp_lower","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":97,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_25_exp_lower"} +{"column":5,"declaration":"a2_25_exp_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":103,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_25_exp_upper"} +{"column":9,"declaration":"cert_pow37_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":109,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.pow37_upper"} +{"column":5,"declaration":"a2_30_exp_lower","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":148,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_30_exp_lower"} +{"column":5,"declaration":"a2_30_exp_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":154,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_30_exp_upper"} +{"column":9,"declaration":"cert_pow44_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":160,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.pow44_upper"} +{"column":5,"declaration":"a2_35_exp_lower","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":199,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_35_exp_lower"} +{"column":5,"declaration":"a2_35_exp_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":205,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_35_exp_upper"} +{"column":9,"declaration":"cert_pow51_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":211,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.pow51_upper"} +{"column":5,"declaration":"a2_40_exp_lower","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":250,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_40_exp_lower"} +{"column":5,"declaration":"a2_40_exp_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":256,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_40_exp_upper"} +{"column":9,"declaration":"cert_pow58_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":262,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.pow58_upper"} +{"column":5,"declaration":"a2_43_exp_lower","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":301,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_43_exp_lower"} +{"column":5,"declaration":"a2_43_exp_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":307,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_43_exp_upper"} +{"column":9,"declaration":"cert_pow63_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":313,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.pow63_upper"} +{"column":5,"declaration":"a2_100_exp_lower","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":352,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_100_exp_lower"} +{"column":5,"declaration":"a2_100_exp_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":358,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_100_exp_upper"} +{"column":9,"declaration":"cert_pow145_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":364,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.pow145_upper"} +{"column":5,"declaration":"a2_150_exp_lower","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":402,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_150_exp_lower"} +{"column":5,"declaration":"a2_150_exp_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":408,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_150_exp_upper"} +{"column":9,"declaration":"cert_pow217_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":414,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.pow217_upper"} +{"column":5,"declaration":"a2_200_exp_lower","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":452,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_200_exp_lower"} +{"column":5,"declaration":"a2_200_exp_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":458,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_200_exp_upper"} +{"column":9,"declaration":"cert_pow289_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":464,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.pow289_upper"} +{"column":5,"declaration":"a2_250_exp_lower","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":502,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_250_exp_lower"} +{"column":5,"declaration":"a2_250_exp_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":508,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_250_exp_upper"} +{"column":9,"declaration":"cert_pow361_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":514,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.pow361_upper"} +{"column":5,"declaration":"a2_300_exp_lower","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":552,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_300_exp_lower"} +{"column":5,"declaration":"a2_300_exp_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":558,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.a2_300_exp_upper"} +{"column":15,"declaration":"cert_pow433_upper","interface_provenance":["LeanCert.CertifiedBounds.BKLNW"],"kind":"leancert-reference","line":565,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","symbol":"LeanCert.CertifiedBounds.BKLNW.pow433_upper"} +{"column":6,"declaration":"psi_upper","interface_provenance":["LeanCert.CertifiedBounds.Chebyshev"],"kind":"leancert-reference","line":581,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean","symbol":"LeanCert.CertifiedBounds.Chebyshev"} +{"column":8,"declaration":"psi_num_2","interface_provenance":["LeanCert.CertifiedBounds.Chebyshev"],"kind":"leancert-reference","line":595,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean","symbol":"LeanCert.CertifiedBounds.Chebyshev"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":29,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":29,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":19,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row1.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":19,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row1.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":22,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row2.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":22,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row2.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":18,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row3.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":18,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row3.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":17,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row4.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":17,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row4.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":17,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row6.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":17,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row6.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":13,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row7.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":13,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row7.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":27,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row8.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":27,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row8.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":20,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row9.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":20,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row9.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":18,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":18,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":19,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row1.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":19,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row1.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":27,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row10.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":27,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row10.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":11,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":41,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean","symbol":"LeanCert.Core"} +{"column":25,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":41,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":"mid_xpow_of","interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":363,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":"mid_xpow_of","interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":363,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":21,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row2.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":21,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row2.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":29,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row3.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":29,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row3.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":11,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":37,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row4.lean","symbol":"LeanCert.Core"} +{"column":25,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":37,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row4.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":"floor_xhalf_of_check","interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":180,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row4.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":"floor_xhalf_of_check","interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":180,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row4.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":16,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row5.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":16,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row5.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":27,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row6.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":27,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row6.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":27,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row7.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":27,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row7.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":27,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row8.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":27,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row8.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":21,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":27,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row9.lean","symbol":"LeanCert.Core"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":27,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row9.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":6,"declaration":null,"interface_provenance":["LeanCert.CertifiedBounds.Chebyshev"],"kind":"leancert-reference","line":7,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","symbol":"LeanCert.CertifiedBounds.Chebyshev"} +{"column":35,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":8,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","symbol":"LeanCert.Core"} +{"column":49,"declaration":null,"interface_provenance":["LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":8,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","symbol":"LeanCert.Validity"} +{"column":6,"declaration":"integral_etheta_bound","interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":92,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","symbol":"LeanCert.Core"} +{"column":20,"declaration":"integral_etheta_bound","interface_provenance":["LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":92,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","symbol":"LeanCert.Validity"} +{"column":6,"declaration":"fExpr","interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":97,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","symbol":"LeanCert.Core"} +{"column":6,"declaration":"cbps","interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":105,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","symbol":"LeanCert.Core"} +{"column":20,"declaration":"cbps","interface_provenance":["LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":105,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","symbol":"LeanCert.Validity"} +{"column":11,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":30,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.lean","symbol":"LeanCert.Core"} +{"column":25,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":30,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":11,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":30,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtGenCore.lean","symbol":"LeanCert.Core"} +{"column":25,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":30,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtGenCore.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":11,"declaration":null,"interface_provenance":["LeanCert.ANT","LeanCert.Validity.AffineCover"],"kind":"leancert-reference","line":21,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtGenQuarterCore.lean","symbol":"LeanCert.Core"} +{"column":25,"declaration":null,"interface_provenance":["LeanCert.ANT"],"kind":"leancert-reference","line":21,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtGenQuarterCore.lean","symbol":"LeanCert.ANT.Asymp"} +{"column":36,"declaration":"g","interface_provenance":["LeanCert.CertifiedBounds.Li2"],"kind":"leancert-reference","line":44,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/Li2Bounds.lean","symbol":"LeanCert.CertifiedBounds.Li2.integrand"} +{"column":21,"declaration":"li2_symmetric_eq_Li2_li2","interface_provenance":["LeanCert.CertifiedBounds.Li2"],"kind":"leancert-reference","line":52,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/Li2Bounds.lean","symbol":"LeanCert.CertifiedBounds.Li2.value"} +{"column":7,"declaration":"g_intervalIntegrable_full","interface_provenance":["LeanCert.CertifiedBounds.Li2"],"kind":"leancert-reference","line":95,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/Li2Bounds.lean","symbol":"LeanCert.CertifiedBounds.Li2.integrand_pos"} +{"column":7,"declaration":"g_intervalIntegrable_full","interface_provenance":["LeanCert.CertifiedBounds.Li2"],"kind":"leancert-reference","line":97,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/Li2Bounds.lean","symbol":"LeanCert.CertifiedBounds.Li2.integrand_le_two"} +{"column":9,"declaration":"li2_symmetric_lower","interface_provenance":["LeanCert.CertifiedBounds.Li2"],"kind":"leancert-reference","line":116,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/Li2Bounds.lean","symbol":"LeanCert.CertifiedBounds.Li2.lower"} +{"column":9,"declaration":"li2_symmetric_upper","interface_provenance":["LeanCert.CertifiedBounds.Li2"],"kind":"leancert-reference","line":126,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/Li2Bounds.lean","symbol":"LeanCert.CertifiedBounds.Li2.upper"} +{"column":6,"declaration":"criterion","interface_provenance":["LeanCert.CertifiedBounds.Chebyshev"],"kind":"leancert-reference","line":498,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","symbol":"LeanCert.CertifiedBounds.Chebyshev"} +{"column":6,"declaration":"allThetaChecks_3_599","interface_provenance":["LeanCert.CertifiedBounds.Chebyshev"],"kind":"leancert-reference","line":503,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","symbol":"LeanCert.CertifiedBounds.Chebyshev"} +{"column":7,"declaration":"pi_bound_1","interface_provenance":["LeanCert.CertifiedBounds.Chebyshev"],"kind":"leancert-reference","line":541,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","symbol":"LeanCert.CertifiedBounds.Chebyshev.checkAllThetaRelErrorReal_implies"} +{"column":7,"declaration":"pi_bound_1","interface_provenance":["LeanCert.CertifiedBounds.Chebyshev"],"kind":"leancert-reference","line":548,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","symbol":"LeanCert.CertifiedBounds.Chebyshev.abs_theta_sub_le_mul_of_checkThetaRelErrorReal"} +{"column":7,"declaration":"pi_bound_2","interface_provenance":["LeanCert.CertifiedBounds.Chebyshev"],"kind":"leancert-reference","line":658,"migration":{"note":"lexical audit evidence subsumed by imported-interface classification","status":"inventory-only"},"path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","symbol":"LeanCert.CertifiedBounds.Chebyshev.abs_theta_sub_le_mul_of_checkThetaRelErrorReal"} +{"column":6,"declaration":"allChecks_11723","kind":"native-decide-occurrence","line":586,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean"} +{"column":3,"declaration":"allCells_checked_row5","kind":"native-decide-occurrence","line":76,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23.lean"} +{"column":3,"declaration":"slabs_checked","kind":"native-decide-occurrence","line":331,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23.lean"} +{"column":3,"declaration":"allCells_checked_row1_hi40","kind":"native-decide-occurrence","line":181,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row1.lean"} +{"column":3,"declaration":"slabs_checked1","kind":"native-decide-occurrence","line":219,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row1.lean"} +{"column":3,"declaration":"allCells_checked_row2","kind":"native-decide-occurrence","line":188,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row2.lean"} +{"column":3,"declaration":"slabs_checked2","kind":"native-decide-occurrence","line":212,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row2.lean"} +{"column":3,"declaration":"allCells_checked_row3","kind":"native-decide-occurrence","line":27,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row3.lean"} +{"column":3,"declaration":"slabs_checked3","kind":"native-decide-occurrence","line":161,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row3.lean"} +{"column":3,"declaration":"allCells_checked_row4","kind":"native-decide-occurrence","line":27,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row4.lean"} +{"column":3,"declaration":"slabs_checked4","kind":"native-decide-occurrence","line":192,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row4.lean"} +{"column":3,"declaration":"allCells_checked_row6","kind":"native-decide-occurrence","line":26,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row6.lean"} +{"column":3,"declaration":"slabs_checked6","kind":"native-decide-occurrence","line":84,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row6.lean"} +{"column":3,"declaration":"allCells_checked_row7","kind":"native-decide-occurrence","line":22,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row7.lean"} +{"column":3,"declaration":"slabs_checked7","kind":"native-decide-occurrence","line":80,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row7.lean"} +{"column":3,"declaration":"r8_sides","kind":"native-decide-occurrence","line":39,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row8.lean"} +{"column":3,"declaration":"slabs_checked8","kind":"native-decide-occurrence","line":139,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row8.lean"} +{"column":3,"declaration":"allCells_checked_row9","kind":"native-decide-occurrence","line":83,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row9.lean"} +{"column":3,"declaration":"slabs_checked9","kind":"native-decide-occurrence","line":118,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row9.lean"} +{"column":45,"declaration":"floor_slab_check_row1","kind":"native-decide-occurrence","line":40,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row1.lean"} +{"column":77,"declaration":"midCells_chain_row10","kind":"native-decide-occurrence","line":36,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row10.lean"} +{"column":63,"declaration":"midCells_ne_nil_row10","kind":"native-decide-occurrence","line":38,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row10.lean"} +{"column":74,"declaration":"midCells_last_row10","kind":"native-decide-occurrence","line":40,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row10.lean"} +{"column":73,"declaration":"allCells_take_checkXpow_row10","kind":"native-decide-occurrence","line":46,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row10.lean"} +{"column":3,"declaration":"boundaryCell_fails_row10","kind":"native-decide-occurrence","line":52,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row10.lean"} +{"column":45,"declaration":"floor_slab_check_row10","kind":"native-decide-occurrence","line":71,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row10.lean"} +{"column":65,"declaration":"sampleCells_checkXpow","kind":"native-decide-occurrence","line":187,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean"} +{"column":3,"declaration":"boundaryCell_fails","kind":"native-decide-occurrence","line":193,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean"} +{"column":71,"declaration":"midCells_chain","kind":"native-decide-occurrence","line":383,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean"} +{"column":57,"declaration":"midCells_ne_nil","kind":"native-decide-occurrence","line":385,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean"} +{"column":68,"declaration":"midCells_last","kind":"native-decide-occurrence","line":387,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean"} +{"column":74,"declaration":"allCells_take_checkXpow","kind":"native-decide-occurrence","line":393,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean"} +{"column":53,"declaration":"floor_slab_check","kind":"native-decide-occurrence","line":411,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean"} +{"column":53,"declaration":"floor_slab_check_row2","kind":"native-decide-occurrence","line":41,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row2.lean"} +{"column":45,"declaration":"floor_slab_check_row3","kind":"native-decide-occurrence","line":51,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row3.lean"} +{"column":53,"declaration":"floor_slab_check_row4","kind":"native-decide-occurrence","line":200,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row4.lean"} +{"column":53,"declaration":"floor_slab_check_row5","kind":"native-decide-occurrence","line":37,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row5.lean"} +{"column":74,"declaration":"midCells_chain_row6","kind":"native-decide-occurrence","line":36,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row6.lean"} +{"column":60,"declaration":"midCells_ne_nil_row6","kind":"native-decide-occurrence","line":38,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row6.lean"} +{"column":69,"declaration":"midCells_last_row6","kind":"native-decide-occurrence","line":40,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row6.lean"} +{"column":70,"declaration":"allCells_take_checkXpow_row6","kind":"native-decide-occurrence","line":46,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row6.lean"} +{"column":3,"declaration":"boundaryCell_fails_row6","kind":"native-decide-occurrence","line":52,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row6.lean"} +{"column":52,"declaration":"floor_slab_check_row6","kind":"native-decide-occurrence","line":71,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row6.lean"} +{"column":74,"declaration":"midCells_chain_row7","kind":"native-decide-occurrence","line":36,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row7.lean"} +{"column":60,"declaration":"midCells_ne_nil_row7","kind":"native-decide-occurrence","line":38,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row7.lean"} +{"column":70,"declaration":"midCells_last_row7","kind":"native-decide-occurrence","line":40,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row7.lean"} +{"column":70,"declaration":"allCells_take_checkXpow_row7","kind":"native-decide-occurrence","line":46,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row7.lean"} +{"column":3,"declaration":"boundaryCell_fails_row7","kind":"native-decide-occurrence","line":52,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row7.lean"} +{"column":53,"declaration":"floor_slab_check_row7","kind":"native-decide-occurrence","line":71,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row7.lean"} +{"column":75,"declaration":"midCells_chain_row8","kind":"native-decide-occurrence","line":36,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row8.lean"} +{"column":61,"declaration":"midCells_ne_nil_row8","kind":"native-decide-occurrence","line":38,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row8.lean"} +{"column":71,"declaration":"midCells_last_row8","kind":"native-decide-occurrence","line":40,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row8.lean"} +{"column":71,"declaration":"allCells_take_checkXpow_row8","kind":"native-decide-occurrence","line":46,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row8.lean"} +{"column":3,"declaration":"boundaryCell_fails_row8","kind":"native-decide-occurrence","line":52,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row8.lean"} +{"column":53,"declaration":"floor_slab_check_row8","kind":"native-decide-occurrence","line":71,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row8.lean"} +{"column":75,"declaration":"midCells_chain_row9","kind":"native-decide-occurrence","line":36,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row9.lean"} +{"column":61,"declaration":"midCells_ne_nil_row9","kind":"native-decide-occurrence","line":38,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row9.lean"} +{"column":71,"declaration":"midCells_last_row9","kind":"native-decide-occurrence","line":40,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row9.lean"} +{"column":72,"declaration":"allCells_take_checkXpow_row9","kind":"native-decide-occurrence","line":46,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row9.lean"} +{"column":3,"declaration":"boundaryCell_fails_row9","kind":"native-decide-occurrence","line":52,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row9.lean"} +{"column":45,"declaration":"floor_slab_check_row9","kind":"native-decide-occurrence","line":71,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row9.lean"} +{"column":73,"declaration":"etheta_le_floor","kind":"native-decide-occurrence","line":19,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean"} +{"column":38,"declaration":"cover_cmp","kind":"native-decide-occurrence","line":110,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean"} +{"column":61,"declaration":"linear_le_curve","kind":"native-decide-occurrence","line":123,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean"} +{"column":59,"declaration":"allCells_chain","kind":"native-decide-occurrence","line":99,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean"} +{"column":57,"declaration":"allCells_last","kind":"native-decide-occurrence","line":102,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean"} +{"column":47,"declaration":"allCells_ne_nil","kind":"native-decide-occurrence","line":104,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean"} +{"column":41,"declaration":"cells_00_checked","kind":"native-decide-occurrence","line":1016,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.lean"} +{"column":41,"declaration":"cells_01_checked","kind":"native-decide-occurrence","line":1016,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.lean"} +{"column":41,"declaration":"cells_02_checked","kind":"native-decide-occurrence","line":1016,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.lean"} +{"column":41,"declaration":"cells_03_checked","kind":"native-decide-occurrence","line":1016,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.lean"} +{"column":41,"declaration":"cells_04_checked","kind":"native-decide-occurrence","line":1016,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.lean"} +{"column":41,"declaration":"cells_05_checked","kind":"native-decide-occurrence","line":1016,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.lean"} +{"column":41,"declaration":"cells_06_checked","kind":"native-decide-occurrence","line":1016,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.lean"} +{"column":41,"declaration":"cells_07_checked","kind":"native-decide-occurrence","line":1016,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.lean"} +{"column":41,"declaration":"cells_08_checked","kind":"native-decide-occurrence","line":1016,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.lean"} +{"column":41,"declaration":"cells_09_checked","kind":"native-decide-occurrence","line":1016,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.lean"} +{"column":41,"declaration":"cells_10_checked","kind":"native-decide-occurrence","line":1016,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.lean"} +{"column":41,"declaration":"cells_11_checked","kind":"native-decide-occurrence","line":1016,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.lean"} +{"column":41,"declaration":"cells_12_checked","kind":"native-decide-occurrence","line":1016,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.lean"} +{"column":41,"declaration":"cells_13_checked","kind":"native-decide-occurrence","line":606,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.lean"} +{"column":66,"declaration":"allThetaChecks_3_599","kind":"native-decide-occurrence","line":500,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean"} +{"column":60,"declaration":"thetaCheck599","kind":"native-decide-occurrence","line":505,"mechanism":"native_decide","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean"} +{"actual":false,"column":4,"declaration":null,"kind":"tactic-occurrence","line":19,"migration":{"status":"not-a-call"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean","snippet":"- `interval_decide` tactic from LeanCert","tactic":"interval_decide"} +{"actual":false,"column":2,"declaration":null,"kind":"tactic-occurrence","line":46,"migration":{"status":"not-a-call"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"`interval_decide` calls. -/","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row26_a2_le","kind":"tactic-occurrence","line":136,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row27_a2_le","kind":"tactic-occurrence","line":199,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row28_a2_le","kind":"tactic-occurrence","line":228,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row29_a2_le","kind":"tactic-occurrence","line":257,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row21_a2_le","kind":"tactic-occurrence","line":432,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row22_a2_le","kind":"tactic-occurrence","line":455,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row23_a2_le","kind":"tactic-occurrence","line":478,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row24_a2_le","kind":"tactic-occurrence","line":501,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row30_a2_le","kind":"tactic-occurrence","line":524,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row31_a2_le","kind":"tactic-occurrence","line":547,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row32_a2_le","kind":"tactic-occurrence","line":570,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row33_a2_le","kind":"tactic-occurrence","line":593,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row34_a2_le","kind":"tactic-occurrence","line":616,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row35_a2_le","kind":"tactic-occurrence","line":639,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row36_a2_le","kind":"tactic-occurrence","line":662,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row37_a2_le","kind":"tactic-occurrence","line":685,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row38_a2_le","kind":"tactic-occurrence","line":708,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row39_a2_le","kind":"tactic-occurrence","line":731,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row40_a2_le","kind":"tactic-occurrence","line":754,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row41_a2_le","kind":"tactic-occurrence","line":777,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row42_a2_le","kind":"tactic-occurrence","line":800,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row43_a2_le","kind":"tactic-occurrence","line":1095,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":35,"declaration":"table_10_row43_k5","kind":"tactic-occurrence","line":1265,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"(by unfold Gp expT; norm_num; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row43_k1_margin","kind":"tactic-occurrence","line":1388,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"(by unfold G1 eT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row43_k2_margin","kind":"tactic-occurrence","line":1396,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row43_k3_margin","kind":"tactic-occurrence","line":1404,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row43_k4_margin","kind":"tactic-occurrence","line":1412,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_20_43.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row44_a2_le","kind":"tactic-occurrence","line":118,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row45_a2_le","kind":"tactic-occurrence","line":141,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row46_a2_le","kind":"tactic-occurrence","line":164,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row47_a2_le","kind":"tactic-occurrence","line":187,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row48_a2_le","kind":"tactic-occurrence","line":210,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row49_a2_le","kind":"tactic-occurrence","line":233,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row50_a2_le","kind":"tactic-occurrence","line":256,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row51_a2_le","kind":"tactic-occurrence","line":279,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row52_a2_le","kind":"tactic-occurrence","line":302,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row53_a2_le","kind":"tactic-occurrence","line":325,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row54_a2_le","kind":"tactic-occurrence","line":348,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row55_a2_le","kind":"tactic-occurrence","line":371,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row56_a2_le","kind":"tactic-occurrence","line":394,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row57_a2_le","kind":"tactic-occurrence","line":417,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row58_a2_le","kind":"tactic-occurrence","line":440,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"row59_a2_le","kind":"tactic-occurrence","line":463,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_44_59.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row65_k1_margin","kind":"tactic-occurrence","line":39,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold G1 eT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row65_k1_margin","kind":"tactic-occurrence","line":40,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold G1 eT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row65_k2_margin","kind":"tactic-occurrence","line":47,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row65_k2_margin","kind":"tactic-occurrence","line":48,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row65_k3_margin","kind":"tactic-occurrence","line":55,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row65_k3_margin","kind":"tactic-occurrence","line":56,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row65_k4_margin","kind":"tactic-occurrence","line":63,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row65_k4_margin","kind":"tactic-occurrence","line":64,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":79,"declaration":"table_10_row65_k5_margin","kind":"tactic-occurrence","line":71,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Gp expT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":79,"declaration":"table_10_row65_k5_margin","kind":"tactic-occurrence","line":72,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Gp expT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row70_k1_margin","kind":"tactic-occurrence","line":97,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold G1 eT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row70_k1_margin","kind":"tactic-occurrence","line":98,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold G1 eT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row70_k2_margin","kind":"tactic-occurrence","line":105,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row70_k2_margin","kind":"tactic-occurrence","line":106,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row70_k3_margin","kind":"tactic-occurrence","line":113,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row70_k3_margin","kind":"tactic-occurrence","line":114,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row70_k4_margin","kind":"tactic-occurrence","line":121,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row70_k4_margin","kind":"tactic-occurrence","line":122,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":79,"declaration":"table_10_row70_k5_margin","kind":"tactic-occurrence","line":129,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Gp expT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":79,"declaration":"table_10_row70_k5_margin","kind":"tactic-occurrence","line":130,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Gp expT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row75_k1_margin","kind":"tactic-occurrence","line":155,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold G1 eT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row75_k1_margin","kind":"tactic-occurrence","line":156,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold G1 eT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row75_k2_margin","kind":"tactic-occurrence","line":163,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row75_k2_margin","kind":"tactic-occurrence","line":164,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row75_k3_margin","kind":"tactic-occurrence","line":171,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row75_k3_margin","kind":"tactic-occurrence","line":172,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row75_k4_margin","kind":"tactic-occurrence","line":179,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row75_k4_margin","kind":"tactic-occurrence","line":180,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":79,"declaration":"table_10_row75_k5_margin","kind":"tactic-occurrence","line":187,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Gp expT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":79,"declaration":"table_10_row75_k5_margin","kind":"tactic-occurrence","line":188,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Gp expT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row80_k1_margin","kind":"tactic-occurrence","line":213,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold G1 eT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row80_k1_margin","kind":"tactic-occurrence","line":214,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold G1 eT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row80_k2_margin","kind":"tactic-occurrence","line":221,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row80_k2_margin","kind":"tactic-occurrence","line":222,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row80_k3_margin","kind":"tactic-occurrence","line":229,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row80_k3_margin","kind":"tactic-occurrence","line":230,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row80_k4_margin","kind":"tactic-occurrence","line":237,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row80_k4_margin","kind":"tactic-occurrence","line":238,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":79,"declaration":"table_10_row80_k5_margin","kind":"tactic-occurrence","line":245,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Gp expT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":79,"declaration":"table_10_row80_k5_margin","kind":"tactic-occurrence","line":246,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Gp expT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row85_k1_margin","kind":"tactic-occurrence","line":271,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold G1 eT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row85_k1_margin","kind":"tactic-occurrence","line":272,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold G1 eT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row85_k2_margin","kind":"tactic-occurrence","line":279,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row85_k2_margin","kind":"tactic-occurrence","line":280,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row85_k3_margin","kind":"tactic-occurrence","line":287,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row85_k3_margin","kind":"tactic-occurrence","line":288,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row85_k4_margin","kind":"tactic-occurrence","line":295,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row85_k4_margin","kind":"tactic-occurrence","line":296,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":79,"declaration":"table_10_row85_k5_margin","kind":"tactic-occurrence","line":303,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Gp expT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":79,"declaration":"table_10_row85_k5_margin","kind":"tactic-occurrence","line":304,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_65_85.lean","snippet":"(by unfold Gp expT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"table_10_row90_k1_margin","kind":"tactic-occurrence","line":71,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean","snippet":"(by norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"table_10_row90_k2_margin","kind":"tactic-occurrence","line":78,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean","snippet":"(by norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"table_10_row90_k3_margin","kind":"tactic-occurrence","line":85,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean","snippet":"(by norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"table_10_row90_k4_margin","kind":"tactic-occurrence","line":92,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean","snippet":"(by norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"table_10_row90_k5_margin","kind":"tactic-occurrence","line":99,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean","snippet":"(by norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"table_10_row95_k1_margin","kind":"tactic-occurrence","line":106,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean","snippet":"(by norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"table_10_row95_k2_margin","kind":"tactic-occurrence","line":113,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean","snippet":"(by norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"table_10_row95_k3_margin","kind":"tactic-occurrence","line":120,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean","snippet":"(by norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"table_10_row95_k4_margin","kind":"tactic-occurrence","line":127,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean","snippet":"(by norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"table_10_row95_k5_margin","kind":"tactic-occurrence","line":134,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_90_95.lean","snippet":"(by norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":false,"column":44,"declaration":null,"kind":"tactic-occurrence","line":703,"migration":{"status":"not-a-call"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean","snippet":"constant inequality, dischargeable by `interval_decide` per row. Ported from the","tactic":"interval_decide"} +{"actual":true,"column":35,"declaration":"table_10_row60_k5","kind":"tactic-occurrence","line":49,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold Gp expT; norm_num; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":35,"declaration":"table_10_row60_k5","kind":"tactic-occurrence","line":50,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold Gp expT; norm_num; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row60_k1_margin","kind":"tactic-occurrence","line":60,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold G1 eT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row60_k1_margin","kind":"tactic-occurrence","line":61,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold G1 eT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row60_k2_margin","kind":"tactic-occurrence","line":68,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row60_k2_margin","kind":"tactic-occurrence","line":69,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row60_k3_margin","kind":"tactic-occurrence","line":76,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row60_k3_margin","kind":"tactic-occurrence","line":77,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row60_k4_margin","kind":"tactic-occurrence","line":84,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row60_k4_margin","kind":"tactic-occurrence","line":85,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":79,"declaration":"table_10_row60_k5_margin","kind":"tactic-occurrence","line":92,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold Gp expT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":79,"declaration":"table_10_row60_k5_margin","kind":"tactic-occurrence","line":93,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold Gp expT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":79,"declaration":"table_10_row19log10_k5_margin","kind":"tactic-occurrence","line":191,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold Gp expT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row19log10_k1_margin","kind":"tactic-occurrence","line":300,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold G1 eT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row19log10_k2_margin","kind":"tactic-occurrence","line":308,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row19log10_k3_margin","kind":"tactic-occurrence","line":316,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":77,"declaration":"table_10_row19log10_k4_margin","kind":"tactic-occurrence","line":324,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_misc.lean","snippet":"(by unfold Pp pT; norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"table_10_row13800_7464_k1_margin","kind":"tactic-occurrence","line":812,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_12600_24000.lean","snippet":"(by norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"table_10_row13800_7464_k2_margin","kind":"tactic-occurrence","line":821,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_12600_24000.lean","snippet":"(by norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"table_10_row13800_7464_k3_margin","kind":"tactic-occurrence","line":830,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_12600_24000.lean","snippet":"(by norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"table_10_row13800_7464_k4_margin","kind":"tactic-occurrence","line":839,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_12600_24000.lean","snippet":"(by norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"table_10_row13800_7464_k5_margin","kind":"tactic-occurrence","line":848,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_12600_24000.lean","snippet":"(by norm_num [table_10_margin, BKLNW_app.table_8_margin]; interval_decide)","tactic":"interval_decide"} +{"actual":false,"column":32,"declaration":null,"kind":"tactic-occurrence","line":1295,"migration":{"status":"not-a-call"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_tables.lean","snippet":"-- `table_12_check` runs ~135 `interval_decide` numerical checks in a single","tactic":"interval_decide"} +{"actual":true,"column":72,"declaration":"table_12_check","kind":"tactic-occurrence","line":1313,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_tables.lean","snippet":"(refine \u27e8?_, ?_, ?_, ?_, ?_\u27e9 <;> (simp only [C_bk_S, RS_prime.c\u2080]; interval_decide; done))","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"table_12_check","kind":"tactic-occurrence","line":1319,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_tables.lean","snippet":"(by norm_num) (by simp only [C_bk_S, RS_prime.c\u2080]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"table_12_check","kind":"tactic-occurrence","line":1325,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_tables.lean","snippet":"(by norm_num) (by simp only [C_bk_S, RS_prime.c\u2080]; interval_decide)","tactic":"interval_decide"} +{"actual":true,"column":44,"declaration":"proposition_5_4a","kind":"tactic-occurrence","line":361,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","snippet":"have : exp (29 : \u211d) \u2264 (4e18 : \u211d) := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":56,"declaration":"proposition_5_4a","kind":"tactic-occurrence","line":406,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","snippet":"(lt_log_iff_exp_lt hx_pos).mpr (lt_of_lt_of_le (by interval_decide) hx)","tactic":"interval_decide"} +{"actual":true,"column":53,"declaration":"proposition_5_4b","kind":"tactic-occurrence","line":458,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","snippet":"have hexp : (370261 : \u211d) \u2264 exp (1283/100) := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":55,"declaration":"proposition_5_4b","kind":"tactic-occurrence","line":463,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","snippet":"have hexp : (492113 : \u211d) \u2264 exp (1312/100) := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":58,"declaration":"proposition_5_4b","kind":"tactic-occurrence","line":468,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","snippet":"have hexp : (2010733 : \u211d) \u2264 exp (1452/100) := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"proposition_5_4b","kind":"tactic-occurrence","line":473,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","snippet":"have hexp : (17051707 : \u211d) \u2264 exp (1666/100) := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":55,"declaration":"proposition_5_4b","kind":"tactic-occurrence","line":527,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","snippet":"\u00b7 have hexp43 : (4e18 : \u211d) \u2264 exp 43 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":67,"declaration":"proposition_5_4b","kind":"tactic-occurrence","line":532,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","snippet":"have hexp22_lb : (117352333 : \u211d) \u2264 exp 22 := by interval_decide","tactic":"interval_decide"} +{"actual":false,"column":28,"declaration":null,"kind":"tactic-occurrence","line":889,"migration":{"status":"not-a-call"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","snippet":"This can be discharged by `interval_decide`.","tactic":"interval_decide"} +{"actual":true,"column":64,"declaration":"theorem_6_2","kind":"tactic-occurrence","line":3605,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","snippet":"show (0 : \u211d) < log 14 + log (log 14) - 1 from by interval_decide]","tactic":"interval_decide"} +{"actual":true,"column":58,"declaration":"mu_asymp_num_le","kind":"tactic-occurrence","line":4274,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","snippet":"have hs_lo : (141.4213562 : \u211d) \u2264 Real.sqrt 20000 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"mu_asymp_num_le","kind":"tactic-occurrence","line":4282,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":58,"declaration":"mu_asymp_num_le_cor14","kind":"tactic-occurrence","line":24,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Cor14Tail.lean","snippet":"have hs_lo : (141.4213562 : \u211d) \u2264 Real.sqrt 20000 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":5,"declaration":"mu_asymp_num_le_cor14","kind":"tactic-occurrence","line":32,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Cor14Tail.lean","snippet":"interval_decide","tactic":"interval_decide"} +{"actual":true,"column":46,"declaration":"exp10_lt","kind":"tactic-occurrence","line":11,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","snippet":"theorem exp10_lt : Real.exp 10 < 22027 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":56,"declaration":"kadiri_lumley_odd_goldbach_finite","kind":"tactic-occurrence","line":250,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","snippet":"have : Real.exp 59 + 4 + 1 \u2264 11325 * 10 ^ 22 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":69,"declaration":"kadiri_lumley_odd_goldbach_finite","kind":"tactic-occurrence","line":267,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","snippet":"have : Real.exp 60 + 4 + 1 \u2264 7785131284000000000000000004 := by interval_decide","tactic":"interval_decide"} +{"actual":false,"column":37,"declaration":null,"kind":"tactic-occurrence","line":5,"migration":{"status":"not-a-call"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"Each bound is proved by LeanCert's `interval_decide` tactic (verified Taylor series).","tactic":"interval_decide"} +{"actual":true,"column":41,"declaration":"log_2_gt","kind":"tactic-occurrence","line":15,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_2_gt : 0.693147 < log 2 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":41,"declaration":"log_2_lt","kind":"tactic-occurrence","line":16,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_2_lt : log 2 < 0.693148 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":41,"declaration":"log_3_gt","kind":"tactic-occurrence","line":18,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_3_gt : 1.098612 < log 3 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":41,"declaration":"log_3_lt","kind":"tactic-occurrence","line":19,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_3_lt : log 3 < 1.098613 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":41,"declaration":"log_5_gt","kind":"tactic-occurrence","line":21,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_5_gt : 1.609437 < log 5 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":41,"declaration":"log_5_lt","kind":"tactic-occurrence","line":22,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_5_lt : log 5 < 1.609438 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":41,"declaration":"log_7_gt","kind":"tactic-occurrence","line":24,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_7_gt : 1.945910 < log 7 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":41,"declaration":"log_7_lt","kind":"tactic-occurrence","line":25,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_7_lt : log 7 < 1.945911 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_10_gt","kind":"tactic-occurrence","line":27,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_10_gt : 2.302585 < log 10 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_10_lt","kind":"tactic-occurrence","line":28,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_10_lt : log 10 < 2.302586 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_11_gt","kind":"tactic-occurrence","line":30,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_11_gt : 2.397895 < log 11 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_11_lt","kind":"tactic-occurrence","line":31,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_11_lt : log 11 < 2.397896 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_13_gt","kind":"tactic-occurrence","line":33,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_13_gt : 2.564949 < log 13 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_13_lt","kind":"tactic-occurrence","line":34,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_13_lt : log 13 < 2.564950 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_17_gt","kind":"tactic-occurrence","line":36,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_17_gt : 2.833213 < log 17 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_17_lt","kind":"tactic-occurrence","line":37,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_17_lt : log 17 < 2.833214 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_19_gt","kind":"tactic-occurrence","line":39,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_19_gt : 2.944438 < log 19 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_19_lt","kind":"tactic-occurrence","line":40,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_19_lt : log 19 < 2.944439 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_23_gt","kind":"tactic-occurrence","line":42,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_23_gt : 3.135494 < log 23 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_23_lt","kind":"tactic-occurrence","line":43,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_23_lt : log 23 < 3.135495 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_29_gt","kind":"tactic-occurrence","line":45,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_29_gt : 3.367295 < log 29 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_29_lt","kind":"tactic-occurrence","line":46,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_29_lt : log 29 < 3.367296 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_30_gt","kind":"tactic-occurrence","line":48,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_30_gt : 3.401197 < log 30 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_30_lt","kind":"tactic-occurrence","line":49,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_30_lt : log 30 < 3.401198 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_32_gt","kind":"tactic-occurrence","line":51,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_32_gt : 3.465735 < log 32 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":43,"declaration":"log_32_lt","kind":"tactic-occurrence","line":52,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_32_lt : log 32 < 3.465736 := by interval_decide","tactic":"interval_decide"} +{"actual":false,"column":62,"declaration":null,"kind":"tactic-occurrence","line":111,"migration":{"status":"not-a-call"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"bound on a tail term without paying the cost of an in-place `interval_decide`. -/","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"exp_neg_one_gt","kind":"tactic-occurrence","line":114,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_one_gt : (0.367879441 : \u211d) < exp (-1 : \u211d) := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_half_lt","kind":"tactic-occurrence","line":115,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_half_lt : exp (-(1/2 : \u211d)) < 0.6065307 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":65,"declaration":"exp_neg_two_thirds_lt","kind":"tactic-occurrence","line":116,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_two_thirds_lt : exp (-(2/3 : \u211d)) < 0.513418 := by interval_decide","tactic":"interval_decide"} +{"actual":false,"column":34,"declaration":null,"kind":"tactic-occurrence","line":121,"migration":{"status":"not-a-call"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"bound at a single threshold via `interval_decide` and use monotonicity to discharge","tactic":"interval_decide"} +{"actual":false,"column":48,"declaration":null,"kind":"tactic-occurrence","line":122,"migration":{"status":"not-a-call"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"all other instances for free. Saves dozens of `interval_decide` invocations per file in","tactic":"interval_decide"} +{"actual":true,"column":56,"declaration":"exp_neg_lt_1e_neg_20","kind":"tactic-occurrence","line":127,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"have h_boundary : Real.exp (-(50 : \u211d)) < 1e-20 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":58,"declaration":"exp_neg_lt_1e_neg_100","kind":"tactic-occurrence","line":132,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"have h_boundary : Real.exp (-(231 : \u211d)) < 1e-100 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":52,"declaration":"log_2_353_gt","kind":"tactic-occurrence","line":137,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_2_353_gt : (0.855 : \u211d) < log 2.353 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":48,"declaration":"log_3_2_gt","kind":"tactic-occurrence","line":138,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_3_2_gt : (1.163 : \u211d) < log 3.2 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":52,"declaration":"exp_1_112_lt","kind":"tactic-occurrence","line":139,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_1_112_lt : exp (1.112 : \u211d) < 3.041 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":53,"declaration":"log_6_58_gt","kind":"tactic-occurrence","line":140,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_6_58_gt : (1.884034 : \u211d) < log 6.58 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"log_log_6_58_gt","kind":"tactic-occurrence","line":141,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_log_6_58_gt : (0.633415 : \u211d) < log (log 6.58) := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":58,"declaration":"log_log_2_gt","kind":"tactic-occurrence","line":142,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_log_2_gt : (-0.366513 : \u211d) \u2264 log (log 2) := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":52,"declaration":"log_log_2_lt","kind":"tactic-occurrence","line":143,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_log_2_lt : log (log 2) \u2264 -0.366512 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":56,"declaration":"log_11723_lt","kind":"tactic-occurrence","line":144,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_11723_lt : log (11723 : \u211d) \u2264 937 / 100 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":55,"declaration":"log_5e10_gt","kind":"tactic-occurrence","line":145,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_5e10_gt : (24.6352888 : \u211d) \u2264 log 5e10 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":55,"declaration":"log_5e10_lt","kind":"tactic-occurrence","line":146,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_5e10_lt : log 5e10 \u2264 (24.6352889 : \u211d) := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"log_32e12_gt","kind":"tactic-occurrence","line":147,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_32e12_gt : (31.0967570 : \u211d) \u2264 log 32e12 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"log_32e12_lt","kind":"tactic-occurrence","line":148,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_32e12_lt : log 32e12 \u2264 (31.0967571 : \u211d) := by interval_decide","tactic":"interval_decide"} +{"actual":false,"column":60,"declaration":null,"kind":"tactic-occurrence","line":154,"migration":{"status":"not-a-call"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"just reads `LogTables.log_N_cube_lt` instead of an inline `interval_auto`. -/","tactic":"interval_auto"} +{"actual":true,"column":42,"declaration":"log_130_lt","kind":"tactic-occurrence","line":156,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_130_lt : log 130 < 4.868 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":42,"declaration":"log_155_lt","kind":"tactic-occurrence","line":157,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_155_lt : log 155 < 5.044 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":42,"declaration":"log_200_lt","kind":"tactic-occurrence","line":158,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_200_lt : log 200 < 5.299 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":42,"declaration":"log_300_lt","kind":"tactic-occurrence","line":159,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_300_lt : log 300 < 5.704 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":42,"declaration":"log_550_lt","kind":"tactic-occurrence","line":160,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_550_lt : log 550 < 6.310 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":44,"declaration":"log_1500_lt","kind":"tactic-occurrence","line":161,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_1500_lt : log 1500 < 7.314 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":46,"declaration":"log_10000_lt","kind":"tactic-occurrence","line":162,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_10000_lt : log 10000 < 9.211 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":52,"declaration":"log_1e8_lt","kind":"tactic-occurrence","line":163,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_1e8_lt : log ((10 : \u211d)^8) < 18.421 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":58,"declaration":"log_3e10_lt","kind":"tactic-occurrence","line":164,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_3e10_lt : log (3 * (10 : \u211d)^10) < 24.125 := by interval_decide","tactic":"interval_decide"} +{"actual":false,"column":50,"declaration":null,"kind":"tactic-occurrence","line":218,"migration":{"status":"not-a-call"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"Cached so the relevant files don't need a fresh `interval_decide` per call site. -/","tactic":"interval_decide"} +{"actual":true,"column":42,"declaration":"exp_two_lt_eight","kind":"tactic-occurrence","line":221,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_two_lt_eight : exp 2 < 8 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":44,"declaration":"exp_20_le","kind":"tactic-occurrence","line":224,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_20_le : exp 20 \u2264 485165196 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":51,"declaration":"one_e9_le_exp_22","kind":"tactic-occurrence","line":227,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma one_e9_le_exp_22 : (1e9 : \u211d) \u2264 exp 22 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":79,"declaration":"inv_900000_le_exp_neg_13_5","kind":"tactic-occurrence","line":230,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma inv_900000_le_exp_neg_13_5 : (1 / 900000 : \u211d) \u2264 exp (-(13.5 : \u211d)) := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":41,"declaration":"pi_le_3_15","kind":"tactic-occurrence","line":233,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma pi_le_3_15 : \u03c0 \u2264 (3.15 : \u211d) := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":56,"declaration":"exp_neg_10_lt","kind":"tactic-occurrence","line":244,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_10_lt : exp (-(10 : \u211d)) < 4.541e-5 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_21_2_lt","kind":"tactic-occurrence","line":245,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_21_2_lt : exp (-(21/2 : \u211d)) < 2.755e-5 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":56,"declaration":"exp_neg_11_lt","kind":"tactic-occurrence","line":246,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_11_lt : exp (-(11 : \u211d)) < 1.672e-5 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_23_2_lt","kind":"tactic-occurrence","line":247,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_23_2_lt : exp (-(23/2 : \u211d)) < 1.015e-5 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":56,"declaration":"exp_neg_12_lt","kind":"tactic-occurrence","line":248,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_12_lt : exp (-(12 : \u211d)) < 6.146e-6 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_25_2_lt","kind":"tactic-occurrence","line":249,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_25_2_lt : exp (-(25/2 : \u211d)) < 3.728e-6 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":56,"declaration":"exp_neg_13_lt","kind":"tactic-occurrence","line":250,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_13_lt : exp (-(13 : \u211d)) < 2.262e-6 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_40_3_lt","kind":"tactic-occurrence","line":251,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_40_3_lt : exp (-(40/3 : \u211d)) < 1.621e-6 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_27_2_lt","kind":"tactic-occurrence","line":252,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_27_2_lt : exp (-(27/2 : \u211d)) < 1.372e-6 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":56,"declaration":"exp_neg_14_lt","kind":"tactic-occurrence","line":253,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_14_lt : exp (-(14 : \u211d)) < 8.317e-7 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_29_2_lt","kind":"tactic-occurrence","line":254,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_29_2_lt : exp (-(29/2 : \u211d)) < 5.045e-7 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_44_3_lt","kind":"tactic-occurrence","line":255,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_44_3_lt : exp (-(44/3 : \u211d)) < 4.271e-7 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":56,"declaration":"exp_neg_15_lt","kind":"tactic-occurrence","line":256,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_15_lt : exp (-(15 : \u211d)) < 3.061e-7 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_46_3_lt","kind":"tactic-occurrence","line":257,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_46_3_lt : exp (-(46/3 : \u211d)) < 2.193e-7 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_31_2_lt","kind":"tactic-occurrence","line":258,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_31_2_lt : exp (-(31/2 : \u211d)) < 1.857e-7 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":56,"declaration":"exp_neg_16_lt","kind":"tactic-occurrence","line":259,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_16_lt : exp (-(16 : \u211d)) < 1.127e-7 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_33_2_lt","kind":"tactic-occurrence","line":260,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_33_2_lt : exp (-(33/2 : \u211d)) < 6.827e-8 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_50_3_lt","kind":"tactic-occurrence","line":261,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_50_3_lt : exp (-(50/3 : \u211d)) < 5.779e-8 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":56,"declaration":"exp_neg_17_lt","kind":"tactic-occurrence","line":262,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_17_lt : exp (-(17 : \u211d)) < 4.141e-8 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_52_3_lt","kind":"tactic-occurrence","line":263,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_52_3_lt : exp (-(52/3 : \u211d)) < 2.968e-8 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_35_2_lt","kind":"tactic-occurrence","line":264,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_35_2_lt : exp (-(35/2 : \u211d)) < 2.512e-8 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":56,"declaration":"exp_neg_18_lt","kind":"tactic-occurrence","line":265,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_18_lt : exp (-(18 : \u211d)) < 1.524e-8 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_37_2_lt","kind":"tactic-occurrence","line":266,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_37_2_lt : exp (-(37/2 : \u211d)) < 9.239e-9 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_56_3_lt","kind":"tactic-occurrence","line":267,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_56_3_lt : exp (-(56/3 : \u211d)) < 7.821e-9 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":56,"declaration":"exp_neg_19_lt","kind":"tactic-occurrence","line":268,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_19_lt : exp (-(19 : \u211d)) < 5.604e-9 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_58_3_lt","kind":"tactic-occurrence","line":269,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_58_3_lt : exp (-(58/3 : \u211d)) < 4.016e-9 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_39_2_lt","kind":"tactic-occurrence","line":270,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_39_2_lt : exp (-(39/2 : \u211d)) < 3.400e-9 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":56,"declaration":"exp_neg_20_lt","kind":"tactic-occurrence","line":271,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_20_lt : exp (-(20 : \u211d)) < 2.063e-9 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_41_2_lt","kind":"tactic-occurrence","line":272,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_41_2_lt : exp (-(41/2 : \u211d)) < 1.252e-9 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":60,"declaration":"exp_neg_62_3_lt","kind":"tactic-occurrence","line":273,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_62_3_lt : exp (-(62/3 : \u211d)) < 1.060e-9 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"exp_neg_21_lt","kind":"tactic-occurrence","line":274,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_21_lt : exp (-(21 : \u211d)) < 7.584e-10 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_64_3_lt","kind":"tactic-occurrence","line":275,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_64_3_lt : exp (-(64/3 : \u211d)) < 5.435e-10 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_43_2_lt","kind":"tactic-occurrence","line":276,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_43_2_lt : exp (-(43/2 : \u211d)) < 4.601e-10 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"exp_neg_22_lt","kind":"tactic-occurrence","line":277,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_22_lt : exp (-(22 : \u211d)) < 2.791e-10 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_45_2_lt","kind":"tactic-occurrence","line":278,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_45_2_lt : exp (-(45/2 : \u211d)) < 1.693e-10 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_68_3_lt","kind":"tactic-occurrence","line":279,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_68_3_lt : exp (-(68/3 : \u211d)) < 1.434e-10 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"exp_neg_23_lt","kind":"tactic-occurrence","line":280,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_23_lt : exp (-(23 : \u211d)) < 1.028e-10 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_70_3_lt","kind":"tactic-occurrence","line":281,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_70_3_lt : exp (-(70/3 : \u211d)) < 7.354e-11 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_47_2_lt","kind":"tactic-occurrence","line":282,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_47_2_lt : exp (-(47/2 : \u211d)) < 6.226e-11 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"exp_neg_24_lt","kind":"tactic-occurrence","line":283,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_24_lt : exp (-(24 : \u211d)) < 3.777e-11 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_49_2_lt","kind":"tactic-occurrence","line":284,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_49_2_lt : exp (-(49/2 : \u211d)) < 2.291e-11 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_74_3_lt","kind":"tactic-occurrence","line":285,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_74_3_lt : exp (-(74/3 : \u211d)) < 1.940e-11 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"exp_neg_25_lt","kind":"tactic-occurrence","line":286,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_25_lt : exp (-(25 : \u211d)) < 1.390e-11 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_76_3_lt","kind":"tactic-occurrence","line":287,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_76_3_lt : exp (-(76/3 : \u211d)) < 9.953e-12 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_51_2_lt","kind":"tactic-occurrence","line":288,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_51_2_lt : exp (-(51/2 : \u211d)) < 8.425e-12 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"exp_neg_26_lt","kind":"tactic-occurrence","line":289,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_26_lt : exp (-(26 : \u211d)) < 5.111e-12 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_53_2_lt","kind":"tactic-occurrence","line":290,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_53_2_lt : exp (-(53/2 : \u211d)) < 3.100e-12 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_80_3_lt","kind":"tactic-occurrence","line":291,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_80_3_lt : exp (-(80/3 : \u211d)) < 2.625e-12 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"exp_neg_27_lt","kind":"tactic-occurrence","line":292,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_27_lt : exp (-(27 : \u211d)) < 1.881e-12 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_82_3_lt","kind":"tactic-occurrence","line":293,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_82_3_lt : exp (-(82/3 : \u211d)) < 1.348e-12 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_55_2_lt","kind":"tactic-occurrence","line":294,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_55_2_lt : exp (-(55/2 : \u211d)) < 1.141e-12 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"exp_neg_28_lt","kind":"tactic-occurrence","line":295,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_28_lt : exp (-(28 : \u211d)) < 6.916e-13 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_57_2_lt","kind":"tactic-occurrence","line":296,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_57_2_lt : exp (-(57/2 : \u211d)) < 4.195e-13 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_86_3_lt","kind":"tactic-occurrence","line":297,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_86_3_lt : exp (-(86/3 : \u211d)) < 3.551e-13 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"exp_neg_29_lt","kind":"tactic-occurrence","line":298,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_29_lt : exp (-(29 : \u211d)) < 2.545e-13 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_88_3_lt","kind":"tactic-occurrence","line":299,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_88_3_lt : exp (-(88/3 : \u211d)) < 1.824e-13 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_59_2_lt","kind":"tactic-occurrence","line":300,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_59_2_lt : exp (-(59/2 : \u211d)) < 1.544e-13 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"exp_neg_30_lt","kind":"tactic-occurrence","line":301,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_30_lt : exp (-(30 : \u211d)) < 9.359e-14 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_92_3_lt","kind":"tactic-occurrence","line":302,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_92_3_lt : exp (-(92/3 : \u211d)) < 4.806e-14 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_94_3_lt","kind":"tactic-occurrence","line":303,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_94_3_lt : exp (-(94/3 : \u211d)) < 2.468e-14 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"exp_neg_32_lt","kind":"tactic-occurrence","line":304,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_32_lt : exp (-(32 : \u211d)) < 1.268e-14 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":61,"declaration":"exp_neg_98_3_lt","kind":"tactic-occurrence","line":305,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_98_3_lt : exp (-(98/3 : \u211d)) < 6.503e-15 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"exp_neg_100_3_lt","kind":"tactic-occurrence","line":306,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_100_3_lt : exp (-(100/3 : \u211d)) < 3.340e-15 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"exp_neg_34_lt","kind":"tactic-occurrence","line":307,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_34_lt : exp (-(34 : \u211d)) < 1.715e-15 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"exp_neg_104_3_lt","kind":"tactic-occurrence","line":308,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_104_3_lt : exp (-(104/3 : \u211d)) < 8.801e-16 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"exp_neg_106_3_lt","kind":"tactic-occurrence","line":309,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_106_3_lt : exp (-(106/3 : \u211d)) < 4.519e-16 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"exp_neg_36_lt","kind":"tactic-occurrence","line":310,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_36_lt : exp (-(36 : \u211d)) < 2.321e-16 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"exp_neg_110_3_lt","kind":"tactic-occurrence","line":311,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_110_3_lt : exp (-(110/3 : \u211d)) < 1.192e-16 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"exp_neg_112_3_lt","kind":"tactic-occurrence","line":312,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_112_3_lt : exp (-(112/3 : \u211d)) < 6.116e-17 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"exp_neg_38_lt","kind":"tactic-occurrence","line":313,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_38_lt : exp (-(38 : \u211d)) < 3.141e-17 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"exp_neg_116_3_lt","kind":"tactic-occurrence","line":314,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_116_3_lt : exp (-(116/3 : \u211d)) < 1.613e-17 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":63,"declaration":"exp_neg_118_3_lt","kind":"tactic-occurrence","line":315,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_118_3_lt : exp (-(118/3 : \u211d)) < 8.276e-18 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"exp_neg_40_lt","kind":"tactic-occurrence","line":316,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_40_lt : exp (-(40 : \u211d)) < 4.250e-18 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":53,"declaration":"exp_neg_50_lt","kind":"tactic-occurrence","line":317,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_50_lt : exp (-(50 : \u211d)) < 1e-20 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":59,"declaration":"exp_neg_200_3_lt","kind":"tactic-occurrence","line":318,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_200_3_lt : exp (-(200/3 : \u211d)) < 1e-26 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":55,"declaration":"exp_neg_100_lt","kind":"tactic-occurrence","line":319,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_100_lt : exp (-(100 : \u211d)) < 1e-40 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":59,"declaration":"exp_neg_400_3_lt","kind":"tactic-occurrence","line":320,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_400_3_lt : exp (-(400/3 : \u211d)) < 1e-53 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":55,"declaration":"exp_neg_150_lt","kind":"tactic-occurrence","line":321,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_150_lt : exp (-(150 : \u211d)) < 1e-60 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":55,"declaration":"exp_neg_200_lt","kind":"tactic-occurrence","line":322,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma exp_neg_200_lt : exp (-(200 : \u211d)) < 1e-80 := by interval_decide","tactic":"interval_decide"} +{"actual":true,"column":57,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":26,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 2 3 count_prime_3_le_1 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":57,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":27,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 3 5 count_prime_5_le_2 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":57,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":28,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 4 7 count_prime_7_le_3 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":59,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":29,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 5 11 count_prime_11_le_4 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":59,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":30,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 6 13 count_prime_13_le_5 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":59,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":31,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 7 17 count_prime_17_le_6 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":59,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":32,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 8 19 count_prime_19_le_7 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":59,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":33,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 9 23 count_prime_23_le_8 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":60,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":34,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 10 29 count_prime_29_le_9 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":61,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":35,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 11 31 count_prime_31_le_10 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":61,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":36,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 12 37 count_prime_37_le_11 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":61,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":37,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 13 41 count_prime_41_le_12 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":61,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":38,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 14 43 count_prime_43_le_13 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":61,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":39,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 15 47 count_prime_47_le_14 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":61,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":40,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 16 53 count_prime_53_le_15 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":61,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":41,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 17 59 count_prime_59_le_16 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":61,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":42,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 18 61 count_prime_61_le_17 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":61,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":43,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 19 67 count_prime_67_le_18 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":61,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":44,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 20 71 count_prime_71_le_19 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":61,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":45,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 21 73 count_prime_73_le_20 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":61,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":46,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 22 79 count_prime_79_le_21 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":61,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":47,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 23 83 count_prime_83_le_22 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":61,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":48,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 24 89 count_prime_89_le_23 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":61,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":49,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 25 97 count_prime_97_le_24 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":63,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":50,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 26 101 count_prime_101_le_25 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":63,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":51,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 27 103 count_prime_103_le_26 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":63,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":52,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 28 107 count_prime_107_le_27 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":63,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":53,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 29 109 count_prime_109_le_28 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":63,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":54,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 30 113 count_prime_113_le_29 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":63,"declaration":"p_n_lower_small","kind":"tactic-occurrence","line":55,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","snippet":"\u00b7 exact nth_prime_gt_bound 31 127 count_prime_127_le_30 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":44,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":925,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 2 3 count_prime_3_le_1 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":44,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":926,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 3 5 count_prime_5_le_2 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":44,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":927,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 4 7 count_prime_7_le_3 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":46,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":928,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 5 11 count_prime_11_le_4 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":46,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":929,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 6 13 count_prime_13_le_5 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":46,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":930,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 7 17 count_prime_17_le_6 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":46,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":931,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 8 19 count_prime_19_le_7 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":46,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":932,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 9 23 count_prime_23_le_8 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":47,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":933,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 10 29 count_prime_29_le_9 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":48,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":934,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 11 31 count_prime_31_le_10 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":48,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":935,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 12 37 count_prime_37_le_11 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":48,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":936,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 13 41 count_prime_41_le_12 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":48,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":937,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 14 43 count_prime_43_le_13 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":48,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":938,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 15 47 count_prime_47_le_14 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":48,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":939,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 16 53 count_prime_53_le_15 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":48,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":940,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 17 59 count_prime_59_le_16 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":48,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":941,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 18 61 count_prime_61_le_17 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":48,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":942,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 19 67 count_prime_67_le_18 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":48,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":943,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 20 71 count_prime_71_le_19 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":48,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":944,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 21 73 count_prime_73_le_20 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":48,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":945,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 22 79 count_prime_79_le_21 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":48,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":946,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 23 83 count_prime_83_le_22 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":48,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":947,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 24 89 count_prime_89_le_23 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":48,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":948,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 25 97 count_prime_97_le_24 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":50,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":949,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 26 101 count_prime_101_le_25 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":50,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":950,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 27 103 count_prime_103_le_26 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":50,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":951,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 28 107 count_prime_107_le_27 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":50,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":952,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 29 109 count_prime_109_le_28 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":50,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":953,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 30 113 count_prime_113_le_29 (by interval_auto)","tactic":"interval_auto"} +{"actual":true,"column":50,"declaration":"p_n_gt_1","kind":"tactic-occurrence","line":954,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","snippet":"\u00b7 exact key 31 127 count_prime_127_le_30 (by interval_auto)","tactic":"interval_auto"} diff --git a/progress/20260814T125511Z.md b/progress/20260814T125511Z.md new file mode 100644 index 000000000..e335bfa0a --- /dev/null +++ b/progress/20260814T125511Z.md @@ -0,0 +1,40 @@ +# Accomplished + +- Implemented the source-pinned PNT+/LeanCert migration inventory generator, + its committed JSONL fixture, and a network-free per-PR integrity gate. +- Audited all tracked PNT+ Lean sources at commit `21998bb`, recording 280 + executable `interval_decide` sites, 60 `interval_auto` sites, 83 executable + textual `native_decide` sites, sixteen direct LeanCert imports, 107 qualified + references, and six load-bearing imported interface families. +- Recorded the generated workload surface separately: 87 Table 10 target + proof sites, 38 supporting `a₂` sites, 130 Table 12 checks, and all 13,590 + FKS2 cells across fourteen shards. +- Added unit coverage for lexical masking, pin and audit identity, migration + schema, exact source partitions, generated batches, classification failure, + and source-field tampering. Updated the SPEC to distinguish a complete audit + backlog from a completed migration or LeanCert compatibility promise. +- Made the maintainer path preserve real classification work: refresh carries + decisions by audit identity and refuses classified deletions, source + verification ignores migration-only edits, and `--update-classifications` + validates edited evidence before resealing the full record digest. + +# Current frontier + +The inventory is fully source-pinned and locally verified, while all 449 +executable/imported migration records deliberately remain `pending`. +Ordinary CI accepts this pre-D8 state; `--require-classified` fails until each +entry carries the required proof, rewrite, replacement, dependency, or +expected-failure evidence. + +# Next step + +Obtain a fresh exact-diff review, address any remaining audit-honesty issue, +then push an upstream PR against current `main` and require exact-head CI before +merge. Subsequent D8 work should classify entries while adding the referenced +ported proof fixtures, beginning with representative logarithm and exponential +families rather than compatibility wrappers. + +# Blockers + +No implementation blocker. This change intentionally does not claim the PNT+ +migration itself is complete. diff --git a/scripts/maintenance/pnt_inventory.py b/scripts/maintenance/pnt_inventory.py new file mode 100644 index 000000000..a5ebe523e --- /dev/null +++ b/scripts/maintenance/pnt_inventory.py @@ -0,0 +1,1111 @@ +#!/usr/bin/env python3 +"""Generate and validate the source-pinned PNT+/LeanCert usage inventory. + +Refresh mode reads an exact checkout of PrimeNumberTheoremAnd, masks Lean +comments and string literals without changing source offsets, and records: + +* textual and executable ``interval_decide`` / ``interval_auto`` occurrences; +* direct LeanCert imports, qualified references, and the six imported public + interface families that the migration must classify; +* executable textual ``native_decide`` occurrences (trust-audit candidates); and +* the generated FKS2 Table4Ext shard sizes plus named BKLNW tactic families. + +Check mode is deliberately network-free. It validates the committed JSONL's +pins, record digest, counts, ordering, classifications, and batch invariants. +Use ``--require-classified`` for a migration/release claim; the ordinary +pre-D8 structural check permits explicit ``pending`` migration decisions. +""" +from __future__ import annotations + +import argparse +import hashlib +import json +import re +import subprocess +import sys +from collections import Counter +from dataclasses import dataclass +from pathlib import Path +from typing import Any, Iterable + + +PNT_COMMIT = "21998bb6196b56789f72a52656a781a75e134eb0" +LEANCERT_COMMIT = "58edbea59458e9b010262238eaca27b6e0240dae" +MATHLIB_COMMIT = "905b95818eb32af7874a58b427f50c1711a5e96c" +LEAN_TOOLCHAIN = "leanprover/lean4:v4.32.2" +FORMAT_VERSION = 1 +PNT_LEAN_SOURCE_DIGEST = "84b1cdfe1cae7b6ddc181aede13c35b276422a206f6815143c2a1c50c3c0b112" +PNT_LEAN_SOURCE_FILES = 232 +# Digest of fixed record identity with editable migration decisions removed. +# It covers source locations plus reviewed interface/workload annotations; it +# is not described as if every annotation were mechanically source-derived. +PNT_AUDIT_RECORD_DIGEST = "6cfed911ea5dc11a114be8cadad83aaf1a68972a166700ceea894a7145e2d07d" + +EXPECTED = { + "interval_decide_actual": 280, + "interval_decide_textual": 290, + "interval_auto_actual": 60, + "interval_auto_textual": 61, + "native_decide_actual": 83, + "leancert_import": 16, + "leancert_reference": 107, + "dependency_interface": 6, + "fks2_cells": 13590, + "fks2_shards": 14, + "bklnw_table10_target_sites": 87, + "bklnw_table10_a2_sites": 38, + "bklnw_table12_checks": 130, + "bklnw_table12_ordinary_rows": 24, + "bklnw_table12_logarithmic_rows": 2, +} + +DEPENDENCY_INTERFACES = { + "LeanCert.ANT": ( + "whole-interval ANT expression checker used by the extended FKS2 table", + "fks2-table4ext", + ), + "LeanCert.CertifiedBounds.BKLNW": ( + "certified exponential and power bounds used by the BKLNW sums", + "bklnw-certified-bounds", + ), + "LeanCert.CertifiedBounds.Chebyshev": ( + "certified Chebyshev bounds used by Chebyshev, FKS2 floor, and Ramanujan proofs", + "chebyshev-certified-bounds", + ), + "LeanCert.CertifiedBounds.Li2": ( + "Li(2) integrand, positivity, boundedness, value, and integral bounds", + "li2-certified-bounds", + ), + "LeanCert.Tactic.IntervalAuto": ( + "interval_decide and interval_auto tactic entry points", + "interval-tactics", + ), + "LeanCert.Validity.AffineCover": ( + "affine-cover certificate used by the small-x FKS2 floor", + "affine-cover", + ), +} + +# Lexical qualified references are audit evidence, not separate migration +# obligations. This table records which reviewed imported interface owns each +# namespace surface, including namespaces reached transitively by that import. +REFERENCE_PROVENANCE = { + "LeanCert.ANT": ("LeanCert.ANT",), + "LeanCert.CertifiedBounds.BKLNW": ("LeanCert.CertifiedBounds.BKLNW",), + "LeanCert.CertifiedBounds.Chebyshev": ( + "LeanCert.CertifiedBounds.Chebyshev", + ), + "LeanCert.CertifiedBounds.Li2": ("LeanCert.CertifiedBounds.Li2",), + "LeanCert.Core": ("LeanCert.ANT", "LeanCert.Validity.AffineCover"), + "LeanCert.Validity": ("LeanCert.Validity.AffineCover",), +} + +CLASSIFICATIONS = { + "pending", + "accepted-unchanged", + "accepted-after-rewrite", + "replaced-by-stronger-result", + "retained-other-dependency", + "expected-failure", +} + +TOKEN_RE = { + name: re.compile(rf"(?theorem|lemma|def|abbrev|opaque|instance|example)\b" + r"(?:\s+(?P[A-Za-z_][A-Za-z0-9_'.]*))?" +) +FKS_CELL_RE = re.compile(r"^\s*⟨") + + +class InventoryError(RuntimeError): + pass + + +@dataclass(frozen=True) +class Source: + path: str + text: str + masked: str + declarations: tuple[str | None, ...] + + +def mask_lean(text: str) -> str: + """Mask comments and string literals, preserving offsets and newlines.""" + out = list(text) + i = 0 + block_depth = 0 + state = "code" + while i < len(text): + if block_depth: + if text.startswith("/-", i): + out[i : i + 2] = " " + block_depth += 1 + i += 2 + elif text.startswith("-/", i): + out[i : i + 2] = " " + block_depth -= 1 + i += 2 + else: + if text[i] != "\n": + out[i] = " " + i += 1 + continue + + if state == "string": + if text[i] == "\\" and i + 1 < len(text): + out[i] = " " + if text[i + 1] != "\n": + out[i + 1] = " " + i += 2 + else: + ch = text[i] + if ch != "\n": + out[i] = " " + i += 1 + if ch == '"': + state = "code" + continue + + if text.startswith("--", i): + while i < len(text) and text[i] != "\n": + out[i] = " " + i += 1 + elif text.startswith("/-", i): + out[i : i + 2] = " " + block_depth = 1 + i += 2 + elif text[i] == "'": + end = char_literal_end(text, i) + if end is None: + i += 1 + else: + for pos in range(i, end): + out[pos] = " " + i = end + elif text[i] == '"': + out[i] = " " + state = "string" + i += 1 + else: + i += 1 + if block_depth: + raise InventoryError("unterminated Lean block comment") + if state == "string": + raise InventoryError("unterminated Lean string literal") + return "".join(out) + + +def char_literal_end(text: str, start: int) -> int | None: + """Return the end offset of a syntactic Lean character literal, if any.""" + if start > 0 and (text[start - 1].isalnum() or text[start - 1] in "_'"): + return None + if start + 2 < len(text) and text[start + 1] not in {"\\", "\n"} \ + and text[start + 2] == "'": + return start + 3 + if start + 3 < len(text) and text[start + 1] == "\\" \ + and text[start + 2] != "\n": + # The byte immediately after the backslash is part of the escape. In + # particular, it is not the closing delimiter in the literal '\\''. + end = start + 3 + while end < min(len(text), start + 16) and text[end] != "\n": + if text[end] == "'": + return end + 1 + end += 1 + return None + + +def declaration_map(masked: str) -> tuple[str | None, ...]: + current: str | None = None + result: list[str | None] = [] + for line_no, line in enumerate(masked.splitlines(), 1): + match = DECL_RE.match(line) + if match: + kind = match.group("kind") + name = match.group("name") + current = name if name and kind != "example" else f"{kind}@{line_no}" + result.append(current) + return tuple(result) + + +def line_col(text: str, offset: int) -> tuple[int, int]: + line = text.count("\n", 0, offset) + 1 + start = text.rfind("\n", 0, offset) + 1 + return line, offset - start + 1 + + +def snippet(text: str, line: int) -> str: + lines = text.splitlines() + return lines[line - 1].strip() if 0 < line <= len(lines) else "" + + +def git_head(root: Path) -> str: + proc = subprocess.run( + ["git", "rev-parse", "HEAD"], cwd=root, text=True, + stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=False, + ) + if proc.returncode != 0: + raise InventoryError(f"source is not a git checkout: {root}") + return proc.stdout.strip() + + +def load_pins(root: Path) -> dict[str, str]: + manifest = json.loads((root / "lake-manifest.json").read_text(encoding="utf-8")) + packages = {entry["name"]: entry["rev"] for entry in manifest["packages"]} + return { + "pnt": git_head(root), + "leancert": packages.get("leancert", ""), + "mathlib": packages.get("mathlib", ""), + "lean_toolchain": (root / "lean-toolchain").read_text(encoding="utf-8").strip(), + } + + +def require_pins(pins: dict[str, str]) -> None: + expected = { + "pnt": PNT_COMMIT, + "leancert": LEANCERT_COMMIT, + "mathlib": MATHLIB_COMMIT, + "lean_toolchain": LEAN_TOOLCHAIN, + } + if pins != expected: + raise InventoryError(f"upstream pins differ: expected {expected}, got {pins}") + + +def load_sources(root: Path) -> list[Source]: + proc = subprocess.run( + ["git", "ls-files", "--", "*.lean"], cwd=root, text=True, + stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=False, + ) + if proc.returncode != 0: + raise InventoryError(f"cannot list pinned Lean sources: {proc.stderr.strip()}") + paths = [root / line for line in proc.stdout.splitlines() if line] + if not paths: + raise InventoryError(f"no tracked Lean sources in {root}") + sources: list[Source] = [] + for path in paths: + text = path.read_text(encoding="utf-8") + masked = mask_lean(text) + sources.append(Source( + path=path.relative_to(root).as_posix(), + text=text, + masked=masked, + declarations=declaration_map(masked), + )) + return sources + + +def source_digest(sources: Iterable[Source]) -> str: + digest = hashlib.sha256() + for source in sources: + digest.update(source.path.encode()) + digest.update(b"\0") + digest.update(source.text.encode()) + digest.update(b"\0") + return digest.hexdigest() + + +def classification() -> dict[str, str]: + return { + "status": "pending", + "note": "D8 migration decision not yet assigned", + } + + +def inventory_only() -> dict[str, str]: + return { + "status": "inventory-only", + "note": "lexical audit evidence subsumed by imported-interface classification", + } + + +def occurrence_record(source: Source, token: str, match: re.Match[str], + actual: bool) -> dict[str, Any]: + line, column = line_col(source.text, match.start()) + declaration = ( + source.declarations[line - 1] + if actual and line <= len(source.declarations) else None + ) + return { + "kind": "tactic-occurrence", + "tactic": token, + "actual": actual, + "path": source.path, + "line": line, + "column": column, + "declaration": declaration, + "snippet": snippet(source.text, line), + "migration": classification() if actual else {"status": "not-a-call"}, + } + + +def tactic_records(sources: Iterable[Source]) -> list[dict[str, Any]]: + records: list[dict[str, Any]] = [] + for source in sources: + for token in ("interval_decide", "interval_auto"): + actual_offsets = {m.start() for m in TOKEN_RE[token].finditer(source.masked)} + for match in TOKEN_RE[token].finditer(source.text): + records.append(occurrence_record( + source, token, match, match.start() in actual_offsets, + )) + return records + + +def import_records(sources: Iterable[Source]) -> list[dict[str, Any]]: + records: list[dict[str, Any]] = [] + for source in sources: + for line_no, line in enumerate(source.masked.splitlines(), 1): + match = IMPORT_RE.match(line) + if match: + records.append({ + "kind": "leancert-import", + "module": match.group(1), + "path": source.path, + "line": line_no, + "migration": classification(), + }) + return records + + +def dependency_records(imports: list[dict[str, Any]]) -> list[dict[str, Any]]: + """Record audited public interfaces without pretending to name-resolve Lean. + + Qualified symbol occurrences are recorded separately. Uses after ``open`` + cannot be resolved reliably by a lexer, so the durable obligation here is + the imported interface family and its load-bearing role. Migration work + later classifies the exact replacement theorem(s). + """ + imported = {row["module"] for row in imports} + expected = set(DEPENDENCY_INTERFACES) + if imported != expected: + raise InventoryError( + f"LeanCert import surface drifted: expected {sorted(expected)}, " + f"got {sorted(imported)}" + ) + result = [] + for module, (role, workload) in DEPENDENCY_INTERFACES.items(): + sites = [ + {"path": row["path"], "line": row["line"]} + for row in imports if row["module"] == module + ] + result.append({ + "kind": "dependency-interface", + "module": module, + "role": role, + "workload": workload, + "import_sites": sites, + "migration": classification(), + }) + return result + + +def reference_records(sources: Iterable[Source], *, audited: bool = True) \ + -> list[dict[str, Any]]: + records: list[dict[str, Any]] = [] + for source in sources: + import_lines = { + index for index, line in enumerate(source.masked.splitlines(), 1) + if IMPORT_RE.match(line) + } + for match in LEANCERT_REF_RE.finditer(source.masked): + line, column = line_col(source.masked, match.start()) + if line in import_lines: + continue + try: + provenance = reference_interfaces(match.group(0)) + except InventoryError: + if audited: + raise + provenance = [] + records.append({ + "kind": "leancert-reference", + "symbol": match.group(0), + "path": source.path, + "line": line, + "column": column, + "declaration": source.declarations[line - 1], + "interface_provenance": provenance, + "migration": inventory_only(), + }) + return records + + +def reference_interfaces(symbol: str) -> list[str]: + matches = [ + (prefix, interfaces) for prefix, interfaces in REFERENCE_PROVENANCE.items() + if symbol == prefix or symbol.startswith(prefix + ".") + ] + if not matches: + raise InventoryError(f"qualified reference lacks interface provenance: {symbol}") + _, interfaces = max(matches, key=lambda item: len(item[0])) + unknown = set(interfaces) - set(DEPENDENCY_INTERFACES) + if unknown: + raise InventoryError(f"reference provenance names unknown interfaces: {sorted(unknown)}") + return list(interfaces) + + +def native_records(sources: Iterable[Source]) -> list[dict[str, Any]]: + records: list[dict[str, Any]] = [] + for source in sources: + for match in TOKEN_RE["native_decide"].finditer(source.masked): + line, column = line_col(source.masked, match.start()) + records.append({ + "kind": "native-decide-occurrence", + "mechanism": "native_decide", + "path": source.path, + "line": line, + "column": column, + "declaration": source.declarations[line - 1], + "migration": classification(), + }) + return records + + +def table_rows(masked: str, definition: str) -> list[str]: + """Return the top-level tuple rows of one masked Lean list definition.""" + marker = re.compile( + rf"\bnoncomputable\s+def\s+{re.escape(definition)}(?![A-Za-z0-9_'])" + ) + matches = list(marker.finditer(masked)) + if len(matches) != 1: + raise InventoryError( + f"expected one pinned {definition} list definition, found {len(matches)}" + ) + try: + start = matches[0].start() + assign = masked.index(":=", matches[0].end()) + opening = masked.index("[", assign + 2) + except ValueError as exc: + raise InventoryError(f"cannot locate the pinned {definition} list") from exc + + bracket_depth = 1 + paren_depth = 0 + row_start: int | None = None + rows: list[str] = [] + index = opening + 1 + while index < len(masked) and bracket_depth: + char = masked[index] + if char == "[": + bracket_depth += 1 + elif char == "]": + bracket_depth -= 1 + if bracket_depth == 0: + if paren_depth or row_start is not None: + raise InventoryError(f"unterminated tuple in {definition}") + break + elif bracket_depth == 1: + if char == "(": + if paren_depth == 0: + row_start = index + paren_depth += 1 + elif char == ")": + if paren_depth == 0: + raise InventoryError(f"unmatched ')' in {definition}") + paren_depth -= 1 + if paren_depth == 0: + assert row_start is not None + rows.append(masked[row_start:index + 1]) + row_start = None + index += 1 + if bracket_depth: + raise InventoryError(f"unterminated list in {definition}") + return rows + + +def batch_records(sources: Iterable[Source], + tactic_rows: list[dict[str, Any]]) -> list[dict[str, Any]]: + source_list = list(sources) + by_path = {source.path: source for source in source_list} + shards: list[dict[str, Any]] = [] + for source in sorted(source_list, key=lambda item: item.path): + if not re.search(r"/FKS2Tables/Table4ExtData_[^/]*\.lean$", source.path): + continue + count = sum(1 for line in source.masked.splitlines() if FKS_CELL_RE.match(line)) + shards.append({"path": source.path, "cells": count}) + + table10_sites = [ + row for row in tactic_rows + if row["tactic"] == "interval_decide" and row["actual"] + and "/BKLNW/BKLNW_table10_rows" in row["path"] + ] + table10_targets = [ + row for row in table10_sites + if str(row.get("declaration", "")).startswith("table_10_") + ] + table10_a2 = [ + row for row in table10_sites + if str(row.get("declaration", "")).startswith("row") + and str(row.get("declaration", "")).endswith("_a2_le") + ] + if len(table10_targets) + len(table10_a2) != len(table10_sites): + raise InventoryError("unclassified BKLNW Table 10 source check site") + bklnw_all = [ + row for row in tactic_rows + if row["tactic"] == "interval_decide" and row["actual"] + and "/BKLNW/" in row["path"] + ] + table12_path = "PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_tables.lean" + try: + table12_masked = by_path[table12_path].masked + except KeyError as exc: + raise InventoryError("pinned BKLNW Table 12 source is not tracked") from exc + table12_rows = table_rows(table12_masked, "table_12") + table12_log_rows = sum(row.lstrip().startswith("(Real.log") for row in table12_rows) + table12_ordinary_rows = len(table12_rows) - table12_log_rows + return [ + { + "kind": "generated-family", + "family": "fks2-table4ext", + "source": "PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_*.lean", + "shards": shards, + "cells": sum(item["cells"] for item in shards), + "migration": classification(), + }, + { + "kind": "generated-family", + "family": "bklnw-table10-source-sites", + "source": "PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows*.lean", + "target_check_sites": len(table10_targets), + "supporting_a2_check_sites": len(table10_a2), + "declarations": [ + {"path": path, "declaration": declaration} + for path, declaration in sorted({ + (row["path"], row["declaration"]) + for row in table10_sites if row["declaration"] + }) + ], + "migration": classification(), + }, + { + "kind": "generated-family", + "family": "bklnw-all-source-checks", + "source": "PrimeNumberTheoremAnd/IEANTN/BKLNW/*.lean", + "actual_interval_decide": len(bklnw_all), + "declarations": [ + {"path": path, "declaration": declaration} + for path, declaration in sorted({ + (row["path"], row["declaration"]) + for row in bklnw_all if row["declaration"] + }) + ], + "migration": classification(), + }, + { + "kind": "generated-family", + "family": "bklnw-table12-cells", + "source": table12_path, + "check_declaration": "table_12_check", + "rows": len(table12_rows), + "ordinary_rows": table12_ordinary_rows, + "logarithmic_rows": table12_log_rows, + "checks_per_row": 5, + "expanded_checks": (table12_ordinary_rows + table12_log_rows) * 5, + "annotation_provenance": ( + "pinned BKLNW_tables.lean row count plus reviewed five-column " + "expansion; false rows from PNT+ PR #1405" + ), + "false_original_boundary_rows": [ + "log(5e10)", "25", "log(3.2e13)", "32", + ], + "migration": classification(), + }, + ] + + +def record_sort_key(record: dict[str, Any]) -> tuple[Any, ...]: + return ( + record["kind"], record.get("path", ""), record.get("line", -1), + record.get("column", -1), record.get("tactic", ""), + record.get("symbol", ""), record.get("module", ""), + record.get("family", ""), + json.dumps( + {name: value for name, value in record.items() if name != "migration"}, + sort_keys=True, separators=(",", ":"), + ), + ) + + +def record_digest(records: list[dict[str, Any]]) -> str: + digest = hashlib.sha256() + for record in records: + digest.update(json.dumps(record, sort_keys=True, separators=(",", ":")).encode()) + digest.update(b"\n") + return digest.hexdigest() + + +def audit_record_digest(records: list[dict[str, Any]]) -> str: + return record_digest(audit_records(records)) + + +def audit_records(records: list[dict[str, Any]]) -> list[dict[str, Any]]: + result = [] + for record in records: + audit_record = dict(record) + audit_record.pop("migration", None) + result.append(audit_record) + return result + + +def carry_migrations( + previous: list[dict[str, Any]], generated: list[dict[str, Any]], +) -> tuple[list[dict[str, Any]], int, int]: + def key(record: dict[str, Any]) -> str: + return json.dumps( + {name: value for name, value in record.items() if name != "migration"}, + sort_keys=True, separators=(",", ":"), + ) + + previous_by_key: dict[str, dict[str, Any]] = {} + for record in previous: + identity = key(record) + if identity in previous_by_key: + raise InventoryError("previous inventory has duplicate audit-record identity") + previous_by_key[identity] = record + + carried = 0 + result = [] + generated_keys = set() + for record in generated: + identity = key(record) + generated_keys.add(identity) + old = previous_by_key.get(identity) + if old is not None: + if record.get("migration", {}).get("status") \ + not in {"not-a-call", "inventory-only"}: + record = dict(record) + record["migration"] = old["migration"] + carried += 1 + result.append(record) + + removed = [ + record for identity, record in previous_by_key.items() + if identity not in generated_keys + ] + classified_removed = [ + record for record in removed + if record.get("migration", {}).get("status") + not in {"pending", "not-a-call", "inventory-only"} + ] + if classified_removed: + raise InventoryError( + f"refresh would discard {len(classified_removed)} classified records; " + "reconcile them explicitly before refreshing" + ) + return result, carried, len(removed) + + +def summarize(records: list[dict[str, Any]]) -> dict[str, int]: + tactic = [row for row in records if row["kind"] == "tactic-occurrence"] + fks = next((row for row in records + if row["kind"] == "generated-family" and row["family"] == "fks2-table4ext"), None) + table10 = next((row for row in records + if row["kind"] == "generated-family" + and row["family"] == "bklnw-table10-source-sites"), None) + table12 = next((row for row in records + if row["kind"] == "generated-family" + and row["family"] == "bklnw-table12-cells"), None) + return { + "interval_decide_actual": sum( + row["tactic"] == "interval_decide" and row["actual"] for row in tactic), + "interval_decide_textual": sum(row["tactic"] == "interval_decide" for row in tactic), + "interval_auto_actual": sum( + row["tactic"] == "interval_auto" and row["actual"] for row in tactic), + "interval_auto_textual": sum(row["tactic"] == "interval_auto" for row in tactic), + "leancert_import": sum(row["kind"] == "leancert-import" for row in records), + "leancert_reference": sum(row["kind"] == "leancert-reference" for row in records), + "dependency_interface": sum( + row["kind"] == "dependency-interface" for row in records), + "native_decide_actual": sum( + row["kind"] == "native-decide-occurrence" for row in records), + "fks2_cells": fks["cells"] if fks else 0, + "fks2_shards": len(fks["shards"]) if fks else 0, + "bklnw_table10_target_sites": table10["target_check_sites"] if table10 else 0, + "bklnw_table10_a2_sites": table10["supporting_a2_check_sites"] if table10 else 0, + "bklnw_table12_checks": table12["expanded_checks"] if table12 else 0, + "bklnw_table12_ordinary_rows": table12["ordinary_rows"] if table12 else 0, + "bklnw_table12_logarithmic_rows": ( + table12["logarithmic_rows"] if table12 else 0 + ), + "records": len(records), + } + + +def require_workload_partitions(records: list[dict[str, Any]]) -> None: + tactics = [row for row in records if row["kind"] == "tactic-occurrence"] + decide = [row for row in tactics if row["tactic"] == "interval_decide"] + + def partition(predicate: Any) -> tuple[int, int]: + rows = [row for row in decide if predicate(row)] + return len(rows), sum(row["actual"] for row in rows) + + log_tables = partition(lambda row: row["path"].endswith("/LogTables.lean")) + bklnw = partition(lambda row: "/BKLNW/" in row["path"]) + remaining = partition( + lambda row: not row["path"].endswith("/LogTables.lean") + and "/BKLNW/" not in row["path"] + ) + expected = { + "LogTables": (141, 136), + "BKLNW": (132, 128), + "remaining": (17, 16), + } + actual = {"LogTables": log_tables, "BKLNW": bklnw, "remaining": remaining} + if actual != expected: + raise InventoryError(f"PNT+ interval_decide partitions drifted: {actual} != {expected}") + bklnw_paths = {row["path"] for row in decide if "/BKLNW/" in row["path"]} + log_paths = {row["path"] for row in decide if row["path"].endswith("/LogTables.lean")} + if len(bklnw_paths) != 9: + raise InventoryError( + f"BKLNW interval_decide file count drifted: expected 9, got {len(bklnw_paths)}" + ) + if log_paths != {"PrimeNumberTheoremAnd/IEANTN/LogTables.lean"}: + raise InventoryError(f"LogTables interval_decide path drifted: {sorted(log_paths)}") + + paths = {row["path"] for row in decide} + if len(paths) != 15: + raise InventoryError(f"interval_decide file count drifted: expected 15, got {len(paths)}") + remaining_paths = { + "PrimeNumberTheoremAnd/IEANTN/Dusart.lean", + "PrimeNumberTheoremAnd/IEANTN/FKS2.lean", + "PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Cor14Tail.lean", + "PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean", + "PrimeNumberTheoremAnd/IEANTN/Goldbach.lean", + } + actual_remaining_paths = { + row["path"] for row in decide + if "/BKLNW/" not in row["path"] + and not row["path"].endswith("/LogTables.lean") + } + if actual_remaining_paths != remaining_paths: + raise InventoryError( + "remaining interval_decide file set drifted: " + f"{sorted(actual_remaining_paths)} != {sorted(remaining_paths)}" + ) + + interval_auto = [row for row in tactics if row["tactic"] == "interval_auto"] + actual_auto = [row for row in interval_auto if row["actual"]] + auto_counts = Counter(row["path"] for row in actual_auto) + expected_auto_counts = Counter({ + "PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean": 30, + "PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean": 30, + }) + if auto_counts != expected_auto_counts: + raise InventoryError( + f"interval_auto executable file partition drifted: {auto_counts} " + f"!= {expected_auto_counts}" + ) + + +def generate(root: Path) -> tuple[dict[str, Any], list[dict[str, Any]]]: + pins = load_pins(root) + require_pins(pins) + sources = load_sources(root) + if len(sources) != PNT_LEAN_SOURCE_FILES: + raise InventoryError( + f"pinned Lean-source file count drifted: expected {PNT_LEAN_SOURCE_FILES}, " + f"got {len(sources)}" + ) + tree_digest = source_digest(sources) + if tree_digest != PNT_LEAN_SOURCE_DIGEST: + raise InventoryError( + "pinned checkout contents differ from the audited Lean-source digest: " + f"expected {PNT_LEAN_SOURCE_DIGEST}, got {tree_digest}" + ) + tactics = tactic_records(sources) + imports = import_records(sources) + records = tactics + imports + dependency_records(imports) + reference_records(sources) + records += native_records(sources) + batch_records(sources, tactics) + records.sort(key=record_sort_key) + counts = summarize(records) + require_workload_partitions(records) + for name, expected in EXPECTED.items(): + if counts.get(name) != expected: + raise InventoryError( + f"upstream {name} drifted: expected {expected}, got {counts.get(name)}" + ) + meta = { + "kind": "meta", + "format": FORMAT_VERSION, + "pins": pins, + "lean_source_digest": tree_digest, + "lean_source_files": len(sources), + "audit_record_digest": audit_record_digest(records), + "record_digest": record_digest(records), + "counts": counts, + } + return meta, records + + +def inspect_source(root: Path) -> dict[str, Any]: + """Report observed pin-bump inputs without accepting them as audited.""" + pins = load_pins(root) + sources = load_sources(root) + tactics = tactic_records(sources) + imports = import_records(sources) + references = reference_records(sources, audited=False) + native = native_records(sources) + batch_error = None + try: + batches = batch_records(sources, tactics) + except InventoryError as exc: + batches = [] + batch_error = str(exc) + provisional = tactics + imports + references + native + batches + provisional.sort(key=record_sort_key) + counts = summarize(provisional) + counts["dependency_interface"] = len({row["module"] for row in imports}) + counts.pop("records", None) + return { + "pins": pins, + "lean_source_files": len(sources), + "lean_source_digest": source_digest(sources), + "observed_counts": counts, + "leancert_import_modules": sorted({row["module"] for row in imports}), + "generated_families": [ + {key: value for key, value in row.items() if key != "migration"} + for row in batches + ], + "generated_family_error": batch_error, + "warning": ( + "inspection is not an accepted audit; review interfaces, workload " + "partitions, constants, SPEC, and fixture before --refresh" + ), + } + + +def write_inventory(path: Path, meta: dict[str, Any], records: list[dict[str, Any]]) -> None: + path.parent.mkdir(parents=True, exist_ok=True) + with path.open("w", encoding="utf-8") as stream: + for row in [meta, *records]: + stream.write(json.dumps(row, sort_keys=True, separators=(",", ":"))) + stream.write("\n") + + +def read_inventory(path: Path) -> tuple[dict[str, Any], list[dict[str, Any]]]: + rows: list[dict[str, Any]] = [] + with path.open(encoding="utf-8") as stream: + for line_no, line in enumerate(stream, 1): + try: + row = json.loads(line) + except json.JSONDecodeError as exc: + raise InventoryError(f"{path}:{line_no}: invalid JSON: {exc}") from exc + if not isinstance(row, dict): + raise InventoryError(f"{path}:{line_no}: inventory row must be an object") + rows.append(row) + if not rows or rows[0].get("kind") != "meta": + raise InventoryError("inventory must start with one meta row") + return rows[0], rows[1:] + + +def migration_statuses(record: dict[str, Any]) -> Iterable[str]: + migration = record.get("migration") + if migration and migration.get("status") not in {"not-a-call", "inventory-only"}: + yield migration.get("status", "") + + +def require_migrations(records: list[dict[str, Any]]) -> None: + for index, record in enumerate(records): + migration = record.get("migration") + if not isinstance(migration, dict): + raise InventoryError(f"record {index}: migration must be an object") + status = migration.get("status") + raw_tactic = record.get("kind") == "tactic-occurrence" and not record.get("actual") + audit_reference = record.get("kind") == "leancert-reference" + if raw_tactic: + if status != "not-a-call": + raise InventoryError( + f"record {index}: non-executable textual occurrence must be not-a-call" + ) + elif audit_reference: + if status != "inventory-only": + raise InventoryError( + f"record {index}: lexical reference must be inventory-only" + ) + expected_provenance = reference_interfaces(record.get("symbol", "")) + if record.get("interface_provenance") != expected_provenance: + raise InventoryError( + f"record {index}: lexical reference provenance drifted" + ) + elif status not in CLASSIFICATIONS: + raise InventoryError( + f"record {index}: executable/imported record has invalid migration {status!r}" + ) + else: + note = migration.get("note") + if not isinstance(note, str) or not note.strip(): + raise InventoryError(f"record {index}: migration requires a nonempty note") + if status == "pending": + continue + evidence = migration.get("evidence") + if not isinstance(evidence, list) or not evidence or not all( + isinstance(item, str) and item.strip() for item in evidence + ): + raise InventoryError( + f"record {index}: {status} requires nonempty evidence entries" + ) + if status == "accepted-after-rewrite": + if not isinstance(migration.get("rewrite"), str) \ + or not migration["rewrite"].strip(): + raise InventoryError( + f"record {index}: accepted-after-rewrite requires rewrite and evidence" + ) + elif status == "replaced-by-stronger-result": + replacement = migration.get("replacement") + if not isinstance(replacement, str) or not replacement.strip(): + raise InventoryError( + f"record {index}: replacement theorem/result is required" + ) + elif status == "retained-other-dependency": + dependency = migration.get("dependency") + if not isinstance(dependency, str) or not dependency.strip(): + raise InventoryError( + f"record {index}: retained dependency is required" + ) + + +def validate_inventory( + meta: dict[str, Any], records: list[dict[str, Any]], + require_classified: bool, require_record_digest: bool = True, +) -> None: + if meta.get("format") != FORMAT_VERSION: + raise InventoryError(f"unsupported inventory format {meta.get('format')}") + require_pins(meta.get("pins", {})) + if meta.get("lean_source_digest") != PNT_LEAN_SOURCE_DIGEST: + raise InventoryError("inventory Lean-source digest does not match the pinned PNT+ tree") + if meta.get("lean_source_files") != PNT_LEAN_SOURCE_FILES: + raise InventoryError("inventory Lean-source file count does not match the pinned PNT+ tree") + if meta.get("audit_record_digest") != PNT_AUDIT_RECORD_DIGEST: + raise InventoryError( + "inventory audit-record digest does not match the pinned audit surface: " + f"expected {PNT_AUDIT_RECORD_DIGEST}, got {meta.get('audit_record_digest')}" + ) + if records != sorted(records, key=record_sort_key): + raise InventoryError("inventory records are not in canonical order") + if require_record_digest and meta.get("record_digest") != record_digest(records): + raise InventoryError("inventory record digest does not match contents") + if meta.get("audit_record_digest") != audit_record_digest(records): + raise InventoryError("inventory audit-record digest does not match record contents") + require_migrations(records) + counts = summarize(records) + require_workload_partitions(records) + if meta.get("counts") != counts: + raise InventoryError(f"inventory counts disagree: {meta.get('counts')} != {counts}") + for name, expected in EXPECTED.items(): + if counts.get(name) != expected: + raise InventoryError(f"{name}: expected {expected}, got {counts.get(name)}") + + statuses = Counter(status for row in records for status in migration_statuses(row)) + unknown = set(statuses) - CLASSIFICATIONS + if unknown: + raise InventoryError(f"unknown migration classifications: {sorted(unknown)}") + if require_classified and statuses["pending"]: + raise InventoryError( + f"migration inventory still has {statuses['pending']} pending decisions" + ) + + +def check_inventory(path: Path, require_classified: bool) -> None: + meta, records = read_inventory(path) + validate_inventory(meta, records, require_classified) + + +def update_classifications(path: Path) -> None: + meta, records = read_inventory(path) + validate_inventory(meta, records, require_classified=False, require_record_digest=False) + meta["record_digest"] = record_digest(records) + validate_inventory(meta, records, require_classified=False) + write_inventory(path, meta, records) + + +def require_source_match( + committed_meta: dict[str, Any], committed_records: list[dict[str, Any]], + generated_meta: dict[str, Any], generated_records: list[dict[str, Any]], +) -> None: + fixed_meta = { + "kind", "format", "pins", "lean_source_digest", "lean_source_files", + "audit_record_digest", "counts", + } + if any(committed_meta.get(key) != generated_meta.get(key) for key in fixed_meta) \ + or audit_records(committed_records) != audit_records(generated_records): + raise InventoryError("committed inventory differs from pinned source regeneration") + + +def default_fixture() -> Path: + return Path(__file__).resolve().parents[2] / ( + "conformance-fixtures/HexIntervalMathlib/pnt-inventory.jsonl" + ) + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + mode = parser.add_mutually_exclusive_group(required=True) + mode.add_argument("--refresh", action="store_true", help="regenerate from --source") + mode.add_argument("--verify-source", action="store_true", + help="regenerate from --source and compare with --output") + mode.add_argument("--check", action="store_true", + help="validate the committed fixture without network/source access") + mode.add_argument( + "--update-classifications", action="store_true", + help="validate edited migration fields and refresh only the record digest", + ) + mode.add_argument( + "--inspect-source", action="store_true", + help="print observed pin/count inputs without accepting or writing them", + ) + parser.add_argument("--source", type=Path, + help="exact PrimeNumberTheoremAnd checkout for refresh/verify") + parser.add_argument("--output", type=Path, default=default_fixture()) + parser.add_argument("--require-classified", action="store_true", + help="reject pending migration decisions") + args = parser.parse_args() + + try: + if args.require_classified and not args.check: + parser.error("--require-classified is valid only with --check") + if args.check: + check_inventory(args.output, args.require_classified) + print(f"pnt inventory: {args.output} is valid") + return 0 + if args.update_classifications: + update_classifications(args.output) + print(f"pnt inventory: validated classifications in {args.output}") + return 0 + if args.source is None: + parser.error("--source is required with source-reading modes") + if args.inspect_source: + print(json.dumps(inspect_source(args.source.resolve()), indent=2, sort_keys=True)) + return 0 + meta, records = generate(args.source.resolve()) + if args.refresh: + carried = 0 + removed = 0 + if args.output.exists(): + _, previous = read_inventory(args.output) + records, carried, removed = carry_migrations(previous, records) + meta["record_digest"] = record_digest(records) + validate_inventory(meta, records, require_classified=False) + write_inventory(args.output, meta, records) + print( + f"pnt inventory: wrote {len(records)} records to {args.output}; " + f"carried {carried} migration decisions, removed {removed} pending/raw records" + ) + return 0 + committed_meta, committed_records = read_inventory(args.output) + validate_inventory(committed_meta, committed_records, require_classified=False) + require_source_match(committed_meta, committed_records, meta, records) + print(f"pnt inventory: {args.output} matches {args.source}") + return 0 + except (InventoryError, OSError, KeyError, TypeError, ValueError) as exc: + print(f"error: {exc}", file=sys.stderr) + return 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/maintenance/test_pnt_inventory.py b/scripts/maintenance/test_pnt_inventory.py new file mode 100644 index 000000000..8301678dc --- /dev/null +++ b/scripts/maintenance/test_pnt_inventory.py @@ -0,0 +1,274 @@ +#!/usr/bin/env python3 +"""Unit tests for the source-pinned PNT+ migration inventory.""" + +import copy +import json +import tempfile +import unittest +from pathlib import Path + +from scripts.maintenance import pnt_inventory as inventory + + +class MaskLeanTests(unittest.TestCase): + def test_masks_comments_and_strings_but_not_identifiers(self) -> None: + source = """theorem check' : True := by + interval_decide + -- interval_decide + /- outer interval_auto /- nested interval_decide -/ done -/ + let s := "interval_auto" + let c := 'x' + let escaped := '\\x41' + let quote := '\\"' + interval_auto +""" + masked = inventory.mask_lean(source) + + self.assertIn("check'", masked) + self.assertEqual(len(source), len(masked)) + self.assertEqual(source.count("\n"), masked.count("\n")) + self.assertEqual(len(list(inventory.TOKEN_RE["interval_decide"].finditer(masked))), 1) + self.assertEqual(len(list(inventory.TOKEN_RE["interval_auto"].finditer(masked))), 1) + self.assertEqual( + len(list(inventory.TOKEN_RE["interval_decide"].finditer("interval_decide'"))), + 0, + ) + + def test_rejects_unterminated_comment_and_string(self) -> None: + with self.assertRaisesRegex(inventory.InventoryError, "block comment"): + inventory.mask_lean("/- unfinished") + with self.assertRaisesRegex(inventory.InventoryError, "string literal"): + inventory.mask_lean('"unfinished') + + def test_masks_escaped_single_quote_character(self) -> None: + literal = r"'\''" + self.assertEqual(inventory.char_literal_end(literal, 0), len(literal)) + masked = inventory.mask_lean(f"let apostrophe := {literal}\ninterval_auto\n") + self.assertEqual(len(list(inventory.TOKEN_RE["interval_auto"].finditer(masked))), 1) + + def test_escaped_character_cannot_consume_a_newline(self) -> None: + source = "let broken := '\\\ninterval_auto\n'\n" + masked = inventory.mask_lean(source) + self.assertEqual(source.count("\n"), masked.count("\n")) + self.assertEqual(len(list(inventory.TOKEN_RE["interval_auto"].finditer(masked))), 1) + + def test_table_rows_include_first_tuple_on_opening_line(self) -> None: + source = ( + "noncomputable def table_12_aux := [(0, 0)]\n" + "noncomputable def table_12 := [(1, f (2)),\n (3, 4)]\n" + "def later := []\n" + ) + rows = inventory.table_rows(inventory.mask_lean(source), "table_12") + self.assertEqual(rows, ["(1, f (2))", "(3, 4)"]) + + def test_declaration_map_tracks_enclosing_declaration(self) -> None: + masked = inventory.mask_lean( + "theorem first : True := by\n trivial\n\nexample : True := by\n trivial\n" + ) + declarations = inventory.declaration_map(masked) + self.assertEqual(declarations[1], "first") + self.assertEqual(declarations[4], "example@4") + + +class InventoryTests(unittest.TestCase): + @classmethod + def setUpClass(cls) -> None: + cls.fixture = inventory.default_fixture() + cls.meta, cls.records = inventory.read_inventory(cls.fixture) + + def write_rows(self, meta: dict, records: list[dict]) -> Path: + directory = tempfile.TemporaryDirectory() + self.addCleanup(directory.cleanup) + path = Path(directory.name) / "inventory.jsonl" + inventory.write_inventory(path, meta, records) + return path + + def test_committed_inventory_is_valid_but_not_yet_classified(self) -> None: + inventory.check_inventory(self.fixture, require_classified=False) + with self.assertRaisesRegex(inventory.InventoryError, "pending decisions"): + inventory.check_inventory(self.fixture, require_classified=True) + + def test_classification_edits_do_not_change_audit_identity(self) -> None: + meta = copy.deepcopy(self.meta) + records = copy.deepcopy(self.records) + row = next(row for row in records if row.get("migration", {}).get("status") == "pending") + row["migration"] = { + "status": "accepted-after-rewrite", + "note": "unit-test classification", + "rewrite": "factor the repeated bound through one shared theorem", + "evidence": ["conformance/HexIntervalMathlib/PNTConformance.lean:example"], + } + path = self.write_rows(meta, records) + inventory.update_classifications(path) + inventory.check_inventory(path, require_classified=False) + + def test_source_verification_ignores_valid_migration_edits(self) -> None: + committed_meta = copy.deepcopy(self.meta) + committed_records = copy.deepcopy(self.records) + generated_meta = copy.deepcopy(self.meta) + generated_records = copy.deepcopy(self.records) + row = next( + row for row in committed_records + if row.get("migration", {}).get("status") == "pending" + ) + row["migration"]["note"] = "classification work may change this note" + committed_meta["record_digest"] = inventory.record_digest(committed_records) + inventory.require_source_match( + committed_meta, committed_records, generated_meta, generated_records, + ) + + def test_refresh_carries_classifications_by_audit_identity(self) -> None: + previous = copy.deepcopy(self.records) + generated = copy.deepcopy(self.records) + previous[0]["migration"]["note"] = "preserved migration note" + carried_records, carried, removed = inventory.carry_migrations(previous, generated) + expected_carried = sum( + row["migration"]["status"] not in {"not-a-call", "inventory-only"} + for row in self.records + ) + self.assertEqual((carried, removed), (expected_carried, 0)) + self.assertEqual(carried_records[0]["migration"]["note"], "preserved migration note") + + def test_refresh_does_not_report_fixed_audit_labels_as_carried(self) -> None: + previous = [{"kind": "leancert-reference", "migration": inventory.inventory_only()}] + generated = copy.deepcopy(previous) + _, carried, removed = inventory.carry_migrations(previous, generated) + self.assertEqual((carried, removed), (0, 0)) + + def test_refresh_refuses_to_drop_classified_record(self) -> None: + previous = copy.deepcopy(self.records[:1]) + previous[0]["migration"] = { + "status": "accepted-unchanged", + "note": "classified", + "evidence": ["HexIntervalMathlib.PNT.example"], + } + with self.assertRaisesRegex(inventory.InventoryError, "discard 1 classified"): + inventory.carry_migrations(previous, []) + + def test_source_field_tamper_is_rejected_even_with_updated_record_digest(self) -> None: + meta = copy.deepcopy(self.meta) + records = copy.deepcopy(self.records) + row = next(row for row in records if "path" in row) + row["path"] += ".tampered" + records.sort(key=inventory.record_sort_key) + meta["record_digest"] = inventory.record_digest(records) + meta["counts"] = inventory.summarize(records) + path = self.write_rows(meta, records) + with self.assertRaisesRegex(inventory.InventoryError, "audit-record digest"): + inventory.check_inventory(path, require_classified=False) + + def test_noncanonical_order_is_rejected(self) -> None: + meta = copy.deepcopy(self.meta) + records = copy.deepcopy(self.records) + records[0], records[1] = records[1], records[0] + meta["record_digest"] = inventory.record_digest(records) + path = self.write_rows(meta, records) + with self.assertRaisesRegex(inventory.InventoryError, "canonical order"): + inventory.check_inventory(path, require_classified=False) + + def test_missing_migration_classification_is_rejected(self) -> None: + meta = copy.deepcopy(self.meta) + records = copy.deepcopy(self.records) + row = next(row for row in records if row.get("migration", {}).get("status") == "pending") + row.pop("migration") + meta["record_digest"] = inventory.record_digest(records) + path = self.write_rows(meta, records) + with self.assertRaisesRegex(inventory.InventoryError, "migration must be an object"): + inventory.check_inventory(path, require_classified=False) + + def test_malformed_migration_is_reported_as_inventory_error(self) -> None: + record = {"kind": "dependency-interface", "migration": "pending"} + with self.assertRaisesRegex(inventory.InventoryError, "migration must be an object"): + inventory.require_migrations([record]) + + def test_lexical_reference_is_audit_evidence_not_release_obligation(self) -> None: + record = { + "kind": "leancert-reference", + "symbol": "LeanCert.Core", + "interface_provenance": [ + "LeanCert.ANT", "LeanCert.Validity.AffineCover", + ], + "migration": inventory.inventory_only(), + } + inventory.require_migrations([record]) + self.assertEqual(list(inventory.migration_statuses(record)), []) + + def test_unowned_lexical_reference_is_rejected(self) -> None: + with self.assertRaisesRegex(inventory.InventoryError, "lacks interface provenance"): + inventory.reference_interfaces("LeanCert.Unreviewed.API") + + def test_finished_classification_requires_structured_evidence(self) -> None: + record = { + "kind": "dependency-interface", + "migration": { + "status": "replaced-by-stronger-result", + "note": "ported", + "evidence": ["HexIntervalMathlib.PNT.bklnwBounds"], + }, + } + with self.assertRaisesRegex(inventory.InventoryError, "replacement theorem"): + inventory.require_migrations([record]) + record["migration"]["replacement"] = "PNT.Hex.bklnwBounds" + inventory.require_migrations([record]) + + def test_dependency_surface_must_match_all_six_interfaces(self) -> None: + imports = [ + {"module": module, "path": "X.lean", "line": index + 1} + for index, module in enumerate(inventory.DEPENDENCY_INTERFACES) + ] + rows = inventory.dependency_records(imports) + self.assertEqual({row["module"] for row in rows}, set(inventory.DEPENDENCY_INTERFACES)) + with self.assertRaisesRegex(inventory.InventoryError, "import surface drifted"): + inventory.dependency_records(imports[:-1]) + + def test_fks2_family_has_exact_shard_partition(self) -> None: + family = next( + row for row in self.records + if row.get("kind") == "generated-family" + and row.get("family") == "fks2-table4ext" + ) + sizes = sorted(shard["cells"] for shard in family["shards"]) + self.assertEqual(sizes, [590] + [1000] * 13) + self.assertEqual(sum(sizes), 13590) + + def test_bklnw_generated_families_expand_outer_source_forms(self) -> None: + families = { + row["family"]: row for row in self.records + if row.get("kind") == "generated-family" + } + table10 = families["bklnw-table10-source-sites"] + self.assertEqual(table10["target_check_sites"], 87) + self.assertEqual(table10["supporting_a2_check_sites"], 38) + table12 = families["bklnw-table12-cells"] + self.assertEqual( + (table12["rows"], table12["ordinary_rows"], table12["logarithmic_rows"]), + (26, 24, 2), + ) + self.assertEqual(table12["checks_per_row"], 5) + self.assertEqual(table12["expanded_checks"], 130) + self.assertEqual(len(table12["false_original_boundary_rows"]), 4) + + def test_headline_source_counts_are_pinned_independently(self) -> None: + self.assertEqual(self.meta["lean_source_files"], 232) + self.assertEqual(self.meta["counts"], { + "bklnw_table10_a2_sites": 38, + "bklnw_table10_target_sites": 87, + "bklnw_table12_checks": 130, + "bklnw_table12_logarithmic_rows": 2, + "bklnw_table12_ordinary_rows": 24, + "dependency_interface": 6, + "fks2_cells": 13590, + "fks2_shards": 14, + "interval_auto_actual": 60, + "interval_auto_textual": 61, + "interval_decide_actual": 280, + "interval_decide_textual": 290, + "leancert_import": 16, + "leancert_reference": 107, + "native_decide_actual": 83, + "records": 567, + }) + + +if __name__ == "__main__": + unittest.main()