Ackermann Runtime Certification Protocol

This file is the falsifiability protocol for the Ackermann runtime certification. It is the prediction ledger, not a results document. Every empirical claim below is marked as a prediction (P*) or a falsification trigger (F*); nothing here is an observation.

Sibling deliverables (6-file fanout, all written in parallel):

• Gnosis/AckermannRuntimeCertificate.lean (in open-source/gnosis-math/) — the kernel-checked certificate that the runtime ceiling carries the Ackermann growth class.
• Gnosis/AckermannPrimitiveRecursiveBound.lean (same dir) — the primitive-recursive boundary theorems and the calibration-window bound (primitive_recursive_calibration_window_bound).
• Gnosis/AckermannRuntimeOracle.lean (same dir) — the five ackermann_runtime_oracle_* theorems pinning the Lean → Rust value contract.
• src/ackermann_certificate.rs — the Rust kernel that exercises the pentad and the polynomial-degree estimator.
• src/bin/ackermann-bench.rs — the CLI harness that drives the certification against named targets.
• This file — the falsifiability ledger that the other five are measured against.

Companion documents (existing, referenced):

• BOWL_MESH_FALSIFIABILITY.md (same dir) — the canonical protocol pattern this file mirrors exactly. Tone, structure, the *_runtime_oracle_* pentad discipline, the honesty boundary — inherited verbatim.
• Gnosis/AmplituhedronFalsifiability.lean (in open-source/gnosis-math/) — the original vandermonde_runtime_oracle_* pentad pattern; this protocol mirrors its shape on a different mathematical object.
• Gnosis/AckermannFunction.lean — the upstream theorems (ack_0..ack_3, ack_dominates, level_variation, ackermann_master) the certificate rests on.

1. Headline reframe

AckermannFunction.ackermannDiag models the canonical limit of total-recursive growth that is not primitive recursive — the diagonal H(n, n, n) of the hyperoperation tower. Upstream (AckermannFunction.lean) proves the two facts that load-bear this reframe: ack_dominates (the diagonal grows faster than any fixed-level tower) and level_variation (the level itself varies along the diagonal, which is exactly the structural reason the diagonal escapes primitive recursion). Read as a runtime ceiling: 100% Ackermann saturation means the target's step count is pinned to the diagonal itself; 0% means the target is microscopically below it. Most real code lives at near-0%, because polynomial and even fixed-tower exponential growth are dwarfed by ackermannDiag(4) — already astronomical at hyperop 4 4 4.

2. What is being certified

The metric is a structural ceiling certifier, not a profiler. It distinguishes primitive-recursive growth from non-primitive-recursive growth. It does NOT distinguish O(n) from O(n²) — both report as 0% Ackermann at every calibration point. A polynomial-degree estimator runs alongside as a secondary, non-theorem-backed heuristic for inside-the-PR-class discrimination; the only formal guarantee is the ceiling pentad in §3.

The certificate answers one question: does the target's step count stay below the Ackermann diagonal on the calibration window? If yes, the target is structurally below the PR boundary on that window. The metric is unitless and saturating: above 100% the harness reports "diverges from window-pinned diagonal" rather than a percentage.

3. The pentad

AckermannRuntimeOracle.lean exports five ackermann_runtime_oracle_* theorems mirroring the AmplituhedronFalsifiability.vandermonde_runtime_oracle_* pentad and the BowlMeshRuntimeOracle.* pentad. These are the value-level contracts the Rust kernel (src/ackermann_certificate.rs::ackermann_ceiling) MUST reproduce on the four-point calibration window.

Contracts #1–#4 are exact-value contracts; the Lean theorems chain through ack_0..ack_3 from AckermannFunction.lean and the Rust kernel must reproduce the same Nat values. Contract #5 is symbolic: the diagonal at n=4 is astronomical (hyperop 4 4 4 is well beyond Nat materialization on any concrete machine), and the kernel falls back to the structural verdict rather than attempting to compute the closed form. The symbolic equality is the contract; numeric materialization is not.

4. The calibration window

The measurement window is n ∈ {0, 1, 2, 3}. This window is the only regime where the Lean ledger pins exact Nat values (ackermann_runtime_oracle_zero..three) and the Rust kernel can exercise them numerically. For n ≥ 4 the ceiling is astronomical and the kernel falls back to the structural verdict via the polynomial-degree estimator.

AckermannPrimitiveRecursiveBound.lean::primitive_recursive_calibration_window_bound formalizes this: every primitive-recursive function whose step count is bounded by ackermannDiag n on n ∈ {0, 1, 2, 3} is not therefore proven primitive recursive at n ≥ 4; the bound only carries on the window. The honesty rule is that the certificate reports a confident verdict on the window and a heuristic verdict beyond it, never confuses the two.

