Inspection with a Free-Flying Space Manipulator

proof_roadmap

8 min read

Proof roadmap — covered and remaining

The stream goal (user, 2026-07-10): cover all of the pre-risk and risk proofs. Three flowcharts, one per phase. Reading rule:

  • Blue — kernel-checked in ctrllib: the theorem compiles axiom-clean (#print axioms ⊆ {propext, Classical.choice, Quot.sound}). An interfaced module is blue too — its named open hypotheses are drawn separately as the lighter nodes feeding it, per interfaces.
  • Lighter blue — genuinely remaining: an open interface row, an un-formalized target, or an unbuilt rung.
  • Dashed — a documented wall or design decision: a boundary marker, never a proof target.

Node labels are literal Lean identifiers, ledger rows, or obligation ids — evidence tables are folded under each chart. interfaces is the source of truth; this page only draws it.

Pre-risk 6-DOF — the Giordano Prop IV.1 chain

flowchart TD
    classDef sealed fill:#4a90d9,stroke:#2a6099,color:#fff
    classDef open fill:#b8d4f0,stroke:#6a94c0,color:#16324f

    subgraph OPEN["open — genuinely remaining work"]
        IsSolutionTo["IsSolutionTo — flow solves ODE"]
        hreal_hfield["hreal / hfield — moving-metric bracket"]
        hsvd["hsvd — σ_min ↔ det"]
        hsand_hdi["hsand / hdi — cascade inputs"]
        R3_khalil["R3 Khalil layer — unbuilt"]
    end

    subgraph FOUND["foundations and pilot"]
        det_gamma_identity["det_gamma_identity — det Γ pilot"]
        skew_char_p["skew_char_p — skew quadratic form"]
        comparison_functions["ComparisonFunctions — 𝒦∞ 𝒦ℒ toolkit"]
        rayleigh_sandwich["rayleigh_sandwich — Rayleigh–Ritz bounds"]
        gamma_invertible["gamma_isUnit_iff — Γ invertibility"]
    end

    subgraph ENERGY["energy and comparison"]
        lyapunov_comparison["lyapunov_comparison — norm-sq decay"]
        block_lyapunov["blockLyap_coercive — coercive V"]
        time_varying_comparison["comparison_tendsto_zero — time-varying"]
        barbalat["barbalat — standalone lemma"]
    end

    subgraph INV["invariance and passivity"]
        lasalle["lasalle — invariance engine"]
        passivity_identity["passivity_identity — eq 23"]
        passivity_transport["congruence_transport — transported passivity"]
    end

    subgraph COUPLED["coupled and CoM blocks"]
        coupled_field["g2Field — eq 34b field"]
        coupled_dissipation["coupled_hdec — energy decrease"]
        stiffness_residual["stiffness_residual — Jᵀ K injective"]
        com_gas["com_gas — CoM block GAS"]
    end

    subgraph REDUCTION["reduction — EHM"]
        reduction_cascade["reduction_cascade — L4a engine"]
        reduction_stability["reduction_stability — R5 groundwork"]
        reduction_stability_finish["stableSet_of_uniformSemiAttractor — set stability"]
        reduction_attraction["reduction_attraction — ω-limit collapse"]
        reduction_uniformization["reduction_uniformization — hUSA discharge"]
    end

    subgraph CASCADE["cascade"]
        cascade_gas["cascade_gas — Panteley–Loría"]
        seven_dof["nullspace_damping_gas — 7-DOF arm"]
    end

    subgraph ASSEMBLY["assembly"]
        coupled_gas["coupled_gas — Prop IV.1 assembled"]
        propIV1_cascade["propIV1_cascade_gas — 2nd route"]
        reduction_iface_free["reduction_asymptotic_stability_of_asymStableRelativeTo — interface-free"]
        com_gas_matrix["com_gas_matrix — concrete SPD"]
        coupled_gas_matrix["coupled_gas_matrix — concrete SPD"]
    end

    det_gamma_identity --> gamma_invertible
    hsvd --> gamma_invertible
    passivity_identity -.- skew_char_p

    rayleigh_sandwich -->|"discharges QuadSandwich"| lyapunov_comparison
    block_lyapunov -->|"discharges hcpt"| lasalle
    passivity_transport -->|"discharges hM"| passivity_identity

    comparison_functions --> cascade_gas
    time_varying_comparison -->|"eq 35"| cascade_gas

    lasalle --> com_gas
    lasalle --> coupled_gas
    passivity_transport -->|"discharges hpass"| coupled_dissipation
    coupled_field -->|"discharges g2"| coupled_dissipation
    coupled_dissipation -->|"discharges hdec"| coupled_gas
    stiffness_residual --> coupled_gas

    reduction_stability --> reduction_stability_finish
    reduction_uniformization -->|"discharges hUSA"| reduction_stability_finish
    reduction_uniformization -->|"discharges hUSA"| reduction_attraction
    reduction_stability_finish --> reduction_attraction
    reduction_stability_finish -->|"discharges hStable"| reduction_cascade
    reduction_attraction -->|"discharges hLandsInΓ₁"| reduction_cascade
    reduction_cascade --> coupled_gas
    reduction_attraction --> reduction_iface_free
    reduction_uniformization --> reduction_iface_free

    cascade_gas --> propIV1_cascade
    com_gas --> propIV1_cascade
    coupled_gas --> propIV1_cascade
    cascade_gas --> seven_dof

    com_gas --> com_gas_matrix
    rayleigh_sandwich --> com_gas_matrix
    coupled_gas --> coupled_gas_matrix
    rayleigh_sandwich --> coupled_gas_matrix
    gamma_invertible --> coupled_gas_matrix
    stiffness_residual --> coupled_gas_matrix
    passivity_transport --> coupled_gas_matrix

    IsSolutionTo --> lasalle
    IsSolutionTo --> reduction_cascade
    IsSolutionTo --> cascade_gas
    hreal_hfield --> coupled_dissipation
    hreal_hfield --> coupled_gas
    hreal_hfield --> coupled_gas_matrix
    hsand_hdi --> cascade_gas
    hsand_hdi --> seven_dof
    R3_khalil -.->|"re-points cites"| comparison_functions
    R3_khalil -.->|"re-points cites"| barbalat

    class det_gamma_identity,skew_char_p,comparison_functions,rayleigh_sandwich,gamma_invertible,lyapunov_comparison,block_lyapunov,time_varying_comparison,barbalat,lasalle,passivity_identity,passivity_transport,coupled_field,coupled_dissipation,stiffness_residual,com_gas,reduction_cascade,reduction_stability,reduction_stability_finish,reduction_attraction,reduction_uniformization,cascade_gas,seven_dof,coupled_gas,propIV1_cascade,reduction_iface_free,com_gas_matrix,coupled_gas_matrix sealed
    class IsSolutionTo,hreal_hfield,hsvd,hsand_hdi,R3_khalil open

Pre-risk 7-DOF — the redundant-arm extension (P1–P4)

flowchart TD
    S["7th redundant joint<br/>coordinated map Γ wide (12×13)"]
    K["self-motion k̂ = ker Γ<br/>one-dimensional"]
    ZA["z_a inertia-weighted row<br/>Γ_a square, invertible on Ω"]

    S --> K
    K --> ZA

    P1["P1 · M̂ decouples v_n<br/>task-block reconciliation"]
    ZA --> P1

    P2["P2 · CoM row Coriolis-free<br/>expected free — verify"]
    S --> P2

    IDE["inv_deriv_eq<br/>inverse-derivative step"]
    CS["congruence_skew<br/>basis-change of skew"]
    APD["augmented_passivity_decomp<br/>§5 additive identity"]
    APS["augmented_passivity_skew<br/>dM̂/dt − 2Ĉ skew"]
    API["augmented_passivity_identity<br/>eq 23 · 13×13"]
    CX["Ĉ cross-terms exist<br/>workless, passivity safe"]

    ZA --> APD
    IDE --> APD
    APD --> APS
    CS --> APS
    APS --> API
    API --> CX

    HSAND(["hsand · 𝒦∞ sandwich"])
    HDI(["hdi · interconnection ineq"])
    ISOL(["IsSolutionTo · flow solves ODE"])

    CG["cascade_gas<br/>reused 6-DOF stone"]
    PIV["propIV1_cascade_gas<br/>reused com→coupled stone"]

    HSAND --> CG
    HDI --> CG
    HSAND --> PIV
    HDI --> PIV
    ISOL --> PIV

    NDG["nullspace_damping_gas<br/>null-space = driven block"]
    NDD["nullspace_damping_driven<br/>joint state → 0"]

    P1 --> NDG
    CX --> NDG
    CG --> NDG
    NDG --> NDD
    PIV --> NDD

    ALLOC{"1 DOF among 3 objectives<br/>design decision — not a proof target"}
    K --> ALLOC

    classDef sealed fill:#4a90d9,stroke:#2a6099,color:#fff
    classDef open fill:#b8d4f0,stroke:#6a94c0,color:#16324f
    classDef decision fill:#b8d4f0,stroke:#6a94c0,color:#16324f,stroke-dasharray: 5 5

    class IDE,CS,APD,APS,API,CG,PIV,NDG,NDD sealed
    class S,K,ZA,P1,P2,HSAND,HDI,ISOL,CX open
    class ALLOC decision

Risk-aware — obligations A1–E1 (quartet ①–④ highlighted)

Quartet SEALED 2026-07-10 — the library's first risk modules: ① var_subadditivity · ② cvar_inf_form (A1+A5, atoms at the quantile handled) · ③ actuation_bound (bounded case) · ④ gaussian_tail (tail half). The dashed walls below are unchanged — Φ⁻¹, DKW/Massart, σ_min↔det stay documented boundaries.

flowchart TD
  subgraph PA["Phase A — CVaR view scoring"]
    A1["② A1 R-U inf-form"]
    A2["① A2 VaR subadditivity fails"]
    A3["④ A3 Gaussian tail integral"]
    A4["A4 affine of Gaussian"]
    A5["A5 atomic-tail SAA"]
    A6["A6 Hoeffding mean bound"]
    A7["A7 r_fail invariance offline"]
  end
  subgraph PB["Phase B — state uncertainty"]
    B1["B1 covariance propagation"]
    B2["B2 belief-ellipsoid extent"]
    B3["B3 state-cost CVaR"]
    B4["B4 standoff-inflation robustness"]
  end
  subgraph PC["Phase C — actuation uncertainty"]
    C1["③ C1 bounded-noise ultimate bound"]
    C2["C2 vanishing-derate convergence"]
    C3["C3 σ_crit cascade"]
    C4["C4 Rayleigh non-bridge"]
    C5["C5 confidence-gated derate"]
  end
  subgraph PDE["Phases D–E — objective extensions"]
    D1["D1 reconstruction-confidence metric"]
    E1["E1 margin CVaR wrapper"]
  end

  Scmp["comparison_bounded / _tendsto_zero"]
  Sray["rayleigh_sandwich / quadSandwich"]

  Wphi["WALL: Φ⁻¹ / erf absent"]
  Wdkw["WALL: DKW / Massart absent"]
  Wsvd["WALL: σ_min↔det unproved"]
  Wgauss["WALL: unbounded-Gaussian ISS"]
  Wgeom["WALL: margin / occlusion geometry"]

  A5 -->|rides| A1
  B3 -->|reuses| A1
  B3 -->|reuses| A2
  E1 -->|rides| A1
  B2 -->|rides| Sray
  C1 -->|rides| Scmp
  C2 -->|rides| Scmp
  A3 -.->|full α form| Wphi
  A6 -.->|quantile route| Wdkw
  C1 -.->|unbounded case| Wgauss
  C3 -.->|interfaces hsvd| Wsvd
  C4 -.->|does NOT bridge| Wsvd
  E1 -.->|geometry| Wgeom

  classDef sealed fill:#4a90d9,stroke:#2a6099,color:#fff
  classDef open fill:#b8d4f0,stroke:#6a94c0,color:#16324f
  classDef wall fill:#dce9f7,stroke:#6a94c0,color:#16324f,stroke-dasharray: 5 5
  classDef quartet stroke-width:3px

  class Scmp,Sray,B2,C1,C2,A1,A2,A3,A5 sealed
  class A4,A6,B3,E1 open
  class A7,B1,B4,C3,C4,C5,D1,Wphi,Wdkw,Wsvd,Wgauss,Wgeom wall
  class A1,A2,A3,C1 quartet

Graph View

Backlinks