The multiplicative-hardness consequence of conditional MinKT SoI #
This module composes the complete finite spine of Hirahara's conditional MinKT
argument. An admissible primitive clock p (the theorems' clock) supplies a
polynomial slack-amplified gap clock, an operational condition-first compiler
supplies the paired upper chain, and one ordinary estimator, correct on the
plan's own queries, plus time-bounded symmetry of information supplies the
conditional estimator. If the induced threshold language is in P, NP-hardness
of the corresponding multiplicative gap forces P = NP.
Every remaining research obligation stays explicit in the theorem statement; in particular, this result does not assert the SoI hypothesis, a concrete universal evaluator, estimator efficiency, or multiplicative-gap hardness. The SoI hypothesis is satisfiable on its own (it holds trivially for a machine that describes nothing), so the theorems here are not vacuous on that account; the remaining hypotheses are what constrain the machines.
The estimator is required to be correct only on the plan's paired and
condition-only queries. Correctness on every instance cannot hold for these
ordinary parameters (not_satisfiesBounds_ordinaryParameters).
Even on the plan's queries, correctness needs clocks that leave room to print
the paired output. For t' = max(t, |x| + |y|), the paired query asks for
pair x y, of length 2|x| + |y| + 2, at source clock p(t') and transformed
clock p(p(t')), while admissibility bounds p from below only by
t ≤ p(t). The estimator hypothesis forces 2n + 2 ≤ p(p(n)) for every n
(two_mul_add_two_le_clock_clock_of_satisfiesBoundsOn), and the solver forms'
finiteness premise forces 2n + 2 ≤ p(n)
(two_mul_add_two_le_clock_of_forall_ne_top). Both fail for slow admissible
clocks such as id (isAdmissibleClock_id, not_satisfiesBoundsOn_plan_id),
where every theorem below is vacuous. The estimator hypothesis can be met
exactly when the ordinary machine prints every plan query's output within that
query's transformed clock: the transformed-clock complexity itself is then a
correct, though not necessarily efficient, estimator.
The complete finite multiplicative-hardness consequence of the slack-amplified SoI reduction.
The clock admissibility hypothesis proves that the final conditional clock is
both widening and polynomially bounded. Only widening is needed to construct
the promise; the polynomial bound remains available as part of the public
parameter theorem. Admissibility does not make hestimate satisfiable:
hestimate forces 2n + 2 ≤ clock (clock n)
(two_mul_add_two_le_clock_clock_of_satisfiesBoundsOn), which fails at the
admissible clock id (not_satisfiesBoundsOn_plan_id).
The implementation-level form of the complete consequence. Polynomial-time
encoded query builders and an encoded ordinary estimator construct the induced
threshold language in P, so no separate semantic membership premise remains.
Former name of P_eq_NP_of_multiplicative_hard_of_SoI_of_implementations,
which now requires estimator correctness only on the plan's queries.
Replace the abstract ordinary estimator and its encoded implementation by
an FP solver for logarithmic GapMINKT.
The bounded threshold sweep supplies both the Fact 3.4 estimator sandwich and
the encoded estimator consumed by the two-query conditional reduction. The
threshold sweep needs every query of the plan to have finite ordinary
complexity at its own source clock; that is the explicit premise hfinite,
which says exactly that the ordinary machine prints every plan query's output
within that clock. The paired query asks for pair x y, of length
2|x| + |y| + 2, within clock (max t (|x| + |y|)) steps, so hfinite forces
2n + 2 ≤ clock n for every n (two_mul_add_two_le_clock_of_forall_ne_top)
and fails for slow admissible clocks such as id.
Assuming P ≠ NP, the simultaneous SoI, estimator-efficiency, compiler,
and multiplicative-hardness hypotheses are inconsistent. This is the
contrapositive form a future DistNP ⊆ AvgP → SoI theorem (for machines also
meeting the other hypotheses) would combine with to rule out Heuristica.
Under P ≠ NP, implementation-level estimator efficiency and
multiplicative hardness rule out the corresponding time-bounded SoI statement.
Under P ≠ NP, an efficient logarithmic GapMINKT solver, the encoded
two-query plan, and multiplicative conditional-gap hardness rule out the
corresponding SoI statement.