🧮 Fundações matemáticas

O PAEBIRU é um sistema distribuído termodinamicamente fundamentado. Esta página é o índice das ferramentas matemáticas que sustentam os principais protocolos. As provas formais vivem em crates/*/formal/ (TLA+ para concorrência, Lean 4 para pureza).

Sumário

1. Equações de Langevin
2. Hamiltoniano de Ising
3. Reed-Solomon sobre Corpos de Galois
4. Dotted Version Vectors (DVV)
5. Fórmula de Haversine
6. Análise Topológica de Dados (TDA)
7. Backpressure M/M/1
8. Groth16 (zk-SNARKs)
9. Verificação formal

Equações de Langevin

A dinâmica de Langevin governa o “tempo” do PAEBIRU:

$$ m , \frac{dv}{dt} = -\gamma v + \sqrt{2D} , \xi(t) + F_{\text{ext}} $$

Implicação para o scheduler: um Langevin Tick só avança quando a entropia local varia ($\Delta S \neq 0$). Sem variação, o sistema “congela” — por isso o regime v3+ chama-se Dança Politemporal (tópico em formalização; ainda sem número de RFC atribuído, conforme a regra de ouro do processo).

Modelo formal em Lean 4: crates/paebiru-math/formal/lean/Langevin.lean.

Hamiltoniano de Ising

Usado pelo scheduler de enxame e pelo consenso bizantino adaptativo. Modelo $N$ spins em rede $d$-dimensional:

$$ \mathcal{H} = -J \sum_{\langle i,j \rangle} s_i s_j - h \sum_i s_i, \quad s_i \in {-1, +1} $$

Onde:

• $J$ = acoplamento (positivo: ferromagnético; negativo: vidro de spin).
• $h$ = campo externo (urgência do scheduler).
• $\langle i, j \rangle$ = pares de vizinhos na malha.

O Ising solver (Fase 4) usa annealing simulado em paebiru-math para encontrar configurações de baixa energia — mapeando “tarefas” para “spins” e “custo” para “acoplamento”.

Reed-Solomon sobre Corpos de Galois

Usado em C.A.P.I.B.A. para reconstrução de blocos perdidos e correção de erros no WAL distribuído.

Dado mensagem $m = (m_0, \ldots, m_{k-1})$ em $\mathrm{GF}(2^8)$:

1. Codifica em polinômio $p(x) = m_0 + m_1 x + \cdots + m_{k-1} x^{k-1}$.
2. Avalia em $n$ pontos ($\mathrm{GF}(2^8)^* \cup {0}$).
3. Distribui $n$ símbolos; recupera com $k \leq n’ < n$ (decodificação de Berlekamp-Welch ou Sugiyama).

Por que RS, não LDPC? O custo de decodificação em MCUs é proibitivo para LDPC; RS é tabelável em ROM de 2 kB.

Prova formal em Lean 4: crates/paebiru-math/formal/lean/ReedSolomon.lean.

Dotted Version Vectors (DVV)

Um DVV é um mapeamento de identificadores de evento para contadores, estendendo Causal Version Vectors com a noção de “discrete snapshot”.

$$ D_v : \text{EventId} \to \mathbb{N}, \quad D_v(\text{evento}) = \text{contador no produtor} $$

• $D_v \sqsubseteq D_w$ significa “DVV $v$ é causalmente anterior a $D_w$”.
• União por componente: $D_v \sqcup D_w$ é o least upper bound.
• Maturidade Causal de um evento $e$ é a condição $D_e \sqsubseteq D_{\text{local}}$, isto é, todos os seus dependentes foram observados localmente.

tópico em formalização — referência normativa.

Fórmula de Haversine

Distância geodésica entre dois pontos na esfera ($\oplus$ = Terra, raio $R = 6371{,}0088$ km):

$$ d = 2R \cdot \arcsin!\left(\sqrt{\sin^2!\left(\frac{\Delta\phi}{2}\right) + \cos\phi_1 \cos\phi_2 \sin^2!\left(\frac{\Delta\lambda}{2}\right)}\right) $$

Usada em:

• PoL (ZK-PoL): circunscrição de raio garantido.
• Scheduler de proximidade: priorizar peers geograficamente próximos em redes LoRa (limites de tempo de propagação).

Implementação no_std em paebiru-math::geo::haversine_distance. Prova formal em Lean 4: Haversine.lean.

Análise Topológica de Dados (TDA)

Usada para detectar mudança de regime no comportamento da malha (saturação, deriva, partição).

A ferramenta central é a homologia persistente: dada uma nuvem de pontos $(x_i) \in \mathbb{R}^d$, constrói-se uma família de complexos simpliciais (Vietoris-Rips) e computa-se a persistência de cada classe homológica ($\beta_0$, $\beta_1$).

• Classes de vida longa → estrutura topológica real.
• Classes de vida curta → ruído.

Em Rust, integração com rust_tda (Fase 4) ou com bindings para gudhi (Python).

Modelagem de filas M/M/1

Para dimensionar buffers, backpressure e latência do ZeroTrustPipeline.

Consulte queues-model.md para a derivação completa de Little, Pollaczek-Khinchine e o regime de Langevin adaptativo.

Groth16 (zk-SNARKs)

zk-SNARK de referência usado no ZK-PoL. Setup confiável $S$ produz:

• Chave de prova: $\text{pk} \in \mathbb{G}_1^{n+l} \times \mathbb{G}_2^{n}$.
• Chave de verificação: $\text{vk} \in \mathbb{G}_1 \times \mathbb{G}_2^2$.
• Prova: $\pi \in \mathbb{G}_1 \times \mathbb{G}_2$.

Para o PoL, o circuito verifica: “a posição $p$ está dentro do disco de raio $r$ centrado em $c$, sem revelar $p$ nem $c$.”

Curvas alvo: BN254 (default) e BLS12-381 (Fase 4). Mais em BC ZK.

Verificação formal

A verificação formal do PAEBIRU é cirúrgica: TLA+ para concorrência e estado global, Lean 4 para pureza algorítmica.

Acionada por make verify-formal.

Veja também

• Dicionário canônico — termos, não fórmulas.
• Filas M/M/1 — modelagem detalhada de filas.
• Padrões — receitas algorítmicas recorrentes.
• Verificação formal (guia de contribuidor).