5. Predictions

All five are predictions, not observations. They will be falsified or upheld by ackermann-bench.rs running against the canonical target set: constant, identity, quadratic, cubic, exponential, memoized Ackermann, naive Ackermann.

• P1. A constant-runtime target reports 0% Ackermann at every calibration point n ∈ {0, 1, 2, 3}. Trivial — the step count is 1 regardless of input scale, and 1 / ackermannDiag n ≤ 1 / 1 = 100% bounds the metric but the saturating arithmetic resolves to 0% on the constant baseline by definition. Listed for completeness; this is the floor case.

• P2. The naive (non-memoized) two-argument Ackermann target reports ≈100% Ackermann at n=3 by construction. The naive recursion IS the diagonal up to the inner-call counting convention; the expectation is exact saturation modulo the small constant the counting convention introduces. Justification: the Rust kernel measures step count, and the step count of naive Ackermann at the diagonal point IS ackermannDiag 3 = 27 plus the convention constant.

• P3. A memoized Ackermann target (same recursion, with a call-cache) reports strictly less than 100% Ackermann at n=3. The memoization buys headroom by collapsing repeated subcalls; how much headroom is the empirical question. The prediction is "strictly below", not a specific percentage. Justification: memoization on a recursion with repeated subcalls cannot increase step count and almost always decreases it; the bench measures by how much.

• P4. Identity, quadratic, and cubic targets all report below 50% Ackermann at every calibration point in {0, 1, 2}, with the cubic target hitting exactly 100% at n=3. The cubic-meets-Ackermann coincidence at n=3 is a structural artifact of ack_3 : ackermannDiag 3 = 27 and the identity 3³ = 27. Numerically: identity at n=3 yields step count 3 against ceiling 27, ≈11%; quadratic yields 9 against 27, ≈33%; cubic yields 27 against 27, exactly 100%. This 100% is not a certification failure — it is the calibration window doing what it advertises: at n=3 the ceiling happens to equal the cubic step count, and the harness must report this honestly rather than mask it. Outside n=3 the cubic target is well below the diagonal. The artifact is called out here so it is not mistaken later for a true Ackermann-class growth signal.

• P5. The polynomial-degree estimator (ackermann_certificate.rs::polynomial_degree) returns Some(1) on the identity target, Some(2) on the quadratic target, Some(3) on the cubic target, and None on the exponential and naive-Ackermann targets. The exact return shape depends on the calibration constants shipped in ackermann_certificate.rs; the prediction is the qualitative classification ("polynomial of degree k" vs "super-polynomial"), not the exact integer return. The estimator is a heuristic, not a theorem; this prediction is the load-bearing honesty claim about it.

6. Falsification triggers

These are the curves and points that would kill the certification. Triggers, not observations.

• F1. Any of the five oracle pentad contracts (§3) fails on the Rust side. The Lean ↔ Rust parity is broken below the formalization level: either the Lean spec mis-models the diagonal at the calibration point, or the Rust kernel does not honor the spec. Either way the certificate needs to be rewritten from the primitive up, same as F5 in BOWL_MESH_FALSIFIABILITY.md.

• F2. A target whose Lean-side runtime is provably primitive-recursive (constant, identity, polynomial) reports > 0% Ackermann at a calibration point in a way that does not reduce to a calibration-window arithmetic identity (P4 cubic-at-n=3 is the only sanctioned identity). This indicates the ceiling computation is leaking — the metric is supposed to be 0%-bounded on the PR class modulo the named identity, and any non-identity leak breaks the structural claim.

• F3. The memoized Ackermann target is NOT strictly below the naive Ackermann target at n=3. P3 then fails: either memoization is not actually reducing step count on this recursion (broken cache), or the step counter is not measuring what it claims to measure (broken instrumentation). Both are recoverable but blocking.

• F4. The polynomial-degree estimator misclassifies the exponential target as polynomial — returns Some(k) for any finite k on an exponential-growth input. The structural-fallback verdict for n ≥ 4 is then unsound: the heuristic the certificate relies on beyond the calibration window does not actually discriminate polynomial from super-polynomial growth. The window-pinned theorem still holds, but the n ≥ 4 verdict shipped by the kernel becomes untrustworthy and must be removed from the public surface until the heuristic is corrected.

• F5. The cubic-meets-Ackermann coincidence at n=3 (P4) fails to land at exactly 100%. Either the Rust step counter for the cubic target diverges from the closed-form value 3³ = 27, or the Lean side disagrees with ackermannDiag 3 = 27 (which would itself contradict ack_3 in AckermannFunction.lean and therefore invalidate the entire upstream chain). This is the cheapest end-to-end Lean ↔ Rust audit point in the protocol and is load-bearing precisely because it is so cheap to check.

