Research proof index

Proposition 2.8 (a): μA (u, x ⊔ y) dominates the meet μA (u,x) ⊓ μA (u,y). This is obtained by taking an infimum and using prop2d8₀I to select the relevant branch.

Proposition 2.8 (b): under comparability or attainment, one of the two μA values is dominated by μA (u, x ⊔ y). This is a “one-sided dominance” conclusion that matches the alternative in the paper statement.

Proposition 3.12 (internal): explicit computation of μA (μ R M). For any strict interval I : N₁ < N₂, the auxiliary function μA evaluates to the singleton finset containing the minimal element of _μ R M I (in the S₀ R order). Proof idea: * Show that the intermediate submodule ker_of_quot_comp_localization I realizes an element of the defining...

Lower bound property of the minimal associated prime. Given an intermediate submodule N'' in an interval I, any associated prime of I.val.2 / N'' is ≥ the minimal element of _μ R M I. This uses the admitted equivalence between minimal associated primes and minimal support, plus the existence of minimal primes in the support.

Singleton lower bound for μA: the chosen minimal prime is ≤ every tail _μ. Specializing the previous lemma to the minimal element of a smaller interval, we obtain the order relation needed to show that the singleton {min} is the infimum in the definition of μA.

Proposition 3.4: nonemptiness of the set of stable breakpoints StI μ I. Under well-foundedness and the DCC hypothesis, and assuming convexity on I, the selection predicates S₁I/S₂I can be satisfied by a canonical choice produced by the recursion prop3d4₀func. API note: this provides the key existential input for later uniqueness/maximality argum...