sharp-symmetry-bounds-lean registered in the Palomar registry: PALOMAR-2026-09-18-000007

carlok/sharp-symmetry-bounds-lean is now a registered entry in the Palomar registry — PALOMAR-2026-09-18-000007, version 1, status registered, trust level high, on the source of commit ced9fe2 (the record’s own copy of the entry is here). This is the first third-party verification of one of these formalizations, and what the registry actually did is the news: it rebuilt the project in a sandbox from the pinned dependencies (Lean v4.32.0), exported the proof terms with lean4export and replayed them on nanoda, an independent kernel implementation rather than the author’s own build, then used the Comparator to check that Solution.lean proves the Challenge.lean statements — five theorems of SharpSymmetryBounds — using only propext, Quot.sound and Classical.choice, verified at 2026-09-18T13:50:47Z.

An immutable copy of the source was then archived with a receipt hash (2026-09-18T14:30:13Z): carlok/sharp-symmetry-bounds-lean was forked by PalomarArchive, the registry’s archive organisation, at the same ced9fe2 commit. Automated editorial review came back neutral with no warnings, and the machine-readable evidence — build, replay, comparison, axioms — is published alongside the entry. The record certifies that the Lean proofs check, not that the result is new. The repository’s own commits the same day are this story: the working note recorded as the formalized source, the registry record linked from the README and citation metadata and badges.