Abstract
The order-statistic gaps that underlie PPP-residualized functional identity measurement are exactly invariant to log-softmax transformation, exactly equivariant under positive scaling (including temperature), and exactly invariant to any position-independent constant shift applied to the logit vector. These are not empirical approximations — they are mathematical identities that hold for any logit vector over any vocabulary size. The result has been formally verified in Coq (GapInvariance.v: 5 theorems, 2 axioms, 0 Admitted). It retroactively strengthens the empirical API-wall finding reported in earlier work: the order-statistic gap geometry measured through API logprobs does not merely "survive" the log-softmax transformation — it is mathematically immune to it. Any deviation attributable to the API boundary must come from truncation, quantization, or coverage limitations, not from the probability-domain transformation itself.
1. The Measurement and the Question
PPP-residualized functional identity measurement [1, 2] operates on the gaps between adjacent order statistics of a model's output logit vector. For each generated token, the model's top-K logits are sorted in descending order and the gaps G_k = z_(k) − z_(k+1) are computed for k = 1, ..., K−1. These gaps are then residualized against a power-law baseline (the PPP fit β̂/k) to produce a template that captures the model's characteristic gap shape after removing shared scale structure.
This measurement has been validated empirically across 14 API-served models from three providers [2, 4], across adversarial erasure conditions [3], and across frontier-scale distillation pairs spanning 1.5B to 70B parameters [5, 6]. Throughout these validations, a foundational question has been answered empirically rather than mathematically: when an API serves log-probabilities (log-softmax values) rather than raw logits, does the gap geometry change?
The answer is no, and it is not an empirical finding. It is a mathematical identity.
Why this matters. Earlier work showed empirically that PPP-based measurements remained stable when models were accessed through APIs that expose log-probabilities instead of raw logits. This note upgrades that result from empirical robustness to mathematical invariance. It removes the probability-domain transformation itself from the list of plausible failure modes. If an API-based PPP measurement deviates from a weights-based measurement, the cause must lie in truncation, quantization, coverage limitations, or the model — not in log-softmax. The API wall is narrower than previously understood, and the space of plausible objections to API-domain model identity measurement has shrunk by one major category.
2. The Gap Cancellation Theorem
Definition. Let z = (z₁, ..., z_V) be a logit vector over vocabulary size V. Let z₍₁₎ ≥ z₍₂₎ ≥ ··· ≥ z₍V₎ denote the order statistics. The order-statistic gaps are G_k := z₍k₎ − z₍k+1₎.
Theorem 1 (Constant-Shift Gap Invariance). For any constant c ∈ ℝ, G_k(z + c) = G_k(z).
Proof. Adding c to every component preserves the sorting permutation. Therefore (z + c)₍k₎ = z₍k₎ + c. The gap becomes (z₍k₎ + c) − (z₍k+1₎ + c) = z₍k₎ − z₍k+1₎ = G_k(z). ∎
Theorem 2 (Positive-Scale Gap Equivariance). For any a > 0, G_k(a · z) = a · G_k(z).
Proof. Multiplying by a > 0 preserves the ordering. Therefore (a · z)₍k₎ = a · z₍k₎. The gap becomes a · z₍k₎ − a · z₍k+1₎ = a · G_k(z). ∎
Theorem 3 (Affine Gap Scaling). For a > 0 and b ∈ ℝ, G_k(a · z + b) = a · G_k(z).
Proof. The additive constant b cancels by Theorem 1. The multiplicative constant a scales uniformly by Theorem 2. ∎
Theorem 4 (Log-Softmax Gap Invariance). Let logsoftmax(z)ᵢ = zᵢ − log(Σⱼ exp(zⱼ)). Then G_k(logsoftmax(z)) = G_k(z).
Proof. The log-partition function C = log(Σⱼ exp(zⱼ)) is a scalar: it depends on the full vector z but not on the component index i. Therefore logsoftmax is a constant shift by c = −C, and the result follows from Theorem 1. ∎
Theorem 5 (General Position-Independent Shift Invariance). For any function f(z)ᵢ = zᵢ + c(z) where c: ℝ^V → ℝ depends on z but not on i, G_k(f(z)) = G_k(z).
Proof. c(z) is the same for all components, so f is a constant shift. Theorem 1 applies. ∎
Corollary (PPP Domain Invariance). The PPP-residualized template — computed from the gap vector after β̂ subtraction — is identical whether computed from raw logits, log-probabilities, or any constant-shifted logit representation. For PPP residualization specifically, the β̂ estimator is computed from the gaps themselves and therefore inherits whatever scaling the gaps carry. Under constant shifts, β̂ is unchanged; under positive scaling by a, β̂ scales by a and the residual r_k = G_k − β̂/k scales uniformly by a, preserving all distance ratios.
Corollary (Temperature Equivariance). Temperature scaling z → z/T is a positive scaling with a = 1/T. All gaps scale by 1/T, all residuals scale by 1/T, and all pairwise L₂ distances scale by 1/T. Distance ratios are invariant. Absolute threshold decisions require consistent serving temperature or explicit scale normalization.
3. Formal Verification
The theorem has been formally verified in Coq 8.18.0 and confirmed forward-compatible with Rocq Prover 9.1.1 (OCaml 5.4.0).
| Component | Count |
|---|---|
| Theorems proved | 5 (T1–T5) |
| Axioms | 2 (OS1, OS2) |
| Admitted | 0 |
| Lines | 469 |
| Tactic policy | intros, unfold, rewrite, exact, ring only |
The two axioms encode standard properties of order statistics: OS1 states that adding a constant to every component shifts every order statistic by that constant; OS2 states that multiplying by a > 0 scales every order statistic by that factor. Both are elementary consequences of the definition of order statistics [7]. Both are falsifiable: any sorting procedure that is not a faithful permutation would violate OS1; any procedure that renormalizes values after extraction would violate OS2. Both participate in the headline theorems — neither is decorative.
The log_sum_exp function is declared as Vec → R (a scalar-valued function of the full vector), enforcing position-independence at the type level. The Coq type system itself prevents a position-dependent log-partition function from type-checking.
GapInvariance.v is the 57th file in the Fall Risk formal verification program (56 files, 875+ theorems, 0 Admitted prior to this addition). The Coq file formalizes the gap identities themselves (Theorems 1–5); the PPP corollaries are algebraic consequences stated here in prose.
4. Empirical Confirmation
The theorem was discovered during CJ-52D (March 25, 2026), when PPP template extraction for a 70B declared-lineage distillation pair was run in both raw-logit and log-softmax domains. Results were identical to 10⁻⁸ precision:
| Metric | Raw logits | Log-softmax | Residual |
|---|---|---|---|
| Centroid distance | 0.89102141... | 0.89102143... | ~10⁻⁸ |
| CRP distance | 2.10881180... | 2.10881180... | ~10⁻⁸ |
| Self-baseline | 0.32909214... | 0.32909214... | ~10⁻⁹ |
The residual at 10⁻⁸ is floating-point arithmetic noise from the exp/log round-trip, consistent with IEEE 754 double-precision accumulation error. The mathematical discrepancy is exactly zero. Separately, CJ-40 (March 1, 2026) found that speculative decoding is transparent to the measurement at 10.6% residual (d(SD, V-pure) / d(V-pure, D-pure) = 0.106). This is consistent with the theorem: the accept/reject mechanism does not apply rank-dependent logit shifts. A full formal treatment of speculative decoding transparency would require separate work on the stochastic acceptance mechanism.
5. What This Changes
The Gap Cancellation Theorem retroactively strengthens four components of the published series.
Paper 2 [2]: API-wall transparency. Paper 2 empirically validated that the order-statistic gap geometry "survives API truncation" across 6 models, 3 providers, and 3 sessions. The theorem proves the gap geometry does not merely survive — it is mathematically invariant to the log-softmax transformation. Any δ-norm deviation observed through APIs (Paper 2 reported 0.297–0.312 versus the raw-logit prediction of 0.318) is now precisely attributable: the log-softmax wall is transparent by construction; only truncation to top-K, provider-specific quantization, and coverage limitations produce deviation. This narrows the diagnostic from "something about the API might change the measurement" to "only truncation and quantization change the measurement."
Paper 4 [4]: Provenance measurement. Paper 4 validated provenance detection across multiple teacher-student-protocol combinations with PPP-residualized templates. The theorem establishes that functional provenance measurement is immune to serving-time logit transforms by construction, not merely robust to them empirically.
Paper 12 [6]: Domain-invariance citation. Paper 12 references the domain-invariance of PPP gap measurements as established in a companion note. This technical note is that companion note. The G₁ concentration results reported in Paper 12 — including the sign-oscillating morphology in Mistral — are properties of the models, not artifacts of whether the measurement was conducted in logit or logprob space.
APINoSpoofing.v: Geometric foundation. The shift-equivariance theorem in APINoSpoofing.v (41 theorems, 0 Admitted) proves that β̂ subtraction absorbs exactly the uniform scale direction, leaving (d−1) expensive structural directions for an attacker. GapInvariance.v provides the geometric explanation: constant shifts are the only free direction in gap space because they are the only transforms that leave all gaps unchanged. The attacker has one free axis (uniform shift, absorbed by β̂) and (d−1) expensive axes (structural, requiring KL expenditure per component). The gap cancellation theorem and the budget exhaustion theorem together fully characterize the attacker's action space in the PPP measurement domain.
6. Scope
The theorem applies to any scoring function that computes order-statistic gaps from a logit or log-probability vector, to PPP residualization and any downstream residualization whose scale estimator is itself a function of the gap vector and preserves the affine behavior established above, and to any distance metric applied to the residualized template.
The theorem does not protect against rank-changing perturbations (reordering which tokens occupy which rank positions), non-uniform rank-dependent logit perturbations (which change gap magnitudes differentially), or model replacement (which changes the entire gap structure). These are the attack classes addressed by APINoSpoofing.v's budget exhaustion framework: they require per-component KL expenditure that exceeds the attacker's coherence budget.
The theorem also does not address truncation effects (reporting only top-K logprobs discards information about lower-ranked gaps) or provider-specific quantization (rounding logprob values to fixed precision). These are empirical concerns that require measurement-based characterization, as conducted in [2] and [4].
References
View 7 references ↓
[1] A. R. Coslett, "The δ-Gene: Inference-Time Physical Unclonable Functions from Architecture-Invariant Output Geometry," 2026. DOI: 10.5281/zenodo.18704275
[2] A. R. Coslett, "Template-Based Endpoint Verification via Logprob Order-Statistic Geometry," 2026. DOI: 10.5281/zenodo.18776711
[3] A. R. Coslett, "The Geometry of Model Theft: Distillation Forensics, Adversarial Erasure, and the Illusion of Spoofing," 2026. DOI: 10.5281/zenodo.18818608
[4] A. R. Coslett, "Provenance Generalization and Verification Scaling for Neural Network Forensics," 2026. DOI: 10.5281/zenodo.18872071
[5] A. R. Coslett, "Post-Hoc Disclosure Is Not Runtime Proof: Model Identity at Frontier Scale," 2026. DOI: 10.5281/zenodo.19216634
[6] A. R. Coslett, "Family-Dependent Response to Reasoning Distillation Across Structural and Functional Identity Layers," 2026. DOI: 10.5281/zenodo.19298857
[7] H. A. David and H. N. Nagaraja, Order Statistics, 3rd edition, Wiley, 2003.
Cite this paper
Acknowledgments
Portions of this research were developed in collaboration with AI systems. All scientific claims, proofs, and editorial decisions remain the sole responsibility of the author.
Supplementary Material
This note is accompanied by GapInvariance.v, a Coq proof file that formally verifies the five gap-invariance theorems described in §2: constant-shift invariance, positive-scale equivariance, affine scaling, log-softmax invariance, and general position-independent shift invariance. The file proves 5 theorems from 2 named axioms (OS1 and OS2), with no unresolved obligations (Admitted), and compiles cleanly under the Rocq Prover 9.1.1 (the current release of the Coq proof assistant, compiled with OCaml 5.4.0). It is available as a supplementary file alongside this note on Zenodo.
Patent Disclosure
The measurement protocol underlying the PPP framework operates within the scope of U.S. Provisional Patent Applications 63/982,893, 63/990,487, 63/996,680, and 64/003,244. All four provisional patents are assigned to Fall Risk AI, LLC.