CPFormal v0.63.0 — Tilt cofinal e gate exato do carrier C3

CPFormal v0.63.0 — tilt cofinal e gate exato do carrier C3

Estado da release

• release pai: v0.62.0;
• tag anotada: v0.63.0;
• Lean e Mathlib: v4.32.0;
• Zenodo concept DOI estável: 10.5281/zenodo.21483474.

Esta release consolida três resultados posteriores à correção semântica de
v0.62.0. Ela não altera a definição de zero e não introduz a meia-abscissa
como hipótese de anulação.

Proveniência mínima

O módulo CpMinimalProvenanceQuotient constrói o quociente canônico que
preserva simultaneamente o readout coarse e a informação Green. A construção
não escolhe pseudoinversa nem representante e identifica exatamente a
proveniência apagada pelo quociente coarse.

Não compensação da cauda de tilt

Para todo parâmetro no strip aberto com parte real diferente de 1 / 2, o
primeiro centro C3 completo domina estritamente todos os centros de tilt
posteriores. A constante explícita é

$$\rho=\frac34\left(\frac65\right)^{3/2}, \qquad \rho^2=\frac{243}{250}<1.$$

Logo a série cofinal dos blocos de tilt não se autocancela fora do equilíbrio.
O teorema é anterior a qualquer hipótese de zero.

Ledger exato do carrier

Para o tilt cofinal W_infinity, o remainder do carrier R_infinity e o
fator não nulo da câmera C3, Lean prova universalmente

$$1+W_\infty(s)+R_\infty(s) =a_3(s)\,\mathrm{Genuine}(s).$$

Consequentemente, no strip,

$$1+R_\infty(s)=-W_\infty(s) \quad\Longleftrightarrow\quad \mathrm{Genuine}(s)=0.$$

Isso identifica o gate restante sem escondê-lo: proibir globalmente essa
compensação é equivalente à não anulação forte no strip. A release não declara
essa equivalência como prova do lado ainda aberto.

Escopo lógico

A release prova que a cauda de centros completos do próprio tilt não apaga o
defeito central. Ela também prova que completude celular, C0 e simples
reassociação escalar não fornecem, sozinhas, uma ortogonalidade do carrier.
Uma conclusão adicional precisa usar coerência do estado completo, endpoint e
bulk, e não redefinir zero como compatibilidade de massa.

Verificação

O artefato publicável é o commit exato de main que passa:

bash scripts/static_audit.sh
lake build --wfail

A tag e a GitHub Release são criadas somente depois do workflow Lean verde
nesse mesmo SHA. A release do GitHub é o evento de arquivamento consumido pela
integração do Zenodo.

CPFormal v0.62.0 — Correcao semantica do zero nativo

CPFormal v0.62.0 — correção semântica do zero nativo

Estado da release

• release pai: v0.61.0;
• tag anotada planejada: v0.62.0;
• Zenodo concept DOI estável: 10.5281/zenodo.21483474.

Esta é uma release corretiva. A tag histórica v0.61.0 permanece imutável;
a v0.62.0 publica a API ativa já corrigida e fornece a versão canônica para
novos consumidores.

Resultado

O zero nativo volta a significar exatamente anulação da câmera:

def IsNativeCarryRealOperatorZero
    (camera : ℕ) (sigma time : ℝ) : Prop :=
  NativeCarryRealOperatorBoundaryClosesAt camera sigma time

Compatibilidade de massa não integra essa definição. A arquitetura formal é:

carry/massa       -> equilíbrio quadrático sigma = 1/2
câmera/Genuine    -> anulação
centro Green      -> diagnóstico do deslocamento sigma - 1/2

Identidade de zeros no strip

Para todo s no strip Genuine aberto, o Lean prova:

IsNativeCarryRealOperatorZero 3 s.re s.im
  ↔ genuineContinuation s = 0

Não existe hipótese s.re = 1/2 nesse teorema. A embalagem complexa também
preserva o mesmo predicado de zero para todo sigma.

Separação Green fora do equilíbrio

O operador completado possui dois canais independentes. No mesmo strip:

genuineGreenCompletedLimitOperator p q s = 0
  ↔ IsNativeCarryRealOperatorZero 3 s.re s.im ∧
      s.re = (1 : ℝ) / 2

Portanto, se for apresentado um zero nativo/Genuine com
s.re ≠ (1 : ℝ) / 2, o zero não é revogado. O teorema
nativeZero_offEquilibrium_channelSeparation conclui:

canal Genuine = 0
canal Green   ≠ 0

O Green denuncia o tilt; ele não redefine a anulação.

Migração da API

Símbolos e leituras anteriores devem ser migrados assim:

Forma anterior	Forma canônica na v0.62.0
zero como MassCompatible ∧ BoundaryCloses	IsNativeCarryRealOperatorZero, somente fechamento
NativeCarryRealPlaneAdmissibleFiniteZero	separar compatibilidade de massa da hipótese de zero
NativeCarryRealPlaneAdmissibleBoundaryClosesAt	separar compatibilidade de massa de NativeCarryRealOperatorBoundaryClosesAt
“zero fora de 1/2 não é zero”	zero preservado; canal Green não nulo fora do equilíbrio
promoção Genuine → zero nativo	identidade direta dos predicados no strip

Os módulos-folha que apresentavam confinamento como parte da semântica do
zero foram removidos da API ativa. O script scripts/static_audit.sh rejeita
a reintrodução dos símbolos obsoletos e rejeita MassCompatible dentro da
definição pública de zero.

Escopo lógico

Esta release não afirma que exista um zero fora da meia-abscissa e não afirma
que todos os zeros estejam nela. Ela prova e preserva a distinção necessária
para qualquer investigação posterior:

equilíbrio não é definição de zero;
zero não apaga o diagnóstico Green;
diagnóstico Green não revoga um zero.

Verificação e publicação

O workflow da release executa, sobre o commit exato de main:

• auditoria estática da API e dos imports;
• testes numéricos de regressão;
• lake build --wfail pelo kernel Lean;
• construção e restauração de um bundle Git completo;
• comparação do manifesto de refs e verificação SHA-256 dos artefatos.

