From 0bdfeb9b6961b02c8a24e116e7686c18f8d62d0f Mon Sep 17 00:00:00 2001 From: Dylan Roy Date: Fri, 2 Oct 2026 10:48:05 -0500 Subject: [PATCH 1/2] Prove conditional sub-pin witness collision and marked lifetime bounds --- frontiers/subpin_collision_20261002/PROOF.md | 237 ++++++++++++++++++ frontiers/subpin_collision_20261002/README.md | 30 +++ .../subpin_collision_20261002/RESULTS.json | 51 ++++ .../subpin_collision_20261002/SOURCES.json | 139 ++++++++++ .../subpin_collision_20261002/controls.py | 87 +++++++ 5 files changed, 544 insertions(+) create mode 100644 frontiers/subpin_collision_20261002/PROOF.md create mode 100644 frontiers/subpin_collision_20261002/README.md create mode 100644 frontiers/subpin_collision_20261002/RESULTS.json create mode 100644 frontiers/subpin_collision_20261002/SOURCES.json create mode 100644 frontiers/subpin_collision_20261002/controls.py diff --git a/frontiers/subpin_collision_20261002/PROOF.md b/frontiers/subpin_collision_20261002/PROOF.md new file mode 100644 index 000000000..4d903d0f8 --- /dev/null +++ b/frontiers/subpin_collision_20261002/PROOF.md @@ -0,0 +1,237 @@ +# Collisions below the pin scale have vanishing weighted mass + +Object OA-SUBPIN-COLLISION-20261002-v1. Author-side conditional corollary, +OpenAI/Codex, 2 October 2026. Scientific effect NONE. This is a deduction from +the exact imported results below, not a new acceptance of their proofs. + +## 1. Observable and source boundary + +Fix a dimension d >= 2 and a torus side L > 0. Use the centered variance-one +periodized Gaussian field, the pin pair M = -ru/2, S = ru/2 with heights +b and b-kr^3, k > 0, and both gradients zero. Q_r is the canonical regression +on these pins. Retain the original typed determinant weight and FULL normalizer + + W_r = F_d(H_M) F_(d-1)(H_S), + Z_r = E_Qr W_r, P_r = (W_r/Z_r) Q_r. + +F_j is the absolute Hessian determinant times its index-j indicator. Let N_r +count all additional critical points in the open window (b-kr^3,b), excluding +M and S. All distances below are torus geodesic distances. The count is finite +almost surely under the imported regularity and moment statements. + +Let epsilon:(0,r_*) -> (0,infinity) be deterministic and Borel measurable, with +epsilon(r) -> 0. Define the ORDERED distinct-pair count + + C_r = sum_(x != y, additional window critical points) + 1{dist_T(x,y) <= r epsilon(r)}. (1) + +There is no adjacency, persistence or gradient-connection condition on x,y. +The endpoints of (1) are additional witnesses, not the original pins. + +All source identities and exact consumed portions are in SOURCES.json, at +Math- commit a808ba25de9db22110db8b7555a64852f38e031d: + +- [TS] TWO_SCALE_LAW.md, Theorems T and L, (T5), (T7), (L1), (L3). + Its complete configuration-space limit and ordered-pair law are needed; + convergence of the one-point intensity alone would not suffice. +- [SC] spectral_cluster_closure/PROOF.md, as consumed by TS: finite nonempty + cubic measure, pointwise simple roots, and the first/count-moment bounds. +- [C6] c6_palm_route/PROOF.md, Theorem Q: the original weighted factorial + moments of orders q >= 2, uniform on compact b,k and frames. The uniform + first-moment upper bound is [DL](1.7), explicitly used in the proof of C6 + Section 7, Corollary P. With that first moment, the Stirling expansion gives + E_Pr N_r^q <= C_q r^3 for every positive integer q on such compact sets. +- [DL] d5_dimension_lift/PROOF.md, Theorem G_d (1.7), with its stated + dimension-lift/regional dependencies retained. This is the compact-uniform + first-moment interface; SC's pointwise statement alone is not substituted. +- [P] the lifetime parent, read with its required reconciliation/errata and + replacement Section 9. We use its full normalizer Z_r/r^2 -> z_0 > 0, + its marked Kac-Rice identity, and (10.2)-(11.2), including the compact-uniform + bound on A_r. The original parent Section 9 is not an unrepaired premise. + +TS has a source-bound nonauthor acceptance in review5360227991 and its current +REVIEW_RECORD.md. That acceptance remains conditional on the exact SC/CUB/RM/C6/P +interfaces stated in TS. We neither remove those conditions nor re-review them. +No conclusion here is conditional on the open PR242, PR243 or PR244. + +## 2. The sub-pin-scale theorem + +**Theorem D.** For every fixed b, k > 0, frame, d and L, and every epsilon above, +for each fixed nonnegative integer p, + + E_Pr [N_r^p C_r] = o(r^3), + P_r(C_r > 0) = o(r^3), + E_Qr [W_r N_r^p C_r] = o(r^5). (2) + +N_r^0 is defined to be 1, including at N_r = 0. The little-o is pointwise in +the fixed marks. No uniform little-o, algebraic rate, numerical constant, +growing dimension/volume, or k -> 0 assertion is supplied. + +**Proof: remove pairs outside the microscopic component.** Choose a deterministic +cutoff delta_r = sqrt(r) for small r; only delta_r -> 0 and delta_r/r -> infinity +are used. Let N_in count the points at distance < delta_r from the pin midpoint. +TS(L1), with q = 2, gives + + E_Pr [(N_r)_2 - (N_in)_2] = o(r^3). (3) + +Every ordered pair not wholly inside that ball, including close pairs far from +the pins, is counted in (3). Thus no near-diagonal covariance bound uniform in +the midpoint location is being silently assumed. + +**Proof: the microscopic limit puts no mass on coincident spatial positions.** +For the pairs wholly inside the delta_r ball, let nu_r be r^-3 times their +expected ordered-pair measure on + + E x E, E = R^d x (0,1) x {0,...,d}, + +using positions x/r, downward normalized height, and index. TS(L3) gives weak +convergence of FINITE measures nu_r -> nu, including convergence of total mass. +The limiting measure is the integral, on two-root cubic configurations, of +the two ordered atoms (z_1,z_2) and (z_2,z_1) against the finite nonempty +spectral measure. The cubic roots have distinct spatial positions almost +everywhere on this measure. Therefore the spatial coincidence diagonal D has +nu(D) = 0. This is stronger than finite-r simplicity alone. + +For eta > 0 define the bounded continuous cutoff on E x E + + phi_eta(z,z') = min(1, max(0, 2 - |pos(z)-pos(z')|/eta)). (4) + +It equals 1 when the distance is <= eta and vanishes at distance >= 2 eta. +Eventually epsilon(r) <= eta. Also 2 delta_r < L/2, so the torus distance +between any two points in the delta_r ball equals the Euclidean distance +between their chosen local lifts. Consequently + + limsup_(r->0) r^-3 E_Pr [C_r with both points inside] + <= lim_(r->0) integral phi_eta dnu_r + = integral phi_eta dnu. (5) + +As eta decreases to zero, phi_eta tends to 1_D. Finiteness of nu and dominated +convergence give integral phi_eta dnu -> 0. Combining (3) and (5) proves +E_Pr C_r = o(r^3). The order of limits is r -> 0 first for fixed eta, then +eta -> 0. No finite-r density estimate, spatial total variation, or choice of +root ordering is needed. + +**Proof: multiplicities and the original numerator.** C_r is either zero or +at least two, since both orientations of a close pair are included. Hence + + P_r(C_r > 0) <= E_Pr C_r/2 = o(r^3). (6) + +Pathwise, N_r^p C_r <= N_r^(p+2) 1{C_r>0}. Cauchy-Schwarz and the imported +ordinary moment of order 2p+4 give + + r^-3 E_Pr[N_r^p C_r] + <= (r^-3 E_Pr N_r^(2p+4))^(1/2) + (r^-3 P_r(C_r>0))^(1/2) -> 0. (7) + +This is why an event probability alone is not substituted for counted mass. +Finally the definition of P_r is an exact identity: + + E_Qr[W_r N_r^p C_r] = Z_r E_Pr[N_r^p C_r]. (8) + +Since Z_r/r^2 -> z_0, (8) proves the o(r^5) numerator. There is exactly one +endpoint determinant weight and one full normalizer. QED. + +## 3. Compact-mark lifetime consequence in the actual intensity units + +Fix compact intervals B in R and K = [k_-,k_+] with k_- > 0, a fixed d,L, +and all directions u in S^(d-1). Define + + m_p(r,b,k,u) = E_Pr[N_r^p C_r]. + +The mark is jointly Borel: on a compact spatial domain away from the pin and +pair diagonals, critical-point counts with the Borel distance/height indicator +are measurable under the canonical regression kernels; exhaust these domains. +The inherited weighted marked Kac-Rice identity extends by monotone truncation +to this nonnegative count mark. Its integrability follows from C6's ordinary +moment bound. This uses the repaired [P] Section 9, not continuity of C_r. + +Per unit midpoint volume, the candidate intensity carrying this multiplicity is + + d beta_p = r A_r(b,k,u) m_p(r,b,k,u) dr db dk d sigma(u), (9) + A_r = 12 pi_r (Z_r/r^2). + +Thus every pin density, spatial/height Jacobian and original determinant +normalization is already present in (9). sigma is ordinary spherical surface +area, not normalized Haar probability. The pin roles order the maximum/saddle +pair; there is no new factor 1/2. C_r itself counts ordered witness pairs. + +**Corollary E.** Under the exact height-gap map ell = k r^3, beta_p has a +Lebesgue density satisfying + + rho_p(ell) = o(ell^(2/3)), + beta_p{0 < ell <= t} = o(t^(5/3)). (10) + +This statement concerns the collision-marked candidate measure (9). Its +submeasure obtained by inserting the actual global elder indicator satisfies +the same estimates. It is not an identification of another proxy population +with the persistence bars, nor a claim that all selection failures satisfy (10). + +**Proof.** For ell < k_- r_*^3, put R = (ell/k)^(1/3). Tonelli and the exact +one-variable change of variables give the density version + + rho_p(ell) = ell^(2/3)/3 * integral_(B x K x S^(d-1)) + k^(-5/3) A_R(b,k,u) [m_p(R,b,k,u)/R^3] + db dk d sigma(u). (11) + +Indeed r dr/dell = k^(-2/3) ell^(-1/3)/3 and R^3 = ell/k. +For every fixed b,k,u the bracket in (11) tends to zero by Theorem D. +It is bounded uniformly on the compact mark domain because +m_p <= E_Pr N_r^(p+2) <= C r^3 there. A_R is also uniformly bounded by [P]. +The remaining k^(-5/3) factor is integrable because k >= k_- and the domain +has finite measure. Dominated convergence proves the density assertion. +Integrating its absolute nonnegative bound gives the cumulative assertion: +for any a > 0, rho_p(ell) <= a ell^(2/3) for all sufficiently small ell for +this density version, so beta_p(0,t] <= (3a/5)t^(5/3). +Any other version obeys the corresponding almost-everywhere bound. QED. + +Pointwise convergence in the marks plus this uniform integrable majorant is +enough; no compact-uniform little-o is being imported. The Borel epsilon is +the same function of r across the mark domain and need not be monotone. + +## 4. What the hypotheses prevent + +These are abstract marked-count examples, not counterexamples to the Gaussian +field. Their purpose is to make the logical boundaries testable. + +1. **Moments alone do not remove subscale collisions.** With probability r^3 + place two witnesses at scaled positions 2 and 2+r, otherwise none. Then + every fixed moment is 2^q r^3, but for epsilon(r)=sqrt(r), E C_r=2r^3. + The limiting pair measure charges the diagonal. The simple limiting roots + in TS(L3), not merely the global factorial bound, exclude this example. +2. **No algebraic rate follows from weak convergence.** In a rare event of + probability r^3, place the two scaled points at 2 and 3 with probability + 1-a_r, and at 2 and 2+r with probability a_r, where a_r=1/log(1/r) + for r0. +3. **An event estimate alone does not control multiplicity.** Let r_n=2^-n, + N_n=r_n^-1 with probability r_n^5 and zero otherwise, and cluster those + witnesses within the distance cutoff. Then P(C_n>0)=r_n^5=o(r_n^3), + but E C_n = r_n^3(1-r_n), which is not o(r_n^3). Its fourth count moment + is r_n, violating the moment hypothesis used in (7). +4. **Scale-r doublets remain.** Replacing epsilon(r)->0 by a fixed positive + cutoff can retain positive limiting pair mass. TS's positive two-root + coefficient and all consequences about non-singleton clusters remain intact. + +The exact controls check finite count inequalities, these examples' rational +arithmetic and the coarea exponents. They do not prove weak convergence, +Gaussian conditioning, the imported parent theorems, or mathematical acceptance. + +## 5. Relation to the completion directive + +The earlier proposed compact-mark O(r^3) task was already supplied by C6 +pointwise in b,k and frame; [P](11.2) already uses height-disintegrated units. +The missing implication in a generic marginal example cannot be attributed to +these sources. Likewise the existing globally elder-marked endpoint route +identifies actual finite bars at its own conditional scope; it does not require +auxiliary-witness uniqueness. This note leaves that route and its review +requirements unchanged. It supplies the stricter sub-pin-scale conclusion (2). + +This result removes subscale extra-witness collisions from a compact-mark +ell^(2/3) coefficient in any argument whose error is explicitly dominated by +the measure (9). It does not prove that every bad geometric configuration has +that domination. It supplies no O(ell^(3/4)) remainder, no uniform k->0 tail, +no rate in an expanding annulus, and no resolution of PR242 Conjecture 7. +It does not concern a witness colliding with a pin, shared endpoints between +different candidate pairs, or the whole class of scale-r doublets. No status, +historical predicate, normalizer, scientific gate or independence credit changes. diff --git a/frontiers/subpin_collision_20261002/README.md b/frontiers/subpin_collision_20261002/README.md new file mode 100644 index 000000000..795230242 --- /dev/null +++ b/frontiers/subpin_collision_20261002/README.md @@ -0,0 +1,30 @@ +# Witness collisions below the pin scale + +Pairs of additional critical points can occur with probability of order r^3 +when their separation is comparable to the pin distance r. This conditional +corollary shows that pairs separated by o(r) carry only o(r^3) weighted mass. +On compact positive gap marks, their collision-marked lifetime density is +o(ell^(2/3)). The original determinant weight and full normalizer are retained. + +Read [the proof and boundaries](PROOF.md), [the exact source map](SOURCES.json), +and [finite negative controls](controls.py). This is a new deduction from the +reviewed two-scale pair law, not a new Gaussian collision calculation or a +whole-project completion certificate. No convergence rate is claimed. + +From the repository root, run: + +```sh +python3 -B -S frontiers/subpin_collision_20261002/controls.py +python3 -B -O -S frontiers/subpin_collision_20261002/controls.py +``` + +The output should match [RESULTS.json](RESULTS.json). The script checks exact +algebra and logical counterexamples; the proof's analytic imports require their +own source-bound reviews. Hosted downstream/formal checks have a different scope. + +Author-side OpenAI/Codex work, with root and named analytical subagents. +Dylan Roy delegated the work; personal reading remains PENDING. +Organizational independence 0; scientific effect NONE. + +[Public mathematical reading map](../../PUBLIC_READING_MAP.md) +ยท [Two-scale configuration source](../two_scale_cluster_geometry_20260929/TWO_SCALE_LAW.md) diff --git a/frontiers/subpin_collision_20261002/RESULTS.json b/frontiers/subpin_collision_20261002/RESULTS.json new file mode 100644 index 000000000..d0a10dc0a --- /dev/null +++ b/frontiers/subpin_collision_20261002/RESULTS.json @@ -0,0 +1,51 @@ +{ + "coarea": { + "cumulative_power": "5/3", + "gap_power": "-5/3", + "lifetime_power": "2/3", + "radial_power": "4" + }, + "diagonal_mass_ratios": [ + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + "not_certified": [ + "analytic limits", + "Gaussian parent proofs", + "uniform little-o", + "algebraic rate", + "scientific acceptance" + ], + "rare_high_multiplicity_ratios": [ + "3/4", + "7/8", + "15/16", + "31/32", + "63/64", + "127/128", + "255/256", + "511/512", + "1023/1024" + ], + "simple_witness_graphs": 33868, + "slow_convergence_ratios": [ + "1", + "2/3", + "1/2", + "2/5", + "1/3", + "2/7", + "1/4", + "2/9", + "1/5" + ], + "source_files_verified": 13, + "status": "PASS_EXACT_FINITE_CONTROLS_ONLY" +} diff --git a/frontiers/subpin_collision_20261002/SOURCES.json b/frontiers/subpin_collision_20261002/SOURCES.json new file mode 100644 index 000000000..08d7e94a6 --- /dev/null +++ b/frontiers/subpin_collision_20261002/SOURCES.json @@ -0,0 +1,139 @@ +{ + "schema": 1, + "repository": "d6g8k5htny-coder/Math-", + "commit": "a808ba25de9db22110db8b7555a64852f38e031d", + "scientific_effect": "NONE", + "inherited_hypotheses": "All TS/SC/CUB/RM/C6/P interfaces retained; this map does not accept parent proofs.", + "sources": [ + { + "id": "TS", + "path": "frontiers/two_scale_cluster_geometry_20260929/TWO_SCALE_LAW.md", + "role": "consumed", + "consumes": "T5,T7,L1,L3; complete finite weak ordered-pair law; all imported interfaces retained", + "bytes": 17139, + "sha256": "e81d7fe09d25c3266eb8e62922756f54761d7f74d692fb35d9a8071fffd73769", + "git_blob": "a32fd5f7d941bbe1fe943df045b1e0fbec8d691c", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/a808ba25de9db22110db8b7555a64852f38e031d/frontiers/two_scale_cluster_geometry_20260929/TWO_SCALE_LAW.md" + }, + { + "id": "TS-review", + "path": "frontiers/two_scale_cluster_geometry_20260929/REVIEW_RECORD.md", + "role": "review provenance", + "consumes": "Source-bound conditional review5360227991; not new parent acceptance", + "bytes": 6732, + "sha256": "af1540308f37220e6592b700bf42181205b1d4588a040a5c151bf0a6f861e728", + "git_blob": "31896de23fc56822c184375d0dc2b1c7e27fcae4", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/a808ba25de9db22110db8b7555a64852f38e031d/frontiers/two_scale_cluster_geometry_20260929/REVIEW_RECORD.md" + }, + { + "id": "SC", + "path": "frontiers/spectral_cluster_closure_20260929/PROOF.md", + "role": "consumed through TS", + "consumes": "Finite cubic measure and distinct nondegenerate roots; count first moments", + "bytes": 25006, + "sha256": "e971b2cbe50a8a06b47c1219191201e0d1037c9adac23e5e3b7d2051bb70c2eb", + "git_blob": "16c56821b52fd76b0be791622b9c3809eafde75a", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/a808ba25de9db22110db8b7555a64852f38e031d/frontiers/spectral_cluster_closure_20260929/PROOF.md" + }, + { + "id": "C6", + "path": "frontiers/c6_palm_route_20260929/PROOF.md", + "role": "consumed", + "consumes": "Theorem Q compact-uniform original weighted factorial moments q>=2; Section7 CorollaryP proof imports [DL](1.7) first moment", + "bytes": 53364, + "sha256": "aa37f16040ab9e05bb2e4e3f1d678367497e8dc2cf43eef197a4d6592c2f129b", + "git_blob": "89eb8adf08fe7afc2cab9662d3a9875c05ae5cc5", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/a808ba25de9db22110db8b7555a64852f38e031d/frontiers/c6_palm_route_20260929/PROOF.md" + }, + { + "id": "P", + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "role": "consumed with amendments", + "consumes": "Sections5,10.2,11.2 full normalizer and marked intensity/coarea", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/a808ba25de9db22110db8b7555a64852f38e031d/imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md" + }, + { + "id": "CAP", + "path": "imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md", + "role": "required parent identity", + "consumes": "Sections1-5; no new cap proof claimed", + "bytes": 15160, + "sha256": "0bf922b9203c29088b12388807aa0e2ecd020485eb0f6e919679841b5b2636fc", + "git_blob": "0633aca3c2a2882b0de4399da0a75d64c2e6b2e1", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/a808ba25de9db22110db8b7555a64852f38e031d/imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md" + }, + { + "id": "E1", + "path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", + "role": "required parent amendment", + "consumes": "Correct congruence factor", + "bytes": 1782, + "sha256": "bad7ef609c4ad8c41ad6af562c1b6807921e19a9d556ed793ad1a0db6e202028", + "git_blob": "213594d6ca6a86fb938110f4d166d9ce275a02d0", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/a808ba25de9db22110db8b7555a64852f38e031d/imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md" + }, + { + "id": "E2", + "path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "role": "consumed", + "consumes": "Section9 replacement: whole-field Borel marked Kac-Rice", + "bytes": 9062, + "sha256": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f", + "git_blob": "fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/a808ba25de9db22110db8b7555a64852f38e031d/reviews/d1_section9_borel_repair_20260925/REPAIR.md" + }, + { + "id": "REC", + "path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", + "role": "required parent amendment and review provenance", + "consumes": "Reading rule; W1 and embedding radius; source-bound review ledger", + "bytes": 23312, + "sha256": "451b9d7ffee072a73fc904cab891b6693e3f233808b89df10cce1b57036b65da", + "git_blob": "75da2597971510f843f8d90c743950cb8c177342", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/a808ba25de9db22110db8b7555a64852f38e031d/reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md" + }, + { + "id": "BAR-context", + "path": "frontiers/short_bar_endpoint_law_20261001/PROOF.md", + "role": "context only", + "consumes": "Existing globally elder-marked actual-bar route; no new theorem imported", + "bytes": 13815, + "sha256": "4fc567b5bed7967bba7b7fc609da8219b6cd2c605e9291b7b82c8a538ced1a29", + "git_blob": "0d47dbc1d92863d8c51b918aa47d1fa8b605cfdc", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/a808ba25de9db22110db8b7555a64852f38e031d/frontiers/short_bar_endpoint_law_20261001/PROOF.md" + }, + { + "id": "C6-context", + "path": "reviews/c6_witness_collision_reconciliation_20260929/RECONCILIATION.md", + "role": "context only", + "consumes": "All Borel pair selectors; distinction from limiting cluster law", + "bytes": 41289, + "sha256": "96a0f0bf2700b64b933d08d3c81efbfa8388aa2094e5528a1a6bd627e69f902a", + "git_blob": "e488c0afed5c41c2872de0902f0e3d1c08e1b2ce", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/a808ba25de9db22110db8b7555a64852f38e031d/reviews/c6_witness_collision_reconciliation_20260929/RECONCILIATION.md" + }, + { + "id": "C6-successor-context", + "path": "reviews/c6_residual_closure_20260930/RECONCILIATION.md", + "role": "context only", + "consumes": "Existing conditional leading-mass localization", + "bytes": 34758, + "sha256": "b647a186d0cfd1662fc69e9d31dfd447dbb1b2f6ef4364bbd59c4956f18aed25", + "git_blob": "3cfd17c5ef0356dbd3e8f98a2d08cb404ddd982c", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/a808ba25de9db22110db8b7555a64852f38e031d/reviews/c6_residual_closure_20260930/RECONCILIATION.md" + }, + { + "id": "DL", + "path": "frontiers/d5_dimension_lift_20260929/PROOF.md", + "role": "consumed via C6 Section7 CorollaryP", + "consumes": "Theorem G_d (1.7): compact-uniform first-moment upper bound; every-d regional dependencies retained", + "bytes": 53727, + "sha256": "6fb94b247e8e45bca9dc02f46670ac6029fb54e0ef906001efe48fe908549b80", + "git_blob": "9d82c707fdb17d3072a8930f26dabedf59e456fc", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/a808ba25de9db22110db8b7555a64852f38e031d/frontiers/d5_dimension_lift_20260929/PROOF.md" + } + ] +} diff --git a/frontiers/subpin_collision_20261002/controls.py b/frontiers/subpin_collision_20261002/controls.py new file mode 100644 index 000000000..27992c01c --- /dev/null +++ b/frontiers/subpin_collision_20261002/controls.py @@ -0,0 +1,87 @@ +"""Exact finite controls; no analytic theorem or review is certified here.""" +from fractions import Fraction as F +from pathlib import Path +import hashlib +import json + + +def require(condition, label): + if not condition: + raise RuntimeError(label) + + +def main(): + here = Path(__file__).resolve().parent + root = here.parents[1] + source_map = json.loads((here / 'SOURCES.json').read_text()) + for source in source_map['sources']: + raw = (root / source['path']).read_bytes() + require(len(raw) == source['bytes'], 'source size: ' + source['id']) + require(hashlib.sha256(raw).hexdigest() == source['sha256'], + 'source digest: ' + source['id']) + + # Exhaust all simple undirected witness graphs on at most six vertices. + # C is twice the edge count: ordered pairs, not unordered pairs or events. + graphs = 0 + for n in range(7): + edges = n * (n - 1) // 2 + for bits in range(1 << edges): + c = 2 * bits.bit_count() + require(c <= n * (n - 1), 'factorial count domination') + require((c == 0) or c >= 2, 'ordered nonempty lower bound') + for p in (0, 1, 2, 5): + require(n**p * c <= n**(p + 2) * int(c > 0), + 'polynomial insertion') + graphs += 1 + + # Exact discrete subsequences of the proof's three abstract examples. + diagonal_ratios = [] + multiplicity_ratios = [] + slow_ratios = [] + for j in range(2, 11): + r = F(1, 2**j) + # Two points a scaled distance r apart fall below sqrt(r). + require(r*r <= r, 'shrinking cutoff inclusion') + close_count = r**3 * 2 + require(close_count/r**3 == 2, 'moments do not remove diagonal mass') + diagonal_ratios.append(str(close_count/r**3)) + # Rare many-point cluster: small event probability, non-small count. + n = 2**j + require(r**5 * n*(n-1) / r**3 == 1-r, 'count/event distinction') + require(r**5 * n**4 == r, 'fourth moment fails') + multiplicity_ratios.append(str(1-r)) + # a_j=1/j tends to zero arbitrarily slowly relative to powers of r_j. + a = F(1, j) + require((r**3 * 2*a)/r**3 == 2*a, 'slow convergence family') + slow_ratios.append(str(2*a)) + + # If a radial density is r^alpha and ell=k r^3, its density is + # (1/3) k^(-(alpha+1)/3) ell^((alpha-2)/3). + alpha = F(4) # r times the o(r^3) weighted mark + lifetime_power = (alpha-2)/3 + gap_power = -(alpha+1)/3 + cumulative_power = lifetime_power+1 + require((lifetime_power, gap_power, cumulative_power) == + (F(2, 3), F(-5, 3), F(5, 3)), 'coarea units') + require(F(2)+F(3) == F(5), 'one full normalizer only') + # Negative controls for common incorrect substitutions. + require(F(3)/3 != lifetime_power, 'omit radial/coarea Jacobian rejected') + require(F(2)+F(2)+F(3) != F(5), 'double normalizer rejected') + require(F(1) != F(2), 'unordered/ordered counts are different') + + print(json.dumps({ + 'status': 'PASS_EXACT_FINITE_CONTROLS_ONLY', + 'source_files_verified': len(source_map['sources']), + 'simple_witness_graphs': graphs, + 'diagonal_mass_ratios': diagonal_ratios, + 'rare_high_multiplicity_ratios': multiplicity_ratios, + 'slow_convergence_ratios': slow_ratios, + 'coarea': {'radial_power': str(alpha), 'lifetime_power': str(lifetime_power), + 'gap_power': str(gap_power), 'cumulative_power': str(cumulative_power)}, + 'not_certified': ['analytic limits', 'Gaussian parent proofs', + 'uniform little-o', 'algebraic rate', 'scientific acceptance'] + }, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() From 87372f2bceeab21e58b8a5ca04cb55105193b1c1 Mon Sep 17 00:00:00 2001 From: Dylan Roy Date: Fri, 2 Oct 2026 10:49:07 -0500 Subject: [PATCH 2/2] Keep exact collision controls compatible with system Python --- frontiers/subpin_collision_20261002/controls.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontiers/subpin_collision_20261002/controls.py b/frontiers/subpin_collision_20261002/controls.py index 27992c01c..5eca8d739 100644 --- a/frontiers/subpin_collision_20261002/controls.py +++ b/frontiers/subpin_collision_20261002/controls.py @@ -26,7 +26,7 @@ def main(): for n in range(7): edges = n * (n - 1) // 2 for bits in range(1 << edges): - c = 2 * bits.bit_count() + c = 2 * bin(bits).count('1') require(c <= n * (n - 1), 'factorial count domination') require((c == 0) or c >= 2, 'ordered nonempty lower bound') for p in (0, 1, 2, 5):