Moment ambiguity and exact contact certificates

Abstract

Rational contacts certify an attained largest query difference and an attained least residual budget. Support-monotone compression preserves their optimality.

All coefficients are rational. Feature has type Fin n to Fin d to Q; query and the two weights have type Fin n to Q; tolerance and predictor coefficients have type Fin d to Q. Indices i and j range over Fin n and Fin d respectively. Named applications also denote structure-field access.

Definition 1.1 (Two probability laws with moment tolerances).

$$\forall n,d,feature,tolerance,high,low,(\mathrm{MomentTolerancePair}(feature,tolerance,high,low))\iff ((\forall i,(0)\le (\mathrm{high}(i)))\wedge ((\sum _i(\mathrm{high}(i)))=(1))\wedge (\forall i,(0)\le (\mathrm{low}(i)))\wedge ((\sum _i(\mathrm{low}(i)))=(1))\wedge (\forall j,(|(\mathrm{linearObjective}((\lambda i\mapsto \mathrm{feature}(i,j)),high))-(\mathrm{linearObjective}((\lambda i\mapsto \mathrm{feature}(i,j)),low))|)\le (\mathrm{tolerance}(j))))$$

Formalization. D5/S0/Certificates/RationalMomentAmbiguityCertificate.MomentTolerancePair (✓ std3).

Source. Repository-derived.

Commentary.

Tolerances compare the two models directly. The laws have separate nonnegativity and normalization conditions.

Definition 1.2 (Envelope on every allowed atom).

$$\forall n,d,feature,query,envelope,(\mathrm{GlobalQueryEnvelope}(feature,query,envelope))\iff (\forall i,((\mathrm{lower}(envelope))\le (\mathrm{queryResidual}(feature,query,envelope,i)))\wedge ((\mathrm{queryResidual}(feature,query,envelope,i))\le (\mathrm{upper}(envelope))))$$

Formalization. D5/S0/Certificates/RationalMomentAmbiguityCertificate.GlobalQueryEnvelope (✓ std3).

Source. Repository-derived.

Commentary.

The check covers the whole carrier, including atoms absent from both proposed witnesses.

Definition 1.3 (Slope-weighted uncertainty cost).

$$\forall d,tolerance,envelope,(\mathrm{momentToleranceCost}(tolerance,envelope))=(\sum _j((|\mathrm{coefficient}(envelope,j)|)\cdot (\mathrm{tolerance}(j))))$$

Formalization. D5/S0/Certificates/RationalMomentAmbiguityCertificate.momentToleranceCost (✓ std3).

Source. Repository-derived.

Commentary.

Absolute predictor slopes weight the coordinatewise moment tolerances.

Definition 1.4 (Width plus uncertainty).

$$\forall d,tolerance,envelope,(\mathrm{residualBudget}(tolerance,envelope))=(((\mathrm{upper}(envelope))-(\mathrm{lower}(envelope)))+(\mathrm{momentToleranceCost}(tolerance,envelope)))$$

Formalization. D5/S0/Certificates/RationalMomentAmbiguityCertificate.residualBudget (✓ std3).

Source. Repository-derived.

Commentary.

This is the dual value compared against all admissible query differences.

Theorem 1.5 (Uniform query bound).

$$\forall n,d,feature,query,tolerance,high,low,envelope,((\mathrm{MomentTolerancePair}(feature,tolerance,high,low))\wedge (\mathrm{GlobalQueryEnvelope}(feature,query,envelope)))\Rightarrow ((|(\mathrm{linearObjective}(query,high))-(\mathrm{linearObjective}(query,low))|)\le (\mathrm{residualBudget}(tolerance,envelope)))$$

Proof. Machine-checked in Lean as D5/S0/Certificates/RationalMomentAmbiguityCertificate.query_gap_le_residualBudget (✓ std3). ∎

Source. Repository-derived.

Commentary.

The existing expectation enclosure is applied to both laws, then their predictor-center difference is bounded using the nominated moment errors.

Theorem 1.6 (Exact three-part gap identity).

$$\forall n,d,feature,query,tolerance,high,low,envelope,(((\sum _i(\mathrm{high}(i)))=(1))\wedge ((\sum _i(\mathrm{low}(i)))=(1)))\Rightarrow (((\mathrm{residualBudget}(tolerance,envelope))-(((\mathrm{linearObjective}(query,high))-(\mathrm{linearObjective}(query,low)))))=(((\sum _i((((\mathrm{upper}(envelope))-(\mathrm{queryResidual}(feature,query,envelope,i))))\cdot (\mathrm{high}(i))))+(\sum _i((((\mathrm{queryResidual}(feature,query,envelope,i))-(\mathrm{lower}(envelope))))\cdot (\mathrm{low}(i)))))+(\sum _j(((|\mathrm{coefficient}(envelope,j)|)\cdot (\mathrm{tolerance}(j)))-((\mathrm{coefficient}(envelope,j))\cdot (((\mathrm{linearObjective}((\lambda i\mapsto \mathrm{feature}(i,j)),high))-(\mathrm{linearObjective}((\lambda i\mapsto \mathrm{feature}(i,j)),low)))))))))$$

