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 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, whose clocks dominate their output lengths. Correctness on every instance cannot hold for these ordinary parameters (not_satisfiesBounds_ordinaryParameters).

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.P_eq_NP_of_multiplicative_hard_of_SoI {ordinaryTapes conditionalTapes : ℕ} {clock : ℕ → ℕ} (additive compilerLoss : ℕ) {composition : PairCompositionPlan} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (hclock : IsAdmissibleClock clock) (hsupports : SupportsPairUpper (plan clock compilerLoss) composition ordinaryMachine conditionalMachine) {ordinaryEstimate : GapMINKT.Logarithmic.Estimator} (hestimate : ordinaryEstimate.SatisfiesBoundsOn ordinaryMachine (ordinaryParameters clock) (plan clock compilerLoss).IsEstimatorQuery) (hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine clock (logarithmicSoILoss clock additive)) (factor : ℕ → ℕ) (hfactor : ∀ (length : ℕ), 1 ≤ factor length) (hhard : PromiseNPHard (Multiplicative.problem ordinaryMachine conditionalMachine (parameters clock additive compilerLoss) factor ⋯ hfactor)) (hpolynomial : estimatorLanguage ((plan clock compilerLoss).components ordinaryEstimate).estimate ∈ P) : P = NP

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.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.P_eq_NP_of_multiplicative_hard_of_SoI_of_implementations {ordinaryTapes conditionalTapes : ℕ} {clock : ℕ → ℕ} (additive compilerLoss : ℕ) {composition : PairCompositionPlan} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (hclock : IsAdmissibleClock clock) (hsupports : SupportsPairUpper (plan clock compilerLoss) composition ordinaryMachine conditionalMachine) {ordinaryEstimate : GapMINKT.Logarithmic.Estimator} (hestimate : ordinaryEstimate.SatisfiesBoundsOn ordinaryMachine (ordinaryParameters clock) (plan clock compilerLoss).IsEstimatorQuery) (encodedPlan : EncodedPlan (plan clock compilerLoss)) (encodedEstimator : EncodedEstimator ordinaryEstimate) (hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine clock (logarithmicSoILoss clock additive)) (factor : ℕ → ℕ) (hfactor : ∀ (length : ℕ), 1 ≤ factor length) (hhard : PromiseNPHard (Multiplicative.problem ordinaryMachine conditionalMachine (parameters clock additive compilerLoss) factor ⋯ hfactor)) : P = NP

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.

@[deprecated Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.P_eq_NP_of_multiplicative_hard_of_SoI_of_implementations (since := "2026-09-25")]

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.P_eq_NP_of_multiplicative_hard_of_SoI_of_query_implementations {ordinaryTapes conditionalTapes : ℕ} {clock : ℕ → ℕ} (additive compilerLoss : ℕ) {composition : PairCompositionPlan} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (hclock : IsAdmissibleClock clock) (hsupports : SupportsPairUpper (plan clock compilerLoss) composition ordinaryMachine conditionalMachine) {ordinaryEstimate : GapMINKT.Logarithmic.Estimator} (hestimate : ordinaryEstimate.SatisfiesBoundsOn ordinaryMachine (ordinaryParameters clock) (plan clock compilerLoss).IsEstimatorQuery) (encodedPlan : EncodedPlan (plan clock compilerLoss)) (encodedEstimator : EncodedEstimator ordinaryEstimate) (hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine clock (logarithmicSoILoss clock additive)) (factor : ℕ → ℕ) (hfactor : ∀ (length : ℕ), 1 ≤ factor length) (hhard : PromiseNPHard (Multiplicative.problem ordinaryMachine conditionalMachine (parameters clock additive compilerLoss) factor ⋯ hfactor)) : P = NP

