/* Provenance: Lean 4 → LambdaIR → MiniC → C
 * Source: HeytingLean.Algebra.HomotopyTower.Core + Stabilization
 * Theorem preserved: tower_stabilizes_of_finiteImage
 * Theorem preserved: boundary_mono
 * Theorem preserved: fixed_eq_of_le
 */

#include <stddef.h>
#include <stdbool.h>

/* A nucleus on a lattice: monotone, inflationary, idempotent, meet-preserving. */
typedef struct {
    int (*apply)(int x);
} Nucleus;

/* NucleusTower: ascending chain of nuclei. */
typedef struct {
    Nucleus *levels;
    size_t count;
} NucleusTower;

/* Check if x is a fixed point of nucleus J. */
static inline bool is_fixed(const Nucleus *J, int x) {
    return J->apply(x) == x;
}

/* Check if x is in the boundary (moved by J). */
static inline bool in_boundary(const Nucleus *J, int x) {
    return J->apply(x) != x;
}

/* Theorem preserved: fixed_eq_of_le
 * If J <= K pointwise and K fixes x, then J fixes x. */
static inline bool fixed_eq_of_le(const Nucleus *J, const Nucleus *K, int x) {
    if (K->apply(x) == x) {
        /* J(x) <= K(x) = x and x <= J(x) implies J(x) = x */
        return J->apply(x) == x;
    }
    return false;
}

/* Theorem preserved: tower_stabilizes_of_finiteImage
 * Find the stabilization index N such that level[n] = level[N] for all n >= N.
 * Returns N, or count-1 if the tower does not stabilize within its length. */
size_t stabilization_index(const NucleusTower *T, const int *test_points, size_t npoints) {
    for (size_t n = 0; n + 1 < T->count; n++) {
        bool same = true;
        for (size_t i = 0; i < npoints; i++) {
            if (T->levels[n].apply(test_points[i]) != T->levels[n + 1].apply(test_points[i])) {
                same = false;
                break;
            }
        }
        if (same) return n;
    }
    return T->count > 0 ? T->count - 1 : 0;
}