Minimal Axiom Sets for Kerr Geodesic Conservation Laws: A Machine-Verified Audit Using Aristotle

Minimal Axiom Sets for Kerr Geodesic Conservation Laws: A Machine-Verified Audit Using Aristotle | Research Square window.SnipcartSettings = { analytics: { enabled: false } }; (function() { var accessVector = localStorage.getItem('access_vector') || ''; window.dataLayer = window.dataLayer || []; if (accessVector) { window.dataLayer.push({ user: { profile: { profileInfo: { snid: accessVector } } } }); } })(); (function(w,d,s,l,i){w[l]=w[l]||[];w[l].push({'gtm.start':new Date().getTime(),event:'gtm.js'});var f=d.getElementsByTagName(s)[0],j=d.createElement(s),dl=l!='dataLayer'?'&l='+l:'';j.async=true;j.src='https://www.googletagmanager.com/gtm.js?id='+i+dl;f.parentNode.insertBefore(j,f);})(window,document,'script','dataLayer','GTM-K279D39R'); Browse Preprints In Review Journals COVID-19 Preprints AJE Video Bytes Research Tools Research Promotion AJE Professional Editing AJE Rubriq About Preprint Platform In Review Editorial Policies Our Team Advisory Board Help Center Sign In Submit a Preprint Cite Share Download PDF Research Article Minimal Axiom Sets for Kerr Geodesic Conservation Laws: A Machine-Verified Audit Using Aristotle Abdul Rahim Iqbal This is a preprint; it has not been peer reviewed by a journal. https://doi.org/ 10.21203/rs.3.rs-9185708/v1 This work is licensed under a CC BY 4.0 License Status: Posted Version 1 posted You are reading this latest preprint version Abstract We present, to our knowledge, the first systematic machine-verified audit of foundational assumptions used in classical proofs of Kerr geodesic conservation laws. The method is intentionally adversarial: for each target theorem, we submit an under-specified Lean 4 theorem stub to Aristotle (Harmonic’s AI theorem prover), then record which hypotheses, definitions, or infrastructural objects Aristotle must inject to close the proof attempt. These injected artifacts are treated as explicit witnesses of assumptions that are usually implicit in coordinate-free presentations. We formalized all four standard conservation laws in Boyer–Lindquist coordinates (rest mass, energy, axial angular momentum, and Carter constant). The central result is a formal partition into two classes. Energy and angular momentum, both tied to Killing vectors, are derivable from a common axiom set and yield isomorphic proof certificates. By contrast , the Carter constant, tied to a rank-2 Killing tensor, requires an irreducibly new axiom: across seven submissions and two independent tensor formulations, Aristotle either introduces a circular conservation premise or collapses derivative infrastructure to trivi-alize the target equation. Secondary results include three unstated C 2 regularity assumptions in energy conservation, a syntax-forced clarification of the symmetrized Killing-tensor equation, and diagnosis of Aristotle’s intermediate “Form B” tensor as mathematically incorrect by componentwise verification. Artifacts are available at github.com/abdulrahimiqbal/KerrFormalization. formal verification Kerr geometry Killing tensor Carter constant Lean 4 automated theorem proving Full Text Additional Declarations No competing interests reported. Cite Share Download PDF Status: Posted Version 1 posted You are reading this latest preprint version Research Square lets you share your work early, gain feedback from the community, and start making changes to your manuscript prior to peer review in a journal. As a division of Research Square Company, we’re committed to making research communication faster, fairer, and more useful. We do this by developing innovative software and high quality services for the global research community. Our growing team is made up of researchers and industry professionals working together to solve the most critical problems facing scientific publishing. Also discoverable on Platform About Our Team In Review Editorial Policies Advisory Board Help Center Resources Author Services Accessibility API Access RSS feed Manage Cookie Preferences © Research Square 2026 | ISSN 2693-5015 (online) Privacy Policy Terms of Service Do Not Sell My Personal Information {"props":{"pageProps":{"initialData":{"identity":"rs-9185708","acceptedTermsAndConditions":true,"allowDirectSubmit":true,"archivedVersions":[],"articleType":"Research Article","associatedPublications":[],"authors":[{"id":610693132,"identity":"5700cd07-5bbe-448d-98a2-9c1df41f9e19","order_by":0,"name":"Abdul Rahim Iqbal","email":"data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAZAAAAAyAQMAAABI0h/eAAAABlBMVEX///8AAABVwtN+AAAACXBIWXMAAA7EAAAOxAGVKw4bAAAArklEQVRIiWNgGAWjYFACxgZmBgYLOZK1SBiTZg9IS2ID0cr5Zx9uvF1QI5G+dkbuAYYfNURokTiX2Gw945hE7rYbeQmMPceIseYMY5s0DxtIS44BMwMbETrkwVr+SaSbgbX8I0KLAUgLb5tEAlgLYxsRWgzPMDZbz+yTMNx25o3Bwd4+IrTInWF/eLvgm4282fEcwwc/vhGhBQQkYIwDRGpA0jIKRsEoGAWjACsAAOBdMpnyNaWKAAAAAElFTkSuQmCC","orcid":"","institution":"Independent Researcher","correspondingAuthor":true,"prefix":"","firstName":"Abdul","middleName":"Rahim","lastName":"Iqbal","suffix":""}],"badges":[],"createdAt":"2026-03-21 12:23:41","currentVersionCode":1,"declarations":"","doi":"10.21203/rs.3.rs-9185708/v1","doiUrl":"https://doi.org/10.21203/rs.3.rs-9185708/v1","draftVersion":[],"editorialEvents":[],"editorialNote":"","failedWorkflow":false,"files":[{"id":106724972,"identity":"e369b42d-493c-4f9a-81da-81989c661e8c","added_by":"auto","created_at":"2026-04-12 18:30:50","extension":"pdf","order_by":1,"title":"","display":"","copyAsset":false,"role":"manuscript-pdf","size":259920,"visible":true,"origin":"","legend":"","description":"","filename":"main.pdf","url":"https://assets-eu.researchsquare.com/files/rs-9185708/v1_covered_58227903-b8f5-4f10-bc5e-56c827260d2f.pdf"}],"financialInterests":"No competing interests reported.","formattedTitle":"Minimal Axiom Sets for Kerr Geodesic Conservation Laws: A Machine-Verified Audit Using Aristotle","fulltext":[],"fulltextSource":"","fullText":"","funders":[],"hasAdminPriorityOnWorkflow":false,"hasManuscriptDocX":false,"hasOptedInToPreprint":true,"hasPassedJournalQc":"","hasAnyPriority":true,"hideJournal":true,"highlight":"","institution":"","isAcceptedByJournal":false,"isAuthorSuppliedPdf":true,"isDeskRejected":"","isHiddenFromSearch":false,"isInQc":false,"isInWorkflow":false,"isPdf":true,"isPdfUpToDate":true,"isWithdrawnOrRetracted":false,"journal":{"display":true,"email":"[email protected]","identity":"researchsquare","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":true,"externalIdentity":"","sideBox":"","snPcode":"","submissionUrl":"/submission","title":"Research Square","twitterHandle":"researchsquare","acdcEnabled":true,"dfaEnabled":false,"editorialSystem":"","reportingPortfolio":"","inReviewEnabled":false,"inReviewRevisionsEnabled":true},"keywords":"formal verification, Kerr geometry, Killing tensor, Carter constant, Lean 4, automated theorem proving","lastPublishedDoi":"10.21203/rs.3.rs-9185708/v1","lastPublishedDoiUrl":"https://doi.org/10.21203/rs.3.rs-9185708/v1","license":{"name":"CC BY 4.0","url":"https://creativecommons.org/licenses/by/4.0/"},"manuscriptAbstract":"We present, to our knowledge, the first systematic machine-verified audit of foundational assumptions used in classical proofs of Kerr geodesic conservation laws. The method is intentionally adversarial: for each target theorem, we submit an under-specified Lean 4 theorem stub to Aristotle (Harmonic’s AI theorem prover), then record which hypotheses, definitions, or infrastructural objects Aristotle must inject to close the proof attempt. These injected artifacts are treated as explicit witnesses of assumptions that are usually implicit in coordinate-free presentations. We formalized all four standard conservation laws in Boyer–Lindquist coordinates (rest mass, energy, axial angular momentum, and Carter constant). The central result is a formal partition into two classes. Energy and angular momentum, both tied to Killing vectors, are derivable from a common axiom set and yield isomorphic proof certificates. By contrast , the Carter constant, tied to a rank-2 Killing tensor, requires an irreducibly new axiom: across seven submissions and two independent tensor formulations, Aristotle either introduces a circular conservation premise or collapses derivative infrastructure to trivi-alize the target equation. Secondary results include three unstated C 2 regularity assumptions in energy conservation, a syntax-forced clarification of the symmetrized Killing-tensor equation, and diagnosis of Aristotle’s intermediate “Form B” tensor as mathematically incorrect by componentwise verification. Artifacts are available at github.com/abdulrahimiqbal/KerrFormalization.","manuscriptTitle":"Minimal Axiom Sets for Kerr Geodesic Conservation Laws: A Machine-Verified Audit Using Aristotle","msid":"","msnumber":"","nonDraftVersions":[{"code":1,"date":"2026-03-26 06:46:40","doi":"10.21203/rs.3.rs-9185708/v1","editorialEvents":[{"type":"communityComments","content":0}],"status":"published","journal":{"display":true,"email":"[email protected]","identity":"researchsquare","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":true,"externalIdentity":"","sideBox":"","snPcode":"","submissionUrl":"/submission","title":"Research Square","twitterHandle":"researchsquare","acdcEnabled":true,"dfaEnabled":false,"editorialSystem":"","reportingPortfolio":"","inReviewEnabled":false,"inReviewRevisionsEnabled":true}}],"origin":"","ownerIdentity":"ca471b2a-613d-4430-9db0-ef18c40a3a06","owner":[],"postedDate":"March 26th, 2026","published":true,"recentEditorialEvents":[],"rejectedJournal":[],"revision":"","amendment":"","status":"posted","subjectAreas":[],"tags":[],"updatedAt":"2026-04-10T00:24:05+00:00","versionOfRecord":[],"versionCreatedAt":"2026-03-26 06:46:40","video":"","vorDoi":"","vorDoiUrl":"","workflowStages":[]},"version":"v1","identity":"rs-9185708","journalConfig":"researchsquare"},"__N_SSP":true},"page":"/article/[identity]/[[...version]]","query":{"redirect":"/article/rs-9185708","identity":"rs-9185708","version":["v1"]},"buildId":"XKTyCvWXoU3ODBz1xrDgd","isFallback":false,"isExperimentalCompile":false,"dynamicIds":[84888],"gssp":true,"scriptLoader":[]}