Coverage
Library: each row is a main result of the library.
- Main results: 17.
- lean-pkg’s claims ledger: ready (
sha256:99271e7536a7de84…).
| Result | Claims | Lean declarations | Ledger | Note |
|---|---|---|---|---|
| The two pitchfork branches | scalar-pitchfork-lean/pitchfork-branch-curves |
ScalarPitchfork.pitchfork_branch_curves |
verified | — |
| One signed zero at a fixed radius | scalar-pitchfork-lean/exists-unique-branch-root-eventually |
ScalarPitchfork.existsUnique_branchRoot_eventually |
verified | — |
| Existence of both branches with explicit amplitude constant and stability sign | scalar-pitchfork-lean/exists-branch-eventually |
ScalarPitchfork.exists_branch_eventually |
verified | — |
| Side and stability of every small nontrivial zero | scalar-pitchfork-lean/branch-side-eventually |
ScalarPitchfork.branch_side_eventually |
verified | — |
| At most one small zero of each sign | scalar-pitchfork-lean/small-zero-eq-branch |
ScalarPitchfork.small_zero_eq_branch |
verified | — |
| Exchange of stability on the exact cubic | scalar-pitchfork-lean/deriv-cubic-field-at-branch |
ScalarPitchfork.deriv_cubicField_at_branch |
verified | — |
| Square-root amplitude error | scalar-pitchfork-lean/abs-sub-sqrt-le-of-cubic-remainder |
ScalarPitchfork.abs_sub_sqrt_le_of_cubic_remainder |
verified | — |
| Remainder bounds from jets at the origin | scalar-pitchfork-lean/remainder-bounds-of-jet |
ScalarPitchfork.remainderBounds_of_jet |
verified | — |
| The stronger remainder bound holds iff the axis condition holds | scalar-pitchfork-lean/strong-bound-iff-axis |
ScalarPitchfork.strongBound_iff_axis |
verified | — |
| The jets at the origin do not give the stronger bound | scalar-pitchfork-lean/jet-not-sufficient-for-strong-bound |
ScalarPitchfork.jet_not_sufficient_for_strongBound |
verified | — |
| A non-compact component has unbounded parameter | scalar-pitchfork-lean/global-s-sup-param-eq-top |
ScalarPitchfork.Global.sSup_param_eq_top |
verified | — |
| The one-sided component is closed | scalar-pitchfork-lean/global-selected-component-is-closed |
ScalarPitchfork.Global.selectedComponent_isClosed |
verified | — |
| Pitchfork branches under the stronger remainder bound | scalar-pitchfork-lean/strong-bounds-of-jetscalar-pitchfork-lean/branch-eventually-of-strong-boundscalar-pitchfork-lean/branch-curves-of-strong-boundscalar-pitchfork-lean/equilibrium-core-of-strong-boundscalar-pitchfork-lean/deriv-zero-of-sq-boundscalar-pitchfork-lean/axis-of-linearization |
ScalarPitchfork.strongBounds_of_jetScalarPitchfork.branch_eventually_of_strongBoundScalarPitchfork.branch_curves_of_strongBoundScalarPitchfork.equilibrium_core_of_strongBoundScalarPitchfork.deriv_zero_of_sq_boundScalarPitchfork.axis_of_linearization |
verified verified verified verified verified verified |
— |
| Pitchfork branches directly from jets at the origin | scalar-pitchfork-lean/pitchfork-branch-curves-of-jetscalar-pitchfork-lean/exists-branch-eventually-of-jet |
ScalarPitchfork.pitchfork_branch_curves_of_jetScalarPitchfork.exists_branch_eventually_of_jet |
verified verified |
— |
| Estimates at a single nontrivial equilibrium | scalar-pitchfork-lean/perturbed-equilibrium-corescalar-pitchfork-lean/equilibrium-corescalar-pitchfork-lean/exists-pos-equilibriumscalar-pitchfork-lean/nonzero-equilibrium-eq-branch |
ScalarPitchfork.perturbed_equilibrium_coreScalarPitchfork.equilibrium_coreScalarPitchfork.exists_pos_equilibriumScalarPitchfork.nonzero_equilibrium_eq_branch |
verified verified verified verified |
— |
| Global alternatives under monotone profiles | scalar-pitchfork-lean/global-global-unbounded-of-monotonescalar-pitchfork-lean/global-not-alt-complementscalar-pitchfork-lean/global-not-alt-other-trivialscalar-pitchfork-lean/global-not-is-compact-of-alternativesscalar-pitchfork-lean/global-is-compact-slicescalar-pitchfork-lean/global-subset-of-rel-clopenscalar-pitchfork-lean/global-strict-anti-on-of-rel-clopen |
ScalarPitchfork.Global.global_unbounded_of_monotoneScalarPitchfork.Global.not_altComplementScalarPitchfork.Global.not_altOtherTrivialScalarPitchfork.Global.not_isCompact_of_alternativesScalarPitchfork.Global.isCompact_sliceScalarPitchfork.Global.subset_of_relClopenScalarPitchfork.Global.strictAntiOn_of_relClopen |
verified verified verified verified verified verified verified |
— |
| Closedness and containment of one-sided components | scalar-pitchfork-lean/global-is-closed-connected-component-in-of-is-closedscalar-pitchfork-lean/global-is-closed-sdiff-of-is-open-preimagescalar-pitchfork-lean/global-parent-component-is-closedscalar-pitchfork-lean/global-unilateral-remainder-is-closedscalar-pitchfork-lean/global-retained-with-base-subset-parent-componentscalar-pitchfork-lean/global-retained-with-base-subset-unilateral-remainderscalar-pitchfork-lean/global-retained-with-base-subset-selected-componentscalar-pitchfork-lean/global-base-mem-selected-componentscalar-pitchfork-lean/global-selected-component-subset-solution-closure |
ScalarPitchfork.Global.isClosed_connectedComponentIn_of_isClosedScalarPitchfork.Global.isClosed_sdiff_of_isOpen_preimageScalarPitchfork.Global.parentComponent_isClosedScalarPitchfork.Global.unilateralRemainder_isClosedScalarPitchfork.Global.retainedWithBase_subset_parentComponentScalarPitchfork.Global.retainedWithBase_subset_unilateralRemainderScalarPitchfork.Global.retainedWithBase_subset_selectedComponentScalarPitchfork.Global.base_mem_selectedComponentScalarPitchfork.Global.selectedComponent_subset_solutionClosure |
verified verified verified verified verified verified verified verified verified |
— |
One line per main result of coverage.yaml. Ledger: the status lean-pkg claims ledger gives each claim, in the order of the claims; only verified means the recorded receipts close the claim.
Back to Verification.