diff --git a/research/complex-halving-degree-invoice/PROOF.md b/research/complex-halving-degree-invoice/PROOF.md new file mode 100644 index 0000000000..31005cc810 --- /dev/null +++ b/research/complex-halving-degree-invoice/PROOF.md @@ -0,0 +1,245 @@ +# Halving degree of the selected complex finite invoice under the inherited degree-t ledger: scoped statement and proof + +All numbers below are recomputed exactly by [verify.py](verify.py) and stored in +[RESULT.json](RESULT.json). This is a scoped finite statement under inherited +hypotheses. It is not a supplier, not a κ and not a multiplication theorem. + +## Objects + +- **Selected invoice.** The selected #1094 replay stores its finite invoice at + `candidate/strict/global/audit/PREFIX-AND-INVOICE.json` inside + `research/community-frontier1094-audit/selected-replay.tar.gz`. Its member + SHA256 is `212cf4ee…0d12`. The fields are: physical roles 14826, stock bits + S = 2642, physical row 16469, retained row 20161, `row_prefix_extra` 1024, and the + halving inequality [5329, 4608], that is, 73² > 2·48². +- **Ledger formula.** The selected assembler `research/complex-sw4-frame8/code/` + (hashed by verify.py against the selected source manifest + `research/community-frontier1094-audit/SELECTED-SOURCE.json`) computes + `row=2*stock.bit_length()+9909+252+2*payload` with `payload=512` + (`invoice_allcold.py:263,278`). It checks `row<20161` and + `halving=m*m>2*maxchild*maxchild` (`:283`). `assemble.py` asserts + `0 2R^t. Every + complex ceiling screen uses t = 2, which forces R ≤ 51. + +## Inherited hypotheses (not proved here) + +- **H1 (degree-t ledger).** The lineage's finite-cover transfer can be instantiated + at halving degree t. It then needs the guard 73^t > 2R^t and charges + Row(t, S) = t·S + 9909 + 252 + prefix(t). The source support is in the lineage's own + notes, which charge "a row divisor W(w) at each coarse level" + (`notes/three-stage-cover-rows.tex`). They instantiate the same ledger at degree 4 + (`notes/paired-cube-assembly.tex`: "least halving degree for 72→60 is four, + contributing 10,284" = 4·2571, then 10284 + 9909 + 252 = 20445). They also + instantiate it at degree 24 (`notes/three-stage-cover-assembly.tex`: 24·2431 = 58344, + then 58344 + 9909 + 252 = 68505). In both, 9909 + 252 is unchanged and the multiplier + of the stock bits is the least halving degree. The bridge factor is derived as + log2 Q ≤ (51/25)·K·log2 p with K a sum of halving-degree × bit-length terms + (`notes/structured-bulk-assembly.tex`), which is linear in the degree. #3421 + (VictorLiwentao, `research/selected-stock-shape-a-zero`) proves the m = 73 per-level + stock shape A = 0 with B_bits = 2642, so S is the per-level allowance (ρ unbound). + Not checked here: whether the written transfer proof behind this particular assembler + is generic in the degree. +- **H2 (prefix).** prefix(t) is either the fixed value 1024 or 512·t. Source does not + settle this. `row_prefix_extra = 2*payload` is only instantiated at t = 2, and the + t = 4 and t = 24 precedents carry no prefix term. Both values are carried throughout. + Reading A's t_max = 3 is robust: t = 3 is admissible under A for any + prefix(3) ≤ 20160 − 3·2642 − 10161 = 2073 (a superlinear form such as 256·t² would + give t_max = 2). +- **H3 (row contract).** + - Reading **B** (bridge-only; favoured by source): the retained coefficient K may be + re-chosen while the bridge factor 51/25 and reserve 10^6 stay fixed. The cap is + K ≤ ⌊(25·10^6 − 1)/51⌋ = 490196, with gap 10^6 − (51/25)·490196 = 4/25 > 0, and + Row < K. Support: the outer engine consumes `degree_gap` only as the positivity slack + `row_product_gap` (`research/contextual-provider-pooling/engines/outer.py:45`); the + lineage calls 20161 a "retained … allowance"; the lineage bridge text + (`research/five-stage-gen4-banks/inputs/complex/retained/FINITE_BRIDGE.txt`, section + 4; outside the selected manifest) derives A = 10000 + 9909 + 252 = 20161 at halving + degree 1 and says increasing these overcharges changes only constants; the + selected-manifest lineage assembler `research/direct-delivery504-global/code/assemble.py:29` + certifies the bridge at max(20161, rows); an earlier assembly in the same bridge + lineage charges row 20445 against its own reserve 70000; and 51/25 is t-independent + (H1). + - Reading **A** (retained-binding; fallback): the retained coefficient 20161 is a + binding contract, so Row < 20161 (`assemble.py:159,175,204`; + `invoice_allcold.py:307`; under B these stay satisfied because K ≥ 20161). + - Reading **C**, recorded but not used for numbers: the reserve exponent itself is + chosen per assembly. The pinned notes use 70000, 108000 and 160000; + `notes/structured-bulk-assembly.tex` says the related suffix condition "holds + eventually for every fixed ε<1". Under C the row invoice gives no finite cap on t, + and every admissibility conclusion of B holds a fortiori (its t_max values, being + upper bounds, do not). +- **H4 (other checks independent of t).** None of the formulas for + `local_primitive_bound`, `logical`, `router`, `literal`, `mass`, `precision` and + `tape` contains the halving degree. The square in `router` and `literal` is the + exchange count of a W-role permutation ("A full W-role permutation costs at most W² + elementary exchanges"). The degree-24 precedent keeps it at W² + (`2GW^2+8s+4W+4+32m_c 2R^t. A child rank R is admissible exactly + when t_min(R) ≤ t_max. So R ≤ 57 under A and R ≤ 72 under B. R = 73 is never + admissible, so R ≤ 72 for every t, independently of H1–H4. A rank-56 idle bin (t_min = 3) is admissible under every reading. +3. For general stock, (R, S) is admissible exactly when + S ≤ S_max(R) = ⌊(cap − 1 − 10161 − prefix(t))/t⌋ with t = t_min(R). Examples: + - R = 57: S ≤ 2991 or 2821 (reading A, fixed or per-level prefix). + - R = 72 under A: S ≤ 175 with the fixed prefix; with the per-level prefix no + positive S works. + - R = 72 under B: S ≤ 9392 or 8900. +4. Apply the relaxation of `research/complex-local-word-ceiling` (Colkitt) to the + selected local word, letting idle ranks go up to R. The certified ceilings are: + - R = 51: a < 1690054109089/10^15, the published value. + - R = 57: a < 426212879067/(2.5·10^14) ≈ 0.001704851516268, which is +0.875558% + over R = 51 (κ < 0.0017019499). + - R = 72: a < 347355787341/(2·10^14) ≈ 0.001736778936705, which is +2.76469% + (κ < 0.0017337678; with the selected bit endpoint b, any conversion is capped at + b/(1+b) = 0.0017304275, so for R ≥ 71 a/(1+a) is valid but no longer binding). + + R = 71 is the least rank whose ceiling cell lies entirely above the selected bit + endpoint 0.001733427039589844234749. Its t_min is 25, its ceiling is + 0.001734834336053, and R = 70 gives 0.001732866531911. + +## Proof + +**(1)** S > 0 and prefix(t) is nondecreasing, so Row(t, S) is strictly increasing in t. +The admissible degrees are therefore an initial segment. The boundary rows are: + +| Reading and prefix | Row at t_max | Row at t_max + 1 | Cap | +|---|---|---|---| +| A, fixed | 3·2642 + 11185 = 19111 | 21753 | 20161 | +| A, 512·t | 19623 | 22777 | 20161 | +| B, fixed | 181·2642 + 11185 = 489387 | 492029 | 490196 | +| B, 512·t | 152·3154 + 10161 = 489569 | 492723 | 490196 | + +The bridge holds at both caps; at 490197 it fails. verify.py also checks that the +admissible set is an initial segment, by direct scan over t = 2..200. + +**(2)** For R < 73, (73/R)^t is strictly increasing in t, so the guard holds exactly +for t ≥ t_min(R). The largest admissible rank R_max(t) is therefore nondecreasing in t. +For R ≥ 73, 73^t ≤ R^t < 2R^t, so the guard fails. The boundary cases, all exact +integer comparisons: +- 2·51² = 5202 < 5329 = 73² < 5408 = 2·52². +- 2·57³ = 370386 < 389017 = 73³ < 390224 = 2·58³. +- 73^50 ≤ 2·72^50 and 73^51 > 2·72^51. + +An implementation cross-check computes every t_min(R), R = 1..72, by iterating the +coarse recurrence n ↦ R·⌊n/73⌋ from n₀ = 73^80, where the floors are exact. It returns +the first level with 2n_t < n₀ and agrees with the power search at every R. Since +n_t = R^t·73^(80−t) exactly for t ≤ 80, this is algebraically the same comparison: it +guards the code, not the model. + +**(3)** Row(t, S) < cap holds exactly when S ≤ S_max(t), by integer division. +verify.py checks Row(t, S_max) < cap ≤ Row(t, S_max + 1). Row is increasing in t, +so the least guard-admissible degree t_min(R) is optimal for a given R. + +**(4)** Colkitt's lemma gives the bound. A rank-r child costs (r/73)^{1−a} += r·r^{−a}·73^{a−1}, and the per-unit-mass price is non-increasing in r. So every idle +histogram with ranks ≤ R has moment at least relax_R(a): the local word plus all idle +mass I = 1646 per call placed in fractional rank-R children, divided by w = 896/9. + +- relax_R(a) is strictly increasing in a, because each term is (r/73)·e^{a·ln(73/r)} + with r < 73. +- For a > 0, relax_R(a) is strictly decreasing in R, because the idle term is + (I/73)(73/R)^a. + +The certificate relax_R(a_lo) < 1 < relax_R(a_hi), with a_hi − a_lo = 10^−15, puts the +root in one grid cell. Two enclosure methods agree on both sides at every +R = 51, …, 72: + +- **Own method.** The `decimal` module's `ln` and `exp`, which are documented as + correctly rounded, so the error is within half an ulp. Each is widened by one ulp, + and every other operation uses directed rounding at 60 digits. +- **Second method.** Colkitt's unmodified rational `child_cost` enclosures + (atanh/Taylor series, 256-bit outward rounding), aggregated independently. The guard + check in `model()` is not called. + +At R = 51 the bracket equals the unmodified `ceiling.ceiling()` and the published +`RESULT.json`. The ceilings increase strictly with R. The bit crossing is the least R +whose whole cell lies above the bit endpoint, and R = 70 is checked to be at or below +it. ∎ + +**Conditional what-if (not part of the theorem).** Reading A's R ≤ 57 depends on the +integer halving degree as the multiplier of S. `research/selected-coarse-depth-stock` +prices the same depth component with a sharper coefficient (43/26 instead of 2 at +R = 48; sharp asymptotic value 1/log2(73/R)), which it calls not an adopted complete row +bound. With the t·S term repriced as ⌈S/log2(73/R)⌉ and the other terms kept, reading A +would admit R ≤ 59 with the fixed prefix (row 19786 at R = 59, 20523 at R = 60; ++1.1501%) and R ≤ 58 with the prefix scaled by the same coefficient (row 19666 at +R = 58, 20429 at R = 59; +1.0138%). verify.py computes these at 60 digits and asserts +that no value lies near an integer tie. + +## What this does not show + +The ceilings are optimistic relaxations. They do not show that idle children of +rank > 48 can be hosted physically (the open question in #3805). They do not bind the +per-level divisor for higher-rank children beyond #3421's A = 0, B_bits = 2642 for the +selected m = 73 divisor; the leaf constant ρ stays unbound (#3113). Coarse depth is not +an extra uncharged cost: H1 charges it, conservatively, as t·S, and a sharper +coefficient could only lower the row. Native admission is not covered: it would have to +change the hard-coded t = 2 guards at `assemble.py:175` and `:191` and `ceiling.py:111`. +Reading A versus B (or C) is a contract question. The computation is exact under each +reading; source favours B, but this package does not decide it. + +The guard limits every child rank, paid or idle, so the admissibility statements of +the theorem also lift the paid-rank cap s = 51 used by the rank-shape screens (open +#3701/#3811) to 57 (A) or 72 (B). The ceilings here price only idle repacking with the +selected word's paid children fixed; the paid-rank lever above 51 is not priced. + +## Verifier checks and negative controls + +`verify.py` checks: + +1. The selected assembler `research/complex-sw4-frame8/code/{assemble,invoice_allcold}.py` + hashes to the entries of the selected source manifest + (`research/community-frontier1094-audit/SELECTED-SOURCE.json`); then 41 literal source + bindings in that code, `outer.py`, the notes and the lineage bridge files, plus the precedent arithmetic + 4·2571 = 10284 and 24·2431 = 58344. +2. The selected invoice member SHA256. It recomputes S from physical roles × group(36), + the row, router, literal and C0 bit lengths from the invoice's own fields, and the + seven invoice inequalities (primitive bound, logical, router, literal, mass, + precision, tape). +3. Guard thresholds for every R = 1..72 by integer power search, with an implementation + cross-check by the exact coarse recurrence n ↦ R·⌊n/73⌋ (algebraically the same + comparison, so it guards the code, not the model). +4. t_max for each reading and prefix, by direct scan, as an initial-segment property; + the (R, S) region; the prefix(3) ≤ 2073 threshold; the depth-six row. +5. The ceilings by the package's own decimal interval bisection (correctly rounded + ln/exp with one-ulp widening, directed rounding). At both bracket endpoints they are + cross-checked against Colkitt's unmodified rational `child_cost` enclosures. At R = 51 + the bracket must equal the unmodified `ceiling.ceiling()` and the published + `RESULT.json`. +6. The conditional sharp-coefficient what-if under A (60-digit values, asserted far from + integer ties) and the #3667 lean-row what-if under A (t_max 7 / 6, R ≤ 66 / 65). + +**Negative controls.** These 11 inputs run through the main check functions and must +fail with the stated assertion message; each did: + +| Control | Why it fails | +|---|---| +| t = 4 under A, fixed prefix | row 21753 ≥ 20161 | +| t = 4 under A, 512·t prefix | row 22777 ≥ 20161 | +| R = 58 at t = 3 | guard 390224 > 389017 | +| R = 72 at t = 50 | guard fails | +| R = 73 at t = 200 | guard can never hold for R ≥ 73 | +| t = 182 under B, fixed prefix | row 492029 ≥ 490196 | +| t = 153 under B, 512·t prefix | row 492723 ≥ 490196 | +| bridge cap + 1 (490197) | degree gap not positive | +| `row_prefix_extra` set to 0 | prefix identity (`row_prefix_extra = 2*payload`) fails | +| stock bits + 1 | invoice stock identity fails | +| physical roles doubled | invoice stock identity fails | diff --git a/research/complex-halving-degree-invoice/README.md b/research/complex-halving-degree-invoice/README.md new file mode 100644 index 0000000000..24e813a45a --- /dev/null +++ b/research/complex-halving-degree-invoice/README.md @@ -0,0 +1,267 @@ +# complex-halving-degree-invoice: halving degree of the selected complex invoice under the inherited degree-t ledger + +**Scoped finite statement, conditional on inherited hypotheses; an optimistic opening only. +No new κ, no supplier, no frontier change.** + +## Answer in three lines + +- **Question.** Every complex ceiling screen caps child ranks (idle and paid) at 51, from the + halving guard 73^t > 2R^t at halving degree t = 2. Does the selected #1094 finite + invoice force t = 2, and what is a larger t worth? +- **Bound that does not depend on the invoice.** R = 73 never meets the guard, so every + child rank, paid or idle, is ≤ 72 for every t. Its idle-cap component (the selected + word's paid children held fixed, only idle mass repacked) is worth at most + **+2.76469%** in Colkitt's ideal relaxation, whatever the row contract is. The same + guard also caps the paid ranks; that rank-shape lever above 51 is not priced here. +- **Under the inherited degree-t ledger (H1–H4 in [PROOF.md](PROOF.md)).** If only the + outer bridge binds (reading B, favoured by the inherited bridge text), t_max = 181 + (152 with a 512·t prefix) and every child rank up to 72 is admissible (from t = 51). If + the retained row 20161 binds (reading A, the fallback), t_max = 3 and every child rank + is ≤ 57 (+0.875558% from idle repacking under the integer-degree ledger). + +## Statement + +At t = 2 the selected invoice charges the row coefficient 2·2642 + 9909 + 252 + 1024 = +16469, where S = 2642 is its stock bits. Under H1 the charge at halving degree t is + +Row(t, S) = t·S + 9909 + 252 + prefix(t), + +and under H1–H4 the halving degree is limited only by this row contract: + +| Row contract | prefix(t) | t_max | Largest admissible R | Rank-56 idle bin¹ | R = 72 | +|---|---|---|---|---|---| +| B, bridge-only: Row < 490196 | 1024 (fixed) | **181** (row 489387) | **72** | admissible | yes (t ≥ 51) | +| B | 512·t | **152** (row 489569) | **72** | admissible | yes | +| A, retained-binding: Row < 20161 | 1024 | **3** (row 19111) | **57** | admissible | no | +| A | 512·t | **3** (row 19623) | **57** | admissible | no | + +¹ 56 = 8 + 16 + 32, a merge of the nine-stage route's smaller idle bins. Open #3836 +(Matarener) reports that bridge-based nine-stage schedules force the 16/32/48 alphabet, +so this bin is guard-admissible here but not realized in that schedule class. + +Reading B keeps the bridge reserve 10^6 and the factor 51/25 fixed and re-chooses the +retained coefficient up to ⌊(25·10^6 − 1)/51⌋ = 490196, where the bridge gap is 4/25 > 0. + +**Why source favours B.** The lineage bridge text that derives 20161 calls it an +overcharge: "The complex child maximum below m/2 gives halving degree1, while +log2 W<5208<10000 … A=10000+9909+252=20161 … Increasing these finite overcharges changes +constants and the all-size bridge, not the selected exponent saving" +(`research/five-stage-gen4-banks/inputs/complex/retained/FINITE_BRIDGE.txt`, section 4; +lineage evidence, outside the selected manifest). The 10000 slot is exactly where +t·S + prefix(t) must fit under A, and it was sized at halving degree 1. The +selected-manifest lineage assembler `research/direct-delivery504-global/code/assemble.py:29` +certifies the bridge at `row=max(20161, bit row, physical row)`, treating 20161 as a +floor. Counter-evidence for A: the selected assembler also asserts the bit row +`<20161` (`assemble.py:204`), the invoice emits `retained_row_coefficient=20161` +(`invoice_allcold.py:307`), and the lineage invoices keep a strict `row<20161`; under B +these stay satisfied because K ≥ 20161. The outer engine consumes the bridge only as +the positivity slack `row_product_gap=bridge['rows']['degree_gap']` +(`research/contextual-provider-pooling/engines/outer.py:45`), not as a κ margin. The +lineage calls 20161 a "retained … allowance" +(`research/contextual-provider-pooling/docs/PRIOR-TN27-README.md:21`). An earlier assembly +in the same bridge lineage charges row 20445 at halving degree 4 against its own reserve +70000 (`notes/paired-cube-assembly.tex`), so reserves and allowances are chosen per +assembly. And 51/25 is derived independently of t +(`notes/structured-bulk-assembly.tex`). Reading A keeps this replay's pinned constant. +Reading A admits t = 3 for any prefix(3) ≤ 2073, so its t_max = 3 holds for every prefix +form with that property (a superlinear form such as 256·t² would give 2). + +A child rank R is admissible exactly when t_min(R) ≤ t_max, where t_min(R) is the least +t with 73^t > 2R^t: t_min(51) = 2, t_min(57) = 3, t_min(58) = 4, t_min(71) = 25, +t_min(72) = 51. For general stock, (R, S) is admissible exactly when +S ≤ ⌊(cap − 1 − 10161 − prefix(t))/t⌋ with t = t_min(R); RESULT.json tabulates this for +R ∈ {48, 51, 52, 56, 57, 58, 64, 68, 71, 72}. + +**Ideal ceilings.** Colkitt's packing relaxation of the selected local word, with idle +ranks allowed up to R: + +| R | t_min | a_ceiling (certified to a 10^−15 grid cell) | κ ≤ a/(1+a) | κ cap with the bit endpoint | gain over R = 51 | +|---|---|---|---|---|---| +| 51 | 2 | 0.001690054109089 (published value, reproduced) | 0.001687202645325402 | same | — | +| 57 | 3 | 0.001704851516268 | 0.001701949944324806 | same | +0.875558% | +| 72 | 51 | 0.001736778936705 | 0.001733767765368969 | 0.001730427469823603 | +2.76469% | + +a/(1+a) is an upper bound in all cases. For R ≥ 71 it is no longer the binding one: the +selected bit endpoint b = 0.001733427039589844234749 caps any conversion at +b/(1+b) = 0.001730427469823603. The full table for R = 51..72 is in RESULT.json and +increases strictly with R. **R = 71 (t_min = 25) is the least rank whose ceiling cell lies +above b**; the ceiling at R = 70 is 0.001732866531911. + +**Conditional what-if under reading A.** Reading A's R ≤ 57 uses the integer halving +degree as the multiplier of S (H1). `research/selected-coarse-depth-stock` prices the same +depth component more sharply (43/26 instead of 2 at R = 48; sharp asymptotic coefficient +1/log2(73/R)) and calls this "not an adopted complete row bound". Repricing the t·S term +at the sharp coefficient, other terms kept, would admit R ≤ 59 under A with the fixed +prefix (row 19786; +1.1501%, ceiling 0.001709491591784) and R ≤ 58 with the prefix scaled +likewise (row 19666; +1.0138%). So reading A's cap depends on the ledger; it is not an +upper bound on every repricing. + +What this decides: + +- R = 51 is not forced by the invoice under either reading (given H1–H4). +- Under B (or C, below), R = 72 is admissible. The ideal lever is +2.76469%, and from + R = 71 this relaxation no longer forces the complex side to bind. +- Under A, the integer-degree ledger gives +0.875558% (R ≤ 57), or up to +1.1501% with the + conditional sharper depth pricing. The complex ceiling stays below b. +- The guard caps every child rank, not only idle ones. The rank-shape screens of open + #3701 and #3811 stop at paid cap s = 51 because of this same t = 2 guard; under H1–H4 + the cap becomes 57 (A) or 72 (B). In their relaxation (all local and idle mass at rank + s) a same-loop AI review computation (not asserted by verify.py) gives 0.013675 at s = 51, 0.019823 at s = 57 and an + uninformative 0.3556 at s = 72, where physical hosting, not the guard, binds. That + paid-rank lever is not priced or claimed here (open question 5); the +2.76469% above is + only the idle-cap component. + +## What is new compared with predecessors + +- **philippeVV**, Discussion #2278 ([comment](https://github.com/CrocSwap/integer-mult-bounds/discussions/2278#discussioncomment-18960261), + 2026-10-15, local-only and unreviewed), stated that the guard is a convention, that + "the retained bridge degree 10^6 already admits t ≤ 181", and that the effect on this + word's ceiling is "≤ +2.8%". This package confirms his ≤ +2.8% bound exactly + (+2.76469%) under every reading, and his t ≤ 181 under reading B with a fixed prefix + (152 with a 512·t prefix). The t = 2 ledger terms were traced concurrently (below); + new here are the t-dependence of the ledger bound to the selected assembler and invoice + bytes; reading A (t_max = 3) and the source evidence for B; the exact (R, S) region; certified ceilings at every + R = 51..72; and the bit-endpoint crossing at R = 71. +- **Gonzalo-Mier**, `research/kappa010-rank-cap-floor`, open question 3, asks whether + depth six fits the row invoice. For the complex invoice: halving degree 6 gives row + 6·2642 + 11185 = 27037, which fits under B (< 490196) and fails under A (≥ 20161). + Every degree 4 ≤ t ≤ 152 fits under B, including the 17 that their complex rank-70 row + needs. The bit invoice is not evaluated here. +- **Douglas Colkitt**, `research/complex-local-word-ceiling`: the relaxation and its + rational enclosure primitives are reused unmodified, as a cross-check. Its guard check + (`ceiling.py:111`) is not called for R > 51. +- **petalas**, open #3701/#3729/#3754/#3805/#3811: ceilings and integer packings for caps + up to the guard cap 51. This package prices only the idle cap past 51. +- **Concurrent (open PRs):** #3768 (jwr404) records the same degree-gap arithmetic + (23971789/25, 141461/5, 20249.8) that this package re-asserts as precedent. #3667 + (Mainzu) traces 9909, 252 and 1024 as w-free degrees of the fixed external reserve + (support for H4) and claims, conditionally, that the 9909/252 slots are slack (lean row + 6308 at t = 2). If that were adopted, reading A would admit t = 7 with the fixed prefix + (row 19518, R ≤ 66) or t = 6 with the 512·t prefix (row 18924, R ≤ 65), still below the + R = 71 bit crossing; verify.py asserts these (`lean_row_what_if_A_3667`). #3670 and + #3766 (jwr404) record the t = 2 rows 16469 and 15555; #3766's "two selected row + readings" are row values, not this package's contract readings A/B. + +## Reproduce + +From the repository root, with the standard library only. Tested locally with Python +3.14 only. `VERIFY.json` targets 3.12, which was not available locally, so the runner's +3.12 replay was not run here. + +```sh +python3 -I -B research/complex-halving-degree-invoice/verify.py +``` + +Expected output, in under 10 s: + +``` +PASS_COMPLEX_HALVING_DEGREE_INVOICE_SCOPED {'A_retained/fixed': 3, 'A_retained/per_level': 3, 'B_bridge/fixed': 181, 'B_bridge/per_level': 152} {'51': '0.001690054109089', '57': '0.001704851516268', '72': '0.001736778936705'} 11 controls +``` + +The verifier recomputes everything and requires byte equality with +[RESULT.json](RESULT.json). `--write` regenerates the file. The six checks and the 11 +negative controls (each must fail with its stated assertion message; each did) are +listed in [PROOF.md](PROOF.md#verifier-checks-and-negative-controls). + +Outside the verifier: `-O` exits non-zero (the assertions are the checks), an unknown +argument is rejected, and a one-digit edit of RESULT.json fails the byte comparison. +The invoice binds only bit lengths, so a change that keeps every bit length (for example +`conservative_pervertex_used + 1`) is not detected. + +## Scope, inherited assumptions and unresolved obligations + +These hypotheses are inherited (see PROOF.md). They are evidenced from source but not +proved here: + +- **H1.** The finite-cover transfer can be instantiated at halving degree t with ledger + t·S + 10161 + prefix(t). The lineage's notes do this at t = 4 and t = 24 with the same + 9909 + 252, and #3421 (VictorLiwentao) proves the per-level stock shape A = 0 with + B_bits = 2642 for the m = 73 divisor, so S is the per-level allowance. The + degree-genericity of the written transfer proof is not re-proved. +- **H2.** prefix(t) is fixed (1024) or 512·t; source does not settle which. +- **H3.** Reading B (bridge-only, favoured by source) or reading A (retained-binding). + A third reading, C, is recorded but not used for any number: the reserve exponent is + itself chosen per assembly (70000, 108000, 160000 in the notes; 10^6 here), and then + the row invoice gives no finite cap. +- **H4.** The other finite checks do not depend on t. The square in router and literal + is the W² exchange count of a W-role permutation, kept at degree 24; C0 = 32·m_c·B² is + kept at degree 4; the bootstrap cutoff max(⌈36/gap²⌉, ⌈2(4+512)/gap⌉) is + self-adjusting. + +The following costs are unknown, not zero: + +- physical hosting of idle children of rank > 48 (#3805 leaves 49–51 open); +- the per-level divisor and stock for higher-rank children: #3421 binds A = 0 and + B_bits = 2642 for the selected m = 73 divisor, and the leaf constant ρ stays unbound + (#3113; selected-coarse-depth-stock open question 1). Coarse depth itself is not an + extra cost: H1 already charges it, conservatively, as t·S; +- native admission, including the hard-coded t = 2 guards at + `complex-sw4-frame8/code/assemble.py:175` and `:191` and `ceiling.py:111`; +- any change to the staged544 template. + +The ceilings are relaxations: they bound what repacking this local word could reach, +and they are not achievable values. This package admits nothing and does not change the +selected frontier. + +## Open next questions + +1. **Does the retained row coefficient 20161 bind, or only the bridge (reading A versus + B or C)?** Source favours B (above): the derivation of 20161 as a degree-1 overcharge + is known (FINITE_BRIDGE section 4), and lineage assemblers certify the bridge at + max(20161, rows). What remains is whether the selected transfer proof inherits the + section-4 "overcharge" clause, or the invoices' strict `row<20161` is a contract. + Blocker: a contract decision. +2. **Is `row_prefix_extra` fixed or proportional to t?** It changes t_max under B from + 181 to 152, but not the R = 72 conclusion. Weak evidence for 512·t: the selected + assembler names the bit side's 512 charge `charged_two_level_coefficient_bits` + (`assemble.py:204`). First step: trace `2*payload` to the PR582 plain-joint-prefix + construction. +3. **Can idle children of rank 71 or 72 be hosted, and what do ρ and the per-level + divisor cost there?** This is where the bit side could start to bind. A sharper depth + coefficient would be a row saving (it could raise reading A's cap to 58–59), not a + cost. Blocked by #3805 (physical hosting) and ρ (#3113 / #3421). +4. **Bit-side analogue.** Does the bit invoice (m = 64) admit the halving degrees that + the kappa010 bit rows need (t = 15 for rank 61)? First step: bind the bit row ledger + the same way. +5. **Paid caps 52–72.** The same guard limits paid child ranks. What do the rank-shape + screens of #3701/#3811 (open) give at paid caps s = 52..72, with physical hosting + (#3805) and stock/depth repricing charged? First step: rerun their screens with the + cap lifted to 57 (A) and to 72 (B). + +## Sources and credit + +- Base commit `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6. Exact Git + blobs and SHA256 values of every input are in [SOURCES.json](SOURCES.json). +- The selected invoice is the tar member `candidate/strict/global/audit/PREFIX-AND-INVOICE.json` + of the #1094 replay (rohanarun), SHA256 `212cf4ee3b16081bf66f300fa18b4070d25c17210c21c78c2967892c91870d12`. +- The ledger formula and contracts are in the selected assembler + `research/complex-sw4-frame8/code/` (PR741 by chafreaky; inherited authors credited + in its PROVENANCE.md): `invoice_allcold.py:263,271-283,297` and + `assemble.py:159,173,175,191,210,213`. The selected record's source chain includes + PR1087 by jeremykothe2. +- Precedents: `notes/paired-cube-assembly.tex`, `notes/three-stage-cover-assembly.tex`, + `notes/three-stage-cover-rows.tex`, `notes/structured-bulk-assembly.tex`, all by + icekylinx. DaysSky's closed PR375 (halving degree two, raised from one) is the earliest + explicit statement of the degree-t ledger (row term t·log2 W, recursion depth + t·⌈log2 n⌉) that H1 relies on. `FINITE_BRIDGE.txt` (five-stage-gen4-banks lineage) and + `research/direct-delivery504-global` are cited as lineage evidence for reading B. +- Predecessors: + - philippeVV: the halving-guard note in Discussion #2278. + - Gonzalo-Mier: kappa010-rank-cap-floor, open question 3. + - Sricharan Vagvala (@theon199): selected-coarse-depth-stock. + - VictorLiwentao: #3421, selected-stock-shape-a-zero. + - Douglas Colkitt: complex-local-word-ceiling. + - Dugongue: contextual-provider-pooling (PR563; `outer.py` and the PRIOR-TN27 README, + from the PR552 lineage), integrated by Douglas Colkitt. + - DaysSky: closed PR375 (degree-t ledger generalization). + - navinor: #3113. + - petalas: #3701/#3729/#3754/#3805/#3811. + - Concurrent (open PRs): jwr404 (#3768, #3670, #3766), Mainzu (#3667), Matarener + (#3836). + +No predecessor file was modified. + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Claude chose the method, wrote verify.py and drafted this +README and PROOF.md. Reviewed by seven independent AI review passes (two rounds) in the same +loop; no human has reviewed it. Apache-2.0. diff --git a/research/complex-halving-degree-invoice/RESULT.json b/research/complex-halving-degree-invoice/RESULT.json new file mode 100644 index 0000000000..206ae4bf63 --- /dev/null +++ b/research/complex-halving-degree-invoice/RESULT.json @@ -0,0 +1,292 @@ +{ + "A_admits_t3_for_any_prefix3_at_most": 2073, + "bit_endpoint_crossing": { + "bit_lower_decimal": "0.001733427039589844234749", + "ceiling_at_that_R": "0.001734834336053", + "ceiling_one_rank_below": "0.001732866531911", + "kappa_cap_from_bit_endpoint_decimal": "0.001730427469823603", + "least_R_with_ceiling_above_bit": 71, + "least_degree": 25 + }, + "bridge_gap_at_B_cap": "4/25", + "caps": { + "A_retained": 20161, + "B_bridge": 490196 + }, + "ceiling_by_rank": { + "51": "0.001690054109089", + "52": "0.001692619193708", + "53": "0.001695142891664", + "54": "0.00169762664321", + "55": "0.001700071812802", + "56": "0.001702479694395", + "57": "0.001704851516268", + "58": "0.001707188445454", + "59": "0.001709491591784", + "60": "0.001711762011617", + "61": "0.001714000711256", + "62": "0.001716208650103", + "63": "0.001718386743558", + "64": "0.001720535865708", + "65": "0.0017226568518", + "66": "0.001724750500536", + "67": "0.001726817576207", + "68": "0.001728858810655", + "69": "0.001730874905114", + "70": "0.001732866531911", + "71": "0.001734834336053", + "72": "0.001736778936705" + }, + "ceilings": { + "51": { + "a_ceiling": "1690054109089/1000000000000000", + "a_ceiling_decimal": "0.001690054109089", + "kappa_upper_bound_decimal": "0.001687202645325402", + "kappa_upper_bound_with_bit_cap_decimal": "0.001687202645325402", + "least_degree": 2 + }, + "57": { + "a_ceiling": "426212879067/250000000000000", + "a_ceiling_decimal": "0.001704851516268", + "gain_over_R51_percent": "0.875558", + "kappa_upper_bound_decimal": "0.001701949944324806", + "kappa_upper_bound_with_bit_cap_decimal": "0.001701949944324806", + "least_degree": 3 + }, + "72": { + "a_ceiling": "347355787341/200000000000000", + "a_ceiling_decimal": "0.001736778936705", + "gain_over_R51_percent": "2.76469", + "kappa_upper_bound_decimal": "0.001733767765368969", + "kappa_upper_bound_with_bit_cap_decimal": "0.001730427469823603", + "least_degree": 51 + } + }, + "controls": [ + "reading_A_t4", + "reading_A_per_level_t4", + "guard_R58_t3", + "guard_R72_t50", + "guard_R73_t200", + "reading_B_t182", + "reading_B_per_level_t153", + "bridge_cap_plus_one", + "prefix_mutation", + "stock_bits_mutation", + "physical_mutation" + ], + "depth6_row_fixed_prefix": { + "fits_A": false, + "fits_B": true, + "row": 27037 + }, + "idle_mass_per_call": 1646, + "invoice_independent": { + "R_max_any_degree": 72, + "note": "R <= 72 for every t and every child rank, paid or idle: R = 73 never meets the guard. The ceilings price only idle repacking of the fixed selected word." + }, + "lean_row_what_if_A_3667": { + "A_retained/fixed": { + "R_max": 66, + "row_at_t_max": 19518, + "t_max": 7 + }, + "A_retained/per_level": { + "R_max": 65, + "row_at_t_max": 18924, + "t_max": 6 + } + }, + "least_degree_by_rank": { + "48": 2, + "49": 2, + "50": 2, + "51": 2, + "52": 3, + "53": 3, + "54": 3, + "55": 3, + "56": 3, + "57": 3, + "58": 4, + "59": 4, + "60": 4, + "61": 4, + "62": 5, + "63": 5, + "64": 6, + "65": 6, + "66": 7, + "67": 9, + "68": 10, + "69": 13, + "70": 17, + "71": 25, + "72": 51 + }, + "ledger": "Row(t,S) = t*S + 10161 + prefix(t); prefix fixed = 1024 or per_level = 512*t", + "local_word": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + }, + "r_max_by_degree": { + "10": 68, + "152": 72, + "16": 69, + "181": 72, + "2": 51, + "25": 71, + "3": 57, + "4": 61, + "5": 63, + "50": 71, + "51": 72, + "6": 65, + "8": 66 + }, + "readings": { + "A_retained/fixed": { + "R72_admissible": false, + "R_max": 57, + "cap": 20161, + "rank56_idle_admissible": true, + "row_at_t_max": 19111, + "row_at_t_max_plus_1": 21753, + "t_max": 3 + }, + "A_retained/per_level": { + "R72_admissible": false, + "R_max": 57, + "cap": 20161, + "rank56_idle_admissible": true, + "row_at_t_max": 19623, + "row_at_t_max_plus_1": 22777, + "t_max": 3 + }, + "B_bridge/fixed": { + "R72_admissible": true, + "R_max": 72, + "cap": 490196, + "rank56_idle_admissible": true, + "row_at_t_max": 489387, + "row_at_t_max_plus_1": 492029, + "t_max": 181 + }, + "B_bridge/per_level": { + "R72_admissible": true, + "R_max": 72, + "cap": 490196, + "rank56_idle_admissible": true, + "row_at_t_max": 489569, + "row_at_t_max_plus_1": 492723, + "t_max": 152 + } + }, + "region_by_child_rank": { + "48": { + "S_max[A_retained/fixed]": 4487, + "S_max[A_retained/per_level]": 4487, + "S_max[B_bridge/fixed]": 239505, + "S_max[B_bridge/per_level]": 239505, + "least_degree": 2 + }, + "51": { + "S_max[A_retained/fixed]": 4487, + "S_max[A_retained/per_level]": 4487, + "S_max[B_bridge/fixed]": 239505, + "S_max[B_bridge/per_level]": 239505, + "least_degree": 2 + }, + "52": { + "S_max[A_retained/fixed]": 2991, + "S_max[A_retained/per_level]": 2821, + "S_max[B_bridge/fixed]": 159670, + "S_max[B_bridge/per_level]": 159499, + "least_degree": 3 + }, + "56": { + "S_max[A_retained/fixed]": 2991, + "S_max[A_retained/per_level]": 2821, + "S_max[B_bridge/fixed]": 159670, + "S_max[B_bridge/per_level]": 159499, + "least_degree": 3 + }, + "57": { + "S_max[A_retained/fixed]": 2991, + "S_max[A_retained/per_level]": 2821, + "S_max[B_bridge/fixed]": 159670, + "S_max[B_bridge/per_level]": 159499, + "least_degree": 3 + }, + "58": { + "S_max[A_retained/fixed]": 2243, + "S_max[A_retained/per_level]": 1987, + "S_max[B_bridge/fixed]": 119752, + "S_max[B_bridge/per_level]": 119496, + "least_degree": 4 + }, + "64": { + "S_max[A_retained/fixed]": 1495, + "S_max[A_retained/per_level]": 1154, + "S_max[B_bridge/fixed]": 79835, + "S_max[B_bridge/per_level]": 79493, + "least_degree": 6 + }, + "68": { + "S_max[A_retained/fixed]": 897, + "S_max[A_retained/per_level]": 487, + "S_max[B_bridge/fixed]": 47901, + "S_max[B_bridge/per_level]": 47491, + "least_degree": 10 + }, + "71": { + "S_max[A_retained/fixed]": 359, + "S_max[A_retained/per_level]": 0, + "S_max[B_bridge/fixed]": 19160, + "S_max[B_bridge/per_level]": 18689, + "least_degree": 25 + }, + "72": { + "S_max[A_retained/fixed]": 175, + "S_max[A_retained/per_level]": 0, + "S_max[B_bridge/fixed]": 9392, + "S_max[B_bridge/per_level]": 8900, + "least_degree": 51 + } + }, + "scope": "Scoped finite invoice statement under inherited PR1087-lineage transfer/bridge hypotheses; optimistic relaxation; admits nothing; no supplier, no kappa, no frontier change.", + "selected_invoice": { + "literal_bits": 35284, + "member": "candidate/strict/global/audit/PREFIX-AND-INVOICE.json", + "physical": 14826, + "physical_row": 16469, + "required_C0_bits": 200012, + "retained_row": 20161, + "router_bits": 7988, + "row_prefix_extra": 1024, + "sha256": "212cf4ee3b16081bf66f300fa18b4070d25c17210c21c78c2967892c91870d12", + "stock_bits": 2642 + }, + "sharp_depth_coefficient_what_if_A": { + "A_retained/fixed": { + "R_max": 59, + "ceiling": "0.001709491591784", + "gain_over_R51_percent": "1.1501", + "row_at_R_max": 19786, + "row_at_R_max_plus_1": 20523 + }, + "A_retained/per_level": { + "R_max": 58, + "ceiling": "0.001707188445454", + "gain_over_R51_percent": "1.0138", + "row_at_R_max": 19666, + "row_at_R_max_plus_1": 20429 + } + }, + "source_bindings_checked": 41, + "status": "PASS_COMPLEX_HALVING_DEGREE_INVOICE_SCOPED" +} diff --git a/research/complex-halving-degree-invoice/SOURCES.json b/research/complex-halving-degree-invoice/SOURCES.json new file mode 100644 index 0000000000..02ab3dcfb1 --- /dev/null +++ b/research/complex-halving-degree-invoice/SOURCES.json @@ -0,0 +1,114 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "notes/paired-cube-assembly.tex", + "usage": "input", + "git_blob": "d44227eb55ab68b9d04ea661bbe486fea66182d4", + "sha256": "45f28775ebf36338df9312957fd09af3c635690acc02ae3d60431ccd16fb46c3" + }, + { + "path": "notes/structured-bulk-assembly.tex", + "usage": "input", + "git_blob": "9bd11d88d201d6aa7b110bc169648d928c3a9c14", + "sha256": "048c67f6473ee4712d37033266a2e507dee9dcd2bb3b0fd177708100e2404d94" + }, + { + "path": "notes/three-stage-cover-assembly.tex", + "usage": "input", + "git_blob": "983ffb6ac8fb9117360cd0797c00c05dfa071c9d", + "sha256": "ccf34a6d37c4af14bebeab15be50ab204eb1caebe546385520050ec30089441d" + }, + { + "path": "notes/three-stage-cover-rows.tex", + "usage": "input", + "git_blob": "590da4b892a08b9d5182fb3d8a983c6239dd27db", + "sha256": "6ad97a5cd7d6aecf978a81226e1c2763d37840caca130c61f3bf5c4ac111c5c8" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/INDEPENDENT1094.json", + "usage": "input", + "git_blob": "009a385e26858058a18188364078d162aa6f9519", + "sha256": "301fb8a0e4ab7e3c383ff974c54c08178283b2a3453c5282757f692a3c7a4bfd" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/complex-local-word-ceiling/RESULT.json", + "usage": "input", + "git_blob": "77f55043a679dd722330f1e2499863e36376d9f9", + "sha256": "d91d6c46509875abf1f61de67c2609656d3dc685451299f83caa6f922493692d" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + }, + { + "path": "research/complex-sw4-frame8/code/assemble.py", + "usage": "input", + "git_blob": "2e098cabbd09edcca56780469b083385b1bc365e", + "sha256": "bb32035aefe575da3335da4e907553e2e6fdca0a0f997db569cab651c2ddb008" + }, + { + "path": "research/complex-sw4-frame8/code/invoice_allcold.py", + "usage": "input", + "git_blob": "b244cd59940659465c07b013ebe3225077496f45", + "sha256": "141bd2fd58bbfb5b8d0fc8f56f61c45586d5608a5af3487c6b883dd987f998ec" + }, + { + "path": "research/contextual-provider-pooling/docs/PRIOR-TN27-README.md", + "usage": "input", + "git_blob": "71aaed09f42a5782ed00788870bb09edac4a9555", + "sha256": "1c5c8a75542d2ee33efd600f3695253db63b38f810fda865d8b7c669d762be29" + }, + { + "path": "research/contextual-provider-pooling/engines/outer.py", + "usage": "input", + "git_blob": "43007488ad2c43187c77cc6798beff8b1cd76ad2", + "sha256": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c" + }, + { + "path": "research/direct-delivery504-global/code/assemble.py", + "usage": "input", + "git_blob": "a234aecb14de159247809af1120fedc1aab20df9", + "sha256": "71b4cbbbc5acdfe06ac67879cf54ea761e29e52143af1cd8410ad672a5cc190b" + }, + { + "path": "research/five-stage-gen4-banks/inputs/complex/retained/FINITE_BRIDGE.txt", + "usage": "input", + "git_blob": "c1a88436113a1351f80c72bd08f6406ed5faa51d", + "sha256": "66d8f4ea8752abd89952d6674a636575a0db16e18b1c16e293f48f64242f0c46" + } + ] +} diff --git a/research/complex-halving-degree-invoice/TASK.json b/research/complex-halving-degree-invoice/TASK.json new file mode 100644 index 0000000000..6bc201ae7f --- /dev/null +++ b/research/complex-halving-degree-invoice/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "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": "changed", + "actual_scope": "For the selected #1094 complex finite invoice, under the inherited degree-t ledger Row(t,S) = t*S + 9909 + 252 + prefix(t) bound to the selected complex-sw4-frame8 assembler: the largest admissible halving degree t (guard 73^t > 2R^t) under two row-contract readings (B, bridge-only and favoured by source: 10^6 - (51/25)K > 0; A, retained-binding fallback: Row < 20161) and two prefix readings (fixed 1024 or 512t); the exact admissible (R, S) region; the ideal local-word packing ceilings with idle ranks up to R for R = 51..72 (named: 51, 57, 72), the least R whose ceiling exceeds the selected bit endpoint, and a conditional sharper-depth-coefficient what-if under A. No supplier, no kappa.", + "scope_change_reason": "The card's allowed variation says: if the guard changes, \"derive an applicable fully charged replacement bound\" instead of applying the incumbent ceiling outside its scope. This package gives the guard ledger plus an ideal, not fully charged, ceiling. Every complex ceiling screen fixes R = 51 via the t = 2 halving guard; whether that is an invoice consequence or a convention decides how much the guard lever is worth. The question was raised as a local-only, unreviewed note by philippeVV (#2278) and left open in kappa010-rank-cap-floor OQ3. The card's two-unpaid-coordinate premise is not studied.", + "bottleneck_link": "The complex primitive binds. Every child rank, paid or idle, is <= 72 for every halving degree; the idle-cap component (selected word's paid children fixed) is at most +2.76469% ideal whatever the row contract. Under the inherited ledger: R <= 72 (t_max 181/152) if only the bridge binds (favoured by source); R <= 57 (+0.875558%) if the retained row 20161 binds, or R <= 59 (+1.1501%) with a conditional sharper depth coefficient. From R = 71 the relaxation no longer forces the complex side to bind. The same guard caps the paid ranks: the rank-shape screens' cap s = 51 (#3701/#3811, open) is this t = 2 guard, and A or B lifts it to 57 or 72; that paid-rank lever is not priced here.", + "budget_minutes": 60, + "stop_rule": "Stop after binding every t-dependent invoice term, exact t_max under both readings and prefixes, the (R, S) region and the ceilings; if source does not settle reading A versus B, ship both. No kappa, no supplier, no re-tabulation of the cap tables up to 51.", + "outcome": "completed", + "evidence": "RESULT.json: t_max = 181 (B, fixed prefix), 152 (B, 512t prefix), 3 (A, both prefixes; any prefix(3) <= 2073); R_max 72 (B) / 57 (A); conditional sharp-coefficient what-if under A: R <= 59 fixed / 58 scaled prefix (+1.1501% / +1.0138%); ceilings a < 0.001690054109089 (R=51, reproduced), 0.001704851516268 (R=57), 0.001736778936705 (R=72); bit-endpoint kappa cap 0.001730427469823603; least R with ceiling above bit endpoint = 71 (t_min 25); depth-six row 27037 (fits B, fails A); conditional #3667 lean-row what-if under A: t_max 7 / 6, R <= 66 / 65 (below the R = 71 crossing); 41 source bindings with the selected assembler hashed against SELECTED-SOURCE.json; 11 negative controls with expected failure reasons; ceilings checked by two methods, guard thresholds by power search plus an implementation cross-check.", + "author": "Sagar Thakrar (thakrarsagar)", + "ai_assistance": "Substantial: Claude (Anthropic, Claude Opus 5.5) bound the sources, chose the method, wrote verify.py and drafted README.md and PROOF.md. Reviewed by seven independent AI review passes (two rounds) in the same loop; no human has reviewed it.", + "open_questions": [ + { + "question": "Does the retained row coefficient 20161 bind, or only the bridge (reading A versus B/C)?", + "why_it_matters": "It decides between R <= 72 (+2.76469% ideal, bit-crossing from R = 71) and R <= 57 (+0.875558%; up to R <= 59 with a sharper depth coefficient). Source favours B: outer.py uses degree_gap only as a positivity slack.", + "first_step": "Decide whether the selected transfer proof inherits the FINITE_BRIDGE section-4 'overcharge' clause (20161 = 10000 + 9909 + 252 sized at halving degree 1; lineage assemblers certify the bridge at max(20161, rows)), or whether the invoices' strict row < 20161 is a contract.", + "blocked_by": "A contract decision, not a computation." + }, + { + "question": "Is row_prefix_extra = 2*payload fixed or proportional to the halving degree?", + "why_it_matters": "It moves t_max under reading B from 181 to 152 (not the R = 72 conclusion).", + "first_step": "Trace 2*payload to the PR582 plain-joint-prefix construction.", + "blocked_by": "None known." + }, + { + "question": "Can idle children of rank 71-72 be hosted, and what do the leaf constant rho and the per-level divisor cost there?", + "why_it_matters": "That is where the complex ceiling first exceeds the current bit endpoint. A sharper depth coefficient is a row saving (it could raise reading A's cap to 58-59), not a cost.", + "first_step": "Bind rho for the m = 73 divisor on top of #3421's A = 0, B_bits = 2642, then check hosting above rank 48.", + "blocked_by": "#3805 (physical hosting above 48) and rho (#3113 / #3421)." + }, + { + "question": "Does the bit invoice (m = 64) admit the depths the kappa010 bit rows need (t = 15 for rank 61)?", + "why_it_matters": "It is the bit-side counterpart of this guard lever.", + "first_step": "Bind the bit row ledger the same way.", + "blocked_by": "None known." + }, + { + "question": "What do the rank-shape screens give at paid caps s = 52..72?", + "why_it_matters": "The halving guard caps paid ranks too; under A or B the paid cap rises from 51 to 57 or 72, and in the #3701/#3799 relaxation a(s) goes from 0.013675 (s = 51) to 0.019823 (s = 57).", + "first_step": "Rerun the #3701/#3811 screens with the cap lifted to 57 and 72, charging physical hosting (#3805) and stock/depth repricing.", + "blocked_by": "#3805 (physical hosting above 48)." + } + ] +} diff --git a/research/complex-halving-degree-invoice/VERIFY.json b/research/complex-halving-degree-invoice/VERIFY.json new file mode 100644 index 0000000000..9e39f252fb --- /dev/null +++ b/research/complex-halving-degree-invoice/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "notes/paired-cube-assembly.tex", + "notes/structured-bulk-assembly.tex", + "notes/three-stage-cover-assembly.tex", + "notes/three-stage-cover-rows.tex", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/community-frontier1094-audit/INDEPENDENT1094.json", + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/complex-local-word-ceiling/RESULT.json", + "research/complex-local-word-ceiling/ceiling.py", + "research/complex-sw4-frame8/code/assemble.py", + "research/complex-sw4-frame8/code/invoice_allcold.py", + "research/contextual-provider-pooling/docs/PRIOR-TN27-README.md", + "research/contextual-provider-pooling/engines/outer.py", + "research/direct-delivery504-global/code/assemble.py", + "research/five-stage-gen4-banks/inputs/complex/retained/FINITE_BRIDGE.txt" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "41 source bindings (selected complex-sw4-frame8 assembler hashed against SELECTED-SOURCE.json; lineage FINITE_BRIDGE section 4 and direct-delivery504-global bridge row); selected invoice member hash and recomputed S/row/router/literal/C0/logical/primitive bounds; guard thresholds by power search plus an implementation cross-check; exact t_max per reading/prefix; (R,S) region; ceilings R=51..72 by own decimal intervals cross-checked with unmodified child_cost and ceiling.ceiling at R=51; conditional sharp-depth-coefficient and #3667 lean-row what-ifs under A; RESULT.json byte match; 11 negative controls with expected failure reasons" + } + ] +} diff --git a/research/complex-halving-degree-invoice/verify.py b/research/complex-halving-degree-invoice/verify.py new file mode 100644 index 0000000000..1a6a3c20ca --- /dev/null +++ b/research/complex-halving-degree-invoice/verify.py @@ -0,0 +1,476 @@ +#!/usr/bin/env python3 +"""Halving degree of the selected complex finite invoice under the inherited degree-t ledger: +exact t_max, the admissible (child rank R, stock bits S) region, and ideal local-word +ceilings at R = 51, 57, 72. + +Scoped finite statement under inherited hypotheses (see PROOF.md). No kappa, no supplier. +usage: verify.py [--write] (default: recompute and require byte equality with RESULT.json) +Sagar Thakrar (thakrarsagar), with substantial AI assistance from Claude (Anthropic, +Claude Opus 5.5). Apache-2.0. +""" +import hashlib, json, sys, tarfile +from decimal import Decimal as D, Context, ROUND_FLOOR, ROUND_CEILING, ROUND_HALF_EVEN +from fractions import Fraction as Q +from pathlib import Path + +if not __debug__: + raise SystemExit('run without -O: assertions are the checks') +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +M = 73 # complex parent dimension (assemble.py halving 73*73) +SEL = 'research/complex-sw4-frame8/code/' # selected assembler (SELECTED-SOURCE.json manifest) +RETAINED = 20161 # assemble.py:159 retained_row_coefficient +RESERVE, FACTOR = 10 ** 6, Q(51, 25) # assemble.py:213 degree_gap = 10**6 - (51/25)*20161 +BIT_RESERVES = 9909 + 252 # invoice_allcold.py:278; notes/*-assembly.tex +PAYLOAD = 512 # invoice_allcold.py:263 payload=512 +INVOICE = 'candidate/strict/global/audit/PREFIX-AND-INVOICE.json' +INVOICE_SHA = '212cf4ee3b16081bf66f300fa18b4070d25c17210c21c78c2967892c91870d12' +FAMILIES, STAGES, CENTRE = 2 * 4 * 112, 9, 64 # complex-local-word-ceiling model +T_RANGE = range(2, 201) + + +def text(rel): + return (ROOT / rel).read_text() + + +def bind_sources(): + """Every t-dependent invoice term, bound to literal pinned source text.""" + manifest = json.loads(text(json.loads(text('certificates/selected-result.json'))['source_manifest'])) + for f in ('assemble.py', 'invoice_allcold.py'): + want = manifest['files'].get(SEL + f) + assert hashlib.sha256((ROOT / SEL / f).read_bytes()).hexdigest() == want, f'{f} is not the selected source' + need = { + SEL + 'invoice_allcold.py': [ + 'row=2*stock.bit_length()+9909+252+2*payload', + 'used=max(rebased,parent_pervertex); retained=None; payload=512', + 'half=m//2; group=2**(half*half)', + 'for i in range(1,half+1): group*=2**(2*i)-1', + 'stock,streamed_mass=group*physical,group*mass', + 'logical=group*used+64; router=compiler*(logical+1)*(stock+1)**2', + 'literal=2*g_bound*stock**2+8*streamed_mass+4*stock+4+32*m', + 'tape=2*total_mass+182*maxchild*maxchild)', + 'inequalities=dict(local_primitive_bound=primitive_bound<2**48,', + 'logical=logical<2**6050,router=router2*48*48)", + "'rows':{'degree_gap':Q(10**6)-Q(51*20161,25)}", + 'precision=32*73*total_mass*total_mass<2**210000', + 'cut=max(ceil(36/gap**2),ceil(2*(4+512)/gap))', + 'and m*m>2*max(h)**2', + "bit['bit']['two_level_coefficient_bits']0.', + 'Thus the fixed external reserve $p^{70000}$ suffices.', + 'A full $W$-role permutation costs at most $W^2$ elementary exchanges;', + 'E=64(W+m_c+G+1)^3,\\quad B=s+E,\\quad C_0=32m_cB^2.'], + 'notes/three-stage-cover-assembly.tex': [ + 'The least halving degree for $70\\to68$ is 24, contributing 58,344.', + '58344+9909+252=68505,\\qquad', '160000-\\frac{51}{25}\\,68505=20249.8>0.', + 'A fixed role permutation has at most $W^2$ elementary exchanges; the', + ' 2GW^2+8s+4W+4+32m_c RETAINED + assert least_degree(70, 68) == 24 and 24 * 2431 == 58344 and 58344 + BIT_RESERVES == 68505 + assert 70000 - FACTOR * 20445 == Q(141461, 5) and 160000 - FACTOR * 68505 == Q(202498, 10) + return sum(len(v) for v in need.values()) + + +def least_degree(m, r): + """Least t >= 1 with m^t > 2 r^t (integer arithmetic); None if r >= m.""" + if r >= m: + return None + t = 1 + while m ** t <= 2 * r ** t: + t += 1 + return t + + +def least_degree_recurrence(m, r): + """Implementation cross-check (algebraically the same comparison): iterate the coarse recurrence n -> r*floor(n/m) from n0 = m^T (floors exact) + and return the first level t with 2*n_t < n0.""" + T = 80 + n0 = n = m ** T + for t in range(1, T + 1): + n = r * (n // m) + if 2 * n < n0: + return t + return None + + +def r_max(t): + """Largest R with 2 R^t < 73^t.""" + return max(r for r in range(1, M) if 2 * r ** t < M ** t) + + +def group(half): + g = 2 ** (half * half) + for i in range(1, half + 1): + g *= 2 ** (2 * i) - 1 + return g + + +def load_invoice(): + with tarfile.open(ROOT / 'research/community-frontier1094-audit/selected-replay.tar.gz') as tf: + raw = tf.extractfile(INVOICE).read() + assert hashlib.sha256(raw).hexdigest() == INVOICE_SHA, 'selected invoice bytes changed' + return json.loads(raw) + + +def selected_word(): + """Selected complex profile and its per-call local word (same split as complex-local-word-ceiling).""" + rec = json.loads(text('certificates/selected-result.json')) + asm = json.loads(text(rec['certificate'])) + ind = json.loads(text('research/community-frontier1094-audit/INDEPENDENT1094.json')) + H = {int(r): n for r, n in asm['complex_profile'].items()} + idle = {int(r): n for r, n in ind['owner']['idle'].items()} + N, W = ind['price']['calls'], ind['price']['live'] + assert H == {int(r): n for r, n in ind['owner']['profile'].items()} + assert N % STAGES == 0 and W == FAMILIES * (N // STAGES) + mass = sum(r * n for r, n in H.items()) + assert mass == (M - 1) * W + CENTRE * N + local = {} + for r, n in H.items(): + k = n - idle.get(r, 0) + assert k >= 0 and k % N == 0 + if k: + local[r] = k // N + return H, mass, local, Q(asm['bit_lower']), Q(asm['complex_lower']), asm['binding'] + + +def bind_invoice(inv, H, mass): + """Recompute the selected finite invoice from its own fields: S, row, router, literal, C0.""" + fin = inv['finite'] + g = group(M // 2) + stock = g * inv['physical'] + S = stock.bit_length() + assert S == fin['physical_stock_bits'], 'stock bits' + assert inv['row_prefix_extra'] == 2 * inv['charged_prefix_bits'] == 2 * PAYLOAD, 'prefix' + assert fin['physical_row_coefficient'] == 2 * S + BIT_RESERVES + inv['row_prefix_extra'], 'row identity' + assert fin['retained_row_coefficient'] == RETAINED and fin['physical_row_coefficient'] < RETAINED + assert fin['halving_integer_inequality'] == [M * M, 2 * 48 * 48] and max(H) == 48 + logical = g * inv['conservative_pervertex_used'] + 64 + router = inv['compiler'] * (logical + 1) * (stock + 1) ** 2 + literal = 2 * 2 ** 30000 * stock ** 2 + 8 * g * mass + 4 * stock + 4 + 32 * M + total = g * mass + 2 ** 100000 + assert inv['local_primitive_bound'] < 2 ** 48 and logical < 2 ** 6050 + assert router.bit_length() == fin['router_bits'] and literal.bit_length() == fin['literal_bits'] + assert (32 * M * total * total).bit_length() == fin['required_C0_bits'] + assert router < 2 ** 30000 and literal < 2 ** 100000 and total < 2 ** 100001 + assert 32 * M * total * total < 2 ** 210000 and 2 * total + 18 < 2 ** 210000 + return S + + +PREFIX = {'fixed': lambda t: 2 * PAYLOAD, 'per_level': lambda t: t * PAYLOAD} +CAP = {'A_retained': RETAINED, 'B_bridge': (25 * RESERVE - 1) // 51} + + +def row(t, S, prefix): + return t * S + BIT_RESERVES + PREFIX[prefix](t) + + +def bridge_ok(cap): + return RESERVE - FACTOR * cap > 0 + + +def check_point(t, R, S, reading, prefix, cap=None): + """Main check: guard m^t > 2R^t, physical row < retained cap, bridge positive at that cap.""" + cap = CAP[reading] if cap is None else cap + assert t >= 2 and R > 0 and S > 0 + assert M ** t > 2 * R ** t, f'guard fails at t={t}, R={R}' + assert row(t, S, prefix) < cap, f'row {row(t, S, prefix)} >= cap {cap}' + assert bridge_ok(cap), 'bridge degree_gap not positive' + return True + + +def t_max(S, reading, prefix): + ok = [t for t in T_RANGE if row(t, S, prefix) < CAP[reading]] + assert ok == list(range(2, max(ok) + 1)), 'admissible degrees are not an initial segment' + assert max(ok) < T_RANGE[-1], 'scan range too small' + return max(ok) + + +def s_max(t, reading, prefix): + """Largest S with row(t, S) < cap, i.e. S <= (cap - 1 - 10161 - prefix(t)) / t.""" + return (CAP[reading] - 1 - BIT_RESERVES - PREFIX[prefix](t)) // t + + +def sharp_row(R, S, prefix): + """Conditional what-if (not an adopted row bound): the depth component t*S repriced at the sharp + asymptotic coefficient c = 1/log2(73/R) of selected-coarse-depth-stock, other terms kept; the + per-level prefix is scaled by the same c. Returns ceil(c*S) + 10161 + prefix, exact away from ties.""" + c = EVEN.divide(EVEN.ln(D(2)), EVEN.ln(EVEN.divide(D(M), D(R)))) + terms = [EVEN.multiply(c, D(S))] + ([EVEN.multiply(c, D(PAYLOAD))] if prefix == 'per_level' else []) + for x in terms: # 60-digit value is far from an integer + assert abs(x - x.to_integral_value()) > D('1e-20') + pre = 2 * PAYLOAD if prefix == 'fixed' else int(terms[1].to_integral_value(rounding=ROUND_CEILING)) + return int(terms[0].to_integral_value(rounding=ROUND_CEILING)) + BIT_RESERVES + pre + + +# ---------- ideal ceilings: own decimal interval method (correctly rounded ln/exp + 1 ulp) ---------- +PREC = 60 +EVEN = Context(prec=PREC, rounding=ROUND_HALF_EVEN) +DN = Context(prec=PREC, rounding=ROUND_FLOOR) +UP = Context(prec=PREC, rounding=ROUND_CEILING) + + +def ln_enc(k): + v = EVEN.ln(D(k)) # documented correctly rounded => within 1/2 ulp + return EVEN.next_minus(v), EVEN.next_plus(v) + + +def cost_enc(r, a): + """Enclosure of (r/M)^(1-a) = exp((1-a)(ln r - ln M)).""" + lr, lm = ln_enc(r), ln_enc(M) + d_lo, d_hi = DN.subtract(lr[0], lm[1]), UP.subtract(lr[1], lm[0]) + oma = EVEN.subtract(D(1), a) + assert oma + a == 1 and oma > 0 + x_lo, x_hi = DN.multiply(oma, d_lo), UP.multiply(oma, d_hi) + return EVEN.next_minus(EVEN.exp(x_lo)), EVEN.next_plus(EVEN.exp(x_hi)) + + +def idle_mass(local): + total = (M - 1) * Q(FAMILIES, STAGES) + CENTRE + idle = total - sum(r * n for r, n in local.items()) + assert idle.denominator == 1 and idle > 0 + return int(idle) + + +def relax_dec(local, R, a): + lo = hi = D(0) + for r, n in sorted(local.items()): + c = cost_enc(r, a) + lo, hi = DN.add(lo, DN.multiply(D(n), c[0])), UP.add(hi, UP.multiply(D(n), c[1])) + c, I = cost_enc(R, a), idle_mass(local) + lo = DN.add(lo, DN.divide(DN.multiply(D(I), c[0]), D(R))) + hi = UP.add(hi, UP.divide(UP.multiply(D(I), c[1]), D(R))) + return (DN.divide(DN.multiply(lo, D(STAGES)), D(FAMILIES)), + UP.divide(UP.multiply(hi, D(STAGES)), D(FAMILIES))) + + +def ceiling_dec(local, R, digits=15): + """Unique grid cell [j, j+1] * 10^-digits with relax(lo) < 1 < relax(hi).""" + a = lambda j: D(j).scaleb(-digits) + lo, hi = 0, 5 * 10 ** (digits - 2) # [0, 1/20] + assert relax_dec(local, R, a(lo))[1] < 1 < relax_dec(local, R, a(hi))[0] + while hi - lo > 1: + mid = (lo + hi) // 2 + v = relax_dec(local, R, a(mid)) + if v[1] < 1: + lo = mid + elif v[0] > 1: + hi = mid + else: + raise AssertionError('decimal enclosure too wide') + return Q(lo, 10 ** digits), Q(hi, 10 ** digits) + + +def relax_colkitt(C, local, R, a): + """Second method: unmodified rational enclosures C.child_cost, own aggregation (no guard call).""" + lo = hi = Q(0) + for r, n in local.items(): + c = C.child_cost(r, M, a) + lo, hi = lo + n * c[0], hi + n * c[1] + c, k = C.child_cost(R, M, a), Q(idle_mass(local), R) + w = Q(FAMILIES, STAGES) + return (lo + k * c[0]) / w, (hi + k * c[1]) / w + + +def dec(x, n=16): + x = Q(x) + return str(Context(prec=n).divide(D(x.numerator), D(x.denominator))) + + +def main(): + nbind = bind_sources() + inv = load_invoice() + H, mass, local, bit_lower, complex_lower, binding = selected_word() + assert binding == 'complex' and complex_lower < bit_lower + S = bind_invoice(inv, H, mass) + assert S == 2642 and inv['finite']['physical_row_coefficient'] == 16469 + # Guard thresholds by two methods, every child rank below m. + tmin = {} + for r in range(1, M): + t1, t2 = least_degree(M, r), least_degree_recurrence(M, r) + assert t1 == t2, f'guard threshold disagreement at R={r}' + tmin[r] = t1 + assert least_degree(M, M) is None + assert tmin[48] == tmin[51] == 2 and tmin[52] == tmin[56] == tmin[57] == 3 and tmin[58] == 4 + assert tmin[72] == 51 and M ** 50 <= 2 * 72 ** 50 and M ** 51 > 2 * 72 ** 51 + rmax = {t: r_max(t) for t in T_RANGE} + assert all(rmax[t] <= rmax[t + 1] for t in range(2, 200)) and rmax[2] == 51 and rmax[3] == 57 + assert min(t for t in T_RANGE if rmax[t] == 72) == 51 + # Exact degree ledger. + assert bridge_ok(CAP['B_bridge']) and not bridge_ok(CAP['B_bridge'] + 1) and bridge_ok(RETAINED) + readings = {} + for reading in CAP: + for prefix in PREFIX: + tm = t_max(S, reading, prefix) + assert row(2, S, prefix) == 16469 + check_point(tm, rmax[tm], S, reading, prefix) + readings[f'{reading}/{prefix}'] = dict( + cap=CAP[reading], t_max=tm, row_at_t_max=row(tm, S, prefix), + row_at_t_max_plus_1=row(tm + 1, S, prefix), R_max=rmax[tm], + rank56_idle_admissible=tmin[56] <= tm, R72_admissible=tmin[72] <= tm) + want = {'A_retained/fixed': 3, 'A_retained/per_level': 3, 'B_bridge/fixed': 181, 'B_bridge/per_level': 152} + assert {k: v['t_max'] for k, v in readings.items()} == want + region = {} + for r in (48, 51, 52, 56, 57, 58, 64, 68, 71, 72): + t = tmin[r] + # 0 means no positive stock fits at the least admissible degree + region[str(r)] = dict(least_degree=t, **{f'S_max[{k}/{p}]': max(s_max(t, k, p), 0) for k in CAP for p in PREFIX}) + for k in CAP: + for p in PREFIX: + sm = s_max(t, k, p) + assert row(t, sm, p) < CAP[k] <= row(t, sm + 1, p) + assert (S <= sm) == (t <= t_max(S, k, p)) + # Ideal ceilings (optimistic relaxation; no supplier, no kappa claim). + sys.path.insert(0, str(ROOT / 'research/complex-local-word-ceiling')) + import ceiling as C + base = C.ceiling(local, M, FAMILIES, STAGES, CENTRE) # unmodified, R = 51 from its guard + old = json.loads(text('research/complex-local-word-ceiling/RESULT.json'))['ceiling']['a_ceiling'] + ceilings, table = {}, {} + for R in range(51, M): + lo, hi = ceiling_dec(local, R) + f_lo, f_hi = relax_colkitt(C, local, R, lo), relax_colkitt(C, local, R, hi) + assert f_lo[1] < 1 < f_hi[0], f'second method disagrees at R={R}' + if R == 51: + assert (lo, hi) == base and str(hi) == old + table[R] = hi + if R in (51, 57, 72): + ceilings[str(R)] = dict(least_degree=tmin[R], a_ceiling=str(hi), a_ceiling_decimal=dec(hi), + kappa_upper_bound_decimal=dec(hi / (1 + hi))) + a51 = table[51] + for R in ('57', '72'): + ceilings[R]['gain_over_R51_percent'] = dec(100 * (Q(ceilings[R]['a_ceiling']) / a51 - 1), 6) + assert all(table[R] < table[R + 1] for R in range(51, 72)) + # Least child rank whose ideal ceiling exceeds the selected bit endpoint (grid cell entirely above it). + above = [R for R in table if table[R] - Q(1, 10 ** 15) > bit_lower] + assert above == list(range(min(above), M)) and table[min(above) - 1] <= bit_lower + crossing = dict(bit_lower_decimal=dec(bit_lower, 22), least_R_with_ceiling_above_bit=min(above), + least_degree=tmin[min(above)], ceiling_at_that_R=dec(table[min(above)]), + ceiling_one_rank_below=dec(table[min(above) - 1])) + for R in ceilings: + cap = min(Q(ceilings[R]['a_ceiling']), bit_lower) # the selected bit endpoint caps any conversion + ceilings[R]['kappa_upper_bound_with_bit_cap_decimal'] = dec(cap / (1 + cap)) + crossing['kappa_cap_from_bit_endpoint_decimal'] = dec(bit_lower / (1 + bit_lower)) + # Conditional what-if under reading A: sharper depth coefficient (selected-coarse-depth-stock). + sharp = {} + for prefix in PREFIX: + ok = [R for R in range(49, M) if sharp_row(R, S, prefix) < RETAINED] + assert ok == list(range(49, max(ok) + 1)) + Rs = max(ok) + sharp[f'A_retained/{prefix}'] = dict(R_max=Rs, row_at_R_max=sharp_row(Rs, S, prefix), + row_at_R_max_plus_1=sharp_row(Rs + 1, S, prefix), + ceiling=dec(table[Rs]), gain_over_R51_percent=dec(100 * (table[Rs] / a51 - 1), 5)) + assert {k: v['R_max'] for k, v in sharp.items()} == {'A_retained/fixed': 59, 'A_retained/per_level': 58} + # Robustness and direct answers. + prefix3_max = RETAINED - 1 - 3 * S - BIT_RESERVES # any prefix(3) <= this admits t = 3 under A + assert prefix3_max == 2073 and row(3, S, 'fixed') < RETAINED and 256 * 9 > prefix3_max + depth6 = row(6, S, 'fixed') # kappa010-rank-cap-floor OQ3 (depth six) + assert depth6 == 27037 and RETAINED <= depth6 < CAP['B_bridge'] + # Conditional what-if (#3667, unadopted): 9909/252 slots slack, lean row t*S + prefix(t) under A. + lean = {} + for prefix in PREFIX: + ts = [t for t in T_RANGE if row(t, S, prefix) - BIT_RESERVES < RETAINED] + assert ts == list(range(2, max(ts) + 1)) + lean[f'A_retained/{prefix}'] = dict(t_max=max(ts), row_at_t_max=row(max(ts), S, prefix) - BIT_RESERVES, + R_max=rmax[max(ts)]) + assert {k: (v['t_max'], v['R_max']) for k, v in lean.items()} == {'A_retained/fixed': (7, 66), 'A_retained/per_level': (6, 65)} + assert row(2, S, 'fixed') - BIT_RESERVES == 6308 and max(v['R_max'] for v in lean.values()) < min(above) + controls = run_controls(S, inv, H, mass) + return dict( + status='PASS_COMPLEX_HALVING_DEGREE_INVOICE_SCOPED', + scope=('Scoped finite invoice statement under inherited PR1087-lineage transfer/bridge hypotheses; ' + 'optimistic relaxation; admits nothing; no supplier, no kappa, no frontier change.'), + source_bindings_checked=nbind, + selected_invoice=dict(member=INVOICE, sha256=INVOICE_SHA, physical=inv['physical'], stock_bits=S, + physical_row=16469, retained_row=RETAINED, row_prefix_extra=inv['row_prefix_extra'], + router_bits=inv['finite']['router_bits'], literal_bits=inv['finite']['literal_bits'], + required_C0_bits=inv['finite']['required_C0_bits']), + ledger='Row(t,S) = t*S + 10161 + prefix(t); prefix fixed = 1024 or per_level = 512*t', + caps=dict(CAP), bridge_gap_at_B_cap=str(RESERVE - FACTOR * CAP['B_bridge']), + readings=readings, region_by_child_rank=region, + least_degree_by_rank={str(r): tmin[r] for r in range(48, M)}, + r_max_by_degree={str(t): rmax[t] for t in (2, 3, 4, 5, 6, 8, 10, 16, 25, 50, 51, 152, 181)}, + local_word={str(r): n for r, n in sorted(local.items())}, idle_mass_per_call=idle_mass(local), + ceilings=ceilings, ceiling_by_rank={str(R): dec(v) for R, v in table.items()}, + bit_endpoint_crossing=crossing, controls=controls, + invoice_independent=dict(R_max_any_degree=max(rmax.values()), note=('R <= 72 for every t and every child rank, paid or idle: R = 73 never meets the guard. ' + 'The ceilings price only idle repacking of the fixed selected word.')), + sharp_depth_coefficient_what_if_A=sharp, A_admits_t3_for_any_prefix3_at_most=prefix3_max, + lean_row_what_if_A_3667=lean, + depth6_row_fixed_prefix=dict(row=depth6, fits_A=depth6 < RETAINED, fits_B=depth6 < CAP['B_bridge'])) + + +def must_fail(name, fn, why): + try: + fn() + except AssertionError as e: + assert why in str(e), f'control {name} failed for another reason: {e}' + return name + raise AssertionError(f'control {name} unexpectedly passed') + + +def run_controls(S, inv, H, mass): + def mutated(path, value): + x = json.loads(json.dumps(inv)) + node = x + for k in path[:-1]: + node = node[k] + node[path[-1]] = value + return lambda: bind_invoice(x, H, mass) + return [ + must_fail('reading_A_t4', lambda: check_point(4, 57, S, 'A_retained', 'fixed'), 'row 21753 >= cap 20161'), + must_fail('reading_A_per_level_t4', lambda: check_point(4, 57, S, 'A_retained', 'per_level'), 'row 22777 >= cap 20161'), + must_fail('guard_R58_t3', lambda: check_point(3, 58, S, 'B_bridge', 'fixed'), 'guard fails at t=3, R=58'), + must_fail('guard_R72_t50', lambda: check_point(50, 72, S, 'B_bridge', 'fixed'), 'guard fails at t=50, R=72'), + must_fail('guard_R73_t200', lambda: check_point(200, 73, S, 'B_bridge', 'fixed'), 'guard fails at t=200, R=73'), + must_fail('reading_B_t182', lambda: check_point(182, 72, S, 'B_bridge', 'fixed'), 'row 492029 >= cap 490196'), + must_fail('reading_B_per_level_t153', lambda: check_point(153, 72, S, 'B_bridge', 'per_level'), 'row 492723 >= cap 490196'), + must_fail('bridge_cap_plus_one', lambda: check_point(2, 51, S, 'B_bridge', 'fixed', cap=CAP['B_bridge'] + 1), + 'bridge degree_gap not positive'), + must_fail('prefix_mutation', mutated(['row_prefix_extra'], 0), 'prefix'), + must_fail('stock_bits_mutation', mutated(['finite', 'physical_stock_bits'], S + 1), 'stock bits'), + must_fail('physical_mutation', mutated(['physical'], inv['physical'] * 2), 'stock bits'), + ] + + +if __name__ == '__main__': + out = json.dumps(main(), indent=2, sort_keys=True) + '\n' + path = HERE / 'RESULT.json' + if sys.argv[1:] == ['--write']: + path.write_text(out) + else: + assert sys.argv[1:] == [], __doc__ + assert path.read_text() == out, 'RESULT.json differs from the recomputation' + r = json.loads(out) + print(r['status'], {k: v['t_max'] for k, v in r['readings'].items()}, + {k: v['a_ceiling_decimal'] for k, v in r['ceilings'].items()}, len(r['controls']), 'controls')