Proof. Machine-checked in Lean as D5/S0/Certificates/RationalMomentAmbiguityCertificate.primal_dual_gap_identity (✓ std3). ∎

Source. Repository-derived.

Commentary.

The identity requires only normalization. Under pair and global-envelope feasibility its upper-contact, lower-contact and signed-moment contributions are all nonnegative.

Definition 1.7 (Data-only certificate).

Lean statement: D5/S0/Certificates/RationalMomentAmbiguityCertificate.ContactCertificate

Formalization. D5/S0/Certificates/RationalMomentAmbiguityCertificate.ContactCertificate (✓ std3).

Source. Repository-derived.

Commentary.

The structure has exactly high : Fin n to Q, low : Fin n to Q, and envelope : QueryEnvelope d. There are no proof fields.

Definition 1.8 (Contact and alignment conditions).

$$\forall n,d,feature,query,tolerance,certificate,(\mathrm{ValidContactCertificate}(feature,query,tolerance,certificate))\iff ((\mathrm{MomentTolerancePair}(feature,tolerance,\mathrm{high}(certificate),\mathrm{low}(certificate)))\wedge (\mathrm{GlobalQueryEnvelope}(feature,query,\mathrm{envelope}(certificate)))\wedge (\forall i,((\mathrm{high}(certificate,i))\ne (0))\Rightarrow ((\mathrm{queryResidual}(feature,query,\mathrm{envelope}(certificate),i))=(\mathrm{upper}(\mathrm{envelope}(certificate)))))\wedge (\forall i,((\mathrm{low}(certificate,i))\ne (0))\Rightarrow ((\mathrm{queryResidual}(feature,query,\mathrm{envelope}(certificate),i))=(\mathrm{lower}(\mathrm{envelope}(certificate)))))\wedge (\forall j,((\mathrm{coefficient}(\mathrm{envelope}(certificate),j))\cdot (((\mathrm{linearObjective}((\lambda i\mapsto \mathrm{feature}(i,j)),\mathrm{high}(certificate)))-(\mathrm{linearObjective}((\lambda i\mapsto \mathrm{feature}(i,j)),\mathrm{low}(certificate))))))=((|\mathrm{coefficient}(\mathrm{envelope}(certificate),j)|)\cdot (\mathrm{tolerance}(j)))))$$

Formalization. D5/S0/Certificates/RationalMomentAmbiguityCertificate.ValidContactCertificate (✓ std3).

Source. Repository-derived.

Commentary.

The high support touches the upper residual level and the low support the lower level. Predictor slopes align with the signed moment discrepancies.

Definition 1.9 (Finite rational checker).

$$\forall n,d,feature,query,tolerance,certificate,(\mathrm{checkContactCertificate}(feature,query,tolerance,certificate))=(\mathrm{decide}(\mathrm{ValidContactCertificate}(feature,query,tolerance,certificate)))$$

Formalization. D5/S0/Certificates/RationalMomentAmbiguityCertificate.checkContactCertificate (✓ std3).

Source. Repository-derived.

Commentary.

Decides all probability, moment, envelope, contact and alignment conditions from the raw data.

Theorem 1.10 (Acceptance reflection).

$$\forall n,d,feature,query,tolerance,certificate,((\mathrm{checkContactCertificate}(feature,query,tolerance,certificate))=(true))\iff (\mathrm{ValidContactCertificate}(feature,query,tolerance,certificate))$$

Proof. Machine-checked in Lean as D5/S0/Certificates/RationalMomentAmbiguityCertificate.checkContactCertificate_eq_true_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

Acceptance is equivalent to the displayed finite contract.

Theorem 1.11 (Oriented gap attains the budget).

$$\forall n,d,feature,query,tolerance,certificate,(\mathrm{ValidContactCertificate}(feature,query,tolerance,certificate))\Rightarrow (((\mathrm{linearObjective}(query,\mathrm{high}(certificate)))-(\mathrm{linearObjective}(query,\mathrm{low}(certificate))))=(\mathrm{residualBudget}(tolerance,\mathrm{envelope}(certificate))))$$

Proof. Machine-checked in Lean as D5/S0/Certificates/RationalMomentAmbiguityCertificate.contact_gap_eq_budget (✓ std3). ∎

Source. Repository-derived.

Commentary.

Contact and alignment make every contribution to the primal-dual gap vanish.

Definition 1.12 (Attainable query differences).

$$\forall n,d,feature,query,tolerance,value,((value)\in (\mathrm{ambiguityValues}(feature,query,tolerance)))\iff (\exists high,low,(\mathrm{MomentTolerancePair}(feature,tolerance,high,low))\wedge ((value)=(|(\mathrm{linearObjective}(query,high))-(\mathrm{linearObjective}(query,low))|)))$$

Formalization. D5/S0/Certificates/RationalMomentAmbiguityCertificate.ambiguityValues (✓ std3).

Source. Repository-derived.

Commentary.

Both probability laws vary over the same finite carrier subject to the same tolerance vector.

