The whole actual fixed-core fiber is a product of positive vectors
Abstract
The whole actual fixed-core fiber is a product of positive vectors.
Theorem 1.1 (An equivalence of the original actual fiber).
Lean statement: D5/S3/Combinatorics/Geometry/MiuraFiberEquiv.core_positive_vectors_equiv
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Geometry/MiuraFiberEquiv.core_positive_vectors_equiv (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every existing Core(a,b) member K and every rectangle m,n at least 2(a+b)-1, the product PositiveLengths(m-rowOccupied K,rowRuns K) times PositiveLengths(n-colOccupied K,colRuns K) is equivalent to the entire actual residual fiber reducing to K. The fiber retains the exact integer-valued normalized function and, for each physical side separately, equivalence of the assertion that all minima lie on that side. The inverse reads supported weights along an actual reduction and adds the compulsory first line of each isolated frozen run. Equal positive readouts imply equal weights, then equality of every actual height value. Conversely, the existing simultaneous indexed realization produces an actual residual function for every positive vector; exact occupied-position uniqueness reads back that same vector. The equivalence therefore includes all individual functions in the stated fiber.