Repository navigation
Import Pure Nock semantics, trace certificates and fingerprints - #623
Merged
Merged
Conversation
Collaborator
Author
|
Separate thorough review of {
"review": "Separate acquisition-agent thorough review",
"head": "ba2297df4eccade3f06a1a04d56e7d9aa82c9c0d",
"conclusion": "approve",
"merge_eligibility": "Pending current-head CI, GPT and Greptile; no merge or auto-merge has been requested.",
"coverage": "All 23 upstream release modules, imported dependency closure, all seven card headlines, representative proof and implementation chunks in every file, all port/refactoring edits, entry card and generated imports; no approval from an elided diff.",
"faithfulness": {
"verdict": "pass",
"bottom_line": "The card accurately scopes evaluator equivalence, trace certification, crash completeness and fingerprint collision bounds.",
"proves_the_claim": "proves_it",
"claim_note": "The modular bridge requires bounded natural-number nouns and a successful guarded execution; collision distinctness concerns field-valued data.",
"assumed_inputs": "Generic field/finiteness instances, length bounds and distinct field coefficient data for collisions; modulus greater than one, bounded inputs and guarded success for the bridge. These are disclosed.",
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "No duplicate Nock formalization was found in the pool, Mathlib or TauCeti.",
"already_formalized": "",
"novelty_note": "Mathlib binary-tree/Catalan and polynomial root-counting infrastructure is reused; the Nock machine, evaluator simulation, crash/trace certificates and guarded bridges are new to the searched collections.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "This is a completed semantics and verification theory with machine adequacy and executable certificate endpoints.",
"fit": "good_fit",
"level": "research",
"branch": "operational semantics and verifiable computation",
"mode": "theory_building",
"significance_one_sentence": "It preserves a reusable foundation for relating Nock execution to checkable traces and algebraic fingerprints.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "The pinned public release and bundled manuscript support the imported scope, with representation differences explicitly labelled.",
"source_match": "matches",
"findings": []
},
"quality": {
"verdict": "pass",
"bottom_line": "Competent explicit simulation and cost proofs, with bounded helper lemmas and measured simplification improvements.",
"code_quality": 3,
"findings": []
},
"source_audit": [
"Apache-2.0 LICENSE and collective NOTICE verified; public release/tag timestamp lies inside the exact eligible interval.",
"Initial source commit credits Akis, whose identity matches the cited manuscript contributor; collective attribution is retained.",
"Provenance human follows the checked-in absence-of-credible-AI-evidence rubric, with its evidential limitation disclosed.",
"Paper OP0\u201310, separate OP11 hints, guarded modular sublanguage, natural leaf casts, corrected Dyck exponents and the shared-randomness union bound were checked against actual definitions, theorem types and manuscript passages.",
"No claim to full zkVM/AIR/RAP/table security, arbitrary base-field embeddings or Goldilocks primality."
],
"engineering_audit": [
"Lean 4.35.0-rc3 and pinned Mathlib c55e6e786f49471c72fbddbec5415808896aec1e; content-only clean branch and fixed LeanPool.lean.",
"Final clean 25-module build: zero warnings; 39.92s baseline to 29.69s final wall time with warm dependencies and LEAN_NUM_THREADS=4.",
"574 public declarations passed axiom closure; every owned compiled declaration passed the option/trust backdoor audit.",
"All seven headlines resolve; 15 slow linters pass on 3566 compiled declarations; style, generated index and full static quality pass.",
"Synchronous profiles show den_succ 5974487 to 2403278 and denP_succ 8527592 to 2428273 raw ticks. Opcode extraction costs were considered together with their new helpers. A measured regression was reverted.",
"No custom axiom, sorry/admit, prohibited evaluation mechanism, resource override, linter waiver or policy modification."
],
"ci_observation": "At review time the PR checks are queued and Greptile is running. Full CI success is not inferred from local checks.",
"unresolved_material_findings": []
} |
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Low impact] No blocking finding remains from this review; external source and provenance checks remain unverified. SummaryImports Pure Nock semantics, trace certificates, guarded modular bridges, and finite-field fingerprints. Since the previous review, only the trace headline and its theorem description changed.
Reviews (3) · Last reviewed commit: "Correct the trace certificate headline a..." · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
Collaborator
Author
|
/review |
Collaborator
Author
|
Updated separate thorough review of {
"review": "Separate acquisition-agent thorough review",
"head": "bafd5a4299eb048846376c813aa6e294e214f205",
"conclusion": "approve",
"merge_eligibility": "Pending current-head CI, GPT and Greptile; no merge or auto-merge has been requested.",
"coverage": "All 23 upstream release modules, imported dependency closure, all seven card headlines, representative proof and implementation chunks in every file, all port/refactoring edits, entry card and generated imports; no approval from an elided diff.",
"faithfulness": {
"verdict": "pass",
"bottom_line": "The card accurately scopes evaluator equivalence, trace certification, crash completeness and fingerprint collision bounds.",
"proves_the_claim": "proves_it",
"claim_note": "The modular bridge requires bounded natural-number nouns and a successful guarded execution; collision distinctness concerns field-valued data.",
"assumed_inputs": "Generic field/finiteness instances, length bounds and distinct field coefficient data for collisions; modulus greater than one, bounded inputs and guarded success for the bridge. These are disclosed.",
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "No duplicate Nock formalization was found in the pool, Mathlib or TauCeti.",
"already_formalized": "",
"novelty_note": "Mathlib binary-tree/Catalan and polynomial root-counting infrastructure is reused; the Nock machine, evaluator simulation, crash/trace certificates and guarded bridges are new to the searched collections.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "This is a completed semantics and verification theory with machine adequacy and executable certificate endpoints.",
"fit": "good_fit",
"level": "research",
"branch": "operational semantics and verifiable computation",
"mode": "theory_building",
"significance_one_sentence": "It preserves a reusable foundation for relating Nock execution to checkable traces and algebraic fingerprints.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "The pinned public release and bundled manuscript support the imported scope, with representation differences explicitly labelled.",
"source_match": "matches",
"findings": []
},
"quality": {
"verdict": "pass",
"bottom_line": "Competent explicit simulation and cost proofs, with bounded helper lemmas and measured simplification improvements.",
"code_quality": 3,
"findings": []
},
"source_audit": [
"Apache-2.0 LICENSE and collective NOTICE verified; public release/tag timestamp lies inside the exact eligible interval.",
"Initial source commit credits Akis, whose identity matches the cited manuscript contributor; collective attribution is retained.",
"Provenance human follows the checked-in absence-of-credible-AI-evidence rubric, with its evidential limitation disclosed.",
"Paper OP0\u201310, separate OP11 hints, guarded modular sublanguage, natural leaf casts, corrected Dyck exponents and the shared-randomness union bound were checked against actual definitions, theorem types and manuscript passages.",
"No claim to full zkVM/AIR/RAP/table security, arbitrary base-field embeddings or Goldilocks primality."
],
"engineering_audit": [
"Lean 4.35.0-rc3 and pinned Mathlib c55e6e786f49471c72fbddbec5415808896aec1e; content-only clean branch and fixed LeanPool.lean.",
"Final clean 25-module build: zero warnings; 39.92s baseline to 29.69s final wall time with warm dependencies and LEAN_NUM_THREADS=4.",
"574 public declarations passed axiom closure; every owned compiled declaration passed the option/trust backdoor audit.",
"All seven headlines resolve; 15 slow linters pass on 3566 compiled declarations; style, generated index and full static quality pass.",
"Synchronous profiles show den_succ 5974487 to 2403278 and denP_succ 8527592 to 2428273 raw ticks. Opcode extraction costs were considered together with their new helpers. A measured regression was reverted.",
"No custom axiom, sorry/admit, prohibited evaluation mechanism, resource override, linter waiver or policy modification.",
"The repaired head independently reproduced the 29.69s clean wall measurement; user 72.12s, system 8.86s, max RSS 1141320 KiB."
],
"ci_observation": "Current-head GitHub checks remain queued without an assigned runner; Greptile reruns for this head. Explicit /review requested the configured GPT worker. None of these pending external checks is counted as green.",
"unresolved_material_findings": [],
"previous_review_head": "ba2297df4eccade3f06a1a04d56e7d9aa82c9c0d",
"review_update": "Horner computation generalized to Semiring after Greptile advisory; final-head kernel build, all linters, style, index and trust audits repeated successfully. Separate evaluator references retained with explicit architectural rationale; this remains subject to independent review."
} |
Collaborator
Author
|
Updated separate thorough review of {
"review": "Separate acquisition-agent thorough review",
"head": "b21340222b0d340dcc5975a2091225dcbce7b007",
"conclusion": "approve",
"merge_eligibility": "Pending current-head CI, GPT and Greptile; no merge or auto-merge has been requested.",
"coverage": "All 23 upstream release modules, imported dependency closure, all seven card headlines, representative proof and implementation chunks in every file, all port/refactoring edits, entry card and generated imports; no approval from an elided diff.",
"faithfulness": {
"verdict": "pass",
"bottom_line": "The card accurately scopes evaluator equivalence, trace certification, crash completeness and fingerprint collision bounds.",
"proves_the_claim": "proves_it",
"claim_note": "The modular bridge requires bounded natural-number nouns and a successful guarded execution; collision distinctness concerns field-valued data. Trace completion distinguishes terminal state recognition from checker acceptance of the final crash edge.",
"assumed_inputs": "Generic field/finiteness instances, length bounds and distinct field coefficient data for collisions; modulus greater than one, bounded inputs and guarded success for the bridge. These are disclosed.",
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "No duplicate Nock formalization was found in the pool, Mathlib or TauCeti.",
"already_formalized": "",
"novelty_note": "Mathlib binary-tree/Catalan and polynomial root-counting infrastructure is reused; the Nock machine, evaluator simulation, crash/trace certificates and guarded bridges are new to the searched collections.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "This is a completed semantics and verification theory with machine adequacy and executable certificate endpoints.",
"fit": "good_fit",
"level": "research",
"branch": "operational semantics and verifiable computation",
"mode": "theory_building",
"significance_one_sentence": "It preserves a reusable foundation for relating Nock execution to checkable traces and algebraic fingerprints.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "The pinned public release and bundled manuscript support the imported scope, with representation differences explicitly labelled.",
"source_match": "matches",
"findings": []
},
"quality": {
"verdict": "pass",
"bottom_line": "Competent explicit simulation and cost proofs, with bounded helper lemmas and measured simplification improvements.",
"code_quality": 3,
"findings": []
},
"source_audit": [
"Apache-2.0 LICENSE and collective NOTICE verified; public release/tag timestamp lies inside the exact eligible interval.",
"Initial source commit credits Akis, whose identity matches the cited manuscript contributor; collective attribution is retained.",
"Provenance human follows the checked-in absence-of-credible-AI-evidence rubric, with its evidential limitation disclosed.",
"Paper OP0\u201310, separate OP11 hints, guarded modular sublanguage, natural leaf casts, corrected Dyck exponents and the shared-randomness union bound were checked against actual definitions, theorem types and manuscript passages.",
"No claim to full zkVM/AIR/RAP/table security, arbitrary base-field embeddings or Goldilocks primality."
],
"engineering_audit": [
"Lean 4.35.0-rc3 and pinned Mathlib c55e6e786f49471c72fbddbec5415808896aec1e; content-only clean branch and fixed LeanPool.lean.",
"Optimized clean 25-module build at bafd5a429: zero warnings; 39.92s baseline to 29.69s final wall time with warm dependencies and LEAN_NUM_THREADS=4.",
"574 public declarations passed axiom closure; every owned compiled declaration passed the option/trust backdoor audit.",
"All seven headlines resolve; 15 slow linters pass on 3566 compiled declarations; style, generated index and full static quality pass.",
"Synchronous profiles show den_succ 5974487 to 2403278 and denP_succ 8527592 to 2428273 raw ticks. Opcode extraction costs were considered together with their new helpers. A measured regression was reverted.",
"No custom axiom, sorry/admit, prohibited evaluation mechanism, resource override, linter waiver or policy modification.",
"The Horner-repaired head independently reproduced the 29.69s clean wall measurement; user 72.12s, system 8.86s, max RSS 1141320 KiB.",
"Current b21340222 only corrects a docstring and card prose; its incremental project build and full owned declaration/compiled trust, linters, style and index checks pass. Compile profiles remain those of identical proof bodies."
],
"ci_observation": "Current-head CI remains queued; Greptile reruns for this head. Explicit /review requested configured GPT review; no result yet. Pending checks are not counted as passing.",
"unresolved_material_findings": [],
"previous_review_head": "bafd5a4299eb048846376c813aa6e294e214f205",
"review_update": "Greptile identified an overstatement missed by the previous review: the final trace state is terminal or has a checker-accepted crash edge. The card and inherited docstring are corrected; theorem and proof unchanged. All seven headlines were rechecked against actual types, and local build, all linters, style, index and trust audits passed. Horner semiring generalization retained. Greptile conceded the separate-reference-pipeline architectural rationale."
} |
Collaborator
Author
|
Current-head checkpoint: Lean CI remains pending without its first check run, and the five visible workflow jobs remain queued. The explicit GPT request has not produced a result. These external prerequisites are not counted as passing. Some workflow-detail REST endpoints are rate-limited until 2026-10-09T11:55:43Z; PR GraphQL status remains readable. No queue entry or auto-merge is enabled. |
Contributor
Proof profile (new / modified Lean files)
This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 529,564 maxHeartbeats units across 25 valid files (11,596 added LOC). Sum of Count-heartbeats wall-clock total: 141.35 s. Repeated import cost inside Heartbeat values sum disjoint root command traces with LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.PureNock.ModularEval |
10.00 s |
LeanPool.PureNock.PureCompleteHint |
8.90 s |
LeanPool.PureNock.PureAgreement |
6.90 s |
LeanPool.PureNock.Dyck |
5.00 s |
LeanPool.PureNock.NounValidation |
4.70 s |
LeanPool.PureNock.Agreement |
4.60 s |
LeanPool.PureNock.PaperFieldBridge |
4.50 s |
LeanPool.PureNock.PureComplete |
4.40 s |
LeanPool.PureNock.NPR |
4.20 s |
LeanPool.PureNock.PaperReference |
4.10 s |
LeanPool.PureNock.PaperReferenceMod |
3.80 s |
LeanPool.PureNock.Semantics |
3.30 s |
Per-file `lean --profile` output
LeanPool/PureNock.lean
import took 1.34s
cumulative profiling times:
elaboration 0.59ms
import 1.34s
initialization 33.9ms
interpretation 134ms
linting 0.705ms
module linting 0.00199ms
overlappingInstancesLinter 0.896ms
parsing 0.0736ms
tacticAnalysis 4.93ms
real 2.01
user 0.80
sys 0.57
LeanPool/PureNock/Agreement.lean
import took 135ms
tactic execution of Lean.Parser.Tactic.simp took 190ms
simp took 104ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 171ms
cumulative profiling times:
attribute application 3.33ms
blocked (unaccounted) 6.7s
compilation (IR) 4.24ms
compilation (LCNF base) 26.2ms
compilation (LCNF impure) 23.6ms
compilation (LCNF mono) 30.2ms
congr simp thm 25.7ms
elaboration 283ms
fix level params 6.55ms
import 135ms
initialization 45.8ms
instantiate metavars 55.6ms
interpretation 2.8ms
let-to-have transformation 14.2ms
linting 126ms
module linting 0.00175ms
parsing 84.2ms
process pre-definitions 126ms
share common exprs 47.7ms
simp 1.72s
tactic execution 3.13s
type checking 664ms
typeclass inference 233ms
real 2.67
user 5.74
sys 0.57
LeanPool/PureNock/Determinism.lean
import took 515ms
cumulative profiling times:
attribute application 0.0457ms
elaboration 9.05ms
fix level params 0.0485ms
import 515ms
initialization 33.4ms
instantiate metavars 0.123ms
interpretation 143ms
let-to-have transformation 0.0511ms
linting 4.65ms
module linting 0.00193ms
overlappingInstancesLinter 1.75ms
parsing 2.69ms
process pre-definitions 0.512ms
share common exprs 0.216ms
tactic execution 4.03ms
tacticAnalysis 8.39ms
type checking 0.908ms
real 1.17
user 0.72
sys 0.50
LeanPool/PureNock/Dyck.lean
import took 491ms
cumulative profiling times:
attribute application 1.11ms
blocked (unaccounted) 96.9ms
compilation (IR) 1.22ms
compilation (LCNF base) 9.96ms
compilation (LCNF impure) 5.95ms
compilation (LCNF mono) 8.04ms
congr simp thm 3.95ms
elaboration 82ms
fix level params 0.56ms
import 491ms
initialization 33.9ms
instantiate metavars 1.74ms
interpretation 280ms
let-to-have transformation 0.711ms
linting 26ms
module linting 0.00183ms
overlappingInstancesLinter 6.97ms
parsing 15.2ms
process pre-definitions 27.4ms
share common exprs 3.51ms
simp 138ms
tactic execution 292ms
tacticAnalysis 43.9ms
type checking 150ms
typeclass inference 113ms
real 1.55
user 1.75
sys 0.53
LeanPool/PureNock/Fingerprint.lean
import took 596ms
cumulative profiling times:
attribute application 0.0487ms
compilation (IR) 0.204ms
compilation (LCNF base) 3.06ms
compilation (LCNF impure) 0.995ms
compilation (LCNF mono) 2.81ms
congr simp thm 0.883ms
elaboration 10.5ms
fix level params 0.165ms
import 596ms
initialization 33.8ms
instantiate metavars 0.077ms
interpretation 164ms
let-to-have transformation 0.0549ms
linting 4.8ms
module linting 0.00186ms
overlappingInstancesLinter 5.74ms
parsing 2.39ms
process pre-definitions 3.6ms
share common exprs 0.36ms
simp 12.2ms
tactic execution 17.7ms
tacticAnalysis 8.48ms
type checking 3.22ms
typeclass inference 4.22ms
real 1.30
user 0.89
sys 0.50
LeanPool/PureNock/FingerprintLayer.lean
import took 596ms
cumulative profiling times:
elaboration 0.242ms
import 596ms
initialization 33.5ms
interpretation 126ms
linting 0.713ms
module linting 0.00186ms
overlappingInstancesLinter 0.644ms
parsing 0.499ms
tacticAnalysis 1.78ms
real 1.25
user 0.75
sys 0.52
LeanPool/PureNock/Imports.lean
import took 598ms
cumulative profiling times:
elaboration 0.0813ms
import 598ms
initialization 33.5ms
interpretation 111ms
linting 0.23ms
module linting 0.00213ms
overlappingInstancesLinter 0.0983ms
parsing 0.00247ms
tacticAnalysis 0.384ms
real 1.25
user 0.76
sys 0.49
LeanPool/PureNock/Language.lean
import took 486ms
cumulative profiling times:
elaboration 0.246ms
import 486ms
initialization 33.8ms
interpretation 118ms
linting 0.987ms
module linting 0.00182ms
overlappingInstancesLinter 0.681ms
parsing 0.243ms
tacticAnalysis 4.4ms
real 1.13
user 0.68
sys 0.46
LeanPool/PureNock/Modular.lean
import took 537ms
cumulative profiling times:
elaboration 0.43ms
import 537ms
initialization 42.6ms
interpretation 122ms
linting 1.07ms
module linting 0.00224ms
overlappingInstancesLinter 0.852ms
parsing 0.283ms
tacticAnalysis 1.57ms
real 1.19
user 0.70
sys 0.51
LeanPool/PureNock/ModularEval.lean
import took 501ms
tactic execution of Lean.Parser.Tactic.simp took 217ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
tactic execution of Lean.Parser.Tactic.simp took 138ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
tactic execution of Lean.Parser.Tactic.simp took 147ms
tactic execution of Lean.Parser.Tactic.simp took 270ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 146ms
simp took 114ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
tactic execution of Lean.Parser.Tactic.simp took 313ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
simp took 116ms
cumulative profiling times:
attribute application 0.962ms
blocked (unaccounted) 2.31s
compilation (IR) 3.9ms
compilation (LCNF base) 34.9ms
compilation (LCNF impure) 20.1ms
compilation (LCNF mono) 31.3ms
congr simp thm 12.2ms
dsimp 2.37ms
elaboration 136ms
fix level params 2.05ms
import 501ms
initialization 34.9ms
instantiate metavars 24.4ms
interpretation 383ms
let-to-have transformation 0.896ms
linting 59.9ms
module linting 0.00199ms
overlappingInstancesLinter 9.2ms
parsing 32.3ms
process pre-definitions 35ms
share common exprs 20.3ms
simp 2s
tactic execution 2.11s
tacticAnalysis 82.5ms
type checking 220ms
typeclass inference 43ms
real 3.54
user 7.23
sys 0.64
LeanPool/PureNock/NPR.lean
import took 587ms
cumulative profiling times:
attribute application 8.14ms
compilation (IR) 0.304ms
compilation (LCNF base) 3.53ms
compilation (LCNF impure) 1.34ms
compilation (LCNF mono) 5.79ms
congr simp thm 8.79ms
elaboration 235ms
fix level params 6.98ms
import 587ms
initialization 39.2ms
instantiate metavars 7.73ms
interpretation 672ms
let-to-have transformation 0.825ms
linting 66.7ms
module linting 0.00192ms
norm_num 9.93ms
overlappingInstancesLinter 28.8ms
parsing 37.3ms
process pre-definitions 28.1ms
ring 46.2ms
share common exprs 26.3ms
simp 218ms
tactic execution 436ms
tacticAnalysis 118ms
type checking 275ms
typeclass inference 681ms
real 2.03
user 3.48
sys 0.56
LeanPool/PureNock/NounValidation.lean
import took 407ms
cumulative profiling times:
attribute application 0.935ms
blocked (unaccounted) 34ms
compilation (IR) 1.06ms
compilation (LCNF base) 12.1ms
compilation (LCNF impure) 5.21ms
compilation (LCNF mono) 7.73ms
congr simp thm 2.98ms
elaboration 61.1ms
fix level params 0.537ms
import 407ms
initialization 34ms
instantiate metavars 1.96ms
interpretation 228ms
let-to-have transformation 0.258ms
linting 19.9ms
module linting 0.00225ms
overlappingInstancesLinter 6.22ms
parsing 12ms
process pre-definitions 11.7ms
share common exprs 3.57ms
simp 66.1ms
tactic execution 172ms
tacticAnalysis 35ms
type checking 95.4ms
typeclass inference 32.6ms
real 1.28
user 1.31
sys 0.45
LeanPool/PureNock/PaperFieldBridge.lean
import took 509ms
tactic execution of Lean.Parser.Tactic.induction took 122ms
tactic execution of Lean.Parser.Tactic.simpAll took 135ms
tactic execution of Lean.Parser.Tactic.simpAll took 125ms
cumulative profiling times:
attribute application 0.639ms
blocked (unaccounted) 2.57s
compilation (IR) 2.37ms
compilation (LCNF base) 28.1ms
compilation (LCNF impure) 17.5ms
compilation (LCNF mono) 23.3ms
congr simp thm 11ms
elaboration 107ms
fix level params 1.81ms
grind 22.6ms
grind ac 0.0173ms
grind cutsat 0.014ms
grind ematch 3.09ms
grind linarith 0.0103ms
grind mark subsingleton 1.3ms
grind ring 0.0207ms
grind simp 23.3ms
import 509ms
initialization 33.7ms
instantiate metavars 6.46ms
interpretation 294ms
let-to-have transformation 0.342ms
linting 35.4ms
module linting 0.00175ms
norm_num 11.4ms
overlappingInstancesLinter 6.74ms
parsing 16.2ms
process pre-definitions 23.6ms
share common exprs 16.5ms
simp 2.12s
sym canon 1.65ms
sym typeclass inference 55.3ms
tactic execution 819ms
tacticAnalysis 53ms
type checking 295ms
typeclass inference 46.7ms
real 2.98
user 5.14
sys 0.54
LeanPool/PureNock/PaperNames.lean
import took 482ms
cumulative profiling times:
attribute application 0.0784ms
compilation (IR) 0.146ms
compilation (LCNF base) 1.21ms
compilation (LCNF impure) 0.576ms
compilation (LCNF mono) 0.582ms
elaboration 2.13ms
import 482ms
initialization 34.4ms
interpretation 192ms
linting 6.94ms
module linting 0.00192ms
overlappingInstancesLinter 3.02ms
parsing 4.57ms
tacticAnalysis 11.3ms
type checking 1.55ms
real 1.15
user 0.73
sys 0.49
LeanPool/PureNock/PaperReference.lean
import took 135ms
tactic execution of Lean.Parser.Tactic.simp took 113ms
tactic execution of Lean.Parser.Tactic.induction took 115ms
type checking took 102ms
tactic execution of Lean.Parser.Tactic.simpAll took 397ms
cumulative profiling times:
attribute application 0.0627ms
blocked (unaccounted) 444ms
compilation (IR) 1.95ms
compilation (LCNF base) 15.6ms
compilation (LCNF impure) 12.9ms
compilation (LCNF mono) 18.1ms
congr simp thm 7.09ms
elaboration 42.7ms
fix level params 0.835ms
grind 6.5ms
grind ac 0.00572ms
grind cutsat 0.00706ms
grind ematch 0.25ms
grind linarith 0.00385ms
grind mark subsingleton 0.345ms
grind ring 0.00672ms
grind simp 5.85ms
import 135ms
initialization 40.1ms
instantiate metavars 3.32ms
interpretation 3.01ms
let-to-have transformation 0.179ms
linting 7.17ms
module linting 0.00195ms
parsing 3.5ms
process pre-definitions 15ms
share common exprs 5.8ms
simp 1.44s
sym canon 0.478ms
sym typeclass inference 1.98ms
tactic execution 758ms
type checking 199ms
typeclass inference 17.3ms
real 2.28
user 3.91
sys 0.37
LeanPool/PureNock/PaperReferenceMod.lean
import took 496ms
tactic execution of Lean.Parser.Tactic.induction took 116ms
type checking took 101ms
tactic execution of Lean.Parser.Tactic.simpAll took 140ms
cumulative profiling times:
attribute application 0.0851ms
blocked (unaccounted) 459ms
compilation (IR) 1.45ms
compilation (LCNF base) 15.5ms
compilation (LCNF impure) 8.9ms
compilation (LCNF mono) 13.4ms
congr simp thm 6.76ms
elaboration 52ms
fix level params 0.83ms
grind 6.98ms
grind ac 0.00586ms
grind cutsat 0.0068ms
grind ematch 0.226ms
grind linarith 0.00352ms
grind mark subsingleton 0.38ms
grind ring 0.00705ms
grind simp 5.95ms
import 496ms
initialization 33.9ms
instantiate metavars 3.13ms
interpretation 177ms
let-to-have transformation 0.179ms
linting 15.1ms
module linting 0.00195ms
overlappingInstancesLinter 3.39ms
parsing 7.75ms
process pre-definitions 17.4ms
share common exprs 7.58ms
simp 1.54s
sym canon 0.51ms
sym typeclass inference 16.3ms
tactic execution 476ms
tacticAnalysis 23.7ms
type checking 199ms
typeclass inference 45.1ms
real 2.89
user 3.74
sys 0.51
LeanPool/PureNock/PureAgreement.lean
import took 438ms
tactic execution of Lean.Parser.Tactic.simp took 108ms
tactic execution of Lean.Parser.Tactic.simpAll took 256ms
simp took 155ms
simp took 155ms
simp took 155ms
simp took 155ms
simp took 155ms
simp took 155ms
simp took 155ms
simp took 155ms
simp took 155ms
type checking took 170ms
cumulative profiling times:
attribute application 1.15ms
blocked (unaccounted) 4.64s
compilation (IR) 5.01ms
compilation (LCNF base) 48.3ms
compilation (LCNF impure) 29ms
compilation (LCNF mono) 44.2ms
congr simp thm 24.8ms
elaboration 353ms
fix level params 8.19ms
grind 73ms
grind ac 0.0238ms
grind cutsat 0.214ms
grind dsimp 1.13ms
grind ematch 3.72ms
grind linarith 0.0126ms
grind mark subsingleton 3.75ms
grind ring 0.0473ms
grind simp 54.5ms
import 438ms
initialization 33.6ms
instantiate metavars 57.4ms
interpretation 1.11s
let-to-have transformation 2.93ms
linting 185ms
module linting 0.002ms
norm_num 0.12ms
overlappingInstancesLinter 28.1ms
parsing 119ms
process pre-definitions 121ms
share common exprs 61.6ms
simp 2.66s
sym canon 5.52ms
sym typeclass inference 83ms
tactic execution 2.54s
tacticAnalysis 317ms
type checking 856ms
typeclass inference 136ms
real 4.96
user 9.76
sys 0.71
LeanPool/PureNock/PureComplete.lean
import took 438ms
cumulative profiling times:
attribute application 5.71ms
compilation (IR) 1.58ms
compilation (LCNF base) 12.2ms
compilation (LCNF impure) 9.64ms
compilation (LCNF mono) 15ms
congr simp thm 10.4ms
elaboration 166ms
fix level params 4.46ms
import 438ms
initialization 35.3ms
instantiate metavars 39.8ms
interpretation 669ms
let-to-have transformation 0.584ms
linting 122ms
module linting 0.00225ms
norm_num 0.121ms
overlappingInstancesLinter 17.2ms
parsing 72.2ms
process pre-definitions 45.5ms
share common exprs 31.2ms
simp 1.21s
tactic execution 1.32s
tacticAnalysis 229ms
type checking 574ms
typeclass inference 210ms
real 2.56
user 5.35
sys 0.52
LeanPool/PureNock/PureCompleteHint.lean
import took 438ms
simp took 176ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
type checking took 216ms
tactic execution of Lean.Parser.Tactic.simp took 316ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
tactic execution of Lean.Parser.Tactic.simp took 135ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
tactic execution of Lean.Parser.Tactic.simp took 112ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
tactic execution of Lean.Parser.Tactic.simp took 126ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
tactic execution of Lean.Parser.Tactic.simp took 169ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
tactic execution of Lean.Parser.Tactic.simp took 153ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
tactic execution of Lean.Parser.Tactic.simp took 122ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
tactic execution of Lean.Parser.Tactic.simp took 133ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
simp took 301ms
simp took 120ms
cumulative profiling times:
attribute application 5.46ms
blocked (unaccounted) 6.61s
compilation (IR) 3.35ms
compilation (LCNF base) 32.4ms
compilation (LCNF impure) 25.1ms
compilation (LCNF mono) 36ms
congr simp thm 38.6ms
elaboration 314ms
fix level params 13ms
grind 80.2ms
grind ac 0.0267ms
grind cutsat 0.246ms
grind dsimp 1.33ms
grind ematch 4.23ms
grind linarith 0.014ms
grind mark subsingleton 4.13ms
grind ring 0.054ms
grind simp 58.9ms
import 438ms
initialization 40.8ms
instantiate metavars 107ms
interpretation 881ms
let-to-have transformation 3.22ms
linting 173ms
module linting 0.00214ms
norm_num 0.199ms
overlappingInstancesLinter 20.6ms
parsing 108ms
process pre-definitions 112ms
share common exprs 89.1ms
simp 3.92s
sym canon 5.77ms
sym typeclass inference 90.2ms
tactic execution 3.87s
tacticAnalysis 287ms
type checking 1.01s
typeclass inference 364ms
real 5.20
user 11.25
sys 0.68
LeanPool/PureNock/Reference.lean
import took 136ms
cumulative profiling times:
attribute application 0.0739ms
compilation (IR) 0.868ms
compilation (LCNF base) 10.6ms
compilation (LCNF impure) 5.09ms
compilation (LCNF mono) 7.31ms
congr simp thm 1.98ms
elaboration 55.2ms
fix level params 0.0909ms
import 136ms
initialization 34ms
instantiate metavars 0.0961ms
interpretation 2.82ms
let-to-have transformation 0.886ms
linting 4.21ms
module linting 0.00185ms
parsing 4.34ms
process pre-definitions 38.6ms
share common exprs 1.14ms
simp 43.9ms
tactic execution 6.46ms
type checking 76.3ms
typeclass inference 17.6ms
real 0.84
user 0.65
sys 0.34
LeanPool/PureNock/Semantics.lean
import took 137ms
tactic execution of Lean.Parser.Tactic.simp took 188ms
tactic execution of Lean.Parser.Tactic.induction took 109ms
type checking took 116ms
cumulative profiling times:
attribute application 0.0313ms
compilation (IR) 0.773ms
compilation (LCNF base) 4.94ms
compilation (LCNF impure) 4.38ms
compilation (LCNF mono) 6.2ms
congr simp thm 3.81ms
elaboration 9.22ms
fix level params 0.485ms
import 137ms
initialization 37.7ms
instantiate metavars 2.26ms
interpretation 3.04ms
let-to-have transformation 0.0996ms
linting 3.55ms
module linting 0.00171ms
parsing 1.51ms
process pre-definitions 4.06ms
share common exprs 2.93ms
simp 773ms
tactic execution 344ms
type checking 122ms
typeclass inference 12ms
real 1.91
user 2.19
sys 0.33
LeanPool/PureNock/Trace.lean
import took 135ms
cumulative profiling times:
attribute application 0.495ms
blocked (unaccounted) 20.1ms
compilation (IR) 0.296ms
compilation (LCNF base) 1.84ms
compilation (LCNF impure) 1.55ms
compilation (LCNF mono) 2.42ms
congr simp thm 3.6ms
elaboration 120ms
fix level params 0.981ms
import 135ms
initialization 33.8ms
instantiate metavars 4.27ms
interpretation 2.79ms
let-to-have transformation 0.407ms
linting 33.9ms
module linting 0.00231ms
parsing 22.5ms
process pre-definitions 30.3ms
share common exprs 6.01ms
simp 86.5ms
tactic execution 181ms
type checking 59.8ms
typeclass inference 12.2ms
real 0.84
user 0.88
sys 0.34
LeanPool/PureNock/TraceCertificate.lean
import took 135ms
cumulative profiling times:
attribute application 0.166ms
compilation (IR) 0.455ms
compilation (LCNF base) 3.14ms
compilation (LCNF impure) 1.94ms
compilation (LCNF mono) 2.6ms
congr simp thm 1.69ms
elaboration 49.2ms
fix level params 0.357ms
import 135ms
initialization 34.1ms
instantiate metavars 2.32ms
interpretation 2.77ms
let-to-have transformation 0.168ms
linting 11.4ms
module linting 0.00178ms
parsing 8.61ms
process pre-definitions 13ms
share common exprs 2.51ms
simp 52.9ms
tactic execution 100ms
type checking 15.4ms
typeclass inference 1.9ms
real 0.74
user 0.62
sys 0.32
LeanPool/PureNock/Tree.lean
import took 134ms
cumulative profiling times:
attribute application 0.424ms
blocked (unaccounted) 222ms
compilation (IR) 0.842ms
compilation (LCNF base) 8.01ms
compilation (LCNF impure) 4.2ms
compilation (LCNF mono) 5.4ms
congr simp thm 1.01ms
elaboration 47.6ms
fix level params 0.156ms
import 134ms
initialization 38.8ms
instantiate metavars 0.389ms
interpretation 2.8ms
let-to-have transformation 0.521ms
linting 6.79ms
module linting 0.00196ms
parsing 4.41ms
process pre-definitions 13.4ms
share common exprs 0.964ms
simp 30.5ms
tactic execution 157ms
type checking 157ms
typeclass inference 42.8ms
real 0.91
user 0.81
sys 0.34
LeanPool/PureNock/Verb.lean
import took 138ms
cumulative profiling times:
attribute application 4.78ms
blocked (unaccounted) 391ms
compilation (IR) 4.18ms
compilation (LCNF base) 40.1ms
compilation (LCNF impure) 21ms
compilation (LCNF mono) 29.7ms
congr simp thm 9.36ms
elaboration 304ms
fix level params 2.05ms
import 138ms
initialization 38.3ms
instantiate metavars 8.74ms
interpretation 3.01ms
let-to-have transformation 3.38ms
linting 66.7ms
module linting 0.002ms
parsing 48.2ms
process pre-definitions 86.9ms
share common exprs 18.7ms
simp 237ms
tactic execution 528ms
type checking 184ms
typeclass inference 69.1ms
real 1.37
user 2.02
sys 0.40
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Vilin97
commented
Oct 9, 2026
Collaborator
Author
There was a problem hiding this comment.
Independent permanent-reviewer source assessment at b21340222b0d340dcc5975a2091225dcbce7b007.
The review covered all 26 added files, with an independent whole-file review of the evaluator, agreement, completeness and modular bridge proofs. The OP0–10 equivalence constructs finite successful runs from progress and a decreasing cost; the separate hint machine proves its OP11 completeness. The trace certificate faithfully distinguishes a terminal final state from a checker-accepted crash edge. The guarded bridge explicitly requires modulus greater than one, bounded atoms and successful guarded evaluation.
The fingerprint proofs construct a nonzero difference polynomial from distinct field-valued noun data or tree shapes. Root counting gives the stated single-pair bound; the table bound uses a union bound with one shared random evaluation point. Horner evaluation agrees with the polynomial construction. Natural leaf casts, the corrected Dyck exponent and modular overflow restrictions are disclosed. The conditional modular oracle claim does not establish arbitrary wrapping replay of the manuscript's OP6 macro.
These are substantial, completed results in operational semantics and verifiable computation. The pinned bundled manuscript, release README, Apache-2.0 license and contributor notice support the imported language/fingerprint scope. The card excludes the framework's zkVM/AIR/RAP security endpoints and distinguishes its draft from the posted ePrint revision.
Novelty follow-up: the named closest declarations provide generic infrastructure. Mathlib's StateTransition.mem_eval characterizes termination by reachability; tr_eval and tr_eval_rev require an already proved Respects simulation. Lean4Itree.ITree.ieq_iff_eq proves constructor-preserving coinductive equality, and bind_assoc proves generic monad associativity. They do not construct the Nock opcode simulation, certified finite traces, crash completeness or guarded evaluator bridge proved here. Generic polynomial root bounds also require the separating noun polynomial and degree bound that this project constructs. Horner agreement and the shared-point table bound are meaningful implementation and application extensions.
This supports a qualified novelty pass. No named duplicate headline was identified. Actual Tau Ceti declaration comparisons remain unverifiable; the bounded lexical searches are discovery evidence and do not prove novelty. The unlocated ITree.interp contract is also unchecked. Incomplete coverage alone is not the rubric's real-overlap or suspected-prior-art criterion for discuss. Separate reference evaluators are a defensible architectural choice because their semantic differences are tested by the agreement results.
The mathematical and source judgment remains favorable at this exact head. The finite follow-up resolves my prior novelty discuss assessment; the configured exact-head review also reports all five dimensions passing. Current-head required checks must still be refreshed for integration. This review preserves all normal protected native queue checks.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This imports the completed Pure Nock language and fingerprint formalization: small-step/big-step evaluator equivalence, executable trace certificates and crash completeness, guarded modular bridges, and finite-field fingerprint collision bounds. It provides a reusable semantics and verification foundation for a verifiable VM, with a 23-module source closure and no dependency beyond the pinned Mathlib.
The daily acquisition interval is [2026-08-09T09:45:11Z, 2026-10-02T09:45:11Z). Upstream publicly released the completed language deliverable on 2026-08-26T15:48:50Z in commit 4838863baa2d49e38573efa3474e77bf1154f300, tagged
ncc/pure-nock-drop1.2.2. This is release evidence, rather than a repository refresh date.The Apache-2.0 license and collective upstream NOTICE attribution are preserved in the headers and entry module. The initial source commit credits Akis; the card records Assimakis A. Kattis as a contributor and credits the formalization contributors collectively.
provenance: humanfollows the checked-in evidence rubric: the complete two-commit public history, README, manuscript, source and publisher supplied no credible AI authorship disclosure. This is an evidence-based classification, not a claim that undisclosed AI assistance is impossible. Lean Pool porting and optimization were performed by this acquisition agent.Mathematical scope and source fidelity
The source is the bundled manuscript draft v0.1.6; its title and line references differ from the posted ePrint revision. The import preserves the original 19
Nockmodules and four layer roots, with imports relocated underLeanPool.PureNock. Audit executables, differential corpora, C extraction, branding and patches are excluded.The card records seven actual headline statements. In particular:
runProgram_adequate_completeproves finite-fuel equivalence for the paper's OP0–10 machine and derived evaluator. The OP11 hint extension has its own completeness theorem.runTraceProgram_certificateproves consistency, completion and adjacent checker acceptance; its final state is terminal or has a checker-accepted crash edge. Crash soundness and completeness concern the input program's trace.paper_field_bridgerequires bounded inputs, modulus greater than one, and a successful guarded execution. It does not identify natural and modular increment across wraparound. Modular OP6 uses the documented if/else representation; agreement with the paper's literal increment macro is scoped accordingly.collision_prob_ledistinguishes field-valued coefficient data and shape. Natural leaf casts can identify different natural-number nouns. The table theorem proves the shared-randomness union bound; the source's stronger independence/product bound is not claimed. The import retains the explicitly corrected Dyck polynomial decomposition exponents.fnHorner_eq_fnconnects the computable fingerprint to the polynomial one over a generic field.The zkVM, AIR, RAP, compute/memory table security theorem and concrete Goldilocks field/primality are outside this closure. A literal modulus witness does not assume primality. Nock source/API searches found no matching project in Lean Pool cards, source, open/merged PRs, issues or history, and none in Mathlib or TauCeti. The one Mathlib text hit was an unrelated “knock out cases” comment.
Port and validation
Pinned target: Lean 4.35.0-rc3, Mathlib c55e6e786f49471c72fbddbec5415808896aec1e. The branch starts at main checkpoint
fbe0fe3397f00e1933ffec1aed9a7f882898b1d2; it has not been repeatedly rebased.LeanPool.lean, checks, policies, workflows, options and linter configuration are unchanged. One split YAML card and the public per-project imports are added.Repairs include public module-system exposure, retained copyright/NOTICE credit, explicit field-simp import, new Lean matcher handling in two arithmetic proofs, deprecated simplifier names, definition documentation, unnecessary decidability/nonzero assumptions, style cleanup, and semantic lemma extraction from six oversized proofs. Public theorem strength is preserved; removed assumptions strengthen the affected injection results. No resource override or waiver is used.
Local checks:
Classical.choice/propext/Quot.sound.CI and the configured GPT/Greptile reviews remain the final authority; local checks do not substitute for their current-head results.
Measured compile optimization
Measurements use this VM (16 CPUs, 125 GiB RAM), warm pinned dependencies, project outputs removed from both
.lake/build/lib/lean/LeanPool/PureNock*and.lake/build/ir/LeanPool/PureNock*, andLEAN_NUM_THREADS=4:/usr/bin/time -f 'wall_seconds=%e user_seconds=%U system_seconds=%S max_rss_KiB=%M' \ env LEAN_NUM_THREADS=4 lake build LeanPool.PureNock.ImportsBaseline checkpoint
91d8641b1: 39.92s wall, 81.27s user, 9.08s system, max RSS 1,148,000 KiB. Baseline slowest modules: hint completeness 9.9s, paper agreement 9.4s, paper completeness 5.9s, modular evaluation 5.4s.Final checkpoint
bafd5a429: 29.69s wall, 72.12s user, 8.86s system, max RSS 1,141,320 KiB. The measured wall reduction is 25.6%.Declaration profiles (raw heartbeat ticks, synchronous elaboration) confirm targeted reductions:
den_succ5,974,487 → 2,403,278, anddenP_succ8,527,592 → 2,428,273. These are declaration costs; opcode extraction redistributes costs across helpers, so only whole-module totals are used to assess those splits. The five profiled modules together fell from 329,821,673 to 305,313,978 raw ticks (7.4%). Whole-module changes were paper agreement −17.2%, agreement −9.7%, paper completeness −2.9%, hint completeness −1.6%, and modular evaluation +0.9% (helper overhead).The evidence-driven pass extracts coherent opcode/progress lemmas, removes a global concrete-field demonstration instance/import, and restricts denotation/terminal proofs to the simplifications they use. Synchronous per-declaration profiles expose the remaining genuine evaluator/cost work. A scoped evaluator-unfolding experiment increased cost-stability heartbeat use and was reverted; limiting
grindinputs alone had essentially unchanged heartbeat cost. No theorem was weakened to improve a measurement. Greptile's trace-card overstatement was corrected in the card and inherited docstring without changing the theorem. Its standalone Horner API finding was repaired by generalizing that computation to semirings; a clean rebuild at the repaired head again measured 29.69s wall. These single-run wall timings are observations on a shared VM; deterministic declaration profiles are retained alongside them.The rollout prerequisites for PR610/611 were verified merged and green at the start. This PR will only be eligible for the protected native queue once current-head CI, mathematical review, licensing/provenance and all material findings are resolved.