Any of F1–F5 reverts the certification to "interesting toy" status. None of them by themselves invalidates the upstream AckermannFunction theorems; those sit structurally below this protocol and are not at stake here.

7. Honesty boundary

The metric is structural, not benchmark-style. The harness pin is at n ∈ {0, 1, 2, 3} because that is exactly the window the Lean ledger materializes Nat values for. For n ≥ 4 the kernel runs the polynomial-degree heuristic and ships a structural verdict; that heuristic is honest but it is not a theorem. The only formal guarantee is at the calibration window, and the bound is exactly the one stated in AckermannPrimitiveRecursiveBound.lean::primitive_recursive_calibration_window_bound.

Reading the certification output: a target reporting "0% Ackermann across n ∈ {0,1,2,3}, polynomial-degree estimator returns Some(k)" means the target is structurally below the PR boundary on the window AND the heuristic suggests it is degree-k polynomial. Both halves are needed; neither by itself is a full classification.

8. Composition with Amplituhedron and Bowl-Mesh

All three falsifiability protocols in this directory share the same Lean → Rust runtime-oracle pattern: name the failure regime, prove five *_runtime_oracle_* contracts, exhibit the structural property the regime would violate. The mathematical objects differ:

• Amplituhedron (AmplituhedronFalsifiability.lean): scattering amplitudes, prefix cache, Vandermonde 2×4 oracle. Granularity: prefix × layer-range. Failure regime: lossy qk / 10 placeholder.
• Bowl-Mesh (BOWL_MESH_FALSIFIABILITY.md): per-token residual filter, balanced/pejorative/filled bowl oracle. Granularity: single residual vector. Failure regime: high-damping mask crush.
• Ackermann (this protocol): runtime step count, primitive-recursive ceiling, four-point Ackermann diagonal oracle. Granularity: per-target step count on the calibration window. Failure regime: Lean ↔ Rust value disagreement on the pentad.

Read as a stack, the three certify disjoint axes of the same runtime:

• Ackermann certifies how computable — the algorithm's growth rate is below the PR boundary on the calibration window.
• Amplituhedron certifies how often — cache hits skip work on known prefixes, the volume key space is disjoint from intra-layer matVec keys.
• Bowl-Mesh certifies how preserved — the residual stream survives compression in the healthy interior of the damping sweep.

The three operate on disjoint axes (growth class, replay frequency, residual fidelity) and compose without interference; the runtime deploys all three simultaneously without one's verdict feeding into another's.

9. Pointers

Six sibling files in this fanout, plus the upstream Lean module the certificate rests on:

• Gnosis/AckermannRuntimeCertificate.lean — the certificate that the runtime ceiling carries the Ackermann growth class on the calibration window.
• Gnosis/AckermannPrimitiveRecursiveBound.lean — the primitive-recursive boundary theorems including primitive_recursive_calibration_window_bound, the formal statement of the n ∈ {0,1,2,3} guarantee.
• Gnosis/AckermannRuntimeOracle.lean — the five ackermann_runtime_oracle_* theorems pinning the Rust value contracts on the calibration window.
• src/ackermann_certificate.rs — the Rust kernel implementing ackermann_ceiling(n), the step counter, and the polynomial-degree estimator. Honors the §3 pentad in unit tests.
• src/bin/ackermann-bench.rs — the CLI harness driving the certification against the named target set (constant, identity, quadratic, cubic, exponential, memoized Ackermann, naive Ackermann).
• ACKERMANN_CERTIFICATION_PROTOCOL.md — this file. The falsifiability ledger.
• Gnosis/AckermannFunction.lean — the upstream module supplying ackermannDiag, ack_0..ack_3, ack_dominates, level_variation, ackermann_master. Pre-existing; not part of the fanout.

10. Honesty note

Nothing in §5 has been measured. The Lean theorems referenced in §3 and §4 will be kernel-checked under Init when the sibling Lean files land in this same fanout, and the Rust kernel exercises them in unit tests — but the empirical bench predictions are predictions, not observations. The certification survives or falls on ackermann-bench.rs running against the canonical target set, not on the algebraic argument.

If F1–F5 all fire, the protocol has been falsified at the same operational level the wave-3 / wave-4 binary mask was falsified at on 2026-05-03. The previous-snapshot rule from STANDING_WAVE_STATUS_2026_05_03_AFTER_FALSIFICATION.md applies: this file becomes the historical record, an addendum captures the falsification, the certification gets demoted to "interesting toy" status, and the runtime continues without the Ackermann gate until a revised primitive is ready.