Somente depois dessas etapas o workflow cria a tag anotada, publica a GitHub
Release e emite o evento consumido pela integração do Zenodo.

Consulte também
NATIVE_ZERO_SEMANTICS_CORRECTION.md
para a justificativa formal detalhada.

CPFormal v0.61.0 — Confinamento nativo por tilt e remocao da Hipotese de Riemann

CPFormal v0.61.0 — Confinamento nativo por tilt e remoção da Hipótese de Riemann

Esta versão alinha o repositório com a lei Genuine First: a teoria nasce do
carry (massa → operador de ramo → amplitude → norma quadrática → bracket →
tilt), o confinamento dos zeros é uma positividade de curvatura de dois
lados, e nenhum teorema fala de Hipótese de Riemann.

Novidades

Tilt nativo: o confinamento como curvatura de dois lados

Novo módulo CPFormal/Analytic/CpCarryTiltBracket.lean (sem zeta, sem número
complexo, sem continuação):

• carryBracket2 f c = f(c-1) + f(c+1) - 2 f(c) — segunda diferença centrada;
• carryTilt δ x = x^(-δ) — o peso de carry inclinado por δ;
• carryTiltBracket δ c — a curvatura do peso inclinado;
• carryTiltBracket_eq_zero_iff — a curvatura anula-se ⇔ δ = 0;
• carryTiltBracket_criticalDisplacement_confines — a tricotomia
  (δ = σ - 1/2):
  • σ < 1/2 ⟹ curvatura < 0 (peso estritamente côncavo);
  • σ = 1/2 ⟹ curvatura = 0;
  • 1/2 < σ ⟹ curvatura > 0 (peso estritamente convexo).

O único expoente com curvatura nula é 1/2, e a exclusão vale nos dois lados
por igual — não por uma simetria σ ↦ 1-σ, mas porque o peso curva
definidamente para um lado abaixo da linha e para o outro acima. Confinamento é
positividade de curvatura, não reflexão.

Substituição da equação funcional pelo tilt

CPFormal/Analytic/CpGenuineSimpleRootCarryState.lean deixa de usar a equação
funcional da zeta completa (completedRiemannZeta_one_sub) para transportar a
simplicidade refletida. Como nativamente não existe simetria σ ↦ 1-σ, a
simplicidade refletida passa a ser o quarto campo explícito de
IsSimpleGenuineZeroInStrip — uma hipótese visível, não um fato emprestado da
zeta. O arquivo não referencia mais riemannZeta / completedRiemannZeta.

Remoção completa da Hipótese de Riemann

Removidos os dois arquivos-folha que faziam afirmações sobre RH:

• CpMathlibRiemannHypothesisPromotion (… ↔ RiemannHypothesis);
• CpPrimitiveGenuineZetaZeroSet (zero Genuine ↔ zero de riemannZeta).

O repositório passa a ter zero ocorrências de RiemannHypothesis. O
resultado nativo nativeCarryRealPlaneBoundaryClosurePreservesMass_iff_zeroRigidity
(sem RH) permanece, auto-contido.

Escopo honesto

Esta versão não é a remoção total de zeta. Dois arquivos ainda mencionam a
riemannZeta analítica como ponte de continuação, não como afirmação de RH:

• CpGenuineRiemannZetaIdentification — a continuação analítica do
  genuineContinuation é obtida identificando a série de Dirichlet nativa com a
  riemannZeta do Mathlib (cuja analiticidade o Mathlib prova). Removê-la
  exigiria re-derivar a continuação analítica do zero.
• CpNativeCarryMobiusLogDerivativeGuardrail — a inversão de Möbius/von Mangoldt
  (mostra que a informação dos primos vem da inversão sobre a não-dependência
  dos zeros com os primos); fora do escopo da prova principal.

O confinamento nativo (massa↔amplitude e curvatura↔tilt) e o operador real/
complexo não dependem de zeta.

Verificação

• lake build --wfail — verde, sem warnings.
• Núcleo axiom-clean [propext, Classical.choice, Quot.sound], sem sorry.
• Testes de regressão Python (rotação real e operador de ramo/tilt) — OK.
• Auditoria estática — imports locais resolvidos; sem axiom/sorry/admit
  locais.

Um laboratório numérico finito não substitui a elaboração pelo kernel Lean; os
mínimos de grade não são prova sobre o limite infinito.

CPFormal v0.60.0 — Fontes G_pre finitas explicitas e preservacao raw completa

CPFormal v0.60.0 — Fontes G_pre finitas explicitas e preservacao raw completa

Estado da release

• release pai: v0.59.0;
• tag anotada planejada: v0.60.0;
• Zenodo concept DOI estavel: 10.5281/zenodo.21483474.

O workflow da release cria a tag somente no commit exato de main que passou
pela auditoria estatica, pelos testes numericos, pelo kernel Lean e pela
restauracao do bundle completo. A publicacao da GitHub Release e o evento
consumido pela integracao Zenodo para atribuir o DOI imutavel desta versao.

O carry continua anterior aos observaveis

A teoria estrutural permanece quantificada sobre toda base inteira b>1.
Primos aparecem em certas cameras Cp e nos readouts Green como observaveis do
mesmo carrier; eles nao originam a massa critica, a meia-abscissa ou a
persistencia do carry.

O kernel ja separa os escopos:

base material e carry:                 b >= 2
cartas naturais analiticas:            b >= 2
cameras naturais nao degeneradas:      b >= 3
especializacao Green Cp desta release: p : Nat.Primes

A C2 alinhada continua sendo o detector local de raio 1, com uma perna de
cada lado. Sua implementacao pelo parametro nativo 4 nao a identifica com
uma C4 geometrica de duas pernas por lado.

Extracao finita base-neutra

O novo modulo CpNativeGpreFiniteTowerCollapse fatora literalmente cada
coordenada tipada de proveniencia G_pre em:

kernel aritmetico/canto/orientacao/role
  * perfil material da torre.

Ele constroi a fonte adjunta no nivel material e prova que o inner product com
o perfil da mesma base e tempo recupera exatamente o readout real. A identidade
vale para uma coordenada, para uma fibra finita e para pesos complexos
arbitrarios escolhidos antes da leitura. Peso zero produz readout zero.

