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 correct ordinary estimator 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.

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.SatisfiesBounds ordinaryMachine (ordinaryParameters clock)) (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.SatisfiesBounds ordinaryMachine (ordinaryParameters clock)) (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.

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

Implementation-level collapse using ordinary estimator correctness only on the plan's paired and condition-only query families.

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) (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 operational pair-composition contract proves finiteness of both query families, so no separate source-finiteness premise remains.

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.SatisfiesBounds ordinaryMachine (ordinaryParameters clock)) (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 precise contrapositive needed before a future DistNP ⊆ AvgP → SoI theorem can 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.SatisfiesBounds ordinaryMachine (ordinaryParameters clock)) (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) (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.