Skip to content

perf(hex-int-factor): complete decomposed Phase-4 evidence - #9864

Merged
kim-em merged 33 commits into
mainfrom
issue-9634
Sep 1, 2026
Merged

perf(hex-int-factor): complete decomposed Phase-4 evidence#9864
kim-em merged 33 commits into
mainfrom
issue-9634

Conversation

@kim-em

@kim-em kim-em commented Aug 31, 2026

Copy link
Copy Markdown
Owner

Closes #9634.

This implements the issue's rewritten, preregistered Phase-4 contract:

  • measures public factor?, raw rho splitting, and post-split completion as three distinct surfaces, explicitly identifying the 32-bit public rung as table-complete and the 40--80-bit rungs as rho-driven;
  • keeps only the output-agreeing table gate and treats unequal-API ratios as explanatory;
  • normalizes PARI to one Hex factorization and pins GMP-ECM explicitly to -sigma 0:7, B1=1000, stage 2 disabled, with one fixed 256-input protocol;
  • uses identical seeds and canonical complete outputs for exponents 12 through 80, retaining the power split at 0.946x;
  • keeps scientific budgets in the pinned-host collector, leaving verify timing-free;
  • records actual rotated fresh-module checkFactorization replays for k=1..10, ending with a 61-bit factor, including both null controls and all raw paired samples;
  • commits clean compiled profile summaries for all five declared families; the smooth-family runner now profiles ECM stage 1, and private Hex symbols are correctly attributed as repository code;
  • marks HexIntFactor complete through Phase 4 and declares its proof-probe tree.

Key evidence:

  • table public/direct: 1.181x (gate <= 1.25)
  • power split/generic: 0.946x (retention gate <= 0.98)
  • all seven parametric verdicts: consistent_with_declared_complexity
  • all 31 fixed scientific budgets and hashes pass
  • all 49 default-fuel cases succeed
  • explicit GMP-ECM curve: parameterization 0, sigma 7; one of six rows is overhead-eligible under the unchanged preregistered rule
  • kernel artifact: release-quality, all ten cases below 5 s, null/raw measurements reported
  • all five profiles pass calibration, retained-sample, off-thread-noise, and sensitivity diagnostics

Fresh independent Claude Opus review completed while CI was running. Substantive findings were addressed: route and RNG-trajectory descriptions, null/raw replay reporting, actual ECM attribution, private-symbol categorization, committed profile summaries, Phase-4 metadata, residual-exponent semantics, power-margin disclosure, and the Concerns narrative. Two suggestions were rejected with concrete verification: GMP-ECM verbose output confirms the original command already selected sigma=0:7 (the collector now states it explicitly), and the exact issue contract requires the combined comparator name PARI factor and GMP-ECM plus the preregistered <=50% overhead eligibility calculation.

Local verification:

  • lake build (10,500 jobs)
  • lake build HexIntFactor HexIntFactor.Conformance hexintfactor_bench
  • .lake/build/bin/hexintfactor_bench verify (40/40)
  • .lake/build/bin/hexintfactor_bench control-audit
  • .lake/build/bin/hexintfactor_bench default-fuel (49/49)
  • clean native artifact validation/render and five clean sampling captures
  • python3 scripts/check_phase4.py
  • full CI structural/lint suite, including trust surface, DAG, copyright, file-line, conformance matrix, 41 Mathlib-free bench executables, 178 proof probes, and 72 fresh-module tests

Kim Morrison added 3 commits August 31, 2026 05:00
Cost-model derivation: balanced rho uses the O(n^(1/4)) expected iteration bound; fixed-bound word routes are constant and direct-Nat p-1/ECM use a quadratic operand-cost bound. Replay, entry products, square divisors, and totient use quadratic widening-product bounds; order and primitive-root search use linear candidate bounds. Power forms use the conservative 2^n input-value bound, cyclotomic recursion is quadratic, and sigma exponentiation uses n log n.
@kim-em

kim-em commented Aug 31, 2026

Copy link
Copy Markdown
Owner Author

Closing without merge after premise validation. The clean measurements contradict the pre-registered comparator expectation, the GMP-ECM curve is overhead-ineligible on five of six rungs, and the required kernel replay family is absent. Full evidence and corrected-scope requirements are recorded on #9634.

@kim-em kim-em closed this Aug 31, 2026
Kim Morrison added 17 commits August 31, 2026 22:26
PARI factor does not expose a mode restricted to Hex's trial-division-plus-rho portfolio, so an external ratio cannot diagnose dispatch or rho by itself. Require same-input internal controls for those claims and keep PARI/GMP-ECM as explicitly portfolio-mismatched informational comparisons.
Use the existing Phase-4 one-second soft ceiling at the 80-bit top rung as the independent absolute criterion for deciding whether the current balanced route requires SQUFOF work.
The table control has an explicit 1.25 ratio, while the balanced control uses the dispatcher's exact rho allocation, rejects failures, normalizes outputs, and has an explicit factor-of-two ratio. The comparator contract now reports every GMP-ECM rung with eligibility labels, scopes each endpoint, and leaves SQUFOF to a genuine within-Lean prototype comparison.
# Conflicts:
#	HexIntFactor/SPEC/hex-int-factor.md
#	libraries.yml
Replace the mismatched complete-factorization/direct-split ratio with a preregistered comparison between default and rho-only route policies through the same completion and certificate path. Keep direct rho as the independent 2^(bits/4) scaling and profiling target.
Thread a private split policy through the production search so the diagnostic rho-only arm retains the exact public preprocessing, random-state progression, recursive certificate construction, and checked-factorization acceptance while disabling only smooth fallback after rho exhaustion.

