# PORTA -- `Um (absoluto) — Grande Atrator/Lean/tgl_kernel`

porta acima: https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/Um%20%28absoluto%29%20%E2%80%94%20Grande%20Atrator/Lean/PORTA.md

> **A REGRA DA PORTA.** Toda pasta canonica tem `PORTA.md` + `PORTA.json`;
> toda porta aponta para cima e para baixo. Todo link abaixo e' a URL raw
> DIRETA do arquivo -- nao ha nome de pasta para adivinhar.

O KERNEL FORMAL: as fontes .lean exatamente como `um.py` as materializa a cada
rodada -- nao ha segundo arquivo: o kernel mora DENTRO do canonico e sai dele.

**1215 arquivos** nesta arvore; **1215** hasheados no manifesto formal (1211 `.lean`
+ `README.md` + `lakefile.toml` + `lean-toolchain`); **10256 teoremas** auditados
por `#print axioms`, bases de axiomas subset de {`propext`, `Classical.choice`,
`Quot.sound`}, zero `sorry`. Toolchain `leanprover/lean4:v4.31.0`, modo `strict`.

O manifesto e' a fonte desses numeros -- nunca a prosa:
[`tgl_kernel_proof_manifest.json`](https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/Um%20%28absoluto%29%20%E2%80%94%20Grande%20Atrator/Lean/tgl_kernel_proof_manifest.json).

Sem Lean o rito declara `FORMAL_CHECKER_UNAVAILABLE` e **recusa selar**:
o gate nao se move por declaracao.

## A PORTA ACIMA

| destino | link |
|---|---|
| PORTA.md da pasta acima (`Um (absoluto) — Grande Atrator/Lean`) | https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/Um%20%28absoluto%29%20%E2%80%94%20Grande%20Atrator/Lean/PORTA.md |
| PORTA.json da pasta acima | https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/Um%20%28absoluto%29%20%E2%80%94%20Grande%20Atrator/Lean/PORTA.json |
| PORTA.md da RAIZ | https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/PORTA.md |
| `llms.txt` (a porta de entrada para IA) | https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/llms.txt |
| `README.md` (o atlas da fronteira) | https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/README.md |
| o site | https://teoriadagravitacaoluminodinamica.com |
| o repositorio | https://github.com/rotolimiguel-iald/the_boundary |

## OS ARQUIVOS DESTA PASTA

7 arquivo(s) -- pasta no GitHub: https://github.com/rotolimiguel-iald/the_boundary/tree/main/Um%20%28absoluto%29%20%E2%80%94%20Grande%20Atrator/Lean/tgl_kernel

**PROVA FORMAL**

| arquivo | papel | link raw direto |
|---|---|---|
| `TGL.lean` | A raiz da biblioteca TGL (importa os modulos base) | [raw](https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/Um%20%28absoluto%29%20%E2%80%94%20Grande%20Atrator/Lean/tgl_kernel/TGL.lean) |
| `TGLExt.lean` | A raiz da biblioteca TGLExt (importa a extensao: onde vivem as pedras) | [raw](https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/Um%20%28absoluto%29%20%E2%80%94%20Grande%20Atrator/Lean/tgl_kernel/TGLExt.lean) |
| `_check_damming.lean` | Prova formal (Lean 4): _check_damming | [raw](https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/Um%20%28absoluto%29%20%E2%80%94%20Grande%20Atrator/Lean/tgl_kernel/_check_damming.lean) |

**DOCUMENTO**

| arquivo | papel | link raw direto |
|---|---|---|
| `README.md` | Como construir e auditar o kernel Lean 4 materializado por um.py | [raw](https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/Um%20%28absoluto%29%20%E2%80%94%20Grande%20Atrator/Lean/tgl_kernel/README.md) |

**OUTROS**

| arquivo | papel | link raw direto |
|---|---|---|
| `lake-manifest.json` | O pin do mathlib usado pelo kernel | [raw](https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/Um%20%28absoluto%29%20%E2%80%94%20Grande%20Atrator/Lean/tgl_kernel/lake-manifest.json) |
| `lakefile.toml` | A configuracao lake do kernel | [raw](https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/Um%20%28absoluto%29%20%E2%80%94%20Grande%20Atrator/Lean/tgl_kernel/lakefile.toml) |
| `lean-toolchain` | O pin do toolchain Lean (leanprover/lean4:v4.31.0) | [raw](https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/Um%20%28absoluto%29%20%E2%80%94%20Grande%20Atrator/Lean/tgl_kernel/lean-toolchain) |

## AS PORTAS ABAIXO

| subpasta | arquivos | PORTA.md | PORTA.json |
|---|---|---|---|
| `TGL/` | 27 | [PORTA.md](https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/Um%20%28absoluto%29%20%E2%80%94%20Grande%20Atrator/Lean/tgl_kernel/TGL/PORTA.md) | [PORTA.json](https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/Um%20%28absoluto%29%20%E2%80%94%20Grande%20Atrator/Lean/tgl_kernel/TGL/PORTA.json) |
| `TGLExt/` | 1181 | [PORTA.md](https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/Um%20%28absoluto%29%20%E2%80%94%20Grande%20Atrator/Lean/tgl_kernel/TGLExt/PORTA.md) | [PORTA.json](https://raw.githubusercontent.com/rotolimiguel-iald/the_boundary/main/Um%20%28absoluto%29%20%E2%80%94%20Grande%20Atrator/Lean/tgl_kernel/TGLExt/PORTA.json) |

---

gerado por script de git ls-files em 2026-10-06 -- nao editar a mao