feat(bg): additive-subaction ceiling — mixed-config tail closed for d=6, d∈[10,61], d≥65 - #210
Open
DrMurphyIsIn wants to merge 50 commits into
Open
feat(bg): additive-subaction ceiling — mixed-config tail closed for d=6, d∈[10,61], d≥65#210DrMurphyIsIn wants to merge 50 commits into
DrMurphyIsIn wants to merge 50 commits into
Conversation
…f FlowedHubStep) Discharges the Telperion PerHubDecoupleResidualCertificate in Lean for d=2 (sorry-free, axiom-clean [propext, Classical.choice, Quot.sound], builds locally). The "highest-risk nlinarith" technique, validated end-to-end: - log76_gap: log(7/6) - F* <= -1/22, via 11*(...) = log((7/6)^11 * 64/621) (combined into ONE log of a rational) bounded by the clean half-integer exp(1/2)=sqrt(exp 1) < 1.6489. - decouple_d2: R(S) <= 0 on S in [0,1/2], mu in I -- clear the mu/(2+S) division via the inverse-as-atom, then nlinarith on the upward parabola in S. d=3..6 follow the SAME template (different rational constants). This is the core of FlowedHubStep's d<=6 tangent decouple; wiring the list machinery + hbroom + leaf + child-IH + d>=7 ceiling is next. NOTE: local Lean builds work again (M3 Ultra 22-day uptime, no crash; ~4s/module) -- the Aug-9 SoC-watchdog CI-only constraint is resolved. conjecture1_proved = False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…ith core done) decouple_d2..d6 + log_gap_d3..d6: the SCL per-hub decouple residual R(S)<=0 for every hub-degree 2..6, sorry-free, builds locally. d=2 uses exp(1/2); d=3 log_nonpos; d=4,5,6 log_le_sub_one_of_pos on the combined log(X_d) rational. Discharges the Telperion PerHubDecoupleResidualCertificate. Next: list machinery + tangent connection + hbroom/leaf legs + d>=7 ceiling => FlowedHubStep. conjecture1_proved = False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…can fix child_bell_sum_le: from per-child SCL at price nu, the sum bound Sigma bell(c) <= |cs|*bV_nu(cherry) - nu*S (via list induction). Feeds bell_node_tangent + bY_node + decouple_d for the d<=6 hub connection. FINDING: d>=7 case needs the branch ceiling bell(node cs)<=0, which is NOT yet formalized in the SCL Lean (a separate result). conjecture1_proved = False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…ple bridge) Clean bridge: hRHS (inequality chain via bell_node_tangent + child_bell_sum_le) + hbridge (algebraic identity RHS - bVcherry = decouple_d3 LHS, via ring with muPP expanded and mu/(3+S) a shared atom) + linarith with decouple_d3. Builds axiom-clean. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
Uniform tangent pattern (s0=(d-1)/3, log inner (4d-1)/(3d), denom (4d-1)/3). d=5,d=6 route through the uniform decouple_d5/d6. d=4's pre-existing decouple lemma uses a non-uniform normalization (muS/16, -1/4), so the uniform d=4 residual is proven inline via log_gap_d4 (same nlinarith structure). All axiom-clean. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…couple) d=2 splits: leaf child => node [node []] = cherry (le_of_eq rfl); non-leaf child => bY<=1/2 (bY_nonleaf_le_half) so S<=1/2, decouple_d2 with child IH at muPP 2 mu in I. All degree cases d=2..6 now closed. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…h ceiling
- cherry_ceiling_gap: log(3/2)-2F* >= -1/50 (two_le_log_gap too loose; combine to
log(354294/385641), lower-bound via log x >= 1-1/x on the inverse).
- hub_le_highdeg: d>=7 hub bV_mu(node cs) <= bell + mu/7 <= bVcherry, using the
branch ceiling bell(node cs)<=0 (hypothesis) + bY<=1/7 + cherry_ceiling_gap.
- flowed_hub_step_of_ceiling: case-split cs.length {1..5}->hub_le_d2..d6, >=6->highdeg,
giving FlowedHubStep from the single global obligation (all b, bell b <= 0).
- scl_of_ceiling: chains into scl_of_flowed_step -> SCL for every non-leaf branch.
All axiom-clean [propext, Classical.choice, Quot.sound], no sorry. Bullets 3/4/5 done.
The SCL is now reduced to ONE clean hypothesis: the branch ceiling. conjecture1_proved=False.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…obligation FINDING: the branch ceiling (all b, bell b <= 0) is NOT a separate open obligation. Per the BG upper-bound ledger (bg_upper_bound.py), it and the SCL are ONE joint well-founded induction; all 10 arithmetic legs are GATED (verified: gated_ok=True, sole open = 2b-lo-scl-induction, the recursion). Numerics: the ceiling is TIGHT (=0) at n=11 deg-6 (the 23-adic arithmetic tie); d>=7 has margin +0.0015; the SCL bound alone can't close the tail (needs the M_d envelope, which IS gated). - CeilStep: per-hub ceiling step (child ceilings + child SCL => hub ceiling) = ledger step 1b / M_d frontier, gated by MdStep/NearBroomUnimodal/HighDegreeTail/BroomOptimum. - ceil_and_scl_of_ceilStep: ONE strong induction proving bell b<=0 AND PSCLne b jointly. d<=6 SCL via hub_le_d2..d6 (child SCL from IH), d>=7 via hub_le_highdeg (hub ceiling from the just-proved CeilStep). Eliminates the free-floating (all b, bell b<=0) hypothesis: the d>=7 leg now draws the ceiling from the JOINT IH. - bell_ceiling_of_ceilStep / scl_of_ceilStep: corollaries. Sole residual now matches the ledger's single open piece exactly. Axiom-clean, no sorry. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…etic tie) New R3Cert/BGSCLCeil.lean discharges CeilStep for root-degree d<=6, leaving only the d>=7 tail. KEY: the concave-log tangent at the EXACT all-cherry slope mu*=3/(4d-1) (which lies in the invariant interval I for d<=6) makes the child S-terms cancel EXACTLY against the child SCL bound, giving bell(node cs) <= A_d = (d-1)(log(3/2)-2F*) + log((4d-1)/(3d)) - F*. - acl_d2..d6: A_d <= 0 as clean rational log inequalities (11x-clear + log_nonpos on (3/2)^(11(d-1))*((4d-1)/(3d))^11*(64/621)^(2d-1) <= 1). d=6 is EXACTLY the tie (3/2)^5*(23/18) = 621/64 -> A_6 = 0. This is the n=11 deg-6 23-adic crux, now IN LEAN. - bell_cherry_nonpos, ceil_hub_d2..d6: the per-degree ceiling (leaf child -> hub=cherry; non-leaf -> all-cherry decouple + child SCL at mu* in I via leaf_le_cherry/PSCLne). - CeilStepHi: the d>=7 hub-ceiling residual (mu*=3/(4d-1) < I-floor for d>=7; SCL-on-I overshoots ~0.004; margin +0.0015; gated in Telperion by HighDegreeTail + near-broom). - ceilStep_of_hi / ceil_and_scl_of_ceilStepHi: assemble -> the ENTIRE branch ceiling AND SCL for every branch reduces to CeilStepHi. The tight crux is proven; residual is the tail. All axiom-clean [propext, Classical.choice, Quot.sound], no sorry. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…=15; d>=16=TieSlack) Attacked the d>=7 hub-ceiling residual via the all-cherry mu*=3/(4d-1) tangent + SHARP per-degree ceiling cbound. CORRECTION: cbound(2)=log(3/2)-2F* (the cherry), NOT A_2 -- A_k is the true per-degree max for all k EXCEPT k=2 (verified over 376k branches). With correct cbounds + deg-2 SCL extend-below-I, the decouple closes EXACTLY for 7<=d<=15. d>=16 hits the SCL-below-I wall (mu* below crossover; incompatible bell-max/y-max for low-degree children) = the genuine TieSlack regime, matching the BG ledger's k>=16 split. New R3Cert/BGSCLCeilHi.lean (axiom-clean, no sorry): key_d2..d6 (7*A_k+1/k<=F*) via a reusable exp-enclosure (exp(11/k)^k=(exp 1)^11 < 2.7182818286^11 <= r_k^k, small r_k, then W_k*r_k<=1 by norm_num -- avoids huge powers); k=5,6 via A_k<=0 + 1/k<=F*; recip5_le_fstar. HONEST: these are NECESSARY infrastructure but do NOT discharge CeilStepHi -- the d>=16 tail (TieSlack) remains the open piece. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
… to ONE message inequality (GStep) The recursion-assembly (ii) that no file on main had: connects the CappedJoint g-step machinery to the concrete classical branch ceiling bell b <= 0. - Gf b := exp(11*bell b) (= btotal^11*(64/621)^|b|); Gf b<=1 <=> bell b<=0. - Gf_node: the cavity recursion in product form, Gf(node cs)=(64/621)*(1+S/d)^11*prod Gf(c) (exp of bell_node; no division -- three-term sum with exp(-(11 F*))=64/621). - capB(mu)=min(masterUb,glemmaUb,1); capB_le_one; capB_one=64/621 (leaf/arm). - bY_achievable: the message bY(c) is Achievable (bY_leaf=1, bY_nonleaf<=1/2). - ceiling_of_gstep (hstep : GStep) : forall b, bell b <= 0 -- THE BRIDGE. Well-founded recursion proves the capped invariant Gf b<=capB(bY b) for EVERY branch (leaf: Gf=64/621=capB 1; hub: child IH + Gf_node + list_prod_mono + GStep with achievable child messages), then capB<=1. GStep (the per-hub W*a^11*prod capB <= capB(mu_hub), the CappedJoint STEP<=1, tight only at the d=6 tie which acl_d6 already nails) is the SINGLE explicit hypothesis -- the honest remaining obligation, NOT proven here. Axiom-clean [propext,Classical.choice,Quot.sound], no sorry. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…eiling reduces to glemma + Le1Step
PIECE 1 (masterUb-general): SOLVED, but not as a separate master proof -- it turns out
glemmaUb(mu) <= masterUb(mu) for ALL mu<=1/2 (every hub message). So the master cap is a
le_trans off the (proven) glemma cap; no independent master argument is needed.
- glemmaUb_le_masterUb {mu} (0<=mu) (mu<=1/2): glemmaUb mu <= masterUb mu. Via
(3+mu)/(2+mu) >= 7/5 <=> mu<=1/2, and (64/621)(5/3)^11 <= (7/5)^11 (int 64*25^11<=621*21^11).
SHARPENED BRIDGE: gstep_of_glemma_le1 (GlemmaStep) (Le1Step) : GStep, and
ceiling_of_glemma_le1 : GlemmaStep -> Le1Step -> forall b, bell b <= 0. So the whole classical
BG ceiling now reduces to just TWO per-hub message inequalities: GlemmaStep (= CappedJoint
gstep_le_one_achievable, PROVEN in Q, all arities) and Le1Step (piece 2). Master subsumed.
PIECE 2 (<=1 step, Le1Step): W*a^11*prodBcap<=1. Isolated as the SOLE open obligation. It is
NOT implied by glemma when the hub message <0.306 (there both caps>1); for message>=0.306 it
DOES follow from GlemmaStep. The residual is the small-message/large-hub tie region, TIGHT at the
d=6 all-cherry 27*23=621 tie (acl_d6) -- the M_d frontier. Not closed here.
Axiom-clean [propext,Classical.choice,Quot.sound], no sorry. conjecture1_proved=False.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…xample Le1Step (W*a^11*prod Bcap <= 1, the '1' leg of Bcap) is FALSE, not just unproven: a hub with 3 children each at message 13/42 (reachable deg-3 branch) gives W*a^11*Bcap^3 = 1.006 > 1 exactly, rising to 1.25 at j=5. Root cause: Bcap is too loose in the mid-band mu in (0.30,0.45) -- a real branch at bY=0.31 has Gf~0.20 but Bcap(0.31)=0.994. Consequences: (1) my bridge ceiling <== GlemmaStep and Le1Step is a valid reduction to a FALSE hypothesis, so it can't close the ceiling; (2) refutes the parallel session's CappedJoint candidate -- its <=1 step is false (the n<=15 census missed it because actual small trees have linked Gf/message); (3) the ceiling is still TRUE, and the true envelope env(mu) DOES satisfy the step with margin -- closing it needs a cap tighter than Bcap in the mid-band = the M_d frontier. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…fied witness Reframe the branch ceiling via the ergodic-optimization additive subaction (SUB): e_v + rho(v) <= sum_c rho(c), rho>=0, which telescopes to bell b <= -rho(root) <= 0. Additive (sum) structurally avoids the multiplicative overshoot that made Le1Step FALSE. Found an EXPLICIT affine-per-degree witness: rho(leaf)=F*, rho(2,mu) through the cherry anchor 2F*-log(3/2), rho(3,mu) small, rho(d>=4)=0. VERIFIED on all 376,464 branches n<=16 (worst margin -4e-6) AND the continuous interior grid (worst +1e-6, tail slack +0.022). Only 3 constraints are tight = exactly the tie's 3 states; consistency is the exact 27*23=621 identity; everything else is free rational slack. Reduces the ceiling to: (1) a Lean additive bridge (provable now), (2) finitely many compact-core per-cell affine-endpoint + log-enclosure inequalities, (3) a high-degree tail lemma, (4) the exact tie identity. Dispelled: aperiodicity and a hard tail. Empirically decisive, NOT yet kernel-proven; no sorry discharged. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
… cell BGSCLSubaction.lean, axiom-clean [propext, Classical.choice, Quot.sound], no sorry: - ceiling_of_subaction : (rho>=0 and IsSubaction rho) -> forall b, bell b <= 0. The additive analog of ceiling_of_gstep. Since bell b = sum_v e_v telescopes (bell_node), a subaction rho>=0 with per-vertex e_v + rho(v) <= sum_child rho(c) gives bell b <= -rho(root) <= 0 by scl_of_child_step strong induction (invariant bell b + rho b <= 0). Being a SUM it structurally cannot incur the multiplicative overshoot that makes the capped-product step Le1Step FALSE. - subaction_cell_broom_d4 : the FIRST compact-core cell of the empirically-verified affine-per-degree witness (rho(leaf)=F*, rho(deg>=4)=0) against the kernel -- the deg-4 all-leaf (broom) corner, (SUB) content log(7/4) <= 4*F*, discharged by log-monotonicity reduced to the rational (7/4)^11 <= (621/64)^4 (norm_num). This is the all-children-maximal message-endpoint corner. Witness + reduction, NOT a closed ceiling: the full per-cell certificate family over the compact deg<=6 core (affine-in-mu endpoint + log(1+S/d) enclosure) and the high-degree tail lemma remain. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…l-green Adds to BGSCLSubaction.lean (axiom-clean [propext,Classical.choice,Quot.sound], no sorry): - rho3 mu := (1/8)(mu - 1/5): the rational, tie-free degree-3 line of the witness. Verified globally: rho(leaf)=F*, rho(2,mu)=2F*-log(3/2)+(1/4)(mu-1/3), rho(3,.)=rho3, rho(deg>=4)=0 gives a valid subaction on all branches n<=14 (worst margin 0, tight only at the leaf). b3=1/8, b2=1/4 are clean choices in the wide valid range. - log54_sub_fstar_le : log(5/4) - F* <= 1/20, via log x <= x-1 at x=(5/4)^11*(64/621)~1.20 (clearing 11*F*=log(621/64)). The log-enclosure. - subaction_cell_d4_d3 : the FIRST TIGHT cell -- (SUB) at a deg-4 hub (rho=0) with three deg-3 children (y_i in [1/5,1/3]): (log(1+(sum y)/4) - F*) + 0 <= sum rho3(y_i). Margin ~0.033, the binding class (far tighter than the broom corner). Proof = the two tools the full certificate needs: the concave-log TANGENT at the aggregate endpoint S=1 (log_tangent) collapsing the 3-var box to the message endpoint, plus the log-enclosure. This is the pattern the whole per-cell family reduces to (tangent-endpoint + enclosure), now kernel-tested on the tight class. Witness + reduction, NOT a closed ceiling: the full cell family, tail lemma, tie identity, and witness instantiation remain. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
… theorem CORRECTION + instantiation in BGSCLSubaction.lean (axiom-clean, no sorry): The earlier affine-per-degree witness (rho(deg>=4)=0, rho3 slope 1/8) was found to FAIL the high-degree-parent tail: a deg-D hub with deg-4 children at message ->1/4 has e_node>0, RHS=0 (verified: deg-50 gives -0.011). Only d=2,3,4 have e_tail=log(1+1/d)-F*>0, so rho must be positive there and vanishes for d>=5. Earlier cells/log-lemmas stay TRUE isolated inequalities but aren't cells of a globally-valid witness. CORRECTED witness rho_wit (thoroughly validated: enumerated n<=15 + tail to deg-140 + spider family k=3..12 + 120k mixed high-degree trees, margin 0 tight only at the 27*23 tie, rho>=0), clean rationals except the two tie anchors F*, log(3/2): rho(leaf)=F*, rho(2,mu)=2F*-log(3/2)+(1/4)(mu-1/3), rho(3,mu)=mu/32, rho(4,mu)=mu/384, rho(deg>=5)=0. New kernel-green pieces: - bY_le_one, bY_deg2_ge_third (message bounds for nonnegativity) - fstar_nonneg, cherry_anchor_nonneg (2F*-log(3/2)>=0 via (621/64)^2>=(3/2)^11, F*-folded) - rho_wit : Branch -> R (the validated witness, keyed by bcc/degree + bY) - rho_wit_nonneg : forall b, 0 <= rho_wit b - ceiling_of_witness : IsSubaction rho_wit -> forall b, bell b <= 0 This reduces the whole branch ceiling to the SINGLE explicit obligation IsSubaction rho_wit (the finite per-cell family over the compact deg<=4 core + the deg>=5 => rho=0 tail), against a concrete thoroughly-validated witness, with nonnegativity discharged. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…leg)
Start discharging the remaining obligation IsSubaction rho_wit, kernel-green + axiom-clean:
- rho_wit_leaf : rho_wit(leaf) = F*.
- subaction_nil : the leaf-node cell (cs=[], degree 1) -- (log 1 - F*) + F* = 0 <= 0, the
trivial base of the family.
- subaction_cherry : the cherry cell (cs=[leaf], degree 2, one leaf child) -- bY(leaf)=1,
bY(node)=1/3, rho_wit(node)=2F*-log(3/2), giving (log(3/2)-F*)+(2F*-log(3/2)) <= F*, i.e.
F* <= F* -- the EXACT tie leg (equality), the 27*23 identity's degree-2 face.
IsSubaction rho_wit remains a finite per-node family: node degree d in {1,2,3,4} with arbitrary
child-degree mixes + the d>=5 => rho=0 tail, each cell a tangent-endpoint reduction + F*-folded
log-enclosure (emitter-backed by curvature_boundary + log_combination). These two anchor the
base and the tie. conjecture1_proved=False.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
More cells of IsSubaction rho_wit, kernel-green + axiom-clean: - bY_le_inv_deg : bY b <= 1/(bcc b + 1) = 1/deg (reusable message-by-degree bound). - d2_deg5_enc : log(11/15) + F* + 1/24 <= 0, via log x <= x-1 at x=(11/15)^11*(621/64)~0.32, F*-folded (the log-enclosure for the deg-2/deg>=5 cell). - subaction_deg2_deg5child : the degree-2 node with ANY deg>=5 child. Since such a child has rho_wit=0 and message <=1/5, the local excess is already <0: (log(1+bYc/2)-F*)+rho_wit(node) <= log(11/10)-F*+[2F*-log(3/2)+1/24] = log(11/15)+F*+1/24 <= 0. Covers infinitely many child degrees (5,6,7,...) uniformly in one cell. IsSubaction rho_wit progress: leaf base, cherry tie leg, and now the d=2/deg>=5 family done. Remaining d=2 sub-cases: deg-2 child (delicate tangent at 1/2), deg-3/deg-4 children (finer log-enclosure near threshold); then node degrees 3,4 and their tails. Emitter-backed. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
More cells of IsSubaction rho_wit, kernel-green + axiom-clean:
- log54_sub_fstar_le' : log(5/4)-F* <= 1/55 (tighter than the 1/20 version; via log x<=x-1
at x=(5/4)^11*(64/621)~1.1998, F*-folded) -- the thin enclosure this cell needs.
- bY_ge_third_of_bcc1 : a deg-2 branch has message >= 1/3.
- subaction_deg2_deg2child : the degree-2 node with a deg-2 child (bY c in [1/3,1/2]). The
delicate mid case (razor-thin margin): after cancelling the shared 2F*-log(3/2)-(1/4)/3,
reduces to log(1+y/2)-F*+(1/4)/(2+y) <= (1/4)y, closed by the concave-log TANGENT at y=1/2,
the convex SECANT bound 1/(2+y) <= 3/7-(6/35)(y-1/3) (keeps it affine), and log54_sub_fstar_le'.
IsSubaction rho_wit: node degree 1 done; node degree 2 done for child degrees {1(leaf),2,>=5}.
Remaining d=2 sub-cases: deg-3, deg-4 children (need finer degree-3 log-enclosure, = emitter
transcendental_enclosure); then multi-child node degrees 3,4 (tangent decouple) + the >=5 tail.
conjecture1_proved=False.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…elperion emit_log_combination) log79_add_fstar : log(7/9) + FSTAR + 1/24 <= 0 -- the analytic core the degree-2 node / degree-3 child subaction cell needs, where log x <= x-1 is too loose. Telperion route='tight' (log X <= Q via X <= exp Q + degree-3 Taylor exp upper, Real.exp_bound'). Kernel-GREEN against R3Cert.BGSCLInduction (lake build, 8656 jobs). Drop-in for the deg-3-child cell. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DRASsvp3tERc662HjyVdbc
…er enclosure Uses the parallel session's emitter-generated tight-route enclosure (log79_add_fstar : log(7/9)+F*+1/24<=0, Telperion emit_log_combination route='tight', merged from bg/scl-tight-enclosure) to close the degree-2 node completely: - subaction_deg2_highchild : the degree-2 node with ANY deg>=3 child. Since bY c <= 1/3 there, LHS <= log(7/6)-F*+[2F*-log(3/2)+1/24] = log(7/9)+F*+1/24 <= 0 <= rho_wit c. One cell covers child degrees 3,4,5,... -- subsumes subaction_deg2_deg5child and handles the deg-3/deg-4 children the degree-1 tangent (log x<=x-1) could NOT (their fold sits at x~0.611 where x-1~-0.389 overshoots the needed -0.458; the degree-3 exp enclosure closes it). IsSubaction rho_wit: node degrees 1 and 2 now COMPLETE (leaf/cherry + deg-2 + all deg>=3). The cross-front convergence lands in the kernel: my cell + their emitter enclosure compose axiom-clean [propext,Classical.choice,Quot.sound]. Remaining: multi-child node degrees 3,4 (tangent decouple over S=sum bY(c)) + the >=5 tail. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
- log53_enc : log(5/3) + 1/160 <= 3*F* (monotone route, comfortable margin). - subaction_broom_d3 : the degree-3 node with two leaf children. bY(node)=1/5, rho_wit(node)=1/160; inequality (log(5/3)-F*)+1/160 <= 2F*. A fixed-point 2-child enclosure (messages pinned, no decouple), pinning the two-child list mechanics (map/sum over 2 elements, rho_wit for a 2-child node) that the decouple cells reuse. IsSubaction rho_wit: node degrees 1,2 complete; first 2-child cell (d=3 broom) done. Remaining: the genuine multi-child DECOUPLE cells (variable child messages, tangent at all-cherry reference splitting S=sum bY(c) per-child) for node degrees 3,4 + the >=5 tail. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…b, two deg>=3 children) subaction_deg3_highchildren : (log(1+S/3)-F*) + rhowit(node[c1,c2]) <= rhowit c1 + rhowit c2 for bcc c1,c2 >= 2 (bY ci in [0,1/3]). The first cell needing the concave-log DECOUPLE over a free 2-variable message box: log_tangent at the aggregate endpoint S=2/3 -> slope line log(11/9)+(3/11)(S-2/3), node-rho bound <= 1/96, the Telperion enclosure atom log119_sub_fstar (log(11/9)-F* <= -1/200), and a per-child rho lower bound (deg 3/4/>=5 split). Kernel-GREEN + axiom-clean [propext, Classical.choice, Quot.sound] against the real R3Cert.BGSCLInduction/BGSCLSubaction (lake build, 8658 jobs). Pins the decouple-assembly pattern for the remaining d=3/d=4 multi-child family. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DRASsvp3tERc662HjyVdbc
Consolidates the session's BG classical-ceiling work: the kernel-complete reduction chain (ceiling_of_subaction -> ceiling_of_witness -> single obligation IsSubaction rho_wit), the validated witness rho_wit, the full per-cell map (node degrees 1,2 + single-child spine COMPLETE; d=3 broom + first genuine decouple cell done), the proven spec->emitter->assemble round-trip protocol, the three enclosure regimes (monotone/tangent/tight), the slope-matching s0 trick, and ready-to-generate next-cell specs (deg-3 two-deg-2-children with the tight route inside the decouple; d=4; deg>=5 tail; the 27*23 tie). conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…rged cells Wire the current live ceiling line into AxiomGuard.lean so the "kernel-green, axiom-clean" claim is machine-enforced by CI (not just asserted in the handoff). Guards ceiling_of_subaction, ρwit_nonneg, ceiling_of_witness (the reduction chain that collapses the classical branch ceiling to the single obligation IsSubaction ρwit), plus every discharged cell (subaction_nil/cherry/deg2_deg2child/ deg2_highchild/broom_d3/deg3_highchildren). All 12 verified locally to depend on exactly [propext, Classical.choice, Quot.sound] -- no sorryAx. conjecture1_proved = False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JzHTerQF58GdEHfTty8GNt
…ells Specs for the parallel Telperion session to build emit_log_combination atoms: 3 READY exact atoms (deg3-two-deg2 tight q=79/96; deg3-leaf+deg2 monotone; deg3-leaf+deg>=3 monotone), each with fold X, route, 11B, and cell margin. Flags the deg2+deg>=3 two-slope obstruction (single tangent can't match both 1/4 and 3/11 slopes -> BG-side design first) + d=4 mixed / deg>=5 tail as needing BG decomposition before an atom is well-defined. Reconciles the stale cell table (broom_d4 / d4_d3 / deg2_deg5child already landed). conjecture1_proved = False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JzHTerQF58GdEHfTty8GNt
…log_combination) Three IsSubaction rho_wit enclosure atoms for the next degree-3 hub cells, from the BG->Telperion round-trip handoff (BG_SUBACTION_TELPERION_NEXTCELLS.md): deg3_deg2children_enc : 2*log(3/2)+log(4/3) - 5*FSTAR <= 79/1056 (tight_hi route) log32_sub2fstar : log(3/2) - 2*FSTAR <= -1/144 (tangent route) log139_sub2fstar : log(13/9) - 2*FSTAR <= -3/416 (tangent route) Generated by Telperion emit_log_combination; kernel-green against R3Cert.BGSCLInduction (lake build 8656 jobs), axiom-clean [propext, Classical.choice, Quot.sound], no sorryAx. Route finding: atom (A) needed a NEW emitter route "tight_hi" -- fold X~2.06 > 1 with Q=+79/96 > 0, which BOTH the degree-1 tangent (needs X-1 <= Q) and the existing tight route (requires Q < 0) miss. tight_hi discharges log X <= Q via Real.log_le_iff_le_exp plus a degree-4 Taylor LOWER bound on exp Q (Real.exp_bound). Atoms (B)/(C) are the tangent route (q<0), not monotone (which the emitter restricts to q=0). conjecture1_proved = False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017GTVuZNJ2q9yCHMkEKSM7J
Post-delivery fix to the Telperion spec. The first-draft route tags were wrong: - (A) deg3_deg2children_enc is the NEW tight_hi route (Q>0, fold X~2.06), not the existing tight route (which hard-requires Q<0, the added-F* blocker); the tangent gate x-1<=Q also fails (1.06 > 0.82). Adds tight_hi to the route list. - (B) log32_sub2fstar and (C) log139_sub2fstar are TANGENT, not monotone (monotone strictly requires q=0; the X-1<=N*q gate is the tangent gate). - Note atom A folds cleanly 2log(3/2)+log(4/3)=log 3. Rides along with the atom delivery so bg/scl-on-main merges a corrected doc. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JzHTerQF58GdEHfTty8GNt
Wires the three delivered Telperion atoms into their cells and closes the whole degree-3 hub family of IsSubaction ρwit (new R3Cert/BGSCLSubactionDeg3Mid.lean, no `sorry`, all axiom-clean [propext, Classical.choice, Quot.sound]): - subaction_deg3_deg2children (two deg-2 children) -- deg3_deg2children_enc, tangent s0=1, node-rho <= 3/352. margin +0.0091 - subaction_deg3_leaf_deg2 (leaf + deg-2) -- log32_sub2fstar, tangent s0=3/2, node-rho folded to a quadratic (div_le_iff0 + nlinarith). margin +0.0008 - subaction_deg3_leaf_high (leaf + deg>=3) -- log139_sub2fstar, tangent s0=4/3, quadratic node-rho. margin +0.038 CELL (D) SOLVED (subaction_deg3_deg2_high, deg-2 + deg>=3). The two-slope obstruction (deg-2 slope 1/4 vs deg>=3 perchild slope 3/11, single tangent can't match both, overshoots ~+0.0043) is dissolved WITHOUT a two-slope decouple: bound the high child's message <= 1/3, DROP its nonneg rho (no per-child line => no slope to match), reduce to a single-variable inequality slope-matched to the deg-2 child. Needs one new atom, dogfooded here via the tight_hi route: log2_sub3fstar : log(4/3) + log(3/2) - 3*FSTAR <= 71/960 (fold X ~ 2.2418 > 1, Q = 781/960; needs DEGREE-5 Taylor -- n=4 lower bound ~2.2114 < X; n=5 gives exp Q >= 61122928451812033/27179089920000000 >= X). AxiomGuard.lean extended: all 5 new theorems guarded, verified locally to depend on exactly [propext, Classical.choice, Quot.sound] (17 guarded total, 0 sorryAx). Full `lake build` green (8861 jobs). Updated the Telperion spec doc: cell (D) marked SOLVED, d=4 mixed profiles unblocked by the same recipe. conjecture1_proved = False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JzHTerQF58GdEHfTty8GNt
Prepares the three remaining pieces of IsSubaction rho_wit after the deg-3 family completed (378186e). All numerics verified exactly. (A) d=4 mixed profiles -- PATTERNED, ready to emit. All 35 profiles close with a single log_tangent at the binding corner (no two-slope wall: each profile's binding corner puts all children at a common message). Full 35-atom table (single-log enclosures, ALL tangent route, one monotone); post-tangent goal is linear so linarith closes each over the message box. Corrects the stale table: the old broom_d4/d4_d3 cells are for a SUPERSEDED witness, not rho_wit. (B) deg>=5 tail -- THE ONE OPEN PIECE. Refutes the naive "Sum rho >= |leaves|*F*" design (fails at 4x deg-3, no leaves, e_node>0). Worst profile per d is uniform-type (all-deg-2 for d<=9, all-deg-4 for d>=10); d=6 five-deg-2 is the exact tie. Crude bound fails until d~62, so finite+crude is impractical. Recommended design: reduce-to-uniform (exchange/convexity) + three per-type d-families (deg-4 the crux, min slack +0.0057 at d=18), each slack convex in d with one interior min, closed by a cubic-log upper bound for large d. This is a BG-side uniform induction, NOT a Telperion emit. (C) 27*23 tie identity -- subaction_cherry (done, deg-2 face) + subaction_tail_ tie_d6 (open): d=6, five deg-2 @ 1/3, EXACT identity (23/18)*(3/2)^5 = 621/64, a norm_num log-identity (not an enclosure). Subsumed by the deg-2 tail family. conjecture1_proved = False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JzHTerQF58GdEHfTty8GNt
Three deliverables, no `sorry`, all axiom-clean [propext, Classical.choice, Quot.sound]; full lake build green (8863 jobs); AxiomGuard now 24 guarded thms. R3Cert/BGSCLSubactionD4.lean -- the whole 35-atom d=4 table, DOGFOODED via one reusable lemma `tangent_atom` (the tangent-route enclosure generator, written with `zpow` so a SINGLE lemma covers every log(3/2)-fold sign) + 35 one-line applications d4_<profile>. The zpow formulation handles the (2,*) profiles' negative -kL*log(3/2) term uniformly -- no per-route special-casing needed on the Lean side. All 35 are tangent route (one monotone, (4,5,5) bound=0). R3Cert/BGSCLSubactionTail.lean: - tail_all_deg4 : the deg>=5 tail CRUX family. For d>=1, log((5d-1)/(4d)) - F* <= (d-1)/1536 (all-deg-4 hub, min slack +0.0057 @ d=18). Proof: log((5d-1)/(4d)) = log(5/4) + log(1-1/(5d)) <= log(5/4) - 1/(5d) (concavity), then the atom log(5/4)-F*<=1/55 reduces it to a rational quadratic 55d^2 - 1591d + 16896 > 0 (negative discriminant, sq_nonneg(110d-1591)). - subaction_tail_tie_d6 + tie_identity_d6 : the 27*23=621 tie. A deg-6 hub with five cherry children meets (SUB) with EXACT equality via (23/18)*(3/2)^5=621/64. conjecture1_proved = False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JzHTerQF58GdEHfTty8GNt
… uniform tail families proven Completes the three per-type uniform families of the deg>=5 tail. No `sorry`, all axiom-clean [propext, Classical.choice, Quot.sound]; full build 8863 jobs; AxiomGuard now 28 guarded thms. tail_all_deg3 (d>=1) : log((4d-1)/(3d)) - F* <= (d-1)/96 -- comfortable (min slack +0.0119 @ d=5), same concavity+quadratic recipe as deg-4; the atom log(4/3)-F*<=1/12 needed the TIGHT_HI route (fold (4/3)^11*(64/621)~2.44 > 1, n=5 Taylor), not tangent. tail_all_deg2 (d>=5, the TIE family, hardest -- EXACT equality at d=6): log((4d-1)/(3d)) <= (2d-1)*F* - (d-1)*log(3/2). Not closable by a single concavity bound over R (tight at d=6), so dispatch on the natural degree: d=5 (fold X<1), d=6 (exact 27*23 tie via tie_identity_d6), d>=7 via tail_all_deg2_large -- concavity + the quadratic q(x)=4a*x^2-4(a+p)*x+1>=0 (a=2F*-log(3/2), p=log(4/3)-F*), whose real roots are both <7, decomposed as q(x)=4a(x-7)^2 + 4(13a-p)(x-7) + (1-28(p-6a)) with two enclosures: henc_deg2_qp7 : 13a-p>=0 (direct X>=1 fold, (621/64)^27 >= (3/2)^143*(4/3)^11) henc_deg2_q7 : p-6a<=1/28 (TIGHT_HI, fold ~1.467, Q=11/28, n=4 Taylor) closed by nlinarith on q(x)>=0. Remaining tail work: the reduce-to-uniform exchange lemma (extremal child profile is uniform-type) + composing the three families into the arbitrary-child deg>=5 cell. conjecture1_proved = False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JzHTerQF58GdEHfTty8GNt
First step of the reduce-to-uniform exchange: tail_deg2_sum lifts tail_all_deg2 from "all children at the exact tie message bY=1/3" to arbitrary deg-2-child messages. For a deg-d hub (d>=5) whose d-1 children are all degree-2 with messages y_i in [1/3,1/2] summing to S: log(1 + S/d) - F* <= (d-1)*(2F*-log(3/2)) + (S - (d-1)/3)/4 [= Sum rho]. Why deg-2 is the clean case: rho_wit(deg-2,.) is AFFINE in the message (so Sum rho depends only on count and message-sum S), and the deg-2 rho-slope 1/4 dominates 1/(d+S) for every d>=5, so the SUB-slack is MONOTONE in S over the whole range (no interior extremum) -- worst at S=(d-1)/3 (the tie), reducing to tail_all_deg2. Proof: g(S)=log(1+S/d)-S/4 monotone via log((d+S)/(d+S0)) <= (S-S0)/(d+S0) <= (S-S0)/4 (Real.log_le_sub_one_of_pos + d+S0>=4). No `sorry`, axiom-clean; build 8863 jobs; AxiomGuard now 29 thms. Remaining for the full exchange: the counts->single-degree exchange across degrees, and the deg-3/deg-4 message halves (their slack is CONCAVE with a d-dependent worst endpoint, so not a single clean monotonicity like deg-2). conjecture1_proved = False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JzHTerQF58GdEHfTty8GNt
Single entry-point doc for the merged state (bg/scl-on-main @ the d=4/tail/tie/ reduce-to-uniform work). Inventories what's proven (reduction chain; deg-1/2/3 cell families complete; full 35-atom d=4 table; all three uniform deg>=5 tail families + 27*23 tie; deg-2 message half of reduce-to-uniform), the ONE remaining piece (reduce-to-uniform: deg-3/deg-4 message case-work + the counts exchange + Branch list-lift), the reusable tools (tangent_atom, tight_hi, cell-D recipe, tail recipe), and the footguns. AxiomGuard 29 thms; build 8863 jobs. conjecture1_proved = False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JzHTerQF58GdEHfTty8GNt
…ndent verification Reviewed + independently re-verified the merged additive-SUBACTION state (8 modules, 8663 jobs green, no sorry, AxiomGuard clean over 31 guarded thms, all [propext,Classical.choice, Quot.sound]). Corrections to the canonical record: - The deg-3/deg-4 reduce-to-uniform MESSAGE halves are DONE (tail_deg3_sum, tail_deg4_sum in BGSCLSubactionExch.lean) -- the doc listed them as OPEN. So the message half is CLOSED for every degree; the remaining reduce-to-uniform work is only the counts->single-degree EXCHANGE (the genuine research nub) + Branch list-lift. - Recorded the d=4 cell wiring (35 mechanical cells; atoms+recipe done) as an explicit remaining item. - NO-GO finding: log-subadditivity log(1+S/d)<=sum log(1+bYi/d) is TOO LOSSY to dissolve the counts exchange (at d=18 all-deg-4 it overshoots 0.0279 vs the exact-required 0.0111, failing by 2.5x). So the exchange must use the exact coupled log; the per-child/independence shortcut is a dead end. Recorded as a footgun. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…ngent-decouple
The one piece the consolidated handoff flagged as the genuine research nub (counts ->
single-degree exchange for mixed-degree tail configs, 'no clean Lean path yet, likely
discrete convexity/majorization') is DISSOLVED -- it is NOT discrete convexity.
The tangent-decouple does it (subadditivity was too lossy, but the tangent at a chosen S0 is
tight): for the tail node (deg d, rhowit(node)=0), from log_tangent, for ANY S0,
G(config) = sum rhowit(ci) - (log(1+S/d)-F*)
>= const(S0) + sum_i phi_{S0}(ci) >= const(S0) + (d-1)*min_c phi_{S0}(c) =: B(S0),
phi_{S0}(c)=rhowit(c)-bY(c)/(d+S0), const(S0)=F*-log(1+S0/d)+S0/(d+S0). min_c phi is a FINITE
per-degree-class check (affine in message). Choosing S0 in {(d-1)/3,(d-1)/4,(d-1)/5} gives
B(S0)>=0 for every d>=5 (tight=0 at the d=6 tie), collapsing at the self-consistent S0 EXACTLY
to the proven tail_all_deg2/deg4 families or the easy F*-log((6d-1)/(5d))>=0.
Numerically decisive: B>=0 for all d in [5,2000); 400k random mixed configs worst G=+0.025, no
violations (repro proof/docs/probes/bg_tail_counts_exchange_dissolution.py). So NO open
mathematics remains in IsSubaction rho_wit -- only the Lean assembly (per-child min lemma +
list-lift + 3-way d-split; d=4 cell wiring; top-level dispatch), all patterned. Doc updated.
conjecture1_proved=False until the chain builds sorry-free.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
… cells to per-child + B>=0
Converts the counts-exchange dissolution (paper argument) into kernel-checked Lean.
BGSCLSubactionTailDecouple.lean, axiom-clean [propext,Classical.choice,Quot.sound], no sorry,
added to AxiomGuard CI gate (now 34 guarded thms):
- sum_rhowit_ge : list-lift -- per-child affine lower bound m+sigma*bY c <= rhowit c sums to
|cs|*m + sigma*(sum bY) <= sum rhowit (structural recursion + calc).
- rhowit_node_high : rhowit(node cs)=0 for |cs|>=4 (degree>=5).
- tail_decouple : for a node of degree d=|cs|+1>=5 (rhowit(node)=0), the subaction inequality
(log(1+S/d)-F*)+0 <= sum rhowit(c) follows -- via the concave-log tangent at ANY reference S0 --
from (i) a per-child lower bound rhowit(c) >= m + bY(c)/(d+S0) and (ii) B(S0):=(d-1)*m +
[F*-log(1+S0/d)+S0/(d+S0)] >= 0. log_tangent decouples the coupled log; sum_rhowit_ge lifts.
This is the reusable core of the tail: instantiate hpc (per-degree-class min m) + hB (via the
proven tail_all_deg2/4 families) with the S0 in {(d-1)/3,(d-1)/4,(d-1)/5} d-split to close any
mixed-degree tail cell. No discrete convexity. Remaining tail work = those instantiations +
d=4 wiring + top-level dispatch. conjecture1_proved=False.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…couple) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…il_decouple First CLOSED mixed-config tail cell -- instantiates the tail_decouple backbone end-to-end. BGSCLSubactionTailDecouple.lean, axiom-clean, AxiomGuard-guarded: - cherry_anchor_le : 2F*-log(3/2) <= 1/96 (log x<=x-1 at (621/64)^2*(2/3)^11~1.088). - log32_sub_fstar_ge : 2/23 <= log(3/2)-F* (via exp(22/23)<=exp 1<2.7182818286<=(3/2)^11*64/621). - phi_lb_d6 : the per-child min at sigma=3/23 -- m+(3/23)*bY c <= rhowit c for EVERY branch, m= 2F*-log(3/2)-1/23, by a per-degree-class check (leaf via log32_sub_fstar_ge; deg 3/4/>=5 via cherry_anchor_le; deg-2 via bY>=1/3). - subaction_tail_d6 : IsSubaction rhowit at any degree-6 node (|cs|=5, ARBITRARY children) -- tail_decouple with S0=5/3 (all-cherry ref), hpc=phi_lb_d6, and B=0 = the EXACT 27*23 identity (tie_identity_d6). Closes the tie for ALL mixed child configs (not just the uniform 5-cherry one). Demonstrates the tail closure recipe end-to-end (per-child min -> tail_decouple -> family/tie). The remaining tail regimes (S0=(d-1)/4 for d in [10,61], S0=(d-1)/5 for d>=62, and d=5,7,8,9) are the same instantiation with their per-child min m + tail_all_deg4 / easy bound. conjecture1_proved=False. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
… tail_decouple
Closes the entire infinite part of the IsSubaction rho_wit tail. BGSCLSubactionTailDecouple.lean,
axiom-clean, AxiomGuard-guarded:
- cherry_anchor_ge : 1/500 <= 2F*-log(3/2) (via 1-1/X <= log X at X=(621/64)^2*(2/3)^11~1.088).
- phi_lb_general : the per-child min for the deg-5-min regime -- for any sigma in (0,5/384],
(-sigma/5)+sigma*bY c <= rhowit c for EVERY branch (m=-sigma/5), by the per-degree-class check
(leaf/deg-2 via an inline F*>=7/100 + cherry_anchor_ge; deg-3 sigma<1/32; deg-4 sigma<=5/384;
deg>=5 bY<=1/5). Reusable across the whole large-d range.
- subaction_tail_deg5 : IsSubaction rho_wit at ANY node of degree d=|cs|+1 >= 65 with ARBITRARY
children -- tail_decouple at the all-deg-5 reference S0=|cs|/5, hpc=phi_lb_general, and
B = F*-log((6d-1)/(5d)) >= 0 (log(6/5) <= F* since (6/5)^11 <= 621/64). The two B-terms
(|cs|*m and S0/(d+S0)) cancel exactly.
So the tail is now closed for d=6 (tie) AND all d>=65 (infinite). Remaining: the FINITE middle
d in {5,7,8,9} (cherry regime, hB=tail_all_deg2) and d in [10,64] (deg-4 regime, m=1/1536-sigma/4,
hB=tail_all_deg4) -- same tail_decouple pattern, with boundary-thin enclosures. conjecture1_proved=False.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
Closes 52 more tail d-values (the big finite chunk). BGSCLSubactionTailDecouple.lean, axiom-clean,
AxiomGuard-guarded:
- cherry_anchor_ge_tight : 3/400 <= 2F*-log(3/2) -- the TIGHT anchor bound the deg-4 regime's d=10
boundary needs (log x>=1-1/x is too loose there). Uses the exact 2F*-log(3/2)=(1/11)log(529/486)
(529/486=(621/64)^2(2/3)^11, the 27*23 structure) + a degree-3 Taylor bound exp(33/400)<=529/486
(Real.exp_bound).
- phi_lb_deg4 : per-child min for the deg-4-min regime, sigma in [5/384,4/49], m=1/1536-sigma/4, by
the per-degree-class check (deg-2 via cherry_anchor_ge_tight; deg-3 by a sigma<1/32 vs >1/32 split;
deg-4 tight; deg>=5 sigma>=5/384; leaf inline F*>=7/100).
- subaction_tail_deg4 : IsSubaction rho_wit at ANY node of degree d in [10,61] with ARBITRARY children
-- tail_decouple at S0=|cs|/4, hpc=phi_lb_deg4, hB=tail_all_deg4 (the two B-terms collapse to
|cs|/1536, log(1+S0/d)=log((5d-1)/(4d))).
Tail now closed for d=6 (tie), d in [10,61] (deg-4), d>=65 (deg-5). Remaining: d in {5,7,8,9}
(cherry) + d in {62,63,64} (boundary) = 7 values, then the rcases wrapper. conjecture1_proved=False.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
…in [10,61], d>=65
Update the consolidated handoff to reflect the tail-cell closures (tail_decouple + subaction_tail_d6/deg4/deg5
+ phi_lb_* + cherry_anchor_ge_tight): the mixed-config tail (arbitrary children) is now closed for the tie (d=6),
the deg-4 regime d in [10,61] (52 values), and the INFINITE deg-5 tail (d>=65). Remaining = 7 straggler degrees
(d in {5,7,8,9} cherry + {62,63,64} boundary) + the rcases wrapper + d=4 cell wiring + top-level dispatch.
AxiomGuard now 40 guarded theorems. conjecture1_proved=False.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy
DrMurphyIsIn
enabled auto-merge
September 4, 2026 12:43
…ers for Wave 2) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017tanHspSnAobPr8ehGcmJE
Adds R3Cert/BGSCLSubactionD4Cells.lean: the 35 node-level `subaction_deg4_*`
cells discharging the per-node additive-subaction inequality for every
degree-4 hub profile (3 children, multisets over {leaf,2,3,4,H}).
Each cell mirrors the degree-3 template (BGSCLSubactionDeg3Mid.lean): bound
each child message, `set S`, `log_tangent` at the profile's binding corner,
bound the node rho `1/(384*(4+S))`, apply the single-log enclosure atom,
`linarith`. All 35 close with a single tangent (no two-slope decouple).
Note: the 20 profiles WITHOUT deg-2 children reuse the existing `d4_*` atoms
from BGSCLSubactionD4.lean directly. The 15 profiles WITH deg-2 children need
a correctly-signed log(3/2) fold (kL = +#deg2) to make linarith cancel the
deg-2 child's `-log(3/2)`; the pre-existing `d4_*` atoms for those carry
kL = -#deg2 (true but a loose, opposite-signed fold that cannot combine), so
these cells re-derive the atom via the public `tangent_atom` generator.
Local `lake build R3Cert.BGSCLSubactionD4Cells` green, no sorry.
conjecture1_proved = False.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017tanHspSnAobPr8ehGcmJE
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017tanHspSnAobPr8ehGcmJE
…ing capstone
Wire the two Wave-2 placeholder arms of isSubaction_ρwit:
- deg-4 (cs=[c1,c2,c3]): subaction_deg4 sorts the triple by bcc via three
le_total splits, transports subaction_deg4_canon back with subaction_perm;
subaction_deg4_canon classifies bcc x/y/z into {0,1,2,3,≥4} and routes the 35
monotone class-triples to subaction_deg4_XYZ (omega kills the 90 non-monotone).
- tail (cs.length≥5): exact tail_wrapper _ (length ≥ 4).
Add capstone bg_ceiling : ∀ b, bell b ≤ 0 := ceiling_of_witness isSubaction_ρwit.
Both isSubaction_ρwit and bg_ceiling build green, sorry-free, kernel axioms
[propext, Classical.choice, Quot.sound].
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017tanHspSnAobPr8ehGcmJE
Assembles IsSubaction ρwit end-to-end: 35 deg-4 node cells (wiring the d4_* atoms), the 7 tail stragglers + gap-free tail_wrapper, the subaction_perm permutation bridge, and the top-level degree dispatch. The capstone bg_ceiling : ∀ b, bell b ≤ 0 is now machine-checked and kernel-clean [propext, Classical.choice, Quot.sound]. AxiomGuard extended to 51 theorems. Scope: this closes the classical-branch ceiling line (bell b ≤ 0), not the full BG conjecture; conjecture1_proved remains to be re-evaluated separately. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017tanHspSnAobPr8ehGcmJE
Owner
Author
|
Ceiling closed. Scope (honest): this closes the classical-branch ceiling line, one input to the larger BG program. It is NOT conjecture1 (which reduces the Laplacian-permanent-ratio maximizer via the still-open Hnorm/Hdom layers and is not wired to this branch). |
…n, CI green) Scope stays honest: closes the branch ceiling line bell b ≤ 0, one input to the SCL/G-step bridge; NOT conjecture1. conjecture1_proved = False unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017tanHspSnAobPr8ehGcmJE
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
1 participant
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.
BG classical branch ceiling via additive SUBACTION — progress landing
Purely additive (3903 insertions, 0 deletions vs main; all new files under
proof/). Kernel-verified, axiom-clean[propext, Classical.choice, Quot.sound], fulllake buildgreen (8659 jobs, 9 modules), CI-enforced byAxiomGuard.lean(40 guarded theorems).conjecture1_proved = False— this is incremental proof progress, NOT a closed conjecture.The line
The ceiling
∀ b, bell b ≤ 0reduces (kernel-green) to the single obligationIsSubaction ρwit(the earlier multiplicativeLe1Stepwas refuted —BG_LE1STEP_REFUTED_20260902.md). The additive subaction telescopes; a sum of slightly-loose local terms works where a product overshoots.What this branch proves
ceiling_of_subaction,ρwit_nonneg,ceiling_of_witness) + the validated witnessρwit.tangent_atom).tail_decouple.subaction_tail_d6— the 27·23 tie (d=6), viaphi_lb_d6+tie_identity_d6.subaction_tail_deg4— d∈[10,61] (52 values), viaphi_lb_deg4+tail_all_deg4; its razor-thin d=10 boundary uses the tight anchorcherry_anchor_ge_tight : 3/400 ≤ 2F*−log(3/2)(exact2F*−log(3/2)=(1/11)log(529/486),529/486=(621/64)²(2/3)¹¹— the 27·23 structure — + a degree-3Real.exp_bound).subaction_tail_deg5— the INFINITE deg-5 tail (d≥65), viaphi_lb_general+F*−log((6d−1)/(5d))≥0.Remaining (finite, patterned — no open mathematics)
7 tail straggler degrees (
d∈{5,7,8,9}cherry +d∈{62,63,64}boundary — each atail_decoupleinstantiation needing its boundary enclosure), thercases-on-length tail wrapper, the 35 d=4 cell wirings, and the top-levelIsSubactiondegree-dispatch. Full handoff:proof/docs/BG_SUBACTION_CONSOLIDATED_HANDOFF.md.Safety
All changes are Lean proof files + docs under
proof/; no trading code touched. Daemons run from a different branch. Does NOT flipconjecture1_proved.🤖 Generated with Claude Code
https://claude.ai/code/session_01U5GjxUBoxVBMPwNwUH9RKy