back to table · edit · history · where entries came from · files · download
2812 bytes, as of the version from 2026-11-11 08:15 (current). Recorded here, not run.
# Argument selection: Log-sinh-cosh integrals
Natural quantity: H_(m,n)(x) = -integral_0^x log(2sinh(t/2))^(m-1)
log(2cosh(t/2))^(n-1) dt, for ordered integers m,n>=1 and real x>0.
All logarithms are natural; all roots/logarithms use positive real branches.
There is no factorial normalization, regularization, absolute value of a logarithm,
or division of the endpoint by pi. The ordinary improper integral converges,
since the sole singularity is a finite power of log(t).
Checked source: Charlton, Gangl, Lai, Xu and Zhao, arXiv:2210.14704v1,
Definition 2.1, Lemma 2.2 equation (2.5), and section 4 equation (4.2).
The source has absolute values inside the logs; for positive t the arguments
are positive, so removing these absolute values changes nothing.
Let phi=(1+sqrt(5))/2 and a=log(phi). The parameter order is (m,n,x).
The entire selection consists of:
- x=logphi, displaying a: m>=1, n>=2, m+n<=10 (36 entries).
- x=2logphi, displaying 2a: n=2, 1<=m<=8 (8 entries).
m and n are discrete_index parameters: the two ordered logarithmic orders.
At z=1/4 in (2.5), theta=asinh(1/2)=a and log(2sinh(theta))=0.
For each p=1,...,8, only j=p survives. Its terms are H_(p,2)(2a)
and H_(l,p-l+2)(a), 1<=l<=p. Taking their union gives exactly the stated
44 entries. Thus even m=1 is needed by the harmonic-binomial application;
n=1 is the pure log-sinh boundary already covered where needed by T713.
Eight is a noncanonical finite prefix, selected to cover both balanced and
unbalanced ordered mixed powers before deepening any single order. There is
no reflection symmetry allowing m<=n, and no rectangular hull is implied.
x has type R and category mixed, with exhaustive disjoint groups:
- ['logphi']: documented_application, the half-endpoint selected by (2.5)
at z=1/4, used explicitly in section 4. Every selected order is a term
in the same published identity, not an assertion that each value is tabulated.
- ['2logphi']: intrinsic, also application-selected. 2a is the unique
positive zero of log(2sinh(x/2)); its n=2 slice is exactly the other term
of (2.5). Positivity and strict monotonicity prove uniqueness.
Breadth review: both application endpoint regimes, pure-cosh boundary, both
parities, and balanced/unbalanced moments are retained. Adding the sibling's
exploratory silver endpoint would lack this mixed-family application rationale.
A broader endpoint family needs its own selection; there is no arbitrary mesh,
no statistical quantile, and no famous-only pruning here. Completeness is no.
Enumeration, Programs and complete-note must reproduce precisely these slices.
This is the builder's justification, not an independent argument-review verdict.
Instructions: skill-manifest.json, archived bundle SHA-256
d6661c2f21613524889fa3a57d3c95f8330344ca62e5a856211c08a282b7dbab.