diff --git a/research/two-central-laurent-coverage/PROOF.md b/research/two-central-laurent-coverage/PROOF.md new file mode 100644 index 0000000000..fb283fcd31 --- /dev/null +++ b/research/two-central-laurent-coverage/PROOF.md @@ -0,0 +1,172 @@ +# Two-central substitution on the selected p16 controller: written argument + +JoyboyBrian, with substantial assistance from Anthropic Claude. Apache-2.0. + +## 0. Object and premises + +The object is the selected complete invoice of #4470 +(`research/joint-helper-lattice/RESULT.json`, sha256 `c7b2388f…5236c`, which is the +selected record's `source_certificate_sha256`). Write `T` for its productive (target) rank +histogram and `P` for its paid histogram. For `t = 1 - C` put `T_t = Σ T_k k^t`, +`P_t = Σ P_r r^t` and `S(C) = T_t - P_t`. The selected fixed-invoice root lies in +`(0.0030201659770, 0.0030201659771)`. + +Inherited, not re-proved: the native all-column semantics, the PR4440 Laurent controller +factorization, the whole-job matcher, completion/splitting, compiler and outer transfer +of the selected review. Nothing here changes the selected record. + +## 1. Where the single unpaid coordinate comes from + +`verify.py` checks on the pinned bytes: + +- The main targets are 224 of rank 145 = 1 + 8·18, 448 of each rank 1 + 8k for + k = 2,…,8, and 224 of rank 73 = 1 + 8·9. That is 2·V·p = 3,584 main targets, with + V = 112 ports and p = 16 pairs. +- Every arm target 1 + 8k has a paid whole-idle of rank exactly 8k with the same + multiplicity. The long targets are covered by the 18 native calls. +- The rank-one surplus is `752 = 18·(H_1 - P_1 + V + 2VB) - V`, with H_1 = 3,471, + P_1 = 5,327 and B = 8. + +The extra coordinate in each main target is the central Gaussian line `Q = C_q`, with +`q ∈ F2^9` the port's odd vector (`kappa-hybrid-controller/NATIVE.md` §2). The Laurent +controller has diagonal targets `D·Q^{±1}` (central exponent ±1, PR4470 PROOF §4). The +paid idles carry only the D blocks. In this interface the old #1094 coverage identity +`mass = 72W + 64N` and `ceiling.ceiling(unpaid=…)` do not apply. The replacement +identity is the one above: one central credit per main target. + +## 2. The changed contract: substitution Q → Q_a Q_b + +Let `q_b` be a fresh spectator axis of every main field and `Q_b = C_{q_b}`. The PR4440 +factorization is an identity in the commutative Laurent ring generated by `Q, D_0, …`. +The map `Q ↦ Q_a Q_b` (with `Q_a = C_q`) is a ring homomorphism into a commutative +algebra, because operators on disjoint axes commute. So the substituted word is again an +exact controller, and every main target becomes `D·Q_a^{±1} Q_b^{±1}`. These are **two +unpaid coordinates per main family**, the card's object. + +`C_{q_a} C_{q_b}` is a rank-2 Gaussian request (kernel support spans {q_a, q_b}). Its +inverse is `X_{q_a} X_{q_b} C_{q_a} C_{q_b}`, because `C_q^{-1} = X_q C_q`. + +The fully charged realizations considered are: + +1. **Thin shears.** The 15 query shears per port become rank-2 requests (+1 rank each). +2. **Native contacts by conjugation.** With `Δ = diag(1, Q_b)` on the stage's (X, Y) + pair, + `D_s S_y(Q_a^{-1} Q_b^{-1}) = Δ^{-1} (D_s S_y(Q_a^{-1})) Δ` and + `S_x(-Q_a Q_b) = Δ^{-1} S_x(-Q_a) Δ`. + So each unchanged native call plus two rank-one `q_b` requests per port realizes the + substituted native stage. +3. **Optimistic relaxation.** Item 1 with native calls unchanged and free. This is a + screen, not a realization. + +## 3. Credit-rank lemma + +Work over the field `K = F(x)[Q_b]/(Q_b^2 - x)`. Here F is the rational function field +in all other symbols, and x stands for the translation `X_{q_b}`. Let `σ` be the +Galois automorphism `Q_b ↦ -Q_b`. It fixes x, so it fixes `X_{q_b} = Q_b^2` and every +`Q_b`-free operator. + +**Lemma.** Let `W = F_1 ⋯ F_m` be a program of square matrices over K. Every column is +a physical field, including helpers and copies. Suppose its productive block, between +`σ`-fixed boundary programs, is monomial with entries `u_i Q_b^{e_i}`, where each `u_i` is +`σ`-fixed. Then + + #{i : e_i odd} ≤ Σ_j rank(σ(F_j) - F_j). + +*Proof.* `σ(W) - W = Σ_j σ(F_1)⋯σ(F_{j-1}) (σ(F_j) - F_j) F_{j+1}⋯F_m`, so its rank is at +most the right side. A submatrix and a product with fixed invertible boundary matrices do +not increase rank. For the monomial target, `σ(T) - T = Π·diag(((-1)^{e_i} - 1) u_i Q_b^{e_i})`, +whose rank is the number of odd `e_i`. ∎ + +**Premise (P).** A factor is `σ`-fixed unless it is a paid Gaussian request on one field +whose effective active span contains `q_b`. Scalar operations, copies, adds, routes fixing +`q_b` and the translation `X_{q_b}` are `σ`-fixed. A request on one field is a diagonal +factor, so `rank(σ(F) - F) ≤ 1`. A request inside a native call is counted +individually; the native is a product of its operations. + +Under (P), **c credited targets require at least c paid requests containing q_b**. In the +substitution contract, c = 3,584. The 15·112 = 1,680 thin shears supply at most 1,680, so +the native stages must contain at least **1,904 q_b-touching requests** (≈105.8 per +native call). The formal and literal instances in `verify.py` show both cases: the +substituted three-shear word has 3 terms for 2 credits; the gauge realization has 2 terms +for 2 credits, so the bound is tight there. A pure gauge on a diagonal target yields zero +credits. + +## 4. Obstruction for incremental full-credit realizations + +**Incremental premise (I).** Relative to the selected invoice, the realization keeps +every productive field. It adds `q_b` to targets only, so each main target R becomes R + 1. +It keeps every selected paid request. Each `q_b`-touching request is either an existing +selected request enlarged by `q_b` (rank r → r + 1, at most once per request) or an +additional request of rank ≥ 1. Further costs only add paid work. + +Put `g(x) = (x+1)^t - x^t = ∫_x^{x+1} t y^{t-1} dy`. For `0 < t < 1` it is strictly +decreasing, with `g(0) = 1`. An additional request of rank r' costs `r'^t ≥ 1 ≥ g(x)` for +every x ≥ 0. + +**Theorem.** Under (P) and (I), if every one of the 3,584 main targets is credited (two +unpaid coordinates per live main family), then `S_new(C) < S(C)` for every `0 < C < 1`. +At C = 0 the gain is exactly repaid at best. + +*Proof.* The gain is `Σ_main g(R_i)`. By the lemma, at least 3,584 distinct q_b-touching +requests are charged. Their cost is at least the sum of g over the 3,584 largest selected +paid ranks; additional requests cost at least 1. `verify.py` checks exactly that the +sorted main targets dominate these paid ranks elementwise. The pairs are +145↔72, 73↔64, 65↔64, …, 17↔8 or 5, and every target is larger. Since g is strictly +decreasing, the gain is strictly below the cost. ∎ + +So the fixed-invoice root of any such realization is strictly below the selected root. +The selected package certifies that `S` decreases through C = 1/20 and is negative beyond +it; this is inherited. `verify.py` also encloses the net change at three points +(selected root: ≤ −2.285). + +The conjugation realization is one instance: its rank-one surplus is +`752 + 3584 - 1680 - 4032 = -1376`. It is negative already at C = 0. + +## 5. Partial credits: an explicit ceiling + +When only a subset of main families gets the second coordinate, dominance can fail. Small +targets (17) can be paired with large idles (72). The verifier rejects that case as a +mutation control. For any credited subset of main targets, of size c, + + S_new(C) ≤ S(C) + max_c [ Σ_{c smallest main targets} g(R) - Σ_{c largest paid ranks} g(r) ]. + +The second term is computed with outward intervals as a best prefix; 1,568 pairs have +R < r. At the selected root it is at most 3.67. Bisection on a 1e-9 grid certifies that the +right side is negative at **C = 0.003035069**. No partial-credit incremental +realization certifies that saving, a ceiling of +0.49% over the selected root. + +This is a pointwise certificate at the stated point; the bisection's other points are +sign checks. Credits on helper targets are outside this scope: they change helper +residual frames, which is the helper-retiming mechanism, not a coverage law. + +## 6. What is left open: the native allowance + +In the optimistic relaxation (§2.3) the root is enclosed in +`(0.01023582, 0.010235821)`, 3.39× the selected root. So the relaxation passes, and +only the native charge decides the contract. Adding E rank-one paid units keeps a +positive surplus at the selected root's upper end exactly for **E ≤ 1,859** +(103.28 per native call; E = 1,860 fails). The lemma forces at least 1,904 q_b-touching +requests in the native stages. Paying each one as a separate rank-one request +therefore loses; the conjugation contract pays 4,032. + +By §4, enlarging the selected native requests does not help either. **The only +route left open under (P) is a redesigned native word on the enlarged central block.** +Its own complete local profile must change, and its moment must beat the selected +`H_t - P_t` after it realizes ≥ 1,904/18 central-q_b contacts per call. No such word +is constructed here. + +## 7. Small complete instance + +`verify.py` replays: + +- **Formal (Laurent polynomials in Q_a, Q_b, D).** The one- and two-central three-shear + identities; the native and back-shear conjugations; the gauge realization; the + credit-rank counts; and the diagonal-target zero-credit case. +- **Literal (Gaussian-rational kernels on F2^3, axes q_a, q_b, d).** `C_q^2 = X_q`, + `C_q^{-1} = X_q C_q` and Fourier ranks 1 and 2. It runs six arbitrary dirty input pairs + (X, Y) through the substituted swap word and through the conjugated native-shaped + factor, and compares them with the declared targets. + +The literal algebra has `C_q ∈ span{1, X_q}`, so `σ` is not an automorphism there. The +lemma is a statement about the formal Laurent model in which the controller is +factorized; this is recorded as a modelling premise. diff --git a/research/two-central-laurent-coverage/README.md b/research/two-central-laurent-coverage/README.md new file mode 100644 index 0000000000..300b81d416 --- /dev/null +++ b/research/two-central-laurent-coverage/README.md @@ -0,0 +1,138 @@ +# A second central coordinate on the selected p16 controller must be repaid + +**This is a scoped obstruction with an explicit allowance. It claims no new κ and leaves +the selected record unchanged.** + +Original card: `coverage-law-change` ("Can a template or call contract leave two or more +unpaid coordinates per live family?"). Scope status is **refined**. The card's +`72W + 64N` identity and `ceiling.ceiling(unpaid=…)` belong to the obsolete #1094 +template. This package rebinds the question to the selected #4470 invoice and derives a +replacement bound; [TASK.json](TASK.json) gives the reason. The written argument is in +[PROOF.md](PROOF.md). The exact certificate is [RESULT.json](RESULT.json). + +## Where the one unpaid coordinate comes from + +The selected invoice is #4470, Cinna Davis's p16 query-thinned controller, pinned +byte-for-byte at `research/joint-helper-lattice/RESULT.json`. It has 3,584 = 2·112·16 main +targets: + +- each arm target has rank `1 + 8k` and is paid by a whole-idle of rank `8k`; +- each long target has rank `145 = 1 + 8·18`. + +The extra coordinate is the central Gaussian line `Q = C_q`, which enters every diagonal +target with exponent ±1. The replacement coverage identity is exact: + + rank-one surplus 752 = 18·(H1 − P1 + V + 2VB) − V (V = 112, B = 8). + +## The changed contract and its price + +**Contract.** Substitute `Q → Q_a Q_b`, with `Q_b = C_{q_b}` on a fresh axis. Because all +the symbols commute, this is a ring homomorphism of the Laurent factorization. Every main +target becomes `D·Q_a^{±1}Q_b^{±1}`, so each live main family keeps **two** unpaid +coordinates. The 15 thin shears per port become rank-2 requests. Native stages are realized +exactly by the conjugation + + D_s S_y(Q_a⁻¹Q_b⁻¹) = Δ⁻¹ (D_s S_y(Q_a⁻¹)) Δ, Δ = diag(1, Q_b). + +| Profile (exact intervals) | Result | +|---|---| +| Selected invoice | root in (0.0030201659770, 0.0030201659771), reproduced | +| Optimistic: natives unchanged and free, thin shears rank 2 | root in (0.01023582, 0.010235821), **3.39×** | +| Conjugation-charged natives (+2 rank-one q_b requests per port per native stage) | rank-one surplus **−1,376**: no saving | +| Native allowance over the optimistic profile at the selected root | **≤ 1,859** extra rank-one units (103.28 per call); 1,860 fails | +| q_b-touching requests the natives must contain (credit-rank lemma) | **≥ 1,904** (3,584 credits − 1,680 thin shears) | +| Any incremental full-credit realization (selected paid profile kept, q_b added to requests) | surplus **strictly below the selected surplus at every 0 < C < 1** | +| Any incremental partial-credit realization (main targets only) | cannot certify **C = 0.003035069** (+0.49%) | + +**Credit-rank lemma** (PROOF §3, formal Laurent model). Let σ map `Q_b` to `−Q_b`. The +number of targets with an odd `Q_b` exponent is at most `Σ rank(σ(F) − F)` over the +program's factors. Each paid request containing `q_b` on one field contributes at most 1. +So every second-coordinate credit needs its own `q_b`-touching paid request. + +**Dominance.** The sorted main targets dominate the 3,584 largest paid ranks elementwise. +The marginal `g(x) = (x+1)^t − x^t` strictly decreases. So for every family, adding `q_b` +to existing requests costs more than it earns. + +## What this establishes and what it does not + +- **Established**, under the premises (P) and (I) of PROOF.md: + - the second unpaid coordinate is exactly repaid at C = 0 at best, and is a strict loss + for every C > 0 when every main family is credited; + - partial crediting gains at most +0.49%; + - separate rank-one payment of the forced native terms fails, since 1,904 > 1,859. +- **Not established:** a redesigned native word on the enlarged central block whose own + profile changes. That is the one route left open (see below). +- Scope limits: + - The lemma lives in the formal Laurent model where the controller is factorized. In + the literal group algebra, `C_q ∈ span{1, X_q}`. + - Helper-frame credits are excluded. + - Native/all-column, compiler, completion, precision and outer premises are inherited + unchanged. +- The small complete instance is checked two ways: + - formally, in Laurent polynomials; + - literally, with Gaussian-rational kernels on F2^3 and six arbitrary dirty input + pairs. + + It covers the substitution and conjugation identities only. It is not a replay of the + p16 native word. + +## Reproduce + +Python 3.12, standard library only, about 8 seconds: + +```sh +python3 scripts/research_package.py --package research/two-central-laurent-coverage --check-only +python3.12 -B scripts/research_package.py --package research/two-central-laurent-coverage +python3.12 -B research/two-central-laurent-coverage/verify.py # PASS_TWO_CENTRAL_LAURENT_COVERAGE +``` + +`--write` regenerates RESULT.json. Otherwise the recomputed certificate must match it +byte-for-byte. + +The verifier rejects six mutation controls: + +- an inverse without its `X_q` translation; +- an uncharged second coordinate; +- dominance claimed for small targets only; +- allowance + 1; +- a mutated main target; +- a gauge on the wrong field. + +## Open next questions + +1. **A ten-axis native word.** Is there a redesigned native word on the enlarged central + block whose complete invoice realizes its ≥ 1,904/18 `q_b` contacts per call? It must + still beat the selected native's `H_t − P_t`. + - Why it matters: this is the only route the lemma and the incremental theorem leave + open, and it is worth up to 3.39×. + - First step: lift one fresh-helper stage to a ten-dimensional frame lattice and price + the `Q_aQ_b` cross term against the 1,859-unit allowance. + - Blocker: there is no ten-axis contact proof. +2. **Helper-frame credits.** Can the second coordinate be credited to helper exits + (rank ≤ 9) instead of main targets? + - This belongs to the helper-retiming mechanism and is excluded here. + - First step: count admissible `q_b` helper exits under premise (P). +3. **A global partial-credit ceiling.** Can the pointwise certificate at C = 0.003035069 + become an all-C ceiling? + - First step: bound each paired term's C-derivative by `ln((r+1)/R)`. + - Not blocked. + +## Credit + +- Selected construction and p16 controller: Cinna Davis (1337isnot1337), #4470 and + #4440, with the credited native, helper-retiming and outer lineage in the selected + review. +- Laurent shear and conjugation conventions: `research/kappa-hybrid-controller/NATIVE.md`. +- Complete-surplus model: `research/controller-stage-ceiling` (Cinna Davis). +- Exact ln/exp enclosures: Douglas Colkitt's `research/complex-local-word-ceiling/ceiling.py` + (#1240), reused unchanged. +- Earlier coverage-law work on the #1094 template, which this package does not reprice: + - #1012's coverage identity; + - Navinor's `complex-coverage-law-relief`; + - Clear1nsight's `selected-family-coverage-boundary`; + - `three-bank-restored-unpaid` and `line-port-unpaid-cap`. +- Distinct from the active centre-path, coded p16, two-FULL, H3-prefix and raw-dual lines + (Clear1nsight #4902/#4931/#4932/#4943/#4945; dillona #4930/#4933). + +Prepared by JoyboyBrian with substantial assistance from Anthropic Claude (Claude Code, +Opus 5.5). Apache-2.0. diff --git a/research/two-central-laurent-coverage/RESULT.json b/research/two-central-laurent-coverage/RESULT.json new file mode 100644 index 0000000000..a695530da6 --- /dev/null +++ b/research/two-central-laurent-coverage/RESULT.json @@ -0,0 +1,55 @@ +{ + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "controls": { + "allowance_holds": true, + "allowance_plus_one_fails": true, + "inverse_without_translation": true, + "mutated_main_target_rejected": true, + "partial_credit_breaks_dominance": true, + "uncharged_second_coordinate": true, + "wrong_gauge_orientation_rejected": true + }, + "coverage_identity": { + "helper_mass": 3471, + "identity": "surplus(C=0) = 18*(H1 - P1 + V + 2VB) - V = 752", + "main_targets": 3584, + "native_paid_mass": 5327, + "rank_one_surplus": 752 + }, + "formal_instance": { + "credits": 2, + "gauge_qb_terms": 2, + "interleaved_monomial": true, + "substitution_qb_terms": 3 + }, + "literal_instance": { + "central_ranks": [ + 1, + 2 + ], + "columns_replayed": 6, + "field_dimension": 3 + }, + "moments": { + "allowance_per_native_call": "1859/18", + "allowance_rank_one_units": 1859, + "conjugation_rank_one_surplus": -1376, + "full_credit_net_upper_at_selected_root": -2.2852989943453053, + "native_qb_terms_needed": 1904, + "native_terms_fit_allowance_as_rank_one": false, + "optimistic_ratio_vs_selected": 3.3891581050881707, + "optimistic_root": [ + "511791/50000000", + "10235821/1000000000" + ], + "partial_best_net_gain_at_selected_root": 3.668156940596911, + "partial_credit_ceiling": "3035069/1000000000", + "partial_pairs_with_target_below_charge": 1568, + "selected_root": [ + "3020165977/1000000000000", + "30201659771/10000000000000" + ] + }, + "selected_source_sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21", + "status": "PASS_TWO_CENTRAL_LAURENT_COVERAGE" +} diff --git a/research/two-central-laurent-coverage/SOURCES.json b/research/two-central-laurent-coverage/SOURCES.json new file mode 100644 index 0000000000..e27fe58c43 --- /dev/null +++ b/research/two-central-laurent-coverage/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + }, + { + "path": "research/controller-stage-ceiling/PROOF.md", + "usage": "input", + "git_blob": "23a4ba90aad2bd5a1ce4dac2a435e0a7029f71f4", + "sha256": "10d7b104ee29c31f481bbe6bb82a0177e8c1c114cdeb8da2a047963f48772c04" + }, + { + "path": "research/joint-helper-lattice/RESULT.json", + "usage": "input", + "git_blob": "edf41a49a0350862c23378f837c7397fc5dc7596", + "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21" + }, + { + "path": "research/kappa-hybrid-controller/NATIVE.md", + "usage": "input", + "git_blob": "ea4cfb4a556a68a9c73956900eb4df144226157d", + "sha256": "69f06a56bb0cf7d1922df7ac5e7cc36f5c67d17c52f244b1231bd58b050a590a" + } + ] +} diff --git a/research/two-central-laurent-coverage/TASK.json b/research/two-central-laurent-coverage/TASK.json new file mode 100644 index 0000000000..56b34ad3a9 --- /dev/null +++ b/research/two-central-laurent-coverage/TASK.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 7, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "original_card": { + "id": "coverage-law-change", + "question": "Can a template or call contract leave two or more unpaid coordinates per live family?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/idle-axis-hosting/PROOF.md", + "certificates/selected-result.json" + ], + "methods": [ + "State a replacement for the coverage identity (mass = 72W + 64N) and the contract change that realizes it, with its implementation cost.", + "Find an obstruction: show which data-endpoint obligation forces exactly one unpaid coordinate in the current template." + ], + "acceptance_gate": "An explicit replacement identity, verified on a small complete instance with dirty inputs, priced with ceiling.ceiling(unpaid=...). A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Explain where the single unpaid coordinate per family comes from in the hosted template; propose one change and price it. Ideal budget: two unpaid coordinates per family is 3.77x (levers.py).", + "bottleneck_link": "The deficit is one coordinate per family minus the centre charge; doubling unpaid coordinates per family scales it directly.", + "allowed_variations": [ + "One template change or one endpoint-contract change.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Counting a coordinate as unpaid while leaving it unadvanced in the data endpoint.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "coverage identity", + "unpaid coordinate", + "deficit law", + "W - 64N" + ] + }, + "scope_status": "refined", + "actual_scope": "On the selected #4470 p16 Laurent controller, can the ring substitution Q -> Qa*Qb (a second central Gaussian line on a fresh axis) leave two unpaid coordinates per main family at a fully charged cost that beats the selected fixed-invoice root?", + "scope_change_reason": "The card's starting points price the obsolete #1094 hosted template (mass = 72W + 64N, ceiling.ceiling(unpaid=...)). The selected record is now the #4470 productive-helper interface, where that identity and ceiling do not apply. This package rebinds the card to the selected invoice: it identifies the single unpaid coordinate as the central line Q = C_q in every main target, names one changed call contract (Q -> Qa*Qb), and derives a replacement bound for it instead of reusing the incumbent ceiling outside its scope.", + "bottleneck_link": "In the selected invoice the 3,584 main targets each carry one central coordinate that no paid idle advances. A second central coordinate per family is worth 3.39x the selected root under the optimistic relaxation. That is the card's lever on the current interface, so its price decides whether the coverage lever is live.", + "budget_minutes": 150, + "stop_rule": "Stop after the source identity, the formal and literal instance, the credit-rank lemma, the optimistic root, the native allowance, the full-credit obstruction and the partial-credit ceiling are certified. Do not search for a redesigned ten-axis native word in this package.", + "outcome": "negative-result", + "evidence": "Exact identity on the pinned #4470 invoice: every main target is 1 + 8k with an 8k paid idle (or 1 + 8*18 for the long target); the rank-one surplus is 752 = 18*(H1 - P1 + V + 2VB) - V. The substitution Q -> Qa*Qb is an exact controller with two central exponents per target, checked formally and on six dirty F2^3 inputs. Optimistic relaxation (natives unchanged, thin shears rank 2): root in (0.01023582, 0.010235821), 3.39x. Credit-rank lemma: c credited targets need c q_b-touching paid requests, so the natives need at least 1,904. Allowance: at most 1,859 extra rank-one units keep a positive surplus at the selected root. Conjugation-charged profile: rank-one surplus -1,376. Full-credit theorem: any incremental realization (selected paid profile kept, q_b added to requests or new requests) is strictly below the selected surplus at every 0 < C < 1. Partial-credit incremental realizations cannot certify C = 0.003035069 (+0.49% ceiling).", + "author": "JoyboyBrian", + "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5)", + "open_questions": [ + { + "question": "Is there a redesigned native word on the enlarged central block (q_a, q_b plus the eight stage axes) whose complete local invoice realizes its at least 1,904/18 q_b contacts per call and still beats the selected native's H_t - P_t?", + "why_it_matters": "It is the only route the credit-rank lemma and the incremental theorem leave open, and the optimistic relaxation is worth 3.39x the selected root.", + "first_step": "Lift one fresh-helper native stage to a ten-dimensional frame lattice and compute the minimal number of helper-frame and paid-request changes needed to produce the Qa*Qb cross term; compare its local moment change against the 1,859-unit allowance.", + "blocked_by": "No ten-axis native word or contact proof exists; the native geometry and phase checks are pinned to nine-axis blocks." + }, + { + "question": "Can a contract credit the second coordinate to helper residual frames rather than main targets, at a q_b-request cost below the helper gain?", + "why_it_matters": "Helper targets have rank at most 9, so g(R) is larger there; the partial-credit ceiling here deliberately excludes them.", + "first_step": "Bound the number of helper exits that can contain q_b under the premise (P) and price them against the largest paid requests, as in section 5 of PROOF.md.", + "blocked_by": "This is the helper-retiming mechanism; whether a fresh central axis is admissible in helper exit frames needs the native contact proof." + }, + { + "question": "Does the partial-credit bound extend to a global all-C ceiling?", + "why_it_matters": "The certificate is pointwise at C = 0.003035069; a monotonicity argument would make it a ceiling in the stage-ceiling sense.", + "first_step": "Bound the C-derivative of each paired term g(R) - g(r) by ln((r+1)/R) and combine with the selected package's certified surplus derivative.", + "blocked_by": "Not blocked; omitted for the session budget." + } + ] +} diff --git a/research/two-central-laurent-coverage/VERIFY.json b/research/two-central-laurent-coverage/VERIFY.json new file mode 100644 index 0000000000..c440296d5f --- /dev/null +++ b/research/two-central-laurent-coverage/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-local-word-ceiling/ceiling.py", + "research/controller-stage-ceiling/PROOF.md", + "research/joint-helper-lattice/RESULT.json", + "research/kappa-hybrid-controller/NATIVE.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source identity of the selected #4470 invoice; formal and literal (dirty F2^3) instances of the two-central substitution and conjugation; credit-rank lemma counts; exact interval roots, allowance, full-credit dominance and partial-credit ceiling; controls reject a missing inverse translation, an uncharged second coordinate, partial-credit dominance, allowance+1, a mutated main target and a wrong gauge orientation; RESULT.json must equal the recomputed certificate." + } + ] +} diff --git a/research/two-central-laurent-coverage/verify.py b/research/two-central-laurent-coverage/verify.py new file mode 100644 index 0000000000..1db4e7ba66 --- /dev/null +++ b/research/two-central-laurent-coverage/verify.py @@ -0,0 +1,487 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Two-central Laurent substitution on the selected #4470 p16 invoice. + +Checks, all exact (Fractions and outward-rounded rational intervals): + + 1. source binding: the selected complete invoice (joint-helper-lattice RESULT.json, + the selected record's source certificate) and its one-central coverage identity; + 2. a small complete instance: formal Laurent identities for the substitution + Q -> Qa*Qb and the conjugation contract, plus a literal Gaussian-rational + operator replay on F2^3 with arbitrary (dirty) inputs; + 3. the credit-rank lemma on those instances (sigma: Qb -> -Qb); + 4. moments: the selected root, the optimistic relaxation, the conjugation-charged + profile, the native allowance, the full-credit dominance obstruction and the + partial-credit ceiling; + 5. mutation controls that must be rejected. + +usage: verify.py [--write] +JoyboyBrian, with substantial assistance from Anthropic Claude. Apache-2.0. +""" +import hashlib +import json +import random +import sys +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(ROOT / 'research' / 'complex-local-word-ceiling')) +import ceiling as CE # noqa: E402 (stdlib exact ln/exp enclosures, pinned in SOURCES.json) + +SELECTED = ROOT / 'research' / 'joint-helper-lattice' / 'RESULT.json' +SELECTED_SHA = 'c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21' +V, B, NATIVE, PAIRS, THIN = 112, 8, 18, 16, 15 +SEL_LO, SEL_HI = Q(3020165977, 10 ** 12), Q(30201659771, 10 ** 13) + + +def require(ok, why): + if not ok: + raise SystemExit('FAIL: ' + why) + + +def rejected(fn, *args): + """True when fn raises (a control the verifier must reject).""" + try: + fn(*args) + except (SystemExit, AssertionError, ValueError): + return True + return False + + +# ---------------------------------------------------------------- 1. source binding +def load_selected(): + raw = SELECTED.read_bytes() + require(hashlib.sha256(raw).hexdigest() == SELECTED_SHA, 'selected RESULT.json hash') + d = json.loads(raw) + T = {int(k): v for k, v in d['targets'].items()} + P = {int(k): v for k, v in d['paid'].items()} + return d, T, P + + +def coverage_identity(d, T, P): + """One central credit per main target: target 1+8k against paid idle 8k, 145 = 1+8*18.""" + require(d['full_calls'] == NATIVE and d['pairs'] == PAIRS and d['query_shears'] == THIN, 'controller shape') + H = {int(k): v for k, v in d['local_helpers'].items()} + Pl = {int(k): v for k, v in d['local_paid'].items()} + main = {r: n for r, n in T.items() if r > 9} + require(sum(T.values()) == d['productive_fields'] == 10928, 'productive fields') + require(sum(P.values()) == d['paid_calls'] == 64620, 'paid calls') + require(main == {145: 2 * V, 73: 2 * V, **{1 + B * k: 4 * V for k in range(2, 9)}}, 'main targets') + require(all(P[B * k] == main[1 + B * k] for k in range(2, 10)), 'idle 8k matches target 1+8k') + require(145 == 1 + B * NATIVE, 'long target is 1 + 8 * natives') + credits = sum(main.values()) + require(credits == 2 * V * PAIRS == 3584, 'one central credit per main target') + require(P[1] == NATIVE * Pl[1] + V * THIN, 'thin queries are rank one') + m1 = sum(r * n for r, n in T.items()) - sum(r * n for r, n in P.items()) + h1, p1 = sum(r * n for r, n in H.items()), sum(r * n for r, n in Pl.items()) + require(m1 == 752 == NATIVE * (h1 - p1 + V + 2 * V * B) - V, 'rank-one surplus identity') + return dict(main_targets=credits, rank_one_surplus=m1, helper_mass=h1, native_paid_mass=p1, + identity='surplus(C=0) = 18*(H1 - P1 + V + 2VB) - V = 752') + + +# ---------------------------------------------------------------- 2/3. small complete instance +class L: + """Laurent polynomial in (Qa, Qb, D) with rational coefficients.""" + + def __init__(self, t=None): + self.t = {k: v for k, v in (t or {}).items() if v} + + @staticmethod + def mono(a=0, b=0, d=0, c=1): + return L({(a, b, d): Q(c)}) + + def __add__(s, o): + t = dict(s.t) + for k, v in o.t.items(): + t[k] = t.get(k, 0) + v + return L(t) + + def __neg__(s): + return L({k: -v for k, v in s.t.items()}) + + def __sub__(s, o): + return s + (-o) + + def __mul__(s, o): + t = {} + for k1, v1 in s.t.items(): + for k2, v2 in o.t.items(): + k = tuple(x + y for x, y in zip(k1, k2)) + t[k] = t.get(k, 0) + v1 * v2 + return L(t) + + def __eq__(s, o): + return s.t == o.t + + def sigma(s): + return L({k: (-v if k[1] % 2 else v) for k, v in s.t.items()}) + + +ONE, ZERO = L.mono(), L() + + +def mm(A, Bm): + n = len(A) + return [[sum((A[i][k] * Bm[k][j] for k in range(n)), ZERO) for j in range(n)] for i in range(n)] + + +def word(*Ms): + out = Ms[0] + for M in Ms[1:]: + out = mm(out, M) + return out + + +def Sy(c): # (X, Y) -> (X, Y + c X) + return [[ONE, ZERO], [c, ONE]] + + +def Sx(c): # (X, Y) -> (X + c Y, Y) + return [[ONE, c], [ZERO, ONE]] + + +def diag(a, b): + return [[a, ZERO], [ZERO, b]] + + +def rank2(M): + if all(x == ZERO for row in M for x in row): + return 0 + return 2 if not (M[0][0] * M[1][1] - M[0][1] * M[1][0]) == ZERO else 1 + + +def sig_pert(M): + return [[x.sigma() - x for x in row] for row in M] + + +def odd_entries(T): + return sum(1 for row in T for x in row if x != ZERO and any(k[1] % 2 for k in x.t)) + + +def formal_instance(): + Qa, Qb, D = L.mono(1), L.mono(0, 1), L.mono(0, 0, 1) + Qai, Qbi = L.mono(-1), L.mono(0, -1) + Q2, Q2i = Qa * Qb, Qai * Qbi + out = {} + # one-central swap controller and its substitution + W1 = word(Sy(Qai), Sx(-Qa), Sy(Qai)) + require(W1 == [[ZERO, -Qa], [Qai, ZERO]], 'one-central three-shear identity') + W2 = word(Sy(Q2i), Sx(-Q2), Sy(Q2i)) + T2 = [[ZERO, -Q2], [Q2i, ZERO]] + require(W2 == T2, 'two-central substituted identity') + # native contact by conjugation, Delta = diag(1, Qb) + Dl, Dli = diag(ONE, Qb), diag(ONE, Qbi) + F1 = mm(diag(D, D), Sy(Qai)) + require(word(Dli, F1, Dl) == mm(diag(D, D), Sy(Q2i)), 'native conjugation F_s(QaQb) = Delta^-1 F_s(Qa) Delta') + require(word(Dli, Sx(-Qa), Dl) == Sx(-Q2), 'back shear conjugation') + G = word(Dli, W1, Dl) + require(G == T2, 'gauge realization of the two-central swap') + # credit-rank lemma on both realizations (sigma: Qb -> -Qb) + credits = odd_entries(T2) + require(credits == 2 and rank2(sig_pert(T2)) == 2, 'two odd credits') + subst_terms = sum(rank2(sig_pert(F)) for F in (Sy(Q2i), Sx(-Q2), Sy(Q2i))) + gauge_terms = sum(rank2(sig_pert(F)) for F in (Dli, Dl)) + require(credits <= subst_terms == 3 and credits <= gauge_terms == 2, 'credit-rank lemma instances') + # gauge on a diagonal target gives no credit + Td = diag(D * Qa, D * Qai) + require(odd_entries(word(Dli, Td, Dl)) == 0, 'diagonal targets absorb a pure gauge') + # a longer interleaved controller with D factors: 2*p shears, product is monomial + W3 = word(mm(diag(D, D), Sy(Q2i)), Sx(-Q2), Sy(Q2i)) + out['interleaved_monomial'] = all((W3[i][j] == ZERO) == (i == j) for i in range(2) for j in range(2)) + require(out['interleaved_monomial'], 'interleaved word stays antidiagonal') + require(odd_entries(W3) <= 3, 'lemma on interleaved word') + out.update(credits=credits, substitution_qb_terms=subst_terms, gauge_qb_terms=gauge_terms) + return out + + +# literal operators on F2^3: axes qa = 1, qb = 2, d = 4 (bit masks); Gaussian rationals as pairs +def gmul(x, y): + return (x[0] * y[0] - x[1] * y[1], x[0] * y[1] + x[1] * y[0]) + + +def gadd(x, y): + return (x[0] + y[0], x[1] + y[1]) + + +HALF_P, HALF_M = (Q(1, 2), Q(1, 2)), (Q(1, 2), Q(-1, 2)) # (1+i)/2, (1-i)/2 +N3 = 8 + + +def conv(kernel, f): + out = [(Q(0), Q(0))] * N3 + for s, c in kernel.items(): + for x in range(N3): + out[x ^ s] = gadd(out[x ^ s], gmul(c, f[x])) + return out + + +def kmul(k1, k2): + out = {} + for s1, c1 in k1.items(): + for s2, c2 in k2.items(): + out[s1 ^ s2] = gadd(out.get(s1 ^ s2, (Q(0), Q(0))), gmul(c1, c2)) + return {s: c for s, c in out.items() if c != (Q(0), Q(0))} + + +def Cq(q): + return {0: HALF_P, q: HALF_M} + + +def Xq(q): + return {q: (Q(1), Q(0))} + + +def fourier_rank(kernel): + basis = [] + for s in kernel: + for b in basis: + s = min(s, s ^ b) + if s: + basis.append(s) + return len(basis) + + +def literal_instance(inverse_translation=True): + qa, qb, dd = 1, 2, 4 + require(kmul(Cq(qa), Cq(qa)) == Xq(qa), 'C_q^2 = X_q') + inv = (lambda q: kmul(Xq(q), Cq(q))) if inverse_translation else Cq + require(kmul(Cq(qa), inv(qa)) == {0: (Q(1), Q(0))}, 'C_q^-1 = X_q C_q') + Q2 = kmul(Cq(qa), Cq(qb)) + Q2i = kmul(inv(qa), inv(qb)) + require(fourier_rank(Cq(qa)) == 1 and fourier_rank(Q2) == 2, 'central ranks one and two') + D = Cq(dd) + rng = random.Random(20261023) + for _ in range(6): # arbitrary dirty inputs (Gaussian integers) + X = [(Q(rng.randint(-9, 9)), Q(rng.randint(-9, 9))) for _ in range(N3)] + Y = [(Q(rng.randint(-9, 9)), Q(rng.randint(-9, 9))) for _ in range(N3)] + # three-shear word with Q = Qa Qb: S_y(Q^-1) S_x(-Q) S_y(Q^-1), rightmost first + x, y = X, [gadd(a, b) for a, b in zip(Y, conv(Q2i, X))] + x = [gadd(a, (-b[0], -b[1])) for a, b in zip(x, conv(Q2, y))] + y = [gadd(a, b) for a, b in zip(y, conv(Q2i, x))] + require(x == [(-b[0], -b[1]) for b in conv(Q2, Y)] and y == conv(Q2i, X), 'two-central swap on dirty input') + # conjugation contract for one native-shaped factor D S_y(Qa^-1 Qb^-1) + lhs_x, lhs_y = conv(D, X), conv(D, [gadd(a, b) for a, b in zip(Y, conv(Q2i, X))]) + y1 = conv(Cq(qb), Y) # Delta + x2, y2 = conv(D, X), conv(D, [gadd(a, b) for a, b in zip(y1, conv(inv(qa), X))]) # F_s(Qa) + y3 = conv(inv(qb), y2) # Delta^-1 + require(x2 == lhs_x and y3 == lhs_y, 'conjugated native factor on dirty input') + return dict(columns_replayed=6, field_dimension=3, central_ranks=[1, 2]) + + +# ---------------------------------------------------------------- 4. moments +def power(r, C): + """Enclosure of r^(1-C) for integer r >= 1, 0 <= C <= 1/20.""" + if r == 1: + return Q(1), Q(1) + lo, hi = CE.ln(r) + e = CE.exp(C * lo, C * hi) + return CE.down(Q(r) / e[1]), CE.up(Q(r) / e[0]) + + +def moment(prof, C): + lo = hi = Q(0) + for r, n in prof.items(): + a, b = power(r, C) + lo, hi = lo + n * a, hi + n * b + return lo, hi + + +def surplus(T, P, C): + t, p = moment(T, C), moment(P, C) + return t[0] - p[1], t[1] - p[0] + + +def sign(T, P, C): + lo, hi = surplus(T, P, C) + require(lo > 0 or hi < 0, f'enclosure does not separate at C={C}') + return 1 if lo > 0 else -1 + + +def bump(prof, delta): + out = dict(prof) + for r, n in delta.items(): + out[r] = out.get(r, 0) + n + require(out[r] >= 0, 'negative count') + return {r: n for r, n in out.items() if n} + + +def credited(T): + """Every main target gains the second central coordinate (rank + 1).""" + out = {} + for r, n in T.items(): + k = r + 1 if r > 9 else r + out[k] = out.get(k, 0) + n + return out + + +def root_bracket(T, P, lo, hi, grid): + require(sign(T, P, lo) > 0 and sign(T, P, hi) < 0, 'root bracket ends') + while hi - lo > grid: + mid = Q(int((lo + hi) / 2 / grid)) * grid + mid = lo + grid if mid <= lo else mid + if sign(T, P, mid) > 0: + lo = mid + else: + hi = mid + return lo, hi + + +def charged(credits, qb_terms): + """Credit-rank lemma: every second-coordinate credit needs a q_b-touching rank-one term.""" + require(credits <= qb_terms, f'{credits} credits but only {qb_terms} q_b-touching terms') + return True + + +def dominates(targets, paid): + """Sorted main targets dominate the same number of largest paid ranks, elementwise.""" + tl = sorted((r for r, n in targets.items() for _ in range(n)), reverse=True) + pl = sorted((r for r, n in paid.items() for _ in range(n)), reverse=True)[:len(tl)] + require(len(pl) == len(tl) and all(a >= b for a, b in zip(tl, pl)) and tl != pl, 'dominance') + return True + + +def g(r, C): + a, b = power(r + 1, C) + if r == 0: + return a, b + c, d = power(r, C) + return a - d, b - c + + +def partial_gain_upper(main, P, C): + """Max over credited subsets S of sum_S g(R) - (cheapest charge for |S| q_b terms).""" + tl = sorted((r for r, n in main.items() for _ in range(n))) # small targets first + pl = sorted((r for r, n in P.items() for _ in range(n)), reverse=True) # large requests first + best = cur = Q(0) + cache = {} + for R, r in zip(tl, pl): + key = (R, r) + if key not in cache: + cache[key] = g(R, C)[1] - g(r, C)[0] + cur += cache[key] + best = max(best, cur) + return best, sum(1 for R, r in zip(tl, pl) if R < r) + + +def moments(T, P): + out = {} + require(sign(T, P, SEL_LO) > 0 and sign(T, P, SEL_HI) < 0, 'selected root bracket') + out['selected_root'] = [str(SEL_LO), str(SEL_HI)] + main = {r: n for r, n in T.items() if r > 9} + credits = sum(main.values()) + T2 = credited(T) + # (i) optimistic relaxation: natives unchanged, thin queries rank 2 + P_opt = bump(P, {1: -V * THIN, 2: V * THIN}) + # the thin shears supply V*THIN q_b terms; the lemma charges the rest to the natives + require(rejected(charged, credits, V * THIN), 'thin shears alone cannot pay every credit') + lo, hi = root_bracket(T2, P_opt, Q(1, 100), Q(11, 1000), Q(1, 10 ** 9)) + out['optimistic_root'] = [str(lo), str(hi)] + out['optimistic_ratio_vs_selected'] = float(lo / SEL_HI) + out['native_qb_terms_needed'] = credits - V * THIN + # (ii) conjugation-charged: two rank-one q_b requests per port per native stage + P_conj = bump(P_opt, {1: 2 * V * NATIVE}) + charged(credits, V * THIN + 2 * V * NATIVE) + m1 = sum(r * n for r, n in T2.items()) - sum(r * n for r, n in P_conj.items()) + require(m1 == 752 + credits - V * THIN - 2 * V * NATIVE == -1376, 'conjugation mass') + require(sign(T2, P_conj, SEL_LO) < 0, 'conjugation profile loses at the selected root') + out['conjugation_rank_one_surplus'] = m1 + # (iii) allowance: extra rank-one units on top of the optimistic profile at the selected root end + def ok(e): + return sign(T2, bump(P_opt, {1: e}), SEL_HI) > 0 + lo_e, hi_e = 0, 2 * V * NATIVE + require(ok(lo_e) and not ok(hi_e), 'allowance bracket') + while hi_e - lo_e > 1: + mid = (lo_e + hi_e) // 2 + lo_e, hi_e = (mid, hi_e) if ok(mid) else (lo_e, mid) + out['allowance_rank_one_units'] = lo_e + out['allowance_per_native_call'] = str(Q(lo_e, NATIVE)) + out['native_terms_fit_allowance_as_rank_one'] = (credits - V * THIN) <= lo_e + # (iv) full-credit dominance: any incremental realization is strictly below selected + dominates(main, P) + gain, cost = Q(0), Q(0) + tl = sorted((r for r, n in main.items() for _ in range(n)), reverse=True) + pl = sorted((r for r, n in P.items() for _ in range(n)), reverse=True)[:len(tl)] + for C in (SEL_LO, Q(1, 1000), Q(1, 100)): + acc = Q(0) + cache = {} + for R, r in zip(tl, pl): + if (R, r) not in cache: + cache[(R, r)] = g(R, C)[1] - g(r, C)[0] + acc += cache[(R, r)] + require(acc < 0, f'full-credit gain below cheapest charge at C={C}') + if C == SEL_LO: + gain = acc + out['full_credit_net_upper_at_selected_root'] = float(gain) + # (v) partial-credit ceiling: surplus_sel + best partial net gain + def part_sign(C): + best, _ = partial_gain_upper(main, P, C) + lo_s, hi_s = surplus(T, P, C) + if lo_s > 0: + return 1 + require(hi_s + best < 0, f'partial ceiling does not separate at C={C}') + return -1 + best_sel, pairs_gaining = partial_gain_upper(main, P, SEL_HI) + require(best_sel > 0, 'partial credits can gain a little (positive control)') + lo_c, hi_c = SEL_LO, Q(3040, 10 ** 6) + require(part_sign(hi_c) < 0, 'partial ceiling end') + grid = Q(1, 10 ** 9) + while hi_c - lo_c > grid: + mid = Q(int((lo_c + hi_c) / 2 / grid)) * grid + mid = lo_c + grid if mid <= lo_c else mid + try: + s = part_sign(mid) + except SystemExit: + s = 1 + lo_c, hi_c = (mid, hi_c) if s > 0 else (lo_c, mid) + out['partial_credit_ceiling'] = str(hi_c) + out['partial_best_net_gain_at_selected_root'] = float(best_sel) + out['partial_pairs_with_target_below_charge'] = pairs_gaining + return out, T2, P_opt + + +# ---------------------------------------------------------------- 5. controls +def controls(d, T, P, T2, P_opt, allowance): + main = {r: n for r, n in T.items() if r > 9} + c = {} + c['inverse_without_translation'] = rejected(literal_instance, False) + c['uncharged_second_coordinate'] = rejected(charged, sum(main.values()), 0) + # crediting only the smallest main targets is the partial-credit loophole: no dominance + c['partial_credit_breaks_dominance'] = rejected(dominates, {17: 4 * V}, P) + c['allowance_plus_one_fails'] = sign(T2, bump(P_opt, {1: allowance + 1}), SEL_HI) < 0 + c['allowance_holds'] = sign(T2, bump(P_opt, {1: allowance}), SEL_HI) > 0 + bad = dict(T) + bad[145] -= 1 + bad[146] = 1 + c['mutated_main_target_rejected'] = rejected(coverage_identity, d, bad, P) + D, Qb, Qbi = L.mono(0, 0, 1), L.mono(0, 1), L.mono(0, -1) + native = mm(diag(D, D), Sy(L.mono(-1))) + wrong = word(diag(Qbi, ONE), native, diag(Qb, ONE)) # gauge on X instead of Y + c['wrong_gauge_orientation_rejected'] = wrong != mm(diag(D, D), Sy(L.mono(-1, -1))) + require(all(c.values()), 'control failed: ' + json.dumps(c)) + return c + + +def main(): + d, T, P = load_selected() + res = {'status': 'PASS_TWO_CENTRAL_LAURENT_COVERAGE', 'base_commit': 'cef4b52f2a59009865bf8eabde1be3f159063703', + 'selected_source_sha256': SELECTED_SHA} + res['coverage_identity'] = coverage_identity(d, T, P) + res['formal_instance'] = formal_instance() + res['literal_instance'] = literal_instance() + mres, T2, P_opt = moments(T, P) + res['moments'] = mres + res['controls'] = controls(d, T, P, T2, P_opt, mres['allowance_rank_one_units']) + path = HERE / 'RESULT.json' + text = json.dumps(res, indent=2, sort_keys=True) + '\n' + if '--write' in sys.argv[1:]: + path.write_text(text) + else: + require(path.exists() and path.read_text() == text, 'RESULT.json differs from the recomputed certificate') + print(json.dumps(res['moments'], indent=2, sort_keys=True)) + print('PASS_TWO_CENTRAL_LAURENT_COVERAGE') + + +if __name__ == '__main__': + main()