CorrRank — Cycle Overlap Rank Rigidity (Lean Formalization)

This repository contains a Lean 4 formalization of the Cycle Overlap Rank (COR) rigidity framework.

The project formalizes the structural chain

COR → FO^k local type diversity → EntropyDepth lower bounds

for bounded-degree graphs.

Core Idea

For a graph G and radius R:

1. Each vertex v defines a local neighborhood (ball) B_R(v).
2. Neighborhoods are grouped by isomorphism type.
3. For each type τ we compute β₁(τ), the cycle rank (first homology dimension).
4. The Correlation Rank

CorrRank_R(G) = Σ_τ (β₁(τ))²

measures the total cycle interaction across local types.

Large CorrRank forces multiple FO^k local types, breaking FO^k-homogeneity.

Mathematical Role

This repository provides machine-checked components of the rigidity chain used in:

Cycle-Overlap Rigidity → FO^k Local Diversity → EntropyDepth Lower Bounds

within the broader Chronos / Unified Rigidity Framework program.

Repository Structure

src/ CorrRank/ CorrRankRigidity_Final.lean

Main definitions:

• Ball / BallGraph • BallIsoRel and BallSetoid • β₁ cycle rank • β₁_class quotient invariant • CorrRank_R(G)

All definitions avoid representative choice via Quotient.lift.

Build

Requirements:

Lean 4 + mathlib4

Build with:

lake update lake exe cache get lake build

Status

Mathematical core complete. Remaining work is API engineering around Sym2 edge representations.

Author

Inacio F. Vasquez Independent Researcher — Foundations of Physics & Mathematics

Lean proof portfolio classification

This repository is governed by docs/status/LEAN_PROOF_PORTFOLIO_CLASSIFICATION.md. Its role in the portfolio is explicitly classified as proof-facing, conditional frontier, infrastructure/documentation, or legacy/scaffold.

External status

This repository is governed by docs/status/EXTERNAL_STATUS_LOCK.md. Build success, CI success, dashboards, ledgers, axioms, admits, sorry, or placeholder witnesses do not constitute theorem-level closure.

Formal Status

Status: Toy Cardinality Model / Not a Real Bridge

Build status:

• A successful build means the checked root target compiles.
• It does not imply that the current theorem surface proves a substantive COR-to-EntropyDepth bridge.

Theorem status:

• The current theorem surface is toy-level.
• Current theorem class: toy cardinality bridge.
• Substantive COR-to-EntropyDepth bridge verified: no.
• The main quantities must be made mathematically independent before a real bridge theorem can be claimed.

Current status:

• Strongest verified theorem: toy cardinality implication only
• Weakest missing theorem: define nontrivial independent COR, FO-type-count, and EntropyDepth objects, then prove the bridge without definitional collapse
• Definitional-collapse boundary: docs/status/DEFINITIONAL_COLLAPSE_STATUS_2026_04_27.md