Os campos legados towerPrime e arithmeticPrime sao rotulos ℕ; eles nao
carregam um certificado de primalidade. Portanto esta extracao nao restringe o
carry aos primos.

Fonte TFVD--log-jet--Green nao vacua

O modulo CpNativeGpreTfvdCommutatorTowerSource aplica a extracao ao wedge
refletido ordinario/log-jet. A formulacao dos drafts #40/#42 exigia uma
coordenada ativa na celula zero, mas o proprio kernel prova que toda coordenada
nativa nessa celula e zero. A release nao conserva essa contradicao como
premissa ativa.

O reparo construtivo usa, para a aresta analitica n:

celula nativa = p * (n + 1)
nivel material = n + 1.

O Lean prova que a coordenada canonica e ativa para todo observavel primo p,
tempo tau e aresta n. Em seguida, prova sem atlas assumido que a soma finita
das fontes tem como momento exatamente o trace normalizado do comutador e,
para 3*M arestas, exatamente o bulk Green log-jet finito existente.

Os quatro valores usados no wedge sao o canal ordinario e o log-jet em s,
mais os dois canais no parametro refletido. Eles nao sao quatro pernas
geometricas. O resultado e finito e camera-a-camera.

Ponto cego global sem perda de energia

O checkpoint anterior permanece ativo. Para s na faixa critica:

genuineContinuation s = 0
  <-> todas as cameras naturais b >= 3 sao cegas em s.

Nesse locus, para cada base fixa, a sequencia de resultantes finitas converge a
zero; essa afirmacao nao e uniforme em b. Ao mesmo tempo,
infiniteReflectedGreenEnergy_pos mantem uma serie Green refletida construida
independentemente estritamente positiva. A nova fonte finita explicita realiza
o bulk radial vezes o pareamento Green dentro de cada camera; ela nao identifica
a energia positiva isolada nem as fontes de cameras distintas como um unico
estado pre-compressao.

Preservacao sem perda

Esta release incorpora:

• as normalizacoes verdes mais recentes dos PRs #40/#42;
• o reparo nao vacuo da fonte de comutador;
• o registro unico ops/v0.56.0-preservation-confirmed.json, incluindo o DOI
  Zenodo 10.5281/zenodo.21735211;
• as 22 fontes recuperadas em forma byte-exata sob
  docs/recovered/2026-08-01/raw/, com manifesto SHA-256;
• o manifesto pos-v0.59 de branches, PRs, resultados ativos e workflows
  historicos deliberadamente nao reativados.

Nenhuma branch historica e apagada. O publisher busca todas as branches, tags
e refs de heads de pull requests, constroi um bundle completo, restaura um
mirror limpo, executa git fsck --full --strict, compara os manifests de refs
e publica seis assets protegidos por SHA-256.

O que esta release nao afirma

Esta release nao prova:

• que as fontes finitas de cameras diferentes formem um unico estado;
• uma cota uniforme ou passagem ao limite desses estados;
• que um zero Genuine anule o tilt, o bulk ou o fluxo Green;
• GenuineStrongNonvanishingInStrip;
• RiemannHypothesis da Mathlib;
• o GREEN-NATCAM-INTERTWINER;
• um operador de Hilbert--Polya.

Ela prova uma etapa de proveniencia genuinamente nova: cada bulk Green log-jet
finito da especializacao Cp e um momento nativo de uma fonte explicita,
construida das arestas antes da leitura e apoiada em coordenadas positivas e
distintas. A meia-abscissa continua vindo da convexidade/concavidade do carry;
nenhum estado e escolhido a partir da conclusao.

Protocolo de publicacao

Antes de publicar, o workflow v0.60.0 executa:

bash scripts/static_audit.sh

python -m unittest -v \
  experiments/test_c2_real_rotation_operator.py \
  experiments/test_c2_real_rotation_minimal.py \
  experiments/test_cp_branch_tilt_operator.py

lake build --wfail

Somente depois de todos os checks verdes e da restauracao integral do bundle o
workflow cria a tag anotada no main auditado, publica a release com o corpo
deste arquivo e verifica por attestation ou por download mais SHA-256 os seis
assets de recuperacao.

CPFormal v0.59.0 — Carry-first active integration and immutable mirror

CPFormal v0.59.0 — Carry-first active integration and immutable mirror

Release status

• parent release: v0.58.0;
• release branch: agent/v059-active-integration;
• planned annotated tag: v0.59.0;
• stable Zenodo concept DOI: 10.5281/zenodo.21483474.

The release workflow is the authority for the exact main commit tagged by
v0.59.0. It refuses to publish if the checked-out commit is not the current
remote main, if the static audit fails, if any Python regression fails, or if
lake build --wfail does not elaborate the full Lean project.

Reconciliation after the immutable v0.58.0 checkpoint

The v0.58.0 preservation release retained every draft head in the Git object
graph, but several draft theorems were intentionally absent from its active
checkout. This release performs the second, semantic half of preservation: it
merges the green, non-circular content into the active main tree while keeping
all v0.56.0–v0.58.0 workflows, notes, tags and recovery artifacts intact.

The publisher again constructs a complete bundle of all branch, tag and
pull-request refs, restores it into a fresh mirror, runs git fsck --full --strict, compares ref manifests and checksum-protects the recovery assets
before publishing the immutable release. Thus both meanings of “do not lose
anything” are checked: historical reachability and active kernel integration.

Carry comes first

This checkpoint preserves the causal order of the theory:

positional carry and its quadratic mass
  -> critical displacement delta = sigma - 1/2
  -> convexity / concavity of x^(-delta)
  -> signed Cp tilt
  -> cpTiltAtSigma = 0 iff sigma = 1/2.

The half-abscissa is not introduced by a Hilbert-state existence assumption.
The existing kernel theorem cpTiltAtSigma_eq_zero_iff_half, preceded by the
strict positive and negative tilt theorems, already establishes the unique
radial equilibrium from carry geometry.

The new CpGenuineCarryTiltFrontier module then distinguishes that proved
rigidity from the remaining zero-transfer question. It proves:

finite reflected Green bulk = 0
  iff carry tilt = 0                       (pointwise, nonempty cutoff)

every Genuine zero annihilates carry tilt
  iff GenuineStrongNonvanishingInStrip

every Genuine zero annihilates reflected Green bulk
  iff GenuineStrongNonvanishingInStrip.

Thus the Green and tilt languages agree on the radial zero, while the global
arrow from a raw Genuine zero to that radial zero remains explicit. Endpoint
closure is not misidentified with bulk closure: at a Genuine zero the proved
endpoint limit removes the boundary and leaves the radial bulk.

Natural integer bases and the global blind point

The carry structure is not prime-specific. The inherited PR #30 results
cover every positional base b > 1; the finite and analytic natural-camera
theorems cover every nondegenerate width b >= 3, without a primality or
parity hypothesis. The new CpNaturalCameraGlobalBlindSpot module packages
the common factorization as

genuineContinuation s = 0
  iff every natural camera b >= 3 is zero at s

for s in the critical strip. At such a zero, every finite natural-camera
resultant converges to zero. Independently,
infiniteReflectedGreenEnergy_pos proves that the reflected Green energy is
strictly positive at the same parameter. Thus the kernel distinguishes a
simultaneous scalar blind point from disappearance of energy.

It does not yet identify that Green energy with one common pre-compression
state for all natural cameras. That state-level identification is the open
GREEN-NATCAM-INTERTWINER, so it is not used to infer confinement.

The aligned C2 scanner has one leg on each side. Its equality with the
native scanner whose parameter is 4 is an implementation identity with
halfRange 4 = 1; it is not an equality with a geometric C4 having two
legs on each side.

Recovered conformal and coercive modules

Four Lean modules recovered from the interrupted research session are active
and compiled in this release:

• CpConformalJacobian: the complex-differentiable quarter-turn law and its
  norm/orthogonality consequences;
• CpConformalBranchScale: the exact radial derivative of the branch mass and
  its nonzero restoring slope at sigma = 1/2;
• CpRadialCoercivity: the global quantitative estimate
  2 * |delta| * log p <= |cpRadialDifference p delta|;
• CpReflectedGreenBridge: positive reflected energy and the exact conditional
  reduction from bulk-flux closure to the half-abscissa.

No bridge structure is instantiated by renaming the desired conclusion.

Seeded TFVD reconstruction and finite Bessel conservation

The complete green content of draft PR #34 is incorporated. The kernel now
checks:

• the seeded finite TFVD reconstruction checkpoint;
• exact endpoint and border cancellation identities;
• the radial closure observable as radial difference times reflected pairing;
• the amplitude/readout crosswalk;
• exact finite Bessel energy conservation;
• the associated Pythagoras identity;
• uniform finite-atlas Bessel boundedness iff the critical displacement is
  zero;
• the conditional contraction from a fixed-time native moment realization to
  Re(s) = 1/2.

Two additional audit modules make the terminal gate precise:

existence of the proposed fixed-time native moment source
  iff Re(s) = 1/2

sources for every raw Genuine zero
  iff GenuineStrongNonvanishingInStrip.

CpTfvdGpreCollapseInterface gives a typed, non-circular interface for a
future explicit collapse from the two same-edge TFVD states into one native
tower state. The terminal theorem is proved conditional on its coordinate
law; no collapse instance is asserted.

Integrated draft history

This release incorporates all unique mathematical content from the outstanding
draft stacks:

• PRs #25–#26: primitive/Genuine/Riemann-zeta zero-set identity and the exact
  comparison with Mathlib's RiemannHypothesis proposition;
• PRs #27, #31 and #32: native/Genuine/Green crosswalk, the raw-zero
  confinement frontier, and the quadratic C2 activation frontier;
• PR #33: the deliberate red carry-cost probe, repaired into a green theorem
  with the missing mass-compatibility datum explicit;
• PR #34: seeded TFVD reconstruction, Bessel conservation, and native-moment
  contraction;
• ops/ensure-v0.45.0-release: its immutable GitHub/Zenodo confirmation JSON
  records, without reactivating obsolete branch-specific workflows.

Closed historical drafts already superseded by main were audited for unique
content. The original notes recovered from the interrupted chat are preserved
under docs/recovered/2026-08-01/, explicitly classified as research records
rather than kernel certificates.

Independent formalizacao_C2 cross-audit

The separate green repository thiagomassensini/formalizacao_C2 was audited
at commit dc35555879e3c0f188508c729c4a0ea31be246fb, including its complete
37-commit history. Its sole GitHub Actions run, 29081538415 / job
86325282214, successfully builds the active tilt, center-Gaussian and
anti-miracle route modules.

That repository independently kernel-checks local sign and uniqueness laws for
the C2 tilt bracket, center-Gaussian saturation and branch-norm barrier. Its
C2 bracket is the local one-leg-per-side +/-1 detector already generalized
by the Cp tilt in this repository; it is not a geometric C4. It does not
contain a theorem taking an arbitrary Genuine zero to any of those saturation
conditions. The anti-miracle nonvanishing
endpoint assumes decomposition, resolvent shape and strict dominance; the
tilt-curvature theorem is separate. Consequently no duplicate module was
imported as if it paid the missing coupling law. The cross-audit strengthens
the carry-first diagnosis while preserving the exact open frontier.

Exact negative result retained

The failed historical attempt to derive unconditional confinement from raw
boundary closure was not discarded. Its open goal was

NativeCarryRealPlaneMassCompatible s.re s.im.

The corrected green theorem accepts that datum explicitly. The primitive
closure predicate and the full native-zero predicate remain different types:

full native zero = mass compatibility + boundary closure.

The integrated Mathlib comparison proves that reconstructing this mass from
every raw scalar closure is equivalent to Mathlib's RH proposition. It does
not claim that proposition.

No-escape audit

The certified Lean source contains no local declaration beginning with
axiom, sorry, or admit. It does not choose a Hilbert witness from an
existence proof that already assumes the half-abscissa. Diagnostic failures
are preserved in documentation and history, not left as red default targets.

The recovered Python branch/tilt companion is covered by regression tests for:

• exact branch-mass saturation at sigma = 1/2;
• negative/zero/positive tilt across the three radial regimes;
• restoration of critical saturation after weighted-leg normalization.

Numerical output remains an audit aid and is not a premise of any Lean proof.

What this release does not claim

This release does not prove:

• GenuineStrongNonvanishingInStrip;
• Mathlib's RiemannHypothesis;
• that raw scalar boundary closure reconstructs native mass;
• that every Genuine zero annihilates the carry tilt or reflected Green bulk;
• an unconditional TFVD-to-fixed-time native moment collapse;
• a global Parseval/LSB state whose coordinates are all prime Green readouts;
• a common natural-camera pre-compression state or the
  GREEN-NATCAM-INTERTWINER;
• a Hilbert–Polya operator.

It proves that these proposed terminal formulations meet at one sharply typed
frontier, after the carry geometry has already selected the half-abscissa.

Release protocol

Before publication the v0.59.0 workflow must run on main and execute:

bash scripts/...

CPFormal v0.58.0 — Immutable complete Git mirror

CPFormal v0.58.0 — Immutable complete Git mirror

Purpose

This is the final preservation checkpoint created after enabling:

• protection of the main branch against force-push and deletion;
• GitHub immutable releases for all future publications.

The release is published from a draft only after all preservation assets are attached. Once published, GitHub locks the tag and attached assets and generates a release attestation.

Complete repository preservation

The release contains a self-contained Git bundle carrying every ref available at publication time:

• all refs/heads/* branches;
• all refs/tags/* tags;
• all available refs/pull/*/head pull-request heads;
• the complete Git object graph reachable from those refs.

This is stronger than GitHub's automatically generated source ZIP, which contains only the checked-out tree at one tag.

Immutable release assets

Before publication, the draft must contain:

• primos-complete-v0.58.0.bundle;
• primos-complete-v0.58.0-refs.txt;
• primos-complete-v0.58.0-heads.txt;
• primos-complete-v0.58.0-verify.txt;
• primos-complete-v0.58.0-SHA256SUMS.txt;
• primos-complete-v0.58.0-RESTORE.txt.

The publisher then makes the draft public. With release immutability enabled, the Git tag and these six assets cannot be moved, replaced, or deleted through normal GitHub release management.

Verification gates

The publisher fails closed unless it:

1. sees all branch, tag, and pull-request refs;
2. passes scripts/static_audit.sh;
3. passes all real-rotation regression tests;
4. passes lake build --wfail;
5. verifies the bundle with git bundle verify;
6. restores the bundle into a fresh bare repository;
7. passes git fsck --full --strict on the restored repository;
8. proves the restored ref manifest equals the original manifest;
9. attaches all six assets before publication;
10. verifies the published release with gh release verify.

Mathematical content preserved

The bundle includes the complete history of the project, including:

• positional carry, mass and quadratic rigidity;
• all camera, Green, TFVD, boundary and return constructions;
• native real-operator confinement;
• Genuine/native crosswalks and their exact logical frontiers;
• the C2 quadratic diagnostic route;
• exact seeded TFVD radial reconstruction;
• finite Bessel/Pythagoras conservation;
• native G_pre moment contraction;
• intentionally failing probes and every superseded historical route.

The deliberately red diagnostic modules remain outside the active default build but are preserved exactly in the Git bundle.

Recovery

sha256sum -c primos-complete-v0.58.0-SHA256SUMS.txt

git clone --mirror \
  primos-complete-v0.58.0.bundle \
  primos-restored.git

git -C primos-restored.git fsck --full --strict

A normal working checkout can then be created with:

git clone primos-restored.git primos-working-copy

External archive

The published GitHub Release triggers the repository's Zenodo integration. The stable concept DOI remains:

10.5281/zenodo.21483474

A separate verification records the version DOI, checksums and exact agreement between the immutable GitHub assets and the files ingested by Zenodo.

CPFormal v0.57.0 — Complete Git mirror preservation

CPFormal v0.57.0 — Complete Git mirror preservation

Purpose

This is a preservation release correcting an important distinction:
GitHub and Zenodo source-code archives contain the checked-out tree of a tag,
but they are not themselves a complete Git repository and do not necessarily
contain every historical branch tree.

Version v0.57.0 therefore publishes a verified Git bundle as an explicit
release asset. The bundle is a self-contained, cloneable Git database carrying
all repository branches, tags, and pull-request head refs fetched at publication
time.

Preserved refs

The publisher fetches and records:

• every refs/heads/* branch;
• every refs/tags/* tag;
• every available refs/pull/*/head pull-request head;
• the complete object graph reachable from those refs.

Remote branch refs are promoted to their original local branch names before the
bundle is created, so recovery recreates the branch namespace rather than only
remote-tracking aliases.

Release assets

The release must contain, before publication:

• primos-complete-v0.57.0.bundle — complete cloneable Git bundle;
• primos-complete-v0.57.0-refs.txt — exact ref/SHA manifest;
• primos-complete-v0.57.0-heads.txt — heads reported by the bundle;
• primos-complete-v0.57.0-verify.txt — bundle and restored-repository checks;
• primos-complete-v0.57.0-SHA256SUMS.txt — cryptographic checksums;
• primos-complete-v0.57.0-RESTORE.txt — recovery commands.

The publisher fails closed unless it sees at least the 52 branch refs and 12 tag
refs audited immediately before this checkpoint, verifies the bundle, restores
it into a fresh bare repository, and passes git fsck --full --strict on the
restored copy.

Mathematical checkpoint

The active tree contains the green v0.56.0 preservation checkpoint, including
PR #34:

• exact seeded TFVD reconstruction;
• exact finite radial Green bulk;
• finite Bessel/Pythagoras conservation;
• native G_pre moment contraction.

Deliberately failing diagnostic probes remain outside the active build but are
preserved in the bundle and in the archived Git ancestry.

Verification gates

Before publishing, the workflow must pass:

bash scripts/static_audit.sh
python -m unittest -v \
  experiments/test_c2_real_rotation_operator.py \
  experiments/test_c2_real_rotation_minimal.py
