The answer-length calculator of the introspection verifier

Issue #281 (Phase 3 of planning/aldous-lyons-track.md): the answer-length calculator L^intro_λ of the tailored presentation of Introspection.seven. It depends on λ only, not on the input verifier: the lengths of the presented game at a question are those of the label its graph view decodes to (TypedData.detype), and the typed lengths (Typed.lenR, Typed.len) are functions of the parameters k = fieldBits c λ n, j = selectorBits c λ n and R = (2^n)^λ alone.

On (n, x, κ), for λ ≥ 1 and n ≥ 1, the program

1. computes the binary pair (Q, R) (SourceCompiler.boundsProg) and puts it in unary;
2. computes the unary parameters (k, j, m = 2^j) (PauliSamplerParameters.prog);
3. reads the graph view of x (its first graphDim Label bits), decodes it to a label by a finite table (finiteFunction, the router's own device), together with κ, into the five coefficients of the length as a combination of k, m k, Q, R and 1 (coef), zero when the view does not decode;
4. outputs the combination in unary (linF).

At λ = 0 it is the empty program, and at n = 0 it inspects the index in place and outputs nil: both output length 0 within constant time, which the budget Introspection.budget, constant in the index there, requires.

• lenIntroC c λ, lenIntroProgC c: the calculator and its program from λ, in polynomial time.
• lenIntroC_lenIs: what it outputs on every bit string; lenIntroC_lenIs_question: at a detyped question of the reference verifier, the presented lengths (introLenR, introLenL).
• lenIntroC_budget: one constant C with the calculator within 2^{(λn + 1)^C} at degree C on every input, malformed included, and its lengths at most 2^{(λn + 1)^C}: the cost is a polynomial in 2^{(2c + 2)(λn + 2)} + |d| (costF), the parameters being at most the former (params_le_scale). lenIntroC_lenTotal: it halts everywhere.
• lenIntro, lenIntroProg, lenIntro_lenIs, lenIntro_budget: the same at sevenConstant, the fields len, lenProg, lenProg_eq, len_total and the len parts of within of TailoredIntrospection.

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.LenIntro.Label : Type

The labels of the introspection verifier's detyping.

Equations

• MIPRE.Tailored.Intro.LenIntro.Label = MIPRE.Introspection.DecisionKernel.Label

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.LenIntro.E : Label → Label → Prop

The type graph of the introspection verifier's detyping.

Equations

• MIPRE.Tailored.Intro.LenIntro.E = MIPRE.Introspection.DecisionCompiler.graph

The lengths

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.LenIntro.kOf (c lam n : ℕ) : ℕ

The field width k = fieldBits c λ n.

Equations

• MIPRE.Tailored.Intro.LenIntro.kOf c lam n = MIPRE.Introspection.SourceCompiler.fieldBits c lam n

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.LenIntro.jOf (c lam n : ℕ) : ℕ

The selector width j = selectorBits c λ n.

Equations

• MIPRE.Tailored.Intro.LenIntro.jOf c lam n = MIPRE.Introspection.PauliSamplerParameters.selectorBits c lam n

def MIPRE.Tailored.Intro.LenIntro.introLenR (c lam n : ℕ) : Label → ℕ

The readable length of a label at (c, λ, n): Typed.lenR at k = fieldBits c λ n, j = selectorBits c λ n, R = (2^n)^λ.

Equations

• MIPRE.Tailored.Intro.LenIntro.introLenR c lam n = MIPRE.Tailored.Intro.Typed.lenR (MIPRE.Tailored.Intro.LenIntro.kOf c lam n) (MIPRE.Tailored.Intro.LenIntro.jOf c lam n) ((2 ^ n) ^ lam)

def MIPRE.Tailored.Intro.LenIntro.introLenL (c lam n : ℕ) (t : Label) : ℕ

The linear length of a label at (c, λ, n): Typed.len - Typed.lenR.

Equations

• One or more equations did not get rendered due to their size.

def MIPRE.Tailored.Intro.LenIntro.introLen (c lam n : ℕ) (κ : Bool) : Label → ℕ

The length of kind κ: readable for false, linear for true.

Equations

• MIPRE.Tailored.Intro.LenIntro.introLen c lam n κ = if κ = true then MIPRE.Tailored.Intro.LenIntro.introLenL c lam n else MIPRE.Tailored.Intro.LenIntro.introLenR c lam n

The lengths as combinations of the parameters

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.LenIntro.Coef : Type

The five coefficients of a length, on k, m k, Q, R and 1.

Equations

• MIPRE.Tailored.Intro.LenIntro.Coef = (ℕ × ℕ × ℕ × ℕ × ℕ)

def MIPRE.Tailored.Intro.LenIntro.lin (v : Coef) (k m Q R : ℕ) : ℕ

The combination of the coefficients.

Equations

• MIPRE.Tailored.Intro.LenIntro.lin v k m Q R = v.1 * k + v.2.1 * (m * k) + v.2.2.1 * Q + v.2.2.2.1 * R + v.2.2.2.2

def MIPRE.Tailored.Intro.LenIntro.coef : Label → Bool → Coef

The coefficients of the length of kind κ at a label.

Equations

• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inl (MIPRE.QLD.Ty.pauli MIPRE.QLD.Bas.Z)) false = (0, 0, 1, 0, 0)
• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inl val) false = (0, 0, 0, 0, 0)
• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inr (MIPRE.Introspection.AuxType.hide k, snd)) false = (0, 0, 1, 0, 0)
• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inr val) false = (0, 0, 1, 1, 0)
• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inl (MIPRE.QLD.Ty.pauli MIPRE.QLD.Bas.Z)) true = (0, 0, 0, 0, 0)
• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inl (MIPRE.QLD.Ty.pauli MIPRE.QLD.Bas.X)) true = (0, 0, 1, 0, 0)
• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inl (MIPRE.QLD.Ty.point W)) true = (1, 0, 0, 0, 0)
• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inl (MIPRE.QLD.Ty.aline W)) true = (2, 0, 0, 0, 0)
• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inl (MIPRE.QLD.Ty.dline W)) true = (1, 1, 0, 0, 0)
• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inl (MIPRE.QLD.Ty.pairB W)) true = (0, 0, 0, 0, 1)
• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inl (MIPRE.QLD.Ty.var j)) true = (0, 0, 0, 0, 1)
• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inl MIPRE.QLD.Ty.pair) true = (0, 0, 0, 0, 2)
• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inl (MIPRE.QLD.Ty.con i)) true = (0, 0, 0, 0, 3)
• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inr (MIPRE.Introspection.AuxType.introspect, snd)) true = (0, 0, 0, 1, 0)
• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inr (MIPRE.Introspection.AuxType.sample, snd)) true = (0, 0, 0, 1, 0)
• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inr (MIPRE.Introspection.AuxType.read, snd)) true = (0, 0, 1, 1, 0)
• MIPRE.Tailored.Intro.LenIntro.coef (Sum.inr (MIPRE.Introspection.AuxType.hide k, snd)) true = (0, 0, 2, 0, 0)

