feat(bg): additive-subaction ceiling — mixed-config tail closed for d=6, d∈[10,61], d≥65 - #210

Merged

DrMurphyIsIn merged 50 commits into

mainfrom

Sep 6, 2026

Commits on Sep 3, 2026

feat(bg-lean): d=2 per-hub decouple residual PROVEN (nlinarith core of FlowedHubStep)

Dr. Murphy
and
claude
committed
56165c7
feat(bg-lean): all 5 per-hub decouple residuals d=2..6 PROVEN (nlinarith core done)

Dr. Murphy
and
claude
committed
feac4e1
feat(bg-lean): list machinery (child_bell_sum_le) + docstring sorry-scan fix

Dr. Murphy
and
claude
committed
4103c6c
feat(bg-scl): hub_le_d3 — d=3 hub connection (tangent+child-sum+decouple bridge)

Dr. Murphy
and
claude
committed
53e3df9
feat(bg-scl): hub_le_d4/d5/d6 — hub connections for degrees 4,5,6

Dr. Murphy
and
claude
committed
6481e96
feat(bg-scl): hub_le_d2 — single-child hub (leaf=cherry / non-leaf decouple)

Dr. Murphy
and
claude
committed
8c59605
feat(bg-scl): d>=7 ceiling + FlowedHubStep assembly -> SCL from branch ceiling

Dr. Murphy
and
claude
committed
58fd600
feat(bg-scl): joint ceiling+SCL induction -> single per-hub CeilStep obligation

Dr. Murphy
and
claude
committed
8a56854
feat(bg-scl): PROVE the branch ceiling for d<=6 (incl. the d=6 arithmetic tie)

Dr. Murphy
and
claude
committed
c21377a
feat(bg-scl): per-child budget lemmas toward CeilStepHi (closes 7<=d<=15; d>=16=TieSlack)

Dr. Murphy
and
claude
committed
86f6f83
feat(bg-scl): the g-step<->Branch BRIDGE -- classical ceiling reduced to ONE message inequality (GStep)

Dr. Murphy
and
claude
committed
1d98893
feat(bg-scl): PIECE 1 SOLVED (master<=glemma) + sharpened bridge -> ceiling reduces to glemma + Le1Step

Dr. Murphy
and
claude
committed
a13baa5
docs(bg): REFUTE Le1Step (the CappedJoint <=1 step) -- exact counterexample

Dr. Murphy
and
claude
committed
db73b31
docs(bg): additive SUBACTION closes the ceiling core -- explicit verified witness

Dr. Murphy
and
claude
committed
fbfe887
feat(bg): kernel-green additive SUBACTION bridge + first compact-core cell

Dr. Murphy
and
claude
committed
8a7bbcf
feat(bg): first TIGHT compact-core subaction cell (deg-4/deg-3) kernel-green

Dr. Murphy
and
claude
committed
b669f00
feat(bg): instantiate validated witness -> single conditional ceiling theorem

Dr. Murphy
and
claude
committed
9b68014
feat(bg): first cells of IsSubaction rho_wit (leaf base + cherry tie leg)

Dr. Murphy
and
claude
committed
586391c
feat(bg): d=2 node cells -- message bound + first infinite-family cell

Dr. Murphy
and
claude
committed
7245a3c
feat(bg): degree-2 node with deg-2 child cell (the delicate mid case)

Dr. Murphy
and
claude
committed
827d9a9
feat(bg): tight-route log-enclosure for the deg-2/deg-3-child cell (Telperion emit_log_combination)

Dr. Murphy
and
claude
committed
50be077
feat(bg): unified deg>=3-child cell -- degree-2 node CLOSED via emitter enclosure

Dr. Murphy
and
claude
committed
b936f80
feat(bg): first multi-child cell -- degree-3 broom (two leaf children)

Dr. Murphy
and
claude
committed
e051831
feat(bg): first genuine multi-child decouple SUBACTION cell (deg-3 hub, two deg>=3 children)

