diff --git a/research/proof-explicit-4p-error/README.md b/research/proof-explicit-4p-error/README.md new file mode 100644 index 0000000000..e835e72bda --- /dev/null +++ b/research/proof-explicit-4p-error/README.md @@ -0,0 +1,158 @@ +# Explicit dimension exponent for the 2^{-4p} sentence + +**Scoped audit of one #4100 sentence. No new κ. #4100 is not accepted.** + +## Result + +In Cinna Davis's `research/unconditional-batched-crt/PROOF.md`, the source-transform +error claim says that polynomially many full-array norm changes cost at most +`2^{O(p)}`, because `T=2^{Θ(p)}`, and that a sufficiently large fixed `C` then +makes every absolute coefficient error smaller than `2^{-4p}`. + +That product reading does not follow from the size section. With the parameters +PROOF.md defines, `log2 T` is within two bits of `b=p/6`. Charging `p` factors +of `T` therefore costs `2^{Θ(p^2)}` bits, not `2^{O(p)}`. The cited sentence does +not determine a working-precision coefficient. + +The same size section does determine the exponent. For every integer `n≥4`, +`b=ceil(log2 n)`, `p=6b` and `T` the unique power of two in `[4n/b, 8n/b)`: + + b − floor(log2 b) + 1 ≤ log2 T ≤ b + 2 − floor(log2 b). + +Both ends are attained (`n=5` gives the lower bound, `n=4` the upper). In +particular `log2 T ≤ p/6 + 2 − floor(log2 b)`. For `b≥8` this is at most `b−1`, +so `T<2^b`, which is the cutoff already checked by #4320. + +Under the **one-factor** reading — at most `m` factors of `T`, times a fixed +`constant · p^{degree}` — an explicit `C` is enough: + +| Charge | `C` | Holds for every bucket | +| --- | ---: | --- | +| one `T` | 5 | `b≥2` | +| one `T` and `p^{10}` | 5 | `b≥13` | +| one `T` and `p^{10}` | 8 | `b≥2` | +| `16 p^2 · T` | 5 | `b≥3` | +| `16 p^2 · T` | 6 | `b≥2` | +| `512 p^5 · T` | 5 | `b≥8` | +| `512 p^5 · T` | 7 | `b≥2` | +| six factors of `T`, times `p^{10}` | 5 | never, through `b<400` | +| six factors of `T`, times `p^{10}` | 6 | `b≥9` | + +The `16 p^2` and `512 p^5` rows are what GAUSSIAN.md's displayed dominance +bounds give for one inverse, **if** the row gap is at least `1/(16p^2)` and the +bandwidth is an integer `≤ p−1`. They are not a count of how many such inverses +the circuit applies. Six factors at `C=5` leave no linear room: each factor +costs about `p/6` bits, and `4 + 6/6 = 5`. + +#4320's open question 1 asked for this constant and said the row gap blocked +it. The product-reading failure and the exponent lemma do not use the row gap. +The row gap remains the hypothesis that turns GAUSSIAN.md's inverse into the +polynomial `16 p^2` or `512 p^5`. + +## Scope + +Card `uniform-transfer-audit`, refined to PROOF.md's `2^{-4p}` amplification +sentence at the parameters of its size section. Priority revision 7. Base +`12fa8c5c844be21bfefb38a19503fbd867a11244`. The #4100 text is the retained +package at that commit (head `337d04939571a637aeab54a0f58f54fde811663a` on the +source PR). Selected κ stays `0.001672660197076918`. + +This is item 2 of the [#4311](https://github.com/CrocSwap/integer-mult-bounds/pull/4311) +shortest unaudited list: PROOF.md's `2^{-4p}` precision constant. #4320 audited +the algebraic identities and left this sentence open. #4325 audited chirp head +travel. Neither derives the exponent above. + +## Proof + +Let `b=ceil(log2 n)≥2` and let `k` be the integer defined by +`b·2^{k−1} < 4n ≤ b·2^k`. Then `T=2^k` is the unique power of two in +`[4n/b, 8n/b)`, because a second power of two cannot fit in an interval of +ratio 2, and the displayed inequality is exactly membership. + +Write `t=floor(log2 b)`. + +**Upper bound.** `n≤2^b`, so `b·2^k < 8n ≤ 2^{b+3}` and +`b·2^k ≤ 2^{b+3}−1`. Also `b≥2^t`, hence +`b·2^{b+3−t} ≥ 2^{b+3} > 2^{b+3}−1`. Therefore `2^k < 2^{b+3−t}`, so +`k ≤ b+2−t`. At `n=4`, `b=2`, `t=1` and `k=3`, equal to the bound. + +**Lower bound.** The smallest `n` in the bucket is `2^{b−1}+1`, so +`4n > 2^{b+1}`. Also `b<2^{t+1}`, hence `2^{b+1}/b > 2^{b−t}`. The minimizing +`k` still satisfies `2^k > 2^{b−t}`, so `k ≥ b−t+1`. At `n=5`, `b=3`, `t=1` +and `k=3`, equal to the bound. + +`k` is nondecreasing in `n` inside a bucket because the interval +`[4n/b, 8n/b)` only moves right. The verifier checks that directly for every +`n` from 4 through 200000, and checks both endpoints for every bucket through +`b=4096`. + +**Product reading.** Take `m(p)=p` norm changes and charge each at `T`. At +`n=2^b` the exponent is `p·log2 T`. That quotient over `p` is exactly +`14, 60, 250, 1016, 4086` at `b=16, 64, 256, 1024, 4096`. No constant `C0` +satisfies `p·log2 T ≤ C0·p` for every `b`. Replacing every norm change by the +full array dimension therefore does not cost merely `2^{O(p)}`. + +**One-factor reading.** `T ≤ 2^{b+2−t}` and `p=6b`, so +`constant · p^{degree} · T^{m} · 2^{−C p} < 2^{−4p}` as soon as + + constant · (6b)^{degree} < 2^{(C−4)·6b − m(b+2−t)}. + +The table is this comparison, exact, for every bucket from the stated cutoff +through `b=399`. + +**Conditional inverse.** Assume `δ ≥ 1/(16p^2)` and an integer bandwidth +`w ≤ p−1`. GAUSSIAN.md's formulas give +`‖H^{−1}‖_∞ ≤ δ^{−1} ≤ 16p^2` and + + ‖H^{−1}‖_1 ≤ δ^{−1} + 2w(1−δ)δ^{−2} + ≤ 512 p^5 − 512 p^4 − 32 p^3 + 48 p^2 + < 512 p^5. + +The verifier recomputes that polynomial. It does not prove the gap, and it +does not count how many inverses, Fourier scales or tensor factors sit on one +coefficient path. PROOF.md also names an `M<2^p` scale; the exponent lemma +replaces that `p` by `p/6 + O(log b)` whenever `M≤T`. + +## Evidence + +`verify.py` exits only after the sentence pins, the exhaustive size check, the +product-reading ratios, the conditional table and these failure controls: + +- the upper bound is false if decreased by one (`n=4`); +- `m=p` factors are not bounded by `10p` bits (`b=64`); +- `C=5` never absorbs six dimension factors on `2≤b<80`. + +No proof kernel, no Gaussian circuit execution, and no claim that a particular +`m` occurs in the program. + +## Reproduce + +From the repository root, Python 3.12: + +```sh +python3 scripts/research_package.py --package research/proof-explicit-4p-error --check-only +python3.12 scripts/research_package.py --package research/proof-explicit-4p-error +``` + +## Open next questions + +1. Count the factors of `T` on one coefficient of the three normalized + transforms, the pointwise product and the final `M` scale. + The count is the integer `m` in the table. The normalized butterfly + `H0/2` may contribute none; the final scale contributes one if `M≤T`. + Nothing in the size section blocks the count. A Gaussian factor still + requires the row-gap hypothesis before its norm is polynomial. +2. Make `δ ≥ 1/(16p^2)` effective after alias removal, truncation and + rounding, which is #4217's open question 1. + Until that holds, the `16 p^2` and `512 p^5` rows stay conditional. + This dimension lemma does not remove that hypothesis. + +## Credit + +The construction and the `2^{-4p}` sentence are Cinna Davis's #4100, with +OpenAI Codex assistance, and the retained Gaussian sources named in +GAUSSIAN.md. #4320 (Ryanson Jonathan, Claude) audited the surrounding +identities, proved `T<2^b` for `b≥8`, and left this sentence open. #4311 +(Ryanson Jonathan) listed it as unaudited obligation 2. This note and verifier +were prepared by unpaidmoon with substantial Cursor Grok assistance. +Apache-2.0. No independent human or formal-kernel acceptance is claimed. diff --git a/research/proof-explicit-4p-error/SOURCES.json b/research/proof-explicit-4p-error/SOURCES.json new file mode 100644 index 0000000000..895586cccd --- /dev/null +++ b/research/proof-explicit-4p-error/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/unconditional-batched-crt/GAUSSIAN.md", + "usage": "input", + "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242" + }, + { + "path": "research/unconditional-batched-crt/PROOF.md", + "usage": "input", + "git_blob": "406eb561cc8d6041ea3fba1a849653b654f2198c", + "sha256": "689fc7b01c5f04f77019ff02d1b79cb4f7020bd98e05b1052020bad295dec060" + } + ] +} diff --git a/research/proof-explicit-4p-error/TASK.json b/research/proof-explicit-4p-error/TASK.json new file mode 100644 index 0000000000..c7181b268c --- /dev/null +++ b/research/proof-explicit-4p-error/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Does PROOF.md's 2^{-4p} sentence follow from its size parameters, and which explicit C works for one factor of T?", + "scope_change_reason": "The card asks for one quantified #4100 implication. This package takes only the 2^{-4p} amplification sentence in PROOF.md, the obligation #4320 left open and #4311 listed second among unaudited steps. It does not audit CRT repair, the free-algebra lift, or the row gap.", + "bottleneck_link": "#4100 proposes an unconditional exponent above the selected kappa. The 2^{-4p} sentence is the recovery-precision step on that argument. A gap there blocks treating the proposed exponent as proved. This audit does not change the selected frontier.", + "budget_minutes": 60, + "stop_rule": "Stop after the dimension exponent, the product-reading counterexample, and the conditional one-factor table. Do not prove the row gap or execute the Gaussian circuit.", + "outcome": "completed", + "evidence": "verify.py pins the source sentences and checks the exponent for every n from 4 through 200000, every bucket through b=4096, the product quotients 14,60,250,1016,4086, and the conditional C table by exact powers of two. Failure controls reject a one-bit-tighter upper bound, a 10p product claim, and C=5 with six dimension factors.", + "author": "unpaidmoon", + "ai_assistance": "Cursor Grok 4.7", + "open_questions": [ + { + "question": "How many factors of T lie on one coefficient of the three normalized transforms, the pointwise product and the final M scale?", + "why_it_matters": "That integer is the m for which the conditional table supplies an explicit C. The product reading gives no such C.", + "first_step": "Trace PROOF.md's normalized H0/2 butterflies and the final multiplication by M, and record each factor whose modulus can be as large as T.", + "blocked_by": "Nothing in the size section. A Gaussian inverse on the same path still needs the row-gap hypothesis before its norm is the polynomial 16 p^2." + }, + { + "question": "Does alias removal, band truncation and rounding preserve a row gap of at least 1/(16p^2) for every large p?", + "why_it_matters": "GAUSSIAN.md's inverse bounds are conditional on that gap. Without it the 16 p^2 and 512 p^5 rows do not apply.", + "first_step": "Take #4217 open question 1 and the retained PR1673/PR1786 row-gap argument, and name the truncation and rounding defects they do not yet charge.", + "blocked_by": "The half-gap sentence is still an open hypothesis. This dimension lemma does not prove it." + } + ] +} diff --git a/research/proof-explicit-4p-error/VERIFY.json b/research/proof-explicit-4p-error/VERIFY.json new file mode 100644 index 0000000000..1583bb3c7e --- /dev/null +++ b/research/proof-explicit-4p-error/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/unconditional-batched-crt/GAUSSIAN.md", + "research/unconditional-batched-crt/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Source-sentence pins, dimension exponent through n=200000 and b=4096, product-reading quotients, conditional one-factor C table, and three failure controls." + } + ] +} diff --git a/research/proof-explicit-4p-error/verify.py b/research/proof-explicit-4p-error/verify.py new file mode 100644 index 0000000000..4b0dbacd61 --- /dev/null +++ b/research/proof-explicit-4p-error/verify.py @@ -0,0 +1,225 @@ +#!/usr/bin/env python3 +"""Dimension exponent of #4100's 2^{-4p} sentence, and the product-reading gap. + +The checker uses only the standard library. It binds two source sentences, +proves the size-section exponent for every admissible b, and checks the +conditional one-factor precision coefficient by exact integer comparison. +""" + +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PROOF = ROOT / "research/unconditional-batched-crt/PROOF.md" +GAUSSIAN = ROOT / "research/unconditional-batched-crt/GAUSSIAN.md" + +AMPLIFICATION = ( + "There are polynomially many\n" + "levels/groups per coefficient. Allowing even the full array dimension in\n" + "all norm changes costs at most2^O(p), since T=2^Theta(p)." +) + + +def ceil_log2(n): + if n < 1: + raise ValueError(n) + return (n - 1).bit_length() + + +def floor_log2(n): + if n < 1: + raise ValueError(n) + return n.bit_length() - 1 + + +def exponent_k(n): + """Unique k with T=2^k in [4n/b, 8n/b), b=ceil(log2 n).""" + b = ceil_log2(n) + if b < 2: + raise ValueError(n) + k = 0 + while (b << k) < 4 * n: + k += 1 + if k > b + 4: + raise AssertionError((n, b, k)) + if (b << k) >= 8 * n: + raise AssertionError(("interval missed", n, b, k)) + if k and (b << (k - 1)) >= 4 * n: + raise AssertionError(("not minimal", n, b, k)) + return b, 6 * b, k + + +def bucket_bounds(b): + """Proved bounds on k for every n with ceil(log2 n)=b and n>=4.""" + t = floor_log2(b) + if not ((1 << t) <= b < (1 << (t + 1))): + raise AssertionError(b) + # Upper. Admissible n satisfy n<=2^b, so b*2^k < 8n <= 2^{b+3}. + # Thus b*2^k <= 2^{b+3}-1. Since b>=2^t, + # b*2^{b+3-t} >= 2^{b+3} > 2^{b+3}-1, so 2^k < 2^{b+3-t} and k<=b+2-t. + if (b << (b + 3 - t)) < (1 << (b + 3)): + raise AssertionError(("upper comparison", b)) + # Lower. The smallest admissible n is 2^{b-1}+1, so 4n > 2^{b+1}. + # b<2^{t+1} makes 2^{b+1}/b > 2^{b-t}, hence 2^k > 2^{b-t} and k>=b-t+1. + if 4 * ((1 << (b - 1)) + 1) <= (1 << (b + 1)): + raise AssertionError(("lower comparison", b)) + return b - t + 1, b + 2 - t + + +def sum_holds(b, factors, degree, coefficient, constant): + """constant * (6b)^degree * T^factors * 2^{-coefficient * p} < 2^{-4p}. + + Uses the proved upper bound on log2 T, so a pass covers every n in the bucket. + """ + _, high = bucket_bounds(b) + room = (coefficient - 4) * 6 * b - factors * high + if room <= 0: + return False + return constant * pow(6 * b, degree) < (1 << room) + + +def first_b0(factors, degree, coefficient, constant, limit=400): + for start in range(2, limit): + if all(sum_holds(b, factors, degree, coefficient, constant) + for b in range(start, limit)): + return start + return None + + +def require_source_sentences(): + proof = PROOF.read_text(encoding="utf-8") + gaussian = GAUSSIAN.read_text(encoding="utf-8") + required = ( + (proof, "nominal p=6b"), + (proof, "power of two in [4n/b,8n/b)"), + (proof, AMPLIFICATION), + (proof, "absolute coefficient error less than 2^-4p"), + (gaussian, "row gap delta>=1/(16p^2)"), + (gaussian, "||H^-1||_infinity<=delta^-1"), + (gaussian, "||H^-1||_1<=delta^-1+2w(1-delta)delta^-2"), + (gaussian, "2^{-(C-O(1))p}"), + ) + for text, snippet in required: + if snippet not in text: + raise AssertionError("missing source sentence: " + snippet[:80]) + # Control: the gap is this sentence, not a nearby cost row. + if "costs at most 2^{p/6}" in proof: + raise AssertionError("source unexpectedly contains the explicit exponent") + + +def check_dimension(exhaustive_n=200000, bucket_limit=4096): + sharp_upper = sharp_lower = None + previous = None + for n in range(4, exhaustive_n + 1): + b, p, k = exponent_k(n) + low, high = bucket_bounds(b) + if not (low <= k <= high and p == 6 * b): + raise AssertionError((n, b, p, k, low, high)) + if previous is not None and b == previous[0] and k < previous[1]: + raise AssertionError(("k decreased", n, k, previous)) + previous = (b, k) + if k == high and sharp_upper is None: + sharp_upper = (n, b, k) + if k == low and sharp_lower is None: + sharp_lower = (n, b, k) + if sharp_upper != (4, 2, 3): + raise AssertionError(sharp_upper) + if sharp_lower != (5, 3, 3): + raise AssertionError(sharp_lower) + for b in range(2, bucket_limit + 1): + low, high = bucket_bounds(b) + _, _, k_min = exponent_k((1 << (b - 1)) + 1) + _, _, k_max = exponent_k(1 << b) + if k_min < low or k_max > high or k_min > k_max: + raise AssertionError((b, k_min, k_max, low, high)) + # Control: shaving one bit off the upper bound is false. + if exponent_k(4)[2] <= bucket_bounds(2)[1] - 1: + raise AssertionError("upper bound was not sharp") + return sharp_upper, sharp_lower + + +def check_product_reading(): + """m(p)=p factors of T are not a 2^{O(p)} amplification.""" + ratios = [] + expected = (3, 4, 14, 60, 250, 1016, 4086) + for b in (2, 4, 16, 64, 256, 1024, 4096): + low, _ = bucket_bounds(b) + _, p, k = exponent_k(1 << b) + if k < low: + raise AssertionError((b, k, low)) + ratios.append(k) + if p * k <= 10 * p and b >= 64: + raise AssertionError((b, p, k)) + if tuple(ratios) != expected or ratios != sorted(ratios): + raise AssertionError(ratios) + # Control: a uniform linear claim with coefficient 10 fails at b=64. + if ratios[3] <= 10: + raise AssertionError("product reading unexpectedly became O(p) with constant 10") + return ratios + + +def check_conditional_constants(): + claims = ( + # one factor T, no extra polynomial: C=5 for every b>=2 + (1, 0, 5, 1, 2), + # one T and p^10: C=5 from b=13; C=8 from b=2 + (1, 10, 5, 1, 13), + (1, 10, 8, 1, 2), + # infinity-norm inverse 16 p^2 times one T + (1, 2, 5, 16, 3), + (1, 2, 6, 16, 2), + # one-norm majorant 512 p^5 times one T + (1, 5, 5, 512, 8), + (1, 5, 7, 512, 2), + # six T factors need a linear coefficient past 4+6/6=5 + (6, 0, 6, 1, 2), + (6, 10, 6, 1, 9), + ) + found = [] + for factors, degree, coefficient, constant, expected in claims: + got = first_b0(factors, degree, coefficient, constant) + if got != expected: + raise AssertionError((factors, degree, coefficient, constant, got, expected)) + found.append(got) + # Control: six T factors leave no room at C=5, at every checked bucket. + if first_b0(6, 10, 5, 1) is not None: + raise AssertionError("C=5 unexpectedly absorbed six dimension factors") + if any(sum_holds(b, 6, 10, 5, 1) for b in range(2, 80)): + raise AssertionError("C=5 passed a six-factor bucket") + return found + + +def inverse_majorant(p): + """Displayed dominance bounds at delta>=1/(16p^2) and bandwidth <= p-1. + + The infinity norm is at most 16 p^2. The one-norm is at most + 512 p^5 - 512 p^4 - 32 p^3 + 48 p^2, which is < 512 p^5. + """ + if p < 1: + raise ValueError(p) + infinity = 16 * p * p + # 32*(p-1)*p^2*(16*p^2-1) is the expanded one-norm majorant before +16p^2. + expanded = 32 * (p - 1) * p * p * (16 * p * p - 1) + 16 * p * p + one = 512 * p**5 - 512 * p**4 - 32 * p**3 + 48 * p * p + if expanded != one or one >= 512 * p**5 or infinity != 16 * p * p: + raise AssertionError((p, infinity, one, expanded)) + return infinity, one + + +def main(): + require_source_sentences() + sharp_upper, sharp_lower = check_dimension() + ratios = check_product_reading() + thresholds = check_conditional_constants() + for p in range(1, 41): + inverse_majorant(p) + print("sharp_upper_witness", sharp_upper) + print("sharp_lower_witness", sharp_lower) + print("product_exponent_over_p", ratios) + print("conditional_b0", thresholds) + print("infinity_norm_p4", inverse_majorant(4)[0]) + print("one_norm_p4", inverse_majorant(4)[1]) + print("PASS_EXPLICIT_4P_DIMENSION") + + +if __name__ == "__main__": + main()