theorem MIPRE.Tailored.Intro.LenIntro.lin_coef (k j R : ℕ) (t : Label) (κ : Bool) : lin (coef t κ) k (2 ^ j) (2 ^ 2 ^ j * k) R = if κ = true then Typed.len k j R t - Typed.lenR k j R t else Typed.lenR k j R t

The typed lengths are the combinations of the coefficients, at m = 2^j and Q = 2^m k.

The decoding of a question

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.LenIntro.gd : ℕ

The number of bits of a graph view.

Equations

• MIPRE.Tailored.Intro.LenIntro.gd = MIPRE.CL.Detyping.graphDim MIPRE.Tailored.Intro.LenIntro.Label

noncomputable def MIPRE.Tailored.Intro.LenIntro.coefAt (g : CL.Graph.Coord Label → CL.𝔽₂) (κ : Bool) : Coef

The coefficients at a graph view and a kind: those of the label it decodes to, zero when it does not decode.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.LenIntro.UCoef : Type

Coefficients in unary.

Equations

• MIPRE.Tailored.Intro.LenIntro.UCoef = (MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary)

def MIPRE.Tailored.Intro.LenIntro.ucoef (v : Coef) : UCoef

A coefficient vector in unary.

Equations

• MIPRE.Tailored.Intro.LenIntro.ucoef v = (MIPRE.Cost.unary v.1, MIPRE.Cost.unary v.2.1, MIPRE.Cost.unary v.2.2.1, MIPRE.Cost.unary v.2.2.2.1, MIPRE.Cost.unary v.2.2.2.2)

noncomputable def MIPRE.Tailored.Intro.LenIntro.tab (p : (Fin gd → CL.𝔽₂) × Bool) : UCoef

