Computer-assisted Proof Under Audit: Typos, Certificate Errors, and Reproducible Exact Checks for a Symbolic Invertibility Proof

Technische Samenvatting: Computerondersteund Bewijs Onder Audit

Probleemstelling
Dit artikel presenteert een onafhankelijke, versie-gepinde, broncode-niveau audit van een gepubliceerd computerondersteund bewijs (CAP) betreffende de inversibiliteit van een gelineariseerde operator rond een benaderend zelf-similar Boussinesq-profiel. Het doelbewijs, dat oorspronkelijk verscheen als arXiv:2310.19781v2 en vervolgens in Communications in Mathematical Physics (CMP), steunt op een symbolisch certificaat gegenereerd via MATLAB om grenzen en reconstructiestappen vast te stellen die noodzakelijk zijn voor het bewijzen van singulariteitsvorming in incompressibele vloeistoffen. De audit onderzoekt of het vrijgegeven computationele certificaat de geclaimde conclusies rigoureus ondersteunt, waarbij specifiek wordt gecontroleerd op consistentie tussen de wiskundige tekst, de vrijgegeven broncode en de exacte rekenkundige resultaten.

Methodologie
De auteur hanteert een forensische audit-methodologie die onderscheid maakt tussen "gedrukte typefouten" (drukfouten in de tekst waarbij de code of het omliggende argument correct blijft) en "certificaatfouten" (defecten waarbij de vrijgegeven berekening er niet in slaagt een noodzakelijke implicatie vast te stellen). Het proces omvat:

1. Versie-pinning: De audit stemt de CMP-versie af op het specifieke arXiv v2 bronarchief, gebruikmakend van SHA-256-digests om exacte herkomst te garanderen.
2. Verificatie van Exacte Rekenkunde: In plaats van te vertrouwen op floating-point heruitvoeringen, construeert de auteur reproduceerbare exacte-rekenkundige scripts (met behulp van rationale getallen) om specifieke grenzen, coëfficiëntlussen en reconstructieformules te verifiëren.
3. Broncode-vergelijking: De audit vergelijkt de wiskundige definities in het artikel met de werkelijke implementatie in de vrijgegeven MATLAB-scripts (bijv. invertibility.tex, shorttime_sym.m, profile.m), waarbij wordt gecontroleerd op discrepanties in indices, tekens, domeindekking en weggelaten termen.
4. Constructie van Tegenvoorbeelden: Waar defecten worden gevonden, genereert de auteur exacte tegenvoorbeelden om aan te tonen dat specifieke grenzen of vergelijkingen falen onder de condities die in het certificaat zijn gedefinieerd.

Belangrijkste Bevindingen en Resultaten
De audit identificeert 11 bewijs-affecterende defecten naast diverse typografische slordigheden. Cruciaal is dat de CMP-publicatie geen van deze punten heeft gecorrigeerd. De defecten zijn als volgt gecategoriseerd:

• Certificaatfouten (Bewijs-affecterend):

  • Short-Time Coëfficiëntlussen: De residu-coëfficiëntlus in de code is niet componentgewijs zoals in de tekst wordt gesuggereerd, en het bovenste eindpunt wordt onjuist behandeld als een hybride modus.
  • Picard-multiplicatie: De implementatie van de tekengevoelige Picard-multiplicatie bevat fouten die de gerichte insluitingslogica ongeldig maken.
  • Profielgrenzen: De geregistreerde $L^\infty$-test is vijf keer te zwak om het geclaimde budget te ondersteunen, en de daaropvolgende budgetallocatie (113) volgt niet uit de gecorrigeerde grenzen.
  • Nulde Moment: De berekening van het nulde moment mist een geldige staart-toelage (tail allowance), waardoor de bijbehorende grens ongeldig is.
  • Vergelijking (27) en Rechthoekige Boekhouding: Een direct tegenvoorbeeld toont aan dat Vergelijking (27) in v2 en CMP onwaar is. Bovendien worden twee eindige rechthoeken die vereist zijn voor de decompositie niet geëvalueerd in de code, en de bovengrens van de kernel deelt hetzelfde eindige gat.
  • Grote-Tijd Reconstructie: De puntwaarde-cascade laat één forceringsterm weg, en Vergelijking (30) keert beide reconstructietekens om. Daarnaast laat de code een exponentiële kortingsfactor weg die vereist is voor de staart-schatting.

• Gedrukte Typefouten (Niet-bewijs-affecterend):

  • Er zijn verschillende inconsistenties gevonden waarbij de tekst fouten bevat (bijv. onjuiste ondergrenzen in sommen, verkeerde coëfficiëntnamen in staart-expansies, ontbrekende exponenten in bèta-staatnotatie), maar de vrijgegeven code of het omliggende logische argument reeds de correcte beoogde versie gebruikt. Deze worden geclassificeerd als "T" (Typos) in plaats van "C" (Certificaatfouten).

Significantie en Claims
Het artikel claimt de eerste onafhankelijke, versie-gepinde, broncode-niveau audit te zijn van een gepubliceerd computerondersteund bewijs in de analyse dat meerdere bewijs-affecterende defecten binnen een vrijgegeven computationeel certificaat identificeert.

• Aard van de Fout: De bevindingen weerleggen niet de beoogde stelling of de analytische reductie ervan. In plaats daarvan demonstreren ze dat het gepubliceerde certificaat de geclaimde conclusie niet bewijst. De kloof ligt in de vertaling van het wiskundige argument naar het computationele certificaat, waarbij specifieke constanten, tekens en domeindekkingen onjuist zijn afgehandeld.
• Implicaties voor CAP's: De audit benadrukt dat bij analytische/numerieke CAP's het verifiëren dat een programma draait of dat de gehele rekenkunde intern consistent is, onvoldoende is. De audit moet de interfaces tussen formules, code en continue objecten verifiëren (bijv. domeindekking, afkaping, staartgedrag en tekenpropagatie).
• Toekomstig Werk: De auteur stelt dat een gecorrigeerd, structureel eenvoudiger bewijs met aanzienlijk minder machine-assistentie in toekomstig werk zal worden verstrekt.

Conclusie
De audit concludeert dat hoewel de beoogde stelling mogelijk nog steeds standhoudt, het specifieke symbolische certificaat dat bij het artikel is vrijgegeven, defect is. Het publicatieproces (CMP) is er niet in geslaagd deze defecten te identificeren of te corrigeren. Het artikel dient als een methodologische demonstratie dat het rigoureus auditeren van CAP's vereist dat men onderscheid maakt tussen gedrukte slordigheden en structurele certificaatfouten, en dat dit een reproduceerbare exacte controle vereist in plaats van louter het heruitvoeren van de code.