/* Provenance: Lean 4 → LambdaIR → MiniC → C
 * Source: HeytingLean.Algebra.HomotopyTower.PenumbraBridge + SpectralBridge
 * Theorem preserved: stableBoundary_not_boolean_of_bridge
 * Theorem preserved: stableBoundaryGap_nonempty_of_moved
 * Theorem preserved: spectralConverges_of_finiteImage
 */

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

/* Boundary nucleus: a nucleus viewed through the Hossenfelder gap interface. */
typedef struct {
    int (*apply)(int x);
} BoundaryNucleus;

/* Check if the boundary gap at point a is nonempty. */
static inline bool boundary_gap_nonempty(const BoundaryNucleus *N, int a) {
    return N->apply(a) != a;
}

/* Theorem preserved: stableBoundary_not_boolean_of_bridge
 * If a BooleanBoundaryBridge exists, the nucleus is not Boolean. */
bool stable_boundary_not_boolean(const BoundaryNucleus *N, const int *test_points,
                                  size_t npoints) {
    for (size_t i = 0; i < npoints; i++) {
        if (N->apply(test_points[i]) != test_points[i]) {
            return true; /* Non-Boolean: found a moved point */
        }
    }
    return false;
}

/* Theorem preserved: spectralConverges_of_finiteImage
 * Rank profile of a tower: rank(level(n)) for each n. */
typedef struct {
    size_t *ranks;
    size_t length;
} RankProfile;

/* Find spectral convergence index: first N where rank stabilizes. */
size_t spectral_convergence_index(const RankProfile *profile) {
    for (size_t n = 0; n + 1 < profile->length; n++) {
        if (profile->ranks[n] == profile->ranks[n + 1]) {
            /* Check if it stays constant */
            bool stable = true;
            for (size_t m = n + 1; m + 1 < profile->length; m++) {
                if (profile->ranks[m] != profile->ranks[m + 1]) {
                    stable = false;
                    break;
                }
            }
            if (stable) return n;
        }
    }
    return profile->length > 0 ? profile->length - 1 : 0;
}