diff --git a/research/idempotent-path-rank-audit/CERTIFICATE.json b/research/idempotent-path-rank-audit/CERTIFICATE.json new file mode 100644 index 0000000000..41701eb6b8 --- /dev/null +++ b/research/idempotent-path-rank-audit/CERTIFICATE.json @@ -0,0 +1,1085 @@ +{ + "generated_controls": { + "arbitrary_internal_matrices": 60, + "completed_pairs": 30, + "dimensions": [ + 2, + 3, + 4, + 5, + 6 + ], + "generator": "2d elementary rational shears per label; independent uniform ranks 0..d", + "product_rank_histogram": { + "(0, 0)": 15, + "(1, 1)": 8, + "(2, 2)": 4, + "(3, 3)": 2, + "(4, 4)": 1 + }, + "seed": 71, + "stopping_rule": "Exactly 6 pairs in each dimension 2..6; no adaptive search", + "transcript_sha256": "87aaacd2713372ced5bd1f44d6398db8b921bd03874732ddf738741621512ea5", + "trials_per_dimension": 6 + }, + "independent": { + "assignment_seed": 71, + "controls": { + "false_converse_equal_product_ranks_implies_common_form": { + "P": [ + [ + 1, + 0 + ], + [ + 0, + 0 + ] + ], + "Q": [ + [ + 1, + 1 + ], + [ + 0, + 0 + ] + ], + "common_nondegenerate_symmetric_form_exists": false, + "direct_edge_excess": 2, + "ranks": { + "difference": 2, + "p": 1, + "pq": 1, + "q": 1, + "qp": 1 + }, + "signed_rank_change": 0, + "symmetric_form_equations": [ + "H_00 - H_01 = 0", + "H_01 = 0" + ] + }, + "false_excess_at_least_two_rank_pq": { + "P": [ + [ + 1, + 0 + ], + [ + 0, + 0 + ] + ], + "Q": [ + [ + 0, + 1 + ], + [ + 0, + 1 + ] + ], + "direct_edge_excess": 1, + "ranks": { + "difference": 1, + "p": 1, + "pq": 1, + "q": 1, + "qp": 0 + }, + "signed_rank_change": 0 + }, + "false_excess_at_least_two_rank_qp": { + "P": [ + [ + 0, + 1 + ], + [ + 0, + 1 + ] + ], + "Q": [ + [ + 1, + 0 + ], + [ + 0, + 0 + ] + ], + "direct_edge_excess": 1, + "ranks": { + "difference": 1, + "p": 1, + "pq": 0, + "q": 1, + "qp": 1 + }, + "signed_rank_change": 0 + }, + "false_identity_without_idempotence": { + "P": [ + [ + "1/2", + 0 + ], + [ + 0, + "1/2" + ] + ], + "Q": [ + [ + "1/2", + 0 + ], + [ + 0, + "1/2" + ] + ], + "direct_edge_excess": 0, + "invalid_identity_rhs": 2, + "ranks": { + "difference": 0, + "p": 2, + "pq": 2, + "q": 2, + "qp": 2 + }, + "signed_rank_change": 0 + }, + "false_unrestricted_shared_additive_block": { + "B": [ + [ + -1, + 0 + ], + [ + 0, + 0 + ] + ], + "P": [ + [ + 1, + 0 + ], + [ + 0, + 0 + ] + ], + "Q": [ + [ + 1, + 0 + ], + [ + 0, + 0 + ] + ], + "actual_excess": 0, + "direct_charge": 2, + "incorrectly_transferred_bound": 2, + "signed_rank_change": 2, + "source": [ + [ + 0, + 0 + ], + [ + 0, + 0 + ] + ], + "target": [ + [ + -1, + 0 + ], + [ + 0, + 1 + ] + ] + } + }, + "domain": { + "dimension": 2, + "entries_max": 3, + "entries_min": -3, + "idempotents": 44, + "matrices_examined": 2401, + "ordered_pairs": 1936, + "radius_rule": "assignment_seed % 4", + "stopping_rule": "Exhaust every matrix and every ordered idempotent pair" + }, + "method": "Explicit 2 by 2 determinant; no elimination or imported rank routine", + "product_rank_histogram": { + "0,0": 129, + "0,1": 152, + "1,0": 152, + "1,1": 1502, + "2,2": 1 + }, + "scope": "Finite independent evidence and explicit counterexamples to stronger statements; the unrestricted idempotent identity requires the written proof; no new kappa", + "status": "PASS_EXACT_BOUNDED_IDEMPOTENT_PATH_RANK_AUDIT" + }, + "inherited_controls": { + "compiled_endpoint_controls": [ + { + "ambient_dimension": 2, + "compiled_gates": 144, + "endpoint_pairs": [ + { + "exact_excess": 1, + "fixed": [ + 0, + 0 + ], + "spectator_rank": 1, + "stage": 0 + }, + { + "exact_excess": 1, + "fixed": [ + 0, + 1 + ], + "spectator_rank": 1, + "stage": 0 + }, + { + "exact_excess": 1, + "fixed": [ + 1, + 0 + ], + "spectator_rank": 1, + "stage": 0 + }, + { + "exact_excess": 1, + "fixed": [ + 1, + 1 + ], + "spectator_rank": 1, + "stage": 0 + }, + { + "exact_excess": 1, + "fixed": [ + 0, + 0 + ], + "spectator_rank": 1, + "stage": 1 + }, + { + "exact_excess": 1, + "fixed": [ + 0, + 1 + ], + "spectator_rank": 1, + "stage": 1 + }, + { + "exact_excess": 1, + "fixed": [ + 1, + 0 + ], + "spectator_rank": 1, + "stage": 1 + }, + { + "exact_excess": 1, + "fixed": [ + 1, + 1 + ], + "spectator_rank": 1, + "stage": 1 + }, + { + "exact_excess": 1, + "fixed": [ + 0, + 0 + ], + "spectator_rank": 1, + "stage": 2 + }, + { + "exact_excess": 1, + "fixed": [ + 0, + 1 + ], + "spectator_rank": 1, + "stage": 2 + }, + { + "exact_excess": 1, + "fixed": [ + 1, + 0 + ], + "spectator_rank": 1, + "stage": 2 + }, + { + "exact_excess": 1, + "fixed": [ + 1, + 1 + ], + "spectator_rank": 1, + "stage": 2 + } + ], + "label_rank": 1, + "name": "one_sided_rank_one", + "scope": "Actual endpoint matrices only; no full scalar/rank-sum certification" + }, + { + "ambient_dimension": 3, + "compiled_gates": 144, + "endpoint_pairs": [ + { + "exact_excess": 12, + "fixed": [ + 0, + 0 + ], + "spectator_rank": 4, + "stage": 0 + }, + { + "exact_excess": 12, + "fixed": [ + 0, + 1 + ], + "spectator_rank": 4, + "stage": 0 + }, + { + "exact_excess": 12, + "fixed": [ + 1, + 0 + ], + "spectator_rank": 4, + "stage": 0 + }, + { + "exact_excess": 12, + "fixed": [ + 1, + 1 + ], + "spectator_rank": 4, + "stage": 0 + }, + { + "exact_excess": 12, + "fixed": [ + 0, + 0 + ], + "spectator_rank": 4, + "stage": 1 + }, + { + "exact_excess": 12, + "fixed": [ + 0, + 1 + ], + "spectator_rank": 4, + "stage": 1 + }, + { + "exact_excess": 12, + "fixed": [ + 1, + 0 + ], + "spectator_rank": 4, + "stage": 1 + }, + { + "exact_excess": 12, + "fixed": [ + 1, + 1 + ], + "spectator_rank": 4, + "stage": 1 + }, + { + "exact_excess": 12, + "fixed": [ + 0, + 0 + ], + "spectator_rank": 4, + "stage": 2 + }, + { + "exact_excess": 12, + "fixed": [ + 0, + 1 + ], + "spectator_rank": 4, + "stage": 2 + }, + { + "exact_excess": 12, + "fixed": [ + 1, + 0 + ], + "spectator_rank": 4, + "stage": 2 + }, + { + "exact_excess": 12, + "fixed": [ + 1, + 1 + ], + "spectator_rank": 4, + "stage": 2 + } + ], + "label_rank": 2, + "name": "asymmetric_rank_two", + "scope": "Actual endpoint matrices only; no full scalar/rank-sum certification" + } + ], + "original_mutual_annihilation_rejections": [ + { + "ell": 1, + "reason": "Side edges require mutual, not one-sided, annihilation", + "rows": [ + 3, + 2 + ] + }, + { + "ell": 1, + "reason": "Side edges require mutual, not one-sided, annihilation", + "rows": [ + 1, + 3 + ] + }, + { + "ell": 2, + "reason": "Every side edge needs mutual annihilation", + "rows": [ + 3, + 2 + ] + }, + { + "ell": 2, + "reason": "Every side edge needs mutual annihilation", + "rows": [ + 1, + 3 + ] + } + ], + "original_triples": { + "h": 6, + "intersection_histogram": { + "0": 20, + "1": 180, + "2": 180, + "3": 20 + }, + "labels": 20, + "ordered_pairs": 400 + }, + "positive_contract_controls": 4 + }, + "scope": "Written proof plus finite exact evidence; no new circuit, no new kappa, no formal proof of the multiplication theorem", + "source_pins": { + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "checked_files": 23 + }, + "status": "PASS_EXACT_IDEMPOTENT_PATH_RANK_AUDIT", + "witnesses": { + "asymmetric_rank_two": { + "P": [ + [ + "1", + "0", + "0" + ], + [ + "0", + "0", + "0" + ], + [ + "0", + "0", + "1" + ] + ], + "Q": [ + [ + "0", + "1", + "0" + ], + [ + "0", + "1", + "0" + ], + [ + "0", + "0", + "1" + ] + ], + "direct_edge": { + "charge": 2, + "excess": 3, + "signed_rank_increment": -1 + }, + "independent_ranks": [ + 2, + 2, + 2, + 1, + 2 + ], + "profile": { + "d": 3, + "endpoint_difference_rank": 2, + "kernel_left_basis": [ + [ + "1", + "0", + "0" + ] + ], + "kernel_right_basis": [], + "minimum_path_excess": 3, + "rank_P": 2, + "rank_PQ": 2, + "rank_Q": 2, + "rank_QP": 1, + "signed_rank_increment": -1 + } + }, + "common_form_nonorthogonal_lines": { + "P": [ + [ + "1", + "0" + ], + [ + "0", + "0" + ] + ], + "Q": [ + [ + "1/2", + "1/2" + ], + [ + "1/2", + "1/2" + ] + ], + "direct_edge": { + "charge": 2, + "excess": 2, + "signed_rank_increment": 0 + }, + "independent_ranks": [ + 1, + 1, + 1, + 1, + 2 + ], + "profile": { + "d": 2, + "endpoint_difference_rank": 2, + "kernel_left_basis": [], + "kernel_right_basis": [], + "minimum_path_excess": 2, + "rank_P": 1, + "rank_PQ": 1, + "rank_Q": 1, + "rank_QP": 1, + "signed_rank_increment": 0 + } + }, + "common_form_partial_block_overlap": { + "P": [ + [ + "1", + "0", + "0" + ], + [ + "0", + "1", + "0" + ], + [ + "0", + "0", + "0" + ] + ], + "Q": [ + [ + "0", + "0", + "0" + ], + [ + "0", + "1", + "0" + ], + [ + "0", + "0", + "1" + ] + ], + "direct_edge": { + "charge": 1, + "excess": 2, + "signed_rank_increment": -1 + }, + "independent_ranks": [ + 2, + 2, + 1, + 1, + 1 + ], + "profile": { + "d": 3, + "endpoint_difference_rank": 1, + "kernel_left_basis": [ + [ + "1", + "0", + "0" + ] + ], + "kernel_right_basis": [ + [ + "0", + "0", + "1" + ] + ], + "minimum_path_excess": 2, + "rank_P": 2, + "rank_PQ": 1, + "rank_Q": 2, + "rank_QP": 1, + "signed_rank_increment": -1 + } + }, + "equal_product_ranks_without_common_form": { + "P": [ + [ + "1", + "0" + ], + [ + "0", + "0" + ] + ], + "Q": [ + [ + "1", + "1" + ], + [ + "0", + "0" + ] + ], + "direct_edge": { + "charge": 2, + "excess": 2, + "signed_rank_increment": 0 + }, + "independent_ranks": [ + 1, + 1, + 1, + 1, + 2 + ], + "profile": { + "d": 2, + "endpoint_difference_rank": 2, + "kernel_left_basis": [], + "kernel_right_basis": [], + "minimum_path_excess": 2, + "rank_P": 1, + "rank_PQ": 1, + "rank_Q": 1, + "rank_QP": 1, + "signed_rank_increment": 0 + } + }, + "one_sided_rank_one": { + "P": [ + [ + "1", + "0" + ], + [ + "0", + "0" + ] + ], + "Q": [ + [ + "0", + "1" + ], + [ + "0", + "1" + ] + ], + "direct_edge": { + "charge": 1, + "excess": 1, + "signed_rank_increment": 0 + }, + "independent_ranks": [ + 1, + 1, + 1, + 0, + 1 + ], + "profile": { + "d": 2, + "endpoint_difference_rank": 1, + "kernel_left_basis": [ + [ + "1", + "0" + ] + ], + "kernel_right_basis": [], + "minimum_path_excess": 1, + "rank_P": 1, + "rank_PQ": 1, + "rank_Q": 1, + "rank_QP": 0, + "signed_rank_increment": 0 + } + }, + "orthogonal_lines": { + "P": [ + [ + "1", + "0" + ], + [ + "0", + "0" + ] + ], + "Q": [ + [ + "0", + "0" + ], + [ + "0", + "1" + ] + ], + "direct_edge": { + "charge": 0, + "excess": 0, + "signed_rank_increment": 0 + }, + "independent_ranks": [ + 1, + 1, + 0, + 0, + 0 + ], + "profile": { + "d": 2, + "endpoint_difference_rank": 0, + "kernel_left_basis": [ + [ + "1", + "0" + ] + ], + "kernel_right_basis": [ + [ + "0", + "1" + ] + ], + "minimum_path_excess": 0, + "rank_P": 1, + "rank_PQ": 0, + "rank_Q": 1, + "rank_QP": 0, + "signed_rank_increment": 0 + } + }, + "reverse_one_sided_rank_one": { + "P": [ + [ + "0", + "1" + ], + [ + "0", + "1" + ] + ], + "Q": [ + [ + "1", + "0" + ], + [ + "0", + "0" + ] + ], + "direct_edge": { + "charge": 1, + "excess": 1, + "signed_rank_increment": 0 + }, + "independent_ranks": [ + 1, + 1, + 0, + 1, + 1 + ], + "profile": { + "d": 2, + "endpoint_difference_rank": 1, + "kernel_left_basis": [], + "kernel_right_basis": [ + [ + "1", + "0" + ] + ], + "minimum_path_excess": 1, + "rank_P": 1, + "rank_PQ": 0, + "rank_Q": 1, + "rank_QP": 1, + "signed_rank_increment": 0 + } + }, + "same_line": { + "P": [ + [ + "1", + "0" + ], + [ + "0", + "0" + ] + ], + "Q": [ + [ + "1", + "0" + ], + [ + "0", + "0" + ] + ], + "direct_edge": { + "charge": 2, + "excess": 2, + "signed_rank_increment": 0 + }, + "independent_ranks": [ + 1, + 1, + 1, + 1, + 2 + ], + "profile": { + "d": 2, + "endpoint_difference_rank": 2, + "kernel_left_basis": [], + "kernel_right_basis": [], + "minimum_path_excess": 2, + "rank_P": 1, + "rank_PQ": 1, + "rank_Q": 1, + "rank_QP": 1, + "signed_rank_increment": 0 + } + }, + "unequal_rank_complements": { + "P": [ + [ + "1", + "0", + "0" + ], + [ + "0", + "0", + "0" + ], + [ + "0", + "0", + "0" + ] + ], + "Q": [ + [ + "0", + "0", + "0" + ], + [ + "0", + "1", + "0" + ], + [ + "0", + "0", + "1" + ] + ], + "direct_edge": { + "charge": 0, + "excess": 0, + "signed_rank_increment": 0 + }, + "independent_ranks": [ + 1, + 2, + 0, + 0, + 0 + ], + "profile": { + "d": 3, + "endpoint_difference_rank": 0, + "kernel_left_basis": [ + [ + "1", + "0", + "0" + ] + ], + "kernel_right_basis": [ + [ + "0", + "1", + "0" + ], + [ + "0", + "0", + "1" + ] + ], + "minimum_path_excess": 0, + "rank_P": 1, + "rank_PQ": 0, + "rank_Q": 2, + "rank_QP": 0, + "signed_rank_increment": 0 + } + }, + "zero_labels": { + "P": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + "Q": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + "direct_edge": { + "charge": 2, + "excess": 0, + "signed_rank_increment": 2 + }, + "independent_ranks": [ + 0, + 0, + 0, + 0, + 2 + ], + "profile": { + "d": 2, + "endpoint_difference_rank": 2, + "kernel_left_basis": [], + "kernel_right_basis": [], + "minimum_path_excess": 0, + "rank_P": 0, + "rank_PQ": 0, + "rank_Q": 0, + "rank_QP": 0, + "signed_rank_increment": 2 + } + } + } +} diff --git a/research/idempotent-path-rank-audit/README.md b/research/idempotent-path-rank-audit/README.md new file mode 100644 index 0000000000..2cf8b379c4 --- /dev/null +++ b/research/idempotent-path-rank-audit/README.md @@ -0,0 +1,248 @@ +# Exact endpoint penalties for general idempotent labels + +**Adversarial mathematical audit; no new kappa.** The two-unit path penalties +in [the historical cancellation audit](../../docs/research/cancellation-audit.md) +§§3 and 6 hold in their stated scope. For arbitrary rational idempotents +`P,Q`, the sharp endpoint-only penalty is instead + + w(P,Q) = rank(PQ) + rank(QP). + +This note supplies a self-contained proof, exact counterexamples to stronger +extensions, and source-bound checks of the existing compiler. In particular, +one-sided annihilation can give penalty one; a nonorthogonal pair of rank-two +symmetric projections can give penalty two rather than four. These are +counterexamples to *extensions of* the historical claims, not counterexamples +to those claims or to the selected construction. We make no priority claim +for the elementary idempotent rank identity. + +The other audited transfer is the statement in cancellation-audit §3 that a +common `B` component cancels at later stages. Cancellation explains the +matrix difference, but preserving the **signed rank change** also needs rank +additivity. The retained compiler does supply this missing intermediate +justification: its common and variable blocks have complementary supports. +An arbitrary common additive matrix would not suffice. + +## Scope, base and provenance + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. Assignment seed **71**, drawn +with operating-system randomness (`secrets.randbelow(100)`); track: +adversarial mathematical audit. [SELECTION.json](SELECTION.json) records three +candidate tasks, overlap checks, the local claim and the time budget. No +pinned coordination issue existed when checked. This is a new audit of a +historical interface, independent of the author's pending packed-verifier +[PR #752](https://github.com/CrocSwap/integer-mult-bounds/pull/752). + +The selected record was followed through +[its actual construction](../complex-k492-owner-repair/README.md), +[maintainer review](../../docs/research/community-k492-review.md) and +[assembly certificate](../community-k492-audit/pr626/replay/ASSEMBLY.json). +The accepted conditional value at this base is +`51110230636731/31250000000000000 = 0.001635527380375392`. +The review pins #626 at `660de893d27bb7abd1d5b01b1640207528a5c851`, #622 at +`f69477f4f6d3c7eb1f740b166881bffed4ffa9f6`, and retained #543 at +`2065fe4f72a914d907f1046603f5a36f17018535`. None is changed or recertified here. +Historical frontier language in the cancellation note is not the current +accepted result. + +The precise dependencies being compared are: + +- cancellation-audit §§3 and 6: diagonal and common-form rank-one endpoints; +- [rank-product-core §1](../../docs/research/rank-product-core.md): general, + possibly non-self-adjoint rank-one idempotents with **mutual** annihilation; +- [block-core](../../docs/research/block-core.md): uniform higher-rank labels; +- `check_projector_core`, `check_block_projectors`, and the actual time-2 and + time-5 matrices in `scripts/experiments/rank_product_core.py::_compile`. + +[SOURCES.json](SOURCES.json) pins the audited documents, selected-record +context, complete inherited Python import closure and new witness input. +The replay checks these hashes before importing inherited Python code. +There are no third-party Python dependencies or pending-PR code dependencies. + +## 1. Kernel decomposition and exact endpoint rank + +Work over the rationals in dimension `d`. Assume `P²=P`, `Q²=Q`; write +`p=rank(P)`, `q=rank(Q)`. No symmetry, common form, equal rank or commutation +assumption is needed. Then + + ker(I-P-Q) = (im(P) ∩ ker(Q)) ⊕ (im(Q) ∩ ker(P)). + +To prove this, if `(I-P-Q)v=0`, set `a=Pv`, `b=Qv`, so `v=a+b`. +Applying `P` to this equality gives `a=a+Pb`, hence `Pb=0`. Applying `Q` +gives `Qa=0`. Conversely, such `a,b` satisfy `(I-P-Q)(a+b)=0`. +The intersection of the two summands is zero: a vector there is both fixed +and killed by `P`. + +The restriction `Q|im(P)` has image `im(QP)`, and likewise `P|im(Q)` has +image `im(PQ)`. Rank-nullity gives summand dimensions `p-rank(QP)` and +`q-rank(PQ)`. Therefore + + rank(I-P-Q) = d-p-q + rank(PQ)+rank(QP). (1) + +This is the general mathematical proof. The finite checks below corroborate +it and check the implementation; they do not establish its universal scope. + +## 2. The sharp path penalty + +For an arbitrary finite matrix path `M₀=P,...,Mₖ=I-Q`, with no restriction +on its internal rational matrices, define + + charge = Σⱼ rank(Mⱼ-Mⱼ₋₁), + excess = charge - (rank(I-Q)-rank(P)). + +Rank subadditivity bounds the charge below by `rank(I-P-Q)`. Since +`rank(I-Q)=d-q`, (1) implies + + excess ≥ rank(PQ)+rank(QP). (2) + +The single-edge path attains equality, so this is sharp among arbitrary +matrix paths with only these endpoints specified. This does **not** assert +that a scalar circuit admits that single edge, or that different paths can +simultaneously attain their minima. Each individual edge's excess is +nonnegative. Thus for edge-disjoint paths in an already valid frame network, +the corresponding weights may be summed above its telescoping signed rank +sum. Shared edges cannot be charged repeatedly. + +In particular, a cancelled scalar coefficient or a zero trace is not a +substitute for either product rank. No new path packing, role count, complete +network rank sum, decoder or recursive recurrence is supplied here. + +## 3. Which hypotheses give two units? + +For `P=Q`, both products equal `P`, giving exactly `2p`; no common form is +needed for the original private diagonal argument. + +If an **invertible** symmetric matrix `H` satisfies +`HP=PᵀH` and `HQ=QᵀH`, then + + H(PQ) = (QP)ᵀ H, + +so the two product ranks agree. Common-form rank-one labels have weight zero +when mutually annihilating and weight two otherwise. This recovers the +original nonorthogonal triple-line argument. For rank `ell`, the weight is +`2 rank(PQ)` and need not be `2ell`. Equality of the product ranks alone +does not imply existence of a common nondegenerate symmetric form. + +[WITNESSES.json](WITNESSES.json) specifies ten exact pairs. Representative +cases, also checked by a separate determinant implementation, are: + +| P | Q | rank(PQ), rank(QP) | Exact minimum excess | +|---|---|---|---:| +| diag(1,0) | diag(0,1) | 0,0 | 0 | +| diag(1,0) | `[[0,1],[0,1]]` | 1,0 | 1 | +| diag(1,0) | `[[1/2,1/2],[1/2,1/2]]` | 1,1 | 2 | +| diag(1,1,0) | diag(0,1,1) | 1,1 | 2 | +| diag(1,0,1) | `[[0,1,0],[0,1,0],[0,0,1]]` | 2,1 | 3 | + +The one-sided example has nonzero nilpotent `PQ` of trace zero. Swapping its +labels refutes the analogous one-direction bound using `QP`. The last two +rows distinguish partial block overlap from asymmetric block overlap. +For `P=diag(1,0)`, `Q=[[1,1],[0,0]]`, both product ranks are one, but +`H=[[a,b],[b,c]]` must satisfy `b=0` and `a-b=0`; every such `H` is singular. +That example is already given in rank-product-core, and is credited here as +a regression control, not a newly discovered obstruction. + +Dropping idempotence also fails: `P=Q=I₂/2` gives `rank(I-P-Q)=0`, whereas +the right-hand side of (1) would be two. The checker rejects this input +before applying (1). + +## 4. Tensor factors and common additive blocks + +Tensoring both endpoints with a matrix `A` multiplies the difference rank +and each endpoint rank by `a=rank(A)`. Therefore the sharp endpoint-only +penalty is `a w(P,Q)`. Zero-rank spectators are included. + +For the actual compiler, write `E=prior`, `F=future`, and `B=I-E`. +Products of the earlier/future idempotents are tensor products here, so +`E,F` are idempotent. The endpoints have the form + + S = ((B⊗I) + (E⊗P)) ⊗ F, + T = ((B⊗I) + (E⊗(I-Q))) ⊗ F. + +The decomposition of the prior space into `ker(E) ⊕ im(E)` makes these +operators block diagonal. Their common block contributes +`rank(B) d rank(F)` to both endpoint ranks, and their variable blocks +contribute `rank(E) p rank(F)` and `rank(E)(d-q)rank(F)` respectively. +The difference has rank `rank(E)rank(F)rank(I-P-Q)`. Consequently + + minimum endpoint-only excess = rank(E) rank(F) w(P,Q). (3) + +For the three-factor uniform-rank interface, `rank(E)rank(F)=ell²` at each +stage. It is one in the original rank-one setting. The replay reads actual +compiled time-2 and time-5 endpoints at every stage, including the compiler's +reversed group ordering at stage one (zero-based). It confirms (3) for +rank-one and rank-two asymmetric examples. This is an endpoint audit, not a +replay of full scalar correctness or full compiled edge-rank accounting. + +The complementary-support hypothesis matters. With `P=Q=diag(1,0)` and +an arbitrary shared additive block `B=-P`, the endpoints `B+P=0` and +`B+I-Q=I-2P` have direct charge two and signed rank change two: excess zero. +Their difference agrees with the unshifted pair, but their excess does not. +This is a counterexample to transferring the penalty from cancellation +alone, not to the retained compiler's complementary block formula. + +## 5. Reproduction and bounded coverage + +From the repository root, using Python 3 and its standard library: + +```sh +python3 -I -B research/idempotent-path-rank-audit/verify.py +``` + +Expected output: + +```text +PASS_EXACT_IDEMPOTENT_PATH_RANK_AUDIT: 10 named witnesses; 1936 exhaustive pairs; 30 generated pairs; 400 original triple pairs; 24 compiled endpoint pairs +``` + +The command recomputes and compares every field of +[CERTIFICATE.json](CERTIFICATE.json). `--out /new/path.json` writes a fresh +certificate and refuses to overwrite an existing file. Rational entries use +exact fractions; there is no floating-point rank tolerance or probabilistic +rank test. The certificate retains explicit kernel bases for the named +witnesses. It also records: + +- **Independent exhaustive domain:** all `7⁴=2401` integer 2×2 matrices with + entries in `[-3,3]`, radius `71 % 4 = 3`; all 44 idempotents and all 1936 + ordered pairs. `independent.py` uses explicit 2×2 determinants and no + elimination or repository rank routine. Product-rank counts are + `(0,0):129`, `(0,1):152`, `(1,0):152`, `(1,1):1502`, `(2,2):1`. +- **Generated controls:** exactly six pairs in each dimension 2 through 6, + seed 71, constructed by rational similarity transforms; two unrestricted + internal matrices per pair. The generator and transcript hash are retained. + This is fixed finite coverage, not a search or impossibility theorem. +- **Original projection control:** all 400 ordered pairs of the 20 triples + at `h=6`, checking the common form and zero/two penalty by intersection size. +- **Original input guards:** both directed side-edge orientations reject + one-sided annihilation, for rank one and rank two. The same labels pass + without side edges; mutually annihilating pairs pass with side edges. +- **Actual compiler endpoints:** 12 invocation/stage pairs each for rank-one + and rank-two labels; both endpoint matrices and rank additivity are checked. + +The independent determinant census and focused unit checks also run alone: + +```sh +python3 -I -B research/idempotent-path-rank-audit/independent.py +python3 -I -B research/idempotent-path-rank-audit/test_audit.py +``` + +[VALIDATION.md](VALIDATION.md) records the final commands, negative controls, +source portability check, upstream status and overlap refresh. No original +generator, certificate, selected record or upstream file is changed. The +full multiplication theorem and inherited asymptotic assumptions remain +outside this audit; no proof assistant was used. + +## Attribution and license + +Prepared by **Curtis Dransfield with substantial OpenAI Codex assistance**, +including a separate Codex worker's determinant implementation and review. +That computational independence is methodological, not independent human +review. New code and text are under the repository's Apache-2.0 license. +The historical cancellation argument and general projector/block interfaces +are Douglas R. Colkitt's retained work with their existing AI disclosures. +Their source commit history includes +`6e564879f51ae16f23d392e9e196c605f36d90df` (cancellation note) and +`d55bcd62ceb8f322bcf311a5a66e94c3ac7724f0` (retained interfaces). +The new contribution is the scoped hypothesis audit, directional penalty +rule, complementary-block justification, and independently replayable +boundary examples. It does not depend on or supersede concurrent supplier +constructions. diff --git a/research/idempotent-path-rank-audit/SELECTION.json b/research/idempotent-path-rank-audit/SELECTION.json new file mode 100644 index 0000000000..68b226d96b --- /dev/null +++ b/research/idempotent-path-rank-audit/SELECTION.json @@ -0,0 +1,42 @@ +{ + "track": "adversarial mathematical audit", + "assignment_seed": 71, + "seed_source": "OS randomness via secrets.randbelow(100)", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "started_utc": "2026-10-13T05:18:01Z", + "claimed_utc": "2026-10-13T05:21:09.464853+00:00", + "expected_finish_utc": "2026-10-13T05:58:01Z", + "verification_reserve_starts_utc": "2026-10-13T05:48:01Z", + "coordination": "Pinned GitHub issues query returned no nodes; claim recorded locally", + "candidates": [ + { + "object": "cyclic scan rounding/inverse envelope", + "decision": "declined: active overlapping PR764 and precursor audits" + }, + { + "object": "packed carry exceptional restoration costs", + "decision": "declined: active overlapping PR763 and related carry audits" + }, + { + "object": "nonorthogonal endpoint path-excess lemma under general idempotent labels", + "decision": "selected: seed 71 modulo 3 = 2; no matching audit in 583 open PR bodies or scoped source search" + } + ], + "object": "docs/research/cancellation-audit.md sections 3 and 6, read against rank-product-core.md section 1 and block-core.md general idempotent contracts", + "hypothesis": "The two-unit common-form rank-one path bound is valid in its stated scope; arbitrary idempotents require the exact directional penalty rank(PQ)+rank(QP), and one-sided annihilation cannot be substituted for mutual annihilation.", + "method": "Exact kernel decomposition, rational matrix witnesses/counterexamples to overgeneralization, source-bound original contract rejection controls, independent finite minor checks. No construction search or exponent claim.", + "deliverable": "Scoped mathematical audit with proof, exact reproducible witness certificate, meaningful controls and one focused PR", + "overlap": { + "open_pr_count": 583, + "max_pr_number": 764, + "related_prs": [ + 717, + 455, + 21, + 13, + 14 + ], + "notes": "PR717 non-projection label questions and earlier source-frame translations differ; no changes to their contracts. Own PR752 concerns a separate verification kernel." + }, + "record_type": "selection-time claim snapshot; completed result retained in validation and external live claim" +} diff --git a/research/idempotent-path-rank-audit/SOURCES.json b/research/idempotent-path-rank-audit/SOURCES.json new file mode 100644 index 0000000000..da234896c0 --- /dev/null +++ b/research/idempotent-path-rank-audit/SOURCES.json @@ -0,0 +1,29 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "scope": "Inherited Python import closure and audited documentation; WITNESSES.json is new package input, not inherited base content", + "sha256": { + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "docs/research/block-core.md": "1e060c64c376e3f8cdf48c207b309d8e03fae871a836e60673c422b2e39f0531", + "docs/research/cancellation-audit.md": "408f5fb2e191b9b0bd12ba4ddad2adfc13933de6e7bbbbeef27a28fed23d7cf8", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "docs/research/current-status.md": "197319a6edf04340ec3623d09d03714fcd6a981359f22bdcefdd06e7e2f4174d", + "docs/research/inplace-side.md": "c228f131d95f3ea348455c13378c19ed6e3c75af7e14cf68ea0ada445ab3ac72", + "docs/research/rank-product-core.md": "1028abd145b367f94960264a874b847cdbeb3b4d84dd6d3a890fe4203922bd41", + "research/idempotent-path-rank-audit/WITNESSES.json": "8b990c781e5f5091fb4fea77dddd5b6a209dd67c1772169902af3a3ca781f1c1", + "scripts/audit_cancellation.py": "508934ee4d9514a5519813603b6192a0d53103b6e30d65b8d53a1a774de244b6", + "scripts/audit_fused_block.py": "2afb83ca8e5f193ca8a4c242becf267ad1d9dc2578ba238b820e98d5185f6288", + "scripts/audit_joint_frames.py": "3df8061392ce0ba42bbde8c02f2a30c8141145e70e9a48c18da73d3aafb14423", + "scripts/certify.py": "2348d95008276c5d5764f7e028c3918e484582cd589bd4d9b82919161745e53e", + "scripts/exclusion_circuit.py": "b253f9d7318becda1c1f3b24e2287ed44a9c27fcea00cf9d531afb950d0457a0", + "scripts/experiments/block_core.py": "af94018e8f4b80219a8e9e104eae21e34b66fc670217d03ef54862b59c051fc9", + "scripts/experiments/rank_product_core.py": "7a91c1188c5d42e864a5d2e42397b09c435b526ae4f4210c44bf615de488708e", + "scripts/experiments/shared_core.py": "d3c59b61229956cb54ae1ef9145ed213abdf1ae743929de145a77c43656f01a8", + "scripts/paired_exclusion_circuit.py": "8f05f04cf06217befd6d0ee0f2d7d0c5c5eb32cfab8c9a8ca7917fd6d620b7d2", + "scripts/paired_network.py": "991223dc3c1374284c361ed017e42bf732dd971fa0bea2be2282cfb18257b3f7", + "scripts/prepare_layers.py": "a6e2adc612f264b1c0e51d18ce6315de9ae5e2ae2420aa22e99a22d8bf304947", + "scripts/rational_tensor.py": "629b3f00a1aaab32fe908a73ca8f8412918209a300e6b1e5afe6325b9cfed3c3", + "scripts/search_network.py": "3a4faa5037d9b8e7ca5828afac193a96b6966a8b114f14937921795b24ec4f6a", + "scripts/shared_point_circuit.py": "c9bb7a5df92d260a4e3ad532b53e26936730d7c93f7facfb0784957c1e81c8ba", + "scripts/shared_point_network.py": "a85e7f0d8c42d6a27e3846308571ca324a1824ac5c2d59e4daa5c7673c33c697" + } +} diff --git a/research/idempotent-path-rank-audit/VALIDATION.md b/research/idempotent-path-rank-audit/VALIDATION.md new file mode 100644 index 0000000000..d52184f5f7 --- /dev/null +++ b/research/idempotent-path-rank-audit/VALIDATION.md @@ -0,0 +1,96 @@ +# Validation and handoff + +Validated on 2026-10-13 with CPython 3.14.2, macOS 26.3 arm64, using only the +standard library. Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +The audit began at 05:18 UTC; selection/claim completed at 05:21 UTC. +Implementation and proof were complete by 05:33 UTC, when work moved to +verification and handoff, earlier than the reserved final quarter of the +40-minute budget. No larger search was launched. + +## Commands and observed results + +Run from the repository root: + +```sh +python3 -I -B research/idempotent-path-rank-audit/verify.py +python3 -I -O -B research/idempotent-path-rank-audit/verify.py +python3 -I -B research/idempotent-path-rank-audit/test_audit.py +python3 -I -O -B research/idempotent-path-rank-audit/test_audit.py +python3 -I -B -m unittest discover -s tests -p test_cancellation.py -v +python3 -I -B -m unittest discover -s tests -p test_block_core.py -v +make selected-record-check +``` + +Both full package replays exactly matched the committed certificate. Both +unit-test modes passed all **12 tests**, including 113 rational/rectangular +rank comparisons against permutation determinants. The existing cancellation +suite passed **10 tests** and existing block-core suite passed **5 tests**. +The selected-record check passed with the unchanged exact conditional kappa +`51110230636731/31250000000000000`. + +The main replay checks 10 named witnesses, the independent 1936-pair census, +30 generated pairs, all 400 original h=6 triple pairs, four original guard +rejections and 24 actual compiler endpoint pairs. The endpoint examples +expand two 144-gate control networks solely to obtain their actual matrices; +this package does not claim a full circuit certificate for those examples. + +The proof and implementation were also reviewed by a separate Codex worker. +That worker independently reran the main replay successfully in about 1.60s +and found no material proof or scope error. This is AI-assisted review, not +independent human review or proof-assistant verification. + +## Isolated replay and meaningful failures + +A temporary checkout containing **only** the 23 pinned inputs plus this new +package passed from an unrelated working directory, with spaces in its path +and a hostile `PYTHONPATH/sitecustomize.py`, using `python3 -I -B`. +The observed replay time was approximately 1.73s; this is descriptive, not a +performance claim or acceptance threshold. A fresh `--out` certificate +matched every committed field. These subprocess controls also passed: + +- Existing `--out` target: rejected with `FileExistsError`; its bytes unchanged. +- Appending a comment to the copied `rank_product_core.py`: rejected with + `Source pin mismatch` before inherited imports. +- Replacing the copied certificate's one-sided excess `1` with `2`: rejected + with `Recomputed certificate differs from committed evidence`. + +The unit tests reproduce mutated/missing source-pin rejection, non-idempotent +input rejection, wrong dimensions and inexact-input rejection under normal +and optimized Python. The mathematical controls separately refute one-sided +`2 rank(PQ)`/`2 rank(QP)` bounds, a blanket `2ell` block bound, the converse +common-form claim, removal of idempotence, a trace proxy, and unrestricted +common-offset transfer. These are explicit counterexamples to those stronger +statements. No failed search is being described as an impossibility proof. + +## Final overlap and review scope + +The pre-submission refresh at approximately 05:35 UTC found **607 open PRs** +through **#788**, up from 583 through #764 at selection. Main remained the +exact base above; the pinned-issues query again returned no nodes. The +snapshot was searched across titles and full bodies for the claimed +idempotent/path-excess/common-form/mutual-annihilation scope. All new/changed +titles were reviewed. In particular: + +| PR | Inspected head | Relation | +|---|---|---| +| #717 | `67e9e846d9e8814b2dd01133251bb83fafa8f5b6` | Non-projection sink-interface questions, distinct from this endpoint identity. | +| #778 | `f015b04c74801fa330f818d178e809c760fb5469` | Historical Gram replay performance, distinct from this rank-path proof. | +| #785 | `83e78085ae9c110a34bff87e71387292d85e47c0` | Fixed-support nonlinear message floor, a different model. | + +Earlier source-frame translations (#13, #14, #21) and orthogonal-idempotent +composition (#455) were also checked for overlap; none is imported. No +matching concurrent endpoint audit was identified. This is a bounded review +of public metadata and retained sources, not a guarantee that no similar +work exists elsewhere. + +Only `research/idempotent-path-rank-audit/` is added. Original source files, +`upstream/`, selected frontier and unrelated artifacts remain unchanged. +The selected-supplier cold replay and expensive repository-wide `make verify` +were not repeated because no supplier, generator or original checker changed. +Relevant original tests and selected-record integrity were run as above. +No CI pass or full multiplication-theorem audit is claimed. All construction, +recursive, precision and asymptotic assumptions remain inherited. + +Contributor: Curtis Dransfield; substantial OpenAI Codex assistance in proof, +implementation, independent determinant replay, review and writing. +Apache-2.0; predecessor attribution is in README.md and the pinned sources. diff --git a/research/idempotent-path-rank-audit/WITNESSES.json b/research/idempotent-path-rank-audit/WITNESSES.json new file mode 100644 index 0000000000..c7020d44e9 --- /dev/null +++ b/research/idempotent-path-rank-audit/WITNESSES.json @@ -0,0 +1,42 @@ +{ + "orthogonal_lines": { + "P": [[1,0],[0,0]], "Q": [[0,0],[0,1]], + "expected_ranks": [1,1,0,0,0], "expected_excess": 0 + }, + "same_line": { + "P": [[1,0],[0,0]], "Q": [[1,0],[0,0]], + "expected_ranks": [1,1,1,1,2], "expected_excess": 2 + }, + "common_form_nonorthogonal_lines": { + "P": [[1,0],[0,0]], "Q": [["1/2","1/2"],["1/2","1/2"]], + "expected_ranks": [1,1,1,1,2], "expected_excess": 2 + }, + "one_sided_rank_one": { + "P": [[1,0],[0,0]], "Q": [[0,1],[0,1]], + "expected_ranks": [1,1,1,0,1], "expected_excess": 1 + }, + "reverse_one_sided_rank_one": { + "P": [[0,1],[0,1]], "Q": [[1,0],[0,0]], + "expected_ranks": [1,1,0,1,1], "expected_excess": 1 + }, + "common_form_partial_block_overlap": { + "P": [[1,0,0],[0,1,0],[0,0,0]], "Q": [[0,0,0],[0,1,0],[0,0,1]], + "expected_ranks": [2,2,1,1,1], "expected_excess": 2 + }, + "asymmetric_rank_two": { + "P": [[1,0,0],[0,0,0],[0,0,1]], "Q": [[0,1,0],[0,1,0],[0,0,1]], + "expected_ranks": [2,2,2,1,2], "expected_excess": 3 + }, + "unequal_rank_complements": { + "P": [[1,0,0],[0,0,0],[0,0,0]], "Q": [[0,0,0],[0,1,0],[0,0,1]], + "expected_ranks": [1,2,0,0,0], "expected_excess": 0 + }, + "zero_labels": { + "P": [[0,0],[0,0]], "Q": [[0,0],[0,0]], + "expected_ranks": [0,0,0,0,2], "expected_excess": 0 + }, + "equal_product_ranks_without_common_form": { + "P": [[1,0],[0,0]], "Q": [[1,1],[0,0]], + "expected_ranks": [1,1,1,1,2], "expected_excess": 2 + } +} diff --git a/research/idempotent-path-rank-audit/independent.py b/research/idempotent-path-rank-audit/independent.py new file mode 100644 index 0000000000..6be3f81aa2 --- /dev/null +++ b/research/idempotent-path-rank-audit/independent.py @@ -0,0 +1,208 @@ +#!/usr/bin/env python3 +"""Small exact path-rank controls independent of all elimination routines. + +Copyright 2026 Curtis Dransfield. Apache-2.0. +Prepared with substantial OpenAI Codex assistance. The audited historical +contracts retain Douglas Colkitt's authorship and Codex assistance disclosure. + +This module imports neither the package's linear algebra nor repository rank +code. The bounded enumeration uses the explicit 2-by-2 determinant; exported +rank_by_minors uses permutation determinants and applies only to dimensions +at most three. Finite replay is not a proof of the unrestricted identity. +""" +from collections import Counter +from fractions import Fraction +from itertools import combinations, permutations, product +import json + + +def _require(condition, message): + if not condition: + raise ValueError(message) + + +def _rational(value): + _require(type(value) in (int, str, Fraction), 'Use exact rational entries') + return Fraction(value) + + +def _determinant(matrix): + """Leibniz formula; no row reduction or division by pivots.""" + size = len(matrix) + total = Fraction(0) + for permutation in permutations(range(size)): + inversions = sum(permutation[i] > permutation[j] + for i in range(size) for j in range(i + 1, size)) + term = Fraction(-1 if inversions % 2 else 1) + for i, j in enumerate(permutation): + term *= matrix[i][j] + total += term + return total + + +def rank_by_minors(matrix): + """Exact rank of a rectangular rational matrix with both dimensions <= 3. + + Enumerate square minors in descending size and return the first size + having a nonzero permutation determinant. An empty matrix has rank zero. + """ + rows = tuple(tuple(_rational(x) for x in row) for row in matrix) + height = len(rows) + width = len(rows[0]) if height else 0 + _require(height <= 3 and width <= 3, 'Independent minors budget is at most 3 by 3') + _require(all(len(row) == width for row in rows), 'Ragged matrix') + for size in range(min(height, width), 0, -1): + for selected_rows in combinations(range(height), size): + for selected_columns in combinations(range(width), size): + minor = tuple(tuple(rows[i][j] for j in selected_columns) + for i in selected_rows) + if _determinant(minor): + return size + return 0 + + +IDENTITY = (1, 0, 0, 1) +ZERO = (0, 0, 0, 0) + + +def _multiply(left, right): + a, b, c, d = left + e, f, g, h = right + return a*e + b*g, a*f + b*h, c*e + d*g, c*f + d*h + + +def _rank_two(matrix): + a, b, c, d = matrix + return 2 if a*d - b*c else int(any(matrix)) + + +def _subtract(left, right): + return tuple(a - b for a, b in zip(left, right)) + + +def _transpose(matrix): + a, b, c, d = matrix + return a, c, b, d + + +def _nested(matrix): + def encode(x): + q = Fraction(x) + return q.numerator if q.denominator == 1 else str(q) + return [[encode(matrix[0]), encode(matrix[1])], + [encode(matrix[2]), encode(matrix[3])]] + + +def _profile(p, q): + pq, qp = _multiply(p, q), _multiply(q, p) + difference = _subtract(_subtract(IDENTITY, p), q) + ranks = dict(p=_rank_two(p), q=_rank_two(q), pq=_rank_two(pq), + qp=_rank_two(qp), difference=_rank_two(difference)) + signed = _rank_two(_subtract(IDENTITY, q)) - ranks['p'] + return dict(P=_nested(p), Q=_nested(q), ranks=ranks, + signed_rank_change=signed, + direct_edge_excess=ranks['difference'] - signed) + + +def independent_check(): + assignment_seed = 71 + radius = assignment_seed % 4 + entries = range(-radius, radius + 1) + labels = [p for p in product(entries, repeat=4) if _multiply(p, p) == p] + histogram = Counter() + checked_pairs = 0 + for p, q in product(labels, repeat=2): + pq, qp = _multiply(p, q), _multiply(q, p) + difference = _subtract(_subtract(IDENTITY, p), q) + product_ranks = _rank_two(pq), _rank_two(qp) + expected = 2 - _rank_two(p) - _rank_two(q) + sum(product_ranks) + _require(_rank_two(difference) == expected, 'Idempotent rank identity failed') + histogram[product_ranks] += 1 + checked_pairs += 1 + _require(len(labels) == 44 and checked_pairs == 1936, + 'Unexpected exhaustive-domain coverage') + + p = (1, 0, 0, 0) + q = (0, 1, 0, 1) + forward, backward = _profile(p, q), _profile(q, p) + _require(forward['direct_edge_excess'] == backward['direct_edge_excess'] == 1, + 'One-sided-product counterexample changed') + _require(forward['direct_edge_excess'] < 2*forward['ranks']['pq'], + 'Two-rank-PQ false lower bound was not refuted') + _require(backward['direct_edge_excess'] < 2*backward['ranks']['qp'], + 'Two-rank-QP false lower bound was not refuted') + + half_identity = (Fraction(1, 2), 0, 0, Fraction(1, 2)) + non_idempotent = _profile(half_identity, half_identity) + _require(_multiply(half_identity, half_identity) != half_identity, + 'Non-idempotent control became idempotent') + false_rhs = (2 - non_idempotent['ranks']['p'] - non_idempotent['ranks']['q'] + + non_idempotent['ranks']['pq'] + non_idempotent['ranks']['qp']) + _require(non_idempotent['ranks']['difference'] == 0 and false_rhs == 2, + 'Dropping idempotence was not refuted') + non_idempotent['invalid_identity_rhs'] = false_rhs + + # Equal product ranks are necessary, not sufficient, for a common + # nondegenerate symmetric form. Derive the homogeneous equations in + # H = [[a,b],[b,c]] for the repository's existing rank-one example. + nonsymmetric_q = (1, 1, 0, 0) + h_basis = ((1, 0, 0, 0), (0, 1, 1, 0), (0, 0, 0, 1)) + equations = set() + for projector in (p, nonsymmetric_q): + coefficients = [_subtract(_multiply(h, projector), + _multiply(_transpose(projector), h)) for h in h_basis] + for entry in range(4): + row = tuple(coefficient[entry] for coefficient in coefficients) + if any(row): + first = next(x for x in row if x) + equations.add(tuple(Fraction(x, first) for x in row)) + _require(equations == {(Fraction(1), Fraction(-1), Fraction(0)), + (Fraction(0), Fraction(1), Fraction(0))}, + 'Common-form converse control changed') + converse = _profile(p, nonsymmetric_q) + _require(converse['ranks']['pq'] == converse['ranks']['qp'] == 1, + 'Converse control lost equal product ranks') + converse.update(symmetric_form_equations=['H_00 - H_01 = 0', 'H_01 = 0'], + common_nondegenerate_symmetric_form_exists=False) + + # A common additive matrix cancels from a difference but need not + # preserve endpoint-rank additivity. B=-P, Q=P gives endpoints 0,I-2P. + shared_b = tuple(-x for x in p) + source = tuple(x + y for x, y in zip(shared_b, p)) + target = tuple(b + identity - x for b, identity, x in zip(shared_b, IDENTITY, p)) + charge = _rank_two(_subtract(target, source)) + signed = _rank_two(target) - _rank_two(source) + _require(source == ZERO and charge - signed == 0, + 'Unrestricted additive-block control changed') + + # Cross-check both determinant implementations on the named matrices. + named_matrices = (p, q, _multiply(p, q), _multiply(q, p), nonsymmetric_q, + half_identity, source, target) + for matrix in named_matrices: + _require(rank_by_minors(_nested(matrix)) == _rank_two(matrix), + 'Permutation-minor and explicit determinant ranks differ') + + return dict( + status='PASS_EXACT_BOUNDED_IDEMPOTENT_PATH_RANK_AUDIT', + assignment_seed=assignment_seed, + domain=dict(dimension=2, entries_min=-radius, entries_max=radius, + radius_rule='assignment_seed % 4', matrices_examined=(2*radius + 1)**4, + idempotents=len(labels), ordered_pairs=checked_pairs, + stopping_rule='Exhaust every matrix and every ordered idempotent pair'), + method='Explicit 2 by 2 determinant; no elimination or imported rank routine', + product_rank_histogram={f'{a},{b}': count for (a, b), count in sorted(histogram.items())}, + controls=dict( + false_excess_at_least_two_rank_pq=forward, + false_excess_at_least_two_rank_qp=backward, + false_identity_without_idempotence=non_idempotent, + false_converse_equal_product_ranks_implies_common_form=converse, + false_unrestricted_shared_additive_block=dict( + P=_nested(p), Q=_nested(p), B=_nested(shared_b), source=_nested(source), + target=_nested(target), direct_charge=charge, signed_rank_change=signed, + actual_excess=charge - signed, incorrectly_transferred_bound=2)), + scope='Finite independent evidence and explicit counterexamples to stronger statements; ' + 'the unrestricted idempotent identity requires the written proof; no new kappa') + + +if __name__ == '__main__': + print(json.dumps(independent_check(), indent=2, sort_keys=True)) diff --git a/research/idempotent-path-rank-audit/linalg.py b/research/idempotent-path-rank-audit/linalg.py new file mode 100644 index 0000000000..8308e0edba --- /dev/null +++ b/research/idempotent-path-rank-audit/linalg.py @@ -0,0 +1,145 @@ +"""Small exact rational algebra for the path-rank audit (Apache-2.0). + +Copyright 2026 Curtis Dransfield. Substantial OpenAI Codex assistance. +No floating-point or modular rank heuristics are used. +""" +from fractions import Fraction as F + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def matrix(rows): + rows = tuple(tuple(row) for row in rows) + require(rows and rows[0] and all(len(row) == len(rows[0]) for row in rows), + 'Nonempty rectangular matrix required') + require(all(type(x) in (int, str, F) for row in rows for x in row), + 'Use exact integer/rational entries') + return tuple(tuple(F(x) for x in row) for row in rows) + + +def eye(n): + return matrix([[int(i == j) for j in range(n)] for i in range(n)]) + + +def zero(n): + return matrix([[0] * n for _ in range(n)]) + + +def transpose(A): + return tuple(zip(*A)) + + +def add(A, B): + require(len(A) == len(B) and len(A[0]) == len(B[0]), 'Matrix shape mismatch') + return tuple(tuple(a + b for a, b in zip(ar, br)) for ar, br in zip(A, B)) + + +def scale(A, c): + return tuple(tuple(c * x for x in row) for row in A) + + +def sub(A, B): + return add(A, scale(B, -1)) + + +def mul(A, B): + require(len(A[0]) == len(B), 'Product shape mismatch') + return tuple(tuple(sum(a * b for a, b in zip(row, col)) for col in zip(*B)) for row in A) + + +def rref(A): + out = [list(row) for row in A] + pivots = [] + for col in range(len(out[0])): + row = next((i for i in range(len(pivots), len(out)) if out[i][col]), None) + if row is None: + continue + target = len(pivots) + out[target], out[row] = out[row], out[target] + value = out[target][col] + out[target] = [x / value for x in out[target]] + for i in range(len(out)): + if i != target: + value = out[i][col] + out[i] = [x - value*y for x, y in zip(out[i], out[target])] + pivots.append(col) + if len(pivots) == len(out): + break + return tuple(tuple(row) for row in out), tuple(pivots) + + +def rank(A): + return len(rref(A)[1]) + + +def nullspace(A): + reduced, pivots = rref(A) + basis = [] + for free in range(len(A[0])): + if free not in pivots: + v = [F(0)] * len(A[0]) + v[free] = F(1) + for row, pivot in enumerate(pivots): + v[pivot] = -reduced[row][free] + basis.append(tuple(v)) + return tuple(basis) + + +def inverse(A): + n = len(A) + require(len(A[0]) == n, 'Square inverse required') + augmented = tuple(a + b for a, b in zip(A, eye(n))) + reduced, pivots = rref(augmented) + require(pivots == tuple(range(n)), 'Singular inverse') + return tuple(row[n:] for row in reduced) + + +def kron(A, B): + return tuple(tuple(a*b for a in ar for b in br) for ar in A for br in B) + + +def serializable(value): + if isinstance(value, F): + return str(value) + if isinstance(value, dict): + return {k: serializable(v) for k, v in value.items()} + if isinstance(value, (tuple, list)): + return [serializable(v) for v in value] + return value + + +def analyze_pair(P, Q): + P, Q = matrix(P), matrix(Q) + d = len(P) + require(len(P[0]) == d and len(Q) == d and len(Q[0]) == d, 'Equal square dimensions required') + require(mul(P, P) == P and mul(Q, Q) == Q, 'Idempotence required') + I = eye(d) + PQ, QP, R = mul(P, Q), mul(Q, P), sub(sub(I, P), Q) + p, q, pq, qp, r = map(rank, (P, Q, PQ, QP, R)) + left = nullspace(sub(I, P) + Q) # im(P) intersect ker(Q), via stacked equations + right = nullspace(sub(I, Q) + P) + combined = left + right + require(len(left) == p - qp and len(right) == q - pq, 'Intersection dimension mismatch') + require((rank(combined) if combined else 0) == len(combined), 'Kernel summands are not direct') + for v in combined: + require(all(x == 0 for row in mul(R, transpose((v,))) for x in row), 'Kernel witness failed') + require(len(combined) == d - r, 'Kernel witnesses do not span') + signed = rank(sub(I, Q)) - p + require(signed == d - q - p, 'Complement rank mismatch') + require(r == d - p - q + pq + qp, 'Endpoint rank identity failed') + require(r - signed == pq + qp, 'Exact excess identity failed') + return dict(d=d, rank_P=p, rank_Q=q, rank_PQ=pq, rank_QP=qp, + endpoint_difference_rank=r, signed_rank_increment=signed, + minimum_path_excess=pq + qp, + kernel_left_basis=left, kernel_right_basis=right) + + +def path_excess(chain): + require(len(chain) >= 2, 'Path needs two endpoints') + charge = sum(rank(sub(B, A)) for A, B in zip(chain, chain[1:])) + signed = rank(chain[-1]) - rank(chain[0]) + require(charge >= rank(sub(chain[-1], chain[0])), 'Rank triangle inequality failed') + return dict(charge=charge, signed_rank_increment=signed, excess=charge - signed) diff --git a/research/idempotent-path-rank-audit/test_audit.py b/research/idempotent-path-rank-audit/test_audit.py new file mode 100644 index 0000000000..8560b597b2 --- /dev/null +++ b/research/idempotent-path-rank-audit/test_audit.py @@ -0,0 +1,229 @@ +"""Exact controls for the scoped idempotent path-rank audit. + +Copyright 2026 Curtis Dransfield. Apache-2.0. +Prepared with substantial OpenAI Codex assistance; historical source +attribution remains in the package's proof note and retained repository. +""" +from fractions import Fraction as F +from hashlib import sha256 +import json +from pathlib import Path +import random +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) + +import linalg as algebra +from independent import independent_check, rank_by_minors + + +def fixture_data(): + return json.loads((HERE / 'WITNESSES.json').read_text()) + + +def apply_literal(matrix, vector): + return tuple(sum(a*b for a, b in zip(row, vector)) for row in matrix) + + +class ExactLinearAlgebra(unittest.TestCase): + def test_rational_rectangular_ranks_against_permutation_minors(self): + rng = random.Random(71) + examples = [[[0, 1, 0], [0, 0, 1], [1, 0, 0]], + [[1, '1/2', 0], [0, 0, 1], [2, 1, 3]], + [['1/2', 1, '3/2'], [1, 2, 3], [0, 0, 0]], + [[0, 0, 0]] * 3, [[1, 2], [2, 4], [3, 6]]] + for height in range(1, 4): + for width in range(1, 4): + for _ in range(12): + examples.append([[F(rng.randrange(-3, 4), rng.randrange(1, 6)) + for _ in range(width)] for _ in range(height)]) + for example in examples: + matrix = algebra.matrix(example) + with self.subTest(matrix=matrix): + self.assertEqual(algebra.rank(matrix), rank_by_minors(matrix)) + reduced, pivots = algebra.rref(matrix) + self.assertEqual(rank_by_minors(reduced), len(pivots)) + self.assertTrue(all(isinstance(x, F) for row in reduced for x in row)) + + def test_nullspace_spans_exact_kernel_for_rectangular_matrices(self): + examples = ([[0, 0, 0]], [[1, '1/2', 0], [2, 1, 0]], + [[0, 1, 2], [0, 2, 4]], [[1, 2], [2, 4], [3, 6]], + [[0, 1], [1, 0]], [[1, 0, 2], [0, 1, 3]]) + for example in examples: + matrix = algebra.matrix(example) + basis = algebra.nullspace(matrix) + with self.subTest(matrix=matrix): + self.assertEqual(len(basis), len(matrix[0]) - rank_by_minors(matrix)) + self.assertEqual(rank_by_minors(basis), len(basis)) + for vector in basis: + self.assertEqual(apply_literal(matrix, vector), (0,) * len(matrix)) + + def test_rational_inverse_and_singular_rejection(self): + for raw in ([[0, 1], [1, 0]], [[1, '1/2'], ['1/3', 1]], + [[0, 1, 0], [0, 0, 1], [1, 0, 0]]): + matrix = algebra.matrix(raw) + inverse = algebra.inverse(matrix) + self.assertEqual(algebra.mul(matrix, inverse), algebra.eye(len(matrix))) + self.assertEqual(algebra.mul(inverse, matrix), algebra.eye(len(matrix))) + self.assertEqual(rank_by_minors(inverse), len(matrix)) + with self.assertRaisesRegex(ValueError, 'Singular inverse'): + algebra.inverse(algebra.matrix([[1, 2], [2, 4]])) + with self.assertRaisesRegex(ValueError, 'Square inverse'): + algebra.inverse(algebra.matrix([[1, 2, 3]])) + + def test_exact_inputs_shapes_and_idempotence_are_required(self): + for raw in ([], [[]], [[1], [1, 2]], [[1.0]], [[True]]): + with self.subTest(raw=raw), self.assertRaises(ValueError): + algebra.matrix(raw) + invalid_pairs = (([[F(1, 2), 0], [0, F(1, 2)]], algebra.eye(2)), + ([[0, 1], [0, 0]], algebra.eye(2)), + (algebra.eye(2), algebra.eye(3)), + ([[1, 0, 0], [0, 1, 0]], algebra.eye(2))) + for p, q in invalid_pairs: + with self.subTest(p=p, q=q), self.assertRaises(ValueError): + algebra.analyze_pair(p, q) + for raw in ([[1.0]], [[1], [1, 2]], [[1] * 4] * 4): + with self.assertRaises(ValueError): + rank_by_minors(raw) + + def test_source_guard_rejects_mutated_and_missing_bytes(self): + from verify import verify_pins + with tempfile.TemporaryDirectory(prefix='path-rank-pin-control-') as directory: + root = Path(directory) + source = root / 'fixture.py' + content = b'# exact pinned input\n' + source.write_bytes(content) + manifest = dict(base_commit='test-only', sha256={'fixture.py': sha256(content).hexdigest()}) + self.assertEqual(verify_pins(root=root, manifest=manifest)['checked_files'], 1) + source.write_bytes(content + b'# changed\n') + with self.assertRaisesRegex(ValueError, 'Source pin mismatch: fixture.py'): + verify_pins(root=root, manifest=manifest) + source.unlink() + with self.assertRaises(FileNotFoundError): + verify_pins(root=root, manifest=manifest) + + +class IdempotentPathAudit(unittest.TestCase): + def test_all_ten_named_fixture_ranks_use_independent_oracle(self): + fixtures = fixture_data() + self.assertEqual(len(fixtures), 10) + for name, fixture in fixtures.items(): + p, q = algebra.matrix(fixture['P']), algebra.matrix(fixture['Q']) + difference = algebra.sub(algebra.sub(algebra.eye(len(p)), p), q) + matrices = (p, q, algebra.mul(p, q), algebra.mul(q, p), difference) + independent_ranks = [rank_by_minors(matrix) for matrix in matrices] + with self.subTest(name=name): + self.assertEqual(independent_ranks, fixture['expected_ranks']) + result = algebra.analyze_pair(p, q) + keys = ('rank_P', 'rank_Q', 'rank_PQ', 'rank_QP', 'endpoint_difference_rank') + self.assertEqual([result[key] for key in keys], independent_ranks) + self.assertEqual(result['minimum_path_excess'], fixture['expected_excess']) + + def test_named_kernel_witnesses_lie_in_the_two_intersections(self): + for name, fixture in fixture_data().items(): + p, q = algebra.matrix(fixture['P']), algebra.matrix(fixture['Q']) + result = algebra.analyze_pair(p, q) + left, right = result['kernel_left_basis'], result['kernel_right_basis'] + with self.subTest(name=name): + for vector in left: + self.assertEqual(apply_literal(p, vector), vector) + self.assertEqual(apply_literal(q, vector), (0,) * len(p)) + for vector in right: + self.assertEqual(apply_literal(q, vector), vector) + self.assertEqual(apply_literal(p, vector), (0,) * len(p)) + self.assertEqual(rank_by_minors(left + right), len(left) + len(right)) + self.assertEqual(len(left) + len(right), + len(p) - result['endpoint_difference_rank']) + + def test_arbitrary_nonidempotent_internal_frames_preserve_path_bound(self): + middle = algebra.matrix([[F(2, 3), -2], [3, F(7, 5)]]) + self.assertNotEqual(algebra.mul(middle, middle), middle) + for name in ('same_line', 'one_sided_rank_one', 'reverse_one_sided_rank_one'): + fixture = fixture_data()[name] + p, q = algebra.matrix(fixture['P']), algebra.matrix(fixture['Q']) + end = algebra.sub(algebra.eye(2), q) + bound = algebra.analyze_pair(p, q)['minimum_path_excess'] + for chain in ((p, end), (p, middle, end), (p, middle, algebra.zero(2), end)): + actual = algebra.path_excess(chain) + independent_charge = sum(rank_by_minors(algebra.sub(b, a)) + for a, b in zip(chain, chain[1:])) + signed = rank_by_minors(end) - rank_by_minors(p) + self.assertEqual(actual['charge'], independent_charge) + self.assertEqual(actual['excess'], independent_charge - signed) + self.assertGreaterEqual(actual['excess'], bound) + self.assertEqual(algebra.path_excess((p, end))['excess'], bound) + + def test_common_nondegenerate_indefinite_form_equalizes_product_ranks(self): + h = algebra.matrix([[1, 0], [0, -1]]) + p = algebra.matrix([[1, 0], [0, 0]]) + q = algebra.matrix([['4/3', '-2/3'], ['2/3', '-1/3']]) + self.assertEqual(rank_by_minors(h), 2) + for projector in (p, q): + self.assertEqual(algebra.mul(h, projector), + algebra.mul(algebra.transpose(projector), h)) + result = algebra.analyze_pair(p, q) + self.assertEqual(result['rank_PQ'], result['rank_QP']) + self.assertEqual(result['minimum_path_excess'], 2) + # A degenerate H=0 is common and symmetric for the asymmetric pair, + # so merely saying "symmetric form" would not justify equal ranks. + asymmetric = fixture_data()['one_sided_rank_one'] + p, q = algebra.matrix(asymmetric['P']), algebra.matrix(asymmetric['Q']) + degenerate = algebra.zero(2) + for projector in (p, q): + self.assertEqual(algebra.mul(degenerate, projector), + algebra.mul(algebra.transpose(projector), degenerate)) + self.assertNotEqual(rank_by_minors(algebra.mul(p, q)), rank_by_minors(algebra.mul(q, p))) + + def test_tensor_spectator_scales_all_endpoint_terms(self): + fixture = fixture_data()['one_sided_rank_one'] + p, q = algebra.matrix(fixture['P']), algebra.matrix(fixture['Q']) + end = algebra.sub(algebra.eye(2), q) + base = algebra.path_excess((p, end)) + for spectator in (algebra.matrix([[1, 1], [0, 0]]), algebra.eye(2), algebra.zero(2)): + weight = rank_by_minors(spectator) + lifted = algebra.path_excess((algebra.kron(p, spectator), algebra.kron(end, spectator))) + for key in ('charge', 'signed_rank_increment', 'excess'): + self.assertEqual(lifted[key], weight * base[key]) + + def test_common_additive_block_needs_complementary_support(self): + p = algebra.matrix([[1, 0], [0, 0]]) + q = algebra.matrix([[0, 1], [0, 1]]) + # For P=Q, arbitrary B=-P gives zero excess despite product-rank sum2. + bad_offset = algebra.scale(p, -1) + bad_start = algebra.add(bad_offset, p) + bad_end = algebra.add(bad_offset, algebra.sub(algebra.eye(2), p)) + self.assertEqual(algebra.path_excess((bad_start, bad_end))['excess'], 0) + self.assertEqual(algebra.analyze_pair(p, p)['minimum_path_excess'], 2) + # Actual compiler structure: low=(I-prior) tensor I and variable + # prior tensor P mutually annihilate and have additive ranks. + prior = algebra.matrix([[1, 1], [0, 0]]) + low = algebra.kron(algebra.sub(algebra.eye(2), prior), algebra.eye(2)) + start_active = algebra.kron(prior, p) + end_active = algebra.kron(prior, algebra.sub(algebra.eye(2), q)) + for active in (start_active, end_active): + self.assertEqual(algebra.mul(low, active), algebra.zero(4)) + self.assertEqual(algebra.mul(active, low), algebra.zero(4)) + self.assertEqual(algebra.rank(algebra.add(low, active)), + algebra.rank(low) + algebra.rank(active)) + lifted = algebra.path_excess((algebra.add(low, start_active), algebra.add(low, end_active))) + self.assertEqual(lifted['excess'], algebra.analyze_pair(p, q)['minimum_path_excess']) + + def test_bounded_enumeration_and_counterexamples_complete(self): + result = independent_check() + self.assertEqual(result['domain']['matrices_examined'], 7**4) + self.assertEqual(result['domain']['idempotents'], 44) + self.assertEqual(result['domain']['ordered_pairs'], 44**2) + self.assertEqual(sum(result['product_rank_histogram'].values()), 44**2) + controls = result['controls'] + nonidempotent = controls['false_identity_without_idempotence'] + self.assertNotEqual(nonidempotent['ranks']['difference'], nonidempotent['invalid_identity_rhs']) + converse = controls['false_converse_equal_product_ranks_implies_common_form'] + self.assertEqual(converse['ranks']['pq'], converse['ranks']['qp']) + self.assertFalse(converse['common_nondegenerate_symmetric_form_exists']) + + +if __name__ == '__main__': + unittest.main(verbosity=2) diff --git a/research/idempotent-path-rank-audit/verify.py b/research/idempotent-path-rank-audit/verify.py new file mode 100644 index 0000000000..8da14a84bc --- /dev/null +++ b/research/idempotent-path-rank-audit/verify.py @@ -0,0 +1,208 @@ +#!/usr/bin/env python3 +"""Reproduce a scoped idempotent path-rank audit using exact rational arithmetic. + +Copyright 2026 Curtis Dransfield. Apache-2.0; substantial OpenAI Codex assistance. +""" +import argparse +from collections import Counter +import hashlib +from itertools import combinations, product +import json +from pathlib import Path +import random +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from linalg import (F, add, analyze_pair, eye, inverse, kron, matrix, mul, + path_excess, rank, require, scale, serializable, sub, transpose) +from independent import independent_check, rank_by_minors + + +def verify_pins(root=ROOT, manifest=None): + if manifest is None: + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + for relative, expected in manifest['sha256'].items(): + actual = hashlib.sha256((root / relative).read_bytes()).hexdigest() + require(actual == expected, 'Source pin mismatch: ' + relative) + return dict(base_commit=manifest['base_commit'], checked_files=len(manifest['sha256'])) + + +def named_witnesses(): + fixtures = json.loads((HERE / 'WITNESSES.json').read_text()) + output = {} + for name, fixture in fixtures.items(): + P, Q = matrix(fixture['P']), matrix(fixture['Q']) + profile = analyze_pair(P, Q) + mats = P, Q, mul(P, Q), mul(Q, P), sub(sub(eye(len(P)), P), Q) + independent_ranks = [rank_by_minors(M) for M in mats] + require(independent_ranks == fixture['expected_ranks'], name + ': minor ranks changed') + require([rank(M) for M in mats] == independent_ranks, name + ': rank implementations differ') + direct = path_excess((P, sub(eye(len(P)), Q))) + require(direct['excess'] == profile['minimum_path_excess'] == fixture['expected_excess'], + name + ': direct-edge sharpness failed') + output[name] = dict(P=P, Q=Q, profile=profile, independent_ranks=independent_ranks, + direct_edge=direct) + P, Q = (matrix(fixtures['one_sided_rank_one'][k]) for k in ('P', 'Q')) + PQ = mul(P, Q) + require(sum(PQ[i][i] for i in range(len(PQ))) == 0 and rank(PQ) == 1, + 'Trace-zero nonzero product control failed') + return output + + +def random_controls(): + rng = random.Random(71) + cases = [] + for d in range(2, 7): + for trial in range(6): + labels = [] + for _ in range(2): + # Invertibility is constructive: product of determinant-one shears. + S = eye(d) + for _ in range(2*d): + i, j = rng.sample(range(d), 2) + shear = [list(row) for row in eye(d)] + shear[i][j] = F(rng.choice((-2, -1, 1, 2)), rng.choice((1, 2, 3))) + S = mul(matrix(shear), S) + label_rank = rng.randrange(d+1) + D = matrix([[int(i == j and i < label_rank) for j in range(d)] for i in range(d)]) + labels.append(mul(mul(S, D), inverse(S))) + P, Q = labels + profile = analyze_pair(P, Q) + internal = [matrix([[F(rng.randrange(-2, 3), rng.randrange(1, 4)) + for _ in range(d)] for _ in range(d)]) for _ in range(2)] + path = path_excess((P, *internal, sub(eye(d), Q))) + require(path['excess'] >= profile['minimum_path_excess'], 'Arbitrary internal path failed') + cases.append(dict(d=d, trial=trial, P=P, Q=Q, internal=internal, + profile=profile, path=path)) + encoded = json.dumps(serializable(cases), sort_keys=True, separators=(',', ':')).encode() + return dict(seed=71, dimensions=list(range(2, 7)), trials_per_dimension=6, + completed_pairs=len(cases), arbitrary_internal_matrices=2*len(cases), + generator='2d elementary rational shears per label; independent uniform ranks 0..d', + stopping_rule='Exactly 6 pairs in each dimension 2..6; no adaptive search', + transcript_sha256=hashlib.sha256(encoded).hexdigest(), + product_rank_histogram=dict(sorted(Counter( + str((x['profile']['rank_PQ'], x['profile']['rank_QP'])) for x in cases).items()))) + + +def original_contract_controls(): + sys.path.insert(0, str(ROOT / 'scripts')) + from audit_cancellation import line_projection + from experiments.rank_product_core import check_projector_core, compile_projector_core + from experiments.block_core import check_block_projectors, compile_block + + triples = list(combinations(range(6), 3)) + H = sub(eye(6), scale(matrix([[1]*6 for _ in range(6)]), F(1, 9))) + require(rank(H) == 6, 'Original h=6 form is degenerate') + labels = [matrix(line_projection(6, T)) for T in triples] + for P in labels: + require(mul(H, P) == mul(transpose(P), H), 'Original common form failed') + hist = Counter() + for i, P in enumerate(labels): + for j, Q in enumerate(labels): + profile = analyze_pair(P, Q) + overlap = len(set(triples[i]) & set(triples[j])) + expected = 0 if overlap == 1 else 2 + require(profile['minimum_path_excess'] == expected, 'Original triple penalty changed') + hist[str(overlap)] += 1 + + fixture = json.loads((HERE / 'WITNESSES.json').read_text())['one_sided_rank_one'] + P, Q = matrix(fixture['P']), matrix(fixture['Q']) + rejected = [] + for ell, checker, projections in ( + (1, check_projector_core, (P, Q)), + (2, check_block_projectors, (kron(P, eye(2)), kron(Q, eye(2))))): + checker([1, 2], projections) # No side edge: these are legal labels. + for rows in ([3, 2], [1, 3]): + try: + checker(rows, projections) + except ValueError as exc: + require('mutual' in str(exc), 'Unexpected original rejection reason') + rejected.append(dict(ell=ell, rows=rows, reason=str(exc))) + else: + raise ValueError('Original checker accepted one-sided annihilation') + check_projector_core([3, 3], (P, sub(eye(2), P))) + check_block_projectors([3, 3], (kron(P, eye(2)), kron(sub(eye(2), P), eye(2)))) + + # Check actual time-2/time-5 compiler matrices, including reversed stage 1. + # Eight groups have sizes 2,1,2,1,1,2,1,2 for these n=2 controls. + compiled = [] + for name in ('one_sided_rank_one', 'asymmetric_rank_two'): + f = json.loads((HERE / 'WITNESSES.json').read_text())[name] + Ps = [matrix(f[k]) for k in ('P', 'Q')] + d, ell = len(Ps[0]), rank(Ps[0]) + if ell == 1: + candidate, _ = compile_projector_core([1, 2], Ps) + else: + candidate, _ = compile_block(check_block_projectors([1, 2], Ps)) + offset = 0 + checked = [] + for stage in range(3): + for fixed in product(range(2), repeat=2): + a = list(fixed) + a.insert(stage, 0) + prior, future = eye(1), eye(1) + for j in range(stage): + prior = kron(prior, Ps[a[j]]) + for j in range(stage+1, 3): + future = kron(future, Ps[a[j]]) + B = sub(eye(len(prior)), prior) + common = kron(kron(B, eye(d)), future) + endpoints = [] + for t, group_start in ((0, 3), (1, 7)): + position = t if stage != 1 else 1-t + frame = matrix(candidate['gates'][offset + group_start + position]['frame']) + active = Ps[t] if group_start == 3 else sub(eye(d), Ps[t]) + variable = kron(kron(prior, active), future) + require(frame == add(common, variable), 'Compiled endpoint differs from formula') + require(not any(x for row in mul(common, variable) for x in row) + and not any(x for row in mul(variable, common) for x in row), + 'Compiler summands fail mutual annihilation') + require(rank(frame) == rank(common) + rank(variable), 'Compiler rank additivity failed') + endpoints.append(frame) + actual = path_excess(endpoints) + multiplier = rank(prior)*rank(future) + expected = multiplier*(rank(mul(Ps[0], Ps[1])) + rank(mul(Ps[1], Ps[0]))) + require(actual['excess'] == expected, 'Tensor-stage excess failed') + checked.append(dict(stage=stage, fixed=fixed, spectator_rank=multiplier, + exact_excess=actual['excess'])) + offset += 12 + require(offset == len(candidate['gates']), 'Compiler gate coverage changed') + compiled.append(dict(name=name, ambient_dimension=d, label_rank=ell, + compiled_gates=len(candidate['gates']), endpoint_pairs=checked, + scope='Actual endpoint matrices only; no full scalar/rank-sum certification')) + return dict(original_triples=dict(h=6, labels=20, ordered_pairs=400, + intersection_histogram=dict(sorted(hist.items()))), + original_mutual_annihilation_rejections=rejected, + positive_contract_controls=4, compiled_endpoint_controls=compiled) + + +def certificate(): + pins = verify_pins() # Before importing any inherited implementation. + result = dict(status='PASS_EXACT_IDEMPOTENT_PATH_RANK_AUDIT', source_pins=pins, + witnesses=named_witnesses(), independent=independent_check(), + generated_controls=random_controls(), inherited_controls=original_contract_controls(), + scope='Written proof plus finite exact evidence; no new circuit, no new kappa, ' + 'no formal proof of the multiplication theorem') + return serializable(result) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--out', type=Path, help='Write a fresh certificate; refuses to overwrite') + args = parser.parse_args() + result = certificate() + if args.out: + with args.out.open('x') as stream: + json.dump(result, stream, indent=2, sort_keys=True) + stream.write('\n') + else: + require(result == json.loads((HERE / 'CERTIFICATE.json').read_text()), + 'Recomputed certificate differs from committed evidence') + print('PASS_EXACT_IDEMPOTENT_PATH_RANK_AUDIT: 10 named witnesses; 1936 exhaustive pairs; ' + '30 generated pairs; 400 original triple pairs; 24 compiled endpoint pairs') + + +if __name__ == '__main__': + main()