Repository navigation
F-star residue class (ii): non-3-dichromatic zero digraphs - matched-pivot floor, fixture dichromatic structure, smallest-first falsifier search (no kappa) - #2774
Open
navinor wants to merge 1 commit into
Conversation
…(no kappa) Package research/fstar-zero-digraph-residue-seede9937f18. Exact zero-digraph machinery (subset-DP MAS, exact Lemma MP value over all pivot maps, dichromatic numbers with and without the D(t) pivot constraints), calibration reproducing PR 2717 anchors (tied_min 11/12, cex_min_1 18/19, chain engine 22) and PR 2747 anchors (MP 9 and 16 exhaustive over 4096 / 6144 pivot maps), the exact dichromatic structure of both canonical fixtures zero digraphs (chi = 3 on both; non-3-dichromatic only under the pivot constraints), and a smallest-first class-(ii) falsifier search, 286 instances v = 3..12, zero falsifiers, zero instances with matched-pivot value below floor(2v/3), eight non-3-dichromatic instances all with cert = v exactly. F-star itself not proved and not refuted. Aaron Wang, with help from opencode.
This was referenced Oct 16, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
F-star residue class (ii): non-3-dichromatic zero digraphs - the matched-pivot floor, the fixtures' dichromatic structure, and a smallest-first falsifier search (no kappa)
Scope
Kappa-blocker KB5c (explicit open request; scope changed from the drawn card and recorded in
TASK.json): residue class (ii) non-3-dichromatic zero digraphs of open problem F-star of the mergedresearch/root-unit-decoder-lemmaspackage (PR 1590 by DreamingOfClouds, with Claude Opus 5.5 (Anthropic) via Claude Code assistance; section 7):cert(M) >= floor(2v/3)for every exact 3-total rational decoderM = sum_j p_j q_j^T. This is the residue PR 2717 by Aaron Wang (navinor) demoted as "zero digraphs that are not 3-dichromatic (Lemma MP then gives onlysum_i MAS(Z[C_i]))" and left untouched by PR 2747 by Aaron Wang (navinor), which closed residue class (i). Packageresearch/fstar-zero-digraph-residue-seede9937f18/, registered replayPASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completedon CPython 3.12.The package does three things: (1) exact zero-digraph machinery (MAS over all subsets by DP, the exact Lemma MP value
max_c sum_i MAS(Z[C_i])over all pivot mapsc : [v] -> D(t), dichromatic numbers ofZwith and without the pivot constraint setsD(t)); (2) calibration on DreamingOfClouds' stored fixturestied_min(12 lines) andcex_min_1(19 lines) reproducing every recorded anchor, then the exact dichromatic structure of both zero digraphs (the open question 2 of PR 2717); (3) a smallest-first adversarial search for the first instance where the matched-pivot value falls belowfloor(2v/3)(the open question 1 of PR 2747, which is exactly this class's floor question). F-star itself is not proved and not refuted here. Every claim is labelled PROVEN, CHECKED or DEMOTED.Calibration - CHECKED (all recorded anchors reproduce)
Machine results (
verify.py, stdlib, deterministic; certificate digest86f48c1bacdbe4a9):tied_minone-copy L8cex_min_1one-copy L8cex_min_1stored pairingtied_mincex_min_1New: the dichromatic structure of the canonical fixtures - CHECKED
floor(2v/3)chi(Z)unconstrainedMAS(Z)v - MPDtied_mincex_min_1Consequences, each CHECKED:
cert(M)belowvoncex_min_1(18 of 19) is therefore not the dichromatic number of the digraph; it lives in the pivot constraint setsD(t)together with the labelling structure. PR 2717's open question 2 ("canZitself be non-3-dichromatic") is not realized by either fixture; both fixtures are non-3-dichromatic underD, which is the operative sense of class (ii) for Lemma MP.K_4) is attained, so clique bounds alone cannot force a dichromatic number above 3 on these instances.New: smallest-first falsifier search in the class-(ii) domain - CHECKED (scoped negative)
Smallest falsifying instance first:
vascending from 3, four generator families perv(entries in{-1,0,1}and{-2..2}), all aimed at the residue:random/random2(unstructured boxes),sparse(1-2 nonzero coordinates perp(t),q(t), dense zero digraphs),forced(support masks chosen first so at least half the lines have|D(t)| = 1, heavily constrained pivot maps),mutual(rejection sampling for many mutual-zero pairs). 286 instances,v = 3..12, deterministic seeds per instance inCERTIFICATE.json.Bwith chain cost belowfloor(2v/3), or exactcertbelow threshold)floor(2v/3)v = 3, seed 4611, matched-pivot value 2 equal tofloor(2v/3))v = 11; every witness above threshold)D(matched-pivot value belowv)chi(Z) >= 4unconstrainedThe complete class-(ii) population found (every one has
chi(Z)at most 3 unconstrained andcert(M) = vexactly by exhaustive a-enumeration):floor(2v/3)certZExact obstruction record (early kill). The matched-pivot value never fell below
floor(2v/3)anywhere in the domain; its deficitv - MPnever exceeded 3 (attained only on the fixtures), while the MP route would need the deficit to exceedceil(v/3)(4 atv = 12, 7 atv = 19) to fail on an instance. The first instance where the matched-pivot value touches the floor exactly (v = 3, seed 4611) still hascert(M) = vexactly. On all eight class-(ii) instances the general labellings reachcert(M) = vwhile matched pivots do not: label patterns beyond matched pivots (the same effect PR 2747 documented ontied_min, matched-pivot 9 versuscert11) carry the certificate there.What is proved, what is witnessed, what is demoted
cost >= sum_j r_j >= cert(M)are cited from PR 2717 by Aaron Wang (navinor) and the mergedresearch/root-unit-decoder-lemmaspackage (PR 1590 by DreamingOfClouds, with Claude Opus 5.5 (Anthropic) via Claude Code assistance), not restated.verify.py, stdlib, deterministic, about 57 s): controls (brute-force-over-all-labellings agreement 3/3 atv = 3, diagonal decodercert = 3, corrupted-witness rejection 2/2, subset-DP MAS hand values 3/3, dichromatic hand values 4/4, MP 3 on the diagonal decoder); the calibration table above; the dichromatic structure of both fixtures; and the 286-instance search with exact MP values, replayed witnesses, exactcertwhere a-enumeration terminates, and bounded admissible-Bchain scans.max_c sum_i MAS(Z[C_i]) >= floor(2v/3)is witnessed on 288 instances (2 fixtures plus 286 searched), not proved. No "exactly when" or necessity claim is made for any hypothesis. Whether some rank-3 zero digraph haschi(Z) >= 4unconstrained remains open (none found here; the decision is exact when it terminates and no run in this domain was undecided, but the search is bounded inv). Chain costs are bounded-search upper bounds on the minimum, not exact minima. The recorded fixture limits 11 and 18 rest on PR 2111's recorded CP-SAT optimality, not re-verified here. Residue classes (i) and (iii) are not re-attacked. One control's expected value was initially written wrong (the dichromatic number of a directed 3-cycle is 2, not 1; the subset DP returned the correct 2) and the control was corrected after the first run; the correction is recorded in the README rather than hidden.Overlap and coordination
Pair-collision check before computation (toolkit
disc-comments --grep, discussions 1317 and 1166, nested replies included, 2026-10-15 20:05-20:12 UTC): no live claim on F-star residue (ii) or (iii); PR 2717 (KB5) is DONE/RELEASED 18:20 UTC and PR 2747 (KB5b, residue (i)) is DONE/RELEASED 19:50 UTC. The refined overlap pass on the object's proper names (F-star, cert(M), 3-total decoder, zero digraph, 3-dichromatic, dichromatic number, matched pivot, L8 labelling, MAS, residue (ii), root-unit decoder) at 2026-10-15 21:10-21:14 UTC with complete pagination (716 open PRs, 1407 discussion records) returned only the known predecessors and unrelated objects. The chooser draw (OS seede9937f18f68bb83ac4e780cc2833deb6, track complex-mechanisms) landed on the saturated cardscomplex-new-helper-inventory,complex-rank-shape-decoderandp104-side-correction; the assignment's explicit open request KB5c is taken instead, recorded inTASK.json.Reproduce
Python 3.10+, standard library only, from the repository root:
Expected markers:
PASS_FZD_CONTROLS,PASS_FZD_FIXTURES,PASS_FZD_SEARCH,PASS_FSTAR_ZERO_DIGRAPHS,PASS_REGISTERED_RESEARCH_PACKAGE research/fstar-zero-digraph-residue-seede9937f18 outcome=completed, andCERTIFICATE.jsonwith digest86f48c1bacdbe4a9.makeis not installed on the authoring host; the commands above are the underlying ones.Credit and provenance
F-star,
cert(M), L8 labellings and the proven chain: mergedresearch/root-unit-decoder-lemmas(PR 1590 by DreamingOfClouds, with Claude Opus 5.5 (Anthropic) via Claude Code assistance). The rank-3 configuration model, the named instancestied_minandcex_min_1, their recorded one-copy certificate limits (11 and 18, CP-SAT, CHECKED (recorded)), the stored cost-22 pairing and the structural lemmas L5/SCC: DreamingOfClouds in PR 2111 and PR 2162; the two data files are byte-identical copies of their data (sha256670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93and86064701dde94b4f35427bc3e19275eaf1e40e9e90d4fea28e7857f3564d4dd7). The residue statement, Lemmas SF/MP/RK/AN and the engine design this package adapts: Aaron Wang in PR 2717. Lemma MX and the class-(i) closure: Aaron Wang in PR 2747. The falsifier-census frontier (196 instances): Aaron Wang in PR 2335. Exact cost 12 oftied_min: Aaron Wang in PR 2379. Exact cost 21 ofcex_min_1: Nick Petalas in PR 2206. This package does not claim their results; the new content is the exact zero-digraph machinery, the dichromatic structure of both fixtures' zero digraphs, and the class-(ii) smallest-first search with its exact obstruction record.Prepared by Aaron Wang with help from opencode (substantial AI assistance; no independent human review claimed). New work in this package is Apache-2.0. No kappa, supplier, or frontier claim.