The exact integer-polynomial CLD column Phi(g) = f * g' / g.
Equations
Instances For
If f = g * h and g is monic, the quotient definition of Phi(g) is the
integer polynomial h * g'.
Coefficient bound for the BHKS Phi column from the valid replacement
analytic estimate M(Phi) <= n * ||f||_2.
The hypotheses hphi_degree and hphi_mahler are the precise downstream
analytic obligations: the theorem does not use, imply, or reintroduce the false
unconditional derivative Mahler bound.
BHKS Lemma 5.1 (unconditional form): the coefficient bound for the BHKS
Phi column under a monic factorisation f = g * h. This discharges the
analytic hypotheses of BHKS.abs_phi_coeff_le.
The proof avoids the false unconditional derivative Mahler estimate by
decomposing Phi.map ℂ via the product-rule sum
Polynomial.derivative_eq_sum_rootDeletionDerivativeSummand (one summand per
complex root of g.map ℂ). Each summand has Mahler measure at most
M(f.map ℂ) by Mahler multiplicativity (using g.Monic), and there are at
most g.natDegree ≤ f.natDegree summands.
The exact integer CLD column for an arbitrary factorization f = g * h.
Unlike phi, this definition does not divide by g and therefore does not
need g to be monic. It is the logarithmic-derivative numerator
h * g' = f * g' / g, expressed using the actual integer cofactor.
Equations
Instances For
The direct-coordinate CLD column has the same BHKS coefficient bound for
an arbitrary nonzero integer factorization. Monicity of the integer factor is
irrelevant: the root-deletion proof bounds h * g' directly.
CLD quotient congruence (BHKS logarithmic-derivative correspondence).
When a monic positive-degree lifted factor g divides input modulo p ^ k
(witnessed by input ≡ g * h), multiplying the executable CLD quotient
cldQuotientMod input g p k back by g recovers the logarithmic-derivative
numerator input * g' modulo p ^ k:
g * cldQuotientMod input g p k ≡ input * g' (mod p ^ k).
This is the semantic link from the executable quotient to the exact integer CLD
column BHKS.phi g = input * g' / g: composed with
BHKS.phi_eq_factor_mul_derivative, it identifies g * cldQuotientMod input g p k
with g * BHKS.phi g modulo p ^ k. The divisibility hypothesis is on input
itself, not on the BHKS auxiliary polynomial, which need not be divisible by g
modulo p ^ k.
The proof transports the executable monic division to Polynomial (ZMod (p ^ k)),
where the reconstruction identity and the remainder degree bound pin the mapped
remainder down by uniqueness of division by a monic polynomial; divisibility of
the mapped numerator by g then forces that remainder to vanish.
Product logarithmic-derivative congruence over a list of factors.
If every factor g in gs satisfies the per-factor CLD congruence
g * q g ≡ f * g' (mod m), then the product of gs times the sum of the
q-images is congruent modulo m to f times the derivative of the product.
This is the executable list form of the logarithmic-derivative identity
(∏ gᵢ) · Σ (f · gᵢ' / gᵢ) ≡ f · (∏ gᵢ)', proved by structural induction on the
list using the Leibniz product rule, with no leave-one-out indexing.
A centred residue modulo m has magnitude at most m / 2: 2·|x mod^± m| ≤ m.
BHKS Lemma 5.7, period-aware aggregate form. Where
two_mul_natAbs_sum_psiCut_le bounds the raw high-bit cut-sum and needs
per-element ambient residues pinned to a small integer (forcing per-factor
smallness), this version bounds the cut-sum modulo the period q = p^(a−b) and
needs only the aggregate residue centeredResiduePow p a (Σ w_i) to be small.
This is the main estimate of the recombination case: for split irreducible
factors the per-local CLD residues are not individually small; only their
aggregate Φ(factor) is; and the lattice's period rows diag(p^(a−l_j)) absorb
the large per-local parts. The raw-sum bound is false here (no per-factor
hypothesis is available); the ∃ t period reduction by an integer multiple of q
is exactly what makes the aggregate-only bound true.
The executable Pascal-recursion Hex.Nat.choose agrees with Mathlib's
Nat.choose; needed because Hex.bhksCoeffBound elaborates Nat.choose to the
executable shadow inside namespace Hex.
Monic cancellation modulo m. Over Polynomial ℤ, if C m divides a
product g * z and g is monic, then C m divides z. The proof maps to
Polynomial (ZMod m), where g.map is monic hence a non-zero-divisor.
BHKS Lemma 5.1, executable bound form. For a monic divisor g of f
over Polynomial ℤ, every Phi-column coefficient is bounded by the executable
Mignotte column bound Hex.bhksCoeffBound f j.
Executable-bound form of abs_factorColumn_coeff_le.
Generic CLD residue correspondence. For a monic divisor g of f whose
precision p^a separates the Mignotte column bound, the centred ambient residue
of any polynomial q whose product g * q is congruent to the
logarithmic-derivative numerator f * g' modulo p^a is exactly the integer
Phi-column coefficient. The per-factor correspondence below is the special case
q := cldQuotientMod f g p a; the aggregate residue work instantiates it with
q := supportCldSum, which satisfies the same congruence against the whole
recovered factor without being a single cldQuotientMod.
centeredResiduePow p a depends only on its argument modulo p ^ a.
The j-th coefficient of a list sum of ZPolys is the integer list sum of
the per-summand j-th coefficients.
A finite sum over the support filter of Finset.univ equals the list sum
over the correspondingly filtered finRange.
Coefficientwise congruence modulo m is preserved by the formal
derivative.
Constant scaling commutes with multiplication on the left.
Constant scaling commutes with multiplication on the right.
Constant scaling commutes with the formal derivative.
A scalar coprime to the modulus can be cancelled from a polynomial congruence.
Aggregate CLD congruence for a recovered support, parametrised directly by
the per-selected-factor monic / positive-degree / modular-cofactor data instead
of a semantic package. Mirrors TrueFactorLiftSemantics.supportProduct_cldSum_congr
but takes the per-factor hypotheses explicitly, so it applies to a
RecoveredLift which carries no semantic package.
Aggregate CLD residue from a direct-coordinate recovered lift.
The selected support product is monic, while the recovered integer factor need not be. The direct recovery congruence says
lc(f) · supportProduct ≡ factorScale · factor.
Differentiating this relation and combining it with the aggregate local CLD
congruence shows that supportCldSum is congruent to the exact integer column
cofactor * factor'. Cancellation is sound because the support product is
monic and lc(f) is a unit modulo the Hensel modulus.
The executable cut-threshold array reads back the per-coordinate threshold.
Selection coefficients for the period-adjusted true-factor short vector: the
support indicator on the first block, and −t j on the diagonal-period rows.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The first-block entries of the selection coefficients are the support indicator.
The tail entries of the selection coefficients are the negated period multipliers.
The period-adjusted true-factor short vector: the support indicator on the first block, with the CLD tail reduced by the diagonal-period rows.
Equations
Instances For
The period-adjusted vector is a genuine BHKS lattice vector: it is a row combination of the basis by construction.
Under block form, the first factorCount coordinates of the period-adjusted
vector are exactly the support indicator (the period rows do not touch the first
block).
Under block form, the trailing coeffWidth coordinates of the period-adjusted
vector are the support CLD-column sum reduced by the diagonal-period correction.
Generic tight cut-radius norm bound for any support vector whose first block
is the indicator and whose tail columns satisfy 2·|colⱼ| ≤ factorCount.
Period-adjusted true-factor short vector from a RecoveredLift.
The direct-coordinate aggregate residue correspondence
(recoveredLift_aggregate_residue) and the period-aware carry lemma
(two_mul_natAbs_sum_psiCut_period_le) bound each tail column of the
period-adjusted vector by factorCount/2. Together with the structural project
and lattice-membership facts, this yields a SupportShortVectorData for the
recovered support, feeding the fast-disjunct consumer through
cutProjectionHypotheses_of_shortVectors.
Equations
- One or more equations did not get rendered due to their size.