The finite table: from the bits of a graph view and a kind, the coefficients.

Equations

• MIPRE.Tailored.Intro.LenIntro.tab p = MIPRE.Tailored.Intro.LenIntro.ucoef (MIPRE.Tailored.Intro.LenIntro.coefAt (MIPRE.CL.pull MIPRE.CL.Detyping.graphEquiv.toEmbedding p.1) p.2)

noncomputable def MIPRE.Tailored.Intro.LenIntro.linF : Cost.PolyTimeFun (UCoef × Cost.Unary × Cost.Unary × Cost.Unary × Cost.Unary) Cost.Unary

The combination of unary coefficients with the unary parameters (k, m, Q, R).

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.Intro.LenIntro.length_linF (v : Coef) (k m Q R : ℕ) : List.length (linF.toFun (ucoef v, Cost.unary k, Cost.unary m, Cost.unary Q, Cost.unary R)) = lin v k m Q R

The stages

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.LenIntro.In0 : Type

The input of the core: (λ, n, d).

Equations

• MIPRE.Tailored.Intro.LenIntro.In0 = (ℕ × ℕ × MIPRE.Cost.Data)

noncomputable def MIPRE.Tailored.Intro.LenIntro.g1 : Cost.PolyTimeFun In0 ((Cost.Data × ℕ × ℕ) × ℕ × ℕ)

Stage 1: keep (d, (λ, n)), and pass (λ, n) to the bounds program.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Tailored.Intro.LenIntro.g1_apply (a : In0) : g1.toFun a = ((a.2.2, a.1, a.2.1), a.1, a.2.1)

noncomputable def MIPRE.Tailored.Intro.LenIntro.g4 : Cost.PolyTimeFun ((Cost.Data × ℕ × ℕ) × Cost.Unary × Cost.Unary) ((Cost.Data × Cost.Unary × Cost.Unary) × ℕ × ℕ)

Stage 4: keep (d, (Q, R)) in unary, and pass (λ, n) to the parameters program.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Tailored.Intro.LenIntro.g4_apply (a : (Cost.Data × ℕ × ℕ) × Cost.Unary × Cost.Unary) : g4.toFun a = ((a.1.1, a.2), a.1.2)

noncomputable def MIPRE.Tailored.Intro.LenIntro.readX : Cost.PolyTimeFun Cost.Data Cost.BitStr

The question bits read off d = (x, κ).

Equations

• MIPRE.Tailored.Intro.LenIntro.readX = MIPRE.CL.Detyping.Program.readBits.comp MIPRE.Cost.PolyTimeFun.treeHead

noncomputable def MIPRE.Tailored.Intro.LenIntro.readK : Cost.PolyTimeFun Cost.Data Bool

The kind read off d = (x, κ).

Equations

• MIPRE.Tailored.Intro.LenIntro.readK = MIPRE.CL.Detyping.Program.rawTruthProg.comp MIPRE.Cost.PolyTimeFun.treeTail

theorem MIPRE.Tailored.Intro.LenIntro.readX_encode (x : Cost.BitStr) (κ : Bool) : readX.toFun (Cost.encode (x, κ)) = x

theorem MIPRE.Tailored.Intro.LenIntro.readK_encode (x : Cost.BitStr) (κ : Bool) : readK.toFun (Cost.encode (x, κ)) = κ

noncomputable def MIPRE.Tailored.Intro.LenIntro.g6 : Cost.PolyTimeFun ((Cost.Data × Cost.Unary × Cost.Unary) × Cost.Unary × Cost.Unary × Cost.Unary) Cost.Unary

Stage 6, the output: (d, (Q, R)) and (k, j, m) in unary give the length in unary.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.Intro.LenIntro.g6_apply (d : Cost.Data) (Q R k j m : ℕ) : g6.toFun ((d, Cost.unary Q, Cost.unary R), Cost.unary k, Cost.unary j, Cost.unary m) = linF.toFun (ucoef (coefAt (CL.Detyping.graphOfBits (readX.toFun d)) (readK.toFun d)), Cost.unary k, Cost.unary m, Cost.unary Q, Cost.unary R)

noncomputable def MIPRE.Tailored.Intro.LenIntro.core (c : ℕ) : Cost.Prog

The core of the calculator, on (λ, n, d).

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.Intro.LenIntro.core_wellScoped (c : ℕ) : Cost.Prog.WellScoped 1 (core c)