lake build --wfail
git bundle verify primos-complete-v0.57.0.bundle
git fsck --full --strict  # on a fresh mirror restored from the bundle

The release is created as a draft, all preservation assets are attached, and
only then is it published. This ordering is compatible with GitHub immutable
releases if that repository setting is enabled before publication.

Recovery

A full mirror can be reconstructed with:

git clone --mirror primos-complete-v0.57.0.bundle primos-restored.git
cd primos-restored.git
git fsck --full --strict

A normal working copy can then be created from the restored mirror:

git clone primos-restored.git primos-restored

Zenodo

The published GitHub Release is consumed by the existing Zenodo integration.
The Zenodo record must be checked after ingestion to confirm that the bundle,
ref manifest, verification report, restore instructions, and checksum file are
all present.

Stable concept DOI:

10.5281/zenodo.21483474

CPFormal v0.56.0 — Complete research-history preservation

CPFormal v0.56.0 — Complete research-history preservation

Purpose

This release is a preservation checkpoint. It integrates the fully audited PR #34 and makes every open or historical unmerged pull-request head permanently reachable from main without activating deliberately failing diagnostic code.

Integrated green mathematics

PR #34 is merged into main through merge commit:

a07f9553e14c8586268b8fe7efa1ae443920b192

It contributes:

• seeded TFVD reconstruction without loss;
• exact cancellation of the aligned moving endpoint and bracket boundary at finite cutoff;
• the pure radial Green observable;
• the exact TFVD–Bessel crosswalk;
• finite Pythagorean conservation of active camera energy and orthogonal residual;
• equivalence between uniform finite-atlas Bessel conservation and Re(s) = 1/2;
• the conditional native G_pre moment-contraction endpoint with factor 11/12.

The release does not claim the still-open implication from a raw scalar Genuine zero to a single atlas-independent native moment realization.

Complete draft-history retention

The archive checkpoint commit is:

4e29cb2fb177517d5ddaf70bb7079c8a0f7bc69c

Its working tree preserves the certified active source, while its Git parent graph includes every unmerged research head:

PR #4   c90db393791a34846f002c7bdd526ac39e99b43d
PR #12  fca2eb91cd63bb85544f32b6ce2218b9f27d0c30
PR #16  e68cad52604e6957e19cd7cce8b1a9f21cafacad
PR #17  0519d4629aa82a46aad22d85ce1c8acaad974707
PR #25  d2b36a2f7689684c97b3c73b0122f2369bb1d14b
PR #26  68724075d7d44f7c6efb6cfabfc70030bb295945
PR #27  8d7a65824a56ed7e690d276c64b1929ef4cd021b
PR #31  9038d18de17a9008a93c04385fcabab3e4d3b6c4
PR #32  f21517a027b2ef130102f5c72ab979e88b305dea
PR #33  30c3e3018d1bb91d85c63d28324e97bfda31a994

Because these commits are ancestors of main, their complete trees and histories remain reachable even if the original pull-request branches are removed.

Independent archive/pr-* branch aliases were also created at each exact hash. The recovery manifest is:

docs/ARCHIVE_ALL_DRAFTS_2026-08-01.md

PR #33 remains preserved as a deliberately failing diagnostic probe, but is not part of the active default build. This preserves both the obstruction and the green certification boundary.

Validation protocol

The publisher must verify the exact current main head and run:

bash scripts/static_audit.sh

python -m unittest -v \
  experiments/test_c2_real_rotation_operator.py \
  experiments/test_c2_real_rotation_minimal.py

lake build --wfail

Only after all checks succeed may it create the annotated tag and public GitHub Release.

GitHub and Zenodo archive

The annotated tag is:

v0.56.0

The public, non-draft, non-prerelease GitHub Release is the ingestion event for the repository's Zenodo integration.

Stable concept DOI:

10.5281/zenodo.21483474

The version DOI is assigned by Zenodo after release ingestion.

CPFormal v0.55.0 — Universal carry structural persistence

CPFormal v0.55.0 — Universal carry structural persistence

Release status

• originating pull request:
  #30;
• audited mathematical-source commit:
  6744f44bf0308af11952ef9e8629357c6be60fcf;
• successful Lean kernel workflow:
  30618216161;
• successful Lean kernel job: 91116286122;
• planned annotated tag: v0.55.0.

The audited source head completed both the static audit and
lake build --wfail. The release workflow after merge remains the
authoritative validation of the exact main commit eligible for the
v0.55.0 tag.

Parent checkpoint

The parent release is:

v0.54.0
ad818112c0850be25b3fa73f5dac33f6ab0af835

It retains the direct causal carry family, positional mass and quadratic
rigidity, together with the domain-restricted inverse certificates.

Scope of v0.55.0

This release formalizes a common structural core across positional
carry, natural camera operators, analytic camera factors, normalized readouts,
zero predicates, Green/TFVD identities, and defect ledgers.

For finite natural cameras it proves the normal forms:

odd b:
  C_(b,M) f = P_(bM+h_b) f - b P_M(D_b f)

even b = 2a:
  C_(b,M) f =
    P_(bM+a-1) f - P_(2M)(D_a f) - (b-2) P_M(D_b f).

The odd formula requires oddness, not primality, and therefore includes odd
composite bases. The scanner label C2 is aligned with the exact width-4
geometry:

C2 aligned = C4.

Analytic natural cameras

For every natural camera width b >= 2, the camera series is continued on the
half-plane Re(s) > -1. On Re(s) > 1, the continuation agrees with the
finite Dirichlet description and its exact camera factor.

The factors are:

odd b:  Φ_b(s) = 1 - b^(1-s)

even b: Φ_b(s) = 1 - (b/2)^(-s) - (b-2)b^(-s).

At width 4:

Φ_4(s) = (1 - 2^(1-s))(1 + 2^(-s)).

The kernel-checked source proves that these factors do not vanish on the
critical line in the required ranges. Consequently, for every natural camera
b >= 3, its continued camera function and the shared genuine continuation
have equivalent zero predicates on that line. The aligned C2 statement
follows through its exact identification with width 4.

