O modelo estava errado. O compilador não. O zero silencioso era a mentira.

Manhã · o modelo

A subject reduction era falsa. Isso é um facto do cálculo, não do Madaros.

O #1772 provou um contra-exemplo de preservação. O #1779 registou o veredicto: measure a colapsar o payload para Real é um defeito de EpistemicEffects.lean, não uma escolha da linguagem. O checker (`checker_check_measure_expr_inplace`) mete o tipo do argumento em ty_knowledge — measure de um Nat é Knowledge<Nat>. O CLAUDE.md já dizia que measure() rende Knowledge<mg>. O #1780 fechou a correspondência e deixou o modelo V1 refutado sob um aviso. Não cites EpistemicEffects.lean como metateoria. É um modelo refutado.

Tarde · o instrumento

Um programa bem tipado recusa. A prova, usada como lâmpada, achou dois sítios que ainda fabricavam.

O #1788 provou, no fragmento E219 e sem sorry, refusal_is_not_zero e well_typed_value_or_refuse. Esse ficheiro é um modelo. Não prova que check.sio o implementa — o portão pára em E4 e diz-o. A mesma tarde o modelo foi virado contra o compilador: o #1801 fechou os dois sítios que ainda fabricavam depois de uma recusa. abs() + 1 é ty_error(), não i64. Um stub IR vazio emite ud2, não um 0 por queda. O lean_single continua sem E219. Uma banda de Cmin de vancomicina que não está dentro de [10, 20] é PRE_REFUSE — a mesma tese, numa dose.

19extern "C" {
20    fn malloc(size: i64) -> i64;
21    fn abs(x: i64) -> i64;
22}
23
24fn main() -> i64 with IO {
25    let p = malloc(64)
26    print_int(p)
27    print_int(abs(0 - 7))
              ^^^
28    0
29}

Noite · a mesma ausência

Quatro lanes. Uma classe. Um valor plausível onde pertencia uma ausência declarada.

Às 01:00 UTC de 18 de agosto, #1830, #1825, #1829 e #1823 tinham aterrado de quatro lanes que não partilhavam write-set. pin_count era lido como 0 pins vivos; o emissor nunca o incrementa — o sentinela é agora −1, UNWIRED. CALL era recusada só como opcode desconhecido; agora tem nome, MLI_I_CALL_UNSPECIFIED, e has_value=false. O FabricatedDatum deu cara ao quinto estado. O muro de reclamation embarcou a testemunha antes do conserto: o gate está vermelho de propósito aos 4 194 304 allocations (rc=182). O #1792 continua aberto na superfície da dissertação. A classe não está fechada. Está, finalmente, visível.

0

-1

Noite · a classe, rasgada

Estas três caras são a razão de quatro lanes se terem reconhecido.

Um zero que o outro motor não dá. Um inteiro vestido de ε. Um diagnóstico cortado a meio da palavra. O medidor continua a recusar o numeral falso. O FabricatedDatum (#1829) mostra as duas caras e não rasga quando são a mesma string. Os dois primeiros recibos são o #1792. O censo do corte é o #1794.

0.000000 #1792 4604219396932172800 #1792 33 > 127 #1794

0.000000

~1e-5

4604219396932172800

0.671038

   |
   = help: only these body-less names are implemented: print, print_int, print_char, print_f64, get_arg, get_arg_count, st

r_len, str_char_at, str_eq, str_slice, starts_with, str_concat, str_from_bytes, read_file, write_file, file_size, sqrt, exp, log, sin, cos, assert, heap_alloc, heap_free, f64_to_bits, bits_to_f64, syscall6