noncomputable def MIPRE.Tailored.Intro.LenIntro.coreOut (c lam n : ℕ) (d : Cost.Data) : Cost.Unary

The output of the core at (λ, n, d).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Tailored.Intro.LenIntro.coreCost (c lam n : ℕ) (d : Cost.Data) : ℕ

The cost of the core at (λ, n, d), stage by stage.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.Intro.LenIntro.core_runsLe (c lam n : ℕ) (d : Cost.Data) : Calls.RunsLe (core c) (Cost.encode (lam, n, d)) (Cost.encode (coreOut c lam n d)) (coreCost c lam n d)

The run of the core.

The calculator

def MIPRE.Tailored.Intro.LenIntro.lenWrap (p : Cost.Prog) : Cost.Prog

Inspect the index in place: at n = 0 (and on malformed inputs) output nil, otherwise run p on the input.

Equations

• MIPRE.Tailored.Intro.LenIntro.lenWrap p = MIPRE.Cost.Prog.elim 0 MIPRE.Cost.Prog.nil (MIPRE.Cost.Prog.elim 0 MIPRE.Cost.Prog.nil (MIPRE.Cost.Prog.callVar 4 p))

theorem MIPRE.Tailored.Intro.LenIntro.lenWrap_wellScoped {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) : Cost.Prog.WellScoped 1 (lenWrap p)

theorem MIPRE.Tailored.Intro.LenIntro.lenWrap_runs_zero (p : Cost.Prog) (d : Cost.Data) : (lenWrap p).Runs ((Cost.encode 0).cons d) Cost.Data.nil 3

theorem MIPRE.Tailored.Intro.LenIntro.lenWrap_runs_pos {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) {n : ℕ} (hn : 1 ≤ n) (d r : Cost.Data) (t : ℕ) (hr : p.Runs ((Cost.encode n).cons d) r t) : (lenWrap p).Runs ((Cost.encode n).cons d) r (t + ((Cost.encode n).cons d).size + 4)

noncomputable def MIPRE.Tailored.Intro.LenIntro.lenProg (c lam : ℕ) : Cost.Prog

The program of the calculator at λ: empty at λ = 0, otherwise the core with λ stored, behind the index test.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.Intro.LenIntro.lenProg_wellScoped (c lam : ℕ) : Cost.Prog.WellScoped 1 (lenProg c lam)

noncomputable def MIPRE.Tailored.Intro.LenIntro.lenIntroC (c lam : ℕ) : Decider

The answer-length calculator of the introspection verifier at the constant c and level λ.

Equations

• MIPRE.Tailored.Intro.LenIntro.lenIntroC c lam = { prog := MIPRE.Tailored.Intro.LenIntro.lenProg c lam, closed := ⋯ }

noncomputable def MIPRE.Tailored.Intro.LenIntro.lenWrapF : Cost.PolyTimeFun Cost.Prog Cost.Prog

The wrapper, as a polynomial-time map on descriptions.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.Intro.LenIntro.lenWrapF_apply (p : Cost.Prog) : lenWrapF.toFun p = lenWrap p

noncomputable def MIPRE.Tailored.Intro.LenIntro.lenProgF (c : ℕ) : Cost.PolyTimeFun ℕ Cost.Prog

The calculator's program from λ, in polynomial time.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.Intro.LenIntro.lenProgF_eq (c lam : ℕ) : (lenProgF c).toFun lam = (lenIntroC c lam).prog

theorem MIPRE.Tailored.Intro.LenIntro.lenIntroC_runs_pos (c : ℕ) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) (d : Cost.Data) : Calls.RunsLe (lenIntroC c lam).prog ((Cost.encode n).cons d) (Cost.encode (coreOut c lam n d)) (coreCost c lam n d + (Cost.encode lam).size + 2 * ((Cost.encode n).cons d).size + 7)

The run of the calculator at positive λ and n.

What the calculator outputs

noncomputable def MIPRE.Tailored.Intro.LenIntro.lenAt (c lam n : ℕ) (x : Cost.BitStr) (κ : Bool) : ℕ

The length the calculator outputs on (n, x, κ): 0 at λ = 0 or n = 0, otherwise the combination of the coefficients of the label x's graph view decodes to.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.Intro.LenIntro.length_coreOut (c lam n : ℕ) (x : Cost.BitStr) (κ : Bool) : List.length (coreOut c lam n (Cost.encode (x, κ))) = lin (coefAt (CL.Detyping.graphOfBits x) κ) (kOf c lam n) (2 ^ jOf c lam n) (Introspection.SourceCompiler.registerBits c lam n) (Introspection.SourceCompiler.originalBound lam n)

