JACKAL v1.7.0 — Certified bound_step Composition

JACKAL v1.7.0 — Certified bound_step Composition

Ledger roadmap item (4) — composing bound_step's acceptance policy over
runs_encloses + the Taylor bridges — is closed for the certificate lane
and shipped as a public proof-carrying tool. This release completes the arc
from the shadow mechanization (PR #3, deliberately non-authoritative) to the
public surface (PR #6), and fixes issue #4.

The new certified lane

./jackal-int-cert-release "sin(x)" 0 1 1/100 receipt.json
# status=formal-bounded enclosure=[…] theorem=int_cert_sound … receipt_reverified=true

• Theorem int_cert_sound (JackalIv.IntCert, Lean 4 + Mathlib): an
  artifact accepted by the proved computable checker yields a genuine
  enclosure of the exact integral of the reconstructed integrand over the
  requested interval, under the named TreeTCB (a Prop hypothesis — never
  an axiom — vacuous on the pure-rational fragment). Axioms: exactly
  [propext, Classical.choice, Quot.sound].
• Fourth pinned checker executable jackal_int_cert_check
  (c858e3bfc0ff2809a808170caabbf090077cb54996e76f065dbcd26ffb067d49),
  compiled from the proved parseIntCert + checkIntCert — no
  native_decide, no @[implemented_by] on the path. The lakefile edit
  re-pinned both existing proof identities; the range and gaussian checker
  binaries reproduced byte-identical (05c3518b…, ccac690b…).
• Untrusted producer tools/int_cert_producer.py (b4240fda…): an
  identity-pinned exact-rational mirror of the shipped bound_step
  (float midpoints, exact-ℚ acceptance, budget 60000, depth 60) emitting
  jackal-int-cert v1 subdivision-tree artifacts whose leaves embed ordinary
  jackal-eval-cert v2 certificates. Same architecture as the seven *_rat
  lanes: trust lives ONLY in checker acceptance.
• Fail-closed release binding: request commitment
  (jackal-req-v3-int-cert), producer/checker identity pins with TOCTOU
  stability, checker-echo enclosure binding, formal-status derivation against
  the digest-bound coverage inventory, receipt variant int_cert, and
  independent re-verification before success.
• Plugin surface: 33 → 34 tools — jackal_integrate_bound_cert, plus
  jackal_verify_receipt int_cert mode (expected_tolerance required). The
  weaker float lane integrate-bound / jackal_integrate_bound remains
  bounded/CONDITIONAL and never inherits formal language.

Issue #4 fixed — rat approx= presentation

approx= is now a rendering of the final normalized exact rational
(exact long division to ≥30 significant digits + one correctly-rounded
decimal→f64 parse), never an independently computed float path. Algebraically
equivalent inputs print identical decimals by construction; the verified
repro is pinned as a black-box regression pair. Presentation layer only —
certified lanes, the exact engine, and the checkers are untouched. The
evaluator was rebuilt with the pinned Anubis compiler after the baseline
rebuild of the unmodified source reproduced the v1.6.0 binary 8617ad08…
byte-identically (instrument validated first).

Migration (33 → 34)

Additive only: every v1.6.0 tool, schema, receipt format, and CLI command is
byte-compatible (mechanically locked: COMPAT_FLOOR_PASS frozen_tools=31 live_tools=34). Users of jackal_integrate_bound who need a proof-carrying
enclosure should call jackal_integrate_bound_cert (certified fragment:
num/var/neg/add/sub/mul/div/pow(0..4096)/sin/cos/abs in x; everything
else refuses). Full guidance: release/claim/MIGRATION-v1.7.0.md.
rat approx= semantics changed from "independent f64 evaluation of the
input" to "rendering of exact=" — the honest independent-float lane
remains eval.

Gates

Local sealed aggregate (Apple Silicon):
python3 release/tools/run_gates_v170.py → GATES: PASS (43 gates)
(full log in the evidence asset, sha256
cb614ff388df65b3bb42639e1ae491c808c8c73ace12645ee40b774668bc9caa):

• black-box 202/202 (incl. the issue-#4 regression pair); parser
  differential 78/78
• int-cert matrix 31/31 (6 positive, 7 refusal, 18 semantic poisons)
  against the compiled checker
• int-cert A→B→A: the tolerance guard is load-bearing (poison admitted
  under the mutated, rebuilt checker; original bytes restored hash-verified);
  the enclosure guards are proof-load-bearing — disabling them does not
  compile (int_cert_sound consumes them)
• engine differential 5/5: mpmath 60-dps oracle inside BOTH the engine's
  float enclosure and the certified enclosure
• claim gates: hostile 108/108, package parity 49/49 over this package,
  evidence determinism, frozen v1.6.0 claim fixture replays green
• package double-build byte-identical

Hosted CI (PR #6): Lean source closures + proof-identity/axiom audits for
all three lanes (now incl. int-cert, --proof-only) and the engine-free
34-tool/compat-floor/claim-admission job — all green.

Assets

asset	sha256	bytes
jackal-v1.7.0-macos-arm64.tar.gz	21c7ede586f30a58772f321f7dbb36ab66213e199785489f99133710ac56096e	118862060
jackal-v1.7.0-release-receipt.json	9474b801757b4833597702f60404c2c7f1acbca47a6a2552d0581a9f9922e06b	7354
jackal-v1.7.0-evidence.tar.gz	a62b86c91be50fff423f13d7b662865272a413a08aae2962ac1738d31d647ee2	3965
SHA256SUMS	—	296

Residual non-claims

• Producer fidelity to the shipped engine's bound_step control flow is
  differential-tested, never proved; certified derivative chains are
  Lean's D (no simplify_bound interleave — integer-power integrands may
  refuse taylor4 through 0-crossing domains; fail closed, never unsound).
• Source→native refinement (roadmap item 5) remains OPEN — the last
  bridge.
• Claim-bundle formal-receipt evidence replay stays pinned to the range
  lane; gaussian and int_cert receipts verify directly via
  jackal_verify_receipt, not yet inside bundles (SPEC §6/§12).
• The engine's float integrate-bound lane remains
  implementation-tested-not-mechanized.
• SHA-256 identifies bytes; it does not authenticate an author. The artifact
  is unsigned and has not received an independent external proof audit.