This is camera- and primality-independence of the zero predicate under the
proved factorization. It is not a proof that all zeros of the genuine
continuation lie on the critical line.

Structural persistence certificate

The aggregate CarryStructuralPersistenceCertificate packages:

• carry conservation and the direct causal arithmetic family;
• the restricted inverse family from the parent checkpoint;
• positional mass, amplitude, and quadratic rigidity;
• odd, even, composite, and aligned-C2 finite camera algebra;
• natural camera continuation, factorization, and critical-line
  zero-equivalence;
• base-neutral Green aliases and TFVD identities;
• normalized readout, native-zero, packaging-zero, and defect-ledger
  crosswalks.

The logical interface keeps internal state, observable readout, zero
predicate, and hidden energy distinct. Structural persistence means that an
explicitly certified transport preserves the designated normalized readout;
it does not identify all representations or erase defects.

Open limits

This release does not prove:

• that every zero lies on the critical line;
• an exact zero at a finite experimental cutoff;
• a Green-to-natural-camera intertwiner;
• coercivity or a spectral gap;
• equality between a Wronskian and a defect cumulant;
• a general theorem that every mathematical theory is generated by carry;
• any new statement from numerical evidence alone.

The Green/natural-camera intertwiner and the C2 cumulant/Green bridge remain
explicit next targets.

Source and documentation

Principal formal sources:

• CPFormal/Logic/StructuralPersistence.lean;
• CPFormal/Analytic/CpNativeCarryFiniteCameraAlgebra.lean;
• CPFormal/Analytic/CpNaturalCameraFactor.lean;
• CPFormal/Analytic/CpNaturalEvenCameraRegularity.lean;
• CPFormal/Analytic/CpNaturalCameraAnalyticContinuation.lean;
• CPFormal/Analytic/CpUniversalCarryStructuralPersistence.lean;
• CPFormal.lean.

Principal documentation:

• docs/UNIVERSAL_CARRY_STRUCTURAL_PERSISTENCE.md;
• docs/CLAIM_LEDGER.md;
• docs/AUDIT.md;
• docs/RELEASE_0.55.0.md;
• README.md.

Release automation:

• .github/workflows/release-v0.55.0.yml.

Release protocol

Before publishing, the v0.55.0 workflow must run on main and execute:

bash scripts/static_audit.sh

python -m unittest -v \
  experiments/test_c2_real_rotation_operator.py \
  experiments/test_c2_real_rotation_minimal.py

lake build --wfail

It must verify that the checked-out commit is the current remote main head,
that any existing v0.55.0 tag is annotated and points to that exact commit,
and that any existing GitHub Release is neither draft nor prerelease. Only
after these checks succeed may it create the annotated tag and publish the
release.

The Python experiments are regression tests and are not proof premises of the
Lean certificates.

Archival and Zenodo

The published, non-draft, non-prerelease v0.55.0 GitHub Release is the event
consumed by the repository's Zenodo integration. Zenodo assigns the version
DOI after ingesting the immutable release.

The stable concept DOI remains:

10.5281/zenodo.21483474

CPFormal v0.54.0 — Restricted inverse certificates for positional arithmetic

CPFormal v0.54.0 — Restricted inverse certificates for positional carry

Release status

• integrated pull request:
  #29;
• audited mathematical-source commit:
  8a351323c7476d70e701bed6ab4137d2c5137f2d;
• Lean kernel workflow:
  30607820730;
• Lean kernel job: 91083828864;
• planned annotated tag: v0.54.0.

The audited source head completed both the static audit and
lake build --wfail. The release workflow after merge remains the
authoritative validation of the exact main commit that may be tagged as
v0.54.0.

Parent checkpoint

The parent release is:

v0.53.0
b27f5cfd915a47d49eb6833b259e9f3d47a0fc03

That immutable checkpoint certifies the direct causal family:

positional carry
  -> positional addition
  -> multiplication
  -> natural power.

It also retains the positional mass criticalMass b k = b^(-k), the
quadratic-amplitude identity, and rigidity at sigma = 1/2.

Scope of v0.54.0

This release adds a separate restricted-inverse layer:

carry <-> borrow

translation by y <-> subtraction of y over Z

dividend <-> quotient-remainder pair

multiplication by d <-> division by d on multiples of d

degree-e power <-> Nat.nthRoot e on perfect powers

base-b power <-> Nat.log b on exact base powers.

These relations are paired and branched. They are not a reversed arithmetic
tower.

No new CausalCompressionSystem or CompressionPath is constructed.
Instead, the release introduces RestrictedInverseCertificate, a formal
interface for mutual inverses on explicit source and target domains.

Restricted inverse interface

For maps

forward : Source -> Target
backward : Target -> Source

and predicates

SourceDomain : Source -> Prop
TargetDomain : Target -> Prop,

RestrictedInverseCertificate stores:

forward_maps_domain
backward_maps_domain
left_roundTrip
right_roundTrip.

The domain-preservation obligations prevent either round trip from silently
leaving the region on which it was certified.

This interface is intentionally separate from causal inheritance:

• CausalCompressionSystem records directed semantic ancestry;
• RestrictedInverseCertificate records a domain-restricted round trip.

Neither structure implies the other.

Carry and borrow

The release defines:

PositionalCarryStep
PositionalBorrowStep
CarryBorrowReverseCertificate
carryBorrowReverseCertificate.

The concrete certificate proves:

• borrow reverses the endpoints of one carry relation;
• carry preserves represented value;
• borrow preserves represented value;
• the positional configurations are distinct.

The common value identity remains:

b * b^k = 1 * b^(k+1).

This is a local reverse relation at one scale, not recovery of an arbitrary
normalization history.

Concrete schoolbook borrow

For lower digits with x < y, borrowing one higher unit defines:

borrowedDigit b x y = x + b - y.

The release proves the full-column reconstruction:

(high - 1)*b + borrowedDigit b x y
  =
high*b + x - y.

Under the canonical digit hypotheses

0 <= x < b
0 <= y < b
x < y,

the borrowed result returns to the digit window:

0 <= borrowedDigit b x y < b.

The declarations are:

borrowedDigit
positionalBorrow_reconstruction
borrowedDigit_mem_window
BorrowSubtractionCertificate
borrowSubtractionCertificate.