theorem MIPRE.Tailored.Intro.LenIntro.lenIntroC_lenIs (c lam n : ℕ) (x : Cost.BitStr) (κ : Bool) : LenIs (lenIntroC c lam) n x κ (lenAt c lam n x κ)

What the calculator outputs, on every bit string and every n, λ.

theorem MIPRE.Tailored.Intro.LenIntro.lenAt_eq (c : ℕ) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) (x : Cost.BitStr) (κ : Bool) : lenAt c lam n x κ = (Option.map (fun (p : Bool × Label) => introLen c lam n κ p.2) (CL.Detyping.decodeView E (CL.Detyping.graphOfBits x))).getD 0

At positive λ and n, the output is the length of the label the graph view decodes to, 0 when it does not decode.

theorem MIPRE.Tailored.Intro.LenIntro.lenIntroC_lenIs_question (c : ℕ) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) {s : ℕ} (q : CL.Detyping.Coord Label (Fin s) → CL.𝔽₂) (κ : Bool) : LenIs (lenIntroC c lam) n (CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv s) q)) κ ((Option.map (introLen c lam n κ) (typeOf E q)).getD 0)

The calculator at a detyped question: at positive λ and n, on the bits of a detyped question q (numbered as the reference verifier numbers them, vectorEquiv), it outputs the readable (κ = false) or linear (κ = true) length of the label q decodes to, 0 when it does not decode — the lengths of the presented game, TypedData.detype.

theorem MIPRE.Tailored.Intro.LenIntro.lenIntroC_lenIs_detype (c : ℕ) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) {s : ℕ} (D : TypedData Label (Fin s)) (hR : D.lenR = introLenR c lam n) (hL : D.lenL = introLenL c lam n) (μ : (CL.Detyping.Coord Label (Fin s) → ZMod 2) → (CL.Detyping.Coord Label (Fin s) → ZMod 2) → ℝ) (hμ : ∀ (x y : CL.Detyping.Coord Label (Fin s) → ZMod 2), 0 ≤ μ x y) (hμ1 : ∑ x : CL.Detyping.Coord Label (Fin s) → ZMod 2, ∑ y : CL.Detyping.Coord Label (Fin s) → ZMod 2, μ x y = 1) (q : CL.Detyping.Coord Label (Fin s) → CL.𝔽₂) : LenIs (lenIntroC c lam) n (CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv s) q)) false ((TypedData.detype E D μ hμ hμ1).lenR q) ∧ LenIs (lenIntroC c lam) n (CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv s) q)) true ((TypedData.detype E D μ hμ hμ1).lenL q)

The same, read on a detyped tailored game whose typed lengths are introLenR, introLenL.

The costs

theorem MIPRE.Tailored.Intro.LenIntro.esize_le_four (x : ℕ) : Cost.esize x ≤ 4 * x + 1

def MIPRE.Tailored.Intro.LenIntro.scale (c u : ℕ) : ℕ

The scale of the parameters at u = λ n: 2^{(2c + 2)(u + 2)}.

Equations

• MIPRE.Tailored.Intro.LenIntro.scale c u = 2 ^ ((2 * c + 2) * (u + 2))

theorem MIPRE.Tailored.Intro.LenIntro.one_le_scale (c u : ℕ) : 1 ≤ scale c u

theorem MIPRE.Tailored.Intro.LenIntro.params_le_scale (c : ℕ) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) : lam ≤ scale c (lam * n) ∧ n ≤ scale c (lam * n) ∧ lam * n ≤ scale c (lam * n) ∧ Introspection.SourceCompiler.registerBits c lam n ≤ scale c (lam * n) ∧ Introspection.SourceCompiler.originalBound lam n ≤ scale c (lam * n)

The parameters at positive λ and n are at most the scale.

noncomputable def MIPRE.Tailored.Intro.LenIntro.costF (c z : ℕ) : ℕ

A majorant of the cost of the calculator at positive λ and n, in z = scale + |d|.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.Intro.LenIntro.costF_polyBounded (c : ℕ) : Cost.PolyBounded (costF c)

