Section 6 — Answer-Valued Self-Improvement Slice Transport

This file contains the answer-valued analogues of the Section 6 slice-transport constructors. The ordinary construction, including selfImprovementInInductionSection, lives in SelfImprovementAssembly.Core and is imported here so that the answer-valued construction can reuse the same Section 9 self-improvement theorem.

References

• blueprint/src/chapter/ch10_induction.tex

noncomputable def MIPStarRE.LDT.MainInductionStep.dummyDiagonalCovariantMeasurement (params : Parameters) [FieldModel params.q] (ι : Type uι) [Fintype ι] [DecidableEq ι] : DiagonalCovariantMeasurement params ι

A covariant diagonal measurement with a fixed zero polynomial outcome.

This measurement is used only as an inert diagonal component when applying the axis-parallel/self-consistency form of self-improvement to an answer-valued slice. The Section 9 conclusion obtained in this way is independent of the diagonal-line failure probability.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.answerSelfImprovementCarrier {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params ι) : SymStrat params ι

Forget the answer-valued diagonal alphabet of a restricted slice, replacing it by an inert ordinary diagonal measurement.

The point, axis-parallel, state, and normalization data are unchanged. This is therefore sufficient for the self-improvement theorem variant whose hypotheses are exactly the axis-parallel and point self-consistency bounds.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.restrictAnswerDiagonalAnswerMeasurement {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (x : Fq params) : IdxProjMeas (DiagonalLine params) (DiagonalLineAnswer params) ι

Restrict an answer-valued diagonal-line measurement to the slice at height x.

This is the answer-valued analogue of restrictDiagonalAnswerMeasurement. Because the diagonal answer alphabet is the full function space on the line, restriction is the total map DiagonalLineAnswer.restrictAtHeight; no low-degree support theorem is needed to define this slice.

Equations

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

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.restrictAnswerDiagonalAnswerMeasurement_postprocess_zero {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (x : Fq params) (ℓ : DiagonalLine params) : (postprocess (restrictAnswerDiagonalAnswerMeasurement params strategy x ℓ).toSubMeas fun (f : DiagonalLineAnswer params) => f zeroCoord) = postprocess (strategy.diagonalMeasurement.toIdxProjMeas (DiagonalLine.appendAtHeight params ℓ x)).toSubMeas fun (f : DiagonalLineAnswer params.next) => f zeroCoord

Evaluating the answer-valued restricted diagonal measurement at the base point recovers the ambient answer-valued diagonal readout.

noncomputable def MIPStarRE.LDT.MainInductionStep.xRestrictedAnswerSymStratOfAnswer {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (x : Fq params) : AnswerSymStrat params ι

The x-restricted strategy of an answer-valued successor strategy.

Paper origin: references/ldt-paper/inductive_step.tex:436-455, in the answer-valued strategy interface used for the recursive slice call.

This is the recursive restriction map needed for a simultaneous answer-valued form of the main induction theorem. It preserves the state, point measurement, axis-parallel measurement, and full answer-valued diagonal measurement on the slice.

Equations

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

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.xRestrictedAnswerSymStratOfAnswer_state {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (x : Fq params) : (xRestrictedAnswerSymStratOfAnswer params strategy x).state = strategy.state

Answer-valued slice restriction does not change the bipartite state.

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.xRestrictedAnswerSymStratOfAnswer_pointMeasurement_apply {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (x : Fq params) (u : Point params) : (xRestrictedAnswerSymStratOfAnswer params strategy x).pointMeasurement u = strategy.pointMeasurement (appendPoint params u x)

Answer-valued slice restriction reindexes point questions by appending the slice height.

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.xRestrictedAnswerSymStratOfAnswer_isNormalized {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (x : Fq params) : ⋯ = ⋯

Answer-valued slice restriction reuses the parent normalization witness.

@[simp]

theorem MIPStarRE.LDT.MainInductionStep.xRestrictedAnswerSymStratOfAnswer_diagonalMeasurement_apply {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) (x : Fq params) (ℓ : DiagonalLine params) : (xRestrictedAnswerSymStratOfAnswer params strategy x).diagonalMeasurement.toIdxProjMeas ℓ = restrictAnswerDiagonalAnswerMeasurement params strategy x ℓ

The diagonal measurement of an answer-valued slice is the full answer-valued restriction of the ambient diagonal measurement.

structure MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.SliceStrategyTransport {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k) : Type (max u_1 uι)

Transport data for producing the answer-valued self-improvement data from concrete per-slice symmetric strategies.

Paper origin: references/ldt-paper/inductive_step.tex:461-551 and references/ldt-paper/self_improvement.tex:631-811; this is the answer-valued restricted-slice interface for the same self-improvement step.

The answer-valued restriction xRestrictedAnswerSymStrat has the paper-faithful answer-valued diagonal interface, while the existing Section 9 self-improvement theorem is stated for ordinary SymStrats. This structure records the stronger route through concrete ordinary slice strategies, together with the state and point-measurement transports needed to move the resulting conclusions back to the answer-valued restricted bookkeeping.

The legacy restricted strategy xRestrictedStrategy is not such an ordinary slice strategy. It is a RestrictedSymStrat, and its diagonal measurement is only the degree-bounded re-embedding of the sampled base-point value. Thus it does not by itself supply the transport-covariant diagonal measurement required by SymStrat.

An ordinary covariant realization is not a formal relabelling of the answer-valued strategy. Diagonal covariance after rebasing a line would force the ordinary polynomial outcome to reproduce all values of the function answer, not only the value at zeroCoord used by the diagonal test. Thus this route requires a genuine low-degree support/interpolation theorem for the answer-valued diagonal measurement. In the absence of such a theorem, the mathematically faithful remaining target is an induction-section self-improvement theorem stated directly for AnswerSymStrat.

The Section 9 analytic proof debt is not stored in this record. The data record constructor below calls the paper-facing theorem selfImprovementInInductionSection; its proof applies the Section 9 theorem and then transports the output estimates to the answer-valued induction notation.

• sliceStrategy : Fq params → SymStrat params ι

  Concrete symmetric strategies realizing the answer-restricted slice interfaces.

• state_eq (x : Fq params) : (self.sliceStrategy x).state = strategy.state

  Each concrete slice strategy uses the ambient state.

• pointMeasurement_eq (x : Fq params) : (self.sliceStrategy x).pointMeasurement = (xRestrictedAnswerSymStrat params strategy x).pointMeasurement

  Its point measurement agrees with the answer-valued restricted-slice point interface.

• averagedPoint_eq (x : Fq params) (h : Polynomial params) : IdxPolyFamily.averagedPointEvaluationOperator (self.sliceStrategy x) h = IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x h

  Its averaged point operator is the averaged slice point operator used by Section 6.

• good (x : Fq params) : (self.sliceStrategy x).IsGood (restrictionPkg.profile.axisParallel x) (restrictionPkg.profile.selfConsistency x) (restrictionPkg.profile.diagonal x)

  The concrete slice strategy is good with the answer-restricted failure profile.

theorem MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.SliceStrategyTransport.averagedPoint_eq_of_pointMeasurement_eq {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (sliceStrategy : Fq params → SymStrat params ι) (hpoint : ∀ (x : Fq params), (sliceStrategy x).pointMeasurement = (xRestrictedAnswerSymStrat params strategy x).pointMeasurement) (x : Fq params) (h : Polynomial params) : IdxPolyFamily.averagedPointEvaluationOperator (sliceStrategy x) h = IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x h

The averaged point-operator compatibility for answer-valued slices follows from point-measurement transport.

Both sides unfold to the same average over strategy.pointMeasurement (appendPoint params u x) once the concrete slice point measurement is identified with xRestrictedAnswerSymStrat.

noncomputable def MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.SliceStrategyTransport.ofPointMeasurementEq {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k) (sliceStrategy : Fq params → SymStrat params ι) (state_eq : ∀ (x : Fq params), (sliceStrategy x).state = strategy.state) (pointMeasurement_eq : ∀ (x : Fq params), (sliceStrategy x).pointMeasurement = (xRestrictedAnswerSymStrat params strategy x).pointMeasurement) (good : ∀ (x : Fq params), (sliceStrategy x).IsGood (restrictionPkg.profile.axisParallel x) (restrictionPkg.profile.selfConsistency x) (restrictionPkg.profile.diagonal x)) : SliceStrategyTransport params strategy eps delta gamma k restrictionPkg inductionPkg

Build answer-valued SliceStrategyTransport without separately assuming averaged point-operator compatibility.

Paper origin: references/ldt-paper/inductive_step.tex:461-551; the averaged point-operator compatibility is a formal transport between the answer-valued restricted slice interface and the Section 9 interface.

The structural averaged-point field is derived from pointMeasurement_eq; the remaining inputs are the concrete slice strategies, their state transport, and their restricted-profile goodness.

Equations

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

theorem MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.SliceStrategyTransport.good_of_restrictedGood {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (sliceStrategy : Fq params → SymStrat params ι) (state_eq : ∀ (x : Fq params), (sliceStrategy x).state = strategy.state) (pointMeasurement_eq : ∀ (x : Fq params), (sliceStrategy x).pointMeasurement = (xRestrictedAnswerSymStrat params strategy x).pointMeasurement) (axisParallelMeasurement_eq : ∀ (x : Fq params), (sliceStrategy x).axisParallelMeasurement.toIdxProjMeas = (xRestrictedAnswerSymStrat params strategy x).axisParallelMeasurement.toIdxProjMeas) (diagonalZeroCoord_eq : ∀ (x : Fq params) (ℓ : DiagonalLine params), (postprocess ((sliceStrategy x).diagonalMeasurement.toIdxProjMeas ℓ).toSubMeas fun (f : DiagonalLinePolynomial params) => f.toFun zeroCoord) = postprocess ((xRestrictedAnswerSymStrat params strategy x).diagonalMeasurement.toIdxProjMeas ℓ).toSubMeas fun (f : DiagonalLineAnswer params) => f zeroCoord) (x : Fq params) : (sliceStrategy x).IsGood (restrictionPkg.profile.axisParallel x) (restrictionPkg.profile.selfConsistency x) (restrictionPkg.profile.diagonal x)

Transport answer-restricted goodness to a concrete slice strategy once the state and verifier-visible measurements agree with xRestrictedAnswerSymStrat.

The diagonal compatibility is stated only after postprocessing both diagonal answer alphabets to their zeroCoord value; this is the comparison used by the LDT diagonal subtest and avoids claiming a false equality between DiagonalLinePolynomial and DiagonalLineAnswer families.

noncomputable def MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.SliceStrategyTransport.ofMeasurementEq {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k) (sliceStrategy : Fq params → SymStrat params ι) (state_eq : ∀ (x : Fq params), (sliceStrategy x).state = strategy.state) (pointMeasurement_eq : ∀ (x : Fq params), (sliceStrategy x).pointMeasurement = (xRestrictedAnswerSymStrat params strategy x).pointMeasurement) (axisParallelMeasurement_eq : ∀ (x : Fq params), (sliceStrategy x).axisParallelMeasurement.toIdxProjMeas = (xRestrictedAnswerSymStrat params strategy x).axisParallelMeasurement.toIdxProjMeas) (diagonalZeroCoord_eq : ∀ (x : Fq params) (ℓ : DiagonalLine params), (postprocess ((sliceStrategy x).diagonalMeasurement.toIdxProjMeas ℓ).toSubMeas fun (f : DiagonalLinePolynomial params) => f.toFun zeroCoord) = postprocess ((xRestrictedAnswerSymStrat params strategy x).diagonalMeasurement.toIdxProjMeas ℓ).toSubMeas fun (f : DiagonalLineAnswer params) => f zeroCoord) : SliceStrategyTransport params strategy eps delta gamma k restrictionPkg inductionPkg

Build answer-valued SliceStrategyTransport from concrete slice strategies and verifier-visible measurement transport.

Paper origin: references/ldt-paper/inductive_step.tex:461-551 and references/ldt-paper/self_improvement.tex:631-811.

This constructor fills both structural fields forced by the answer-restricted interface: averaged point compatibility follows from point-measurement transport, and goodness follows from the answer-restricted failure profile plus state, axis-parallel, and diagonal zero-coordinate transport.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.ofSelfImprovementInInductionSection {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k) (hslice : ∀ (x : Fq params), ∃ (H : ProjSubMeas (Polynomial params) ι) (Z : Quantum.Op ι), CompletenessAtLeast strategy.state H.liftLeft (1 - inductionPkg.sliceError x - answerSliceSelfImprovementError params restrictionPkg x) ∧ ConsRel strategy.state (uniformDistribution (Point params)) (xRestrictedAnswerSymStrat params strategy x).pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (answerSliceSelfImprovementError params restrictionPkg x) ∧ BipartiteSSCRel strategy.state (uniformDistribution Unit) (constSubMeasFamily H.toSubMeas) (answerSliceSelfImprovementError params restrictionPkg x) ∧ SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas H.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas H.toSubMeas)) (answerSliceSelfImprovementError params restrictionPkg x) ∧ tensorFailureExpectation strategy.state Z H.toSubMeas ≤ answerSliceSelfImprovementError params restrictionPkg x ∧ ∀ (h : Polynomial params), IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x h ≤ Z) : AnswerSelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg

Convert the slice-wise outputs feeding the answer-valued restricted-strategy self-improvement stage into the bookkeeping object expected by the answer-valued successor-step construction.

Paper origin: references/ldt-paper/inductive_step.tex:461-551 and references/ldt-paper/self_improvement.tex:631-811.

Equations

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

theorem MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.slice_outputs_ofSliceStrategyTransport {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k) (sliceTransport : SliceStrategyTransport params strategy eps delta gamma k restrictionPkg inductionPkg) (x : Fq params) : ∃ (H : ProjSubMeas (Polynomial params) ι) (Z : Quantum.Op ι), CompletenessAtLeast strategy.state H.liftLeft (1 - inductionPkg.sliceError x - answerSliceSelfImprovementError params restrictionPkg x) ∧ ConsRel strategy.state (uniformDistribution (Point params)) (xRestrictedAnswerSymStrat params strategy x).pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (answerSliceSelfImprovementError params restrictionPkg x) ∧ BipartiteSSCRel strategy.state (uniformDistribution Unit) (constSubMeasFamily H.toSubMeas) (answerSliceSelfImprovementError params restrictionPkg x) ∧ SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas H.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas H.toSubMeas)) (answerSliceSelfImprovementError params restrictionPkg x) ∧ tensorFailureExpectation strategy.state Z H.toSubMeas ≤ answerSliceSelfImprovementError params restrictionPkg x ∧ ∀ (h : Polynomial params), IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x h ≤ Z

Concrete answer-valued slice strategies give the slice-wise Section 9 outputs used by the answer-valued self-improvement data.

Paper origin: references/ldt-paper/inductive_step.tex:461-551 and references/ldt-paper/self_improvement.tex:631-811.

This is an internal transport theorem. It applies selfImprovementInInductionSection to each ordinary slice strategy supplied by SliceStrategyTransport, and then rewrites the state, point-measurement, and averaged-point conclusions back into the answer-restricted notation of the successor step.

theorem MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.slice_outputs_ofAnswerCarrier {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k) (x : Fq params) : ∃ (H : ProjSubMeas (Polynomial params) ι) (Z : Quantum.Op ι), CompletenessAtLeast strategy.state H.liftLeft (1 - inductionPkg.sliceError x - answerSliceSelfImprovementError params restrictionPkg x) ∧ ConsRel strategy.state (uniformDistribution (Point params)) (xRestrictedAnswerSymStrat params strategy x).pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (answerSliceSelfImprovementError params restrictionPkg x) ∧ BipartiteSSCRel strategy.state (uniformDistribution Unit) (constSubMeasFamily H.toSubMeas) (answerSliceSelfImprovementError params restrictionPkg x) ∧ SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas H.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas H.toSubMeas)) (answerSliceSelfImprovementError params restrictionPkg x) ∧ tensorFailureExpectation strategy.state Z H.toSubMeas ≤ answerSliceSelfImprovementError params restrictionPkg x ∧ ∀ (h : Polynomial params), IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x h ≤ Z

The answer-valued restricted slices directly give the slice-wise Section 9 outputs once self-improvement is applied in its axis-parallel/self-consistency form.

Paper origin: references/ldt-paper/inductive_step.tex:461-551 and references/ldt-paper/self_improvement.tex:631-811.

The ordinary carrier used in the proof keeps the slice state, point measurement, and axis-parallel measurement, and replaces only the diagonal measurement by an inert covariant measurement. This is sufficient because the called self-improvement theorem consumes only the axis-parallel and point self-consistency bounds.

noncomputable def MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.ofSliceStrategyTransport {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k) (sliceTransport : SliceStrategyTransport params strategy eps delta gamma k restrictionPkg inductionPkg) : AnswerSelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg

Convert concrete per-slice structural data into the answer-valued Section 6 self-improvement data.

Paper origin: references/ldt-paper/inductive_step.tex:461-551 and references/ldt-paper/self_improvement.tex:631-811.

The construction assumes ordinary slice strategies and their structural measurement transports. It applies the theorem selfImprovementInInductionSection slice-by-slice and transports its fields back to the answer-valued restricted-slice interface via the recorded state and point-measurement equalities.

Equations

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

noncomputable def MIPStarRE.LDT.MainInductionStep.AnswerSelfImprovementData.ofAnswerCarrier {ι : Type uι} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma : Error) (k : ℕ) (restrictionPkg : AnswerSliceRestrictionData params strategy eps delta gamma) (inductionPkg : AnswerPerSliceInductionData params strategy eps delta gamma restrictionPkg k) : AnswerSelfImprovementData params strategy eps delta gamma k restrictionPkg inductionPkg

Construct the answer-valued Section 6 self-improvement data directly from the answer-valued restricted slices.

Paper origin: references/ldt-paper/inductive_step.tex:461-551 and references/ldt-paper/self_improvement.tex:631-811.

This removes the ordinary slice-realization assumption from the self-improvement stage. The construction uses the ordinary carrier only as a device for invoking the Section 9 theorem in the form whose hypotheses are the axis-parallel and point self-consistency estimates.

Equations

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