O ambiente de verificação formal da série Principia Orthogona.
The formal verification environment for the Principia Orthogona series.
AXLE é o ambiente de verificação formal da série Principia Orthogona.
Escrito em Lean 4 com Mathlib4, ele traduz as afirmações matemáticas dos
cinco volumes em obrigações verificáveis por máquina. Cada constante,
cada lema, cada cadeia de operadores tem um análogo em Lean —
provado ou marcado honestamente com
sorry.
Nada no AXLE é decorativo. Se uma constante aparece em prosa — g33=33,
ε0=⅓, κ≤√(7/9), T★=2π — ela aparece
também como um theorem
em Main.lean, fechado por rfl,
decide ou
norm_num — ou
por um sorry nomeado,
catalogado no Cap 3.
AXLE is the formal verification environment for the Principia Orthogona
series. Written in Lean 4 with Mathlib4, it translates the mathematical
claims of the five volumes into machine-checkable obligations. Every
constant, every lemma, every operator chain has a Lean analogue —
proved, or honestly marked with
sorry.
Nothing in AXLE is decorative. If a constant appears in prose —
g33=33, ε0=⅓, κ≤√(7/9), T★=2π —
it also appears as a
theorem
in Main.lean, closed by
rfl,
decide, or
norm_num —
or by a named
sorry,
catalogued in Cap 3.
sorry.
— AXLE v6.1 · README
O nome AXLE vem de "Algebraic eXpression Language for Evaluation." O eixo é o ponto em torno do qual a série gira — o ponto fixo G(x★)=x★ do Teorema de Banach aplicado a si mesmo.
AXLE v6.1 é o estado atual: versão 6 (alinhada ao G⁶), patch 1. Cada patch fecha ou refina sorrys sem alterar os enunciados — a numeração da versão acompanha a hierarquia g-série da série, não apenas o ritmo de desenvolvimento do código.
The name AXLE comes from "Algebraic eXpression Language for Evaluation." The axle is the point around which the series turns — the fixed point G(x★)=x★ of the Banach theorem applied to itself.
AXLE v6.1 is the current state: version 6 (aligned with G⁶), patch 1. Each patch closes or refines sorrys without changing the statements — the version number tracks the series' g-series hierarchy, not just the development pace of the code.
O repositório é público. As 8 constantes verificadas estão no Cap 2; os 9 sorrys honestos, nomeados e catalogados, no Cap 3; a conjectura G⁶ aberta — χ(H*(X⁶))=33 ∀n — é o horizonte de Issue 6.
-- Main.lean — entry point
-- 8 constants : proved (rfl / decide / norm_num)
-- 9 sorrys : named, catalogued, Cap 3
-- 1 conjecture : Issue 6 — open horizon, G⁶
theorem AXLE_v6_1_status : verified = 8 ∧ sorry_count = 9 := by decide
The repository is public. The 8 verified constants are in Cap 2; the 9 honest sorrys, named and catalogued, in Cap 3; the open G⁶ conjecture — χ(H*(X⁶))=33 ∀n — is the Issue 6 horizon.
AXLE is the bridge between the prose of Volumes I–V and a machine that checks it. Reading the prose without the Lean status — or reading the Lean status without the prose — gives only half the book. The axle is where both halves meet.