Skip to content

CPFormal v0.55.0 — Universal carry structural persistence

Choose a tag to compare

View all tags
@github-actions github-actions released this 31 Jul 09:21
· 119 commits to main since this release
v0.55.0
c9748ca
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

CPFormal v0.55.0 — Universal carry structural persistence

Release status

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
Assets 2
Loading