ARGOS Globe

ARGOS

Sign In

Appendix G

Formal Verification of ARGOS Mathematical Properties

Seventeen core theorems of the ARGOS algorithm have been machine-checked using the Lean 4 proof assistant via the AXLE verification platform. These proofs confirm weight normalization, output boundedness, monotonicity, classification completeness, and threshold ordering with mathematical certainty.

17/17 Verified
0 Disproved
Lean 4.29.0
AXLE Platform

Verified Theorems

19 of 19 PASS
Weight Normalization (4)Output Boundedness (4)Monotonicity (5)Classification (1)Threshold Ordering (1)Alert System (2)Financial Stress (1)Velocity Detection (1)
Theorem 1: Lambda Normalization

The five layered composite weights used in the GRS computation sum to exactly 1.0.

Weight NormalizationPASS
Theorem 2: GRS-z Alpha Normalization

The four GRS-z component weights (H, C, V, D) sum to exactly 1.0.

Weight NormalizationPASS
Theorem 3a: GRS Baseline Lower Bound

For sub-indices in [0, 100], the GRS baseline is bounded below by -15.

Output BoundednessPASS
Theorem 3b: GRS Baseline Upper Bound

For sub-indices in [0, 100], the GRS baseline is bounded above by 85.

Output BoundednessPASS
Theorem 4: GRS-z Unit Interval

Given H, C, V, D all in [0, 1] and alpha weights summing to 1, GRS-z ∈ [0, 1].

Output BoundednessPASS
Theorem 5a: Monotone in ISI

GRS is strictly increasing in the Internal Stability Index, ceteris paribus.

MonotonicityPASS
Theorem 5b: Monotone in ETI

GRS is strictly increasing in the External Threat Index, ceteris paribus.

MonotonicityPASS
Theorem 5c: Antitone in ACI

GRS is strictly decreasing in the Adaptive Capacity Index, ceteris paribus.

MonotonicityPASS
Theorem 5d: Monotone in ENV

The full layered GRS composite is strictly increasing in the Environmental Vulnerability sub-index (ENV), ceteris paribus.

MonotonicityPASS
Theorem 5e: Monotone in SCI

The full layered GRS composite is strictly increasing in the Supply Chain Instability sub-index (SCI), ceteris paribus.

MonotonicityPASS
Theorem 6: Tier Partition Complete

The five risk tiers form a complete, non-overlapping partition of all non-negative reals.

ClassificationPASS
Theorem 7: Net Baseline Weight Sum

The algebraic sum of the five baseline weights (4 positive, 1 negative) equals 0.70.

Weight NormalizationPASS
Theorem 8: Positive Weights Sum

The four positive baseline weights (ISI, ETI, EVI, CEI) sum to 0.85.

Weight NormalizationPASS
Theorem 9: GRS-z Phase Thresholds

The GRS-z phase transition thresholds (0.30, 0.50, 0.70) are strictly ordered in [0, 1].

Threshold OrderingPASS
Theorem 10: Layered GRS Composite Bounds

The full layered GRS composite is bounded in [-8.25, 93.25].

Output BoundednessPASS
Theorem 14: Proximity Band Completeness

Any GRS in [28, 30] lies within the Moderate tier and satisfies the proximity band predicate deterministically.

Alert SystemPASS
Theorem 15: Sub-Index Alert Monotonicity

If a sub-index triggers an alert (≥ 35), any higher value also triggers. The threshold lies below the Elevated tier boundary (45).

Alert SystemPASS
Theorem 16: FSS Weight Normalization and Boundedness

The Financial Stress Sub-indicator weights (0.40, 0.35, 0.25) sum to 1.0, and FSS output is bounded in [0, 100].

Financial StressPASS
Theorem 17: Velocity Detector Sign Consistency

If the GRS velocity exceeds +5.0 points over 2 years, the current GRS is strictly greater than the prior GRS. The threshold is positive.

Velocity DetectionPASS
Independent Replication

Every theorem listed above can be independently verified by any party. The AXLE request IDs serve as permanent, auditable records, but the proofs themselves are fully reproducible.

How to Verify

  1. Install Lean 4.29.0 and Mathlib following the official setup guide at leanprover.github.io.
  2. Copy the Lean 4 proof code from any theorem card above (click the code toggle to reveal the full proof).
  3. Run locally: Save the proof to a .lean file and execute lean --run filename.lean to verify.
  4. Or submit to AXLE: Use the AXLE check endpoint at axle.axiommath.ai with the proof text to receive an independent verification result and a new request ID.

Submitting the same proof text to AXLE will produce a new request ID that can be compared against the original for consistency. The mathematical result is deterministic: identical proof text always yields identical verification outcomes.