Former name of P_eq_NP_of_multiplicative_hard_of_SoI_of_implementations, which now requires estimator correctness only on the plan's queries.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.P_eq_NP_of_multiplicative_hard_of_SoI_of_logarithmic_solver {ordinaryTapes conditionalTapes : ℕ} {clock : ℕ → ℕ} (additive compilerLoss : ℕ) {composition : PairCompositionPlan} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (hclock : IsAdmissibleClock clock) (hsupports : SupportsPairUpper (plan clock compilerLoss) composition ordinaryMachine conditionalMachine) (hfinite : ∀ (query : MINKT.Instance), (plan clock compilerLoss).IsEstimatorQuery query → ordinaryMachine.timeBoundedKolmogorovComplexity query.output query.time ≠ ⊤) (decide : List Bool → Bool) (hdecide : (fun (bits : List Bool) => [decide bits]) ∈ FP) (hsolve : (GapMINKT.Logarithmic.problem ordinaryMachine (ordinaryParameters clock) ⋯).SolvedBy decide) (encodedPlan : EncodedPlan (plan clock compilerLoss)) (hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine clock (logarithmicSoILoss clock additive)) (factor : ℕ → ℕ) (hfactor : ∀ (length : ℕ), 1 ≤ factor length) (hhard : PromiseNPHard (Multiplicative.problem ordinaryMachine conditionalMachine (parameters clock additive compilerLoss) factor ⋯ hfactor)) : P = NP

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; that is the explicit premise hfinite. It holds when the ordinary machine can print strings within the queries' clocks, which dominate their output lengths.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.not_timeBoundedSymmetryOfInformation_of_P_ne_NP {ordinaryTapes conditionalTapes : ℕ} {clock : ℕ → ℕ} (additive compilerLoss : ℕ) {composition : PairCompositionPlan} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (hclock : IsAdmissibleClock clock) (hsupports : SupportsPairUpper (plan clock compilerLoss) composition ordinaryMachine conditionalMachine) {ordinaryEstimate : GapMINKT.Logarithmic.Estimator} (hestimate : ordinaryEstimate.SatisfiesBoundsOn ordinaryMachine (ordinaryParameters clock) (plan clock compilerLoss).IsEstimatorQuery) (factor : ℕ → ℕ) (hfactor : ∀ (length : ℕ), 1 ≤ factor length) (hhard : PromiseNPHard (Multiplicative.problem ordinaryMachine conditionalMachine (parameters clock additive compilerLoss) factor ⋯ hfactor)) (hpolynomial : estimatorLanguage ((plan clock compilerLoss).components ordinaryEstimate).estimate ∈ P) (hne : P ≠ NP) : ¬TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine clock (logarithmicSoILoss clock additive)

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.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.not_timeBoundedSymmetryOfInformation_of_P_ne_NP_of_implementations {ordinaryTapes conditionalTapes : ℕ} {clock : ℕ → ℕ} (additive compilerLoss : ℕ) {composition : PairCompositionPlan} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (hclock : IsAdmissibleClock clock) (hsupports : SupportsPairUpper (plan clock compilerLoss) composition ordinaryMachine conditionalMachine) {ordinaryEstimate : GapMINKT.Logarithmic.Estimator} (hestimate : ordinaryEstimate.SatisfiesBoundsOn ordinaryMachine (ordinaryParameters clock) (plan clock compilerLoss).IsEstimatorQuery) (encodedPlan : EncodedPlan (plan clock compilerLoss)) (encodedEstimator : EncodedEstimator ordinaryEstimate) (factor : ℕ → ℕ) (hfactor : ∀ (length : ℕ), 1 ≤ factor length) (hhard : PromiseNPHard (Multiplicative.problem ordinaryMachine conditionalMachine (parameters clock additive compilerLoss) factor ⋯ hfactor)) (hne : P ≠ NP) : ¬TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine clock (logarithmicSoILoss clock additive)

Under P ≠ NP, implementation-level estimator efficiency and multiplicative hardness rule out the corresponding time-bounded SoI statement.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.not_timeBoundedSymmetryOfInformation_of_P_ne_NP_of_logarithmic_solver {ordinaryTapes conditionalTapes : ℕ} {clock : ℕ → ℕ} (additive compilerLoss : ℕ) {composition : PairCompositionPlan} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (hclock : IsAdmissibleClock clock) (hsupports : SupportsPairUpper (plan clock compilerLoss) composition ordinaryMachine conditionalMachine) (hfinite : ∀ (query : MINKT.Instance), (plan clock compilerLoss).IsEstimatorQuery query → ordinaryMachine.timeBoundedKolmogorovComplexity query.output query.time ≠ ⊤) (decide : List Bool → Bool) (hdecide : (fun (bits : List Bool) => [decide bits]) ∈ FP) (hsolve : (GapMINKT.Logarithmic.problem ordinaryMachine (ordinaryParameters clock) ⋯).SolvedBy decide) (encodedPlan : EncodedPlan (plan clock compilerLoss)) (factor : ℕ → ℕ) (hfactor : ∀ (length : ℕ), 1 ≤ factor length) (hhard : PromiseNPHard (Multiplicative.problem ordinaryMachine conditionalMachine (parameters clock additive compilerLoss) factor ⋯ hfactor)) (hne : P ≠ NP) : ¬TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine clock (logarithmicSoILoss clock additive)

Under P ≠ NP, an efficient logarithmic GapMINKT solver, the encoded two-query plan, and multiplicative conditional-gap hardness rule out the corresponding SoI statement.