feat(bg-lean): d=2 per-hub decouple residual PROVEN (nlinarith core of FlowedHubStep) - #197
Open
DrMurphyIsIn wants to merge 10 commits into
Open
feat(bg-lean): d=2 per-hub decouple residual PROVEN (nlinarith core of FlowedHubStep)#197DrMurphyIsIn wants to merge 10 commits into
DrMurphyIsIn wants to merge 10 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
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.
Discharges the Telperion
PerHubDecoupleResidualCertificatein Lean for d=2 (sorry-free, axiom-clean, builds locally) — validating the "highest-risk nlinarith" technique forFlowedHubStep's d≤6 tangent decouple.log76_gap:log(7/6) − F* ≤ −1/22, via11·(…) = log((7/6)^11 · 64/621)(combined into one log of a rational) bounded by the clean half-integerexp(1/2)=√(exp 1) < 1.6489.decouple_d2:R(S) ≤ 0onS ∈ [0,1/2],μ ∈ I— clear theμ/(2+S)division via inverse-as-atom, thennlinarithon the upward parabola inS.d=3..6 follow the same template (different rational constants). This is the core of
FlowedHubStep's d≤6 case; the list machinery + hbroom + leaf + child-IH + d≥7 ceiling is next.Local Lean builds work again (M3 Ultra 22-day uptime, no crash, ~4s/module) — the Aug-9 SoC-watchdog CI-only constraint is resolved (memory updated).
conjecture1_proved = False.🤖 Generated with Claude Code