Use canonical full-factorization encodings for the seven balanced fixed pairs and retain raw rho solely as a 2^(bits/4) scaling target. Preregister per-target fixed ceilings and expected hashes, prevent fixed-term lifting, cover the full default-fuel schedule, and add the 1-through-10 kernel replay ladder ending at a 61-bit Pocklington certificate.

The replay n^2 model follows one bounded guarded multiplication per exponent step on a widening accumulator. The square-divisor n^2 model follows sequential multiplication of n fixed-exponent entries into a linearly widening accumulator; its constant 8192-run loop clears the subprocess floor without changing the model. Sigma entry and totient ladders likewise sum linearly widening fixed-entry products, while sigma exponent uses the n log n surrogate for its growing exact quotient. Raw balanced rho uses the expected 2^(bits/4) cycle cost for factors of half the input width, and order uses one modular multiplication per scanned exponent.

Run table trial division before perfect-power root search and classify fully table-factored powers by the gcd of their multiplicities, removing redundant root searches from the dominant small-dispatch batch without changing its route classification.
Add per-rung closed-term-safe ECM anchors with literal expected hashes and absolute ceilings. Replace the obsolete collector registrations with the complete normal/forced policy pairs and validate every harness verdict, expected hash, internal ratio, control audit, and default-fuel result before writing an artifact.

Use the same 256-input GMP-ECM subprocess shape for the factor-of-15 protocol control and every shared rung. Pass sigma 7, B1 1000, and B2 1 explicitly, so stage 2 is disabled by B2 < B1. Preserve no-factor outcomes as results rather than misreporting them as protocol failures, and mark ratio eligibility solely from the preregistered overhead-fraction rule.
Double the constant square-divisor hot loop so its upper three rungs clear the unchanged ten-times subprocess floor even when pinned spawn overhead approaches 200 ms. This does not change the n^2 model, schedule, tolerance, or fixtures. Surface captured benchmark stdout and stderr when the collector rejects a child run.
Raise only the per-call safety cap from 60 to 120 seconds so the already-declared 1024-entry hot-loop rung completes under single-CPU affinity. Keep the n^2 model, 0.20 tolerance, schedule, subprocess filter, and fixtures unchanged.
@kim-em kim-em reopened this Sep 1, 2026
@kim-em kim-em changed the title perf(hex-int-factor): complete Phase-4 evidence package perf(hex-int-factor): complete corrected Phase-4 evidence Sep 1, 2026
@kim-em

kim-em commented Sep 1, 2026

Copy link
Copy Markdown
Owner Author

Closing after fresh Opus review and CI established the revised comparator premise is still unsound; concrete evidence is recorded on #9634. No merge performed.

@kim-em kim-em closed this Sep 1, 2026
Kim Morrison added 4 commits September 1, 2026 05:54
Cost-model derivation: runSmooth performs n copies of one fixed 80-bit unbalanced rho split, so its repetition parameter is linear. runPower performs n copies of one fixed exponent-80 power factorization, so its repetition parameter is also linear. These registrations are attribution-only and do not model operand-size scaling.
@kim-em kim-em reopened this Sep 1, 2026
@kim-em kim-em changed the title perf(hex-int-factor): complete corrected Phase-4 evidence perf(hex-int-factor): complete decomposed Phase-4 evidence Sep 1, 2026
Kim Morrison added 4 commits September 1, 2026 06:21
# Conflicts:
#	HexIntFactorMathlib/SPEC/hex-int-factor-mathlib.md
#	libraries.yml
Cost-model derivation: the attribution runner repeats one fixed 80-bit ECM stage-1 call, so its declared work is linear in the repetition count.
@kim-em

kim-em commented Sep 1, 2026

Copy link
Copy Markdown
Owner Author

Fresh Claude Opus second-opinion disposition:

Addressed:

  • documented that the 32-bit public balanced rung is table-complete, not a rho decomposition;
  • documented that public and direct-rho executions have different RNG trajectories;
  • added both kernel null-control summaries and every raw rotated paired delta;
  • changed the smooth-family profile runner from a second rho capture to actual ECM stage 1;
  • classified compiler-generated _private.Hex... symbols as Hex own code and added unit coverage;
  • committed all five full profile summaries;
  • set HexIntFactor to done_through: 4 with its proof-probe declaration;
  • kept residualExponent = 1 whenever residualBase = 1, including through scaling;
  • disclosed the power retention margin and replaced the empty Concerns section with the informational external gaps.

Verified but not adopted:

  • Opus inferred that -sigma 7 selected different parameterizations. ecm -v -sigma 7 1000 1 reports sigma=0:7 for every admitted operand; the collector now uses explicit -sigma 0:7 to eliminate ambiguity.
  • Opus suggested splitting the comparator declaration and withdrawing the sole eligible GMP-ECM row. The rewritten issue explicitly fixes the name PARI factor and GMP-ECM and preregisters eligibility as protocol overhead <=50% of raw time. The clean recapture gives 45.63% at 48 bits, so the row remains eligible without changing the rule after measurement. Equal discovered factors do not require equal stage-1 wall time across different cofactors.

@kim-em
kim-em merged commit 693d7d3 into main Sep 1, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

perf: complete HexIntFactor Phase-4 evidence with decomposed factorization costs

1 participant