This certificate is the explicit bridge between positional borrow and one
schoolbook subtraction column.

Addition and subtraction with a fixed translation

For fixed y : ℤ, the maps are:

addTranslation y x = x + y
subTranslation y x = x - y.

The release exposes:

subTranslation_eq_add_inverse
AddSubTranslationCertificate
addSubTranslationCertificate.

The certificate proves both unrestricted integer round trips:

(x + y) - y = x
(x - y) + y = x.

The retained parameter y is essential. A sum alone does not identify its two
original operands.

Lossless Euclidean split

For a positive divisor d:

euclideanSplit d n = (n / d, n % d)
euclideanReconstruct d (q,r) = r + d*q.

The canonical target domain is:

IsCanonicalEuclideanPair d (q,r) := r < d.

The exact statements are:

euclideanSplit_reconstruction
euclideanSplit_remainder_lt
euclideanSplit_recovers_canonicalPair
EuclideanSplitCertificate
euclideanSplitCertificate.

The pair (q,r), together with d, reconstructs n, and every canonical pair
is recovered after reconstruction. Quotient alone is not a lossless inverse.

Multiplication and exact division

For a fixed positive d:

mulBy d q = d*q
divBy d n = n/d.

The exact target domain is:

IsMultipleImage d n := exists q, n = d*q.

The release proves and packages:

exactDivision_recovers_factor
MulDivOnMultiplesCertificate
mulDivOnMultiplesCertificate.

Division by d inverts multiplication by d only on the image of multiples.
For arbitrary dividends, the quotient-remainder certificate is the lossless
object.

Power and Nat.nthRoot on perfect powers

For fixed degree:

powerByDegree degree value = value^degree
nthRootByDegree degree value = Nat.nthRoot degree value.

The target domain is:

IsPerfectPowerImage degree value.

For nonzero degree, the release proves:

nthRoot_exact_on_powers
nthRoot_reconstructs_iff_perfectPower.

The restricted inverse is:

PowerNthRootOnPerfectPowersCertificate
powerNthRootOnPerfectPowersCertificate.

No exact inverse is asserted outside the perfect-power image, and degree zero
is excluded.

Base power and Nat.log on exact powers

For fixed base:

powerByBase b exponent = b^exponent
floorLogByBase b value = Nat.log b value.

The target domain is:

IsExactBasePower b value.

For b > 1, the release proves and packages:

floorLog_exact_on_basePowers
BasePowerLogOnExactPowersCertificate
basePowerLogOnExactPowersCertificate.

Thus:

Nat.log b (b^k) = k,

and the opposite round trip is required only for exact powers of b.

Floor logarithm and floor division

For arbitrary positive input, Nat.log b is a magnitude coordinate:

b^(Nat.log b n) <= n
n < b^(Nat.log b n + 1).

The theorem is:

floorLog_power_window.

Whenever b <= n, one floor division by the base removes one logarithmic
unit:

Nat.log b n = Nat.log b (n / b) + 1.

The theorem is:

floorLog_division_step.

This is the precise sense in which Nat.log counts floor divisions. It is not
the real analytic logarithm.

Exact-division depth remains distinct

The release keeps:

repeatedExactDivisionDepth b n = positionalDepth b n.

This coordinate measures maximal exact divisibility:

b^k divides n
b^(k+1) does not divide n.

The exact statements are:

repeatedExactDivisionDepth_spec
repeatedExactDivisionDepth_factorization_existsUnique.

No equality between Nat.log b n and positionalDepth b n is asserted for a
general natural number. They agree on pure powers n = b^k but encode
different information elsewhere.

Consolidated bundle

The release introduces:

PositionalInverseArithmeticCertificates
positionalInverseArithmeticCertificates.

For one base b > 1, the bundle exposes:

carry_borrow
borrow_subtraction
addition_subtraction
euclidean_split
multiplication_division
power_nthRoot
power_log
log_power_window
log_division_step
exact_division_depth.

Divisor- and degree-dependent constructors retain their assumptions:

• positive divisor;
• nonzero degree;
• nondegenerate base.

The bundle does not turn them into one global inverse operation.

Carry mass and quadratic rigidity

This release introduces no new mass law.

The following remain inherited results from v0.53.0:

criticalMass b k = b^(-k)
(criticalAmplitude b k)^2 = criticalMass b k
(branchAmplitude b sigma k)^2 = criticalMass b k
  <->
sigma = 1/2.

Restricted recovery and scale descent do not alter the uniform carry-event
mass and do not provide an independent derivation of quadratic rigidity.

Base independence

The consolidated certificate bundle requires only:

1 < b.

No primality, oddness, distinguished camera, base 3, complex parameter,
zeta function, or analytic continuation is used.

Interpretation boundary

This release does not:

• construct a global inverse tower;
• reverse CompressionPath;
• construct a new CausalCompressionSystem;
• make subtraction recover two operands from their sum;
• make quotient alone a lossless inverse of multiplication;
• permit exact division by zero;
• make Nat.nthRoot exact outside perfect powers;
• permit degree zero in the root round trip;
• make Nat.log exact outside powers of the fixed base;
• identify Nat.log with the real logarithm;
• identify Nat.log b n with positionalDepth b n in general;
• assert backward physical or temporal causation;
• prove that every mathematical system has these certificates;
• introduce a new probability, mass, amplitude, or rigidity law;
• add an axiom, sorry, or admit as mathematical evidence.

Source and documentation

New formal source:

• CPFormal/Carry/PositionalCarryInverseCausalInheritance.lean.

Active import surface:

• CPFormal.lean.

New documentation:

• docs/CARRY_INVERSE_CAUSAL_INHERITANCE.md;
• docs/RELEASE_0.54.0.md.

Updated documentation:

• docs/RESUMO_GERAL_HERANCA_CAUSAL_DO_CARRY.md;
• docs/AUDIT.md;
• docs/CLAIM_LEDGER.md;
• README.md.

Release automation:

• .github/workflows/release-v0.54.0.yml.

The historical files docs/RELEASE_0.53.0.md and
`.github/workflows...