Definition 1.13 (All valid residual budgets).

$$\forall n,d,feature,query,tolerance,value,((value)\in (\mathrm{residualBudgetValues}(feature,query,tolerance)))\iff (\exists envelope,(\mathrm{GlobalQueryEnvelope}(feature,query,envelope))\wedge ((value)=(\mathrm{residualBudget}(tolerance,envelope))))$$

Formalization. D5/S0/Certificates/RationalMomentAmbiguityCertificate.residualBudgetValues (✓ std3).

Source. Repository-derived.

Commentary.

The predictor and envelope may vary, while the carrier, query, features and tolerances stay fixed.

Theorem 1.14 (Attained maximum and attained minimum).

$$\forall n,d,feature,query,tolerance,certificate,((\mathrm{checkContactCertificate}(feature,query,tolerance,certificate))=(true))\Rightarrow ((\mathrm{IsGreatest}(\mathrm{ambiguityValues}(feature,query,tolerance),\mathrm{residualBudget}(tolerance,\mathrm{envelope}(certificate))))\wedge (\mathrm{IsLeast}(\mathrm{residualBudgetValues}(feature,query,tolerance),\mathrm{residualBudget}(tolerance,\mathrm{envelope}(certificate)))))$$

Proof. Machine-checked in Lean as D5/S0/Certificates/RationalMomentAmbiguityCertificate.checkContactCertificate_sound (✓ std3). ∎

Source. Repository-derived.

Commentary.

The same accepted value is the largest feasible query difference and the least valid residual budget. No general certificate-discovery or certificate-existence theorem is claimed.

Theorem 1.15 (Sparse optimal witnesses without another query coordinate).

$$\forall n,d,feature,query,tolerance,certificate,high,low,highSteps,lowSteps,((\mathrm{ValidContactCertificate}(feature,query,tolerance,certificate))\wedge ((\mathrm{checkCompression}(feature,\mathrm{high}(certificate),highSteps))=(\mathrm{some}(high)))\wedge ((\mathrm{checkCompression}(feature,\mathrm{low}(certificate),lowSteps))=(\mathrm{some}(low))))\Rightarrow ((\mathrm{ValidContactCertificate}(feature,query,tolerance,\{(high)=(high),(low)=(low),(envelope)=(\mathrm{envelope}(certificate))\}))\wedge ((\mathrm{card}(\mathrm{activeAtoms}(high)))\le ((d)+(1)))\wedge ((\mathrm{card}(\mathrm{activeAtoms}(low)))\le ((d)+(1)))\wedge (((\mathrm{linearObjective}(query,high))-(\mathrm{linearObjective}(query,low)))=((\mathrm{linearObjective}(query,\mathrm{high}(certificate)))-(\mathrm{linearObjective}(query,\mathrm{low}(certificate))))))$$

Proof. Machine-checked in Lean as D5/S0/Certificates/RationalMomentAmbiguityCertificate.contact_certificate_preserved_by_compression (✓ std3). ∎

Source. Repository-derived.

Commentary.

highSteps and lowSteps are lists of existing EliminationStep values. Separate support-monotone compression preserves the d feature moments, both residual contact levels and the signed alignment. Each endpoint has at most d+1 active atoms and the exact query gap is unchanged.

References

• Truth anchor: D5/S0/Certificates/RationalMomentAmbiguityCertificate.ContactCertificate
• Truth anchor: D5/S0/Certificates/RationalMomentAmbiguityCertificate.GlobalQueryEnvelope
• Truth anchor: D5/S0/Certificates/RationalMomentAmbiguityCertificate.MomentTolerancePair
• Truth anchor: D5/S0/Certificates/RationalMomentAmbiguityCertificate.ValidContactCertificate
• Truth anchor: D5/S0/Certificates/RationalMomentAmbiguityCertificate.ambiguityValues
• Truth anchor: D5/S0/Certificates/RationalMomentAmbiguityCertificate.checkContactCertificate
• Truth anchor: D5/S0/Certificates/RationalMomentAmbiguityCertificate.checkContactCertificate_eq_true_iff
• Truth anchor: D5/S0/Certificates/RationalMomentAmbiguityCertificate.checkContactCertificate_sound
• Truth anchor: D5/S0/Certificates/RationalMomentAmbiguityCertificate.contact_certificate_preserved_by_compression
• Truth anchor: D5/S0/Certificates/RationalMomentAmbiguityCertificate.contact_gap_eq_budget
• Truth anchor: D5/S0/Certificates/RationalMomentAmbiguityCertificate.momentToleranceCost
• Truth anchor: D5/S0/Certificates/RationalMomentAmbiguityCertificate.primal_dual_gap_identity
• Truth anchor: D5/S0/Certificates/RationalMomentAmbiguityCertificate.query_gap_le_residualBudget
• Truth anchor: D5/S0/Certificates/RationalMomentAmbiguityCertificate.residualBudget
• Truth anchor: D5/S0/Certificates/RationalMomentAmbiguityCertificate.residualBudgetValues
• Dependency: D5/S0/Certificates/RationalMomentQueryEnvelope