diff --git a/research/paid-return-bridge-audit/AUDIT.md b/research/paid-return-bridge-audit/AUDIT.md new file mode 100644 index 0000000000..23671c01b5 --- /dev/null +++ b/research/paid-return-bridge-audit/AUDIT.md @@ -0,0 +1,202 @@ +# Conditional paid-return, approximation and invoice audit + +**Verdict: no gap found in the implication in PR5526 REPAIR.md Sections 2–4, +under the stated invariant-history, unitary-coset and one-field pricing +premises.** This is an independent AI-assisted derivation and exact finite +corroboration. It does not independently establish the actual caller's +observation inventory or grade claims, prove the Clifford Gram theorem anew, +or constitute proof-kernel/human acceptance. + +Audited source: Ali Romman's PR5526 at +`45f7de73b168721cdf7ec8c1769b1b594493716a`, retained on canonical main +`5e0052ca0aa3036a3afa8b0438927377c8d97d53`. SOURCES.json binds the exact +documents, declarations and receipts consumed here. DLamdata's PR5547 audits +the earlier core Gram theorem, explicitly excluding this later bridge. + +## 1. Fix one width and make the premises explicit + +Let V be a complex Hilbert space of dimension d. In the source, +d = 2^(17f). Let H be a finite projective unitary group of h elements, +represented on V, and let A be the linear span of its chosen unitary lifts. +Products may acquire scalar phases: A remains a unital algebra. Assume +dim A = h. Work in the finite-dimensional space of operator rows +Hom(V^b,V), with inner product tr(R* S)/d. + +The initial history module M is A-invariant. Each required row t_j has +one unitary target T_j in its own input position j, with zeros elsewhere. +Let F be the frame with bh columns U_g t_j, for g in H and j in 1..b. +The consumed physical-alphabet premise is + + ||F c - m||^2 >= lambda ||c||^2 for all c and m in M, lambda > 0. (A) + +In PR5526, (A) follows from the lower Gram bound on the complete projective +Clifford alphabet and disjoint initial/target coefficient supports, separately +in every independent input column. It is NOT an orthogonality assertion. +The initial support is allowed to have relations among its own coefficients; +choose a representation in that support and apply the full Gram inequality. +The target coefficients are still c because the supports are disjoint. + +The source-specific b=104, allowed initial grades {0,1,7}, target grade 9, +left-grade invariance, complete original observations and same-capacity +premises remain inherited. The verifier checks their retained declarations +and source bytes. It does not replay the 5,408 native grade calculations or +establish that no additional machine observation exists. + +## 2. Arbitrary paid feedback does not bypass the quotient dimension + +Represent each new return b_i by its actual linear map on the original +independent inputs after composing its dependencies on earlier returns. +That map can be arbitrary; it need not lie in the Clifford span, be unitary, +or commute with A. For each completed prefix, available rows are in + + M + A b_1 + ... + A b_q. + +This follows by induction: ordinary steps are A-actions and scalar linear +combinations; adding a paid row adds its cyclic module. Keep a conceptual +history when a physical row is overwritten or cleared. Each map +A -> A b_i, a -> a b_i, is linear and surjective, so its image has dimension +at most h. Zero divisors can reduce that dimension and do not invalidate +the upper bound. Dependence of b_i on earlier returns does not increase it. + +Let Q be orthogonal projection onto M-perp. Taking the infimum in (A) +gives (QF)*QF >= lambda I_(bh). Thus QF has rank bh. If all targets are +returned, A-invariance implies that all their orbit columns are available. +Their projection must fit in N = Q(sum_i A b_i), whose dimension is at most +qh. Consequently bh <= qh and q >= b. No freeness or division-ring +assumption is used. Changing a frozen original paid input would change M +and lies outside this inference. + +## 3. The normalization and orbit factor in the error bound + +For arbitrary approximate returned rows y_j in the available module, set +e_j=t_j-y_j. Every U_g y_j is available. If P projects onto N, then + + sum_(g,j) ||U_g e_j||^2 >= ||(I-P) QF||_HS^2 + >= lambda (b-q)_+ h. + +For the last inequality, rank(P QF) <= qh, so its kernel has dimension +at least (b-q)h. On an orthonormal basis of this kernel, QF has squared +norm at least lambda per vector. Complete the basis and sum nonnegative +terms. This proves the rank-approximation inequality directly. + +Unitary left action makes the left side h sum_j ||e_j||^2. Divide by h +ONCE. If E stacks the b error rows, the chosen row norm gives + + d^(-1) ||E||_HS^2 >= lambda (b-q)_+. + +Since E maps V^b to V^b, rank(E) <= bd and +||E||_HS^2 <= bd ||E||_op^2. Hence + + ||E||_op^2 >= lambda (1-q/b)_+. + +Restriction to these inputs and selection of these outputs are contractions, +so the complete endpoint has at least this operator norm error. This is one +worst-case vector in a direct sum, not b simultaneous per-field maximizers. +The proof permits q and the linear program to depend on the fixed width. +It excludes nonlinear rounding/branching and free actions outside A. + +## 4. Independent exact fixtures, including nonorthogonal supports + +The new checker uses standard-library rational dense matrices, not the +source's Clifford/group-code implementation. Its main fixture has V=R^3, +H generated by the cyclic coordinate shift S, and T=diag(1,1,-1). +The six coefficient matrices I,S,S^2,T,ST,S^2T have normalized Gram matrix + + [ I_3 I_3/3 ] + [ I_3/3 I_3 ]. + +Thus its lower eigenvalue is 2/3. Removing the initial H-support gives +relative Gram matrix (8/9) I_3. With b separate inputs, these matrices +repeat block-diagonally. This example deliberately tests a nonzero overlap: +declaring independent supports orthogonal would give the false constant 1. +The sharper relative constant 8/9 is a fixture calculation, not a claimed +improvement to the 17-axis caller. + +The checker examines 175 prefixes with b=2 or 3, including 120 arbitrary +rational returns outside the initial-plus-target coefficient span. New +returns include a nonordinary shear of the preceding return. Exact +Gram-Schmidt projection computes the minimum total normalized squared error +over the entire available module. Each prefix satisfies both the quotient +dimension bound and the orbit/error identity. Direct target-return controls +attain (8/9)(b-q); these are enlarged-oracle fixtures, not native suppliers. + +A second, orthogonal fixture uses H={I,Z}, T=X and two two-dimensional +inputs. It exhausts all 81 ternary assignments of the four off-diagonal paid +row entries. The exact one-return error distribution is 64 cases at 1, +16 at 3/2, and one at 2. Diagonal entries already lie in the initial module. +Neither finite domain is claimed to enumerate arbitrary paid programs. + +Seven semantic controls expose normalization twice, a missing orbit division, +false orthogonality, cached targets, singular targets, discarded retained +history and a noninvariant initial history. In particular, with diagonal +ordinary algebra, one return [P0,P1] supplies the two singular rows [P0,0] +and [0,P1]. This verifies why counting target rows without full cyclic-module +dimension would be invalid. Four in-memory code defects must separately fail +their intended diagnostics, including a dropped rank-one charge and a changed +target credit. All checks use explicit exceptions and also run under -O. + +## 5. From source-declared invoice to a loss at every power tariff + +The checker parses only the literal P and Tar dictionaries in Dugongue's +retained mixed-thin checker; it does not execute it. Adding 104 rank-one jobs +matches REPAIR-INVOICE.json exactly. Original target credits stay fixed. +For d_r = P_r + 104 [r=1] - Tar_r, it computes ALL integer hinges +K(k)=sum_r d_r min(r,k), k=1..17: + + 5996, 7134, 7448, 6742, 5838, 4854, 3870, 2900, 1800, + 1576, 1352, 1128, 904, 680, 456, 232, 8. + +For an increasing concave phi with phi(0)=0, let +s_k=phi(k)-phi(k-1). The exact identity + + phi(r) = s_17 min(r,17) + sum_(k=1..16) (s_k-s_(k+1)) min(r,k) + +follows by telescoping slopes. Nonnegative coefficients prove the invoice +loss. For phi(r)=r^p, 00 and K(17)=8 make it strict. +With 96 returns K(17)=0 and the earlier hinges are positive, so positive +margin is still impossible; q<=95 is necessary. It is not a claim that +every q<=95 is profitable. At q=95 and p=1 the margin is exactly 1, showing +the rank-mass cutoff itself cannot be reduced by this argument. + +The reference saving is the SOURCE-BOUND rational +605457647/200000000000, not a lookup of a future selected record. For +p=1-saving, an independent rational series enclosure gives the margin + + [18018715749583/500000000000, 2252339468941/62500000000] + = [36.037431499166, 36.037431503056]. + +It contains the predecessor's finer interval and proves 36 < margin < 37. +Therefore positive margin permits at most 36 added positive-rank returns; +the inherited width-84 lambda=125/126 gives squared operator error at least +2125/3276. The same arithmetic checks the width-72 and q=95/103 bounds. + +The enclosure is independent of the existing interval engine. For each +integer rank r<=17, put z=(r-1)/(r+1). Sum 96 terms of +log r = 2 sum_(k>=0) z^(2k+1)/(2k+1). The omitted positive tail is at most +2 z^193 / (193 (1-z^2)). Monotonicity of exp(-x), its alternating +degree-9 lower and degree-8 upper sums for 0<=x<1, and outward rounding on +a 10^-12 grid bound r exp(-saving log r). Sum interval endpoints with the +appropriate signs of the paid/target coefficients. No floating point enters +the acceptance arithmetic. More endpoint digits are not this contribution; +the check independently closes the error-to-budget implication. + +## 6. What remains outside this audit + +The proof bridge is conditional on the source's complete initial history, +grade invariance and target/capacity model. Literal source-word and all-width +native correctness remain separate, as do the core Clifford Gram theorem, +one-return-per-positive-rank-job pricing contract, precision/storage, new +multi-output suppliers, and the complete multiplication theorem. The +histograms are optimistic source declarations, not a fresh physical recount. +The checker consumes receipts as declarations and does not call them a replay. + +Credit: Ali Romman's PR5526 supplies the reviewed theorem and application; +Chris R / Clear1nsight's PR5425/5446 and Ali Romman's PR5449 supply the history +dimension method; Dugongue/PR4948 and Chris R/PR4978 supply the frozen caller +and its prior audit; DLamdata/PR5547 identifies this unaudited bridge. The +existing invoice-comparator lineage, including mightyOil, and zxv's interval +arithmetic retain credit. Projection, dimension, concave-order telescoping, +and log/exponential series are classical methods. No new general lower-bound +theorem or literature-priority claim is made. Prepared for +josecarlosgonzalezroque-design with substantial OpenAI Codex assistance; +Apache-2.0. No subagents or independent human reviewers were used. diff --git a/research/paid-return-bridge-audit/README.md b/research/paid-return-bridge-audit/README.md new file mode 100644 index 0000000000..326b353be6 --- /dev/null +++ b/research/paid-return-bridge-audit/README.md @@ -0,0 +1,111 @@ +# Independent audit of the paid-return/error/invoice bridge + +**No gap found in PR5526 REPAIR.md Sections 2–4, conditional on the declared +initial-history, target-coset and pricing premises.** This audits the later +repair theorem expressly left outside DLamdata's [PR5547](https://github.com/CrocSwap/integer-mult-bounds/pull/5547). +It supplies an independent written derivation, exact rational fixtures and an +independent enclosure of the declared invoice. The theorem and bounds remain +Ali Romman's and the credited predecessors' work. + +The [audit](AUDIT.md) checks why arbitrary linear feedback does not bypass +the quotient-dimension bound, why disjoint coefficient support does not mean +orthogonality, and why the orbit multiplicity and payload normalization occur +exactly once. Under the source premises, 104 extra field returns are necessary, +while the frozen reference-tariff margin permits at most 36. The resulting +width-84 squared operator-error floor remains 2125/3276. No new kappa, +native supplier, selected-frontier change or proof-kernel acceptance is claimed. + +## Evidence and reproduction + +Python 3.12 and the standard library suffice. From the repository root: + +```sh +python -B scripts/research_package.py --package research/paid-return-bridge-audit +``` + +The registered commands run the following in normal and optimized modes: + +```sh +python -I -W error -B research/paid-return-bridge-audit/verify.py +python -I -W error -B research/paid-return-bridge-audit/mutations.py +``` + +They print `PASS_PAID_RETURN_BRIDGE_AUDIT` and +`PASS_PAID_RETURN_BRIDGE_MUTATIONS controls=4`. The complete recomputed +receipt is available with `verify.py --emit`; normal replay compares +[RESULT.json](RESULT.json) without writing it. [VALIDATION.json](VALIDATION.json) +records the actual environment and completed checks. + +- 175 exact prefix checks in two/three-input cyclic-unitary fixtures include + 120 new returns outside the initial-plus-target coefficient span. The + fixture's relative Gram constant is exactly 8/9, with nonzero initial/target + overlap; direct target returns attain its error bound. +- All 81 ternary one-return cases in a two-field Pauli fixture give the exact + normalized error distribution: 64 at 1, 16 at 3/2, one at 2. +- Seven semantic controls expose changed premises and normalization mistakes. + Four deliberately defective in-memory verifier copies fail their intended + diagnostics in each Python mode. Frozen files are never modified. +- Literal AST extraction binds the invoice to its frozen source dictionaries. + Direct sums check every integer hinge from 1 through 17. A separate rational + log/exponential series gives margin + `[36.037431499166, 36.037431503056]`, containing the source's finer enclosure + and proving the 36-return budget without importing its calculator. + +The finite cases corroborate the written general proof; they are not an +exhaustive search of arbitrary programs. The 8/9 fixture constant is not a +new constant for the actual caller. Eight live review inputs have exact Git +blob and SHA256 pins in [SOURCES.json](SOURCES.json). No predecessor executable +is imported or run. The source port list and grade receipts are consumed as +declarations, not relabelled as independently replayed native evidence. + +## Scope and coordination + +Base: canonical `5e0052ca0aa3036a3afa8b0438927377c8d97d53`, priority revision 7. +PR5526's reviewed source head is `45f7de73b168721cdf7ec8c1769b1b594493716a`. +The selected-source orientation passed; it is metadata validation only. +[TASK.json](TASK.json) retains the exact task card and explains the scope +change from formalization to an independent informal proof audit. The picker +nonce was `0ae98c6c6a57ad53401268db8aa558d4`. + +The [prospective claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5236#discussioncomment-19182242) +followed handoff and live overlap checks. PR5547 covers the core Gram theorem; +PR5549 the one-qubit threshold; PR5531 a different endpoint application. Those +are separate from this conditional repair bridge. Targeted all-state PR +searches, the live canonical discussion and relevant local notes were checked. +Sparse local coverage, arbitrary historical diffs and unpublished work remain +outside the overlap claim; absence of a match is not a novelty certificate. + +## Open next questions + +Independently bind the complete actual initial history and its 104 target +columns to the literal PR4948/4978 caller, including both mandatory source +clarifications. Start with the pinned observation list and recompute one +affected input column through all nine cuts, then extend coverage explicitly. +The blocker is full caller/observation coverage, which this conditional bridge +and receipt parsing do not supply. That audit could change whether this theorem +applies, even though its abstract implication is sound. + +Changed original paid inputs, free observations, target credits, ordinary +alphabets, capacities and multi-output suppliers require new contracts and +complete pricing. No additional fixed-invoice construction search is proposed. +See TASK.json for the structured handoff. + +## Credit + +Ali Romman supplies PR5526 and PR5449; Chris R / Clear1nsight supplies the +PR5425/5446 history arguments and PR4978 source audit; Dugongue supplies PR4948; +DLamdata supplies PR5547 and its explicit remaining scope. The existing +concave-order comparator, mightyOil and predecessors, zxv's interval engine, +and the full native/stabilizer lineage retain credit. Their source files and +notices are unchanged. Projection, rank, concave order and series bounds are +classical, not new general methods claimed here. + +Prepared for josecarlosgonzalezroque-design with substantial OpenAI Codex +assistance; Apache-2.0. No subagents, independent human review or proof +assistant were used. Full native/physical replay, selected cold replay, +precision/stock/tape obligations and supplier admission were not performed. + +## Credit + +Prepared by josecarlosgonzalezroque-design. Retain predecessor attribution and source-specific notices. +New work is Apache-2.0. Disclose substantial AI assistance in TASK.json. diff --git a/research/paid-return-bridge-audit/RESULT.json b/research/paid-return-bridge-audit/RESULT.json new file mode 100644 index 0000000000..aa166cf023 --- /dev/null +++ b/research/paid-return-bridge-audit/RESULT.json @@ -0,0 +1,215 @@ +{ + "invoice": { + "all_integer_hinges_q104": [ + 5996, + 7134, + 7448, + 6742, + 5838, + 4854, + 3870, + 2900, + 1800, + 1576, + 1352, + 1128, + 904, + 680, + 456, + 232, + 8 + ], + "all_integer_hinges_q96": [ + 5988, + 7126, + 7440, + 6734, + 5830, + 4846, + 3862, + 2892, + 1792, + 1568, + 1344, + 1120, + 896, + 672, + 448, + 224, + 0 + ], + "independent_margin_interval": [ + "18018715749583/500000000000", + "2252339468941/62500000000" + ], + "inherited_grades": [ + 0, + 1, + 7 + ], + "interval_method": "96-term positive log series; 9/8-term alternating exp; outward 10^-12 grid", + "paid": { + "1": 4754, + "2": 824, + "3": 1020, + "4": 254, + "5": 80, + "8": 224 + }, + "rank_mass_at_q95": -1, + "reference_max_returns_for_positive_margin": 36, + "reference_saving": "605457647/200000000000", + "reference_width84_operator_error_squared": "2125/3276", + "source_error_floors": { + "any_profitable_repair_operator_error_squared_from_width_72": "1/104", + "any_profitable_repair_operator_error_squared_from_width_84": "125/1456", + "operator_error_squared_at_103_returns_and_width_84": "125/13104" + }, + "source_ports": [ + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 21, + 22, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 80, + 81, + 82, + 83, + 84, + 85, + 87, + 88, + 89, + 90, + 91, + 92, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 109, + 110 + ], + "target_grade": 9, + "targets": { + "4": 56, + "7": 14, + "8": 94, + "9": 876, + "17": 224 + } + }, + "module": { + "minimum_errors_by_b_and_q": { + "2:0": "16/9", + "2:1": "66347045/64236924", + "2:2": "43922522888462/89619968495079", + "3:0": "8/3", + "3:1": "2061179/1030068", + "3:2": "307884925646870/226938069518661", + "3:3": "14310023579419757356393/15551650430191095783795" + }, + "prefix_cases": 175, + "relative_gram_lower": "8/9", + "returns_outside_initial_and_target_span": 120, + "whole_gram_lower": "2/3" + }, + "scope": "Conditional proof bridge and declared invoice; no native replay or new kappa", + "semantic_controls": [ + "cache_a_target_without_reducing_missing_count", + "drop_unitary_target_premise", + "forget_retained_history_after_clear", + "normalize_by_payload_dimension_twice", + "omit_orbit_division", + "pretend_disjoint_supports_orthogonal", + "use_noninvariant_initial_history" + ], + "source_inputs": 8, + "status": "PASS_PAID_RETURN_BRIDGE_AUDIT", + "ternary_one_return_errors": { + "1": 64, + "2": 1, + "3/2": 16 + } +} diff --git a/research/paid-return-bridge-audit/SOURCES.json b/research/paid-return-bridge-audit/SOURCES.json new file mode 100644 index 0000000000..53af1aa540 --- /dev/null +++ b/research/paid-return-bridge-audit/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/clifford-pointwise-faithfulness/APPLICATION.md", + "usage": "input", + "git_blob": "bc375ba2eb6956b14b9850ea42f9623b54519653", + "sha256": "babf6ca32983a2820199d3d49d70da6cd08aecee524e58460d5489b94382d107" + }, + { + "path": "research/clifford-pointwise-faithfulness/PROOF.md", + "usage": "input", + "git_blob": "465009d9d1b6947e80e6f1e868022f47ddab1f3c", + "sha256": "45483e4b5f604a5e70602c5caaa4394d4a0d0d1a6d0b6e8a93b836d50b23f764" + }, + { + "path": "research/clifford-pointwise-faithfulness/REPAIR-INVOICE.json", + "usage": "input", + "git_blob": "735e29588ec639a6f4586b3e3bc0e1e1634d7c45", + "sha256": "bc652988ab37af46c2f4617312daf786e6ce71d94b79501a67ea11ee2976fe95" + }, + { + "path": "research/clifford-pointwise-faithfulness/REPAIR-RESULT.json", + "usage": "input", + "git_blob": "015cce7b0cbd37af4a1093dc2c4f5bde48d9753c", + "sha256": "4518525d4cd006516a28f91297b7e6a1841673c1ed4bb4677c8005aa46a6d366" + }, + { + "path": "research/clifford-pointwise-faithfulness/REPAIR.md", + "usage": "input", + "git_blob": "417748bf8620ef23330dfd30d823b4e89370d263", + "sha256": "4b1ec6a8c41dd8e5d49f33c926738b18a41b7cf28d8e81b68faa2ddc59fa3e23" + }, + { + "path": "research/passive-saved-query-ceiling/evidence/INDEPENDENT.json", + "usage": "input", + "git_blob": "d031b7db0b41aeaa99313fb8880a8dbc0c71bcb9", + "sha256": "bfbfeb0a835e11ef9a4638f57e9179758e7bda560c58993e26c6ec9cde8a47d9" + }, + { + "path": "research/passive-saved-query-ceiling/evidence/frozen/pr4948-mixed-thin-gate/check.py", + "usage": "input", + "git_blob": "bee0ff7c400dd91dc7d05f893c7a211a28f7028f", + "sha256": "fe7db972d7ae238b21f8a453c21243360d131d728a76b91a469dacf447629582" + }, + { + "path": "research/passive-saved-query-ceiling/evidence/frozen/pr4948-saved-query-macro-gate/GRADE-GATE.json", + "usage": "input", + "git_blob": "75481eb1e4e62311444d1e73e7f15f14e949476f", + "sha256": "8267ff814fd7fa86638b6ce6384f0ac717a341d871bd302742de6aaf8ba00b6d" + } + ] +} diff --git a/research/paid-return-bridge-audit/TASK.json b/research/paid-return-bridge-audit/TASK.json new file mode 100644 index 0000000000..62b09ee2c7 --- /dev/null +++ b/research/paid-return-bridge-audit/TASK.json @@ -0,0 +1,97 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Independent informal proof audit of PR5526 REPAIR.md Sections 2-4: the arbitrary-linear-return module/error bridge and its declared invoice.", + "scope_change_reason": "The picker selected independent verification. Live overlap showed PR5547 had audited the core Clifford theorem but explicitly excluded the later repair theorem and invoice. This audits that implication before any formalization, retaining native source facts as premises.", + "bottleneck_link": "Checks whether the fixed observation/capacity contract really rules out affordable exact or small-error repair; a false bridge could prematurely exclude a research route.", + "budget_minutes": 60, + "stop_rule": "Stop after the conditional bridge proof, independent finite and invoice checks, semantic controls and reviewable handoff; no fixed-invoice search or full native replay.", + "outcome": "completed", + "evidence": "AUDIT.md; RESULT.json; verify.py; mutations.py; VALIDATION.json", + "author": "josecarlosgonzalezroque-design", + "ai_assistance": "Substantial OpenAI Codex assistance in proof review, implementation, verification and writing. One agent; no independent human or proof-assistant review.", + "open_questions": [ + { + "question": "Does the complete literal PR4948/4978 retained observation inventory satisfy the initial-history and target-coset premises at the actual caller?", + "why_it_matters": "The abstract implication cannot establish its own native/caller applicability; an extra observation or changed original paid input can invalidate it.", + "first_step": "Read both mandatory source clarifications and independently trace one zero-diagonal original input column through all nine cuts, then extend the coverage map.", + "blocked_by": "Complete independent source-to-observation and all-width grade coverage is outside this audit." + } + ], + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5236#discussioncomment-19182242", + "selection_seed": "0ae98c6c6a57ad53401268db8aa558d4" +} diff --git a/research/paid-return-bridge-audit/VALIDATION.json b/research/paid-return-bridge-audit/VALIDATION.json new file mode 100644 index 0000000000..2440b50b3f --- /dev/null +++ b/research/paid-return-bridge-audit/VALIDATION.json @@ -0,0 +1,73 @@ +{ + "checked_at_utc": "2026-10-25T18:53:01.316261+00:00", + "python": "3.12.10", + "platform": "Windows-11-10.0.26300-SP0", + "command": [ + "python", + "-B", + "scripts/research_package.py", + "--package", + "research/paid-return-bridge-audit" + ], + "exit_code": 0, + "elapsed_seconds": 16.563, + "stdout": "CHECK Source hashes; conditional module/approximation fixtures; exhaustive small domain; seven semantic controls; independent source-declared invoice and rational interval.\nPASS_PAID_RETURN_BRIDGE_AUDIT\nCHECK Source hashes; conditional module/approximation fixtures; exhaustive small domain; seven semantic controls; independent source-declared invoice and rational interval.\nPASS_PAID_RETURN_BRIDGE_AUDIT\nCHECK Four deliberate mathematical/accounting defects must fail their specific diagnostics.\nPASS_PAID_RETURN_BRIDGE_MUTATIONS controls=4\nCHECK Four deliberate mathematical/accounting defects must fail their specific diagnostics.\nPASS_PAID_RETURN_BRIDGE_MUTATIONS controls=4\nPASS_REGISTERED_RESEARCH_PACKAGE research/paid-return-bridge-audit outcome=completed\n", + "stderr": "", + "base_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "source_pr5526_head": "45f7de73b168721cdf7ec8c1769b1b594493716a", + "source_head_blob_comparison": "All eight input blob IDs matched the GitHub contents API at the exact PR5526 head; SHA256 and base Git pins are checked by the registered runner.", + "orientation": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY on the selected-source closure; metadata only, not native replay.", + "unrun": [ + "full native/caller replay", + "selected construction cold replay", + "full-history preflight", + "proof assistant", + "independent human review" + ], + "git_free_export": { + "checked_at_utc": "2026-10-25T18:56:59.960134+00:00", + "status": "PASS_READONLY_GIT_FREE_EXPORT", + "exported_files": 18, + "environment": "PATH empty; all export files have the Windows read-only attribute; same absolute Python 3.12.10 interpreter", + "checks": [ + { + "script": "verify.py", + "optimized": false, + "exit_code": 0, + "seconds": 6.656, + "stdout": "PASS_PAID_RETURN_BRIDGE_AUDIT\n", + "stderr": "" + }, + { + "script": "verify.py", + "optimized": true, + "exit_code": 0, + "seconds": 6.859, + "stdout": "PASS_PAID_RETURN_BRIDGE_AUDIT\n", + "stderr": "" + }, + { + "script": "mutations.py", + "optimized": false, + "exit_code": 0, + "seconds": 0.172, + "stdout": "PASS_PAID_RETURN_BRIDGE_MUTATIONS controls=4\n", + "stderr": "" + }, + { + "script": "mutations.py", + "optimized": true, + "exit_code": 0, + "seconds": 0.25, + "stdout": "PASS_PAID_RETURN_BRIDGE_MUTATIONS controls=4\n", + "stderr": "" + } + ], + "unchanged_inventory": true, + "local_validation_commit": "e48ad476f4bc4976ec8dc976b0874e0ddb962a25", + "publication_note": "Local replay commit; verifier, mutation driver and mathematical receipt bytes are unchanged in the publication. This receipt was extended afterward." + }, + "environment_overrides": "TEMP and TMP used a writable workspace directory after default temporary-folder cleanup was denied.", + "prepublication_main": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "prepublication_main_checked_utc": "2026-10-25T18:54:33Z" +} diff --git a/research/paid-return-bridge-audit/VERIFY.json b/research/paid-return-bridge-audit/VERIFY.json new file mode 100644 index 0000000000..e3f2366449 --- /dev/null +++ b/research/paid-return-bridge-audit/VERIFY.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/clifford-pointwise-faithfulness/APPLICATION.md", + "research/clifford-pointwise-faithfulness/PROOF.md", + "research/clifford-pointwise-faithfulness/REPAIR-INVOICE.json", + "research/clifford-pointwise-faithfulness/REPAIR-RESULT.json", + "research/clifford-pointwise-faithfulness/REPAIR.md", + "research/passive-saved-query-ceiling/evidence/INDEPENDENT.json", + "research/passive-saved-query-ceiling/evidence/frozen/pr4948-mixed-thin-gate/check.py", + "research/passive-saved-query-ceiling/evidence/frozen/pr4948-saved-query-macro-gate/GRADE-GATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source hashes; conditional module/approximation fixtures; exhaustive small domain; seven semantic controls; independent source-declared invoice and rational interval." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source hashes; conditional module/approximation fixtures; exhaustive small domain; seven semantic controls; independent source-declared invoice and rational interval." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/mutations.py" + ], + "timeout_seconds": 120, + "checks": "Four deliberate mathematical/accounting defects must fail their specific diagnostics." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/mutations.py" + ], + "timeout_seconds": 120, + "checks": "Four deliberate mathematical/accounting defects must fail their specific diagnostics." + } + ] +} diff --git a/research/paid-return-bridge-audit/mutations.py b/research/paid-return-bridge-audit/mutations.py new file mode 100644 index 0000000000..8df81e3139 --- /dev/null +++ b/research/paid-return-bridge-audit/mutations.py @@ -0,0 +1,33 @@ +#!/usr/bin/env python3 +"""Four deliberate audit defects must fail their mathematical diagnostics. + +Only in-memory copies of this package's verifier are modified. Frozen inputs +are not changed or executed. OpenAI Codex assistance; Apache-2.0. +""" +from pathlib import Path + +path = Path(__file__).with_name("verify.py") +original = path.read_text(encoding="utf-8") +cases = [ + ("dot(e, e)/d for e in errors", "dot(e, e)/(d*d) for e in errors", + "module_checks", "relative error lower bound"), + ("Q(1, 3) if j == k else 0", "Q(0) if j == k else 0", + "module_checks", "nonorthogonal cross Gram"), + ("repaired[1] += len(ports)", "repaired[1] += len(ports)-1", + "pricing_checks", "repair adds exactly the claimed 104 rank-one jobs"), + ("paid, targets = extract_invoice()", "paid, targets = extract_invoice(); targets[17] -= 1", + "pricing_checks", "original target credits retained exactly once"), +] +for old, new, entry, diagnostic in cases: + if original.count(old) != 1: + raise ValueError("mutation anchor must be unique: " + old) + namespace = {"__file__": str(path), "__name__": "audit_mutant"} + exec(compile(original.replace(old, new), str(path), "exec"), namespace) + try: + namespace[entry]() + except ValueError as error: + if str(error) != diagnostic: + raise ValueError("wrong mutation diagnostic: " + str(error)) from error + else: + raise ValueError("deliberate defect was not rejected: " + old) +print("PASS_PAID_RETURN_BRIDGE_MUTATIONS controls=4") diff --git a/research/paid-return-bridge-audit/verify.py b/research/paid-return-bridge-audit/verify.py new file mode 100644 index 0000000000..34dc301a54 --- /dev/null +++ b/research/paid-return-bridge-audit/verify.py @@ -0,0 +1,345 @@ +#!/usr/bin/env python3 +"""Independent exact checks of PR5526's conditional paid-return bridge. + +Prepared for josecarlosgonzalezroque-design with OpenAI Codex assistance. +Apache-2.0. No predecessor executable is imported or executed. +The universal argument and inherited premises are in AUDIT.md. +""" +import argparse +import ast +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +SOURCE = "research/clifford-pointwise-faithfulness/" +PASSIVE = "research/passive-saved-query-ceiling/evidence/" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def read_json(path): + return json.loads((ROOT / path).read_text(encoding="utf-8")) + + +def authenticate(): + sources = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + inputs = [item for item in sources["files"] if item["usage"] == "input"] + need(len(inputs) == 8, "eight declared immutable review inputs") + for item in inputs: + raw = (ROOT / item["path"]).read_bytes() + need(sha256(raw).hexdigest() == item["sha256"], "source bytes changed: " + item["path"]) + return len(inputs) + + +def dot(a, b): + return sum((x*y for x, y in zip(a, b, strict=True)), Q(0)) + + +def plus(a, b, factor=Q(1)): + return tuple(x + factor*y for x, y in zip(a, b, strict=True)) + + +def perpendicular(row, orthogonal): + row = tuple(map(Q, row)) + for vector in orthogonal: + row = plus(row, vector, -dot(row, vector)/dot(vector, vector)) + return row + + +def basis(rows): + result = [] + for row in rows: + residual = perpendicular(row, result) + if any(residual): + result.append(residual) + return result + + +def mm(a, b, d): + return tuple(sum(a[d*i+k]*b[d*k+j] for k in range(d)) + for i in range(d) for j in range(d)) + + +def transpose(a, d): + return tuple(a[d*j+i] for i in range(d) for j in range(d)) + + +def identity(d): + return tuple(Q(i == j) for i in range(d) for j in range(d)) + + +def block(matrix, column, count): + z = (Q(0),)*len(matrix) + return tuple(x for j in range(count) for x in (matrix if j == column else z)) + + +def left(matrix, row, d): + size = d*d + return tuple(x for start in range(0, len(row), size) + for x in mm(matrix, row[start:start+size], d)) + + +def orbit(rows, group, d): + return [left(g, row, d) for row in rows for g in group] + + +def squared_error(targets, rows, d): + orthogonal = basis(rows) + errors = [perpendicular(t, orthogonal) for t in targets] + return sum((dot(e, e)/d for e in errors), Q(0)) + + +def c3_fixture(count): + d = 3 + one = identity(d) + shift = tuple(Q(i == (j+1) % d) for i in range(d) for j in range(d)) + group = [one, shift, mm(shift, shift, d)] + target = tuple(Q((1, 1, -1)[i] if i == j else 0) + for i in range(d) for j in range(d)) + need(mm(group[-1], shift, d) == one, "cyclic unitary group closes") + need(all(mm(transpose(g, d), g, d) == one for g in group), "unitary orbit actions") + need(mm(transpose(target, d), target, d) == one, "unitary target") + history = orbit([block(one, j, count) for j in range(count)], group, d) + targets = [block(target, j, count) for j in range(count)] + frame = orbit(targets, group, d) + need(len(basis(history)) == 3*count, "initial module dimension") + need(len(basis(history+frame)) == 6*count, "disjoint full target modules") + # The two coefficient supports are independent, but are NOT orthogonal. + for j, a in enumerate(history): + for k, b in enumerate(frame): + need(dot(a, b)/d == (Q(1, 3) if j == k else 0), "nonorthogonal cross Gram") + initial = basis(history) + residual = [perpendicular(t, initial) for t in frame] + for j, a in enumerate(residual): + for k, b in enumerate(residual): + need(dot(a, b)/d == (Q(8, 9) if j == k else 0), "relative Gram is 8/9 I") + return d, group, history, targets, frame + + +def module_checks(): + cases = outside = 0 + minima = {} + for count in (2, 3): + d, group, history, targets, frame = c3_fixture(count) + full_support = basis(history+frame) + shear = tuple(map(Q, (1, 1, 0, 0, 1, 0, 0, 0, 1))) + need(shear not in group, "feedback need not be an ordinary action") + seed = 0x5526 + count + for trial in range(24): + available = list(history) + previous = (Q(0),)*(d*d*count) + for q in range(count+1): + if q: + fresh = [] + for _ in previous: + seed = (1664525*seed + 1013904223) % (1 << 32) + fresh.append(Q(seed % 11 - 5, 1 + (seed >> 8) % 3)) + returned = plus(tuple(fresh), left(shear, previous, d)) + outside += bool(any(perpendicular(returned, full_support))) + previous = returned + available += orbit([returned], group, d) + dim = len(basis(available)) - len(basis(history)) + need(dim <= q*len(group), "one return adds at most h quotient dimensions") + error = squared_error(targets, available, d) + need(error >= Q(8, 9)*max(count-q, 0), "relative error lower bound") + orbit_error = squared_error(frame, available, d) + need(orbit_error == len(group)*error, "unitary orbit factor cancels once") + key = str(count) + ":" + str(q) + minima[key] = min(minima.get(key, error), error) + cases += 1 + # The enlarged arbitrary-oracle model attains the HS lower bound. + for q in range(count+1): + available = history + orbit(targets[:q], group, d) + error = squared_error(targets, available, d) + need(error == Q(8, 9)*(count-q), "exact target returns attain fixture bound") + cases += 1 + need(outside > 0, "new paid rows outside the reviewed coefficient support") + return {"prefix_cases": cases, "returns_outside_initial_and_target_span": outside, + "relative_gram_lower": "8/9", "whole_gram_lower": "2/3", + "minimum_errors_by_b_and_q": {k: str(v) for k, v in sorted(minima.items())}} + + +def exhaustive_two_field(): + d = 2 + one = identity(d) + z = tuple(map(Q, (1, 0, 0, -1))) + x = tuple(map(Q, (0, 1, 1, 0))) + group = [one, z] + history = orbit([block(one, j, 2) for j in range(2)], group, d) + targets = [block(x, j, 2) for j in range(2)] + histogram = {} + # All four missing coefficients in {-1,0,1}; diagonal terms are in history. + for entries in product((-1, 0, 1), repeat=4): + row = tuple(map(Q, (0, entries[0], entries[1], 0, + 0, entries[2], entries[3], 0))) + error = squared_error(targets, history+orbit([row], group, d), d) + need(error >= 1, "exhaustive one-return error floor") + histogram[str(error)] = histogram.get(str(error), 0) + 1 + need(sum(histogram.values()) == 81 and histogram.get("1", 0) > 0, + "complete ternary domain and attaining cases") + return histogram + + +def semantic_controls(): + d, group, history, targets, frame = c3_fixture(2) + one_return = history + orbit([targets[0]], group, d) + error = squared_error(targets, one_return, d) + need(error == Q(8, 9), "normalization control fixture") + controls = { + "omit_orbit_division": error < Q(8, 9)*len(group), + "pretend_disjoint_supports_orthogonal": error < 1, + "normalize_by_payload_dimension_twice": error/d < Q(8, 9), + "cache_a_target_without_reducing_missing_count": + squared_error(targets, history+frame, d) < Q(8, 9)*2, + } + # One ordinary-stable return supplies two singular targets on distinct inputs. + p0, p1 = tuple(map(Q, (1, 0, 0, 0))), tuple(map(Q, (0, 0, 0, 1))) + z = tuple(map(Q, (1, 0, 0, -1))) + singular_targets = [block(p0, 0, 2), block(p1, 1, 2)] + packed = plus(*singular_targets) + controls["drop_unitary_target_premise"] = squared_error( + singular_targets, orbit([packed], [identity(2), z], 2), 2) == 0 + zero = (Q(0),)*len(packed) + controls["forget_retained_history_after_clear"] = ( + len(basis([packed, zero])) == 1 and len(basis([zero])) == 0) + controls["use_noninvariant_initial_history"] = ( + len(basis([packed])) < len(basis(orbit([packed], [identity(2), z], 2)))) + need(all(controls.values()), "semantic counterexamples expose weakened premises") + return sorted(controls) + + +def extract_invoice(): + path = PASSIVE + "frozen/pr4948-mixed-thin-gate/check.py" + tree = ast.parse((ROOT / path).read_text(encoding="utf-8")) + selected = {} + for node in tree.body: + if isinstance(node, ast.Assign) and len(node.targets) == 1: + name = node.targets[0] + if isinstance(name, ast.Name) and name.id in ("P", "Tar"): + need(name.id not in selected, "unique literal invoice assignment") + selected[name.id] = ast.literal_eval(node.value) + need(set(selected) == {"P", "Tar"}, "both source invoice dictionaries found") + for profile in selected.values(): + need(all(type(r) is int and type(n) is int and r > 0 and n > 0 + for r, n in profile.items()), "positive integer rank histogram") + return selected["P"], selected["Tar"] + + +def log_interval(r, terms=96): + z = Q(r-1, r+1) + total, power = Q(0), z + for k in range(terms): + total += 2*power/(2*k+1) + power *= z*z + tail = 2*power/((2*terms+1)*(1-z*z)) + return total, total+tail + + +def exp_minus(x, terms): + need(0 <= x < 1, "alternating exponential terms decrease") + total = term = Q(1) + for k in range(1, terms+1): + term *= -x/k + total += term + return total + + +def power_interval(r, saving): + if r == 1: + return Q(1), Q(1) + lo, hi = log_interval(r) + lower = r*exp_minus(saving*hi, 9) + upper = r*exp_minus(saving*lo, 8) + scale = 10**12 + return Q((lower*scale).__floor__(), scale), Q((upper*scale).__ceil__(), scale) + + +def pricing_checks(): + paid, targets = extract_invoice() + gate = read_json(PASSIVE + "frozen/pr4948-saved-query-macro-gate/GRADE-GATE.json") + ports = gate["actual_source_zero_diagonal_ports"] + need(len(ports) == len(set(ports)) == 104 and ports == sorted(ports), + "104 distinct declared source ports") + inherited = read_json(PASSIVE + "INDEPENDENT.json") + need(inherited["earlier_grades"] == [0, 1] and inherited["target_grade"] == 9 + and inherited["post_FULL_unselected_grade_census"] == {"7": 5408}, + "inherited grade declarations match the audited implication") + declared = read_json(SOURCE + "REPAIR-INVOICE.json") + repaired = dict(paid) + repaired[1] += len(ports) + need(repaired == {int(k): v for k, v in declared["paid"].items()}, + "repair adds exactly the claimed 104 rank-one jobs") + need(targets == {int(k): v for k, v in declared["targets"].items()}, + "original target credits retained exactly once") + def hinges(q): + return [sum(n*min(r, k) for r, n in paid.items()) + q + - sum(n*min(r, k) for r, n in targets.items()) for k in range(1, 18)] + h104, h96, h95 = hinges(104), hinges(96), hinges(95) + need(min(h104) > 0 and h104[-1] == 8, "exact repair loses every power tariff") + need(min(h96) == 0 and h96[-1] == 0 and min(h96[:-1]) > 0, + "96 returns exhaust rank mass and every concave margin") + need(h95[-1] == -1, "95 threshold is necessary, not excluded by rank mass") + source = read_json(SOURCE + "REPAIR-RESULT.json") + need(source["new_returns_required"] == len(ports) + and source["first_width"] == 72 and source["later_width"] == 84, + "declared return and width thresholds") + for row in source["optimistic_invoice_comparison"]["hinges"]: + need(row["value"] == (h104[row["rank"]-1] if row["rank"] else 0), + "all saved support hinges agree with independent sums") + saving = Q(source["reference_tariff_budget"]["reference_saving"]) + intervals = {r: power_interval(r, saving) for r in sorted(set(paid) | set(targets))} + lower = sum(targets.get(r, 0)*lo - paid.get(r, 0)*hi + for r, (lo, hi) in intervals.items()) + upper = sum(targets.get(r, 0)*hi - paid.get(r, 0)*lo + for r, (lo, hi) in intervals.items()) + need(36 < lower <= upper < 37, "independent reference budget is strictly between 36 and 37") + source_lo, source_hi = map(Q, source["reference_tariff_budget"]["margin_interval"]) + need(lower <= source_lo <= source_hi <= upper, "predecessor interval fits independent enclosure") + for width, value in ((72, Q(1, 9)*(1-Q(36, 104))), + (84, Q(125, 126)*(1-Q(36, 104)))): + need(Q(source["reference_tariff_budget"]["operator_error_squared_from_width_" + str(width)]) + == value, "reference-budget approximation consequence") + expected_floors = { + "any_profitable_repair_operator_error_squared_from_width_72": Q(1, 9)*(1-Q(95, 104)), + "any_profitable_repair_operator_error_squared_from_width_84": Q(125, 126)*(1-Q(95, 104)), + "operator_error_squared_at_103_returns_and_width_84": Q(125, 126)*(1-Q(103, 104)), + } + for key, value in expected_floors.items(): + need(Q(source[key]) == value, "source approximation consequence: " + key) + return {"source_ports": ports, "inherited_grades": [0, 1, 7], "target_grade": 9, + "paid": paid, "targets": targets, "all_integer_hinges_q104": h104, + "all_integer_hinges_q96": h96, "rank_mass_at_q95": h95[-1], + "reference_saving": str(saving), + "independent_margin_interval": [str(lower), str(upper)], + "reference_max_returns_for_positive_margin": 36, + "reference_width84_operator_error_squared": str(Q(125, 126)*(1-Q(36, 104))), + "source_error_floors": {k: str(v) for k, v in expected_floors.items()}, + "interval_method": "96-term positive log series; 9/8-term alternating exp; outward 10^-12 grid"} + + +def run(): + return {"status": "PASS_PAID_RETURN_BRIDGE_AUDIT", "source_inputs": authenticate(), + "module": module_checks(), "ternary_one_return_errors": exhaustive_two_field(), + "semantic_controls": semantic_controls(), "invoice": pricing_checks(), + "scope": "Conditional proof bridge and declared invoice; no native replay or new kappa"} + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print the complete recomputed receipt") + args = parser.parse_args() + result = run() + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.emit: + print(encoded, end="") + else: + need(json.loads((HERE / "RESULT.json").read_text(encoding="utf-8")) == json.loads(encoded), + "saved audit receipt differs") + print(result["status"])