Cosa è stato aggiunto:
evalComplex(), nuovo e additivo rispetto a evalNumeric() (mai toccato) — provato solo quando il valutatore reale non risolve già l'espressione.
Riconoscimento dell'unità immaginaria (2i, 3.5i, i da sola — ma non come parte di identificatori più lunghi, es. interval resta un normale simbolo).
Aritmetica complessa completa (+, −, ×, ÷) e potenza con esponente intero non negativo (niente potenze complesse generali).
Funzioni Re(), Im(), conj() — quelle che servivano esattamente per affermazioni come Re(s)=1/2.
Due nuovi stati distinti, COMPLEX_OK/COMPLEX_FAIL — mai riusati NUMERIC_OK/NUMERIC_FAIL, per non alterare il significato di codici già in uso da fixture di stress test esistenti.
Verifica (con test eseguiti):
Rieseguiti tutti i casi reali preesistenti (2+3=5, 7*8=56, x+x=2*x, 2^3=8) → comportamento identico, byte per byte, nessuna regressione.
Nuovi casi complessi: somma/prodotto/divisione/potenza vera e falsa, i*i=-1, Re()/Im()/conj(), tutti corretti.
Casi limite onesti: esponente negativo e funzione sconosciuta → REVIEW, mai un risultato indovinato — proprio come promesso.
End-to-end su validateTheory(): un fallimento complesso si propaga correttamente a warning, status e assessment.
Lo Stress Oracle ha raccolto automaticamente il nuovo codice COMPLEX_FAIL senza bisogno di modifiche aggiuntive — conferma che l'architettura del v0.8.2 era ben progettata per essere estesa.
Il valutatore separato in analyzeLogicalProofs e l'intera macchina polinomiale di analyzeAlgebraicConsistency non sono stati toccati — restano rispettivamente il prossimo passo a rischio più basso e il lavoro di portata maggiore.
Sviluppato iterativamente con l'assistenza di Claude (Anthropic) per l'analisi del codice, l'individuazione e la correzione dei difetti, e la verifica funzionale delle modifiche.
Il file JSON di riferimento mostra, in un unico documento, ogni elemento dello schema riconosciuto da ADEC Theory Validator v0.8.3: tutti i tipi di nodo previsti, entrambe le forme di prova ammesse, lo stato di dimostrazione "in sospeso", e la nuova aritmetica dei numeri complessi introdotta nella versione 0.8.3.
Non è pensato per essere caricato così com'è, ma per essere usato come base da cui copiare: ogni nodo isola un caso d'uso specifico, con un commento che ne spiega lo scopo.
Cosa contiene:
Un nodo radice senza dipendenze, e la catena minima definizione → costante → assioma → postulato → concetto, per mostrare quali nodi richiedono una descrizione obbligatoria e quali no.
Una proposizione e un lemma con prova algebrica dichiarata in forma testuale semplice.
Un teorema che dimostra la nuova aritmetica complessa introdotta in v0.8.3: unità immaginaria, operazioni tra numeri complessi, e le funzioni Re(), Im() e conj().
Un teorema con prova formale esterna, nello schema separato previsto per sistemi di dimostrazione come Lean 4, distinto dalla prova dichiarata in linguaggio naturale.
Un teorema con stato "in sospeso": una dimostrazione dichiarata ma non ancora fornita, e un corollario che ne eredita esplicitamente la condizionalità — lo stesso meccanismo con cui il motore rappresenta un'affermazione ancora aperta, invece di darla per dimostrata.
Un nodo sperimentale con un ruolo tratto dal vocabolario ammesso.
Un nodo di autovalidazione e uno di meta-validazione, con le parole chiave che il controllo semantico richiede perché siano riconosciuti come tali.
Il file è stato validato con il motore reale prima della pubblicazione: punteggio pieno su ogni livello (strutturale, semantico, formale, self-validation, meta-validation), zero errori, zero avvisi critici.
{
"title": "ADEC Prototype Model — v0.8.3",
"version": "1.0",
"language": "it",
"nodes": [
{
"id": "F1",
"kind": "foundation",
"name": "Fondamento primario",
"description": "Radice del grafo: nessuna dipendenza, punto di partenza dichiarato dell'intero sviluppo.",
"deps": []
},
{
"id": "D1",
"kind": "definition",
"name": "Definizione di base",
"description": "Introduce un oggetto o una notazione usata dai nodi successivi.",
"deps": ["F1"]
},
{
"id": "C1",
"kind": "constant",
"name": "Costante del modello",
"description": "Una quantità fissata dal framework, non derivata.",
"deps": ["F1"]
},
{
"id": "AX1",
"kind": "axiom",
"name": "Assioma dichiarato",
"description": "Un punto di partenza accettato senza dimostrazione. La descrizione non vuota è obbligatoria per questo kind.",
"deps": ["F1"]
},
{
"id": "P1",
"kind": "postulate",
"name": "Postulato",
"description": "Un'assunzione aggiuntiva, distinta da un assioma per ruolo narrativo ma trattata allo stesso modo dal motore.",
"deps": ["AX1"]
},
{
"id": "CN1",
"kind": "concept",
"name": "Concetto ausiliario",
"description": "Nodo non proof-bearing: non richiede né si aspetta un record proof/evidence.",
"deps": ["D1"]
},
{
"id": "PR1",
"kind": "proposition",
"name": "Proposizione con prova dichiarata",
"description": "Prima proposizione proof-bearing della catena; usa una prova algebrica in forma testuale semplice.",
"deps": ["AX1", "D1"],
"proof": {
"method": "algebra elementare",
"status": "declared",
"steps": [
"2+3 = 5",
"x+x = 2*x",
"a+b = b+a"
]
}
},
{
"id": "L1",
"kind": "lemma",
"name": "Lemma derivato",
"description": "Dipende dalla proposizione precedente; introduce un passaggio intermedio.",
"deps": ["PR1"],
"proof": {
"method": "sostituzione diretta",
"status": "declared",
"steps": [
"(x+1)^2 = x^2 + 2*x + 1"
]
}
},
{
"id": "T1",
"kind": "theorem",
"name": "Teorema con numeri complessi (v0.8.3)",
"description": "Dimostra l'uso della nuova aritmetica complessa: unità immaginaria, operazioni, e le funzioni Re()/Im()/conj().",
"deps": ["L1", "C1"],
"proof": {
"method": "aritmetica complessa",
"status": "declared",
"steps": [
"i*i = -1",
"(1+2i) + (3-1i) = 4+1i",
"Re(3+4i) = 3",
"Im(3+4i) = 4",
"conj(3+4i) = 3-4i"
]
}
},
{
"id": "T2",
"kind": "theorem",
"name": "Teorema con prova formale esterna",
"description": "Esempio di proof coverage tramite un sistema di dimostrazione esterno (es. Lean 4), invece della semplice evidenza dichiarata.",
"deps": ["AX1"],
"proof": {
"system": "Lean 4 / mathlib",
"statement": "∀ n : ℕ, n + 0 = n",
"status": "verified",
"verified": true,
"steps": [
"Dimostrazione verificata dal kernel di Lean 4; riferimento al file .lean e al commit del repository."
]
}
},
{
"id": "T3",
"kind": "theorem",
"name": "Teorema con prova non ancora disponibile",
"description": "Esempio dello stato onesto 'pending': l'affermazione è dichiarata ma la dimostrazione non è inclusa in questo documento.",
"deps": ["T1"],
"proof": {
"method": "dimostrazione richiesta ma non fornita in questo documento",
"status": "pending",
"steps": [
"Passaggio mancante: da fornire in una revisione successiva."
]
}
},
{
"id": "COR1",
"kind": "corollary",
"name": "Corollario finale",
"description": "Conseguenza diretta di T1 e T2; nota come un corollario che dipende da un nodo 'pending' eredita quella condizionalità.",
"deps": ["T1", "T2"],
"proof": {
"method": "conseguenza diretta",
"status": "declared",
"steps": [
"7*8 = 56"
]
}
},
{
"id": "E1",
"kind": "experiment",
"name": "Evidenza sperimentale",
"description": "Osservazione empirica collegata al teorema; il campo 'role' deve appartenere al vocabolario ammesso.",
"role": "observation",
"deps": ["T1"]
},
{
"id": "S1",
"kind": "self_validation",
"name": "Nodo di autovalidazione",
"description": "La descrizione deve richiamare esplicitamente il tema dell'autoreferenzialità o del validatore, altrimenti il controllo semantico SEM_BAD_SELF fallisce.",
"deps": ["F1"],
"proof": {
"method": "verifica interna",
"status": "declared",
"steps": [
"Il modello si autoreferenzia in modo coerente."
]
}
},
{
"id": "M1",
"kind": "meta_validation",
"name": "Nodo di meta-validazione",
"description": "La descrizione deve richiamare esplicitamente coerenza di livello o meta-validazione, altrimenti il controllo semantico SEM_BAD_META fallisce.",
"deps": ["F1"],
"proof": {
"method": "verifica di coerenza tra livelli",
"status": "declared",
"steps": [
"La coerenza tra il livello oggetto e il livello meta è mantenuta."
]
}
}
]
}