Come si definisce la divisione con resto nei numeri gaussiani mantenendosi interamente nell’anello degli interi

Consideriamo l’anello dei numeri gaussiani, cioè i numeri complessi a + bi con a e b interi, e la definizione della divisione con resto in questo contesto. Per la divisione nei numeri interi si sa che dati a e b ≠ 0 esistono q e r tali che a = bq + r con 0 ≤ r < |b|, ma una variante utile afferma che si possono scegliere q′ e r′ tali che a = bq′ + r′ con |r′| ≤ |b|/2. Questa variante permette di ragionare su resti centrati attorno a zero e facilita alcuni calcoli, evitando casi complessi nella definizione della divisione.

Per formalizzare questo concetto nel caso dei numeri gaussiani, si può partire dall’osservazione che, analogamente agli interi, è possibile definire un’operazione di divisione “approssimata” usando il concetto di norma, cioè N(x) = a² + b² per x = a + bi. La norma ha proprietà fondamentali: è sempre non negativa, si annulla solo per l’elemento nullo, e rispetta la moltiplicazione, cioè N(xy) = N(x)N(y). Queste proprietà consentono di estendere la nozione di divisione con resto agli interi gaussiani, pur mantenendosi dentro la teoria degli interi senza passare ai numeri complessi in senso più ampio.

b * div′(a, b) + mod′(a, b) = a,

e assicurano che il modulo mod′(a, b) abbia valore assoluto non superiore a b/2. In tal modo si evita la definizione “a casi” tipica della divisione standard, rendendo l’argomento più elegante e compatto. Le funzioni sono definite in modo che si aggiunga b/2 a a prima della divisione e poi si corregga il resto sottraendo b/2.

La proprietà cruciale da dimostrare è che la norma del resto è strettamente minore della norma del divisore, ovvero

N(x % y) < N(y),

per y ≠ 0. Questa disuguaglianza è essenziale per l’algoritmo euclideo nei numeri gaussiani e permette di definire la divisione euclidea, base della teoria dei numeri gaussiani, dei loro ideali e della fattorizzazione.

La dimostrazione sfrutta la proprietà che la norma del prodotto di numeri gaussiani è il prodotto delle norme e la definizione delle funzioni div′ e mod′. Il risultato è che la norma del resto si riduce almeno della metà rispetto a quella del divisore, grazie all’uso attento degli arrotondamenti e delle proprietà di queste funzioni.

Questa impostazione mostra anche una scelta metodologica tipica nella formalizzazione della matematica: quando un risultato richiede strumenti non ancora presenti in una libreria formale, si può scegliere di sviluppare nuovi concetti o di adattare le dimostrazioni per utilizzare solo ciò che è già disponibile. La seconda opzione spesso porta a prove più elementari e facilmente verificabili, sebbene meno immediate dal punto di vista concettuale.

Infine, è importante ricordare che la nozione di norma e la sua relazione con la divisione e il resto nei numeri gaussiani estendono profondamente i concetti aritmetici classici degli interi. Questo permette di studiare proprietà come la fattorizzazione unica in un contesto più ricco, che ha implicazioni profonde nella teoria dei numeri algebrica e nella crittografia. Comprendere queste costruzioni e le loro proprietà è quindi fondamentale per chi vuole addentrarsi nello studio rigoroso della struttura algebrica degli anelli quadratici.

Come si scrivono e si comprendono le dimostrazioni formali in Lean: l’uso del calc e delle tecniche di riscrittura

La formalizzazione delle dimostrazioni matematiche nel sistema Lean si basa su un insieme di strumenti che consentono di esprimere passaggi logici in modo rigoroso ma anche leggibile, superando la complessità delle singole riscritture. Un esempio tipico è la dimostrazione dell'identità $(a + b)^2 = a^2 + 2ab + b^2$. Scrivere questa dimostrazione tramite semplici riscritture (rw) è possibile, ma tende a generare un testo difficile da seguire. Per ovviare a questo problema, Lean introduce il costrutto calc, che consente di presentare il ragionamento come una catena ordinata di uguaglianze, ciascuna giustificata da un passo specifico.

