Erdős #1052 corollary

Canonical assertion

no unitary perfect number is odd (Erdos1052.not_odd_of_isUnitaryPerfect). Kernel-clean Lean proof — axioms {propext, Classical.choice, Quot.sound}, no sorryAx — whose proof INVOKES the accepted lemma even_of_isUnitaryPerfect (vf_6ccc854a9ab51bbb). A real lemma-inheritance event: an accepted verified lemma composed into a new verified theorem (Compounding B).

Notation is rendered from the stored source. The pinned checkout remains the exact record.

Sourcemodel_output
Assertiontheoretical
Evidence0 spans
Standingrecorded

Scope and conditions

theoretical

Record vrc_c1a3454fddc9ec1f (signed; recorded against the current head). Caveats: Re-homed from the prover-lane frontier (vfr_b354d1ae5d88038b), where it was originally established and signed under the maintainer key; this consolidates the two kernel-verified Lean frontiers into one. | Witness not re-attached in this corpus yet: the proof lives at mzhorvath1/formal-conjectures@b70a2ddf (corollary of even_of), pending upstream; a fresh vlv_ will be minted via `foundry lean-run` once it merges into google-deepmind/formal-conjectures. The claim itself was foundry-verified and human-signed in prover-lane.. Artifacts: 1 hash-verified at propose.

Provenance summary

Source: record:vrc_c1a3454fddc9ec1f
Source type: model_output
Recorded: Jul 6, 2026, 8:58 PM
Updated: not recorded
Evidence spans: 0

Exact record identityFinding ID, frontier identity, and pinned Git source

Finding ID: vf_f0ab437e00bed886
Frontier: vfr_97d7d25957384f80
Commit: 2705e4db4ffb9987c53388c8a89c1450c63afdf8
Tree: a24f2c67b52a5b3c9163438243b95351bbc8e296

Exact source and rootsGit 2705e4db4ffb and content-addressed ledgers

Source identity

Commit: 2705e4db4ffb9987c53388c8a89c1450c63afdf8
Tree: a24f2c67b52a5b3c9163438243b95351bbc8e296
Committed: 2026-07-19T05:13:20Z
Repository: Open source

Content roots

Event log: sha256:c4a00883ab7468dcce59c368b81fd09e45366b21af8e34979d7a639d73a8d32c
Snapshot: sha256:45fa712bd6d9a8d4c8514a7cba107e7f814f2c1368805abd577e762ccb6123a4
Proposals: sha256:ba47ddf5c16ed567ddf835385066e3fc294b447bc0eabd3f9820f5e707efb39e
Actor registry: sha256:f52d59b1db885f467c66a29335ada68544a09da5f3869723461100eed0aac79e
Artifacts: sha256:fbd7e05b185cd06bc06484e8b0216c17c5263a71d8481ca38e574e9b2c5156d8