fix(meta): picks-theorem-oq-03 register PicksTheoremOQ03.lean orphan companion#21912
Merged
Merged
Conversation
…companion 437-line companion file in namespace PicksTheoremOQ03 (the d=2 Pick's- theorem specialization of Ehrhart theory: polygon_2d / unit-simplex / unit-cube / reeve-tetrahedra concrete instances, plus reciprocity- recovers-Picks check) was an unregistered orphan. The file declares 1 axiom ehrhart_fn (Ehrhart counting function as a typed primitive). Register in both meta.additionalFiles (string form — auditor traces) and leanFile.additionalFiles (rich object — preserves file stats). Per PR #21863 picks-theorem-oq-03 uses the swap convention: strings in meta (auditor-visible), rich objects in leanFile (renderer). Updates axiomCount 2 -> 3 and refreshes the assumptions string to mention ehrhart_fn alongside the existing ehrhart_is_polynomial and ehrhart_macdonald_reciprocity. The legacy "axioms": 3 field at meta line 23 was already correct — this aligns the canonical axiomCount.
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.
Fix
Register the 437-line
Proofs/PicksTheoremOQ03.leanorphan companion in bothmeta.additionalFiles(string — auditor-visible) andleanFile.additionalFiles(rich object — renderer). SyncaxiomCount2 → 3 to reflect the now-visibleehrhart_fnaxiom.Evidence
Before:
proofs/Proofs/PicksTheoremOQ03.lean(437 lines, namespacePicksTheoremOQ03, 1 axiomehrhart_fn, 19 theorems, 6 defs, 0 sorries) was an orphan — not listed in anymeta.json.picks-theorem-oq-03slug only registered the main fileEhrhartPolynomialOQ03.lean(leanFile.path) andPicksTheoremOQ03CrossPoly.lean(companion).meta.axiomCount: 2;assumptionsmentioned onlyehrhart_is_polynomial+ehrhart_macdonald_reciprocity.After:
meta.additionalFilesandleanFile.additionalFilesnow includeProofs/PicksTheoremOQ03.lean(string form in meta per the swap convention adopted in fix(meta): picks-theorem-oq-03 swap additionalFiles formats #21863; rich object form in leanFile mirroring the existing CrossPoly entry).meta.axiomCountbumped to 3 andassumptionstext now lists all three axioms (ehrhart_is_polynomial,ehrhart_macdonald_reciprocity,ehrhart_fn).meta.axioms: 3(top of meta block) was already correct — this PR brings the canonicalaxiomCountinto alignment.Slug status (
axiomatized, badgeaxiom) unchanged — the file was already axiomatized, this just exposes one more axiom that was already mathematically in the slug's inventory.Automated fix by lean-mechanic agent.