Il blocco calc non inizia con by perché è esso stesso una costruzione di prova: è un termine che produce direttamente la dimostrazione, e può essere inserito anche all’interno di altri contesti di dimostrazione come un’istruzione per risolvere un obiettivo. La sintassi di calc è rigorosa: ogni passaggio richiede un’espressione, un segno di uguaglianza o di disuguaglianza, e la giustificazione associata, la quale può essere un altro termine di prova o una strategia tattica. Inoltre, l’indentazione è cruciale per delineare chiaramente i blocchi di ragionamento.

Oltre al calc, Lean mette a disposizione altre potenti tattiche, come rw per riscritture dirette e nth_rw per sostituire occorrenze specifiche di un’espressione nel contesto di una dimostrazione, affinando così il controllo sulle trasformazioni applicate. Inoltre, la tattica ring automatizza la verifica di identità in anelli commutativi: essa sfrutta gli assiomi dell’anello per risolvere uguaglianze complesse senza ricorrere a manipolazioni manuali.

La nozione astratta di anello in Lean viene definita tramite un tipo parametrizzato R dotato di una struttura Ring, che garantisce la validità di assiomi fondamentali quali l’associatività e la commutatività dell’addizione, l’esistenza dell’elemento neutro, l’esistenza dell’inverso additivo, e la distributività della moltiplicazione rispetto all’addizione. Lean consente di lavorare sia con anelli astratti sia con istanze concrete, come i numeri interi, razionali o complessi, garantendo che i teoremi dimostrati a livello astratto siano applicabili in contesti specifici.

È importante notare che non tutte le proprietà dei numeri reali si trasferiscono automaticamente a un anello generico: ad esempio, la commutatività della moltiplicazione non è garantita in ogni anello. Questa distinzione è cruciale quando si trattano strutture algebriche più complesse, come l’anello delle matrici quadrate, dove la moltiplicazione è associativa ma generalmente non commutativa.

Lean organizza definizioni e teoremi all’interno di namespace per evitare conflitti di nomi e facilitare la gestione di librerie di teoremi estese. Questa organizzazione risulta particolarmente utile quando si introducono versioni personalizzate di teoremi già presenti in Mathlib o si lavora su sviluppi specifici in contesti limitati.

L’importanza di comprendere a fondo la struttura sintattica e semantica delle dimostrazioni formali risiede nella possibilità di scrivere prove concise e leggibili, che siano al tempo stesso facilmente verificabili dal sistema. La scelta oculata delle tattiche da utilizzare, come il bilanciamento tra rw per riscritture puntuali, calc per ragionamenti strutturati e ring per automazione di algebra commutativa, è determinante per mantenere la leggibilità senza perdere potenza espressiva.

Un ulteriore aspetto da considerare è l’uso delle ipotesi nel contesto di una dimostrazione: Lean permette di applicare riscritture direttamente sulle assunzioni, trasformando l’ambiente di lavoro in modo dinamico e facilitando la progressione verso l’obiettivo finale. Questa manipolazione delle ipotesi è essenziale per affrontare dimostrazioni che coinvolgono equazioni o disuguaglianze definite nel contesto locale.

In conclusione, l’utilizzo combinato di strutture astratte come gli anelli, di tattiche di riscrittura, di costrutti formali come calc e di strumenti di automazione come ring costituisce la base per scrivere dimostrazioni matematiche formali efficaci e comprensibili in Lean. La conoscenza approfondita degli strumenti e delle loro peculiarità permette di ottenere un equilibrio tra formalismo rigoroso e leggibilità, caratteristica fondamentale per la diffusione e l’adozione di sistemi di dimostrazione automatica nella comunità matematica.

Come la struttura topologica risolve i limiti della teoria degli spazi metrici?

Per superare questi limiti, la teoria delle spazi topologici offre un quadro più generale e funzionale. È possibile “trasferire” topologie lungo qualsiasi funzione $f : X \to Y$, sia spingendo una topologia da $X$ a $Y$ (coinduzione), sia richiamandola da $Y$ a $X$ (induzione). Queste due operazioni formano una connessione di Galois e si comportano bene rispetto alla composizione delle funzioni: il push-forward è covariante, il pull-back è contravariante. Si utilizzano notazioni sintetiche $f_* T$ per la coinduzione e $f^* T$ per l’induzione della topologia.