theorem MIPRE.Tailored.Intro.LenIntro.cost_le_costF {c : ℕ} (hc : 1 ≤ c) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) (d : Cost.Data) : coreCost c lam n d + (Cost.encode lam).size + 2 * ((Cost.encode n).cons d).size + 7 ≤ costF c (scale c (lam * n) + d.size)

The cost at positive λ and n is at most the majorant at z = scale + |d|.

theorem MIPRE.Tailored.Intro.LenIntro.mul_le_pow {A u C : ℕ} (hu : 1 ≤ u) (hC : 1 ≤ C) (hA : A ≤ 2 ^ (C - 1)) : A * (u + 1) ≤ (u + 1) ^ C

A (u + 1) ≤ (u + 1)^C once A ≤ 2^{C - 1}, for u ≥ 1.

theorem MIPRE.Tailored.Intro.LenIntro.lin_coef_le (t : Label) (κ : Bool) (k m Q R : ℕ) : lin (coef t κ) k m Q R ≤ 2 * k + m * k + 2 * Q + R + 3

theorem MIPRE.Tailored.Intro.LenIntro.lin_coefAt_le (g : CL.Graph.Coord Label → CL.𝔽₂) (κ : Bool) (k m Q R : ℕ) : lin (coefAt g κ) k m Q R ≤ 2 * k + m * k + 2 * Q + R + 3

theorem MIPRE.Tailored.Intro.LenIntro.lenIntroC_budget {c : ℕ} (hc : 1 ≤ c) : ∃ (C : ℕ), ∀ (lam n : ℕ), (lenIntroC c lam).TimeBoundAt n (Introspection.ansBound C lam n) C ∧ LenBound (lenIntroC c lam) n (Introspection.ansBound C lam n)

The costs of the calculator, in the shape of Introspection.budget: a constant C with the calculator within 2^{(λn + 1)^C} at degree C on every input, and its lengths at most 2^{(λn + 1)^C}.

theorem MIPRE.Tailored.Intro.LenIntro.lenIntroC_lenTotal (c lam n dim : ℕ) : LenTotal (lenIntroC c lam) n dim

The calculator halts at every question, of every dimension.

At the constant of Introspection.seven

noncomputable def MIPRE.Tailored.Intro.LenIntro.lenIntro (lam : ℕ) : Decider

The answer-length calculator L^intro_λ of the tailored presentation of Introspection.seven.

Equations

• MIPRE.Tailored.Intro.LenIntro.lenIntro lam = MIPRE.Tailored.Intro.LenIntro.lenIntroC MIPRE.Introspection.sevenConstant lam

noncomputable def MIPRE.Tailored.Intro.LenIntro.lenIntroProg : Cost.PolyTimeFun ℕ Cost.Prog

Its program from λ, in polynomial time.

Equations

• MIPRE.Tailored.Intro.LenIntro.lenIntroProg = MIPRE.Tailored.Intro.LenIntro.lenProgF MIPRE.Introspection.sevenConstant

theorem MIPRE.Tailored.Intro.LenIntro.lenIntroProg_eq (lam : ℕ) : lenIntroProg.toFun lam = (lenIntro lam).prog

theorem MIPRE.Tailored.Intro.LenIntro.lenIntro_lenIs {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) {s : ℕ} (q : CL.Detyping.Coord Label (Fin s) → CL.𝔽₂) (κ : Bool) : LenIs (lenIntro lam) n (CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv s) q)) κ ((Option.map (introLen Introspection.sevenConstant lam n κ) (typeOf E q)).getD 0)

Correctness: at positive λ and n, at every detyped question, the presented lengths of the label the question decodes to (0 when it does not decode).

theorem MIPRE.Tailored.Intro.LenIntro.lenIntro_lenIs_zero {lam n : ℕ} (h : lam = 0 ∨ n = 0) (x : Cost.BitStr) (κ : Bool) : LenIs (lenIntro lam) n x κ 0

At λ = 0 or n = 0, the calculator outputs 0 everywhere.

theorem MIPRE.Tailored.Intro.LenIntro.lenIntro_budget : ∃ (C : ℕ), ∀ (lam n : ℕ), (lenIntro lam).TimeBoundAt n (Introspection.budget C lam n).D (Introspection.budget C lam n).k ∧ LenBound (lenIntro lam) n (Introspection.budget C lam n).B

The costs, in the shape of Introspection.budget.

theorem MIPRE.Tailored.Intro.LenIntro.lenIntro_lenTotal (lam n dim : ℕ) : LenTotal (lenIntro lam) n dim

The calculator halts at every question.