Dr. Murphy
and
claude
committed
c4688d5
docs(bg): consolidated SUBACTION ceiling handoff

Dr. Murphy
and
claude
committed
ef6dae6
feat(bg): axiom-guard the additive SUBACTION reduction chain + discharged cells

Dr. Murphy
and
claude
committed
80e51d1
docs(bg): Telperion handoff -- enclosure atoms for next IsSubaction cells

Dr. Murphy
and
claude
committed
d8edba0
feat(bg): deg-3 leaf/deg-2 subaction enclosure atoms (Telperion emit_log_combination)

Dr. Murphy
and
claude
committed
84a3d3f
docs(bg): correct enclosure-atom route labels to match delivered atoms

Dr. Murphy
and
claude
committed
aeb5dda
feat(bg): complete the degree-3 IsSubaction cell family + solve cell (D)

Dr. Murphy
and
claude
committed
378186e
docs(bg): spec for d=4 profiles, deg>=5 tail, and the 27*23 tie identity

Dr. Murphy
and
claude
committed
a5e2987
feat(bg): d=4 atoms (all 35), 27*23 tie identity, and tail_all_deg4 crux

Dr. Murphy
and
claude
committed
9ba7020
feat(bg): tail_all_deg2 (the tie family) + tail_all_deg3 -- all three uniform tail families proven

Dr. Murphy
and
claude
committed
0c3b431
feat(bg): reduce-to-uniform message half for the deg-2 (tie) family

Dr. Murphy
and
claude
committed
4878475
docs(bg): consolidated additive-SUBACTION ceiling handoff

Dr. Murphy
and
claude
committed
8d2a2ae
docs(bg): take ownership -- correct consolidated handoff after independent verification

Dr. Murphy
and
claude
committed
4cccb32

Commits on Sep 4, 2026

docs(bg): DISSOLVE the tail counts-exchange 'research nub' via the tangent-decouple

Dr. Murphy
and
claude
committed
a626845
feat(bg): tail DECOUPLE backbone in Lean -- reduces mixed-degree tail cells to per-child + B>=0

Dr. Murphy
and
claude
committed
c6a9257
docs(bg): note the tail decouple backbone is now kernel Lean (tail_decouple)

Dr. Murphy
and
claude
committed
be40996
feat(bg): close the d=6 (tie) tail cell for ARBITRARY children via tail_decouple

Dr. Murphy
and
claude
committed
8d9fbb6
feat(bg): close the INFINITE tail (deg >= 65, arbitrary children) via tail_decouple

Dr. Murphy
and
claude
committed
c607833
feat(bg): close the deg-4 tail range cell d in [10,61] via tail_decouple

Dr. Murphy
and
claude
committed
5253c50
docs(bg): consolidate handoff -- mixed-config tail closed for d=6, d in [10,61], d>=65

Dr. Murphy
and
claude
committed
1fd911e
wip(bg): subaction_perm + deg1/2/3 dispatch arms (deg4/tail placeholders for Wave 2)

Dr. Murphy
and
claude
committed
e3ff713
feat(bg): 35 deg-4 IsSubaction node cells (wire d4_* atoms)

Dr. Murphy
and
claude
committed
0f52277
feat(bg): tail stragglers (d∈{5,7,8,9,62,63,64}) + tail_wrapper

Dr. Murphy
and
claude
committed
beb5c4c
Merge branches 'bg/scl-d4cells' and 'bg/scl-tailwrap' into bg/scl-dispatch
Dr. Murphy
committed
838af8d
feat(bg): complete IsSubaction ρwit dispatch (deg-4 + tail) + bg_ceiling capstone

Dr. Murphy
and
claude
committed
7e51a89
feat(bg): close the additive-SUBACTION ceiling -- bg_ceiling axiom-clean

Dr. Murphy
and
claude
committed
a203967
docs(bg): mark classical-branch ceiling CLOSED (bg_ceiling axiom-clean, CI green)

Dr. Murphy
and
claude
committed
c4b0a00