Questa impostazione consente di recuperare la continuità delle funzioni tramite un confronto tra topologie indotte o coindotte: una funzione $f : X \to Y$ è continua se e solo se la topologia coindotta da $f$ su $Y$ è più fine della topologia già presente su $Y$. Da questa caratterizzazione segue naturalmente la proprietà universale della continuità rispetto alla composizione di funzioni, che rende possibile definire topologie quozienti e topologie prodotto in modo elegante e astratto.

Tuttavia, la generalità degli spazi topologici comporta anche la presenza di spazi con comportamenti patologici. Per avvicinarsi a una struttura più simile agli spazi metrici, si impongono condizioni di separazione, tra cui la più nota è la proprietà di Hausdorff (o $T_2$), che assicura unicità dei limiti. Proprietà più forti come $T_3$ garantiscono ulteriori regolarità, come la possibilità di avere basi di intorni chiusi per ogni punto, che si rivelano fondamentali nello studio delle estensioni di funzioni continue.

In definitiva, la teoria dei topological spaces risolve in modo sistematico i problemi irrisolvibili nel quadro degli spazi metrici, grazie a un impianto più flessibile e funzionale, che combina la struttura di reticolo completo con la capacità di trasferire topologie attraverso mappe generali e di definire prodotti e quozienti in modo coerente.

È importante che il lettore comprenda come questa astrazione non sia mera generalizzazione fine a se stessa, ma una necessità intrinseca per affrontare fenomeni complessi, quali funzioni a vari parametri o spazi di funzioni, che non ammettono una metrica compatibile con le nozioni di convergenza desiderate. Comprendere le proprietà di separazione e regolarità permette inoltre di ottenere risultati cruciali per l’estensione e la continuità delle funzioni, elementi chiave in molti sviluppi successivi della topologia e dell’analisi.

Come si dimostrano proprietà algebriche e logiche in sistemi formali come Lean?

Ad esempio, dimostrare che il prodotto di due numeri reali non negativi è non negativo, non è una semplice osservazione. All’interno di un anello ordinato, dove non si assume necessariamente la commutatività o la piena struttura dei numeri reali, si lavora a partire da assiomi più deboli. In tal modo, l’obiettivo è mostrare che molte proprietà note, come $0 \leq a$ e $0 \leq b \Rightarrow 0 \leq a \cdot b$, possono essere dedotte genericamente.

Nella logica formale, l’implicazione e il quantificatore universale sono strumenti chiave per costruire affermazioni matematiche complesse. Una frase come “per ogni numero reale $x$, se $x \geq 0$ allora $|x| = x$” si esprime formalmente come ∀ $x : \mathbb{R}$, $0 \leq x \rightarrow |x| = x$. Ciò che in matematica si dice a parole, qui viene codificato e trattato come una struttura manipolabile all’interno del sistema.

Un esempio significativo è quello di un lemma che afferma che, date certe condizioni su tre variabili $x$, $y$, ed $\varepsilon$, il valore assoluto del loro prodotto resta al di sotto di $\varepsilon$. La costruzione di questo tipo di lemma non è soltanto un esercizio di algebra, ma un esercizio di gestione delle ipotesi, delle variabili implicite, e dell’ordine logico delle affermazioni.

Altro aspetto centrale è la definizione e l’uso di predicati, come FnUb e FnLb, che rappresentano il concetto di maggiorante e minorante per una funzione. Definire che $a$ è un maggiorante della funzione $f$ significa formalmente che per ogni $x$, $f(x) \leq a$. Allo stesso modo per i minoranti. Queste definizioni vengono poi utilizzate per dimostrare proprietà su combinazioni di funzioni, come somma e prodotto, sfruttando le proprietà dell’ordine.

Importante è anche la capacità del sistema di trattare lambdas e funzioni anonime, cioè definizioni di funzioni date sul momento, e gestirle come oggetti matematici a tutti gli effetti. La semplificazione di espressioni (mediante comandi come dsimp) e il controllo fine della forma delle ipotesi (mediante change) diventano strumenti essenziali per orientarsi nella complessità delle trasformazioni formali.

Comprendere questo linguaggio logico e strutturato non significa solo saper usare un assistente formale. Significa anche imparare a vedere la matematica da un punto di vista inferenziale, dove ogni passaggio, anche il più semplice, ha un ruolo preciso e va giustificato nel contesto delle ipotesi disponibili.