Historisch-herzien: momentopname vóór v0.25. Lees de huidige claimstatus. Status · Original / origineel
Historisch-herzien: momentopname vóór v0.25. Lees de huidige claimstatus. Status · Original / origineel
De oorspronkelijke Lean-bewijzen zijn op 16 september 2026 opnieuw gebouwd: de exponentiële kernstelling en vier resultaten over afgeleiden en symmetrie slagen. Hieronder staan de precieze conclusies, aangevuld met uitgeschreven bewijzen en onafhankelijk nagerekende voorbeelden.
Kies een configuratieruimte C, compositie ⊕ en een niet-negatieve weerstand S. Neem bij toegestane onafhankelijke compositie S(A⊕B)=S(A)+S(B) aan. Neem bovendien aan dat het gewicht uitsluitend van S afhangt: w=φ∘S. Dit zijn modelkeuzes.
Stelling. Als φ:[0,∞)→(0,1] voldoet aan φ(s+t)=φ(s)φ(t) voor alle s,t≥0, dan bestaat λ≥0 met:
φ(s) = exp(−λs), s ≥ 0
φ(0)=1 volgt al uit positiviteit en compositie. Continuïteit hoeft niet apart te worden aangenomen. Voor een strikt dalend gewicht is daarnaast φ(s₀)<1 voor minstens één s₀ nodig; anders is λ=0 toegestaan.
Formele bron: Kern.lean · nieuw compilatielog. De oude Lean-bron gebruikte de juiste beperking s≥0 al. De eerdere webtekst op heel ℝ deed dat niet. De correctie van die webtekst was dus geen weerlegging van het formele bewijs.
Neem C=[0,∞)² met optellen, S(x,y)=x en w(x,y)=e−y. S is additief en w multiplicatief. Toch kunnen configuraties met dezelfde S verschillende gewichten hebben. De factorisatie door S volgt dus niet uit deze twee eigenschappen alleen. Ook moet compositie de functionaalvergelijking op het hele genoemde domein rechtvaardigen.
Kies een referentiemaat ν. Met ε>0 en meetbare S definiëren we:
Zε = ∫ exp(−S(C)/ε) dν(C) με(B) = Zε⁻¹ ∫_B exp(−S(C)/ε) dν(C)
Dit is een kansmaat als 0<Zε<∞. In een discrete ruimte wordt de integraal een som. Een continue dichtheid is geen kans op één punt. De keuze van ν bepaalt mede welke gebieden gezamenlijk zwaar wegen.
S(x)=½ln(1+x²) is glad, niet-negatief en coercief: S(x)→∞ als |x|→∞. Het heeft een uniek niet-ontaard minimum. Toch is bij ε=1:
Z₁ = ∫ℝ 1/√(1+x²) dx = ∞
“S groeit naar oneindig” is dus op zichzelf onvoldoende. De groei moet ook de hoeveelheid beschikbare configuraties compenseren.
Voor één gekozen prefixvrije beschrijving per discrete kandidaat, met bitlengte Lᵢ, geldt Kraft: Σ2−Lᵢ≤1. Als Aᵢ≥B en 0<dᵢ≤D, volgt voor ε>0:
0 < Σᵢ dᵢ exp(−Aᵢ/ε) 2^(−Lᵢ) ≤ D exp(−B/ε) < ∞
Neem bijvoorbeeld de codewoorden 0, 10, 110, … met lengtes 1,2,3,…. Hun gewichten sommeren tot 1. Maar met dᵢ=2Lᵢ en Aᵢ=0 is iedere term 1 en divergeert de som. De begrenzing van de extra factoren doet echt werk.
Ook de Bayesiaanse boekhouding kan terug. Voor prior π(M)∝2−L(M) en positieve likelihood ℒ(D|M):
−ln P(M|D) = (ln 2)L(M) − ln ℒ(D|M) + constante(D)
Dit verklaart een combinatie van beschrijvingskosten en datakosten binnen deze gekozen prior. De coëfficiënt ln 2 zet bits om naar natuurlijke logaritmen. Zij bewijst niet dat de natuur deze prior kiest. Universele Kolmogorov-complexiteit K is bovendien afhankelijk van de beschrijvingstaal tot op een additieve constante.
Bron voor de coderingsvoorwaarden: Péter Gács, algoritmische informatietheorie.
Laat S differentieerbaar zijn en γ een differentieerbare kromme met γ(0)=x en S(γ(t))=S(x). De kettingregel geeft:
dSₓ(γ′(0)) = 0
In een inproductruimte, waar een gradiënt bestaat, betekent dit ∇S⊥γ′(0). Een omkeerbare continue lineaire transformatie U die S bewaart, brengt kritieke punten naar kritieke punten. Ligt een kromme geheel in de kritieke verzameling en bestaat de afgeleide van dS bij x, dan geldt bovendien:
Hess Sₓ(γ′(0), ·) = 0
Deze uitspraken en hun combinatie voor een familie U(t) zijn de vier opnieuw geverifieerde resultaten. De nulrichting heeft geen Hessiaankruistermen met andere richtingen. Daaruit volgt geen unieke opsplitsing van de volledige weerstand als S=A+K+I.
Neem S(x,y,z)=(x²+y²−1)²+z². Rotaties in het xy-vlak bewaren S. Hun raakrichting is ξ=(−y,x,0). Direct differentiëren geeft overal ∇S·ξ=0. Op het kritieke punt (1,0,0):
∇S = 0, Hess S = diag(8, 0, 2)
De orbitrichting (0,1,0) is een nulmode. Een afzonderlijk tegenvoorbeeld toont de grens: S=y²+yz+z² is invariant onder x-translaties, maar heeft een gemengde yz-afgeleide 1. Symmetrie maakt willekeurige overblijvende richtingen dus niet onderling ontkoppeld. Op een kritiek punt is span(∇S) bovendien de nulruimte, geen niet-triviale tijdrichting.
Orthogonaliteit.lean · nieuw compilatielog. De formele statements zijn gecontroleerd; de ruimere fysische interpretatie in oude broncommentaren volgt daar niet automatisch uit.
Neem op ℝⁿ een C²-functie S met een eindig aantal geïsoleerde globale minima x₁,…,xₘ van gelijke waarde s*. Neem positieve Hessianen Hᵢ, een positieve continue dichtheid r, compacte subniveauverzamelingen en Zε₀<∞ voor een ε₀>0 aan. Laplace-asymptotiek geeft als ε↓0:
Zε ~ e^(−s*/ε) (2πε)^(n/2) Σᵢ r(xᵢ)/√det Hᵢ pᵢ → [r(xᵢ)/√det Hᵢ] / Σⱼ[r(xⱼ)/√det Hⱼ]
pᵢ is de massa van een vaste kleine omgeving van minimum i. De kwadratische benadering levert de determinantfactor. De normalisatie- en compactheidsvoorwaarden beheersen de bijdrage daarbuiten. Nulmodi of een doorlopend minimumoppervlak vragen een andere formule.
S(x)=(x²−1)²(x²+x+1), met r=1, heeft twee globale minima op −1 en +1. De Hessianen zijn 8 en 24. Daarom is de limietmassa links √3/(1+√3)=0,6339745962. Onafhankelijke numerieke integratie geeft:
| ε | Massa x<0 |
|---|---|
| 0,1 | 0,6407736507 |
| 0,02 | 0,6353885314 |
| 0,005 | 0,6343259874 |
| 0,001 | 0,6340447322 |
Een breder minimum kan samen meer gewicht dragen, ook wanneer beide laagste punten dezelfde weerstand hebben.
Neem S=aA+bK+cI met a,b,c>0. Als kandidaat X op alle drie de kosten niet slechter is dan Y en op minstens één strikt beter, dan S(X)<S(Y) voor iedere keuze van positieve gewichten.
ΔA ≤ 0, ΔK ≤ 0, ΔI ≤ 0, minstens één strikt ⇒ aΔA + bΔK + cΔI < 0
Dit is Pareto-dominantie. Zodra kandidaten kosten uitruilen, kan de winnaar wél van a,b,c afhangen. De oude algemene robuustheidsclaim moet tot deze precieze situatie worden beperkt.
Veronderstel al complexe amplitudes met kwadratische norm, gewicht dat alleen van |c| afhangt, multiplicatieve gewichten en optelbare gewichten voor orthogonale takken. Voor positieve multiplicatieve f:(0,1]→(0,1] geeft toepassing van de kernstelling op φ(t)=f(e−t):
f(x) = x^p, p ≥ 0
Een toegestane splitsing c→(c/√2,c/√2) bewaart de kwadratische norm. Als zij ook het totale gewicht bewaart, dan:
2 (|c|/√2)^p = |c|^p 2^(1−p/2) = 1 ⇒ p = 2
Dus volgen Born-gewichten |c|² binnen deze aannames. De keuze van amplitudes, orthogonaliteit, norm en behoudsregel is invoer. Dit is geen afleiding van de hele kwantumtheorie uit alleen Effortless Effect.
Als een meetbare omkeerbare T zowel S als ν bewaart, bewaart T ook μ. Dit volgt direct door variabelen te vervangen in de integraal. Alleen S-invariantie is onvoldoende: de referentiemaat moet meedoen.
Een symmetrische verdeling hoeft geen symmetrische individuele uitkomst te geven. De verdeling met kans ½ op −1 en ½ op +1 is invariant onder tekenwisseling, terwijl geen van beide uitkomsten dat is. Een fysisch mechanisme voor spontane symmetriebreking vereist verdere dynamica of limieten.
Dit zijn inhoudelijke bouwstenen. Het blijft nodig om de configuratieruimte, weerstand, maat en fysische interpretatie te onderbouwen. De formele verificatie bewijst de genoemde implicaties, niet dat de wereld de aannames realiseert.
Download het controledossier · Uitvoeren en afbakening
Verder met K3, χ=24 en spectrale meetkunde →Resultaten en grenzen van de rekencontrole →
v0.24 · 16 september 2026